@@ -138,9 +138,9 @@ class GuardCondition extends Expr {
138138 cached
139139 predicate ensuresEq ( Expr left , Expr right , int k , BasicBlock block , boolean areEqual ) { none ( ) }
140140
141- /** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `testIsTrue `. */
141+ /** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `value `. */
142142 cached
143- predicate comparesEq ( Expr e , int k , boolean areEqual , boolean testIsTrue ) { none ( ) }
143+ predicate comparesEq ( Expr e , int k , boolean areEqual , AbstractValue value ) { none ( ) }
144144
145145 /**
146146 * Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
@@ -196,17 +196,18 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
196196 )
197197 }
198198
199- override predicate comparesEq ( Expr e , int k , boolean areEqual , boolean testIsTrue ) {
200- exists ( boolean partIsTrue , GuardCondition part |
201- this .( BinaryLogicalOperation ) .impliesValue ( part , partIsTrue , testIsTrue )
199+ override predicate comparesEq ( Expr e , int k , boolean areEqual , AbstractValue value ) {
200+ exists ( BooleanValue partValue , GuardCondition part |
201+ this .( BinaryLogicalOperation )
202+ .impliesValue ( part , partValue .getValue ( ) , value .( BooleanValue ) .getValue ( ) )
202203 |
203- part .comparesEq ( e , k , areEqual , partIsTrue )
204+ part .comparesEq ( e , k , areEqual , partValue )
204205 )
205206 }
206207
207208 override predicate ensuresEq ( Expr e , int k , BasicBlock block , boolean areEqual ) {
208- exists ( boolean testIsTrue |
209- this .comparesEq ( e , k , areEqual , testIsTrue ) and this .controls ( block , testIsTrue )
209+ exists ( AbstractValue value |
210+ this .comparesEq ( e , k , areEqual , value ) and this .valueControls ( block , value )
210211 )
211212 }
212213}
@@ -270,18 +271,18 @@ private class GuardConditionFromIR extends GuardCondition {
270271 )
271272 }
272273
273- override predicate comparesEq ( Expr e , int k , boolean areEqual , boolean testIsTrue ) {
274+ override predicate comparesEq ( Expr e , int k , boolean areEqual , AbstractValue value ) {
274275 exists ( Instruction i |
275276 i .getUnconvertedResultExpression ( ) = e and
276- ir .comparesEq ( i .getAUse ( ) , k , areEqual , testIsTrue )
277+ ir .comparesEq ( i .getAUse ( ) , k , areEqual , value )
277278 )
278279 }
279280
280281 override predicate ensuresEq ( Expr e , int k , BasicBlock block , boolean areEqual ) {
281- exists ( Instruction i , boolean testIsTrue |
282+ exists ( Instruction i , AbstractValue value |
282283 i .getUnconvertedResultExpression ( ) = e and
283- ir .comparesEq ( i .getAUse ( ) , k , areEqual , testIsTrue ) and
284- this .controls ( block , testIsTrue )
284+ ir .comparesEq ( i .getAUse ( ) , k , areEqual , value ) and
285+ this .valueControls ( block , value )
285286 )
286287 }
287288
@@ -492,19 +493,10 @@ class IRGuardCondition extends Instruction {
492493 )
493494 }
494495
495- /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `testIsTrue `. */
496+ /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value `. */
496497 cached
497- predicate comparesEq ( Operand op , int k , boolean areEqual , boolean testIsTrue ) {
498- exists ( MatchValue mv |
499- compares_eq ( this , op , k , areEqual , mv ) and
500- // A match value cannot be dualized, so `testIsTrue` is always true
501- testIsTrue = true
502- )
503- or
504- exists ( BooleanValue bv |
505- compares_eq ( this , op , k , areEqual , bv ) and
506- bv .getValue ( ) = testIsTrue
507- )
498+ predicate comparesEq ( Operand op , int k , boolean areEqual , AbstractValue value ) {
499+ compares_eq ( this , op , k , areEqual , value )
508500 }
509501
510502 /**
0 commit comments