Merge pull request github#16533 from MathiasVP/better-negation-guards-in-c

C++: Make `IRGuardCondition` handle `p` in `if(p)` and `if(!p)` better in C programs

Author: MathiasVP

cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll

@@ -565,7 +565,7 @@ class IRGuardCondition extends Instruction {
   /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */
   cached
   predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) {
-    compares_eq(this, op, k, areEqual, value)
+    unary_compares_eq(this, op, k, areEqual, false, value)
   }
 
   /**
@@ -586,7 +586,7 @@ class IRGuardCondition extends Instruction {
   cached
   predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) {
     exists(AbstractValue value |
-      compares_eq(this, op, k, areEqual, value) and this.valueControls(block, value)
+      unary_compares_eq(this, op, k, areEqual, false, value) and this.valueControls(block, value)
     )
   }
 
@@ -611,7 +611,7 @@ class IRGuardCondition extends Instruction {
   cached
   predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) {
     exists(AbstractValue value |
-      compares_eq(this, op, k, areEqual, value) and
+      unary_compares_eq(this, op, k, areEqual, false, value) and
       this.valueControlsEdge(pred, succ, value)
     )
   }
@@ -737,26 +737,66 @@ private predicate compares_eq(
   )
 }
 
-/** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */
-private predicate compares_eq(
-  Instruction test, Operand op, int k, boolean areEqual, AbstractValue value
+/**
+ * Holds if `op == k` is `areEqual` given that `test` is equal to `value`.
+ *
+ * Many internal predicates in this file have a `inNonZeroCase` column.
+ * Ideally, the `k` column would be a type such as `Option<int>::Option`, to
+ * represent whether we have a concrete value `k` such that `op == k`, or whether
+ * we only know that `op != 0`.
+ * However, cannot instantiate `Option` with an infinite type. Thus the boolean
+ * `inNonZeroCase` is used to distinquish the `Some` (where we have a concrete
+ * value `k`) and `None` cases (where we only know that `op != 0`).
+ *
+ * Thus, if `inNonZeroCase = true` then `op != 0` and the value of `k` is
+ * meaningless.
+ *
+ * To see why `inNonZeroCase` is needed consider the following C program:
+ * ```c
+ * char* p = ...;
+ * if(p) {
+ *   use(p);
+ * }
+ * ```
+ * in C++ there would be an int-to-bool conversion on `p`. However, since C
+ * does not have booleans there is no conversion. We want to be able to
+ * conclude that `p` is non-zero in the true branch, so we need to give `k`
+ * some value. However, simply setting `k = 1` would make the rest of the
+ * analysis think that `k == 1` holds inside the branch. So we distinquish
+ * between the above case and
+ * ```c
+ * if(p == 1) {
+ *   use(p)
+ * }
+ * ```
+ * by setting `inNonZeroCase` to `true` in the former case, but not in the
+ * latter.
+ */
+private predicate unary_compares_eq(
+  Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
 ) {
   /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
-  exists(AbstractValue v | simple_comparison_eq(test, op, k, v) |
+  exists(AbstractValue v | unary_simple_comparison_eq(test, op, k, inNonZeroCase, v) |
     areEqual = true and value = v
     or
     areEqual = false and value = v.getDualValue()
   )
   or
-  complex_eq(test, op, k, areEqual, value)
+  unary_complex_eq(test, op, k, areEqual, inNonZeroCase, value)
   or
   /* (x is true => (op == k)) => (!x is false => (op == k)) */
-  exists(AbstractValue dual | value = dual.getDualValue() |
-    compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, areEqual, dual)
+  exists(AbstractValue dual, boolean inNonZeroCase0 |
+    value = dual.getDualValue() and
+    unary_compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, inNonZeroCase0, areEqual, dual)
+  |
+    k = 0 and inNonZeroCase = inNonZeroCase0
+    or
+    k != 0 and inNonZeroCase = true
   )
   or
   // ((test is `areEqual` => op == const + k2) and const == `k1`) =>
   // test is `areEqual` => op == k1 + k2
+  inNonZeroCase = false and
   exists(int k1, int k2, ConstantInstruction const |
     compares_eq(test, op, const.getAUse(), k2, areEqual, value) and
     int_value(const) = k1 and
@@ -781,35 +821,53 @@ private predicate simple_comparison_eq(
   value.(BooleanValue).getValue() = false
 }
 
-/** Rearrange various simple comparisons into `op == k` form. */
-private predicate simple_comparison_eq(Instruction test, Operand op, int k, AbstractValue value) {
+/**
+ * Holds if `test` is an instruction that is part of test that eventually is
+ * used in a conditional branch.
+ */
+private predicate relevantUnaryComparison(Instruction test) {
+  not test instanceof CompareInstruction and
+  exists(IRType type, ConditionalBranchInstruction branch |
+    type instanceof IRAddressType or type instanceof IRIntegerType
+  |
+    type = test.getResultIRType() and
+    branch.getCondition() = test
+  )
+  or
+  exists(LogicalNotInstruction logicalNot |
+    relevantUnaryComparison(logicalNot) and
+    test = logicalNot.getUnary()
+  )
+}
+
+/**
+ * Rearrange various simple comparisons into `op == k` form.
+ */
+private predicate unary_simple_comparison_eq(
+  Instruction test, Operand op, int k, boolean inNonZeroCase, AbstractValue value
+) {
   exists(SwitchInstruction switch, CaseEdge case |
     test = switch.getExpression() and
     op.getDef() = test and
     case = value.(MatchValue).getCase() and
     exists(switch.getSuccessor(case)) and
-    case.getValue().toInt() = k
+    case.getValue().toInt() = k and
+    inNonZeroCase = false
   )
   or
   // There's no implicit CompareInstruction in files compiled as C since C
   // doesn't have implicit boolean conversions. So instead we check whether
   // there's a branch on a value of pointer or integer type.
-  exists(ConditionalBranchInstruction branch, IRType type |
-    not test instanceof CompareInstruction and
-    type = test.getResultIRType() and
-    (type instanceof IRAddressType or type instanceof IRIntegerType) and
-    test = branch.getCondition() and
-    op.getDef() = test
-  |
-    // We'd like to also include a case such as:
-    // ```
-    // k = 1 and
-    // value.(BooleanValue).getValue() = true
-    // ```
-    // but all we know is that the value is non-zero in the true branch.
-    // So we can only conclude something in the false branch.
+  relevantUnaryComparison(test) and
+  op.getDef() = test and
+  (
+    k = 1 and
+    value.(BooleanValue).getValue() = true and
+    inNonZeroCase = true
+    or
     k = 0 and
-    value.(BooleanValue).getValue() = false
+    value.(BooleanValue).getValue() = false and
+    inNonZeroCase = false
   )
 }
 
@@ -821,12 +879,12 @@ private predicate complex_eq(
   add_eq(cmp, left, right, k, areEqual, value)
 }
 
-private predicate complex_eq(
-  Instruction test, Operand op, int k, boolean areEqual, AbstractValue value
+private predicate unary_complex_eq(
+  Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
 ) {
-  sub_eq(test, op, k, areEqual, value)
+  unary_sub_eq(test, op, k, areEqual, inNonZeroCase, value)
   or
-  add_eq(test, op, k, areEqual, value)
+  unary_add_eq(test, op, k, areEqual, inNonZeroCase, value)
 }
 
 /*
@@ -1090,16 +1148,20 @@ private predicate sub_eq(
 }
 
 // op - x == c => op == (c+x)
-private predicate sub_eq(Instruction test, Operand op, int k, boolean areEqual, AbstractValue value) {
+private predicate unary_sub_eq(
+  Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
+) {
+  inNonZeroCase = false and
   exists(SubInstruction sub, int c, int x |
-    compares_eq(test, sub.getAUse(), c, areEqual, value) and
+    unary_compares_eq(test, sub.getAUse(), c, areEqual, inNonZeroCase, value) and
     op = sub.getLeftOperand() and
     x = int_value(sub.getRight()) and
     k = c + x
   )
   or
+  inNonZeroCase = false and
   exists(PointerSubInstruction sub, int c, int x |
-    compares_eq(test, sub.getAUse(), c, areEqual, value) and
+    unary_compares_eq(test, sub.getAUse(), c, areEqual, inNonZeroCase, value) and
     op = sub.getLeftOperand() and
     x = int_value(sub.getRight()) and
     k = c + x
@@ -1153,11 +1215,13 @@ private predicate add_eq(
 }
 
 // left + x == right + c => left == right + (c-x)
-private predicate add_eq(
-  Instruction test, Operand left, int k, boolean areEqual, AbstractValue value
+private predicate unary_add_eq(
+  Instruction test, Operand left, int k, boolean areEqual, boolean inNonZeroCase,
+  AbstractValue value
 ) {
+  inNonZeroCase = false and
   exists(AddInstruction lhs, int c, int x |
-    compares_eq(test, lhs.getAUse(), c, areEqual, value) and
+    unary_compares_eq(test, lhs.getAUse(), c, areEqual, inNonZeroCase, value) and
     (
       left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
       or
@@ -1166,8 +1230,9 @@ private predicate add_eq(
     k = c - x
   )
   or
+  inNonZeroCase = false and
   exists(PointerAddInstruction lhs, int c, int x |
-    compares_eq(test, lhs.getAUse(), c, areEqual, value) and
+    unary_compares_eq(test, lhs.getAUse(), c, areEqual, inNonZeroCase, value) and
     (
       left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
       or

cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected

@@ -160,6 +160,9 @@ astGuardsCompare
 | 137 | 0 == 0 when 0 is false |
 | 146 | ! ... != 0 when ! ... is true |
 | 146 | ! ... == 0 when ! ... is false |
+| 146 | x != 0 when ! ... is false |
+| 146 | x != 0 when x is true |
+| 146 | x == 0 when x is false |
 | 152 | x != 0 when ... && ... is true |
 | 152 | x != 0 when x is true |
 | 152 | x == 0 when x is false |
@@ -518,6 +521,7 @@ astGuardsEnsure_const
 | test.c:131:7:131:7 | b | test.c:131:7:131:7 | b | != | 0 | 131 | 132 |
 | test.c:137:7:137:7 | 0 | test.c:137:7:137:7 | 0 | == | 0 | 142 | 136 |
 | test.c:146:7:146:8 | ! ... | test.c:146:7:146:8 | ! ... | != | 0 | 146 | 147 |
+| test.c:146:8:146:8 | x | test.c:146:8:146:8 | x | == | 0 | 146 | 147 |
 | test.c:152:10:152:10 | x | test.c:152:10:152:10 | x | != | 0 | 151 | 152 |
 | test.c:152:10:152:10 | x | test.c:152:10:152:10 | x | != | 0 | 152 | 152 |
 | test.c:152:10:152:15 | ... && ... | test.c:152:10:152:10 | x | != | 0 | 151 | 152 |
@@ -689,6 +693,9 @@ irGuardsCompare
 | 137 | 0 == 0 when Constant: 0 is false |
 | 146 | ! ... != 0 when LogicalNot: ! ... is true |
 | 146 | ! ... == 0 when LogicalNot: ! ... is false |
+| 146 | x != 0 when Load: x is true |
+| 146 | x != 0 when LogicalNot: ! ... is false |
+| 146 | x == 0 when Load: x is false |
 | 152 | x != 0 when Load: x is true |
 | 152 | x == 0 when Load: x is false |
 | 152 | y != 0 when Load: y is true |
@@ -1063,6 +1070,7 @@ irGuardsEnsure_const
 | test.c:131:7:131:7 | Load: b | test.c:131:7:131:7 | Load: b | != | 0 | 132 | 132 |
 | test.c:137:7:137:7 | Constant: 0 | test.c:137:7:137:7 | Constant: 0 | == | 0 | 142 | 142 |
 | test.c:146:7:146:8 | LogicalNot: ! ... | test.c:146:7:146:8 | LogicalNot: ! ... | != | 0 | 147 | 147 |
+| test.c:146:8:146:8 | Load: x | test.c:146:8:146:8 | Load: x | == | 0 | 147 | 147 |
 | test.c:152:10:152:10 | Load: x | test.c:152:10:152:10 | Load: x | != | 0 | 152 | 152 |
 | test.c:152:15:152:15 | Load: y | test.c:152:15:152:15 | Load: y | != | 0 | 152 | 152 |
 | test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:15 | Call: call to foo | != | 0 | 175 | 175 |

cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected

@@ -161,11 +161,20 @@
 | 137 | 0 == 0 when 0 is false |
 | 146 | ! ... != 0 when ! ... is true |
 | 146 | ! ... == 0 when ! ... is false |
+| 146 | x != 0 when ! ... is false |
+| 146 | x != 0 when x is true |
+| 146 | x == 0 when x is false |
 | 152 | p != 0 when p is true |
 | 152 | p == 0 when p is false |
 | 158 | ! ... != 0 when ! ... is true |
 | 158 | ! ... == 0 when ! ... is false |
+| 158 | p != 0 when ! ... is false |
+| 158 | p != 0 when p is true |
+| 158 | p == 0 when p is false |
 | 164 | s != 0 when s is true |
 | 164 | s == 0 when s is false |
 | 170 | ! ... != 0 when ! ... is true |
 | 170 | ! ... == 0 when ! ... is false |
+| 170 | s != 0 when ! ... is false |
+| 170 | s != 0 when s is true |
+| 170 | s == 0 when s is false |

cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected

@@ -245,10 +245,13 @@ unary
 | test.c:131:7:131:7 | b | test.c:131:7:131:7 | b | != | 0 | 131 | 132 |
 | test.c:137:7:137:7 | 0 | test.c:137:7:137:7 | 0 | == | 0 | 142 | 136 |
 | test.c:146:7:146:8 | ! ... | test.c:146:7:146:8 | ! ... | != | 0 | 146 | 147 |
+| test.c:146:8:146:8 | x | test.c:146:8:146:8 | x | == | 0 | 146 | 147 |
 | test.c:152:8:152:8 | p | test.c:152:8:152:8 | p | != | 0 | 152 | 154 |
 | test.c:158:8:158:9 | ! ... | test.c:158:8:158:9 | ! ... | != | 0 | 158 | 160 |
+| test.c:158:9:158:9 | p | test.c:158:9:158:9 | p | == | 0 | 158 | 160 |
 | test.c:164:8:164:8 | s | test.c:164:8:164:8 | s | != | 0 | 164 | 166 |
 | test.c:170:8:170:9 | ! ... | test.c:170:8:170:9 | ! ... | != | 0 | 170 | 172 |
+| test.c:170:9:170:9 | s | test.c:170:9:170:9 | s | == | 0 | 170 | 172 |
 | test.cpp:18:8:18:10 | call to get | test.cpp:18:8:18:10 | call to get | != | 0 | 19 | 19 |
 | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 30 | 30 |
 | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 34 | 34 |