Skip to content

Commit

Permalink
Merge pull request #14588 from aschackmull/shared/rangeanalysis
Browse files Browse the repository at this point in the history
C++/Java: Share core range analysis
  • Loading branch information
MathiasVP authored Oct 26, 2023
2 parents 867a390 + 6882504 commit 30ecb4b
Show file tree
Hide file tree
Showing 22 changed files with 980 additions and 1,106 deletions.
1 change: 1 addition & 0 deletions cpp/ql/lib/qlpack.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ library: true
upgrades: upgrades
dependencies:
codeql/dataflow: ${workspace}
codeql/rangeanalysis: ${workspace}
codeql/ssa: ${workspace}
codeql/tutorial: ${workspace}
codeql/util: ${workspace}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,18 @@ class SemLocation instanceof Location {
*/
string toString() { result = super.toString() }

/** Gets the 1-based line number (inclusive) where this location starts. */
int getStartLine() { result = super.getStartLine() }

/** Gets the 1-based column number (inclusive) where this location starts. */
int getStartColumn() { result = super.getStartColumn() }

/** Gets the 1-based line number (inclusive) where this location ends. */
int getEndLine() { result = super.getEndLine() }

/** Gets the 1-based column number (inclusive) where this location ends. */
int getEndColumn() { result = super.getEndColumn() }

/**
* Holds if this element is at the specified location.
* The location spans column `startcolumn` of line `startline` to
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
private import RangeAnalysisStage
private import RangeAnalysisImpl
private import codeql.rangeanalysis.RangeAnalysis
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType

module FloatDelta implements DeltaSig {
class Delta = float;
Expand All @@ -20,7 +22,7 @@ module FloatDelta implements DeltaSig {
Delta fromFloat(float f) { result = f }
}

module FloatOverflow implements OverflowSig<FloatDelta> {
module FloatOverflow implements OverflowSig<Sem, FloatDelta> {
predicate semExprDoesNotOverflow(boolean positively, SemExpr expr) {
exists(float lb, float ub, float delta |
typeBounds(expr.getSemType(), lb, ub) and
Expand Down

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,13 @@

private import ModulusAnalysisSpecific::Private
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
private import ConstantAnalysis
private import RangeUtils
private import RangeAnalysisStage
private import codeql.rangeanalysis.RangeAnalysis
private import RangeAnalysisImpl

module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
module ModulusAnalysis<DeltaSig D, BoundSig<SemLocation, Sem, D> Bounds, UtilSig<Sem, D> U> {
pragma[nomagic]
private predicate valueFlowStepSsaEqFlowCond(
SemSsaReadPosition pos, SemSsaVariable v, SemExpr e, int delta
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,11 @@
*/

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisStage
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import RangeAnalysisImpl
private import codeql.rangeanalysis.RangeAnalysis

module CppLangImplConstant implements LangSig<FloatDelta> {
module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
Expand Down
Original file line number Diff line number Diff line change
@@ -1,13 +1,104 @@
private import RangeAnalysisStage
private import RangeAnalysisConstantSpecific
private import RangeAnalysisRelativeSpecific
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import RangeUtils
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticCFG
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticGuard
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound as SemanticBound
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticSSA
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType as SemanticType
private import SemanticType
private import codeql.rangeanalysis.RangeAnalysis
private import ConstantAnalysis as ConstantAnalysis

module ConstantBounds implements BoundSig<FloatDelta> {
module Sem implements Semantic {
class Expr = SemExpr;

class ConstantIntegerExpr = ConstantAnalysis::SemConstantIntegerExpr;

class BinaryExpr = SemBinaryExpr;

class AddExpr = SemAddExpr;

class SubExpr = SemSubExpr;

class MulExpr = SemMulExpr;

class DivExpr = SemDivExpr;

class RemExpr = SemRemExpr;

class BitAndExpr = SemBitAndExpr;

class BitOrExpr = SemBitOrExpr;

class ShiftLeftExpr = SemShiftLeftExpr;

class ShiftRightExpr = SemShiftRightExpr;

class ShiftRightUnsignedExpr = SemShiftRightUnsignedExpr;

class RelationalExpr = SemRelationalExpr;

class UnaryExpr = SemUnaryExpr;

class ConvertExpr = SemConvertExpr;

class BoxExpr = SemBoxExpr;

class UnboxExpr = SemUnboxExpr;

class NegateExpr = SemNegateExpr;

class AddOneExpr = SemAddOneExpr;

class SubOneExpr = SemSubOneExpr;

class ConditionalExpr = SemConditionalExpr;

class BasicBlock = SemBasicBlock;

class Guard = SemGuard;

predicate implies_v2 = semImplies_v2/4;

predicate guardDirectlyControlsSsaRead = semGuardDirectlyControlsSsaRead/3;

class Type = SemType;

class IntegerType = SemIntegerType;

class FloatingPointType = SemFloatingPointType;

class AddressType = SemAddressType;

class SsaVariable = SemSsaVariable;

class SsaPhiNode = SemSsaPhiNode;

class SsaExplicitUpdate = SemSsaExplicitUpdate;

class SsaReadPosition = SemSsaReadPosition;

class SsaReadPositionPhiInputEdge = SemSsaReadPositionPhiInputEdge;

class SsaReadPositionBlock = SemSsaReadPositionBlock;

predicate backEdge = semBackEdge/3;

predicate conversionCannotOverflow(Type fromType, Type toType) {
SemanticType::conversionCannotOverflow(fromType, toType)
}
}

module SignAnalysis implements SignAnalysisSig<Sem> {
private import SignAnalysisCommon as SA
import SA::SignAnalysis<FloatDelta, Util>
}

module ConstantBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
SemBound() {
this instanceof SemanticBound::SemZeroBound
Expand All @@ -29,7 +120,7 @@ module ConstantBounds implements BoundSig<FloatDelta> {
}
}

module RelativeBounds implements BoundSig<FloatDelta> {
module RelativeBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
SemBound() { not this instanceof SemanticBound::SemZeroBound }

Expand All @@ -47,13 +138,38 @@ module RelativeBounds implements BoundSig<FloatDelta> {
}
}

module AllBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
string toString() { result = super.toString() }

SemLocation getLocation() { result = super.getLocation() }

SemExpr getExpr(float delta) { result = super.getExpr(delta) }
}

class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }

class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
}
}

