hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-23 15:55:18 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #14742 from aschackmull/rangeanalysis/share-util-3

Browse Source 
Java/C++/Rangeanalysis: Share more range analysis utility predicates.
This commit is contained in:
Anders Schack-Mulligen
2023-11-13 10:19:41 +01:00
committed by GitHub
parent f599c6d8a9 0d8986cfad
commit 00549e36ed
11 changed files with 127 additions and 232 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll
View File

@@ -26,11 +26,6 @@ module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
*/
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.

2
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
View File

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

5
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll
View File

@@ -58,11 +58,6 @@ module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
*/
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.

101
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
View File

@@ -9,107 +9,6 @@ private import RangeAnalysisImpl
private import ConstantAnalysis
module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
/**
* Gets an expression that equals `v - d`.
*/
private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
// There are various language-specific extension points that can be removed once we no longer
// expect to match the original Java implementation's results exactly.
result = v.getAUse() and delta = D::fromInt(0)
or
exists(D::Delta d1, SemConstantIntegerExpr c |
result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
delta = D::fromFloat(D::toFloat(d1) - c.getIntValue())
)
or
exists(SemSubExpr sub, D::Delta d1, SemConstantIntegerExpr c |
result = sub and
sub.getLeftOperand() = semSsaRead(v, d1) and
sub.getRightOperand() = c and
delta = D::fromFloat(D::toFloat(d1) + c.getIntValue())
)
or
result = v.(SemSsaExplicitUpdate).getSourceExpr() and
delta = D::fromFloat(0)
or
result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta)
or
result.(SemStoreExpr).getOperand() = semSsaRead(v, delta)
}
/**
* Gets a condition that tests whether `v` equals `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
pragma[nomagic]
SemGuard semEqFlowCond(
SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue
) {
exists(boolean eqpolarity |
result.isEquality(semSsaRead(v, delta), e, eqpolarity) and
(testIsTrue = true or testIsTrue = false) and
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 |
semImplies_v2(result, testIsTrue, semEqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
)
}
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate semSsaUpdateStep(SemSsaExplicitUpdate v, SemExpr e, D::Delta delta) {
exists(SemExpr defExpr | defExpr = v.getSourceExpr() |
defExpr.(SemCopyValueExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(SemStoreExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(SemAddOneExpr).getOperand() = e and delta = D::fromFloat(1)
or
defExpr.(SemSubOneExpr).getOperand() = e and delta = D::fromFloat(-1)
or
e = defExpr and
not (
defExpr instanceof SemCopyValueExpr or
defExpr instanceof SemStoreExpr or
defExpr instanceof SemAddOneExpr or
defExpr instanceof SemSubOneExpr
) and
delta = D::fromFloat(0)
)
}
/**
* 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.
*

18
java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
View File

@@ -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<Sem, IntDelta> {
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,20 +370,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
}
module Utils implements UtilSig<Sem, IntDelta> {
private import RangeUtils as RU
Sem::Guard semEqFlowCond(
Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
) {
result = RU::eqFlowCond(v, e, delta, isEq, testIsTrue)
}
predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, int delta) {
RU::ssaUpdateStep(v, e, delta)
}
predicate semValueFlowStep = RU::valueFlowStep/3;
Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) {
result = var.getSourceVariable().getType()
}

84
java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
View File

@@ -15,10 +15,16 @@ private predicate backEdge = U::backEdge/3;
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;
predicate eqFlowCond = U::eqFlowCond/5;
/**
* Holds if `v` is an input to `phi` that is not along a back edge, and the
* only other input to `phi` is a `null` value.
@@ -156,89 +162,13 @@ class ConstantStringExpr extends Expr {
string getStringValue() { constantStringExpr(this, result) }
}
/**
* Gets a condition that tests whether `v` equals `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
exists(boolean eqpolarity |
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
(testIsTrue = true or testIsTrue = false) and
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 |
implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
)
}
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate ssaUpdateStep(SsaExplicitUpdate v, Expr e, int delta) {
v.getDefiningExpr().(VariableAssign).getSource() = e and delta = 0
or
v.getDefiningExpr().(PostIncExpr).getExpr() = e and delta = 1
or
v.getDefiningExpr().(PreIncExpr).getExpr() = e and delta = 1
or
v.getDefiningExpr().(PostDecExpr).getExpr() = e and delta = -1
or
v.getDefiningExpr().(PreDecExpr).getExpr() = e and delta = -1
or
v.getDefiningExpr().(AssignOp) = e and delta = 0
}
/**
* 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
)
}

8
java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected
View File

@@ -4,9 +4,11 @@
| ModulusAnalysis.java:4:5:4:22 | ...=... | 0 | 43 | 0 |
| ModulusAnalysis.java:4:5:4:22 | c2 | 0 | 43 | 0 |
| ModulusAnalysis.java:4:20:4:21 | 43 | 0 | 43 | 0 |
| ModulusAnalysis.java:7:13:7:22 | eq | SSA init(i) | 3 | 0 |
| ModulusAnalysis.java:7:18:7:18 | i | SSA init(i) | 0 | 0 |
| ModulusAnalysis.java:7:18:7:22 | ... + ... | SSA init(i) | 3 | 0 |
| ModulusAnalysis.java:7:22:7:22 | 3 | 0 | 3 | 0 |
| ModulusAnalysis.java:9:13:9:29 | mul | 0 | 3 | 42 |
| ModulusAnalysis.java:9:19:9:20 | eq | SSA def(eq) | 0 | 0 |
| ModulusAnalysis.java:9:19:9:20 | eq | SSA init(i) | 3 | 0 |
| ModulusAnalysis.java:9:19:9:25 | ... * ... | 0 | 0 | 42 |
@@ -14,6 +16,7 @@
| ModulusAnalysis.java:9:24:9:25 | c1 | 0 | 42 | 0 |
| ModulusAnalysis.java:9:24:9:25 | c1 | SSA init(this.c1) | 0 | 0 |
| ModulusAnalysis.java:9:29:9:29 | 3 | 0 | 3 | 0 |
| ModulusAnalysis.java:11:13:11:21 | seven | 0 | 7 | 0 |
| ModulusAnalysis.java:11:21:11:21 | 7 | 0 | 7 | 0 |
| ModulusAnalysis.java:12:13:12:15 | mul | 0 | 3 | 42 |
| ModulusAnalysis.java:12:13:12:15 | mul | SSA def(mul) | 0 | 0 |
@@ -24,6 +27,7 @@
| ModulusAnalysis.java:13:32:13:34 | mul | 0 | 3 | 42 |
| ModulusAnalysis.java:13:32:13:34 | mul | 0 | 7 | 43 |
| ModulusAnalysis.java:13:32:13:34 | mul | SSA def(mul) | 0 | 0 |
| ModulusAnalysis.java:16:13:18:23 | j | 0 | 3 | 4 |
| ModulusAnalysis.java:16:17:18:23 | ...?...:... | 0 | 3 | 4 |
| ModulusAnalysis.java:17:15:17:15 | i | SSA init(i) | 0 | 0 |
| ModulusAnalysis.java:17:15:17:19 | ... * ... | 0 | 0 | 4 |
@@ -66,6 +70,7 @@
| ModulusAnalysis.java:26:32:26:36 | ... - ... | SSA init(x) | 35 | 42 |
| ModulusAnalysis.java:26:36:26:36 | y | 0 | 7 | 42 |
| ModulusAnalysis.java:26:36:26:36 | y | SSA init(y) | 0 | 0 |
| ModulusAnalysis.java:29:13:29:35 | l | 0 | 1 | 4 |
| ModulusAnalysis.java:29:17:29:26 | arr.length | SSA impl upd[untracked](arr.length) | 0 | 0 |
| ModulusAnalysis.java:29:17:29:30 | ... * ... | 0 | 0 | 4 |
| ModulusAnalysis.java:29:17:29:35 | ... - ... | 0 | 1 | 4 |
@@ -104,12 +109,14 @@
| ModulusAnalysis.java:49:25:49:25 | 3 | 0 | 3 | 0 |
| ModulusAnalysis.java:50:32:50:32 | x | 0 | 3 | 16 |
| ModulusAnalysis.java:50:32:50:32 | x | SSA init(x) | 0 | 0 |
| ModulusAnalysis.java:56:18:56:22 | i | 0 | 0 | 0 |
| ModulusAnalysis.java:56:22:56:22 | 0 | 0 | 0 | 0 |
| ModulusAnalysis.java:56:25:56:25 | i | SSA phi(i) | 0 | 0 |
| ModulusAnalysis.java:56:29:56:31 | cap | SSA init(cap) | 0 | 0 |
| ModulusAnalysis.java:56:34:56:34 | i | SSA phi(i) | 0 | 0 |
| ModulusAnalysis.java:56:34:56:36 | ...++ | SSA phi(i) | 0 | 0 |
| ModulusAnalysis.java:57:32:57:32 | i | SSA phi(i) | 0 | 0 |
| ModulusAnalysis.java:59:18:59:22 | j | 0 | 0 | 0 |
| ModulusAnalysis.java:59:22:59:22 | 0 | 0 | 0 | 0 |
| ModulusAnalysis.java:59:25:59:25 | j | SSA phi(j) | 0 | 0 |
| ModulusAnalysis.java:59:29:59:31 | cap | SSA init(cap) | 0 | 0 |
@@ -117,6 +124,7 @@
| ModulusAnalysis.java:59:34:59:39 | ...+=... | SSA phi(j) | 1 | 0 |
| ModulusAnalysis.java:59:39:59:39 | 1 | 0 | 1 | 0 |
| ModulusAnalysis.java:60:32:60:32 | j | SSA phi(j) | 0 | 0 |
| ModulusAnalysis.java:62:18:62:22 | k | 0 | 0 | 0 |
| ModulusAnalysis.java:62:22:62:22 | 0 | 0 | 0 | 0 |
| ModulusAnalysis.java:62:25:62:25 | k | 0 | 0 | 3 |
| ModulusAnalysis.java:62:25:62:25 | k | SSA def(k) | 0 | 3 |

12
java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected
View File

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

6
shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
View File

@@ -30,11 +30,11 @@ module ModulusAnalysis<
*/
pragma[nomagic]
private predicate valueFlowStepSsa(Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, int delta) {
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
ssaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
or
exists(Sem::Guard guard, boolean testIsTrue |
hasReadOfVarInlineLate(pos, v) and
guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
)
}
@@ -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

