@@ -111,25 +111,24 @@ float widenUpperBound(Type type, float ub) {
111111 * compilation units, which doesn't necessarily have a getValue() result from the extractor.
112112 */
113113private string getValue ( Expr e ) {
114- if exists ( e .getValue ( ) )
115- then result = e .getValue ( )
116- else
117- /*
118- * It should be safe to propagate the initialization value to a variable if:
119- * The type of v is const, and
120- * The type of v is not volatile, and
121- * Either:
122- * v is a local/global variable, or
123- * v is a static member variable
124- */
125-
126- exists ( VariableAccess access , StaticStorageDurationVariable v |
127- not v .getUnderlyingType ( ) .isVolatile ( ) and
128- v .getUnderlyingType ( ) .isConst ( ) and
129- e = access and
130- v = access .getTarget ( ) and
131- result = getValue ( v .getAnAssignedValue ( ) )
132- )
114+ result = e .getValue ( )
115+ or
116+ not exists ( e .getValue ( ) ) and
117+ /*
118+ * It should be safe to propagate the initialization value to a variable if:
119+ * The type of v is const, and
120+ * The type of v is not volatile, and
121+ * Either:
122+ * v is a local/global variable, or
123+ * v is a static member variable
124+ */
125+
126+ exists ( StaticStorageDurationVariable v |
127+ not v .getUnderlyingType ( ) .isVolatile ( ) and
128+ v .getUnderlyingType ( ) .isConst ( ) and
129+ v = e .( VariableAccess ) .getTarget ( ) and
130+ result = getValue ( v .getAnAssignedValue ( ) )
131+ )
133132}
134133
135134/**
@@ -1214,7 +1213,7 @@ private float getLowerBoundsImpl(Expr expr) {
12141213 // equal to `min(-y + 1,y - 1)`.
12151214 exists ( float childLB |
12161215 childLB = getFullyConvertedLowerBounds ( remExpr .getAnOperand ( ) ) and
1217- not childLB >= 0
1216+ childLB < 0
12181217 |
12191218 result = getFullyConvertedLowerBounds ( remExpr .getRightOperand ( ) ) - 1
12201219 or
@@ -1426,8 +1425,7 @@ private float getUpperBoundsImpl(Expr expr) {
14261425 // adding `-rhsLB` to the set of upper bounds.
14271426 exists ( float rhsLB |
14281427 rhsLB = getFullyConvertedLowerBounds ( remExpr .getRightOperand ( ) ) and
1429- not rhsLB >= 0
1430- |
1428+ rhsLB < 0 and
14311429 result = - rhsLB + 1
14321430 )
14331431 )
@@ -1572,8 +1570,7 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
15721570 exists ( VariableAccess access , Expr guard , boolean branch , float defLB , float guardLB |
15731571 phi .isGuardPhi ( v , access , guard , branch ) and
15741572 lowerBoundFromGuard ( guard , access , guardLB , branch ) and
1575- defLB = getFullyConvertedLowerBounds ( access )
1576- |
1573+ defLB = getFullyConvertedLowerBounds ( access ) and
15771574 // Compute the maximum of `guardLB` and `defLB`.
15781575 if guardLB > defLB then result = guardLB else result = defLB
15791576 )
@@ -1597,8 +1594,7 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
15971594 exists ( VariableAccess access , Expr guard , boolean branch , float defUB , float guardUB |
15981595 phi .isGuardPhi ( v , access , guard , branch ) and
15991596 upperBoundFromGuard ( guard , access , guardUB , branch ) and
1600- defUB = getFullyConvertedUpperBounds ( access )
1601- |
1597+ defUB = getFullyConvertedUpperBounds ( access ) and
16021598 // Compute the minimum of `guardUB` and `defUB`.
16031599 if guardUB < defUB then result = guardUB else result = defUB
16041600 )
@@ -1762,31 +1758,18 @@ private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, bo
17621758}
17631759
17641760/**
1765- * This predicate simplifies the results returned by
1766- * `linearBoundFromGuard`.
1761+ * This predicate simplifies the results returned by `linearBoundFromGuard`.
17671762 */
17681763private predicate boundFromGuard (
17691764 Expr guard , VariableAccess v , float boundValue , boolean isLowerBound ,
17701765 RelationStrictness strictness , boolean branch
17711766) {
17721767 exists ( float p , float q , float r , boolean isLB |
17731768 linearBoundFromGuard ( guard , v , p , q , r , isLB , strictness , branch ) and
1774- boundValue = ( r - q ) / p
1775- |
1769+ boundValue = ( r - q ) / p and
17761770 // If the multiplier is negative then the direction of the comparison
17771771 // needs to be flipped.
1778- p > 0 and isLowerBound = isLB
1779- or
1780- p < 0 and isLowerBound = isLB .booleanNot ( )
1781- )
1782- or
1783- // When `!e` is true, we know that `0 <= e <= 0`
1784- exists ( float p , float q , Expr e |
1785- linearAccess ( e , v , p , q ) and
1786- eqZeroWithNegate ( guard , e , true , branch ) and
1787- boundValue = ( 0.0 - q ) / p and
1788- isLowerBound = [ false , true ] and
1789- strictness = Nonstrict ( )
1772+ if p < 0 then isLowerBound = isLB .booleanNot ( ) else isLowerBound = isLB
17901773 )
17911774}
17921775
@@ -1796,54 +1779,57 @@ private predicate boundFromGuard(
17961779 * lower or upper bound for `v`.
17971780 */
17981781private predicate linearBoundFromGuard (
1799- ComparisonOperation guard , VariableAccess v , float p , float q , float boundValue ,
1782+ Expr guard , VariableAccess v , float p , float q , float r ,
18001783 boolean isLowerBound , // Is this a lower or an upper bound?
18011784 RelationStrictness strictness , boolean branch // Which control-flow branch is this bound valid on?
18021785) {
1803- // For the comparison x < RHS, we create two bounds:
1804- //
1805- // 1. x < upperbound(RHS)
1806- // 2. x >= typeLowerBound(RHS.getUnspecifiedType())
1807- //
1808- exists ( Expr lhs , Expr rhs , RelationDirection dir , RelationStrictness st |
1809- linearAccess ( lhs , v , p , q ) and
1810- relOpWithSwapAndNegate ( guard , lhs , rhs , dir , st , branch )
1811- |
1812- isLowerBound = directionIsGreater ( dir ) and
1813- strictness = st and
1814- getBounds ( rhs , boundValue , isLowerBound )
1786+ exists ( Expr lhs | linearAccess ( lhs , v , p , q ) |
1787+ // For the comparison x < RHS, we create the following bounds:
1788+ // 1. x < upperbound(RHS)
1789+ // 2. x >= typeLowerBound(RHS.getUnspecifiedType())
1790+ exists ( Expr rhs , RelationDirection dir , RelationStrictness st |
1791+ relOpWithSwapAndNegate ( guard , lhs , rhs , dir , st , branch )
1792+ |
1793+ isLowerBound = directionIsGreater ( dir ) and
1794+ strictness = st and
1795+ r = getBounds ( rhs , isLowerBound )
1796+ or
1797+ isLowerBound = directionIsLesser ( dir ) and
1798+ strictness = Nonstrict ( ) and
1799+ r = getExprTypeBounds ( rhs , isLowerBound )
1800+ )
18151801 or
1816- isLowerBound = directionIsLesser ( dir ) and
1817- strictness = Nonstrict ( ) and
1818- exprTypeBounds ( rhs , boundValue , isLowerBound )
1819- )
1820- or
1821- // For x == RHS, we create the following bounds:
1822- //
1823- // 1. x <= upperbound(RHS)
1824- // 2. x >= lowerbound(RHS)
1825- //
1826- exists ( Expr lhs , Expr rhs |
1827- linearAccess ( lhs , v , p , q ) and
1828- eqOpWithSwapAndNegate ( guard , lhs , rhs , true , branch ) and
1829- getBounds ( rhs , boundValue , isLowerBound ) and
1802+ // For x == RHS, we create the following bounds:
1803+ // 1. x <= upperbound(RHS)
1804+ // 2. x >= lowerbound(RHS)
1805+ exists ( Expr rhs |
1806+ eqOpWithSwapAndNegate ( guard , lhs , rhs , true , branch ) and
1807+ r = getBounds ( rhs , isLowerBound ) and
1808+ strictness = Nonstrict ( )
1809+ )
1810+ or
1811+ // When `x` is equal to 0 we create the following bounds:
1812+ // 1. x <= 0
1813+ // 2. x >= 0
1814+ eqZeroWithNegate ( guard , lhs , true , branch ) and
1815+ r = 0.0 and
1816+ isLowerBound = [ false , true ] and
18301817 strictness = Nonstrict ( )
18311818 )
1832- // x != RHS and !x are handled elsewhere
18331819}
18341820
1835- /** Utility for `linearBoundFromGuard `. */
1836- private predicate getBounds ( Expr expr , float boundValue , boolean isLowerBound ) {
1837- isLowerBound = true and boundValue = getFullyConvertedLowerBounds ( expr )
1821+ /** Get the fully converted lower or upper bounds of `expr` based on `isLowerBound `. */
1822+ private float getBounds ( Expr expr , boolean isLowerBound ) {
1823+ isLowerBound = true and result = getFullyConvertedLowerBounds ( expr )
18381824 or
1839- isLowerBound = false and boundValue = getFullyConvertedUpperBounds ( expr )
1825+ isLowerBound = false and result = getFullyConvertedUpperBounds ( expr )
18401826}
18411827
18421828/** Utility for `linearBoundFromGuard`. */
1843- private predicate exprTypeBounds ( Expr expr , float boundValue , boolean isLowerBound ) {
1844- isLowerBound = true and boundValue = exprMinVal ( expr .getFullyConverted ( ) )
1829+ private float getExprTypeBounds ( Expr expr , boolean isLowerBound ) {
1830+ isLowerBound = true and result = exprMinVal ( expr .getFullyConverted ( ) )
18451831 or
1846- isLowerBound = false and boundValue = exprMaxVal ( expr .getFullyConverted ( ) )
1832+ isLowerBound = false and result = exprMaxVal ( expr .getFullyConverted ( ) )
18471833}
18481834
18491835/**
0 commit comments