5
5
*/
6
6
7
7
/*
8
- * The main recursion has base cases in both `ssaModulus` (for guarded reads) and `semExprModulus `
8
+ * The main recursion has base cases in both `ssaModulus` (for guarded reads) and `exprModulus `
9
9
* (for constant values). The most interesting recursive case is `phiModulusRankStep`, which
10
10
* handles phi inputs.
11
11
*/
@@ -229,7 +229,7 @@ module ModulusAnalysis<
229
229
b .( Bounds:: SemSsaBound ) .getVariable ( ) = v and pos .hasReadOfVar ( v ) and val = 0 and mod = 0
230
230
or
231
231
exists ( Sem:: Expr e , int val0 , int delta |
232
- semExprModulus ( e , b , val0 , mod ) and
232
+ exprModulus ( e , b , val0 , mod ) and
233
233
valueFlowStepSsa ( v , pos , e , delta ) and
234
234
val = remainder ( val0 + delta , mod )
235
235
)
@@ -245,7 +245,7 @@ module ModulusAnalysis<
245
245
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
246
246
*/
247
247
cached
248
- predicate semExprModulus ( Sem:: Expr e , Bounds:: SemBound b , int val , int mod ) {
248
+ predicate exprModulus ( Sem:: Expr e , Bounds:: SemBound b , int val , int mod ) {
249
249
e = b .getExpr ( D:: fromInt ( val ) ) and mod = 0
250
250
or
251
251
evenlyDivisibleExpr ( e , mod ) and
@@ -259,7 +259,7 @@ module ModulusAnalysis<
259
259
)
260
260
or
261
261
exists ( Sem:: Expr mid , int val0 , int delta |
262
- semExprModulus ( mid , b , val0 , mod ) and
262
+ exprModulus ( mid , b , val0 , mod ) and
263
263
U:: semValueFlowStep ( e , mid , D:: fromInt ( delta ) ) and
264
264
val = remainder ( val0 + delta , mod )
265
265
)
@@ -297,22 +297,22 @@ module ModulusAnalysis<
297
297
private predicate condExprBranchModulus (
298
298
Sem:: ConditionalExpr cond , boolean branch , Bounds:: SemBound b , int val , int mod
299
299
) {
300
- semExprModulus ( cond .getBranchExpr ( branch ) , b , val , mod )
300
+ exprModulus ( cond .getBranchExpr ( branch ) , b , val , mod )
301
301
}
302
302
303
303
private predicate addModulus ( Sem:: Expr add , boolean isLeft , Bounds:: SemBound b , int val , int mod ) {
304
304
exists ( Sem:: Expr larg , Sem:: Expr rarg | nonConstAddition ( add , larg , rarg ) |
305
- semExprModulus ( larg , b , val , mod ) and isLeft = true
305
+ exprModulus ( larg , b , val , mod ) and isLeft = true
306
306
or
307
- semExprModulus ( rarg , b , val , mod ) and isLeft = false
307
+ exprModulus ( rarg , b , val , mod ) and isLeft = false
308
308
)
309
309
}
310
310
311
311
private predicate subModulus ( Sem:: Expr sub , boolean isLeft , Bounds:: SemBound b , int val , int mod ) {
312
312
exists ( Sem:: Expr larg , Sem:: Expr rarg | nonConstSubtraction ( sub , larg , rarg ) |
313
- semExprModulus ( larg , b , val , mod ) and isLeft = true
313
+ exprModulus ( larg , b , val , mod ) and isLeft = true
314
314
or
315
- semExprModulus ( rarg , b , val , mod ) and isLeft = false
315
+ exprModulus ( rarg , b , val , mod ) and isLeft = false
316
316
)
317
317
}
318
318
}
0 commit comments