Use ConstantExpr::alloc instead of ref<Expr> directly

 - The "constant optimization" embedded inside ref<Expr> is going away.

 - No functionality change.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8

5 files changed, 19 insertions, 58 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index d16a09bf..cb5423e0 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -238,7 +238,7 @@ struct Expr::CreateArg {
   ref<Expr> expr;
   Width width;
   
-  CreateArg(Width w = Bool) : expr(0, Expr::Bool), width(w) {}
+  CreateArg(Width w = Bool) : expr(0), width(w) {}
   CreateArg(ref<Expr> e) : expr(e), width(Expr::InvalidWidth) {}
   
   bool isExpr() { return !isWidth(); }
@@ -328,12 +328,12 @@ public:
   static ref<ConstantExpr> fromMemory(void *address, Width w);
   void toMemory(void *address);
 
-  static ref<ConstantExpr> alloc(uint64_t v, Width w) {
+  static ref<Expr> alloc(uint64_t v, Width w) {
     // constructs an "optimized" ConstantExpr
     return ref<ConstantExpr>(v, w);
   }
   
-  static ref<ConstantExpr> create(uint64_t v, Width w) {
+  static ref<Expr> create(uint64_t v, Width w) {
     assert(v == bits64::truncateToNBits(v, w) &&
            "invalid constant");
     return alloc(v, w);
diff --git a/include/klee/Internal/Support/QueryLog.h b/include/klee/Internal/Support/QueryLog.h
index b090d2d9..212ab760 100644
--- a/include/klee/Internal/Support/QueryLog.h
+++ b/include/klee/Internal/Support/QueryLog.h
@@ -35,7 +35,7 @@ namespace klee {
     std::vector<const Array*> objects;
     
   public:
-    QueryLogEntry() : query(0,Expr::Bool) {}
+    QueryLogEntry() : query(ConstantExpr::alloc(0,Expr::Bool)) {}
     QueryLogEntry(const QueryLogEntry &b);
     QueryLogEntry(const Query &_query, 
                   Type _type,
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index a053050d..1ed8c175 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -35,7 +35,7 @@ namespace klee {
 
     /// withFalse - Return a copy of the query with a false expression.
     Query withFalse() const {
-      return Query(constraints, ref<Expr>(0, Expr::Bool));
+      return Query(constraints, ConstantExpr::alloc(0, Expr::Bool));
     }
 
     /// negateExpr - Return a copy of the query with the expression negated.
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 19f89a03..cb001415 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -69,13 +69,13 @@ namespace klee {
                                         unsigned index) const {
     bindings_ty::const_iterator it = bindings.find(array);
     if (it!=bindings.end() && index<it->second.size()) {
-      return ref<Expr>(it->second[index], Expr::Int8);
+      return ConstantExpr::alloc(it->second[index], Expr::Int8);
     } else {
       if (allowFreeValues) {
         return ReadExpr::create(UpdateList(array, true, 0), 
-                                ref<Expr>(index, Expr::Int32));
+                                ConstantExpr::alloc(index, Expr::Int32));
       } else {
-        return ref<Expr>(0, Expr::Int8);
+        return ConstantExpr::alloc(0, Expr::Int8);
       }
     }
   }
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index a70b09cf..f900f137 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -13,48 +13,11 @@
 #include <assert.h>
 
 class Expr;
-class BinaryExpr;
-class CastExpr;
-class CmpExpr;
-
 class ConstantExpr;
-class ReadExpr;
-class UpdateNode;
-class NotOptimizedExpr;
-class ReadExpr;
-class SelectExpr;
-class ConcatExpr;
-class ExtractExpr;
-class ZExtExpr;
-class SExtExpr;
-class AddExpr;
-class SubExpr;
-class MulExpr;
-class UDivExpr;
-class SDivExpr;
-class URemExpr;
-class SRemExpr;
-class AndExpr;
-class OrExpr;
-class XorExpr;
-class ShlExpr;
-class LShrExpr;
-class AShrExpr;
-class EqExpr;
-class NeExpr;
-class UltExpr;
-class UleExpr;
-class UgtExpr;
-class UgeExpr;
-class SltExpr;
-class SleExpr;
-class SgtExpr;
-class SgeExpr;
-class KModule;
-
-  class ExprVisitor;
-  class StackFrame;
-  class ObjectState;
+
+class ExprVisitor;
+class StackFrame;
+class ObjectState;
 
 template<class T>
 class ref {
@@ -91,9 +54,12 @@ private:
   }  
 
   friend class ExprVisitor;
-  friend class Cell;
-  friend class ObjectState;
-  friend class KModule;
+  friend class ConstantExpr;
+
+  // construct from constant
+  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
+    contents.val = val;
+  }
 
 public:
   template<class U> friend class ref;
@@ -107,14 +73,9 @@ public:
     contents.ptr = p;
     inc();
   }
-
-  // construct from constant
-  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
-    contents.val = val;
-  }
   
   // normal copy constructor
-  ref (const ref<T> &r)
+  ref(const ref<T> &r)
     : constantWidth(r.constantWidth), contents(r.contents) {
     inc();
   }