C++: Add another inference step.

Author: MathiasVP

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

@@ -966,6 +966,18 @@ private module Cached {
     )
     or
     compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), left, right, k, areEqual, value)
+    or
+    exists(Operand l, BooleanValue bv |
+      // 1. test = value -> int(l) = 0 is !bv
+      unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
+      // 2. l = bv -> left + right is areEqual
+      compares_eq(valueNumberOfOperand(l), left, right, k, areEqual, bv)
+      // We want this to hold:
+      // `test = value -> left + right is areEqual`
+      // Applying 2 we need to show:
+      // `test = value -> l = bv`
+      // And `l = bv` holds by `int(l) = 0 is !bv`
+    )
   }
 
   private predicate isConvertedBool(Instruction instr) {
@@ -1006,19 +1018,10 @@ private module Cached {
       k = k1 + k2
     )
     or
-    exists(CompareValueNumber cmp, Operand left, Operand right, AbstractValue v |
-      test = cmp and
-      pragma[only_bind_into](cmp)
-          .hasOperands(pragma[only_bind_into](left), pragma[only_bind_into](right)) and
-      isConvertedBool(left.getDef()) and
-      int_value(right.getDef()) = 0 and
-      unary_compares_eq(valueNumberOfOperand(left), op, k, areEqual, v)
-    |
-      cmp instanceof CompareNEValueNumber and
-      v = value
-      or
-      cmp instanceof CompareEQValueNumber and
-      v.getDualValue() = value
+    // See argument for why this is correct in compares_eq
+    exists(Operand l, BooleanValue bv |
+      unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
+      unary_compares_eq(valueNumberOfOperand(l), op, k, areEqual, bv)
     )
     or
     unary_compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), op, k, areEqual, value)
@@ -1215,6 +1218,12 @@ private module Cached {
     exists(AbstractValue dual | value = dual.getDualValue() |
       compares_lt(test.(LogicalNotValueNumber).getUnary(), left, right, k, isLt, dual)
     )
+    or
+    // See argument for why this is correct in compares_eq
+    exists(Operand l, BooleanValue bv |
+      unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
+      compares_lt(valueNumberOfOperand(l), left, right, k, isLt, bv)
+    )
   }
 
   /** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
@@ -1234,6 +1243,12 @@ private module Cached {
       int_value(const) = k1 and
       k = k1 + k2
     )
+    or
+    // See argument for why this is correct in compares_eq
+    exists(Operand l, BooleanValue bv |
+      unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
+      compares_lt(valueNumberOfOperand(l), op, k, isLt, bv)
+    )
   }
 
   /** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */

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

@@ -278,18 +278,34 @@
 | test.c:176:8:176:15 | ! ... | ! ... == 1 when ! ... is true |
 | test.c:176:8:176:15 | ! ... | ... < ... != 0 when ! ... is false |
 | test.c:176:8:176:15 | ! ... | ... < ... == 0 when ! ... is true |
+| test.c:176:8:176:15 | ! ... | a < b+0 when ! ... is false |
+| test.c:176:8:176:15 | ! ... | a >= b+0 when ! ... is true |
+| test.c:176:8:176:15 | ! ... | b < a+1 when ! ... is true |
+| test.c:176:8:176:15 | ! ... | b >= a+1 when ! ... is false |
 | test.c:176:10:176:14 | ... < ... | ! ... != 0 when ... < ... is false |
 | test.c:176:10:176:14 | ... < ... | ! ... != 1 when ... < ... is true |
 | test.c:176:10:176:14 | ... < ... | ! ... == 0 when ... < ... is true |
 | test.c:176:10:176:14 | ... < ... | ! ... == 1 when ... < ... is false |
 | test.c:176:10:176:14 | ... < ... | ... < ... != 0 when ... < ... is true |
 | test.c:176:10:176:14 | ... < ... | ... < ... == 0 when ... < ... is false |
+| test.c:176:10:176:14 | ... < ... | a < b+0 when ... < ... is true |
+| test.c:176:10:176:14 | ... < ... | a >= b+0 when ... < ... is false |
+| test.c:176:10:176:14 | ... < ... | b < a+1 when ... < ... is false |
+| test.c:176:10:176:14 | ... < ... | b >= a+1 when ... < ... is true |
+| test.c:182:8:182:34 | ! ... | 1.0 >= foo+1 when ! ... is false |
+| test.c:182:8:182:34 | ! ... | 9.999999999999999547e-07 < foo+1 when ! ... is false |
 | test.c:182:8:182:34 | ! ... | ! ... != 0 when ! ... is true |
 | test.c:182:8:182:34 | ! ... | ! ... != 1 when ! ... is false |
 | test.c:182:8:182:34 | ! ... | ! ... == 0 when ! ... is false |
 | test.c:182:8:182:34 | ! ... | ! ... == 1 when ! ... is true |
 | test.c:182:8:182:34 | ! ... | ... && ... != 0 when ! ... is false |
 | test.c:182:8:182:34 | ! ... | ... && ... == 0 when ! ... is true |
