@@ -240,7 +240,10 @@ signature module BoundSig<DeltaSig D> {
240240}
241241
242242module 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
244247
245248 /**
246249 * An expression that does conversion, boxing, or unboxing
@@ -264,8 +267,8 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
264267 */
265268 private class SafeCastExpr extends ConvertOrBoxExpr {
266269 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 ) )
269272 }
270273 }
271274
@@ -275,14 +278,14 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
275278 private class NarrowingCastExpr extends ConvertOrBoxExpr {
276279 NarrowingCastExpr ( ) {
277280 not this instanceof SafeCastExpr and
278- typeBound ( UtilParam :: getTrackedType ( this ) , _, _)
281+ typeBound ( getTrackedType ( this ) , _, _)
279282 }
280283
281284 /** Gets the lower bound of the resulting type. */
282- int getLowerBound ( ) { typeBound ( UtilParam :: getTrackedType ( this ) , result , _) }
285+ int getLowerBound ( ) { typeBound ( getTrackedType ( this ) , result , _) }
283286
284287 /** Gets the upper bound of the resulting type. */
285- int getUpperBound ( ) { typeBound ( UtilParam :: getTrackedType ( this ) , _, result ) }
288+ int getUpperBound ( ) { typeBound ( getTrackedType ( this ) , _, result ) }
286289 }
287290
288291 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<
318321 */
319322 cached
320323 predicate possibleReason ( SemGuard guard ) {
321- guard = boundFlowCond ( _, _, _, _, _) or guard = UtilParam :: semEqFlowCond ( _, _, _, _, _)
324+ guard = boundFlowCond ( _, _, _, _, _) or guard = semEqFlowCond ( _, _, _, _, _)
322325 }
323326 }
324327
@@ -346,27 +349,27 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
346349 private predicate boundCondition (
347350 SemRelationalExpr comp , SemSsaVariable v , SemExpr e , float delta , boolean upper
348351 ) {
349- comp .getLesserOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( delta ) ) and
352+ comp .getLesserOperand ( ) = semSsaRead ( v , fromFloat ( delta ) ) and
350353 e = comp .getGreaterOperand ( ) and
351354 upper = true
352355 or
353- comp .getGreaterOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( delta ) ) and
356+ comp .getGreaterOperand ( ) = semSsaRead ( v , fromFloat ( delta ) ) and
354357 e = comp .getLesserOperand ( ) and
355358 upper = false
356359 or
357360 exists ( SemSubExpr sub , SemConstantIntegerExpr c , float d |
358361 // (v - d) - e < c
359362 comp .getLesserOperand ( ) = sub and
360363 comp .getGreaterOperand ( ) = c and
361- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
364+ sub .getLeftOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
362365 sub .getRightOperand ( ) = e and
363366 upper = true and
364367 delta = d + c .getIntValue ( )
365368 or
366369 // (v - d) - e > c
367370 comp .getGreaterOperand ( ) = sub and
368371 comp .getLesserOperand ( ) = c and
369- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
372+ sub .getLeftOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
370373 sub .getRightOperand ( ) = e and
371374 upper = false and
372375 delta = d + c .getIntValue ( )
@@ -375,15 +378,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
375378 comp .getLesserOperand ( ) = sub and
376379 comp .getGreaterOperand ( ) = c and
377380 sub .getLeftOperand ( ) = e and
378- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
381+ sub .getRightOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
379382 upper = false and
380383 delta = d - c .getIntValue ( )
381384 or
382385 // e - (v - d) > c
383386 comp .getGreaterOperand ( ) = sub and
384387 comp .getLesserOperand ( ) = c and
385388 sub .getLeftOperand ( ) = e and
386- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D :: fromFloat ( d ) ) and
389+ sub .getRightOperand ( ) = semSsaRead ( v , fromFloat ( d ) ) and
387390 upper = true and
388391 delta = d - c .getIntValue ( )
389392 )
@@ -453,8 +456,8 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
453456 ) and
454457 (
455458 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
458461 then
459462 upper = true and strengthen = - 1
460463 or
@@ -479,17 +482,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
479482 semImplies_v2 ( result , testIsTrue , boundFlowCond ( v , e , delta , upper , testIsTrue0 ) , testIsTrue0 )
480483 )
481484 or
482- result = UtilParam :: semEqFlowCond ( v , e , D :: fromFloat ( delta ) , true , testIsTrue ) and
485+ result = semEqFlowCond ( v , e , fromFloat ( delta ) , true , testIsTrue ) and
483486 ( upper = true or upper = false )
484487 or
485488 // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
486489 // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
487490 exists (
488491 SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 , float oldDelta
489492 |
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
493494 result = boundFlowCond ( v2 , e , oldDelta , upper , testIsTrue ) and
494495 // guardEq needs to control guard
495496 guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue ) and
@@ -536,7 +537,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
536537 SemSsaVariable v , SemSsaReadPosition pos , SemExpr e , float delta , boolean upper ,
537538 SemReason reason
538539 ) {
539- UtilParam :: semSsaUpdateStep ( v , e , D :: fromFloat ( delta ) ) and
540+ semSsaUpdateStep ( v , e , fromFloat ( delta ) ) and
540541 pos .hasReadOfVar ( v ) and
541542 ( upper = true or upper = false ) and
542543 reason = TSemNoReason ( )
@@ -553,23 +554,23 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
553554 private predicate unequalFlowStepIntegralSsa (
554555 SemSsaVariable v , SemSsaReadPosition pos , SemExpr e , float delta , SemReason reason
555556 ) {
556- UtilParam :: getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType and
557+ getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType and
557558 exists ( SemGuard guard , boolean testIsTrue |
558559 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
560561 semGuardDirectlyControlsSsaRead ( guard , pos , testIsTrue ) and
561562 reason = TSemCondReason ( guard )
562563 )
563564 }
564565
565566 /** Holds if `e >= 1` as determined by sign analysis. */
566567 private predicate strictlyPositiveIntegralExpr ( SemExpr e ) {
567- semStrictlyPositive ( e ) and UtilParam :: getTrackedType ( e ) instanceof SemIntegerType
568+ semStrictlyPositive ( e ) and getTrackedType ( e ) instanceof SemIntegerType
568569 }
569570
570571 /** Holds if `e <= -1` as determined by sign analysis. */
571572 private predicate strictlyNegativeIntegralExpr ( SemExpr e ) {
572- semStrictlyNegative ( e ) and UtilParam :: getTrackedType ( e ) instanceof SemIntegerType
573+ semStrictlyNegative ( e ) and getTrackedType ( e ) instanceof SemIntegerType
573574 }
574575
575576 /**
@@ -578,7 +579,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
578579 * - `upper = false` : `e2 >= e1 + delta`
579580 */
580581 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
582583 ( upper = true or upper = false )
583584 or
584585 e2 .( SafeCastExpr ) .getOperand ( ) = e1 and
@@ -641,7 +642,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
641642 delta = 0 and
642643 upper = false
643644 or
644- LangParam :: hasBound ( e2 , e1 , D :: fromFloat ( delta ) , upper )
645+ hasBound ( e2 , e1 , fromFloat ( delta ) , upper )
645646 }
646647
647648 /** Holds if `e2 = e1 * factor` and `factor > 0`. */
@@ -883,13 +884,13 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
883884 * (for `upper = false`) bound of `b`.
884885 */
885886 private predicate baseBound ( SemExpr e , float b , boolean upper ) {
886- LangParam :: hasConstantBound ( e , D :: fromFloat ( b ) , upper )
887+ hasConstantBound ( e , fromFloat ( b ) , upper )
887888 or
888889 upper = false and
889890 b = 0 and
890891 semPositive ( e .( SemBitAndExpr ) .getAnOperand ( ) ) and
891892 // REVIEW: We let the language opt out here to preserve original results.
892- not LangParam :: ignoreZeroLowerBound ( e )
893+ not ignoreZeroLowerBound ( e )
893894 }
894895
895896 /**
@@ -923,9 +924,9 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
923924 SemExpr e , SemBound b , float delta , boolean upper , boolean fromBackEdge , float origdelta ,
924925 SemReason reason
925926 ) {
926- not Specific :: ignoreExprBound ( e ) and
927+ not ignoreExprBound ( e ) and
927928 (
928- e = b .getExpr ( D :: fromFloat ( delta ) ) and
929+ e = b .getExpr ( fromFloat ( delta ) ) and
929930 ( upper = true or upper = false ) and
930931 fromBackEdge = false and
931932 origdelta = delta and
0 commit comments