@@ -203,6 +203,11 @@ signature module Semantic {
203203 Expr getDefiningExpr ( ) ;
204204 }
205205
206+ /**
207+ * Holds if the value of `dest` is known to be `src + delta`.
208+ */
209+ predicate additionalValueFlowStep ( Expr dest , Expr src , int delta ) ;
210+
206211 predicate conversionCannotOverflow ( Type fromType , Type toType ) ;
207212}
208213
@@ -277,11 +282,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
277282 */
278283 predicate ignoreExprBound ( Sem:: Expr e ) ;
279284
280- /**
281- * Holds if the value of `dest` is known to be `src + delta`.
282- */
283- predicate additionalValueFlowStep ( Sem:: Expr dest , Sem:: Expr src , D:: Delta delta ) ;
284-
285285 /**
286286 * Gets the type that range analysis should use to track the result of the specified expression,
287287 * if a type other than the original type of the expression is to be used.
@@ -304,8 +304,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
304304}
305305
306306signature module UtilSig< Semantic Sem, DeltaSig DeltaParam> {
307- predicate semValueFlowStep ( Sem:: Expr e2 , Sem:: Expr e1 , DeltaParam:: Delta delta ) ;
308-
309307 /**
310308 * Gets the type used to track the specified source variable's range information.
311309 *
@@ -711,7 +709,7 @@ module RangeStage<
711709 * - `upper = false` : `e2 >= e1 + delta`
712710 */
713711 private predicate boundFlowStep ( Sem:: Expr e2 , Sem:: Expr e1 , D:: Delta delta , boolean upper ) {
714- semValueFlowStep ( e2 , e1 , delta ) and
712+ valueFlowStep ( e2 , e1 , delta ) and
715713 ( upper = true or upper = false )
716714 or
717715 e2 .( SafeCastExpr ) .getOperand ( ) = e1 and
@@ -1344,8 +1342,8 @@ module RangeStage<
13441342 Sem:: AddExpr add , boolean upper , SemBound b , boolean isLeft , D:: Delta delta ,
13451343 boolean fromBackEdge , D:: Delta origdelta , SemReason reason
13461344 ) {
1347- // `semValueFlowStep ` already handles the case where one of the operands is a constant.
1348- not semValueFlowStep ( add , _, _) and
1345+ // `valueFlowStep ` already handles the case where one of the operands is a constant.
1346+ not valueFlowStep ( add , _, _) and
13491347 (
13501348 isLeft = true and
13511349 bounded ( add .getLeftOperand ( ) , b , delta , upper , fromBackEdge , origdelta , reason )
@@ -1364,8 +1362,8 @@ module RangeStage<
13641362 Sem:: SubExpr sub , boolean upper , SemBound b , D:: Delta delta , boolean fromBackEdge ,
13651363 D:: Delta origdelta , SemReason reason
13661364 ) {
1367- // `semValueFlowStep ` already handles the case where one of the operands is a constant.
1368- not semValueFlowStep ( sub , _, _) and
1365+ // `valueFlowStep ` already handles the case where one of the operands is a constant.
1366+ not valueFlowStep ( sub , _, _) and
13691367 bounded ( sub .getLeftOperand ( ) , b , delta , upper , fromBackEdge , origdelta , reason )
13701368 }
13711369
@@ -1380,8 +1378,8 @@ module RangeStage<
13801378 private predicate boundedSubOperandRight (
13811379 Sem:: SubExpr sub , boolean upper , D:: Delta delta , boolean fromBackEdge
13821380 ) {
1383- // `semValueFlowStep ` already handles the case where one of the operands is a constant.
1384- not semValueFlowStep ( sub , _, _) and
1381+ // `valueFlowStep ` already handles the case where one of the operands is a constant.
1382+ not valueFlowStep ( sub , _, _) and
13851383 bounded ( sub .getRightOperand ( ) , any ( SemZeroBound zb ) , delta , upper .booleanNot ( ) , fromBackEdge , _,
13861384 _)
13871385 }
0 commit comments