diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2023-11-20 22:41:19 +0000 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-30 17:56:08 +0000 |
| commit | f813c88c8cb868fc9c0be78fbf92a94d72ac02b0 (patch) | |
| tree | 6647c2eb38a4a1502d9806bcdbfd919a07acaedc /test | |
| parent | cb5e898561f9b8769d8838bc1bdca17a6f4f5d20 (diff) | |
| download | klee-f813c88c8cb868fc9c0be78fbf92a94d72ac02b0.tar.gz | |
Avoid generating array names in solver builders that could accidently collide
If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668
Diffstat (limited to 'test')
| -rw-r--r-- | test/Solver/Z3ConstantArray.c | 8 | ||||
| -rw-r--r-- | test/regression/2023-11-20-solver.c | 36 |
2 files changed, 40 insertions, 4 deletions
diff --git a/test/Solver/Z3ConstantArray.c b/test/Solver/Z3ConstantArray.c index d9495795..c49bbd1b 100644 --- a/test/Solver/Z3ConstantArray.c +++ b/test/Solver/Z3ConstantArray.c @@ -9,10 +9,10 @@ #include "klee/klee.h" int main(int argc, char **argv) { - // CHECK-DAG: (assert (= (select const_arr11 #x00000000) #x67)) - // CHECK-DAG: (assert (= (select const_arr11 #x00000001) #x79)) - // CHECK-DAG: (assert (= (select const_arr11 #x00000002) #x7a)) - // CHECK-DAG: (assert (= (select const_arr11 #x00000003) #x00)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000000) #x67)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000001) #x79)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000002) #x7a)) + // CHECK-DAG: (assert (= (select const_arr1_1 #x00000003) #x00)) // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv0 32) ) (_ bv103 8) ) ) // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv1 32) ) (_ bv121 8) ) ) // TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv2 32) ) (_ bv122 8) ) ) diff --git a/test/regression/2023-11-20-solver.c b/test/regression/2023-11-20-solver.c new file mode 100644 index 00000000..ceef8180 --- /dev/null +++ b/test/regression/2023-11-20-solver.c @@ -0,0 +1,36 @@ +// Test case based on #1668, generates array names as part of the solver builder that collide. +// This depends on the order of expression evaluation. +// +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -silent-klee-assume --use-branch-cache=false --use-cex-cache=false --use-independent-solver=false %t1.bc 2>&1 | FileCheck %s +#include "klee/klee.h" +#include <assert.h> + +int main() { + int p1 = klee_int("val"); + int p2 = klee_int("val"); + int p3 = klee_int("val"); + int p4 = klee_int("val"); + int p5 = klee_int("val"); + int p6 = klee_int("val"); + int p7 = klee_int("val"); + int p8 = klee_int("val"); + int p9 = klee_int("val"); + int p10 = klee_int("val"); + int p11 = klee_int("val"); + int p12 = klee_int("val"); + int p13 = klee_int("val"); + int p14 = klee_int("val"); + int p15 = klee_int("val"); + int cond = klee_int("val"); + klee_assume(p12 > p14); + klee_assume(p6 > p3); + // klee_assume(p2 > 0); + klee_assume(p7 != 0); + klee_assume(p11 < p14 & p15 < p13); + klee_assume(cond > p5); + klee_assume(0 > p4); + // CHECK: [[@LINE+1]]: ASSERTION FAIL + assert(p2 > p11); +} \ No newline at end of file |