@@ -565,7 +565,7 @@ class IRGuardCondition extends Instruction {
565565 /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */
566566 cached
567567 predicate comparesEq ( Operand op , int k , boolean areEqual , AbstractValue value ) {
568- unary_compares_eq ( this , op , k , areEqual , value )
568+ unary_compares_eq ( this , op , k , areEqual , false , value )
569569 }
570570
571571 /**
@@ -586,7 +586,7 @@ class IRGuardCondition extends Instruction {
586586 cached
587587 predicate ensuresEq ( Operand op , int k , IRBlock block , boolean areEqual ) {
588588 exists ( AbstractValue value |
589- unary_compares_eq ( this , op , k , areEqual , value ) and this .valueControls ( block , value )
589+ unary_compares_eq ( this , op , k , areEqual , false , value ) and this .valueControls ( block , value )
590590 )
591591 }
592592
@@ -611,7 +611,7 @@ class IRGuardCondition extends Instruction {
611611 cached
612612 predicate ensuresEqEdge ( Operand op , int k , IRBlock pred , IRBlock succ , boolean areEqual ) {
613613 exists ( AbstractValue value |
614- unary_compares_eq ( this , op , k , areEqual , value ) and
614+ unary_compares_eq ( this , op , k , areEqual , false , value ) and
615615 this .valueControlsEdge ( pred , succ , value )
616616 )
617617 }
@@ -737,26 +737,66 @@ private predicate compares_eq(
737737 )
738738}
739739
740- /** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */
740+ /**
741+ * Holds if `op == k` is `areEqual` given that `test` is equal to `value`.
742+ *
743+ * Many internal predicates in this file have a `inNonZeroCase` column.
744+ * Ideally, the `k` column would be a type such as `Option<int>::Option`, to
745+ * represent whether we have a concrete value `k` such that `op == k`, or whether
746+ * we only know that `op != 0`.
747+ * However, cannot instantiate `Option` with an infinite type. Thus the boolean
748+ * `inNonZeroCase` is used to distinquish the `Some` (where we have a concrete
749+ * value `k`) and `None` cases (where we only know that `op != 0`).
750+ *
751+ * Thus, if `inNonZeroCase = true` then `op != 0` and the value of `k` is
752+ * meaningless.
753+ *
754+ * To see why `inNonZeroCase` is needed consider the following C program:
755+ * ```c
756+ * char* p = ...;
757+ * if(p) {
758+ * use(p);
759+ * }
760+ * ```
761+ * in C++ there would be an int-to-bool conversion on `p`. However, since C
762+ * does not have booleans there is no conversion. We want to be able to
763+ * conclude that `p` is non-zero in the true branch, so we need to give `k`
764+ * some value. However, simply setting `k = 1` would make the rest of the
765+ * analysis think that `k == 1` holds inside the branch. So we distinquish
766+ * between the above case and
767+ * ```c
768+ * if(p == 1) {
769+ * use(p)
770+ * }
771+ * ```
772+ * by setting `inNonZeroCase` to `true` in the former case, but not in the
773+ * latter.
774+ */
741775private predicate unary_compares_eq (
742- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
776+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
743777) {
744778 /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
745- exists ( AbstractValue v | unary_simple_comparison_eq ( test , op , k , v ) |
779+ exists ( AbstractValue v | unary_simple_comparison_eq ( test , op , k , inNonZeroCase , v ) |
746780 areEqual = true and value = v
747781 or
748782 areEqual = false and value = v .getDualValue ( )
749783 )
750784 or
751- unary_complex_eq ( test , op , k , areEqual , value )
785+ unary_complex_eq ( test , op , k , areEqual , inNonZeroCase , value )
752786 or
753787 /* (x is true => (op == k)) => (!x is false => (op == k)) */
754- exists ( AbstractValue dual | value = dual .getDualValue ( ) |
755- unary_compares_eq ( test .( LogicalNotInstruction ) .getUnary ( ) , op , k , areEqual , dual )
788+ exists ( AbstractValue dual , boolean inNonZeroCase0 |
789+ value = dual .getDualValue ( ) and
790+ unary_compares_eq ( test .( LogicalNotInstruction ) .getUnary ( ) , op , k , inNonZeroCase0 , areEqual , dual )
791+ |
792+ k = 0 and inNonZeroCase = inNonZeroCase0
793+ or
794+ k != 0 and inNonZeroCase = true
756795 )
757796 or
758797 // ((test is `areEqual` => op == const + k2) and const == `k1`) =>
759798 // test is `areEqual` => op == k1 + k2
799+ inNonZeroCase = false and
760800 exists ( int k1 , int k2 , ConstantInstruction const |
761801 compares_eq ( test , op , const .getAUse ( ) , k2 , areEqual , value ) and
762802 int_value ( const ) = k1 and
@@ -781,37 +821,53 @@ private predicate simple_comparison_eq(
781821 value .( BooleanValue ) .getValue ( ) = false
782822}
783823
784- /** Rearrange various simple comparisons into `op == k` form. */
824+ /**
825+ * Holds if `test` is an instruction that is part of test that eventually is
826+ * used in a conditional branch.
827+ */
828+ private predicate relevantUnaryComparison ( Instruction test ) {
829+ not test instanceof CompareInstruction and
830+ exists ( IRType type , ConditionalBranchInstruction branch |
831+ type instanceof IRAddressType or type instanceof IRIntegerType
832+ |
833+ type = test .getResultIRType ( ) and
834+ branch .getCondition ( ) = test
835+ )
836+ or
837+ exists ( LogicalNotInstruction logicalNot |
838+ relevantUnaryComparison ( logicalNot ) and
839+ test = logicalNot .getUnary ( )
840+ )
841+ }
842+
843+ /**
844+ * Rearrange various simple comparisons into `op == k` form.
845+ */
785846private predicate unary_simple_comparison_eq (
786- Instruction test , Operand op , int k , AbstractValue value
847+ Instruction test , Operand op , int k , boolean inNonZeroCase , AbstractValue value
787848) {
788849 exists ( SwitchInstruction switch , CaseEdge case |
789850 test = switch .getExpression ( ) and
790851 op .getDef ( ) = test and
791852 case = value .( MatchValue ) .getCase ( ) and
792853 exists ( switch .getSuccessor ( case ) ) and
793- case .getValue ( ) .toInt ( ) = k
854+ case .getValue ( ) .toInt ( ) = k and
855+ inNonZeroCase = false
794856 )
795857 or
796858 // There's no implicit CompareInstruction in files compiled as C since C
797859 // doesn't have implicit boolean conversions. So instead we check whether
798860 // there's a branch on a value of pointer or integer type.
799- exists ( ConditionalBranchInstruction branch , IRType type |
800- not test instanceof CompareInstruction and
801- type = test .getResultIRType ( ) and
802- ( type instanceof IRAddressType or type instanceof IRIntegerType ) and
803- test = branch .getCondition ( ) and
804- op .getDef ( ) = test
805- |
806- // We'd like to also include a case such as:
807- // ```
808- // k = 1 and
809- // value.(BooleanValue).getValue() = true
810- // ```
811- // but all we know is that the value is non-zero in the true branch.
812- // So we can only conclude something in the false branch.
861+ relevantUnaryComparison ( test ) and
862+ op .getDef ( ) = test and
863+ (
864+ k = 1 and
865+ value .( BooleanValue ) .getValue ( ) = true and
866+ inNonZeroCase = true
867+ or
813868 k = 0 and
814- value .( BooleanValue ) .getValue ( ) = false
869+ value .( BooleanValue ) .getValue ( ) = false and
870+ inNonZeroCase = false
815871 )
816872}
817873
@@ -824,11 +880,11 @@ private predicate complex_eq(
824880}
825881
826882private predicate unary_complex_eq (
827- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
883+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
828884) {
829- unary_sub_eq ( test , op , k , areEqual , value )
885+ unary_sub_eq ( test , op , k , areEqual , inNonZeroCase , value )
830886 or
831- unary_add_eq ( test , op , k , areEqual , value )
887+ unary_add_eq ( test , op , k , areEqual , inNonZeroCase , value )
832888}
833889
834890/*
@@ -1093,17 +1149,19 @@ private predicate sub_eq(
10931149
10941150// op - x == c => op == (c+x)
10951151private predicate unary_sub_eq (
1096- Instruction test , Operand op , int k , boolean areEqual , AbstractValue value
1152+ Instruction test , Operand op , int k , boolean areEqual , boolean inNonZeroCase , AbstractValue value
10971153) {
1154+ inNonZeroCase = false and
10981155 exists ( SubInstruction sub , int c , int x |
1099- unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1156+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
11001157 op = sub .getLeftOperand ( ) and
11011158 x = int_value ( sub .getRight ( ) ) and
11021159 k = c + x
11031160 )
11041161 or
1162+ inNonZeroCase = false and
11051163 exists ( PointerSubInstruction sub , int c , int x |
1106- unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , value ) and
1164+ unary_compares_eq ( test , sub .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
11071165 op = sub .getLeftOperand ( ) and
11081166 x = int_value ( sub .getRight ( ) ) and
11091167 k = c + x
@@ -1158,11 +1216,12 @@ private predicate add_eq(
11581216
11591217// left + x == right + c => left == right + (c-x)
11601218private predicate unary_add_eq (
1161- Instruction test , Operand left , int k , boolean areEqual ,
1219+ Instruction test , Operand left , int k , boolean areEqual , boolean inNonZeroCase ,
11621220 AbstractValue value
11631221) {
1222+ inNonZeroCase = false and
11641223 exists ( AddInstruction lhs , int c , int x |
1165- unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1224+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
11661225 (
11671226 left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
11681227 or
@@ -1171,9 +1230,9 @@ private predicate unary_add_eq(
11711230 k = c - x
11721231 )
11731232 or
1233+ inNonZeroCase = false and
11741234 exists ( PointerAddInstruction lhs , int c , int x |
1175-
1176- unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , value ) and
1235+ unary_compares_eq ( test , lhs .getAUse ( ) , c , areEqual , inNonZeroCase , value ) and
11771236 (
11781237 left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRight ( ) )
11791238 or
0 commit comments