about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h18
-rw-r--r--lib/Core/Memory.h4
-rw-r--r--lib/Expr/Parser.cpp6
-rw-r--r--lib/Expr/Updates.cpp18
-rw-r--r--lib/Solver/STPBuilder.cpp4
-rw-r--r--unittests/Expr/ExprTest.cpp8
-rw-r--r--unittests/Solver/SolverTest.cpp2
7 files changed, 33 insertions, 27 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index d9cdf5e0..f13ab6d5 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -476,7 +476,6 @@ public:
   const std::string name;
   // FIXME: This does not belong here.
   const MemoryObject *object;
-  unsigned id;
   // FIXME: Not 64-bit clean.
   unsigned size;
 
@@ -484,14 +483,15 @@ public:
   mutable void *stpInitialArray;
 
 public:
-  // NOTE: id's ***MUST*** be unique to ensure sanity w.r.t. STP,
-  // which hashes different arrays with the same id to the same
-  // object! We should probably use the pointer for talking to STP, as
-  // long as we can guarantee that it won't be a "stale" reference
-  // once we have freed it.
-  Array(const std::string &_name, const MemoryObject *_object, 
-        unsigned _id, uint64_t _size) 
-    : name(_name), object(_object), id(_id), size(_size), stpInitialArray(0) {}
+  /// Array - Construct a new array object.
+  ///
+  /// \param _name - The name for this arrays. Names should generally be unique
+  /// across an application, but this is not necessary for correctness, except
+  /// when printing expressions. When expressions are printed the output will
+  /// not parse correctly since two arrays with the same name cannot be
+  /// distinguished once printed.
+  Array(const std::string &_name, const MemoryObject *_object, uint64_t _size) 
+    : name(_name), object(_object), size(_size), stpInitialArray(0) {}
   ~Array() {
     // FIXME: This relies on caller to delete the STP array.
     assert(!stpInitialArray && "Array must be deleted by caller!");
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 537c783a..141060d0 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -71,7 +71,7 @@ public:
   MemoryObject(uint64_t _address) 
     : id(counter++),
       address(_address),
-      array(new Array("arr" + llvm::utostr(id), this, 0, id)),
+      array(new Array("arr" + llvm::utostr(id), this, id)),
       size(0),
       isFixed(true),
       allocSite(0) {
@@ -82,7 +82,7 @@ public:
                const llvm::Value *_allocSite) 
     : id(counter++),
       address(_address),
-      array(new Array("arr" + llvm::utostr(id), this, id, _size)),
+      array(new Array("arr" + llvm::utostr(id), this, _size)),
       size(_size),
       name("unnamed"),
       isLocal(_isLocal),
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 8c18fe73..856541ee 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -517,11 +517,9 @@ DeclResult ParserImpl::ParseArrayDecl() {
   if (!RangeType.isValid())
     RangeType = 8;
 
-  // FIXME: Array should take name, not id.
   // FIXME: Array should take domain and range.
   const Identifier *Label = GetOrCreateIdentifier(Name);
-  static int counter = 0;
-  Array *Root = new Array(Label->Name, 0, ++counter, Size.get());
+  Array *Root = new Array(Label->Name, 0, Size.get());
   ArrayDecl *AD = new ArrayDecl(Label, Size.get(), 
                                 DomainType.get(), RangeType.get(), Root);
 
@@ -1300,7 +1298,7 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
   VersionResult Res = ParseVersion();
   // Define update list to avoid use-of-undef errors.
   if (!Res.isValid()) {
-    Res = VersionResult(true, UpdateList(new Array("", 0, -1, 0), NULL));
+    Res = VersionResult(true, UpdateList(new Array("", 0, 0), NULL));
   }
   
   if (Label)
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 22544820..379f1c8d 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -94,10 +94,14 @@ void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
 }
 
 int UpdateList::compare(const UpdateList &b) const {
-  // use object id to increase determinism
-  if (root->id != b.root->id) 
-    return root->id < b.root->id ? -1 : 1;
-  
+  if (root->name != b.root->name)
+    return root->name < b.root->name ? -1 : 1;
+
+  // Check the root itself in case we have separate objects with the
+  // same name.
+  if (root != b.root)
+    return root < b.root ? -1 : 1;
+
   if (getSize() < b.getSize()) return -1;
   else if (getSize() > b.getSize()) return 1;    
 
@@ -111,12 +115,14 @@ int UpdateList::compare(const UpdateList &b) const {
         return res;
     }
   }
-  assert(!an && !bn);
+  assert(!an && !bn);  
   return 0;
 }
 
 unsigned UpdateList::hash() const {
-  unsigned res = root->id * Expr::MAGIC_HASH_CONSTANT;
+  unsigned res = 0;
+  for (unsigned i = 0, e = root->name.size(); i != e; ++i)
+    res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
   if (head)
     res ^= head->hash();
   return res;
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 680b7d43..856540fe 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -388,8 +388,10 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
   if (root->stpInitialArray) {
     return root->stpInitialArray;
   } else {
+    // STP uniques arrays by name, so we make sure the name is unique by
+    // including the address.
     char buf[32];
-    sprintf(buf, "arr%d", root->id);
+    sprintf(buf, "%s_%p", root->name.c_str(), (void*) root);
     root->stpInitialArray = buildArray(buf, 32, 8);
     return root->stpInitialArray;
   }
diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp
index f86af1aa..b5f02b83 100644
--- a/unittests/Expr/ExprTest.cpp
+++ b/unittests/Expr/ExprTest.cpp
@@ -28,9 +28,9 @@ TEST(ExprTest, BasicConstruction) {
 }
 
 TEST(ExprTest, ConcatExtract) {
-  Array *array = new Array("arr0", 0, 1, 256);
+  Array *array = new Array("arr0", 0, 256);
   ref<Expr> read8 = Expr::createTempRead(array, 8);
-  Array *array2 = new Array("arr1", 0, 2, 256);
+  Array *array2 = new Array("arr1", 0, 256);
   ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
   ref<Expr> c100 = getConstant(100, 8);
 
@@ -80,10 +80,10 @@ TEST(ExprTest, ConcatExtract) {
 }
 
 TEST(ExprTest, ExtractConcat) {
-  Array *array = new Array("arr0", 0, 3, 256);
+  Array *array = new Array("arr2", 0, 256);
   ref<Expr> read64 = Expr::createTempRead(array, 64);
 
-  Array *array2 = new Array("arr1", 0, 4, 256);
+  Array *array2 = new Array("arr3", 0, 256);
   ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
   
   ref<Expr> extract1 = ExtractExpr::create(read64, 36, 4);
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index a6130716..87ec63ef 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -45,7 +45,7 @@ void testOperation(Solver &solver,
 
     unsigned size = Expr::getMinBytesForWidth(operandWidth);
     static uint64_t id = 0;
-    Array *array = new Array("arr" + llvm::utostr(id), 0, ++id, size);
+    Array *array = new Array("arr" + llvm::utostr(++id), 0, size);
     symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(array, 
                                                                 operandWidth)));
   }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-24 09:27:32 +0000