diff options
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 4 | ||||
| -rw-r--r-- | lib/Solver/Z3Builder.cpp | 4 | ||||
| -rw-r--r-- | test/Solver/Z3ConstantArray.c | 8 | ||||
| -rw-r--r-- | test/regression/2023-11-20-solver.c | 36 | ||||
| -rw-r--r-- | unittests/Solver/Z3SolverTest.cpp | 2 |
5 files changed, 47 insertions, 7 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 9a38183d..69a247c2 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -438,7 +438,9 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width // STP uniques arrays by name, so we make sure the name is unique by // using the size of the array hash as a counter. std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); - std::string unique_name = root->name + unique_id; + // Prefix unique ID with '_' to avoid name collision if name ends with + // number + std::string unique_name = root->name + "_" + unique_id; array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index e1937158..0e51967e 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -394,7 +394,9 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { // Unique arrays by name, so we make sure the name is unique by // using the size of the array hash as a counter. std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); - std::string unique_name = root->name + unique_id; + // Prefix unique ID with '_' to avoid name collision if name ends with + // number + std::string unique_name = root->name + "_" + unique_id; array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); 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 diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp index e81ff19e..0eba3d0e 100644 --- a/unittests/Solver/Z3SolverTest.cpp +++ b/unittests/Solver/Z3SolverTest.cpp @@ -64,7 +64,7 @@ TEST_F(Z3SolverTest, GetConstraintLog) { // Ensure this is not buggy as fixed in https://github.com/klee/klee/pull/1235 // If the bug is still present this fail due to an internal assertion char *ConstraintsString = Z3Solver_->getConstraintLog(TheQuery); - const char *ExpectedArraySelection = "(= (select const_array0"; + const char *ExpectedArraySelection = "(= (select const_array_0"; const char *Occurence = std::strstr(ConstraintsString, ExpectedArraySelection); ASSERT_STRNE(Occurence, nullptr); free(ConstraintsString); |