C++: Convert to qlpack version of core range analysis.

This commit is contained in:
Anders Schack-Mulligen
2023-10-09 14:05:29 +02:00
parent 38274db205
commit ec39de20d8
11 changed files with 182 additions and 70 deletions

View File

@@ -7,6 +7,7 @@ library: true
upgrades: upgrades
dependencies:
codeql/dataflow: ${workspace}
codeql/rangeanalysis: ${workspace}
codeql/ssa: ${workspace}
codeql/tutorial: ${workspace}
codeql/util: ${workspace}

View File

@@ -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

View File

@@ -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;
@@ -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

View File

@@ -1,29 +0,0 @@
private import RangeAnalysisStage
module IntDelta implements DeltaSig {
class Delta = int;
bindingset[d]
bindingset[result]
float toFloat(Delta d) { result = d }
bindingset[d]
bindingset[result]
int toInt(Delta d) { result = d }
bindingset[n]
bindingset[result]
Delta fromInt(int n) { result = n }
bindingset[f]
Delta fromFloat(float f) {
result =
min(float diff, float res |
diff = (res - f) and res = f.ceil()
or
diff = (f - res) and res = f.floor()
|
res order by diff
)
}
}

View File

@@ -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

View File

@@ -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()`.
*

View File

@@ -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
@@ -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 }
@@ -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

View File

@@ -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()`.
*

View File

@@ -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`.
*/
@@ -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()
}
import 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))
}
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()
)
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()
)
}
}

View File

@@ -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.
*

View File

@@ -56,7 +56,7 @@
while (f3_get(n)) n+=2;
for (int i = 0; i < n; i += 2) {
range(i); // $ range=>=0 SPURIOUS: range="<=Phi: call to f3_get-1" range="<=Phi: call to f3_get-2"
range(i); // $ range=>=0 range="<=Phi: call to f3_get-2"
}
}