Generate unique STP and Z3 array names deterministically

lib/Solver/STPBuilder.cpp

@@ -17,6 +17,7 @@
 
 #include "ConstantDivision.h"
 
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CommandLine.h"
 
 #include <cstdio>
@@ -415,15 +416,17 @@ ::VCExpr STPBuilder::getInitialArray(const Array *root) {
 
  if (!hashed) {
  // STP uniques arrays by name, so we make sure the name is unique by
- // including the address.
- char buf[32];
- unsigned const addrlen = sprintf(buf, "_%p", (const void*)root) + 1; // +1 for null-termination
- unsigned const space = (root->name.length() > 32 - addrlen)?(32 - addrlen):root->name.length();
- memmove(buf + space, buf, addrlen); // moving the address part to the end
- memcpy(buf, root->name.c_str(), space); // filling out the name part
-
- array_expr = buildArray(buf, root->getDomain(), root->getRange());
-
+ // using the size of the array hash as a counter.
+ std::string unique_id = llvm::itostr(_arr_hash._array_hash.size());
+ unsigned const uid_length = unique_id.length();
+ unsigned const space = (root->name.length() > 32 - uid_length)
+ ? (32 - uid_length)
+ : root->name.length();
+ std::string unique_name = root->name.substr(0, space) + unique_id;
+
+ array_expr = buildArray(unique_name.c_str(), root->getDomain(),
+ root->getRange());
+
  if (root->isConstantArray()) {
  // FIXME: Flush the concrete values into STP. Ideally we would do this
  // using assertions, which is much faster, but we need to fix the caching
@@ -904,4 +907,3 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
  }
 }
 #endif // ENABLE_STP
-

lib/Solver/Z3Builder.cpp

@@ -15,6 +15,8 @@
 #include "klee/util/Bits.h"
 #include "ConstantDivision.h"
 #include "klee/SolverStats.h"
+
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CommandLine.h"
 
 using namespace klee;
@@ -356,17 +358,16 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
 
  if (!hashed) {
  // Unique arrays by name, so we make sure the name is unique by
- // including the address.
- char buf[32];
- unsigned const addrlen =
- sprintf(buf, "_%p", (const void *)root) + 1; // +1 for null-termination
- unsigned const space = (root->name.length() > 32 - addrlen)
- ? (32 - addrlen)
+ // using the size of the array hash as a counter.
+ std::string unique_id = llvm::itostr(_arr_hash._array_hash.size());
+ unsigned const uid_length = unique_id.length();
+ unsigned const space = (root->name.length() > 32 - uid_length)
+ ? (32 - uid_length)
  : root->name.length();
- memmove(buf + space, buf, addrlen); // moving the address part to the end
- memcpy(buf, root->name.c_str(), space); // filling out the name part
+ std::string unique_name = root->name.substr(0, space) + unique_id;
 
- array_expr = buildArray(buf, root->getDomain(), root->getRange());
+ array_expr = buildArray(unique_name.c_str(), root->getDomain(),
+ root->getRange());
 
  if (root->isConstantArray()) {
  // FIXME: Flush the concrete values into Z3. Ideally we would do this