about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h49
-rw-r--r--lib/Core/Executor.cpp2
-rw-r--r--lib/Core/Memory.cpp4
-rw-r--r--lib/Expr/Expr.cpp17
-rw-r--r--lib/Expr/Parser.cpp2
5 files changed, 38 insertions, 36 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 2ea7f40f..af8bf10f 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -601,7 +601,7 @@ private:
 
 class Array {
 public:
-  //Name of the array
+  // Name of the array
   const std::string name;
 
   // FIXME: Not 64-bit clean.
@@ -620,18 +620,20 @@ private:
   unsigned hashValue;
 
 
-  /// The symbolic array singleton map is necessary to prevent aliasing issues on arrays.
-  /// A lot of the Solvers use maps such as <const * Array, std::vector<unsigned>>.
-  /// This causes problems because stored answers can't be easily recovered.
-  /// Even worse, in read expressions, such as (read array 32), array is a pointer,
-  /// meaning actual solutions don't "work" because the two instances of array
+  /// The symbolic array singleton map is necessary to allow sharing
+  /// of Arrays across states, essentially performing a (limited) form
+  /// of alpha renaming.  Some Solvers use maps such as < const *Array,
+  /// std::vector<unsigned> >.  This causes problems because stored
+  /// answers can't be easily recovered.  Even worse, in read
+  /// expressions, such as (read array 32), array is a pointer, and
+  /// cached solutions are missed because the two Array instances
   /// aren't recognized as the same.
-  static std::map<unsigned, std::vector<const Array *> *> symbolicArraySingletonMap;
+  static std::map < unsigned, std::vector < const Array * > * > symbolicArraySingletonMap;
 
-  //This shouldn't be allowed since it's a singleton class
+  // This shouldn't be allowed since it is a singleton class
   Array(const Array& array);
 
-  //This shouldn't be allowed since it's a singleton class
+  // This shouldn't be allowed since it is a singleton class
   Array& operator =(const Array& array);
 
   ~Array();
@@ -644,11 +646,12 @@ private:
   /// not parse correctly since two arrays with the same name cannot be
   /// distinguished once printed.
   Array(const std::string &_name, uint64_t _size,
-		const ref<ConstantExpr> *constantValuesBegin = 0,
-		const ref<ConstantExpr> *constantValuesEnd = 0,
-		Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8)
+	const ref<ConstantExpr> *constantValuesBegin = 0,
+	const ref<ConstantExpr> *constantValuesEnd = 0,
+	Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8)
     : name(_name), size(_size), domain(_domain), range(_range),
-	  constantValues(constantValuesBegin, constantValuesEnd) {
+      constantValues(constantValuesBegin, constantValuesEnd) {
+    
     assert((isSymbolicArray() || constantValues.size() == size) &&
            "Invalid size for constant array!");
     computeHash();
@@ -674,18 +677,18 @@ public:
   unsigned hash() const { return hashValue; }
 
   /*
-   * Fairly simple idea.  Since by defn (see Array), symbolic arrays
-   * have constant values of size 0.  Concrete Arrays have their respective
-   * values stored in each element.  Therefore, each incoming call is tested.
-   * An array is created and, if it's concrete, it's simply returned.  If
-   * instead it is symbolic, then a map is checked to see if it was created
-   * before, so there is only a single instance floating out there.
+   * Fairly simple idea.  Symbolic arrays have constant values of size
+   * 0, while concrete arrays have constant values of size > 0.
+   * Therefore, on each call, an array is created and, if it is
+   * concrete, it is simply returned.  If instead it is symbolic, then
+   * a map is checked to see if it was created before, so there is
+   * only a single instance floating out there.
    */
   static const Array * CreateArray(const std::string &_name, uint64_t _size,
-	                               const ref<ConstantExpr> *constantValuesBegin = 0,
-			                       const ref<ConstantExpr> *constantValuesEnd = 0,
-			                       Expr::Width _domain = Expr::Int32,
-								   Expr::Width _range = Expr::Int8);
+				   const ref<ConstantExpr> *constantValuesBegin = 0,
+				   const ref<ConstantExpr> *constantValuesEnd = 0,
+				   Expr::Width _domain = Expr::Int32,
+				   Expr::Width _range = Expr::Int8);
 };
 
 /// Class representing a complete list of updates into an array.
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 8631061f..c78c9f8a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2925,7 +2925,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
   
   static unsigned id;
   const Array *array = Array::CreateArray("rrws_arr" + llvm::utostr(++id),
-                                 Expr::getMinBytesForWidth(e->getWidth()));
+					  Expr::getMinBytesForWidth(e->getWidth()));
   ref<Expr> res = Expr::createTempRead(array, e->getWidth());
   ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
   llvm::errs() << "Making symbolic: " << eq << "\n";
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index b9f6afd0..1dd1e1fd 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -223,8 +223,8 @@ const UpdateList &ObjectState::getUpdates() const {
     // FIXME: Leaked.
     static unsigned id = 0;
     const Array *array = Array::CreateArray("const_arr" + llvm::utostr(++id), size,
-                                   &Contents[0],
-                                   &Contents[0] + Contents.size());
+					    &Contents[0],
+					    &Contents[0] + Contents.size());
     updates = UpdateList(array, 0);
 
     // Apply the remaining (non-constant) writes.
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 46ea30fc..baa85663 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -501,31 +501,30 @@ const Array * Array::CreateArray(const std::string &_name, uint64_t _size,
                                  const ref<ConstantExpr> *constantValuesBegin,
                                  const ref<ConstantExpr> *constantValuesEnd,
                                  Expr::Width _domain,
-								 Expr::Width _range){
+				 Expr::Width _range) {
 
   const Array * array = new Array(_name, _size, constantValuesBegin, constantValuesEnd, _domain,_range);
-  if(array->constantValues.size() == 0){
-    //means is a symbolic array and we should look up the values;
+  if (array->constantValues.size() == 0) { // symbolic array
     unsigned hash = array->hash();
     std::vector<const Array *> * bucket = Array::symbolicArraySingletonMap[hash];
-    if(bucket){
-      for(std::vector<const Array*>::const_iterator it = bucket->begin();
-          it != bucket->end(); it ++){
+    if (bucket){
+      for (std::vector<const Array*>::const_iterator it = bucket->begin();
+	   it != bucket->end(); it ++){
         const Array* prospect = *it;
-    	if(prospect->size == array->size && prospect->name == array->name){
+	if (prospect->size == array->size && prospect->name == array->name){
     	  delete array;
     	  return prospect;
     	}
       }
       bucket->push_back(array);
       return array;
-    }else{
+    } else {
       bucket = new std::vector<const Array *>();
       bucket->push_back(array);
       Array::symbolicArraySingletonMap[hash] = bucket;
       return array;
     }
-  }else{
+  } else { // concrete array
     return array;
   }
 }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 9df08903..23a292fa 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -522,7 +522,7 @@ DeclResult ParserImpl::ParseArrayDecl() {
   const Array *Root;
   if (!Values.empty())
     Root = Array::CreateArray(Label->Name, Size.get(),
-                     &Values[0], &Values[0] + Values.size());
+			      &Values[0], &Values[0] + Values.size());
   else
     Root = Array::CreateArray(Label->Name, Size.get());
   ArrayDecl *AD = new ArrayDecl(Label, Size.get(),
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 08:13:28 +0000