about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutionState.cpp3
-rw-r--r--lib/Core/Executor.cpp58
-rw-r--r--lib/Core/ExecutorUtil.cpp4
-rw-r--r--lib/Core/ImpliedValue.cpp5
-rw-r--r--lib/Core/Memory.h6
-rw-r--r--lib/Core/SeedInfo.cpp12
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp2
-rw-r--r--lib/Core/TimingSolver.cpp2
8 files changed, 45 insertions, 47 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index dd6d4647..d07b6490 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -247,7 +247,8 @@ bool ExecutionState::merge(const ExecutionState &b) {
   
   // merge stack
 
-  ref<Expr> inA(1, Expr::Bool), inB(1, Expr::Bool);
+  ref<Expr> inA = ConstantExpr::alloc(1, Expr::Bool);
+  ref<Expr> inB = ConstantExpr::alloc(1, Expr::Bool);
   for (std::set< ref<Expr> >::iterator it = aSuffix.begin(), 
          ie = aSuffix.end(); it != ie; ++it)
     inA = AndExpr::create(inA, *it);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 9c6d84cd..c3d2fcb4 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -902,7 +902,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
 
   state.addConstraint(condition);
   if (ivcEnabled)
-    doImpliedValueConcretization(state, condition, ref<Expr>(1, Expr::Bool));
+    doImpliedValueConcretization(state, condition, ConstantExpr::alloc(1, Expr::Bool));
 }
 
 ref<Expr> Executor::evalConstant(Constant *c) {
@@ -1268,7 +1268,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     KInstIterator kcaller = state.stack.back().caller;
     Instruction *caller = kcaller ? kcaller->inst : 0;
     bool isVoidReturn = (ri->getNumOperands() == 0);
-    ref<Expr> result(0,Expr::Bool);
+    ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool);
 
     if (WriteTraces) {
       state.exeTraceMgr.addEvent(new FunctionReturnTraceEvent(state, ki));
@@ -1402,7 +1402,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
     } else {
       std::map<BasicBlock*, ref<Expr> > targets;
-      ref<Expr> isDefault(1,Expr::Bool);
+      ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool);
       for (unsigned i=1; i<cases; ++i) {
         ref<Expr> value = evalConstant(si->getCaseValue(i));
         ref<Expr> match = EqExpr::create(cond, value);
@@ -1413,7 +1413,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         if (result) {
           std::map<BasicBlock*, ref<Expr> >::iterator it =
             targets.insert(std::make_pair(si->getSuccessor(i),
-                                          ref<Expr>(0,Expr::Bool))).first;
+                                          ConstantExpr::alloc(0, Expr::Bool))).first;
           it->second = OrExpr::create(match, it->second);
         }
       }
@@ -1587,9 +1587,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Arithmetic / logical
 #define FP_CONSTANT_BINOP(op, type, l, r, target, state) \
         bindLocal(target, state, \
-                  ref<Expr>(op(toConstant(state, l, "floating point").getConstantValue(), \
-                               toConstant(state, r, "floating point").getConstantValue(), \
-                               type), type))
+                  ConstantExpr::alloc(op(toConstant(state, l, "floating point").getConstantValue(), \
+                                         toConstant(state, r, "floating point").getConstantValue(), \
+                                         type), type))
   case Instruction::Add: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
     ref<Expr> left = eval(ki, 0, state).value;
