Skip to content

Commit 00549e3

Browse files
aschackmullaschackmull
authored
Merge pull request github#14742 from aschackmull/rangeanalysis/share-util-3
Java/C++/Rangeanalysis: Share more range analysis utility predicates.
2 parents f599c6d + 0d8986c commit 00549e3

File tree

11 files changed

+127
-232
lines changed

11 files changed

+127
-232
lines changed

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,6 @@ module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
2626
*/
2727
predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
2828

29-
/**
30-
* Holds if the value of `dest` is known to be `src + delta`.
31-
*/
32-
predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { none() }
33-
3429
/**
3530
* Gets the type that range analysis should use to track the result of the specified expression,
3631
* if a type other than the original type of the expression is to be used.

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,8 @@ module Sem implements Semantic {
9494

9595
class SsaExplicitUpdate = SemSsaExplicitUpdate;
9696

97+
predicate additionalValueFlowStep(SemExpr dest, SemExpr src, int delta) { none() }
98+
9799
predicate conversionCannotOverflow(Type fromType, Type toType) {
98100
SemanticType::conversionCannotOverflow(fromType, toType)
99101
}

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -58,11 +58,6 @@ module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
5858
*/
5959
predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
6060

61-
/**
62-
* Holds if the value of `dest` is known to be `src + delta`.
63-
*/
64-
predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { none() }
65-
6661
/**
6762
* Gets the type that range analysis should use to track the result of the specified expression,
6863
* if a type other than the original type of the expression is to be used.

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll

Lines changed: 0 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -9,107 +9,6 @@ private import RangeAnalysisImpl
99
private import ConstantAnalysis
1010

1111
module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
12-
/**
13-
* Gets an expression that equals `v - d`.
14-
*/
15-
private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
16-
// There are various language-specific extension points that can be removed once we no longer
17-
// expect to match the original Java implementation's results exactly.
18-
result = v.getAUse() and delta = D::fromInt(0)
19-
or
20-
exists(D::Delta d1, SemConstantIntegerExpr c |
21-
result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
22-
delta = D::fromFloat(D::toFloat(d1) - c.getIntValue())
23-
)
24-
or
25-
exists(SemSubExpr sub, D::Delta d1, SemConstantIntegerExpr c |
26-
result = sub and
27-
sub.getLeftOperand() = semSsaRead(v, d1) and
28-
sub.getRightOperand() = c and
29-
delta = D::fromFloat(D::toFloat(d1) + c.getIntValue())
30-
)
31-
or
32-
result = v.(SemSsaExplicitUpdate).getSourceExpr() and
33-
delta = D::fromFloat(0)
34-
or
35-
result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta)
36-
or
37-
result.(SemStoreExpr).getOperand() = semSsaRead(v, delta)
38-
}
39-
40-
/**
41-
* Gets a condition that tests whether `v` equals `e + delta`.
42-
*
43-
* If the condition evaluates to `testIsTrue`:
44-
* - `isEq = true` : `v == e + delta`
45-
* - `isEq = false` : `v != e + delta`
46-
*/
47-
pragma[nomagic]
48-
SemGuard semEqFlowCond(
49-
SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue
50-
) {
51-
exists(boolean eqpolarity |
52-
result.isEquality(semSsaRead(v, delta), e, eqpolarity) and
53-
(testIsTrue = true or testIsTrue = false) and
54-
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
55-
)
56-
or
57-
exists(boolean testIsTrue0 |
58-
semImplies_v2(result, testIsTrue, semEqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
59-
)
60-
}
61-
62-
/**
63-
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
64-
*/
65-
predicate semSsaUpdateStep(SemSsaExplicitUpdate v, SemExpr e, D::Delta delta) {
66-
exists(SemExpr defExpr | defExpr = v.getSourceExpr() |
67-
defExpr.(SemCopyValueExpr).getOperand() = e and delta = D::fromFloat(0)
68-
or
69-
defExpr.(SemStoreExpr).getOperand() = e and delta = D::fromFloat(0)
70-
or
71-
defExpr.(SemAddOneExpr).getOperand() = e and delta = D::fromFloat(1)
72-
or
73-
defExpr.(SemSubOneExpr).getOperand() = e and delta = D::fromFloat(-1)
74-
or
75-
e = defExpr and
76-
not (
77-
defExpr instanceof SemCopyValueExpr or
78-
defExpr instanceof SemStoreExpr or
79-
defExpr instanceof SemAddOneExpr or
80-
defExpr instanceof SemSubOneExpr
81-
) and
82-
delta = D::fromFloat(0)
83-
)
84-
}
85-
86-
/**
87-
* Holds if `e1 + delta` equals `e2`.
88-
*/
89-
predicate semValueFlowStep(SemExpr e2, SemExpr e1, D::Delta delta) {
90-
e2.(SemCopyValueExpr).getOperand() = e1 and delta = D::fromFloat(0)
91-
or
92-
e2.(SemStoreExpr).getOperand() = e1 and delta = D::fromFloat(0)
93-
or
94-
e2.(SemAddOneExpr).getOperand() = e1 and delta = D::fromFloat(1)
95-
or
96-
e2.(SemSubOneExpr).getOperand() = e1 and delta = D::fromFloat(-1)
97-
or
98-
Lang::additionalValueFlowStep(e2, e1, delta)
99-
or
100-
exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) |
101-
D::fromInt(x.(SemConstantIntegerExpr).getIntValue()) = delta
102-
)
103-
or
104-
exists(SemExpr x, SemSubExpr sub |
105-
e2 = sub and
106-
sub.getLeftOperand() = e1 and
107-
sub.getRightOperand() = x
108-
|
109-
D::fromInt(-x.(SemConstantIntegerExpr).getIntValue()) = delta
110-
)
111-
}
112-
11312
/**
11413
* Gets the type used to track the specified expression's range information.
11514
*

‎java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

Lines changed: 2 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -255,6 +255,8 @@ module Sem implements Semantic {
255255
Expr getDefiningExpr() { result = super.getDefiningExpr() }
256256
}
257257

258+
predicate additionalValueFlowStep = RU::additionalValueFlowStep/3;
259+
258260
predicate conversionCannotOverflow = safeCast/2;
259261
}
260262

@@ -360,8 +362,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
360362

361363
predicate ignoreExprBound(Sem::Expr e) { none() }
362364

363-
predicate additionalValueFlowStep(Sem::Expr dest, Sem::Expr src, int delta) { none() }
364-
365365
Sem::Type getAlternateType(Sem::Expr e) { none() }
366366

367367
Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var) { none() }
@@ -370,20 +370,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
370370
}
371371

372372
module Utils implements UtilSig<Sem, IntDelta> {
373-
private import RangeUtils as RU
374-
375-
Sem::Guard semEqFlowCond(
376-
Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
377-
) {
378-
result = RU::eqFlowCond(v, e, delta, isEq, testIsTrue)
379-
}
380-
381-
predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, int delta) {
382-
RU::ssaUpdateStep(v, e, delta)
383-
}
384-
385-
predicate semValueFlowStep = RU::valueFlowStep/3;
386-
387373
Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) {
388374
result = var.getSourceVariable().getType()
389375
}

‎java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll

Lines changed: 7 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,16 @@ private predicate backEdge = U::backEdge/3;
1515

1616
predicate ssaRead = U::ssaRead/2;
1717

18+
predicate ssaUpdateStep = U::ssaUpdateStep/3;
19+
20+
predicate valueFlowStep = U::valueFlowStep/3;
21+
1822
predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
1923

2024
predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
2125

26+
predicate eqFlowCond = U::eqFlowCond/5;
27+
2228
/**
2329
* Holds if `v` is an input to `phi` that is not along a back edge, and the
2430
* only other input to `phi` is a `null` value.
@@ -156,89 +162,13 @@ class ConstantStringExpr extends Expr {
156162
string getStringValue() { constantStringExpr(this, result) }
157163
}
158164

159-
/**
160-
* Gets a condition that tests whether `v` equals `e + delta`.
161-
*
162-
* If the condition evaluates to `testIsTrue`:
163-
* - `isEq = true` : `v == e + delta`
164-
* - `isEq = false` : `v != e + delta`
165-
*/
166-
Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
167-
exists(boolean eqpolarity |
168-
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
169-
(testIsTrue = true or testIsTrue = false) and
170-
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
171-
)
172-
or
173-
exists(boolean testIsTrue0 |
174-
implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
175-
)
176-
}
177-
178-
/**
179-
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
180-
*/
181-
predicate ssaUpdateStep(SsaExplicitUpdate v, Expr e, int delta) {
182-
v.getDefiningExpr().(VariableAssign).getSource() = e and delta = 0
183-
or
184-
v.getDefiningExpr().(PostIncExpr).getExpr() = e and delta = 1
185-
or
186-
v.getDefiningExpr().(PreIncExpr).getExpr() = e and delta = 1
187-
or
188-
v.getDefiningExpr().(PostDecExpr).getExpr() = e and delta = -1
189-
or
190-
v.getDefiningExpr().(PreDecExpr).getExpr() = e and delta = -1
191-
or
192-
v.getDefiningExpr().(AssignOp) = e and delta = 0
193-
}
194-
195165
/**
196166
* Holds if `e1 + delta` equals `e2`.
197167
*/
198-
predicate valueFlowStep(Expr e2, Expr e1, int delta) {
199-
e2.(AssignExpr).getSource() = e1 and delta = 0
200-
or
201-
e2.(PlusExpr).getExpr() = e1 and delta = 0
202-
or
203-
e2.(PostIncExpr).getExpr() = e1 and delta = 0
204-
or
205-
e2.(PostDecExpr).getExpr() = e1 and delta = 0
206-
or
207-
e2.(PreIncExpr).getExpr() = e1 and delta = 1
208-
or
209-
e2.(PreDecExpr).getExpr() = e1 and delta = -1
210-
or
168+
predicate additionalValueFlowStep(Expr e2, Expr e1, int delta) {
211169
exists(ArrayCreationExpr a |
212170
arrayLengthDef(e2, a) and
213171
a.getDimension(0) = e1 and
214172
delta = 0
215173
)
216-
or
217-
exists(Expr x |
218-
e2.(AddExpr).hasOperands(e1, x)
219-
or
220-
exists(AssignAddExpr add | add = e2 |
221-
add.getDest() = e1 and add.getRhs() = x
222-
or
223-
add.getDest() = x and add.getRhs() = e1
224-
)
225-
|
226-
x.(ConstantIntegerExpr).getIntValue() = delta
227-
)
228-
or
229-
exists(Expr x |
230-
exists(SubExpr sub |
231-
e2 = sub and
232-
sub.getLeftOperand() = e1 and
233-
sub.getRightOperand() = x
234-
)
235-
or
236-
exists(AssignSubExpr sub |
237-
e2 = sub and
238-
sub.getDest() = e1 and
239-
sub.getRhs() = x
240-
)
241-
|
242-
x.(ConstantIntegerExpr).getIntValue() = -delta
243-
)
244174
}

‎java/ql/test/library-tests/dataflow/modulus-analysis/ModulusAnalysis.expected

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,19 @@
44
| ModulusAnalysis.java:4:5:4:22 | ...=... | 0 | 43 | 0 |
55
| ModulusAnalysis.java:4:5:4:22 | c2 | 0 | 43 | 0 |
66
| ModulusAnalysis.java:4:20:4:21 | 43 | 0 | 43 | 0 |
7+
| ModulusAnalysis.java:7:13:7:22 | eq | SSA init(i) | 3 | 0 |
78
| ModulusAnalysis.java:7:18:7:18 | i | SSA init(i) | 0 | 0 |
89
| ModulusAnalysis.java:7:18:7:22 | ... + ... | SSA init(i) | 3 | 0 |
910
| ModulusAnalysis.java:7:22:7:22 | 3 | 0 | 3 | 0 |
11+
| ModulusAnalysis.java:9:13:9:29 | mul | 0 | 3 | 42 |
1012
| ModulusAnalysis.java:9:19:9:20 | eq | SSA def(eq) | 0 | 0 |
1113
| ModulusAnalysis.java:9:19:9:20 | eq | SSA init(i) | 3 | 0 |
1214
| ModulusAnalysis.java:9:19:9:25 | ... * ... | 0 | 0 | 42 |
1315
| ModulusAnalysis.java:9:19:9:29 | ... + ... | 0 | 3 | 42 |
1416
| ModulusAnalysis.java:9:24:9:25 | c1 | 0 | 42 | 0 |
1517
| ModulusAnalysis.java:9:24:9:25 | c1 | SSA init(this.c1) | 0 | 0 |
1618
| ModulusAnalysis.java:9:29:9:29 | 3 | 0 | 3 | 0 |
19+
| ModulusAnalysis.java:11:13:11:21 | seven | 0 | 7 | 0 |
1720
| ModulusAnalysis.java:11:21:11:21 | 7 | 0 | 7 | 0 |
1821
| ModulusAnalysis.java:12:13:12:15 | mul | 0 | 3 | 42 |
1922
| ModulusAnalysis.java:12:13:12:15 | mul | SSA def(mul) | 0 | 0 |
@@ -24,6 +27,7 @@
2427
| ModulusAnalysis.java:13:32:13:34 | mul | 0 | 3 | 42 |
2528
| ModulusAnalysis.java:13:32:13:34 | mul | 0 | 7 | 43 |
2629
| ModulusAnalysis.java:13:32:13:34 | mul | SSA def(mul) | 0 | 0 |
30+
| ModulusAnalysis.java:16:13:18:23 | j | 0 | 3 | 4 |
2731
| ModulusAnalysis.java:16:17:18:23 | ...?...:... | 0 | 3 | 4 |
2832
| ModulusAnalysis.java:17:15:17:15 | i | SSA init(i) | 0 | 0 |
2933
| ModulusAnalysis.java:17:15:17:19 | ... * ... | 0 | 0 | 4 |
@@ -66,6 +70,7 @@
6670
| ModulusAnalysis.java:26:32:26:36 | ... - ... | SSA init(x) | 35 | 42 |
6771
| ModulusAnalysis.java:26:36:26:36 | y | 0 | 7 | 42 |
6872
| ModulusAnalysis.java:26:36:26:36 | y | SSA init(y) | 0 | 0 |
73+
| ModulusAnalysis.java:29:13:29:35 | l | 0 | 1 | 4 |
6974
| ModulusAnalysis.java:29:17:29:26 | arr.length | SSA impl upd[untracked](arr.length) | 0 | 0 |
7075
| ModulusAnalysis.java:29:17:29:30 | ... * ... | 0 | 0 | 4 |
7176
| ModulusAnalysis.java:29:17:29:35 | ... - ... | 0 | 1 | 4 |
@@ -104,19 +109,22 @@
104109
| ModulusAnalysis.java:49:25:49:25 | 3 | 0 | 3 | 0 |
105110
| ModulusAnalysis.java:50:32:50:32 | x | 0 | 3 | 16 |
106111
| ModulusAnalysis.java:50:32:50:32 | x | SSA init(x) | 0 | 0 |
112+
| ModulusAnalysis.java:56:18:56:22 | i | 0 | 0 | 0 |
107113
| ModulusAnalysis.java:56:22:56:22 | 0 | 0 | 0 | 0 |
108114
| ModulusAnalysis.java:56:25:56:25 | i | SSA phi(i) | 0 | 0 |
109115
| ModulusAnalysis.java:56:29:56:31 | cap | SSA init(cap) | 0 | 0 |
110116
| ModulusAnalysis.java:56:34:56:34 | i | SSA phi(i) | 0 | 0 |
111117
| ModulusAnalysis.java:56:34:56:36 | ...++ | SSA phi(i) | 0 | 0 |
112118
| ModulusAnalysis.java:57:32:57:32 | i | SSA phi(i) | 0 | 0 |
119+
| ModulusAnalysis.java:59:18:59:22 | j | 0 | 0 | 0 |
113120
| ModulusAnalysis.java:59:22:59:22 | 0 | 0 | 0 | 0 |
114121
| ModulusAnalysis.java:59:25:59:25 | j | SSA phi(j) | 0 | 0 |
115122
| ModulusAnalysis.java:59:29:59:31 | cap | SSA init(cap) | 0 | 0 |
116123
| ModulusAnalysis.java:59:34:59:34 | j | SSA phi(j) | 0 | 0 |
117124
| ModulusAnalysis.java:59:34:59:39 | ...+=... | SSA phi(j) | 1 | 0 |
118125
| ModulusAnalysis.java:59:39:59:39 | 1 | 0 | 1 | 0 |
119126
| ModulusAnalysis.java:60:32:60:32 | j | SSA phi(j) | 0 | 0 |
127+
| ModulusAnalysis.java:62:18:62:22 | k | 0 | 0 | 0 |
120128
| ModulusAnalysis.java:62:22:62:22 | 0 | 0 | 0 | 0 |
121129
| ModulusAnalysis.java:62:25:62:25 | k | 0 | 0 | 3 |
122130
| ModulusAnalysis.java:62:25:62:25 | k | SSA def(k) | 0 | 3 |

‎java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@
5959
| A.java:12:16:12:20 | ... + ... | SSA init(y) | 1 | upper | NoReason |
6060
| A.java:12:20:12:20 | 1 | 0 | 1 | lower | NoReason |
6161
| A.java:12:20:12:20 | 1 | 0 | 1 | upper | NoReason |
62+
| A.java:13:13:13:23 | sum | SSA init(y) | 400 | upper | NoReason |
6263
| A.java:13:19:13:19 | x | 0 | 400 | upper | ... > ... |
6364
| A.java:13:19:13:19 | x | SSA init(x) | 0 | lower | NoReason |
6465
| A.java:13:19:13:19 | x | SSA init(x) | 0 | upper | NoReason |
@@ -72,6 +73,17 @@
7273
| A.java:15:13:15:13 | y | SSA init(y) | 0 | upper | NoReason |
7374
| A.java:15:17:15:19 | 300 | 0 | 300 | lower | NoReason |
7475
| A.java:15:17:15:19 | 300 | 0 | 300 | upper | NoReason |
76+
| A.java:16:15:16:25 | sum | 0 | 603 | lower | ... > ... |
77+
| A.java:16:15:16:25 | sum | 0 | 799 | upper | ... != ... |
78+
| A.java:16:15:16:25 | sum | 0 | 799 | upper | ... > ... |
79+
| A.java:16:15:16:25 | sum | SSA init(x) | 301 | lower | ... != ... |
80+
| A.java:16:15:16:25 | sum | SSA init(x) | 301 | lower | NoReason |
81+
| A.java:16:15:16:25 | sum | SSA init(x) | 399 | upper | ... != ... |
82+
| A.java:16:15:16:25 | sum | SSA init(x) | 399 | upper | NoReason |
83+
| A.java:16:15:16:25 | sum | SSA init(y) | 302 | lower | ... != ... |
84+
| A.java:16:15:16:25 | sum | SSA init(y) | 302 | lower | NoReason |
85+
| A.java:16:15:16:25 | sum | SSA init(y) | 400 | upper | ... != ... |
86+
| A.java:16:15:16:25 | sum | SSA init(y) | 400 | upper | NoReason |
7587
| A.java:16:21:16:21 | x | 0 | 302 | lower | ... > ... |
7688
| A.java:16:21:16:21 | x | 0 | 400 | upper | ... > ... |
7789
| A.java:16:21:16:21 | x | SSA init(x) | 0 | lower | NoReason |

‎shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,11 @@ module ModulusAnalysis<
3030
*/
3131
pragma[nomagic]
3232
private predicate valueFlowStepSsa(Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, int delta) {
33-
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
33+
ssaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
3434
or
3535
exists(Sem::Guard guard, boolean testIsTrue |
3636
hasReadOfVarInlineLate(pos, v) and
37-
guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
37+
guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
3838
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
3939
)
4040
}
@@ -260,7 +260,7 @@ module ModulusAnalysis<
260260
or
261261
exists(Sem::Expr mid, int val0, int delta |
262262
exprModulus(mid, b, val0, mod) and
263-
U::semValueFlowStep(e, mid, D::fromInt(delta)) and
263+
valueFlowStep(e, mid, D::fromInt(delta)) and
264264
val = remainder(val0 + delta, mod)
265265
)
266266
or

0 commit comments

Comments
 (0)