@@ -1770,22 +1770,10 @@ private predicate boundFromGuard(
17701770) {
17711771 exists ( float p , float q , float r , boolean isLB |
17721772 linearBoundFromGuard ( guard , v , p , q , r , isLB , strictness , branch ) and
1773- boundValue = ( r - q ) / p
1774- |
1773+ boundValue = ( r - q ) / p and
17751774 // If the multiplier is negative then the direction of the comparison
17761775 // needs to be flipped.
1777- p > 0 and isLowerBound = isLB
1778- or
1779- p < 0 and isLowerBound = isLB .booleanNot ( )
1780- )
1781- or
1782- // When `!e` is true, we know that `0 <= e <= 0`
1783- exists ( float p , float q , Expr e |
1784- linearAccess ( e , v , p , q ) and
1785- eqZeroWithNegate ( guard , e , true , branch ) and
1786- boundValue = ( 0.0 - q ) / p and
1787- isLowerBound = [ false , true ] and
1788- strictness = Nonstrict ( )
1776+ if p < 0 then isLowerBound = isLB .booleanNot ( ) else isLowerBound = isLB
17891777 )
17901778}
17911779
@@ -1795,54 +1783,57 @@ private predicate boundFromGuard(
17951783 * lower or upper bound for `v`.
17961784 */
17971785private predicate linearBoundFromGuard (
1798- ComparisonOperation guard , VariableAccess v , float p , float q , float boundValue ,
1786+ Expr guard , VariableAccess v , float p , float q , float r ,
17991787 boolean isLowerBound , // Is this a lower or an upper bound?
18001788 RelationStrictness strictness , boolean branch // Which control-flow branch is this bound valid on?
18011789) {
1802- // For the comparison x < RHS, we create two bounds:
1803- //
1804- // 1. x < upperbound(RHS)
1805- // 2. x >= typeLowerBound(RHS.getUnspecifiedType())
1806- //
1807- exists ( Expr lhs , Expr rhs , RelationDirection dir , RelationStrictness st |
1808- linearAccess ( lhs , v , p , q ) and
1809- relOpWithSwapAndNegate ( guard , lhs , rhs , dir , st , branch )
1810- |
1811- isLowerBound = directionIsGreater ( dir ) and
1812- strictness = st and
1813- getBounds ( rhs , boundValue , isLowerBound )
1790+ exists ( Expr lhs | linearAccess ( lhs , v , p , q ) |
1791+ // For the comparison x < RHS, we create the following bounds:
1792+ // 1. x < upperbound(RHS)
1793+ // 2. x >= typeLowerBound(RHS.getUnspecifiedType())
1794+ exists ( Expr rhs , RelationDirection dir , RelationStrictness st |
1795+ relOpWithSwapAndNegate ( guard , lhs , rhs , dir , st , branch )
1796+ |
1797+ isLowerBound = directionIsGreater ( dir ) and
1798+ strictness = st and
1799+ r = getBounds ( rhs , isLowerBound )
1800+ or
1801+ isLowerBound = directionIsLesser ( dir ) and
1802+ strictness = Nonstrict ( ) and
1803+ r = getExprTypeBounds ( rhs , isLowerBound )
1804+ )
18141805 or
1815- isLowerBound = directionIsLesser ( dir ) and
1816- strictness = Nonstrict ( ) and
1817- exprTypeBounds ( rhs , boundValue , isLowerBound )
1818- )
1819- or
1820- // For x == RHS, we create the following bounds:
1821- //
1822- // 1. x <= upperbound(RHS)
1823- // 2. x >= lowerbound(RHS)
1824- //
1825- exists ( Expr lhs , Expr rhs |
1826- linearAccess ( lhs , v , p , q ) and
1827- eqOpWithSwapAndNegate ( guard , lhs , rhs , true , branch ) and
1828- getBounds ( rhs , boundValue , isLowerBound ) and
1806+ // For x == RHS, we create the following bounds:
1807+ // 1. x <= upperbound(RHS)
1808+ // 2. x >= lowerbound(RHS)
1809+ exists ( Expr rhs |
1810+ eqOpWithSwapAndNegate ( guard , lhs , rhs , true , branch ) and
1811+ r = getBounds ( rhs , isLowerBound ) and
1812+ strictness = Nonstrict ( )
1813+ )
1814+ or
1815+ // When `x` is equal to 0 we create the following bounds:
1816+ // 1. x <= 0
1817+ // 2. x >= 0
1818+ eqZeroWithNegate ( guard , lhs , true , branch ) and
1819+ r = 0.0 and
1820+ isLowerBound = [ false , true ] and
18291821 strictness = Nonstrict ( )
18301822 )
1831- // x != RHS and !x are handled elsewhere
18321823}
18331824
1834- /** Utility for `linearBoundFromGuard `. */
1835- private predicate getBounds ( Expr expr , float boundValue , boolean isLowerBound ) {
1836- isLowerBound = true and boundValue = getFullyConvertedLowerBounds ( expr )
1825+ /** Get the fully converted lower or upper bounds of `expr` based on `isLowerBound `. */
1826+ private float getBounds ( Expr expr , boolean isLowerBound ) {
1827+ isLowerBound = true and result = getFullyConvertedLowerBounds ( expr )
18371828 or
1838- isLowerBound = false and boundValue = getFullyConvertedUpperBounds ( expr )
1829+ isLowerBound = false and result = getFullyConvertedUpperBounds ( expr )
18391830}
18401831
18411832/** Utility for `linearBoundFromGuard`. */
1842- private predicate exprTypeBounds ( Expr expr , float boundValue , boolean isLowerBound ) {
1843- isLowerBound = true and boundValue = exprMinVal ( expr .getFullyConverted ( ) )
1833+ private float getExprTypeBounds ( Expr expr , boolean isLowerBound ) {
1834+ isLowerBound = true and result = exprMinVal ( expr .getFullyConverted ( ) )
18441835 or
1845- isLowerBound = false and boundValue = exprMaxVal ( expr .getFullyConverted ( ) )
1836+ isLowerBound = false and result = exprMaxVal ( expr .getFullyConverted ( ) )
18461837}
18471838
18481839/**
0 commit comments