Merge branch 'master' of https://github.com/hpalikareva/klee into hpalikareva-master

4 files changed, 30 insertions, 35 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d0ad811d..b57b1956 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -189,7 +189,7 @@ namespace {
 
   cl::opt<double>
   MaxInstructionTime("max-instruction-time",
-                     cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-stp"),
+                     cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-solver"),
                      cl::init(0));
   
   cl::opt<double>
@@ -221,16 +221,6 @@ namespace {
   MaxMemoryInhibit("max-memory-inhibit",
             cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=on)"),
             cl::init(true));
-
-  cl::opt<bool>
-  UseForkedSTP("use-forked-stp",
-	       cl::desc("Run STP in a forked process (default=off)"));
-
-  cl::opt<bool>
-  STPOptimizeDivides("stp-optimize-divides", 
-                 cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"),
-                 cl::init(true));
-
 }
 
 
@@ -258,19 +248,20 @@ Executor::Executor(const InterpreterOptions &opts,
     inhibitForking(false),
     haltExecution(false),
     ivcEnabled(false),
-    stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0
-      ? std::min(MaxSTPTime,MaxInstructionTime)
-      : std::max(MaxSTPTime,MaxInstructionTime)) {
-  if (stpTimeout) UseForkedSTP = true;
-  STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
+    coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
+      ? std::min(MaxCoreSolverTime,MaxInstructionTime)
+      : std::max(MaxCoreSolverTime,MaxInstructionTime)) {
+      
+  if (coreSolverTimeout) UseForkedCoreSolver = true;
+  Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);  
   Solver *solver = 
-    constructSolverChain(stpSolver,
+    constructSolverChain(coreSolver,
                          interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
                          interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
                          interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME),
                          interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME));
   
-  this->solver = new TimingSolver(solver, stpSolver);
+  this->solver = new TimingSolver(solver);
 
   memory = new MemoryManager();
 }
@@ -666,7 +657,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     }
   }
 
-  double timeout = stpTimeout;
+  double timeout = coreSolverTimeout;
   if (isSeeding)
     timeout *= it->second.size();
   solver->setTimeout(timeout);
@@ -982,7 +973,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
     ref<ConstantExpr> value;
     bool isTrue = false;
 
-    solver->setTimeout(stpTimeout);      
+    solver->setTimeout(coreSolverTimeout);      
     if (solver->getValue(state, e, value) &&
         solver->mustBeTrue(state, EqExpr::create(e, value), isTrue) &&
         isTrue)
@@ -2979,7 +2970,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   // fast path: single in-bounds resolution
   ObjectPair op;
   bool success;
-  solver->setTimeout(stpTimeout);
+  solver->setTimeout(coreSolverTimeout);
   if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
     address = toConstant(state, address, "resolveOne failure");
     success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
@@ -2996,7 +2987,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     ref<Expr> offset = mo->getOffsetExpr(address);
 
     bool inBounds;
-    solver->setTimeout(stpTimeout);
+    solver->setTimeout(coreSolverTimeout);
     bool success = solver->mustBeTrue(state, 
                                       mo->getBoundsCheckOffset(offset, bytes),
                                       inBounds);
@@ -3035,9 +3026,9 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   // resolution with out of bounds)
   
   ResolutionList rl;  
-  solver->setTimeout(stpTimeout);
+  solver->setTimeout(coreSolverTimeout);
   bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
-                                               0, stpTimeout);
+                                               0, coreSolverTimeout);
   solver->setTimeout(0);
   
   // XXX there is some query wasteage here. who cares?
@@ -3290,7 +3281,7 @@ void Executor::getConstraintLog(const ExecutionState &state,
   case STP:
   {
 	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-	  char *log = solver->stpSolver->getConstraintLog(query);
+	  char *log = solver->getConstraintLog(query);
 	  res = std::string(log);
 	  free(log);
   }
@@ -3328,7 +3319,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
                                    std::pair<std::string,
                                    std::vector<unsigned char> > >
                                    &res) {
-  solver->setTimeout(stpTimeout);
+  solver->setTimeout(coreSolverTimeout);
 
   ExecutionState tmp(state);
   if (!NoPreferCex) {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index c434c34c..a9d6b791 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -173,8 +173,9 @@ private:
   /// false, it is buggy (it needs to validate its writes).
   bool ivcEnabled;
 
-  /// The maximum time to allow for a single stp query.
-  double stpTimeout;  
+  /// The maximum time to allow for a single core solver query.
+  /// (e.g. for a single STP query)
+  double coreSolverTimeout; 
 
   llvm::Function* getTargetFunction(llvm::Value *calledVal,
                                     ExecutionState &state);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 7b3655f8..08c95d48 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -110,6 +110,7 @@ ObjectState::ObjectState(const MemoryObject *mo)
     const Array *array = new Array("tmp_arr" + llvm::utostr(++id), size);
     updates = UpdateList(array, 0);
   }
+  memset(concreteStore, 0, size);
 }
 
 
@@ -126,6 +127,7 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
     readOnly(false) {
   mo->refCount++;
   makeSymbolic();
+  memset(concreteStore, 0, size);
 }
 
 ObjectState::ObjectState(const ObjectState &os) 
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index b13879df..c98dd881 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -17,15 +17,13 @@
 
 namespace klee {
   class ExecutionState;
-  class Solver;
-  class STPSolver;
+  class Solver;  
 
   /// TimingSolver - A simple class which wraps a solver and handles
   /// tracking the statistics that we care about.
   class TimingSolver {
   public:
     Solver *solver;
-    STPSolver *stpSolver;
     bool simplifyExprs;
 
   public:
@@ -34,15 +32,18 @@ namespace klee {
     /// \param _simplifyExprs - Whether expressions should be
     /// simplified (via the constraint manager interface) prior to
     /// querying.
-    TimingSolver(Solver *_solver, STPSolver *_stpSolver, 
-                 bool _simplifyExprs = true) 
-      : solver(_solver), stpSolver(_stpSolver), simplifyExprs(_simplifyExprs) {}
+    TimingSolver(Solver *_solver, bool _simplifyExprs = true) 
+      : solver(_solver), simplifyExprs(_simplifyExprs) {}
     ~TimingSolver() {
       delete solver;
     }
 
     void setTimeout(double t) {
-      stpSolver->setTimeout(t);
+      solver->setCoreSolverTimeout(t);
+    }
+    
+    char *getConstraintLog(const Query& query) {
+      return solver->getConstraintLog(query);
     }
 
     bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);