Skip to content

Commit cc6bf75

Browse files
tamasvajktamasvajk
committed
Extract predicates used in range and modulus analysis to rangeutil file
1 parent 780f421 commit cc6bf75

File tree

4 files changed

+126
-115
lines changed

4 files changed

+126
-115
lines changed

‎csharp/ql/src/semmle/code/csharp/dataflow/RangeAnalysis.qll

Lines changed: 5 additions & 98 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
import csharp
22
import Ssa
3-
import Bound
4-
import SignAnalysis
3+
import semmle.code.csharp.dataflow.internal.rangeanalysis.BoundCommon
4+
import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon
55
import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaReadPositionCommon
66
import semmle.code.csharp.dataflow.internal.rangeanalysis.ConstantUtils
77
import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaUtils
8-
import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisSpecific::Private as SignPrivate
8+
import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils
99
import semmle.code.csharp.controlflow.Guards as G
1010
import semmle.code.csharp.commons.ComparisonTest
1111

@@ -61,29 +61,6 @@ private predicate boundCondition(
6161
// todo: other cases: // (v - d) - e < c, ...
6262
}
6363

64-
/**
65-
* Gets a condition that tests whether `v` equals `e + delta`.
66-
*
67-
* If the condition evaluates to `testIsTrue`:
68-
* - `isEq = true` : `v == e + delta`
69-
* - `isEq = false` : `v != e + delta`
70-
*/
71-
G::Guard eqFlowCond(Definition v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
72-
exists(boolean eqpolarity |
73-
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
74-
(testIsTrue = true or testIsTrue = false) and
75-
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
76-
)
77-
or
78-
exists(
79-
boolean testIsTrue0, G::AbstractValues::BooleanValue b0, G::AbstractValues::BooleanValue b1
80-
|
81-
b1.getValue() = testIsTrue and b0.getValue() = testIsTrue0
82-
|
83-
G::Internal::impliesSteps(result, b1, eqFlowCond(v, e, delta, isEq, testIsTrue0), b0)
84-
)
85-
}
86-
8764
/**
8865
* Gets a condition that tests whether `v` is bounded by `e + delta`.
8966
*
@@ -149,27 +126,10 @@ private predicate boundFlowStepSsa(
149126
exists(G::Guard guard, boolean testIsTrue |
150127
pos.hasReadOfVar(v) and
151128
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
152-
SignPrivate::guardControlsSsaRead(guard, pos, testIsTrue)
129+
guardControlsSsaRead(guard, pos, testIsTrue)
153130
)
154131
}
155132

156-
/**
157-
* Holds if `v` is an `ExplicitDefinition` that equals `e + delta`.
158-
*/
159-
predicate ssaUpdateStep(ExplicitDefinition v, Expr e, int delta) {
160-
v.getADefinition().getExpr().(Assignment).getRValue() = e and delta = 0
161-
or
162-
v.getADefinition().getExpr().(PostIncrExpr).getOperand() = e and delta = 1
163-
or
164-
v.getADefinition().getExpr().(PreIncrExpr).getOperand() = e and delta = 1
165-
or
166-
v.getADefinition().getExpr().(PostDecrExpr).getOperand() = e and delta = -1
167-
or
168-
v.getADefinition().getExpr().(PreDecrExpr).getOperand() = e and delta = -1
169-
or
170-
v.getADefinition().getExpr().(AssignOperation) = e and delta = 0
171-
}
172-
173133
/**
174134
* Holds if `b + delta` is a valid bound for `e`.
175135
* - `upper = true` : `e <= b + delta`
@@ -237,59 +197,6 @@ private predicate bounded(
237197
)
238198
}
239199

240-
/**
241-
* Holds if `e1 + delta` equals `e2`.
242-
*/
243-
predicate valueFlowStep(Expr e2, Expr e1, int delta) {
244-
e2.(AssignExpr).getRValue() = e1 and delta = 0
245-
or
246-
e2.(UnaryPlusExpr).getOperand() = e1 and delta = 0
247-
or
248-
e2.(PostIncrExpr).getOperand() = e1 and delta = 0
249-
or
250-
e2.(PostDecrExpr).getOperand() = e1 and delta = 0
251-
or
252-
e2.(PreIncrExpr).getOperand() = e1 and delta = 1
253-
or
254-
e2.(PreDecrExpr).getOperand() = e1 and delta = -1
255-
or
256-
// exists(ArrayCreationExpr a |
257-
// arrayLengthDef(e2, a) and
258-
// a.getDimension(0) = e1 and
259-
// delta = 0
260-
// )
261-
// or
262-
exists(Expr x |
263-
e2.(AddExpr).getAnOperand() = e1 and
264-
e2.(AddExpr).getAnOperand() = x and
265-
not e1 = x
266-
or
267-
exists(AssignAddExpr add | add = e2 |
268-
add.getLValue() = e1 and add.getRValue() = x
269-
or
270-
add.getLValue() = x and add.getRValue() = e1
271-
)
272-
|
273-
x.(ConstantIntegerExpr).getIntValue() = delta
274-
)
275-
or
276-
exists(Expr x |
277-
exists(SubExpr sub |
278-
e2 = sub and
279-
sub.getLeftOperand() = e1 and
280-
sub.getRightOperand() = x
281-
)
282-
or
283-
exists(AssignSubExpr sub |
284-
e2 = sub and
285-
sub.getLValue() = e1 and
286-
sub.getRValue() = x
287-
)
288-
|
289-
x.(ConstantIntegerExpr).getIntValue() = -delta
290-
)
291-
}
292-
293200
/**
294201
* Holds if `e1 + delta` is a valid bound for `e2`.
295202
* - `upper = true` : `e2 <= e1 + delta`
@@ -465,7 +372,7 @@ private predicate unequalFlowStepIntegralSsa(Definition v, SsaReadPosition pos,
465372
exists(G::Guard guard, boolean testIsTrue |
466373
pos.hasReadOfVar(v) and
467374
guard = eqFlowCond(v, e, delta, false, testIsTrue) and
468-
SignPrivate::guardControlsSsaRead(guard, pos, testIsTrue)
375+
guardControlsSsaRead(guard, pos, testIsTrue)
469376
)
470377
}
471378

‎csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ module Private {
22
private import csharp as CS
33
private import ConstantUtils as CU
44
private import semmle.code.csharp.controlflow.Guards as G
5-
private import semmle.code.csharp.dataflow.RangeAnalysis as RA // todo remove this
5+
private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
66
private import SsaUtils as SU
77
private import SignAnalysisSpecific::Private as SA
88

@@ -83,11 +83,11 @@ module Private {
8383

8484
predicate guardControlsSsaRead = SA::guardControlsSsaRead/3;
8585

86-
predicate valueFlowStep = RA::valueFlowStep/3;
86+
predicate valueFlowStep = RU::valueFlowStep/3;
8787

88-
predicate eqFlowCond = RA::eqFlowCond/5;
88+
predicate eqFlowCond = RU::eqFlowCond/5;
8989

90-
predicate ssaUpdateStep = RA::ssaUpdateStep/3;
90+
predicate ssaUpdateStep = RU::ssaUpdateStep/3;
9191

9292
Expr getAnExpr(BasicBlock bb) { result = bb.getANode().getElement() }
9393

‎csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
/**
2+
* Provides predicates for range and modulus analysis.
3+
*/
4+
5+
private import csharp
6+
private import Ssa
7+
private import SsaUtils
8+
private import ConstantUtils
9+
private import SsaReadPositionCommon
10+
private import semmle.code.csharp.controlflow.Guards as G
11+
12+
private class BooleanValue = G::AbstractValues::BooleanValue;
13+
14+
/**
15+
* Holds if `v` is an `ExplicitDefinition` that equals `e + delta`.
16+
*/
17+
predicate ssaUpdateStep(ExplicitDefinition v, Expr e, int delta) {
18+
v.getADefinition().getExpr().(Assignment).getRValue() = e and delta = 0
19+
or
20+
v.getADefinition().getExpr().(PostIncrExpr).getOperand() = e and delta = 1
21+
or
22+
v.getADefinition().getExpr().(PreIncrExpr).getOperand() = e and delta = 1
23+
or
24+
v.getADefinition().getExpr().(PostDecrExpr).getOperand() = e and delta = -1
25+
or
26+
v.getADefinition().getExpr().(PreDecrExpr).getOperand() = e and delta = -1
27+
or
28+
v.getADefinition().getExpr().(AssignOperation) = e and delta = 0
29+
}
30+
31+
/**
32+
* Gets a condition that tests whether `v` equals `e + delta`.
33+
*
34+
* If the condition evaluates to `testIsTrue`:
35+
* - `isEq = true` : `v == e + delta`
36+
* - `isEq = false` : `v != e + delta`
37+
*/
38+
G::Guard eqFlowCond(Definition v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
39+
exists(boolean eqpolarity |
40+
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
41+
(testIsTrue = true or testIsTrue = false) and
42+
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
43+
)
44+
or
45+
exists(
46+
boolean testIsTrue0, G::AbstractValues::BooleanValue b0, G::AbstractValues::BooleanValue b1
47+
|
48+
b1.getValue() = testIsTrue and b0.getValue() = testIsTrue0
49+
|
50+
G::Internal::impliesSteps(result, b1, eqFlowCond(v, e, delta, isEq, testIsTrue0), b0)
51+
)
52+
}
53+
54+
/**
55+
* Holds if `e1 + delta` equals `e2`.
56+
*/
57+
predicate valueFlowStep(Expr e2, Expr e1, int delta) {
58+
e2.(AssignExpr).getRValue() = e1 and delta = 0
59+
or
60+
e2.(UnaryPlusExpr).getOperand() = e1 and delta = 0
61+
or
62+
e2.(PostIncrExpr).getOperand() = e1 and delta = 0
63+
or
64+
e2.(PostDecrExpr).getOperand() = e1 and delta = 0
65+
or
66+
e2.(PreIncrExpr).getOperand() = e1 and delta = 1
67+
or
68+
e2.(PreDecrExpr).getOperand() = e1 and delta = -1
69+
or
70+
// exists(ArrayCreationExpr a |
71+
// arrayLengthDef(e2, a) and
72+
// a.getDimension(0) = e1 and
73+
// delta = 0
74+
// )
75+
// or
76+
exists(Expr x |
77+
e2.(AddExpr).getAnOperand() = e1 and
78+
e2.(AddExpr).getAnOperand() = x and
79+
not e1 = x
80+
or
81+
exists(AssignAddExpr add | add = e2 |
82+
add.getLValue() = e1 and add.getRValue() = x
83+
or
84+
add.getLValue() = x and add.getRValue() = e1
85+
)
86+
|
87+
x.(ConstantIntegerExpr).getIntValue() = delta
88+
)
89+
or
90+
exists(Expr x |
91+
exists(SubExpr sub |
92+
e2 = sub and
93+
sub.getLeftOperand() = e1 and
94+
sub.getRightOperand() = x
95+
)
96+
or
97+
exists(AssignSubExpr sub |
98+
e2 = sub and
99+
sub.getLValue() = e1 and
100+
sub.getRValue() = x
101+
)
102+
|
103+
x.(ConstantIntegerExpr).getIntValue() = -delta
104+
)
105+
}
106+
107+
/**
108+
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
109+
*/
110+
predicate guardControlsSsaRead(G::Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
111+
exists(BooleanValue b | b.getValue() = testIsTrue |
112+
guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
113+
)
114+
}

‎csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll

Lines changed: 3 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,11 @@
22
* Provides C#-specific definitions for use in sign analysis.
33
*/
44
module Private {
5-
private import SsaUtils as SU
65
private import csharp as CS
6+
private import SsaUtils as SU
77
private import ConstantUtils as CU
8+
private import RangeUtils as RU
89
private import semmle.code.csharp.controlflow.Guards as G
9-
private import SsaReadPositionCommon
10-
11-
private class BooleanValue = G::AbstractValues::BooleanValue;
12-
1310
import Impl
1411

1512
class Guard = G::Guard;
@@ -38,14 +35,7 @@ module Private {
3835

3936
predicate ssaRead = SU::ssaRead/2;
4037

41-
/**
42-
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
43-
*/
44-
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
45-
exists(BooleanValue b | b.getValue() = testIsTrue |
46-
guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
47-
)
48-
}
38+
predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
4939
}
5040

5141
private module Impl {

0 commit comments

Comments
 (0)