42
shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
View File

@@ -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<Semantic Sem, DeltaSig D> {
*/
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,14 +304,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
}
signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
Sem::Guard semEqFlowCond(
Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
);
predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, DeltaParam::Delta delta);
predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta);
/**
* Gets the type used to track the specified source variable's range information.
*
@@ -447,7 +439,7 @@ module RangeStage<
*/
cached
predicate possibleReason(Sem::Guard guard) {
guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _)
guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)
}
}
@@ -609,7 +601,7 @@ module RangeStage<
testIsTrue0)
)
or
result = semEqFlowCond(v, e, delta, true, testIsTrue) and
result = eqFlowCond(v, e, delta, true, testIsTrue) and
(upper = true or upper = false)
or
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
@@ -630,7 +622,7 @@ module RangeStage<
Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
) {
exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
guardEq = semEqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
delta = D::toFloat(d2) - D::toFloat(d1) and
guardEq.directlyControls(result, eqIsTrue)
)
@@ -675,7 +667,7 @@ module RangeStage<
Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, D::Delta delta, boolean upper,
SemReason reason
) {
semSsaUpdateStep(v, e, delta) and
ssaUpdateStep(v, e, delta) and
pos.hasReadOfVar(v) and
(upper = true or upper = false) and
reason = TSemNoReason()
@@ -695,7 +687,7 @@ module RangeStage<
getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and
exists(Sem::Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
guard = eqFlowCond(v, e, delta, false, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
reason = TSemCondReason(guard)
)
@@ -717,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
@@ -1350,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)
@@ -1370,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)
}
@@ -1386,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, _,
_)
}