private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
class ModBound = AllBounds::SemBound;

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.ModulusAnalysis as MA
import MA::ModulusAnalysis<FloatDelta, AllBounds, Util>
}

module Util = RangeUtil<FloatDelta, CppLangImplConstant>;

module ConstantStage =
RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
RangeUtil<FloatDelta, CppLangImplConstant>>;
RangeStage<SemLocation, Sem, FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
SignAnalysis, ModulusAnalysisInstantiated, Util>;

module RelativeStage =
RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
RangeUtil<FloatDelta, CppLangImplRelative>>;
RangeStage<SemLocation, Sem, FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
SignAnalysis, ModulusAnalysisInstantiated, Util>;

private newtype TSemReason =
TSemNoReason() or
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,12 @@
*/

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisStage
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.IntDelta
private import RangeAnalysisImpl
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
private import codeql.rangeanalysis.RangeAnalysis

module CppLangImplRelative implements LangSig<FloatDelta> {
module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,11 @@

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisRelativeSpecific
private import RangeAnalysisStage as Range
private import codeql.rangeanalysis.RangeAnalysis
private import RangeAnalysisImpl
private import ConstantAnalysis

module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::UtilSig<D> {
module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
/**
* Gets an expression that equals `v - d`.
*/
Expand Down Expand Up @@ -138,27 +139,33 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
or
not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
}
}

/**
* Holds if `rix` is the number of input edges to `phi`.
*/
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
import Ranking
}

/**
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
* in an arbitrary 1-based numbering of the input edges to `phi`.
*/
predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
)
import Ranking

module Ranking {
/**
* Holds if `rix` is the number of input edges to `phi`.
*/
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}

/**
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
* in an arbitrary 1-based numbering of the input edges to `phi`.
*/
predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,15 @@
* three-valued domain `{negative, zero, positive}`.
*/

private import RangeAnalysisStage
private import codeql.rangeanalysis.RangeAnalysis
private import RangeAnalysisImpl
private import SignAnalysisSpecific as Specific
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import ConstantAnalysis
private import RangeUtils
private import Sign

module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
/**
* An SSA definition for which the analysis can compute the sign.
*
Expand Down Expand Up @@ -507,4 +508,16 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
not semExprSign(e) = TPos() and
not semExprSign(e) = TZero()
}

/**
* Holds if `e` may have positive values. This does not rule out the
* possibility for negative values.
*/
predicate semMayBePositive(SemExpr e) { semExprSign(e) = TPos() }

/**
* Holds if `e` may have negative values. This does not rule out the
* possibility for positive values.
*/
predicate semMayBeNegative(SemExpr e) { semExprSign(e) = TNeg() }
}
Loading

0 comments on commit 30ecb4b

Please sign in to comment.