+| test.c:182:8:182:34 | ! ... | ... < ... != 0 when ! ... is false |
+| test.c:182:8:182:34 | ! ... | ... < ... == 1 when ! ... is false |
+| test.c:182:8:182:34 | ! ... | ... >= ... != 0 when ! ... is false |
+| test.c:182:8:182:34 | ! ... | ... >= ... == 1 when ! ... is false |
+| test.c:182:8:182:34 | ! ... | foo < 1.0+0 when ! ... is false |
+| test.c:182:8:182:34 | ! ... | foo >= 9.999999999999999547e-07+0 when ! ... is false |
 | test.c:182:10:182:20 | ... >= ... | 9.999999999999999547e-07 < foo+1 when ... >= ... is true |
 | test.c:182:10:182:20 | ... >= ... | 9.999999999999999547e-07 >= foo+1 when ... >= ... is false |
 | test.c:182:10:182:20 | ... >= ... | ... >= ... != 0 when ... >= ... is true |

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

@@ -165,6 +165,10 @@ binary
 | test.c:109:9:109:23 | ... \|\| ... | test.c:109:23:109:23 | 0 | < | test.c:109:19:109:19 | y | 1 | test.c:113:9:113:16 | return ... |
 | test.c:109:19:109:23 | ... < ... | test.c:109:19:109:19 | y | >= | test.c:109:23:109:23 | 0 | 0 | test.c:113:9:113:16 | return ... |
 | test.c:109:19:109:23 | ... < ... | test.c:109:23:109:23 | 0 | < | test.c:109:19:109:19 | y | 1 | test.c:113:9:113:16 | return ... |
+| test.c:176:8:176:15 | ! ... | test.c:176:10:176:10 | a | >= | test.c:176:14:176:14 | b | 0 | test.c:176:18:178:5 | { ... } |
+| test.c:176:8:176:15 | ! ... | test.c:176:14:176:14 | b | < | test.c:176:10:176:10 | a | 1 | test.c:176:18:178:5 | { ... } |
+| test.c:176:10:176:14 | ... < ... | test.c:176:10:176:10 | a | >= | test.c:176:14:176:14 | b | 0 | test.c:176:18:178:5 | { ... } |
+| test.c:176:10:176:14 | ... < ... | test.c:176:14:176:14 | b | < | test.c:176:10:176:10 | a | 1 | test.c:176:18:178:5 | { ... } |
 | test.c:182:10:182:20 | ... >= ... | test.c:182:10:182:12 | foo | >= | test.c:182:17:182:20 | 9.999999999999999547e-07 | 0 | test.c:181:25:182:20 | { ... } |
 | test.c:182:10:182:20 | ... >= ... | test.c:182:10:182:12 | foo | >= | test.c:182:17:182:20 | 9.999999999999999547e-07 | 0 | test.c:182:25:182:33 | foo |
 | test.c:182:10:182:20 | ... >= ... | test.c:182:17:182:20 | 9.999999999999999547e-07 | < | test.c:182:10:182:12 | foo | 1 | test.c:181:25:182:20 | { ... } |

cpp/ql/test/query-tests/Critical/MissingCheckScanf/MissingCheckScanf.expected

@@ -190,5 +190,3 @@ subpaths
 | test.cpp:484:9:484:9 | i | test.cpp:480:25:480:26 | scanf output argument | test.cpp:484:9:484:9 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:480:13:480:17 | call to scanf | call to scanf |
 | test.cpp:495:8:495:8 | i | test.cpp:491:25:491:26 | scanf output argument | test.cpp:495:8:495:8 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:491:13:491:17 | call to scanf | call to scanf |
 | test.cpp:545:8:545:8 | f | test.cpp:541:43:541:44 | sscanf output argument | test.cpp:545:8:545:8 | f | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 3. | test.cpp:541:10:541:15 | call to sscanf | call to sscanf |
-| test.cpp:569:9:569:9 | i | test.cpp:567:35:567:36 | scanf output argument | test.cpp:569:9:569:9 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:567:23:567:27 | call to scanf | call to scanf |
-| test.cpp:577:9:577:9 | i | test.cpp:575:30:575:31 | scanf output argument | test.cpp:577:9:577:9 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:575:18:575:22 | call to scanf | call to scanf |

cpp/ql/test/query-tests/Critical/MissingCheckScanf/test.cpp

@@ -566,14 +566,14 @@ void test_scanf_compared_in_conjunct_right(bool b) {
   int i;
   bool success = b && scanf("%d", &i) == 1;
   if(success) {
-    use(i); // GOOD [FALSE POSITIVE]
+    use(i); // GOOD
   }
 }
 
 void test_scanf_compared_in_conjunct_left(bool b) {
   int i;
   bool success = scanf("%d", &i) == 1 && b;
   if(success) {
-    use(i); // GOOD [FALSE POSITIVE]
+    use(i); // GOOD
   }
 }