@@ -452,6 +452,21 @@ class IRGuardCondition extends Instruction {
452
452
)
453
453
}
454
454
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
+
455
470
/**
456
471
* Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
457
472
* If `areEqual = false` then this implies `left != right + k`.
@@ -463,6 +478,17 @@ class IRGuardCondition extends Instruction {
463
478
)
464
479
}
465
480
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
+
466
492
/**
467
493
* Holds if (determined by this guard) `left == right + k` must be `areEqual` on the edge from
468
494
* `pred` to `succ`. If `areEqual = false` then this implies `left != right + k`.
@@ -477,6 +503,18 @@ class IRGuardCondition extends Instruction {
477
503
)
478
504
}
479
505
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
+
480
518
/**
481
519
* Holds if this condition controls `block`, meaning that `block` is only
482
520
* entered if the value of this condition is `v`. This helper
@@ -598,6 +636,33 @@ private predicate compares_eq(
598
636
)
599
637
}
600
638
639
+ /** Holds if `op == k` is `areEqual` given that `test` is `testIsTrue`. */
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
+
601
666
/** Rearrange various simple comparisons into `left == right + k` form. */
602
667
private predicate simple_comparison_eq (
603
668
CompareInstruction cmp , Operand left , Operand right , int k , AbstractValue value
@@ -615,6 +680,15 @@ private predicate simple_comparison_eq(
615
680
value .( BooleanValue ) .getValue ( ) = false
616
681
}
617
682
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
+
618
692
private predicate complex_eq (
619
693
CompareInstruction cmp , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
620
694
) {
@@ -623,6 +697,14 @@ private predicate complex_eq(
623
697
add_eq ( cmp , left , right , k , areEqual , value )
624
698
}
625
699
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
+
626
708
/*
627
709
* Simplification of inequality expressions
628
710
* Simplify conditions in the source to the canonical form l < r + k.
@@ -802,6 +884,23 @@ private predicate sub_eq(
802
884
)
803
885
}
804
886
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
+
805
904
// left + x == right + c => left == right + (c-x)
806
905
// left == (right + x) + c => left == right + (c+x)
807
906
private predicate add_eq (
@@ -848,5 +947,30 @@ private predicate add_eq(
848
947
)
849
948
}
850
949
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
+
851
975
/** The int value of integer constant expression. */
852
976
private int int_value ( Instruction i ) { result = i .( IntegerConstantInstruction ) .getValue ( ) .toInt ( ) }
0 commit comments