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

This commit is contained in:
Mathias Vorreiter Pedersen
2023-08-11 11:46:28 +01:00
parent c0a54e90c9
commit 3d5b1986c9
5 changed files with 12 additions and 17 deletions

View File

@@ -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`.
*

View File

@@ -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 |

View File

@@ -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 | ... + ... | ... + ... |

View File

@@ -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 |

View File

@@ -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
}
}