@@ -211,10 +211,6 @@ private predicate ssaModulus(SemSsaVariable v, SemSsaReadPosition pos, SemBound
211
211
moduloGuardedRead ( v , pos , val , mod ) and b instanceof SemZeroBound
212
212
}
213
213
214
- predicate semExprModulus ( SemExpr e , SemBound b , int val , int mod ) {
215
- semExprModulus ( e , b , val , mod , _)
216
- }
217
-
218
214
/**
219
215
* Holds if `e` is equal to `b + val` modulo `mod`.
220
216
*
@@ -223,28 +219,25 @@ predicate semExprModulus(SemExpr e, SemBound b, int val, int mod) {
223
219
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
224
220
*/
225
221
cached
226
- predicate semExprModulus ( SemExpr e , SemBound b , int val , int mod , string branch ) {
222
+ predicate semExprModulus ( SemExpr e , SemBound b , int val , int mod ) {
227
223
not ignoreExprModulus ( e ) and
228
224
(
229
- e = b .getExpr ( val ) and mod = 0 and branch = "getExpr"
225
+ e = b .getExpr ( val ) and mod = 0
230
226
or
231
227
evenlyDivisibleExpr ( e , mod ) and
232
228
val = 0 and
233
- b instanceof SemZeroBound and
234
- branch = "evenlyDivisible"
229
+ b instanceof SemZeroBound
235
230
or
236
231
exists ( SemSsaVariable v , SemSsaReadPositionBlock bb |
237
232
ssaModulus ( v , bb , b , val , mod ) and
238
233
e = v .getAUse ( ) and
239
- bb .getAnExpr ( ) = e and
240
- branch = "use"
234
+ bb .getAnExpr ( ) = e
241
235
)
242
236
or
243
237
exists ( SemExpr mid , int val0 , int delta |
244
238
semExprModulus ( mid , b , val0 , mod ) and
245
239
semValueFlowStep ( e , mid , delta ) and
246
- val = remainder ( val0 + delta , mod ) and
247
- branch = "valueFlowStep"
240
+ val = remainder ( val0 + delta , mod )
248
241
)
249
242
or
250
243
exists ( SemConditionalExpr cond , int v1 , int v2 , int m1 , int m2 |
@@ -253,17 +246,15 @@ predicate semExprModulus(SemExpr e, SemBound b, int val, int mod, string branch)
253
246
condExprBranchModulus ( cond , false , b , v2 , m2 ) and
254
247
mod = m1 .gcd ( m2 ) .gcd ( v1 - v2 ) and
255
248
mod != 1 and
256
- val = remainder ( v1 , mod ) and
257
- branch = "condExpr"
249
+ val = remainder ( v1 , mod )
258
250
)
259
251
or
260
252
exists ( SemBound b1 , SemBound b2 , int v1 , int v2 , int m1 , int m2 |
261
253
addModulus ( e , true , b1 , v1 , m1 ) and
262
254
addModulus ( e , false , b2 , v2 , m2 ) and
263
255
mod = m1 .gcd ( m2 ) and
264
256
mod != 1 and
265
- val = remainder ( v1 + v2 , mod ) and
266
- branch = "addModulus"
257
+ val = remainder ( v1 + v2 , mod )
267
258
|
268
259
b = b1 and b2 instanceof SemZeroBound
269
260
or
@@ -275,8 +266,7 @@ predicate semExprModulus(SemExpr e, SemBound b, int val, int mod, string branch)
275
266
subModulus ( e , false , any ( SemZeroBound zb ) , v2 , m2 ) and
276
267
mod = m1 .gcd ( m2 ) and
277
268
mod != 1 and
278
- val = remainder ( v1 - v2 , mod ) and
279
- branch = "subModulus"
269
+ val = remainder ( v1 - v2 , mod )
280
270
)
281
271
)
282
272
}
0 commit comments