Associate a domain and range with each array

2 files changed, 11 insertions, 7 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index f893c6cc..ee3c3253 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -587,7 +587,9 @@ public:
   /// a symbolic array. If non-empty, this size of this array is equivalent to
   /// the array size.
   const std::vector< ref<ConstantExpr> > constantValues;
-  
+
+  Expr::Width domain, range;
+
 public:
   /// Array - Construct a new array object.
   ///
@@ -598,9 +600,11 @@ public:
   /// distinguished once printed.
   Array(const std::string &_name, uint64_t _size, 
         const ref<ConstantExpr> *constantValuesBegin = 0,
-        const ref<ConstantExpr> *constantValuesEnd = 0)
+        const ref<ConstantExpr> *constantValuesEnd = 0,
+        Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8)
     : name(_name), size(_size), 
-      constantValues(constantValuesBegin, constantValuesEnd) {      
+      constantValues(constantValuesBegin, constantValuesEnd),
+      domain(_domain), range(_range) {
     assert((isSymbolicArray() || constantValues.size() == size) &&
            "Invalid size for constant array!");
     computeHash();
@@ -616,8 +620,8 @@ public:
   bool isSymbolicArray() const { return constantValues.empty(); }
   bool isConstantArray() const { return !isSymbolicArray(); }
 
-  Expr::Width getDomain() const { return Expr::Int32; }
-  Expr::Width getRange() const { return Expr::Int8; }
+  Expr::Width getDomain() const { return domain; }
+  Expr::Width getRange() const { return range; }
   
   unsigned computeHash();
   unsigned hash() const { return hashValue; }
@@ -671,7 +675,7 @@ public:
   
   static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
   
-  Width getWidth() const { return Expr::Int8; }
+  Width getWidth() const { return updates.root->getRange(); }
   Kind getKind() const { return Read; }
   
   unsigned getNumKids() const { return numKids; }
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index ad0df3c2..ebc096df 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -439,7 +439,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
     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, 32, 8);
+    array_expr = buildArray(buf, root->getDomain(), root->getRange());
     
     if (root->isConstantArray()) {
       // FIXME: Flush the concrete values into STP. Ideally we would do this