@@ -1418,10 +1418,10 @@ private module Cached {
14181418 */
14191419 cached
14201420 predicate compares_eq (
1421- ValueNumber test , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
1421+ ValueNumber test , Operand left , Operand right , int k , boolean areEqual , GuardValue value
14221422 ) {
14231423 /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
1424- exists ( AbstractValue v | simple_comparison_eq ( test , left , right , k , v ) |
1424+ exists ( GuardValue v | simple_comparison_eq ( test , left , right , k , v ) |
14251425 areEqual = true and value = v
14261426 or
14271427 areEqual = false and value = v .getDualValue ( )
@@ -1436,15 +1436,15 @@ private module Cached {
14361436 complex_eq ( test , left , right , k , areEqual , value )
14371437 or
14381438 /* (x is true => (left == right + k)) => (!x is false => (left == right + k)) */
1439- exists ( AbstractValue dual | value = dual .getDualValue ( ) |
1439+ exists ( GuardValue dual | value = dual .getDualValue ( ) |
14401440 compares_eq ( test .( LogicalNotValueNumber ) .getUnary ( ) , left , right , k , areEqual , dual )
14411441 )
14421442 or
14431443 compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , left , right , k , areEqual , value )
14441444 or
1445- exists ( Operand l , BooleanValue bv |
1445+ exists ( Operand l , GuardValue bv |
14461446 // 1. test = value -> int(l) = 0 is !bv
1447- unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1447+ unary_compares_eq ( test , l , 0 , bv .asBooleanValue ( ) .booleanNot ( ) , value ) and
14481448 // 2. l = bv -> left + right is areEqual
14491449 compares_eq ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , left ,
14501450 right , k , areEqual , bv )
@@ -1461,10 +1461,10 @@ private module Cached {
14611461 */
14621462 cached
14631463 predicate unary_compares_eq (
1464- ValueNumber test , Operand op , int k , boolean areEqual , AbstractValue value
1464+ ValueNumber test , Operand op , int k , boolean areEqual , GuardValue value
14651465 ) {
14661466 /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
1467- exists ( AbstractValue v | unary_simple_comparison_eq ( test , op , k , v ) |
1467+ exists ( GuardValue v | unary_simple_comparison_eq ( test , op , k , v ) |
14681468 areEqual = true and value = v
14691469 or
14701470 areEqual = false and value = v .getDualValue ( )
@@ -1473,7 +1473,7 @@ private module Cached {
14731473 unary_complex_eq ( test , op , k , areEqual , value )
14741474 or
14751475 /* (x is true => (op == k)) => (!x is false => (op == k)) */
1476- exists ( AbstractValue dual |
1476+ exists ( GuardValue dual |
14771477 value = dual .getDualValue ( ) and
14781478 unary_compares_eq ( test .( LogicalNotValueNumber ) .getUnary ( ) , op , k , areEqual , dual )
14791479 )
@@ -1487,18 +1487,18 @@ private module Cached {
14871487 )
14881488 or
14891489 // See argument for why this is correct in compares_eq
1490- exists ( Operand l , BooleanValue bv |
1491- unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1490+ exists ( Operand l , GuardValue bv |
1491+ unary_compares_eq ( test , l , 0 , bv .asBooleanValue ( ) .booleanNot ( ) , value ) and
14921492 unary_compares_eq ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) ,
14931493 op , k , areEqual , bv )
14941494 )
14951495 or
14961496 unary_compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , op , k , areEqual , value )
14971497 or
1498- exists ( BinaryLogicalOperation logical , Expr operand , boolean b |
1498+ exists ( Cpp :: BinaryLogicalOperation logical , Cpp :: Expr operand , boolean b |
14991499 test .getAnInstruction ( ) .getUnconvertedResultExpression ( ) = logical and
15001500 op .getDef ( ) .getUnconvertedResultExpression ( ) = operand and
1501- logical .impliesValue ( operand , b , value .( BooleanValue ) . getValue ( ) )
1501+ logical .impliesValue ( operand , b , value .asBooleanValue ( ) )
15021502 |
15031503 k = 1 and
15041504 areEqual = b
@@ -1510,17 +1510,17 @@ private module Cached {
15101510
15111511 /** Rearrange various simple comparisons into `left == right + k` form. */
15121512 private predicate simple_comparison_eq (
1513- CompareValueNumber cmp , Operand left , Operand right , int k , AbstractValue value
1513+ CompareValueNumber cmp , Operand left , Operand right , int k , GuardValue value
15141514 ) {
15151515 cmp instanceof CompareEQValueNumber and
15161516 cmp .hasOperands ( left , right ) and
15171517 k = 0 and
1518- value .( BooleanValue ) . getValue ( ) = true
1518+ value .asBooleanValue ( ) = true
15191519 or
15201520 cmp instanceof CompareNEValueNumber and
15211521 cmp .hasOperands ( left , right ) and
15221522 k = 0 and
1523- value .( BooleanValue ) . getValue ( ) = false
1523+ value .asBooleanValue ( ) = false
15241524 }
15251525
15261526 /**
@@ -1556,35 +1556,33 @@ private module Cached {
15561556 }
15571557
15581558 /** Rearrange various simple comparisons into `op == k` form. */
1559- private predicate unary_simple_comparison_eq (
1560- ValueNumber test , Operand op , int k , AbstractValue value
1561- ) {
1562- exists ( CaseEdge case , SwitchConditionValueNumber condition |
1559+ private predicate unary_simple_comparison_eq ( ValueNumber test , Operand op , int k , GuardValue value ) {
1560+ exists ( SwitchConditionValueNumber condition , CaseEdge edge |
15631561 condition = test and
15641562 op = condition .getExpressionOperand ( ) and
1565- case = value .( MatchValue ) . getCase ( ) and
1566- exists ( condition . getSuccessor ( case ) ) and
1567- case . getValue ( ) . toInt ( ) = k
1563+ value .asIntValue ( ) = k and
1564+ edge . getValue ( ) . toInt ( ) = k and
1565+ exists ( condition . getSuccessor ( edge ) )
15681566 )
15691567 or
15701568 exists ( Instruction const | int_value ( const ) = k |
1571- value .( BooleanValue ) . getValue ( ) = true and
1569+ value .asBooleanValue ( ) = true and
15721570 test .( CompareEQValueNumber ) .hasOperands ( op , const .getAUse ( ) )
15731571 or
1574- value .( BooleanValue ) . getValue ( ) = false and
1572+ value .asBooleanValue ( ) = false and
15751573 test .( CompareNEValueNumber ) .hasOperands ( op , const .getAUse ( ) )
15761574 )
15771575 or
1578- exists ( BooleanValue bv |
1576+ exists ( GuardValue bv |
15791577 bv = value and
15801578 mayBranchOn ( op .getDef ( ) ) and
15811579 op = test .getAUse ( )
15821580 |
15831581 k = 0 and
1584- bv .getValue ( ) = false
1582+ bv .asBooleanValue ( ) = false
15851583 or
15861584 k = 1 and
1587- bv .getValue ( ) = true
1585+ bv .asBooleanValue ( ) = true
15881586 )
15891587 }
15901588
@@ -1603,15 +1601,15 @@ private module Cached {
16031601 }
16041602
16051603 private predicate complex_eq (
1606- ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
1604+ ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , GuardValue value
16071605 ) {
16081606 sub_eq ( cmp , left , right , k , areEqual , value )
16091607 or
16101608 add_eq ( cmp , left , right , k , areEqual , value )
16111609 }
16121610
16131611 private predicate unary_complex_eq (
1614- ValueNumber test , Operand op , int k , boolean areEqual , AbstractValue value
1612+ ValueNumber test , Operand op , int k , boolean areEqual , GuardValue value
16151613 ) {
16161614 unary_sub_eq ( test , op , k , areEqual , value )
16171615 or
@@ -1626,41 +1624,41 @@ private module Cached {
16261624 /** Holds if `left < right + k` evaluates to `isLt` given that test is `value`. */
16271625 cached
16281626 predicate compares_lt (
1629- ValueNumber test , Operand left , Operand right , int k , boolean isLt , AbstractValue value
1627+ ValueNumber test , Operand left , Operand right , int k , boolean isLt , GuardValue value
16301628 ) {
16311629 /* In the simple case, the test is the comparison, so isLt = testIsTrue */
16321630 simple_comparison_lt ( test , left , right , k ) and
1633- value .( BooleanValue ) . getValue ( ) = isLt
1631+ value .asBooleanValue ( ) = isLt
16341632 or
16351633 complex_lt ( test , left , right , k , isLt , value )
16361634 or
16371635 /* (not (left < right + k)) => (left >= right + k) */
16381636 exists ( boolean isGe | isLt = isGe .booleanNot ( ) | compares_ge ( test , left , right , k , isGe , value ) )
16391637 or
16401638 /* (x is true => (left < right + k)) => (!x is false => (left < right + k)) */
1641- exists ( AbstractValue dual | value = dual .getDualValue ( ) |
1639+ exists ( GuardValue dual | value = dual .getDualValue ( ) |
16421640 compares_lt ( test .( LogicalNotValueNumber ) .getUnary ( ) , left , right , k , isLt , dual )
16431641 )
16441642 or
16451643 compares_lt ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , left , right , k , isLt , value )
16461644 or
16471645 // See argument for why this is correct in compares_eq
1648- exists ( Operand l , BooleanValue bv |
1649- unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1646+ exists ( Operand l , GuardValue bv |
1647+ unary_compares_eq ( test , l , 0 , bv .asBooleanValue ( ) .booleanNot ( ) , value ) and
16501648 compares_lt ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , left ,
16511649 right , k , isLt , bv )
16521650 )
16531651 }
16541652
16551653 /** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
16561654 cached
1657- predicate compares_lt ( ValueNumber test , Operand op , int k , boolean isLt , AbstractValue value ) {
1655+ predicate compares_lt ( ValueNumber test , Operand op , int k , boolean isLt , GuardValue value ) {
16581656 unary_simple_comparison_lt ( test , op , k , isLt , value )
16591657 or
16601658 complex_lt ( test , op , k , isLt , value )
16611659 or
16621660 /* (x is true => (op < k)) => (!x is false => (op < k)) */
1663- exists ( AbstractValue dual | value = dual .getDualValue ( ) |
1661+ exists ( GuardValue dual | value = dual .getDualValue ( ) |
16641662 compares_lt ( test .( LogicalNotValueNumber ) .getUnary ( ) , op , k , isLt , dual )
16651663 )
16661664 or
@@ -1673,16 +1671,16 @@ private module Cached {
16731671 compares_lt ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , op , k , isLt , value )
16741672 or
16751673 // See argument for why this is correct in compares_eq
1676- exists ( Operand l , BooleanValue bv |
1677- unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1674+ exists ( Operand l , GuardValue bv |
1675+ unary_compares_eq ( test , l , 0 , bv .asBooleanValue ( ) .booleanNot ( ) , value ) and
16781676 compares_lt ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , op , k ,
16791677 isLt , bv )
16801678 )
16811679 }
16821680
16831681 /** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
16841682 private predicate compares_ge (
1685- ValueNumber test , Operand left , Operand right , int k , boolean isGe , AbstractValue value
1683+ ValueNumber test , Operand left , Operand right , int k , boolean isGe , GuardValue value
16861684 ) {
16871685 exists ( int onemk | k = 1 - onemk | compares_lt ( test , right , left , onemk , isGe , value ) )
16881686 }
@@ -1708,34 +1706,32 @@ private module Cached {
17081706
17091707 /** Rearrange various simple comparisons into `op < k` form. */
17101708 private predicate unary_simple_comparison_lt (
1711- SwitchConditionValueNumber test , Operand op , int k , boolean isLt , AbstractValue value
1709+ SwitchConditionValueNumber test , Operand op , int k , boolean isLt , GuardValue value
17121710 ) {
1713- exists ( CaseEdge case |
1711+ exists ( string minValue , string maxValue |
17141712 test .getExpressionOperand ( ) = op and
1715- case = value . ( MatchValue ) . getCase ( ) and
1716- exists ( test . getSuccessor ( case ) ) and
1717- case . getMaxValue ( ) > case . getMinValue ( )
1713+ exists ( test . getSuccessor ( EdgeKind :: caseEdge ( minValue , maxValue ) ) ) and
1714+ value . asConstantValue ( ) . isRange ( minValue , maxValue ) and
1715+ minValue < maxValue
17181716 |
17191717 // op <= k => op < k - 1
17201718 isLt = true and
1721- case . getMaxValue ( ) .toInt ( ) = k - 1
1719+ maxValue .toInt ( ) = k - 1
17221720 or
17231721 isLt = false and
1724- case . getMinValue ( ) .toInt ( ) = k
1722+ minValue .toInt ( ) = k
17251723 )
17261724 }
17271725
17281726 private predicate complex_lt (
1729- ValueNumber cmp , Operand left , Operand right , int k , boolean isLt , AbstractValue value
1727+ ValueNumber cmp , Operand left , Operand right , int k , boolean isLt , GuardValue value
17301728 ) {
17311729 sub_lt ( cmp , left , right , k , isLt , value )
17321730 or
17331731 add_lt ( cmp , left , right , k , isLt , value )
17341732 }
17351733
1736- private predicate complex_lt (
1737- ValueNumber test , Operand left , int k , boolean isLt , AbstractValue value
1738- ) {
1734+ private predicate complex_lt ( ValueNumber test , Operand left , int k , boolean isLt , GuardValue value ) {
17391735 sub_lt ( test , left , k , isLt , value )
17401736 or
17411737 add_lt ( test , left , k , isLt , value )
@@ -1744,7 +1740,7 @@ private module Cached {
17441740 // left - x < right + c => left < right + (c+x)
17451741 // left < (right - x) + c => left < right + (c-x)
17461742 private predicate sub_lt (
1747- ValueNumber cmp , Operand left , Operand right , int k , boolean isLt , AbstractValue value
1743+ ValueNumber cmp , Operand left , Operand right , int k , boolean isLt , GuardValue value
17481744 ) {
17491745 exists ( SubInstruction lhs , int c , int x |
17501746 compares_lt ( cmp , lhs .getAUse ( ) , right , c , isLt , value ) and
@@ -1775,7 +1771,7 @@ private module Cached {
17751771 )
17761772 }
17771773
1778- private predicate sub_lt ( ValueNumber test , Operand left , int k , boolean isLt , AbstractValue value ) {
1774+ private predicate sub_lt ( ValueNumber test , Operand left , int k , boolean isLt , GuardValue value ) {
17791775 exists ( SubInstruction lhs , int c , int x |
17801776 compares_lt ( test , lhs .getAUse ( ) , c , isLt , value ) and
17811777 left = lhs .getLeftOperand ( ) and
@@ -1794,7 +1790,7 @@ private module Cached {
17941790 // left + x < right + c => left < right + (c-x)
17951791 // left < (right + x) + c => left < right + (c+x)
17961792 private predicate add_lt (
1797- ValueNumber cmp , Operand left , Operand right , int k , boolean isLt , AbstractValue value
1793+ ValueNumber cmp , Operand left , Operand right , int k , boolean isLt , GuardValue value
17981794 ) {
17991795 exists ( AddInstruction lhs , int c , int x |
18001796 compares_lt ( cmp , lhs .getAUse ( ) , right , c , isLt , value ) and
@@ -1837,7 +1833,7 @@ private module Cached {
18371833 )
18381834 }
18391835
1840- private predicate add_lt ( ValueNumber test , Operand left , int k , boolean isLt , AbstractValue value ) {
1836+ private predicate add_lt ( ValueNumber test , Operand left , int k , boolean isLt , GuardValue value ) {
18411837 exists ( AddInstruction lhs , int c , int x |
18421838 compares_lt ( test , lhs .getAUse ( ) , c , isLt , value ) and
18431839 (
@@ -1862,7 +1858,7 @@ private module Cached {
18621858 // left - x == right + c => left == right + (c+x)
18631859 // left == (right - x) + c => left == right + (c-x)
18641860 private predicate sub_eq (
1865- ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
1861+ ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , GuardValue value
18661862 ) {
18671863 exists ( SubInstruction lhs , int c , int x |
18681864 compares_eq ( cmp , lhs .getAUse ( ) , right , c , areEqual , value ) and
@@ -1895,7 +1891,7 @@ private module Cached {
18951891
18961892 // op - x == c => op == (c+x)
18971893 private predicate unary_sub_eq (
1898- ValueNumber test , Operand op , int k , boolean areEqual , AbstractValue value
1894+ ValueNumber test , Operand op , int k , boolean areEqual , GuardValue value
18991895 ) {
19001896 exists ( SubInstruction sub , int c , int x |
19011897 unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
@@ -1915,7 +1911,7 @@ private module Cached {
19151911 // left + x == right + c => left == right + (c-x)
19161912 // left == (right + x) + c => left == right + (c+x)
19171913 private predicate add_eq (
1918- ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
1914+ ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , GuardValue value
19191915 ) {
19201916 exists ( AddInstruction lhs , int c , int x |
19211917 compares_eq ( cmp , lhs .getAUse ( ) , right , c , areEqual , value ) and
@@ -1960,7 +1956,7 @@ private module Cached {
19601956
19611957 // left + x == right + c => left == right + (c-x)
19621958 private predicate unary_add_eq (
1963- ValueNumber test , Operand left , int k , boolean areEqual , AbstractValue value
1959+ ValueNumber test , Operand left , int k , boolean areEqual , GuardValue value
19641960 ) {
19651961 exists ( AddInstruction lhs , int c , int x |
19661962 unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
@@ -2003,7 +1999,7 @@ private import Cached
20031999 * To find the specific guard that performs the comparison
20042000 * use `IRGuards.comparesLt`.
20052001 */
2006- predicate comparesLt ( Operand left , Operand right , int k , boolean isLt , AbstractValue value ) {
2002+ predicate comparesLt ( Operand left , Operand right , int k , boolean isLt , GuardValue value ) {
20072003 compares_lt ( _, left , right , k , isLt , value )
20082004}
20092005
@@ -2014,6 +2010,6 @@ predicate comparesLt(Operand left, Operand right, int k, boolean isLt, AbstractV
20142010 * To find the specific guard that performs the comparison
20152011 * use `IRGuards.comparesEq`.
20162012 */
2017- predicate comparesEq ( Operand left , Operand right , int k , boolean isLt , AbstractValue value ) {
2013+ predicate comparesEq ( Operand left , Operand right , int k , boolean isLt , GuardValue value ) {
20182014 compares_eq ( _, left , right , k , isLt , value )
20192015}
0 commit comments