@@ -452,6 +452,21 @@ class IRGuardCondition extends Instruction {
452452 )
453453 }
454454
455+ /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
456+ cached
457+ predicate comparesEq ( Operand op , int k , boolean areEqual , boolean testIsTrue ) {
458+ exists ( MatchValue mv |
459+ compares_eq ( this , op , k , areEqual , mv ) and
460+ // A match value cannot be dualized, so `testIsTrue` is always true
461+ testIsTrue = true
462+ )
463+ or
464+ exists ( BooleanValue bv |
465+ compares_eq ( this , op , k , areEqual , bv ) and
466+ bv .getValue ( ) = testIsTrue
467+ )
468+ }
469+
455470 /**
456471 * Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
457472 * If `areEqual = false` then this implies `left != right + k`.
@@ -463,6 +478,17 @@ class IRGuardCondition extends Instruction {
463478 )
464479 }
465480
481+ /**
482+ * Holds if (determined by this guard) `op == k` must be `areEqual` in `block`.
483+ * If `areEqual = false` then this implies `op != k`.
484+ */
485+ cached
486+ predicate ensuresEq ( Operand op , int k , IRBlock block , boolean areEqual ) {
487+ exists ( AbstractValue value |
488+ compares_eq ( this , op , k , areEqual , value ) and this .valueControls ( block , value )
489+ )
490+ }
491+
466492 /**
467493 * Holds if (determined by this guard) `left == right + k` must be `areEqual` on the edge from
468494 * `pred` to `succ`. If `areEqual = false` then this implies `left != right + k`.
@@ -477,6 +503,18 @@ class IRGuardCondition extends Instruction {
477503 )
478504 }
479505
506+ /**
507+ * Holds if (determined by this guard) `op == k` must be `areEqual` on the edge from
508+ * `pred` to `succ`. If `areEqual = false` then this implies `op != k`.
509+ */
510+ cached
511+ predicate ensuresEqEdge ( Operand op , int k , IRBlock pred , IRBlock succ , boolean areEqual ) {
512+ exists ( AbstractValue value |
513+ compares_eq ( this , op , k , areEqual , value ) and
514+ this .valueControlsEdge ( pred , succ , value )
515+ )
516+ }
517+
480518 /**
481519 * Holds if this condition controls `block`, meaning that `block` is only
482520 * entered if the value of this condition is `v`. This helper
@@ -598,6 +636,33 @@ private predicate compares_eq(
598636 )
599637}
600638
639+ /** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */
640+ private predicate compares_eq (
641+ Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
642+ ) {
643+ /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
644+ exists ( AbstractValue v | simple_comparison_eq ( test , op , k , v ) |
645+ areEqual = true and value = v
646+ or
647+ areEqual = false and value = v .getDualValue ( )
648+ )
649+ or
650+ complex_eq ( test , op , k , areEqual , value )
651+ or
652+ /* (x is true => (op == k)) => (!x is false => (op == k)) */
653+ exists ( AbstractValue dual | value = dual .getDualValue ( ) |
654+ compares_eq ( test .( LogicalNotInstruction ) .getUnary ( ) , op , k , areEqual , dual )
655+ )
656+ or
657+ // ((test is `areEqual` => op == const + k2) and const == `k1`) =>
658+ // test is `areEqual` => op == k1 + k2
659+ exists ( int k1 , int k2 , ConstantInstruction const |
660+ compares_eq ( test , op , const .getAUse ( ) , k2 , areEqual , value ) and
661+ int_value ( const ) = k1 and
662+ k = k1 + k2
663+ )
664+ }
665+
601666/** Rearrange various simple comparisons into `left == right + k` form. */
602667private predicate simple_comparison_eq (
603668 CompareInstruction cmp , Operand left , Operand right , int k , AbstractValue value
@@ -615,6 +680,15 @@ private predicate simple_comparison_eq(
615680 value .( BooleanValue ) .getValue ( ) = false
616681}
617682
683+ /** Rearrange various simple comparisons into `op == k` form. */
684+ private predicate simple_comparison_eq ( Instruction test , Operand op , int k , AbstractValue value ) {
685+ exists ( SwitchInstruction switch |
686+ test = switch .getExpression ( ) and
687+ op .getDef ( ) = test and
688+ value .( MatchValue ) .getCase ( ) .getValue ( ) .toInt ( ) = k
689+ )
690+ }
691+
618692private predicate complex_eq (
619693 CompareInstruction cmp , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
620694) {
@@ -623,6 +697,14 @@ private predicate complex_eq(
623697 add_eq ( cmp , left , right , k , areEqual , value )
624698}
625699
700+ private predicate complex_eq (
701+ Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
702+ ) {
703+ sub_eq ( test , op , k , areEqual , value )
704+ or
705+ add_eq ( test , op , k , areEqual , value )
706+ }
707+
626708/*
627709 * Simplification of inequality expressions
628710 * Simplify conditions in the source to the canonical form l < r + k.
@@ -802,6 +884,23 @@ private predicate sub_eq(
802884 )
803885}
804886
887+ // op - x == c => op == (c+x)
888+ private predicate sub_eq ( Instruction test , Operand op , int k , boolean areEqual , AbstractValue value ) {
889+ exists ( SubInstruction sub , int c , int x |
890+ compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
891+ op = sub .getLeftOperand ( ) and
892+ x = int_value ( sub .getRight ( ) ) and
893+ k = c + x
894+ )
895+ or
896+ exists ( PointerSubInstruction sub , int c , int x |
897+ compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
898+ op = sub .getLeftOperand ( ) and
899+ x = int_value ( sub .getRight ( ) ) and
900+ k = c + x
901+ )
902+ }
903+
805904// left + x == right + c => left == right + (c-x)
806905// left == (right + x) + c => left == right + (c+x)
807906private predicate add_eq (
@@ -848,5 +947,30 @@ private predicate add_eq(
848947 )
849948}
850949
950+ // left + x == right + c => left == right + (c-x)
951+ private predicate add_eq (
952+ Instruction test , Operand left , int k , boolean areEqual , AbstractValue value
953+ ) {
954+ exists ( AddInstruction lhs , int c , int x |
955+ compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
956+ (
957+ left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
958+ or
959+ left = lhs .getRightOperand ( ) and x = int_value ( lhs .getLeft ( ) )
960+ ) and
961+ k = c - x
962+ )
963+ or
964+ exists ( PointerAddInstruction lhs , int c , int x |
965+ compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
966+ (
967+ left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
968+ or
969+ left = lhs .getRightOperand ( ) and x = int_value ( lhs .getLeft ( ) )
970+ ) and
971+ k = c - x
972+ )
973+ }
974+
851975/** The int value of integer constant expression. */
852976private int int_value ( Instruction i ) { result = i .( IntegerConstantInstruction ) .getValue ( ) .toInt ( ) }
0 commit comments