55 */
66
77/*
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 `
99 * (for constant values). The most interesting recursive case is `phiModulusRankStep`, which
1010 * handles phi inputs.
1111 */
@@ -229,7 +229,7 @@ module ModulusAnalysis<
229229 b .( Bounds:: SemSsaBound ) .getVariable ( ) = v and pos .hasReadOfVar ( v ) and val = 0 and mod = 0
230230 or
231231 exists ( Sem:: Expr e , int val0 , int delta |
232- semExprModulus ( e , b , val0 , mod ) and
232+ exprModulus ( e , b , val0 , mod ) and
233233 valueFlowStepSsa ( v , pos , e , delta ) and
234234 val = remainder ( val0 + delta , mod )
235235 )
@@ -245,7 +245,7 @@ module ModulusAnalysis<
245245 * - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
246246 */
247247 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 ) {
249249 e = b .getExpr ( D:: fromInt ( val ) ) and mod = 0
250250 or
251251 evenlyDivisibleExpr ( e , mod ) and
@@ -259,7 +259,7 @@ module ModulusAnalysis<
259259 )
260260 or
261261 exists ( Sem:: Expr mid , int val0 , int delta |
262- semExprModulus ( mid , b , val0 , mod ) and
262+ exprModulus ( mid , b , val0 , mod ) and
263263 U:: semValueFlowStep ( e , mid , D:: fromInt ( delta ) ) and
264264 val = remainder ( val0 + delta , mod )
265265 )
@@ -297,22 +297,22 @@ module ModulusAnalysis<
297297 private predicate condExprBranchModulus (
298298 Sem:: ConditionalExpr cond , boolean branch , Bounds:: SemBound b , int val , int mod
299299 ) {
300- semExprModulus ( cond .getBranchExpr ( branch ) , b , val , mod )
300+ exprModulus ( cond .getBranchExpr ( branch ) , b , val , mod )
301301 }
302302
303303 private predicate addModulus ( Sem:: Expr add , boolean isLeft , Bounds:: SemBound b , int val , int mod ) {
304304 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
306306 or
307- semExprModulus ( rarg , b , val , mod ) and isLeft = false
307+ exprModulus ( rarg , b , val , mod ) and isLeft = false
308308 )
309309 }
310310
311311 private predicate subModulus ( Sem:: Expr sub , boolean isLeft , Bounds:: SemBound b , int val , int mod ) {
312312 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
314314 or
315- semExprModulus ( rarg , b , val , mod ) and isLeft = false
315+ exprModulus ( rarg , b , val , mod ) and isLeft = false
316316 )
317317 }
318318}
0 commit comments