C++: Fix a bug where 'boundedImpl' could give back multiple deltas.

MathiasVP · MathiasVP · commit 3d5b1986c9ce · 2023-08-11T11:46:28.000+01:00
diff --git a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/RangeAnalysisUtil.qll b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/RangeAnalysisUtil.qll
@@ -18,7 +18,7 @@ private Instruction getABoundIn(SemBound b, IRFunction func) {
  * Holds if `i <= b + delta`.
  */
 pragma[inline]
-private predicate boundedImpl(Instruction i, Instruction b, int delta) {
+private predicate boundedImplCand(Instruction i, Instruction b, int delta) {
   exists(SemBound bound, IRFunction func |
     semBounded(getSemanticExpr(i), bound, delta, true,
       any(SemReason reason | not reason instanceof SemTypeReason)) and
@@ -27,6 +27,15 @@ private predicate boundedImpl(Instruction i, Instruction b, int delta) {
   )
 }
 
+/**
+ * Holds if `i <= b + delta` and `delta` is the smallest integer that satisfies
+ * this condition.
+ */
+pragma[inline]
+private predicate boundedImpl(Instruction i, Instruction b, int delta) {
+  delta = min(int cand | boundedImplCand(i, b, cand))
+}
+
 /**
  * Holds if `i <= b + delta`.
  *
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/AllocationToInvalidPointer.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/AllocationToInvalidPointer.expected
@@ -1,6 +1,2 @@
 failures
 testFailures
-| test.cpp:308:5:308:11 | PointerAdd: access to array | Unexpected result: alloc=L304 |
-| test.cpp:308:5:308:11 | PointerAdd: access to array | Unexpected result: alloc=L304-1 |
-| test.cpp:725:5:725:11 | PointerAdd: access to array | Unexpected result: alloc=L722 |
-| test.cpp:725:5:725:11 | PointerAdd: access to array | Unexpected result: alloc=L722-1 |
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerDeref.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerDeref.expected
@@ -129,7 +129,6 @@ edges
 | test.cpp:271:14:271:21 | ... + ... | test.cpp:271:14:271:21 | ... + ... |
 | test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... |
 | test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... |
-| test.cpp:304:15:304:26 | new[] | test.cpp:308:5:308:29 | ... = ... |
 | test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... |
 | test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... |
 | test.cpp:355:14:355:27 | new[] | test.cpp:357:24:357:30 | ... + ... |
@@ -223,7 +222,6 @@ edges
 | test.cpp:705:18:705:18 | q | test.cpp:706:12:706:13 | * ... |
 | test.cpp:711:13:711:26 | new[] | test.cpp:714:11:714:11 | q |
 | test.cpp:714:11:714:11 | q | test.cpp:705:18:705:18 | q |
-| test.cpp:722:13:722:22 | new[] | test.cpp:725:5:725:15 | ... = ... |
 nodes
 | test.cpp:4:15:4:20 | call to malloc | semmle.label | call to malloc |
 | test.cpp:5:15:5:22 | ... + ... | semmle.label | ... + ... |
@@ -316,8 +314,6 @@ nodes
 | test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... |
 | test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... |
 | test.cpp:274:5:274:10 | ... = ... | semmle.label | ... = ... |
-| test.cpp:304:15:304:26 | new[] | semmle.label | new[] |
-| test.cpp:308:5:308:29 | ... = ... | semmle.label | ... = ... |
 | test.cpp:355:14:355:27 | new[] | semmle.label | new[] |
 | test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... |
 | test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... |
@@ -376,8 +372,6 @@ nodes
 | test.cpp:706:12:706:13 | * ... | semmle.label | * ... |
 | test.cpp:711:13:711:26 | new[] | semmle.label | new[] |
 | test.cpp:714:11:714:11 | q | semmle.label | q |
-| test.cpp:722:13:722:22 | new[] | semmle.label | new[] |
-| test.cpp:725:5:725:15 | ... = ... | semmle.label | ... = ... |
 subpaths
 #select
 | test.cpp:6:14:6:15 | * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:6:14:6:15 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
@@ -399,7 +393,6 @@ subpaths
 | test.cpp:254:9:254:16 | ... = ... | test.cpp:248:24:248:30 | call to realloc | test.cpp:254:9:254:16 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:248:24:248:30 | call to realloc | call to realloc | test.cpp:254:11:254:11 | i | i |
 | test.cpp:264:13:264:14 | * ... | test.cpp:260:13:260:24 | new[] | test.cpp:264:13:264:14 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:260:13:260:24 | new[] | new[] | test.cpp:261:19:261:21 | len | len |
 | test.cpp:274:5:274:10 | ... = ... | test.cpp:270:13:270:24 | new[] | test.cpp:274:5:274:10 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:270:13:270:24 | new[] | new[] | test.cpp:271:19:271:21 | len | len |
-| test.cpp:308:5:308:29 | ... = ... | test.cpp:304:15:304:26 | new[] | test.cpp:308:5:308:29 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:304:15:304:26 | new[] | new[] | test.cpp:308:8:308:10 | ... + ... | ... + ... |
 | test.cpp:358:14:358:26 | * ... | test.cpp:355:14:355:27 | new[] | test.cpp:358:14:358:26 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
 | test.cpp:359:14:359:32 | * ... | test.cpp:355:14:355:27 | new[] | test.cpp:359:14:359:32 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 2. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
 | test.cpp:384:13:384:16 | * ... | test.cpp:377:14:377:27 | new[] | test.cpp:384:13:384:16 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:377:14:377:27 | new[] | new[] | test.cpp:378:20:378:23 | size | size |
@@ -413,4 +406,3 @@ subpaths
 | test.cpp:647:5:647:19 | ... = ... | test.cpp:642:14:642:31 | new[] | test.cpp:647:5:647:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:642:14:642:31 | new[] | new[] | test.cpp:647:8:647:14 | src_pos | src_pos |
 | test.cpp:701:15:701:16 | * ... | test.cpp:695:13:695:26 | new[] | test.cpp:701:15:701:16 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:695:13:695:26 | new[] | new[] | test.cpp:696:19:696:22 | size | size |
 | test.cpp:706:12:706:13 | * ... | test.cpp:711:13:711:26 | new[] | test.cpp:706:12:706:13 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:711:13:711:26 | new[] | new[] | test.cpp:712:19:712:22 | size | size |
-| test.cpp:725:5:725:15 | ... = ... | test.cpp:722:13:722:22 | new[] | test.cpp:725:5:725:15 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:722:13:722:22 | new[] | new[] | test.cpp:725:8:725:10 | ... + ... | ... + ... |
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerToDereference.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerToDereference.expected
@@ -1,4 +1,2 @@
 failures
 testFailures
-| test.cpp:308:5:308:29 | ... = ... | Unexpected result: deref=L308 |
-| test.cpp:725:5:725:15 | ... = ... | Unexpected result: deref=L725 |
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp
@@ -305,7 +305,7 @@ void test21() {
 
   for (int i = 0; i < n; i += 2) {
     xs[i] = test21_get(i); // GOOD
-    xs[i+1] = test21_get(i+1); // GOOD [FALSE POSITIVE]
+    xs[i+1] = test21_get(i+1); // GOOD
   }
 }
 
@@ -722,6 +722,6 @@ void test21_simple(bool b) {
   int* xs = new int[n];
 
   for (int i = 0; i < n; i += 2) {
-    xs[i+1] = 0; // GOOD [FALSE POSITIVE]
+    xs[i+1] = 0; // GOOD
   }
 }

Original file line number	Diff line number	Diff line change
`@@ -305,7 +305,7 @@ void test21() {`
`305`	`305`
`306`	`306`	`for (int i = 0; i < n; i += 2) {`
`307`	`307`	`xs[i] = test21_get(i); // GOOD`
`308`		`- xs[i+1] = test21_get(i+1); // GOOD [FALSE POSITIVE]`
	`308`	`+ xs[i+1] = test21_get(i+1); // GOOD`
`309`	`309`	`}`
`310`	`310`	`}`
`311`	`311`
`@@ -722,6 +722,6 @@ void test21_simple(bool b) {`
`722`	`722`	`int* xs = new int[n];`
`723`	`723`
`724`	`724`	`for (int i = 0; i < n; i += 2) {`
`725`		`- xs[i+1] = 0; // GOOD [FALSE POSITIVE]`
	`725`	`+ xs[i+1] = 0; // GOOD`
`726`	`726`	`}`
`727`	`727`	`}`