@@ -1915,8 +1915,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::trunc(arg.getConstantValue(),
                                    resultType,
                                    arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1928,8 +1927,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::ext(arg.getConstantValue(),
                                  resultType,
                                  arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1941,8 +1939,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::toUnsignedInt(arg.getConstantValue(),
                                            resultType,
                                            arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1954,8 +1951,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::toSignedInt(arg.getConstantValue(),
                                          resultType,
                                          arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1966,8 +1962,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                "floating point");
     uint64_t value = floats::UnsignedIntToFP(arg.getConstantValue(),
                                              resultType);
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1979,8 +1974,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::SignedIntToFP(arg.getConstantValue(),
                                            resultType,
                                            arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -2088,8 +2082,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       }
     }
 
-    ref<Expr> result(ret, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(ret, resultType));
     break;
   }
 
@@ -2630,7 +2623,7 @@ void Executor::executeAlloc(ExecutionState &state,
     MemoryObject *mo = memory->allocate(size.getConstantValue(), isLocal, false,
                                         state.prevPC->inst);
     if (!mo) {
-      bindLocal(target, state, ref<Expr>(0, kMachinePointerType));
+      bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType));
     } else {
       ObjectState *os = bindObjectInState(state, mo, isLocal);
       if (zeroMemory) {
@@ -2665,8 +2658,8 @@ void Executor::executeAlloc(ExecutionState &state,
     
     // Try and start with a small example
     while (example.getConstantValue()>128) {
-      ref<Expr> tmp = ref<Expr>(example.getConstantValue() >> 1, 
-                                example.getWidth());
+      ref<Expr> tmp = ConstantExpr::alloc(example.getConstantValue() >> 1, 
+                                          example.getWidth());
       bool res;
       bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
       assert(success && "FIXME: Unhandled solver failure");      
@@ -2693,12 +2686,15 @@ void Executor::executeAlloc(ExecutionState &state,
       } else {
         // See if a *really* big value is possible. If so assume
         // malloc will fail for it, so lets fork and return 0.
-        StatePair hugeSize = fork(*fixedSize.second, 
-                                  UltExpr::create(ref<Expr>(1<<31, Expr::Int32), size), 
-                                  true);
+        StatePair hugeSize = 
+          fork(*fixedSize.second, 
+               UltExpr::create(ConstantExpr::alloc(1<<31, Expr::Int32),
+                               size), 
+               true);
         if (hugeSize.first) {
           klee_message("NOTE: found huge malloc, returing 0");
-          bindLocal(target, *hugeSize.first, ref<Expr>(0,kMachinePointerType));
+          bindLocal(target, *hugeSize.first, 
+                    ConstantExpr::alloc(0, kMachinePointerType));
         }
         
         if (hugeSize.second) {
@@ -3011,7 +3007,7 @@ void Executor::runFunctionAsMain(Function *f,
   assert(kf);
   Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
   if (ai!=ae) {
-    arguments.push_back(ref<Expr>(argc, Expr::Int32));
+    arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));
 
     if (++ai!=ae) {
       argvMO = memory->allocate((argc+1+envc+1+1) * kMachinePointerSize, false, true,
@@ -3108,7 +3104,7 @@ void Executor::getConstraintLog(const ExecutionState &state,
                                 std::string &res,
                                 bool asCVC) {
   if (asCVC) {
-    Query query(state.constraints, ref<Expr>(0, Expr::Bool));
+    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
     char *log = solver->stpSolver->getConstraintLog(query);
     res = std::string(log);
     free(log);
@@ -3155,7 +3151,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
     klee_warning("unable to compute initial values (invalid constraints?)!");
     ExprPPrinter::printQuery(std::cerr,
                              state.constraints, 
-                             ref<Expr>(0,Expr::Bool));
+                             ConstantExpr::alloc(0, Expr::Bool));
     return false;
   }
   
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 3b11dd42..62aa45db 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -37,7 +37,7 @@ ref<Expr>
 Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
   const llvm::Type *type = ce->getType();
 
-  ref<Expr> op1(0,Expr::Bool), op2(0,Expr::Bool), op3(0,Expr::Bool);
+  ref<Expr> op1(0), op2(0), op3(0);
   int numOperands = ce->getNumOperands();
 
   if (numOperands > 0) op1 = evalConstant(ce->getOperand(0));
@@ -80,7 +80,7 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
 
       for (gep_type_iterator ii = gep_type_begin(ce), ie = gep_type_end(ce);
            ii != ie; ++ii) {
-        ref<Expr> addend(0, kMachinePointerType);
+        ref<Expr> addend = ConstantExpr::alloc(0, kMachinePointerType);
         
         if (const StructType *st = dyn_cast<StructType>(*ii)) {
           const StructLayout *sl = kmodule->targetData->getStructLayout(st);
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 386c8d80..1de47d0c 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -239,8 +239,9 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
   for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(), 
          ie = reads.end(); i != ie; ++i) {
     ReadExpr *re = i->get();
-    ref<Expr> size = ref<Expr>(re->updates.root->size, kMachinePointerType);
-    assumption.push_back(UltExpr::create(re->index, size));
+    assumption.push_back(UltExpr::create(re->index, 
+                                         ConstantExpr::alloc(re->updates.root->size, 
+                                                             kMachinePointerType)));
   }
 
   ConstraintManager assume(assumption);
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 0f09b162..cfb4ab43 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -118,7 +118,7 @@ public:
 
   ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
     if (size==0) {
-      return EqExpr::create(offset, ref<Expr>(0, kMachinePointerType));
+      return EqExpr::create(offset, ConstantExpr::alloc(0, kMachinePointerType));
     } else {
       return UltExpr::create(offset, getSizeExpr());
     }
@@ -126,9 +126,9 @@ public:
   ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
     if (bytes<=size) {
       return UltExpr::create(offset, 
-                             ref<Expr>(size - bytes + 1, kMachinePointerType));
+                             ConstantExpr::alloc(size - bytes + 1, kMachinePointerType));
     } else {
-      return ref<Expr>(0, Expr::Bool);
+      return ConstantExpr::alloc(0, Expr::Bool);
     }
   }
 };
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index e6d88bac..9369dcbc 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -88,12 +88,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     const Array *array = it->first;
     unsigned i = it->second;
     ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
-                                      ref<Expr>(i, Expr::Int32));
+                                      ConstantExpr::alloc(i, Expr::Int32));
     
     // If not in bindings then this can't be a violation?
     Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
     if (it2 != assignment.bindings.end()) {
-      ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8));
+      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -102,7 +102,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it2->second[i] = value.getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8)));
+        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }
@@ -122,8 +122,8 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     const Array *array = it->first;
     for (unsigned i=0; i<array->size; ++i) {
       ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
-                                        ref<Expr>(i, Expr::Int32));
-      ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8));
+                                        ConstantExpr::alloc(i, Expr::Int32));
+      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -132,7 +132,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it->second[i] = value.getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8)));
+        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 3f7c442e..9f5a2347 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -386,7 +386,7 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
 
   ref<Expr> cond = arguments[1];
   if (cond.getWidth() != Expr::Bool)
-    cond = NeExpr::create(cond, ref<Expr>(0, cond.getWidth()));
+    cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond.getWidth()));
 
   Executor::ExactResolutionList rl;
   executor.resolveExact(state, arguments[0], rl, "prefex_cex");
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 70e42836..4c09a1aa 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -130,7 +130,7 @@ TimingSolver::getInitialValues(const ExecutionState& state,
   sys::Process::GetTimeUsage(now,user,sys);
 
   bool success = solver->getInitialValues(Query(state.constraints,
-                                                ref<Expr>(0, Expr::Bool)), 
+                                                ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
   sys::Process::GetTimeUsage(delta,user,sys);
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 03:38:46 +0000