diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll index d4883b02530..48461afc440 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll @@ -26,11 +26,6 @@ module CppLangImplConstant implements LangSig { */ predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() } - /** - * Holds if the value of `dest` is known to be `src + delta`. - */ - predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { none() } - /** * Gets the type that range analysis should use to track the result of the specified expression, * if a type other than the original type of the expression is to be used. diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll index 4957f700ac6..ca4560a1ff5 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll @@ -94,6 +94,8 @@ module Sem implements Semantic { class SsaExplicitUpdate = SemSsaExplicitUpdate; + predicate additionalValueFlowStep(SemExpr dest, SemExpr src, int delta) { none() } + predicate conversionCannotOverflow(Type fromType, Type toType) { SemanticType::conversionCannotOverflow(fromType, toType) } diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll index 29cef82579c..524bb08e261 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll @@ -58,11 +58,6 @@ module CppLangImplRelative implements LangSig { */ predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() } - /** - * Holds if the value of `dest` is known to be `src + delta`. - */ - predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { none() } - /** * Gets the type that range analysis should use to track the result of the specified expression, * if a type other than the original type of the expression is to be used. diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll index 229c2270e9e..857f69228da 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll @@ -9,33 +9,6 @@ private import RangeAnalysisImpl private import ConstantAnalysis module RangeUtil Lang> implements UtilSig { - /** - * Holds if `e1 + delta` equals `e2`. - */ - predicate semValueFlowStep(SemExpr e2, SemExpr e1, D::Delta delta) { - e2.(SemCopyValueExpr).getOperand() = e1 and delta = D::fromFloat(0) - or - e2.(SemStoreExpr).getOperand() = e1 and delta = D::fromFloat(0) - or - e2.(SemAddOneExpr).getOperand() = e1 and delta = D::fromFloat(1) - or - e2.(SemSubOneExpr).getOperand() = e1 and delta = D::fromFloat(-1) - or - Lang::additionalValueFlowStep(e2, e1, delta) - or - exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) | - D::fromInt(x.(SemConstantIntegerExpr).getIntValue()) = delta - ) - or - exists(SemExpr x, SemSubExpr sub | - e2 = sub and - sub.getLeftOperand() = e1 and - sub.getRightOperand() = x - | - D::fromInt(-x.(SemConstantIntegerExpr).getIntValue()) = delta - ) - } - /** * Gets the type used to track the specified expression's range information. * diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index b4029245d65..d0335efacec 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -255,6 +255,8 @@ module Sem implements Semantic { Expr getDefiningExpr() { result = super.getDefiningExpr() } } + predicate additionalValueFlowStep = RU::additionalValueFlowStep/3; + predicate conversionCannotOverflow = safeCast/2; } @@ -360,8 +362,6 @@ module JavaLangImpl implements LangSig { predicate ignoreExprBound(Sem::Expr e) { none() } - predicate additionalValueFlowStep(Sem::Expr dest, Sem::Expr src, int delta) { none() } - Sem::Type getAlternateType(Sem::Expr e) { none() } Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var) { none() } @@ -370,10 +370,6 @@ module JavaLangImpl implements LangSig { } module Utils implements UtilSig { - private import RangeUtils as RU - - predicate semValueFlowStep = RU::valueFlowStep/3; - Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) { result = var.getSourceVariable().getType() } diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll index 6261a601418..be7f73fe766 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll @@ -17,6 +17,8 @@ predicate ssaRead = U::ssaRead/2; predicate ssaUpdateStep = U::ssaUpdateStep/3; +predicate valueFlowStep = U::valueFlowStep/3; + predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3; predicate guardControlsSsaRead = U::guardControlsSsaRead/3; @@ -163,50 +165,10 @@ class ConstantStringExpr extends Expr { /** * Holds if `e1 + delta` equals `e2`. */ -predicate valueFlowStep(Expr e2, Expr e1, int delta) { - e2.(AssignExpr).getSource() = e1 and delta = 0 - or - e2.(PlusExpr).getExpr() = e1 and delta = 0 - or - e2.(PostIncExpr).getExpr() = e1 and delta = 0 - or - e2.(PostDecExpr).getExpr() = e1 and delta = 0 - or - e2.(PreIncExpr).getExpr() = e1 and delta = 1 - or - e2.(PreDecExpr).getExpr() = e1 and delta = -1 - or +predicate additionalValueFlowStep(Expr e2, Expr e1, int delta) { exists(ArrayCreationExpr a | arrayLengthDef(e2, a) and a.getDimension(0) = e1 and delta = 0 ) - or - exists(Expr x | - e2.(AddExpr).hasOperands(e1, x) - or - exists(AssignAddExpr add | add = e2 | - add.getDest() = e1 and add.getRhs() = x - or - add.getDest() = x and add.getRhs() = e1 - ) - | - x.(ConstantIntegerExpr).getIntValue() = delta - ) - or - exists(Expr x | - exists(SubExpr sub | - e2 = sub and - sub.getLeftOperand() = e1 and - sub.getRightOperand() = x - ) - or - exists(AssignSubExpr sub | - e2 = sub and - sub.getDest() = e1 and - sub.getRhs() = x - ) - | - x.(ConstantIntegerExpr).getIntValue() = -delta - ) } diff --git a/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected b/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected index 9fbe076dfe9..6b9d75a8bc7 100644 --- a/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected +++ b/java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected @@ -59,6 +59,7 @@ | A.java:12:16:12:20 | ... + ... | SSA init(y) | 1 | upper | NoReason | | A.java:12:20:12:20 | 1 | 0 | 1 | lower | NoReason | | A.java:12:20:12:20 | 1 | 0 | 1 | upper | NoReason | +| A.java:13:13:13:23 | sum | SSA init(y) | 400 | upper | NoReason | | A.java:13:19:13:19 | x | 0 | 400 | upper | ... > ... | | A.java:13:19:13:19 | x | SSA init(x) | 0 | lower | NoReason | | A.java:13:19:13:19 | x | SSA init(x) | 0 | upper | NoReason | @@ -72,6 +73,17 @@ | A.java:15:13:15:13 | y | SSA init(y) | 0 | upper | NoReason | | A.java:15:17:15:19 | 300 | 0 | 300 | lower | NoReason | | A.java:15:17:15:19 | 300 | 0 | 300 | upper | NoReason | +| A.java:16:15:16:25 | sum | 0 | 603 | lower | ... > ... | +| A.java:16:15:16:25 | sum | 0 | 799 | upper | ... != ... | +| A.java:16:15:16:25 | sum | 0 | 799 | upper | ... > ... | +| A.java:16:15:16:25 | sum | SSA init(x) | 301 | lower | ... != ... | +| A.java:16:15:16:25 | sum | SSA init(x) | 301 | lower | NoReason | +| A.java:16:15:16:25 | sum | SSA init(x) | 399 | upper | ... != ... | +| A.java:16:15:16:25 | sum | SSA init(x) | 399 | upper | NoReason | +| A.java:16:15:16:25 | sum | SSA init(y) | 302 | lower | ... != ... | +| A.java:16:15:16:25 | sum | SSA init(y) | 302 | lower | NoReason | +| A.java:16:15:16:25 | sum | SSA init(y) | 400 | upper | ... != ... | +| A.java:16:15:16:25 | sum | SSA init(y) | 400 | upper | NoReason | | A.java:16:21:16:21 | x | 0 | 302 | lower | ... > ... | | A.java:16:21:16:21 | x | 0 | 400 | upper | ... > ... | | A.java:16:21:16:21 | x | SSA init(x) | 0 | lower | NoReason | diff --git a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll index 773937bc73d..a94e81a942e 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll @@ -260,7 +260,7 @@ module ModulusAnalysis< or exists(Sem::Expr mid, int val0, int delta | exprModulus(mid, b, val0, mod) and - U::semValueFlowStep(e, mid, D::fromInt(delta)) and + valueFlowStep(e, mid, D::fromInt(delta)) and val = remainder(val0 + delta, mod) ) or diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index 5f32aeec5c0..cc41384b5f3 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -203,6 +203,11 @@ signature module Semantic { Expr getDefiningExpr(); } + /** + * Holds if the value of `dest` is known to be `src + delta`. + */ + predicate additionalValueFlowStep(Expr dest, Expr src, int delta); + predicate conversionCannotOverflow(Type fromType, Type toType); } @@ -277,11 +282,6 @@ signature module LangSig { */ predicate ignoreExprBound(Sem::Expr e); - /** - * Holds if the value of `dest` is known to be `src + delta`. - */ - predicate additionalValueFlowStep(Sem::Expr dest, Sem::Expr src, D::Delta delta); - /** * Gets the type that range analysis should use to track the result of the specified expression, * if a type other than the original type of the expression is to be used. @@ -304,8 +304,6 @@ signature module LangSig { } signature module UtilSig { - predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta); - /** * Gets the type used to track the specified source variable's range information. * @@ -711,7 +709,7 @@ module RangeStage< * - `upper = false` : `e2 >= e1 + delta` */ private predicate boundFlowStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper) { - semValueFlowStep(e2, e1, delta) and + valueFlowStep(e2, e1, delta) and (upper = true or upper = false) or e2.(SafeCastExpr).getOperand() = e1 and @@ -1344,8 +1342,8 @@ module RangeStage< Sem::AddExpr add, boolean upper, SemBound b, boolean isLeft, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, SemReason reason ) { - // `semValueFlowStep` already handles the case where one of the operands is a constant. - not semValueFlowStep(add, _, _) and + // `valueFlowStep` already handles the case where one of the operands is a constant. + not valueFlowStep(add, _, _) and ( isLeft = true and bounded(add.getLeftOperand(), b, delta, upper, fromBackEdge, origdelta, reason) @@ -1364,8 +1362,8 @@ module RangeStage< Sem::SubExpr sub, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, SemReason reason ) { - // `semValueFlowStep` already handles the case where one of the operands is a constant. - not semValueFlowStep(sub, _, _) and + // `valueFlowStep` already handles the case where one of the operands is a constant. + not valueFlowStep(sub, _, _) and bounded(sub.getLeftOperand(), b, delta, upper, fromBackEdge, origdelta, reason) } @@ -1380,8 +1378,8 @@ module RangeStage< private predicate boundedSubOperandRight( Sem::SubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge ) { - // `semValueFlowStep` already handles the case where one of the operands is a constant. - not semValueFlowStep(sub, _, _) and + // `valueFlowStep` already handles the case where one of the operands is a constant. + not valueFlowStep(sub, _, _) and bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge, _, _) } diff --git a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll index aa09c94414e..dc1014a886e 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll @@ -84,6 +84,35 @@ module MakeUtils { ) } + /** + * Holds if `e1 + delta` equals `e2`. + */ + predicate valueFlowStep(Expr e2, Expr e1, D::Delta delta) { + e2.(CopyValueExpr).getOperand() = e1 and delta = D::fromFloat(0) + or + e2.(PostIncExpr).getOperand() = e1 and delta = D::fromFloat(0) + or + e2.(PostDecExpr).getOperand() = e1 and delta = D::fromFloat(0) + or + e2.(PreIncExpr).getOperand() = e1 and delta = D::fromFloat(1) + or + e2.(PreDecExpr).getOperand() = e1 and delta = D::fromFloat(-1) + or + additionalValueFlowStep(e2, e1, D::toInt(delta)) + or + exists(Expr x | e2.(AddExpr).hasOperands(e1, x) | + D::fromInt(x.(ConstantIntegerExpr).getIntValue()) = delta + ) + or + exists(Expr x, SubExpr sub | + e2 = sub and + sub.getLeftOperand() = e1 and + sub.getRightOperand() = x + | + D::fromInt(-x.(ConstantIntegerExpr).getIntValue()) = delta + ) + } + private newtype TSsaReadPosition = TSsaReadPositionBlock(BasicBlock bb) { exists(SsaVariable v | v.getAUse().getBasicBlock() = bb)