76
shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll
View File

@@ -37,6 +37,82 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
result.(CopyValueExpr).getOperand() = ssaRead(v, delta)
}
/**
* Gets a condition that tests whether `v` equals `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
pragma[nomagic]
Guard eqFlowCond(SsaVariable v, Expr e, D::Delta delta, boolean isEq, boolean testIsTrue) {
exists(boolean eqpolarity |
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
(testIsTrue = true or testIsTrue = false) and
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 |
implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
)
}
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate ssaUpdateStep(SsaExplicitUpdate v, Expr e, D::Delta delta) {
exists(Expr defExpr | defExpr = v.getDefiningExpr() |
defExpr.(CopyValueExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(PostIncExpr).getOperand() = e and delta = D::fromFloat(1)
or
defExpr.(PreIncExpr).getOperand() = e and delta = D::fromFloat(1)
or
defExpr.(PostDecExpr).getOperand() = e and delta = D::fromFloat(-1)
or
defExpr.(PreDecExpr).getOperand() = e and delta = D::fromFloat(-1)
or
e = defExpr and
not (
defExpr instanceof CopyValueExpr or
defExpr instanceof PostIncExpr or
defExpr instanceof PreIncExpr or
defExpr instanceof PostDecExpr or
defExpr instanceof PreDecExpr
) and
delta = D::fromFloat(0)
)
}
/**
* 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)