@@ -98,29 +98,6 @@ module RangeAnalysis {
9898 )
9999 }
100100
101- /**
102- * Holds if the given node has a unique data flow predecessor.
103- */
104- pragma [ noinline]
105- private predicate hasUniquePredecessor ( DataFlow:: Node node ) {
106- isRelevant ( node ) and
107- strictcount ( node .getAPredecessor ( ) ) = 1 and
108- // exclude parameters with default values
109- not exists ( Parameter p |
110- DataFlow:: parameterNode ( p ) = node and
111- exists ( p .getDefault ( ) )
112- )
113- }
114-
115- /**
116- * Gets the definition of `node`, without unfolding phi nodes.
117- */
118- DataFlow:: Node getDefinition ( DataFlow:: Node node ) {
119- if hasUniquePredecessor ( node )
120- then result = getDefinition ( node .getAPredecessor ( ) )
121- else result = node
122- }
123-
124101 /**
125102 * Gets a data flow node holding the result of the add/subtract operation in
126103 * the given increment/decrement expression.
@@ -229,8 +206,8 @@ module RangeAnalysis {
229206 * Holds if `r` can be modelled as `r = root * sign + bias`.
230207 */
231208 predicate linearDefinition ( DataFlow:: Node r , DataFlow:: Node root , int sign , Bias bias ) {
232- if hasUniquePredecessor ( r )
233- then linearDefinition ( r .getAPredecessor ( ) , root , sign , bias )
209+ if exists ( r . getImmediatePredecessor ( ) )
210+ then linearDefinition ( r .getImmediatePredecessor ( ) , root , sign , bias )
234211 else
235212 if linearDefinitionStep ( r , _, _, _)
236213 then
@@ -257,8 +234,8 @@ module RangeAnalysis {
257234 predicate linearDefinitionSum (
258235 DataFlow:: Node r , DataFlow:: Node xroot , int xsign , DataFlow:: Node yroot , int ysign , Bias bias
259236 ) {
260- if hasUniquePredecessor ( r )
261- then linearDefinitionSum ( r .getAPredecessor ( ) , xroot , xsign , yroot , ysign , bias )
237+ if exists ( r . getImmediatePredecessor ( ) )
238+ then linearDefinitionSum ( r .getImmediatePredecessor ( ) , xroot , xsign , yroot , ysign , bias )
262239 else
263240 if exists ( r .asExpr ( ) .getIntValue ( ) )
264241 then none ( ) // do not model constants as sums
@@ -336,7 +313,8 @@ module RangeAnalysis {
336313 ConditionGuardNode guard , DataFlow:: Node a , int asign , string operator , DataFlow:: Node b ,
337314 int bsign , Bias bias
338315 ) {
339- exists ( Comparison compare | compare = getDefinition ( guard .getTest ( ) .flow ( ) ) .asExpr ( ) |
316+ exists ( Comparison compare |
317+ compare = guard .getTest ( ) .flow ( ) .getImmediatePredecessor * ( ) .asExpr ( ) and
340318 linearComparison ( compare , a , asign , b , bsign , bias ) and
341319 (
342320 guard .getOutcome ( ) = true and operator = compare .getOperator ( )
0 commit comments