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

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);