63
63
* back-edge as a precise bound might require traversing a loop once).
64
64
*/
65
65
66
- private import RangeAnalysisSpecific as Specific
67
66
private import RangeUtils as Utils
68
67
private import SignAnalysisCommon
69
68
private import ModulusAnalysis
@@ -150,9 +149,35 @@ signature module UtilSig<DeltaSig DeltaParam> {
150
149
predicate semSsaUpdateStep ( SemSsaExplicitUpdate v , SemExpr e , DeltaParam:: Delta delta ) ;
151
150
152
151
predicate semValueFlowStep ( SemExpr e2 , SemExpr e1 , DeltaParam:: Delta delta ) ;
152
+
153
+ /**
154
+ * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
155
+ */
156
+ predicate hasConstantBound ( SemExpr e , int bound , boolean upper ) ;
157
+
158
+ /**
159
+ * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
160
+ */
161
+ predicate hasBound ( SemExpr e , SemExpr bound , int delta , boolean upper ) ;
162
+
163
+ /**
164
+ * Ignore the bound on this expression.
165
+ *
166
+ * This predicate is to keep the results identical to the original Java implementation. It should be
167
+ * removed once we have the new implementation matching the old results exactly.
168
+ */
169
+ predicate ignoreExprBound ( SemExpr e ) ;
170
+
171
+ /**
172
+ * Ignore any inferred zero lower bound on this expression.
173
+ *
174
+ * This predicate is to keep the results identical to the original Java implementation. It should be
175
+ * removed once we have the new implementation matching the old results exactly.
176
+ */
177
+ predicate ignoreZeroLowerBound ( SemExpr e ) ;
153
178
}
154
179
155
- module RangeStage< DeltaSig D, UtilSig< D > UtilParam > {
180
+ module RangeStage< DeltaSig D, UtilSig< D > LangParam > {
156
181
cached
157
182
private module RangeAnalysisCache {
158
183
cached
@@ -178,7 +203,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
178
203
*/
179
204
cached
180
205
predicate possibleReason ( SemGuard guard ) {
181
- guard = boundFlowCond ( _, _, _, _, _) or guard = UtilParam :: semEqFlowCond ( _, _, _, _, _)
206
+ guard = boundFlowCond ( _, _, _, _, _) or guard = LangParam :: semEqFlowCond ( _, _, _, _, _)
182
207
}
183
208
}
184
209
@@ -206,27 +231,27 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
206
231
private predicate boundCondition (
207
232
SemRelationalExpr comp , SemSsaVariable v , SemExpr e , float delta , boolean upper
208
233
) {
209
- comp .getLesserOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
234
+ comp .getLesserOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
210
235
e = comp .getGreaterOperand ( ) and
211
236
upper = true
212
237
or
213
- comp .getGreaterOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
238
+ comp .getGreaterOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
214
239
e = comp .getLesserOperand ( ) and
215
240
upper = false
216
241
or
217
242
exists ( SemSubExpr sub , SemConstantIntegerExpr c , float d |
218
243
// (v - d) - e < c
219
244
comp .getLesserOperand ( ) = sub and
220
245
comp .getGreaterOperand ( ) = c and
221
- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
246
+ sub .getLeftOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
222
247
sub .getRightOperand ( ) = e and
223
248
upper = true and
224
249
delta = d + c .getIntValue ( )
225
250
or
226
251
// (v - d) - e > c
227
252
comp .getGreaterOperand ( ) = sub and
228
253
comp .getLesserOperand ( ) = c and
229
- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
254
+ sub .getLeftOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
230
255
sub .getRightOperand ( ) = e and
231
256
upper = false and
232
257
delta = d + c .getIntValue ( )
@@ -235,15 +260,15 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
235
260
comp .getLesserOperand ( ) = sub and
236
261
comp .getGreaterOperand ( ) = c and
237
262
sub .getLeftOperand ( ) = e and
238
- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
263
+ sub .getRightOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
239
264
upper = false and
240
265
delta = d - c .getIntValue ( )
241
266
or
242
267
// e - (v - d) > c
243
268
comp .getGreaterOperand ( ) = sub and
244
269
comp .getLesserOperand ( ) = c and
245
270
sub .getLeftOperand ( ) = e and
246
- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
271
+ sub .getRightOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
247
272
upper = true and
248
273
delta = d - c .getIntValue ( )
249
274
)
@@ -339,14 +364,16 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
339
364
semImplies_v2 ( result , testIsTrue , boundFlowCond ( v , e , delta , upper , testIsTrue0 ) , testIsTrue0 )
340
365
)
341
366
or
342
- result = UtilParam :: semEqFlowCond ( v , e , D:: fromFloat ( delta ) , true , testIsTrue ) and
367
+ result = LangParam :: semEqFlowCond ( v , e , D:: fromFloat ( delta ) , true , testIsTrue ) and
343
368
( upper = true or upper = false )
344
369
or
345
370
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
346
371
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
347
- exists ( SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 , float oldDelta |
372
+ exists (
373
+ SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 , float oldDelta
374
+ |
348
375
guardEq =
349
- UtilParam :: semEqFlowCond ( v , UtilParam :: semSsaRead ( v2 , D:: fromFloat ( d1 ) ) , D:: fromFloat ( d2 ) ,
376
+ LangParam :: semEqFlowCond ( v , LangParam :: semSsaRead ( v2 , D:: fromFloat ( d1 ) ) , D:: fromFloat ( d2 ) ,
350
377
true , eqIsTrue ) and
351
378
result = boundFlowCond ( v2 , e , oldDelta , upper , testIsTrue ) and
352
379
// guardEq needs to control guard
@@ -394,7 +421,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
394
421
SemSsaVariable v , SemSsaReadPosition pos , SemExpr e , float delta , boolean upper ,
395
422
SemReason reason
396
423
) {
397
- UtilParam :: semSsaUpdateStep ( v , e , D:: fromFloat ( delta ) ) and
424
+ LangParam :: semSsaUpdateStep ( v , e , D:: fromFloat ( delta ) ) and
398
425
pos .hasReadOfVar ( v ) and
399
426
( upper = true or upper = false ) and
400
427
reason = TSemNoReason ( )
@@ -414,7 +441,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
414
441
Utils:: getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType and
415
442
exists ( SemGuard guard , boolean testIsTrue |
416
443
pos .hasReadOfVar ( v ) and
417
- guard = UtilParam :: semEqFlowCond ( v , e , D:: fromFloat ( delta ) , false , testIsTrue ) and
444
+ guard = LangParam :: semEqFlowCond ( v , e , D:: fromFloat ( delta ) , false , testIsTrue ) and
418
445
semGuardDirectlyControlsSsaRead ( guard , pos , testIsTrue ) and
419
446
reason = TSemCondReason ( guard )
420
447
)
@@ -436,7 +463,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
436
463
* - `upper = false` : `e2 >= e1 + delta`
437
464
*/
438
465
private predicate boundFlowStep ( SemExpr e2 , SemExpr e1 , float delta , boolean upper ) {
439
- UtilParam :: semValueFlowStep ( e2 , e1 , D:: fromFloat ( delta ) ) and
466
+ LangParam :: semValueFlowStep ( e2 , e1 , D:: fromFloat ( delta ) ) and
440
467
( upper = true or upper = false )
441
468
or
442
469
e2 .( SafeCastExpr ) .getOperand ( ) = e1 and
@@ -499,7 +526,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
499
526
delta = 0 and
500
527
upper = false
501
528
or
502
- Specific :: hasBound ( e2 , e1 , delta , upper )
529
+ LangParam :: hasBound ( e2 , e1 , delta , upper )
503
530
}
504
531
505
532
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
@@ -741,13 +768,13 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
741
768
* (for `upper = false`) bound of `b`.
742
769
*/
743
770
private predicate baseBound ( SemExpr e , float b , boolean upper ) {
744
- Specific :: hasConstantBound ( e , b , upper )
771
+ LangParam :: hasConstantBound ( e , b , upper )
745
772
or
746
773
upper = false and
747
774
b = 0 and
748
775
semPositive ( e .( SemBitAndExpr ) .getAnOperand ( ) ) and
749
776
// REVIEW: We let the language opt out here to preserve original results.
750
- not Specific :: ignoreZeroLowerBound ( e )
777
+ not LangParam :: ignoreZeroLowerBound ( e )
751
778
}
752
779
753
780
/**
0 commit comments