Skip to content

Commit 780f421

Browse files
tamasvajktamasvajk
committed
WIP - ModulusAnalysis shared between C# and Java
1 parent 5efd675 commit 780f421

File tree

7 files changed

+816
-325
lines changed

7 files changed

+816
-325
lines changed

‎config/identical-files.json

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,10 @@
6666
"java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/BoundCommon.qll",
6767
"csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundCommon.qll"
6868
],
69+
"ModulusAnalysis Java/C#": [
70+
"java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisCommon.qll",
71+
"csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisCommon.qll"
72+
],
6973
"C++ SubBasicBlocks": [
7074
"cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
7175
"cpp/ql/src/semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll"

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
/**
2+
* Provides inferences of the form: `e` equals `b + v` modulo `m` where `e` is
3+
* an expression, `b` is a `Bound` (typically zero or the value of an SSA
4+
* variable), and `v` is an integer in the range `[0 .. m-1]`.
5+
*/
6+
7+
import semmle.code.csharp.dataflow.internal.rangeanalysis.ModulusAnalysisCommon

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

Lines changed: 322 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,322 @@
1+
/**
2+
* Provides inferences of the form: `e` equals `b + v` modulo `m` where `e` is
3+
* an expression, `b` is a `Bound` (typically zero or the value of an SSA
4+
* variable), and `v` is an integer in the range `[0 .. m-1]`.
5+
*/
6+
7+
private import ModulusAnalysisSpecific::Private
8+
private import BoundCommon
9+
private import SsaReadPositionCommon
10+
11+
/**
12+
* Holds if `e + delta` equals `v` at `pos`.
13+
*/
14+
private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, int delta) {
15+
ssaUpdateStep(v, e, delta) and pos.hasReadOfVar(v)
16+
or
17+
exists(Guard guard, boolean testIsTrue |
18+
pos.hasReadOfVar(v) and
19+
guard = eqFlowCond(v, e, delta, true, testIsTrue) and
20+
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
21+
)
22+
}
23+
24+
/**
25+
* Holds if `add` is the addition of `larg` and `rarg`, neither of which are
26+
* `ConstantIntegerExpr`s.
27+
*/
28+
private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
29+
(
30+
exists(AddExpr a | a = add |
31+
larg = a.getLeftOperand() and
32+
rarg = a.getRightOperand()
33+
)
34+
or
35+
exists(AssignAddExpr a | a = add |
36+
larg = a.getDest() and
37+
rarg = a.getRhs()
38+
)
39+
) and
40+
not larg instanceof ConstantIntegerExpr and
41+
not rarg instanceof ConstantIntegerExpr
42+
}
43+
44+
/**
45+
* Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
46+
* a `ConstantIntegerExpr`.
47+
*/
48+
private predicate nonConstSubtraction(Expr sub, Expr larg, Expr rarg) {
49+
(
50+
exists(SubExpr s | s = sub |
51+
larg = s.getLeftOperand() and
52+
rarg = s.getRightOperand()
53+
)
54+
or
55+
exists(AssignSubExpr s | s = sub |
56+
larg = s.getDest() and
57+
rarg = s.getRhs()
58+
)
59+
) and
60+
not rarg instanceof ConstantIntegerExpr
61+
}
62+
63+
/** Gets an expression that is the remainder modulo `mod` of `arg`. */
64+
private Expr modExpr(Expr arg, int mod) {
65+
exists(RemExpr rem |
66+
result = rem and
67+
arg = rem.getLeftOperand() and
68+
rem.getRightOperand().(ConstantIntegerExpr).getIntValue() = mod and
69+
mod >= 2
70+
)
71+
or
72+
exists(ConstantIntegerExpr c |
73+
mod = 2.pow([1 .. 30]) and
74+
c.getIntValue() = mod - 1 and
75+
result.(AndBitwiseExpr).hasOperands(arg, c)
76+
)
77+
}
78+
79+
/**
80+
* Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
81+
* its `testIsTrue` branch.
82+
*/
83+
private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
84+
exists(Expr rem, ConstantIntegerExpr c, int r, boolean polarity |
85+
result.isEquality(rem, c, polarity) and
86+
c.getIntValue() = r and
87+
rem = modExpr(v.getAUse(), mod) and
88+
(
89+
testIsTrue = polarity and val = r
90+
or
91+
testIsTrue = polarity.booleanNot() and
92+
mod = 2 and
93+
val = 1 - r and
94+
(r = 0 or r = 1)
95+
)
96+
)
97+
}
98+
99+
/**
100+
* Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
101+
*/
102+
private predicate moduloGuardedRead(SsaVariable v, SsaReadPosition pos, int val, int mod) {
103+
exists(Guard guard, boolean testIsTrue |
104+
pos.hasReadOfVar(v) and
105+
guard = moduloCheck(v, val, mod, testIsTrue) and
106+
guardControlsSsaRead(guard, pos, testIsTrue)
107+
)
108+
}
109+
110+
/** Holds if `factor` is a power of 2 that divides `mask`. */
111+
bindingset[mask]
112+
private predicate andmaskFactor(int mask, int factor) {
113+
mask % factor = 0 and
114+
factor = 2.pow([1 .. 30])
115+
}
116+
117+
/** Holds if `e` is evenly divisible by `factor`. */
118+
private predicate evenlyDivisibleExpr(Expr e, int factor) {
119+
exists(ConstantIntegerExpr c, int k | k = c.getIntValue() |
120+
e.(MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
121+
or
122+
e.(AssignMulExpr).getSource() = c and factor = k.abs() and factor >= 2
123+
or
124+
e.(LShiftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
125+
or
126+
e.(AssignLShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
127+
or
128+
e.(AndBitwiseExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
129+
or
130+
e.(AssignAndExpr).getSource() = c and factor = max(int f | andmaskFactor(k, f))
131+
)
132+
}
133+
134+
/**
135+
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
136+
* in an arbitrary 1-based numbering of the input edges to `phi`.
137+
*/
138+
private predicate rankedPhiInput(
139+
SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r
140+
) {
141+
edge.phiInput(phi, inp) and
142+
edge =
143+
rank[r](SsaReadPositionPhiInputEdge e | e.phiInput(phi, _) | e order by getId(e.getOrigBlock()))
144+
}
145+
146+
/**
147+
* Holds if `rix` is the number of input edges to `phi`.
148+
*/
149+
private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
150+
rix = max(int r | rankedPhiInput(phi, _, _, r))
151+
}
152+
153+
/**
154+
* Gets the remainder of `val` modulo `mod`.
155+
*
156+
* For `mod = 0` the result equals `val` and for `mod > 1` the result is within
157+
* the range `[0 .. mod-1]`.
158+
*/
159+
bindingset[val, mod]
160+
private int remainder(int val, int mod) {
161+
mod = 0 and result = val
162+
or
163+
mod > 1 and result = ((val % mod) + mod) % mod
164+
}
165+
166+
/**
167+
* Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
168+
*/
169+
private predicate phiSelfModulus(
170+
SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int mod
171+
) {
172+
exists(SsaBound phibound, int v, int m |
173+
edge.phiInput(phi, inp) and
174+
phibound.getSsa() = phi and
175+
ssaModulus(inp, edge, phibound, v, m) and
176+
mod = m.gcd(v) and
177+
mod != 1
178+
)
179+
}
180+
181+
/**
182+
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
183+
*/
184+
private predicate phiModulusInit(SsaPhiNode phi, Bound b, int val, int mod) {
185+
exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge |
186+
edge.phiInput(phi, inp) and
187+
ssaModulus(inp, edge, b, val, mod)
188+
)
189+
}
190+
191+
/**
192+
* Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
193+
*/
194+
private predicate phiModulusRankStep(SsaPhiNode phi, Bound b, int val, int mod, int rix) {
195+
rix = 0 and
196+
phiModulusInit(phi, b, val, mod)
197+
or
198+
exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge, int v1, int m1 |
199+
mod != 1 and
200+
val = remainder(v1, mod)
201+
|
202+
exists(int v2, int m2 |
203+
rankedPhiInput(phi, inp, edge, rix) and
204+
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
205+
ssaModulus(inp, edge, b, v2, m2) and
206+
mod = m1.gcd(m2).gcd(v1 - v2)
207+
)
208+
or
209+
exists(int m2 |
210+
rankedPhiInput(phi, inp, edge, rix) and
211+
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
212+
phiSelfModulus(phi, inp, edge, m2) and
213+
mod = m1.gcd(m2)
214+
)
215+
)
216+
}
217+
218+
/**
219+
* Holds if `phi` is equal to `b + val` modulo `mod`.
220+
*/
221+
private predicate phiModulus(SsaPhiNode phi, Bound b, int val, int mod) {
222+
exists(int r |
223+
maxPhiInputRank(phi, r) and
224+
phiModulusRankStep(phi, b, val, mod, r)
225+
)
226+
}
227+
228+
/**
229+
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
230+
*/
231+
private predicate ssaModulus(SsaVariable v, SsaReadPosition pos, Bound b, int val, int mod) {
232+
phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
233+
or
234+
b.(SsaBound).getSsa() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
235+
or
236+
exists(Expr e, int val0, int delta |
237+
exprModulus(e, b, val0, mod) and
238+
valueFlowStepSsa(v, pos, e, delta) and
239+
val = remainder(val0 + delta, mod)
240+
)
241+
or
242+
moduloGuardedRead(v, pos, val, mod) and b instanceof ZeroBound
243+
}
244+
245+
/**
246+
* Holds if `e` is equal to `b + val` modulo `mod`.
247+
*
248+
* There are two cases for the modulus:
249+
* - `mod = 0`: The equality `e = b + val` is an ordinary equality.
250+
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
251+
*/
252+
cached
253+
predicate exprModulus(Expr e, Bound b, int val, int mod) {
254+
e = b.getExpr(val) and mod = 0
255+
or
256+
evenlyDivisibleExpr(e, mod) and val = 0 and b instanceof ZeroBound
257+
or
258+
exists(SsaVariable v, SsaReadPositionBlock bb |
259+
ssaModulus(v, bb, b, val, mod) and
260+
e = v.getAUse() and
261+
getAnExpr(bb.getBlock()) = e
262+
)
263+
or
264+
exists(Expr mid, int val0, int delta |
265+
exprModulus(mid, b, val0, mod) and
266+
valueFlowStep(e, mid, delta) and
267+
val = remainder(val0 + delta, mod)
268+
)
269+
or
270+
exists(ConditionalExpr cond, int v1, int v2, int m1, int m2 |
271+
cond = e and
272+
condExprBranchModulus(cond, true, b, v1, m1) and
273+
condExprBranchModulus(cond, false, b, v2, m2) and
274+
mod = m1.gcd(m2).gcd(v1 - v2) and
275+
mod != 1 and
276+
val = remainder(v1, mod)
277+
)
278+
or
279+
exists(Bound b1, Bound b2, int v1, int v2, int m1, int m2 |
280+
addModulus(e, true, b1, v1, m1) and
281+
addModulus(e, false, b2, v2, m2) and
282+
mod = m1.gcd(m2) and
283+
mod != 1 and
284+
val = remainder(v1 + v2, mod)
285+
|
286+
b = b1 and b2 instanceof ZeroBound
287+
or
288+
b = b2 and b1 instanceof ZeroBound
289+
)
290+
or
291+
exists(int v1, int v2, int m1, int m2 |
292+
subModulus(e, true, b, v1, m1) and
293+
subModulus(e, false, any(ZeroBound zb), v2, m2) and
294+
mod = m1.gcd(m2) and
295+
mod != 1 and
296+
val = remainder(v1 - v2, mod)
297+
)
298+
}
299+
300+
private predicate condExprBranchModulus(
301+
ConditionalExpr cond, boolean branch, Bound b, int val, int mod
302+
) {
303+
exprModulus(cond.getTrueExpr(), b, val, mod) and branch = true
304+
or
305+
exprModulus(cond.getFalseExpr(), b, val, mod) and branch = false
306+
}
307+
308+
private predicate addModulus(Expr add, boolean isLeft, Bound b, int val, int mod) {
309+
exists(Expr larg, Expr rarg | nonConstAddition(add, larg, rarg) |
310+
exprModulus(larg, b, val, mod) and isLeft = true
311+
or
312+
exprModulus(rarg, b, val, mod) and isLeft = false
313+
)
314+
}
315+
316+
private predicate subModulus(Expr sub, boolean isLeft, Bound b, int val, int mod) {
317+
exists(Expr larg, Expr rarg | nonConstSubtraction(sub, larg, rarg) |
318+
exprModulus(larg, b, val, mod) and isLeft = true
319+
or
320+
exprModulus(rarg, b, val, mod) and isLeft = false
321+
)
322+
}

0 commit comments

Comments
 (0)