@@ -240,7 +240,10 @@ signature module BoundSig<DeltaSig D> {
240
240
}
241
241
242
242
module RangeStage< DeltaSig D, BoundSig< D > Bounds, LangSig< D > LangParam, UtilSig< D > UtilParam> {
243
- private import Bounds // TODO: remove this import?
243
+ private import Bounds
244
+ private import LangParam
245
+ private import UtilParam
246
+ private import D
244
247
245
248
/**
246
249
* An expression that does conversion, boxing, or unboxing
@@ -264,8 +267,8 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
264
267
*/
265
268
private class SafeCastExpr extends ConvertOrBoxExpr {
266
269
SafeCastExpr ( ) {
267
- conversionCannotOverflow ( UtilParam :: getTrackedType ( pragma [ only_bind_into ] ( getOperand ( ) ) ) ,
268
- UtilParam :: getTrackedType ( this ) )
270
+ conversionCannotOverflow ( getTrackedType ( pragma [ only_bind_into ] ( getOperand ( ) ) ) ,
271
+ getTrackedType ( this ) )
269
272
}
270
273
}
271
274
@@ -275,14 +278,14 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
275
278
private class NarrowingCastExpr extends ConvertOrBoxExpr {
276
279
NarrowingCastExpr ( ) {
277
280
not this instanceof SafeCastExpr and
278
- typeBound ( UtilParam :: getTrackedType ( this ) , _, _)
281
+ typeBound ( getTrackedType ( this ) , _, _)
279
282
}
280
283
281
284
/** Gets the lower bound of the resulting type. */
282
- int getLowerBound ( ) { typeBound ( UtilParam :: getTrackedType ( this ) , result , _) }
285
+ int getLowerBound ( ) { typeBound ( getTrackedType ( this ) , result , _) }
283
286
284
287
/** Gets the upper bound of the resulting type. */
285
- int getUpperBound ( ) { typeBound ( UtilParam :: getTrackedType ( this ) , _, result ) }
288
+ int getUpperBound ( ) { typeBound ( getTrackedType ( this ) , _, result ) }
286
289
}
287
290
288
291
private module SignAnalysisInstantiated = SignAnalysis< D , UtilParam > ; // TODO: will this cause reevaluation if it's instantiated with the same DeltaSig and UtilParam multiple times?
@@ -318,7 +321,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
318
321
*/
319
322
cached
320
323
predicate possibleReason ( SemGuard guard ) {
321
- guard = boundFlowCond ( _, _, _, _, _) or guard = UtilParam :: semEqFlowCond ( _, _, _, _, _)
324
+ guard = boundFlowCond ( _, _, _, _, _) or guard = semEqFlowCond ( _, _, _, _, _)
322
325
}
323
326
}
324
327
@@ -346,27 +349,27 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
346
349
private predicate boundCondition (
347
350
SemRelationalExpr comp , SemSsaVariable v , SemExpr e , float delta , boolean upper
348
351
) {
349
- comp .getLesserOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( delta ) ) and
352
+ comp .getLesserOperand ( ) = semSsaRead ( v , fromFloat ( delta ) ) and
350
353
e = comp .getGreaterOperand ( ) and
351
354
upper = true
352
355
or
353
- comp .getGreaterOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( delta ) ) and
356
+ comp .getGreaterOperand ( ) = semSsaRead ( v , fromFloat ( delta ) ) and
354
357
e = comp .getLesserOperand ( ) and
355
358
upper = false
356
359
or
357
360
exists ( SemSubExpr sub , SemConstantIntegerExpr c , float d |
358
361
// (v - d) - e < c
359
362
comp .getLesserOperand ( ) = sub and
360
363
comp .getGreaterOperand ( ) = c and
361
- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
364
+ sub .getLeftOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
362
365
sub .getRightOperand ( ) = e and
363
366
upper = true and
364
367
delta = d + c .getIntValue ( )
365
368
or
366
369
// (v - d) - e > c
367
370
comp .getGreaterOperand ( ) = sub and
368
371
comp .getLesserOperand ( ) = c and
369
- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
372
+ sub .getLeftOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
370
373
sub .getRightOperand ( ) = e and
371
374
upper = false and
372
375
delta = d + c .getIntValue ( )
@@ -375,15 +378,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
375
378
comp .getLesserOperand ( ) = sub and
376
379
comp .getGreaterOperand ( ) = c and
377
380
sub .getLeftOperand ( ) = e and
378
- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
381
+ sub .getRightOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
379
382
upper = false and
380
383
delta = d - c .getIntValue ( )
381
384
or
382
385
// e - (v - d) > c
383
386
comp .getGreaterOperand ( ) = sub and
384
387
comp .getLesserOperand ( ) = c and
385
388
sub .getLeftOperand ( ) = e and
386
- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
389
+ sub .getRightOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
387
390
upper = true and
388
391
delta = d - c .getIntValue ( )
389
392
)
@@ -453,8 +456,8 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
453
456
) and
454
457
(
455
458
if
456
- UtilParam :: getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType or
457
- UtilParam :: getTrackedTypeForSsaVariable ( v ) instanceof SemAddressType
459
+ getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType or
460
+ getTrackedTypeForSsaVariable ( v ) instanceof SemAddressType
458
461
then
459
462
upper = true and strengthen = - 1
460
463
or
@@ -479,17 +482,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
479
482
semImplies_v2 ( result , testIsTrue , boundFlowCond ( v , e , delta , upper , testIsTrue0 ) , testIsTrue0 )
480
483
)
481
484
or
482
- result = UtilParam :: semEqFlowCond ( v , e , D :: fromFloat ( delta ) , true , testIsTrue ) and
485
+ result = semEqFlowCond ( v , e , fromFloat ( delta ) , true , testIsTrue ) and
483
486
( upper = true or upper = false )
484
487
or
485
488
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
486
489
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
487
490
exists (
488
491
SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 , float oldDelta
489
492
|
490
- guardEq =
491
- UtilParam:: semEqFlowCond ( v , UtilParam:: semSsaRead ( v2 , D:: fromFloat ( d1 ) ) , D:: fromFloat ( d2 ) ,
492
- true , eqIsTrue ) and
493
+ guardEq = semEqFlowCond ( v , semSsaRead ( v2 , fromFloat ( d1 ) ) , fromFloat ( d2 ) , true , eqIsTrue ) and
493
494
result = boundFlowCond ( v2 , e , oldDelta , upper , testIsTrue ) and
494
495
// guardEq needs to control guard
495
496
guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue ) and
@@ -536,7 +537,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
536
537
SemSsaVariable v , SemSsaReadPosition pos , SemExpr e , float delta , boolean upper ,
537
538
SemReason reason
538
539
) {
539
- UtilParam :: semSsaUpdateStep ( v , e , D :: fromFloat ( delta ) ) and
540
+ semSsaUpdateStep ( v , e , fromFloat ( delta ) ) and
540
541
pos .hasReadOfVar ( v ) and
541
542
( upper = true or upper = false ) and
542
543
reason = TSemNoReason ( )
@@ -553,23 +554,23 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
553
554
private predicate unequalFlowStepIntegralSsa (
554
555
SemSsaVariable v , SemSsaReadPosition pos , SemExpr e , float delta , SemReason reason
555
556
) {
556
- UtilParam :: getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType and
557
+ getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType and
557
558
exists ( SemGuard guard , boolean testIsTrue |
558
559
pos .hasReadOfVar ( v ) and
559
- guard = UtilParam :: semEqFlowCond ( v , e , D :: fromFloat ( delta ) , false , testIsTrue ) and
560
+ guard = semEqFlowCond ( v , e , fromFloat ( delta ) , false , testIsTrue ) and
560
561
semGuardDirectlyControlsSsaRead ( guard , pos , testIsTrue ) and
561
562
reason = TSemCondReason ( guard )
562
563
)
563
564
}
564
565
565
566
/** Holds if `e >= 1` as determined by sign analysis. */
566
567
private predicate strictlyPositiveIntegralExpr ( SemExpr e ) {
567
- semStrictlyPositive ( e ) and UtilParam :: getTrackedType ( e ) instanceof SemIntegerType
568
+ semStrictlyPositive ( e ) and getTrackedType ( e ) instanceof SemIntegerType
568
569
}
569
570
570
571
/** Holds if `e <= -1` as determined by sign analysis. */
571
572
private predicate strictlyNegativeIntegralExpr ( SemExpr e ) {
572
- semStrictlyNegative ( e ) and UtilParam :: getTrackedType ( e ) instanceof SemIntegerType
573
+ semStrictlyNegative ( e ) and getTrackedType ( e ) instanceof SemIntegerType
573
574
}
574
575
575
576
/**
@@ -578,7 +579,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
578
579
* - `upper = false` : `e2 >= e1 + delta`
579
580
*/
580
581
private predicate boundFlowStep ( SemExpr e2 , SemExpr e1 , float delta , boolean upper ) {
581
- UtilParam :: semValueFlowStep ( e2 , e1 , D :: fromFloat ( delta ) ) and
582
+ semValueFlowStep ( e2 , e1 , fromFloat ( delta ) ) and
582
583
( upper = true or upper = false )
583
584
or
584
585
e2 .( SafeCastExpr ) .getOperand ( ) = e1 and
@@ -641,7 +642,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
641
642
delta = 0 and
642
643
upper = false
643
644
or
644
- LangParam :: hasBound ( e2 , e1 , D :: fromFloat ( delta ) , upper )
645
+ hasBound ( e2 , e1 , fromFloat ( delta ) , upper )
645
646
}
646
647
647
648
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
@@ -883,13 +884,13 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
883
884
* (for `upper = false`) bound of `b`.
884
885
*/
885
886
private predicate baseBound ( SemExpr e , float b , boolean upper ) {
886
- LangParam :: hasConstantBound ( e , D :: fromFloat ( b ) , upper )
887
+ hasConstantBound ( e , fromFloat ( b ) , upper )
887
888
or
888
889
upper = false and
889
890
b = 0 and
890
891
semPositive ( e .( SemBitAndExpr ) .getAnOperand ( ) ) and
891
892
// REVIEW: We let the language opt out here to preserve original results.
892
- not LangParam :: ignoreZeroLowerBound ( e )
893
+ not ignoreZeroLowerBound ( e )
893
894
}
894
895
895
896
/**
@@ -923,9 +924,9 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
923
924
SemExpr e , SemBound b , float delta , boolean upper , boolean fromBackEdge , float origdelta ,
924
925
SemReason reason
925
926
) {
926
- not Specific :: ignoreExprBound ( e ) and
927
+ not ignoreExprBound ( e ) and
927
928
(
928
- e = b .getExpr ( D :: fromFloat ( delta ) ) and
929
+ e = b .getExpr ( fromFloat ( delta ) ) and
929
930
( upper = true or upper = false ) and
930
931
fromBackEdge = false and
931
932
origdelta = delta and
0 commit comments