@@ -16,7 +16,7 @@ private import ConstantAnalysis
16
16
private import RangeUtils
17
17
private import RangeAnalysisStage
18
18
19
- module ModulusAnalysis< DeltaSig D, UtilSig< D > U> {
19
+ module ModulusAnalysis< DeltaSig D, BoundSig < D > Bounds , UtilSig< D > U> {
20
20
/**
21
21
* Holds if `e + delta` equals `v` at `pos`.
22
22
*/
@@ -146,7 +146,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
146
146
private predicate phiSelfModulus (
147
147
SemSsaPhiNode phi , SemSsaVariable inp , SemSsaReadPositionPhiInputEdge edge , int mod
148
148
) {
149
- exists ( SemSsaBound phibound , int v , int m |
149
+ exists ( Bounds :: SemSsaBound phibound , int v , int m |
150
150
edge .phiInput ( phi , inp ) and
151
151
phibound .getAVariable ( ) = phi and
152
152
ssaModulus ( inp , edge , phibound , v , m ) and
@@ -158,7 +158,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
158
158
/**
159
159
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
160
160
*/
161
- private predicate phiModulusInit ( SemSsaPhiNode phi , SemBound b , int val , int mod ) {
161
+ private predicate phiModulusInit ( SemSsaPhiNode phi , Bounds :: SemBound b , int val , int mod ) {
162
162
exists ( SemSsaVariable inp , SemSsaReadPositionPhiInputEdge edge |
163
163
edge .phiInput ( phi , inp ) and
164
164
ssaModulus ( inp , edge , b , val , mod )
@@ -169,7 +169,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
169
169
* Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
170
170
*/
171
171
pragma [ nomagic]
172
- private predicate phiModulusRankStep ( SemSsaPhiNode phi , SemBound b , int val , int mod , int rix ) {
172
+ private predicate phiModulusRankStep ( SemSsaPhiNode phi , Bounds :: SemBound b , int val , int mod , int rix ) {
173
173
/*
174
174
* base case. If any phi input is equal to `b + val` modulo `mod`, that's a potential congruence
175
175
* class for the phi node.
@@ -213,7 +213,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
213
213
/**
214
214
* Holds if `phi` is equal to `b + val` modulo `mod`.
215
215
*/
216
- private predicate phiModulus ( SemSsaPhiNode phi , SemBound b , int val , int mod ) {
216
+ private predicate phiModulus ( SemSsaPhiNode phi , Bounds :: SemBound b , int val , int mod ) {
217
217
exists ( int r |
218
218
maxPhiInputRank ( phi , r ) and
219
219
phiModulusRankStep ( phi , b , val , mod , r )
@@ -224,19 +224,19 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
224
224
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
225
225
*/
226
226
private predicate ssaModulus (
227
- SemSsaVariable v , SemSsaReadPosition pos , SemBound b , int val , int mod
227
+ SemSsaVariable v , SemSsaReadPosition pos , Bounds :: SemBound b , int val , int mod
228
228
) {
229
229
phiModulus ( v , b , val , mod ) and pos .hasReadOfVar ( v )
230
230
or
231
- b .( SemSsaBound ) .getAVariable ( ) = v and pos .hasReadOfVar ( v ) and val = 0 and mod = 0
231
+ b .( Bounds :: SemSsaBound ) .getAVariable ( ) = v and pos .hasReadOfVar ( v ) and val = 0 and mod = 0
232
232
or
233
233
exists ( SemExpr e , int val0 , int delta |
234
234
semExprModulus ( e , b , val0 , mod ) and
235
235
valueFlowStepSsa ( v , pos , e , delta ) and
236
236
val = remainder ( val0 + delta , mod )
237
237
)
238
238
or
239
- moduloGuardedRead ( v , pos , val , mod ) and b instanceof SemZeroBound
239
+ moduloGuardedRead ( v , pos , val , mod ) and b instanceof Bounds :: SemZeroBound
240
240
}
241
241
242
242
/**
@@ -247,14 +247,14 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
247
247
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
248
248
*/
249
249
cached
250
- predicate semExprModulus ( SemExpr e , SemBound b , int val , int mod ) {
250
+ predicate semExprModulus ( SemExpr e , Bounds :: SemBound b , int val , int mod ) {
251
251
not ignoreExprModulus ( e ) and
252
252
(
253
- e = b .getExpr ( val ) and mod = 0
253
+ e = b .getExpr ( D :: fromInt ( val ) ) and mod = 0
254
254
or
255
255
evenlyDivisibleExpr ( e , mod ) and
256
256
val = 0 and
257
- b instanceof SemZeroBound
257
+ b instanceof Bounds :: SemZeroBound
258
258
or
259
259
exists ( SemSsaVariable v , SemSsaReadPositionBlock bb |
260
260
ssaModulus ( v , bb , b , val , mod ) and
@@ -277,21 +277,21 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
277
277
val = remainder ( v1 , mod )
278
278
)
279
279
or
280
- exists ( SemBound b1 , SemBound b2 , int v1 , int v2 , int m1 , int m2 |
280
+ exists ( Bounds :: SemBound b1 , Bounds :: SemBound b2 , int v1 , int v2 , int m1 , int m2 |
281
281
addModulus ( e , true , b1 , v1 , m1 ) and
282
282
addModulus ( e , false , b2 , v2 , m2 ) and
283
283
mod = m1 .gcd ( m2 ) and
284
284
mod != 1 and
285
285
val = remainder ( v1 + v2 , mod )
286
286
|
287
- b = b1 and b2 instanceof SemZeroBound
287
+ b = b1 and b2 instanceof Bounds :: SemZeroBound
288
288
or
289
- b = b2 and b1 instanceof SemZeroBound
289
+ b = b2 and b1 instanceof Bounds :: SemZeroBound
290
290
)
291
291
or
292
292
exists ( int v1 , int v2 , int m1 , int m2 |
293
293
subModulus ( e , true , b , v1 , m1 ) and
294
- subModulus ( e , false , any ( SemZeroBound zb ) , v2 , m2 ) and
294
+ subModulus ( e , false , any ( Bounds :: SemZeroBound zb ) , v2 , m2 ) and
295
295
mod = m1 .gcd ( m2 ) and
296
296
mod != 1 and
297
297
val = remainder ( v1 - v2 , mod )
@@ -300,20 +300,20 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
300
300
}
301
301
302
302
private predicate condExprBranchModulus (
303
- SemConditionalExpr cond , boolean branch , SemBound b , int val , int mod
303
+ SemConditionalExpr cond , boolean branch , Bounds :: SemBound b , int val , int mod
304
304
) {
305
305
semExprModulus ( cond .getBranchExpr ( branch ) , b , val , mod )
306
306
}
307
307
308
- private predicate addModulus ( SemExpr add , boolean isLeft , SemBound b , int val , int mod ) {
308
+ private predicate addModulus ( SemExpr add , boolean isLeft , Bounds :: SemBound b , int val , int mod ) {
309
309
exists ( SemExpr larg , SemExpr rarg | nonConstAddition ( add , larg , rarg ) |
310
310
semExprModulus ( larg , b , val , mod ) and isLeft = true
311
311
or
312
312
semExprModulus ( rarg , b , val , mod ) and isLeft = false
313
313
)
314
314
}
315
315
316
- private predicate subModulus ( SemExpr sub , boolean isLeft , SemBound b , int val , int mod ) {
316
+ private predicate subModulus ( SemExpr sub , boolean isLeft , Bounds :: SemBound b , int val , int mod ) {
317
317
exists ( SemExpr larg , SemExpr rarg | nonConstSubtraction ( sub , larg , rarg ) |
318
318
semExprModulus ( larg , b , val , mod ) and isLeft = true
319
319
or
0 commit comments