6363 * back-edge as a precise bound might require traversing a loop once).
6464 */
6565
66- private import RangeAnalysisSpecific as Specific
6766private import RangeUtils as Utils
6867private import SignAnalysisCommon
6968private import ModulusAnalysis
@@ -150,9 +149,35 @@ signature module UtilSig<DeltaSig DeltaParam> {
150149 predicate semSsaUpdateStep ( SemSsaExplicitUpdate v , SemExpr e , DeltaParam:: Delta delta ) ;
151150
152151 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 ) ;
153178}
154179
155- module RangeStage< DeltaSig D, UtilSig< D > UtilParam > {
180+ module RangeStage< DeltaSig D, UtilSig< D > LangParam > {
156181 cached
157182 private module RangeAnalysisCache {
158183 cached
@@ -178,7 +203,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
178203 */
179204 cached
180205 predicate possibleReason ( SemGuard guard ) {
181- guard = boundFlowCond ( _, _, _, _, _) or guard = UtilParam :: semEqFlowCond ( _, _, _, _, _)
206+ guard = boundFlowCond ( _, _, _, _, _) or guard = LangParam :: semEqFlowCond ( _, _, _, _, _)
182207 }
183208 }
184209
@@ -206,27 +231,27 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
206231 private predicate boundCondition (
207232 SemRelationalExpr comp , SemSsaVariable v , SemExpr e , float delta , boolean upper
208233 ) {
209- comp .getLesserOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
234+ comp .getLesserOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
210235 e = comp .getGreaterOperand ( ) and
211236 upper = true
212237 or
213- comp .getGreaterOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
238+ comp .getGreaterOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( delta ) ) and
214239 e = comp .getLesserOperand ( ) and
215240 upper = false
216241 or
217242 exists ( SemSubExpr sub , SemConstantIntegerExpr c , float d |
218243 // (v - d) - e < c
219244 comp .getLesserOperand ( ) = sub and
220245 comp .getGreaterOperand ( ) = c and
221- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
246+ sub .getLeftOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
222247 sub .getRightOperand ( ) = e and
223248 upper = true and
224249 delta = d + c .getIntValue ( )
225250 or
226251 // (v - d) - e > c
227252 comp .getGreaterOperand ( ) = sub and
228253 comp .getLesserOperand ( ) = c and
229- sub .getLeftOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
254+ sub .getLeftOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
230255 sub .getRightOperand ( ) = e and
231256 upper = false and
232257 delta = d + c .getIntValue ( )
@@ -235,15 +260,15 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
235260 comp .getLesserOperand ( ) = sub and
236261 comp .getGreaterOperand ( ) = c and
237262 sub .getLeftOperand ( ) = e and
238- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
263+ sub .getRightOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
239264 upper = false and
240265 delta = d - c .getIntValue ( )
241266 or
242267 // e - (v - d) > c
243268 comp .getGreaterOperand ( ) = sub and
244269 comp .getLesserOperand ( ) = c and
245270 sub .getLeftOperand ( ) = e and
246- sub .getRightOperand ( ) = UtilParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
271+ sub .getRightOperand ( ) = LangParam :: semSsaRead ( v , D:: fromFloat ( d ) ) and
247272 upper = true and
248273 delta = d - c .getIntValue ( )
249274 )
@@ -339,14 +364,16 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
339364 semImplies_v2 ( result , testIsTrue , boundFlowCond ( v , e , delta , upper , testIsTrue0 ) , testIsTrue0 )
340365 )
341366 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
343368 ( upper = true or upper = false )
344369 or
345370 // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
346371 // 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+ |
348375 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 ) ,
350377 true , eqIsTrue ) and
351378 result = boundFlowCond ( v2 , e , oldDelta , upper , testIsTrue ) and
352379 // guardEq needs to control guard
@@ -394,7 +421,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
394421 SemSsaVariable v , SemSsaReadPosition pos , SemExpr e , float delta , boolean upper ,
395422 SemReason reason
396423 ) {
397- UtilParam :: semSsaUpdateStep ( v , e , D:: fromFloat ( delta ) ) and
424+ LangParam :: semSsaUpdateStep ( v , e , D:: fromFloat ( delta ) ) and
398425 pos .hasReadOfVar ( v ) and
399426 ( upper = true or upper = false ) and
400427 reason = TSemNoReason ( )
@@ -414,7 +441,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
414441 Utils:: getTrackedTypeForSsaVariable ( v ) instanceof SemIntegerType and
415442 exists ( SemGuard guard , boolean testIsTrue |
416443 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
418445 semGuardDirectlyControlsSsaRead ( guard , pos , testIsTrue ) and
419446 reason = TSemCondReason ( guard )
420447 )
@@ -436,7 +463,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
436463 * - `upper = false` : `e2 >= e1 + delta`
437464 */
438465 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
440467 ( upper = true or upper = false )
441468 or
442469 e2 .( SafeCastExpr ) .getOperand ( ) = e1 and
@@ -499,7 +526,7 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
499526 delta = 0 and
500527 upper = false
501528 or
502- Specific :: hasBound ( e2 , e1 , delta , upper )
529+ LangParam :: hasBound ( e2 , e1 , delta , upper )
503530 }
504531
505532 /** Holds if `e2 = e1 * factor` and `factor > 0`. */
@@ -741,13 +768,13 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
741768 * (for `upper = false`) bound of `b`.
742769 */
743770 private predicate baseBound ( SemExpr e , float b , boolean upper ) {
744- Specific :: hasConstantBound ( e , b , upper )
771+ LangParam :: hasConstantBound ( e , b , upper )
745772 or
746773 upper = false and
747774 b = 0 and
748775 semPositive ( e .( SemBitAndExpr ) .getAnOperand ( ) ) and
749776 // REVIEW: We let the language opt out here to preserve original results.
750- not Specific :: ignoreZeroLowerBound ( e )
777+ not LangParam :: ignoreZeroLowerBound ( e )
751778 }
752779
753780 /**
0 commit comments