tc

include/klee-test-comp.c

@@ -82,7 +82,7 @@ unsigned long __VERIFIER_nondet_ulong(void) {
 }
 
 double __VERIFIER_nondet_double(void) {
-  long x;
+  double x;
   klee_make_symbolic(&x, sizeof(x), "double");
   return x;
 }
@@ -96,7 +96,7 @@ void *__VERIFIER_nondet_pointer(void) {
 }
 
 float __VERIFIER_nondet_float(void) {
-  int x;
+  float x;
   klee_make_symbolic(&x, sizeof(x), "float");
   return x;
 }

include/klee/Module/Target.h

@@ -41,6 +41,9 @@ struct ErrorLocation {
   unsigned int endLine;
   optional<unsigned int> startColumn;
   optional<unsigned int> endColumn;
+
+  ErrorLocation(const klee::ref<klee::Location> &loc);
+  ErrorLocation(const KInstruction *ki);
 };
 
 class ReproduceErrorTarget;

include/klee/Support/OptionCategories.h

@@ -21,6 +21,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 DISABLE_WARNING_POP
 
 namespace klee {
+extern llvm::cl::OptionCategory TestCompCat;
 extern llvm::cl::OptionCategory ExecCat;
 extern llvm::cl::OptionCategory DebugCat;
 extern llvm::cl::OptionCategory ExecCat;

lib/Core/ExecutionState.cpp

@@ -114,15 +114,8 @@ StackFrame::StackFrame(const StackFrame &s)
 
 StackFrame::~StackFrame() { delete[] locals; }
 
-CallStackFrame::CallStackFrame(const CallStackFrame &s)
-    : caller(s.caller), kf(s.kf) {}
-
 InfoStackFrame::InfoStackFrame(KFunction *kf) : kf(kf) {}
 
-InfoStackFrame::InfoStackFrame(const InfoStackFrame &s)
-    : kf(s.kf), callPathNode(s.callPathNode),
-      minDistToUncoveredOnReturn(s.minDistToUncoveredOnReturn) {}
-
 /***/
 ExecutionState::ExecutionState()
     : initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1),

lib/Core/ExecutionState.h

@@ -68,7 +68,6 @@ struct CallStackFrame {
   CallStackFrame(KInstIterator caller_, KFunction *kf_)
       : caller(caller_), kf(kf_) {}
   ~CallStackFrame() = default;
-  CallStackFrame(const CallStackFrame &s);
 
   bool equals(const CallStackFrame &other) const;
 
@@ -105,7 +104,6 @@ struct InfoStackFrame {
   unsigned minDistToUncoveredOnReturn = 0;
 
   InfoStackFrame(KFunction *kf);
-  InfoStackFrame(const InfoStackFrame &s);
   ~InfoStackFrame() = default;
 };
 

lib/Core/Executor.cpp

@@ -217,6 +217,10 @@ llvm::cl::opt<unsigned> MinNumberElementsLazyInit(
                    "initialization (default 4)"),
     llvm::cl::init(4), llvm::cl::cat(LazyInitCat));
 
+cl::opt<std::string> FunctionCallReproduce(
+    "function-call-reproduce", cl::init(""),
+    cl::desc("Marks mentioned function as target for error-guided mode."),
+    cl::cat(ExecCat));
 } // namespace klee
 
 namespace {
@@ -509,10 +513,6 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                                                 EqualitySubstitution);
   initializeSearchOptions();
 
-  if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats())
-    klee_error("To use --only-output-states-covering-new, you need to enable "
-               "--output-istats.");
-
   if (DebugPrintInstructions.isSet(FILE_ALL) ||
       DebugPrintInstructions.isSet(FILE_COMPACT) ||
       DebugPrintInstructions.isSet(FILE_SRC)) {
@@ -585,6 +585,13 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
   preservedFunctions.push_back("memcmp");
   preservedFunctions.push_back("memmove");
 
+  if (FunctionCallReproduce != "") {
+    // prevent elimination of the function
+    auto f = kmodule->module->getFunction(FunctionCallReproduce);
+    if (f)
+      f->addFnAttr(Attribute::OptimizeNone);
+  }
+
   kmodule->optimiseAndPrepare(opts, preservedFunctions);
   kmodule->checkModule();
 
@@ -6635,7 +6642,8 @@ void Executor::clearMemory() {
 
 void Executor::runFunctionAsMain(Function *f, int argc, char **argv,
                                  char **envp) {
-  if (guidanceKind == GuidanceKind::ErrorGuidance &&
+  if (FunctionCallReproduce == "" &&
+      guidanceKind == GuidanceKind::ErrorGuidance &&
       (!interpreterOpts.Paths.has_value() || interpreterOpts.Paths->empty())) {
     klee_warning("No targets found in error-guided mode");
     return;
@@ -6646,9 +6654,26 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv,
   std::vector<ExecutionState *> states;
 
   if (guidanceKind == GuidanceKind::ErrorGuidance) {
-    auto &paths = interpreterOpts.Paths.value();
-    auto prepTargets = targetedExecutionManager->prepareTargets(
-        kmodule.get(), std::move(paths));
+    std::map<klee::KFunction *, klee::ref<klee::TargetForest>,
+             klee::TargetedExecutionManager::KFunctionLess>
+        prepTargets;
+    if (FunctionCallReproduce == "") {
+      auto &paths = interpreterOpts.Paths.value();
+      prepTargets = targetedExecutionManager->prepareTargets(kmodule.get(),
+                                                             std::move(paths));
+    } else {
+      /* Find all calls to function specified in .prp file
+       * and combine them to single target forest */
+      KFunction *kEntryFunction = kmodule->functionMap.at(f);
+      ref<TargetForest> forest = new TargetForest(kEntryFunction);
+      auto kfunction = kmodule->functionNameMap.at(FunctionCallReproduce);
+      KBlock *kCallBlock = kfunction->entryKBlock;
+      forest->add(ReproduceErrorTarget::create(
+          {ReachWithError::Reachable}, "",
+          ErrorLocation(kCallBlock->getFirstInstruction()), kCallBlock));
+      prepTargets.emplace(kEntryFunction, forest);
+    }
+
     if (prepTargets.empty()) {
       klee_warning(
           "No targets found in error-guided mode after prepare targets");

lib/Expr/Expr.cpp

@@ -1635,21 +1635,6 @@ ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
     if (ConstantExpr *rCE = dyn_cast<ConstantExpr>(r))
       return lCE->Concat(rCE);
 
-  if (isa<SelectExpr>(l) || isa<SelectExpr>(r)) {
-    if (SelectExpr *se = dyn_cast<SelectExpr>(l)) {
-      if (isa<ConstantExpr>(se->trueExpr)) {
-        return SelectExpr::create(se->cond, ConcatExpr::create(se->trueExpr, r),
-                                  ConcatExpr::create(se->falseExpr, r));
-      }
-    }
-    if (SelectExpr *se = dyn_cast<SelectExpr>(r)) {
-      if (isa<ConstantExpr>(se->trueExpr)) {
-        return SelectExpr::create(se->cond, ConcatExpr::create(l, se->trueExpr),
-                                  ConcatExpr::create(l, se->falseExpr));
-      }
-    }
-  }
-
   // Merge contiguous Extracts
   if (ExtractExpr *ee_left = dyn_cast<ExtractExpr>(l)) {
     if (ExtractExpr *ee_right = dyn_cast<ExtractExpr>(r)) {
@@ -1707,11 +1692,6 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
   } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     return CE->Extract(off, w);
   } else if (SelectExpr *se = dyn_cast<SelectExpr>(expr)) {
-    if (isa<ConstantExpr>(se->trueExpr)) {
-      return SelectExpr::create(se->cond,
-                                ExtractExpr::create(se->trueExpr, off, w),
-                                ExtractExpr::create(se->falseExpr, off, w));
-    }
   } else {
     // Extract(Concat)
     if (ConcatExpr *ce = dyn_cast<ConcatExpr>(expr)) {

lib/Module/Target.cpp

@@ -26,6 +26,15 @@ llvm::cl::opt<bool> LocationAccuracy(
     cl::desc("Check location with line and column accuracy (default=false)"));
 }
 
+ErrorLocation::ErrorLocation(const klee::ref<klee::Location> &loc)
+    : startLine(loc->startLine), endLine(loc->endLine),
+      startColumn(loc->startColumn), endColumn(loc->endColumn) {}
+
+ErrorLocation::ErrorLocation(const KInstruction *ki) {
+  startLine = (endLine = ki->info->line);
+  startColumn = (endColumn = ki->info->line);
+}
+
 std::string ReproduceErrorTarget::toString() const {
   std::ostringstream repr;
   repr << "Target " << getId() << ": ";

lib/Module/TargetForest.cpp

@@ -117,11 +117,8 @@ void TargetForest::Layer::addTrace(
     for (auto block : it->second) {
       ref<Target> target = nullptr;
       if (i == result.locations.size() - 1) {
-        target = ReproduceErrorTarget::create(
-            result.errors, result.id,
-            ErrorLocation{loc->startLine, loc->endLine, loc->startColumn,
-                          loc->endColumn},
-            block);
+        target = ReproduceErrorTarget::create(result.errors, result.id,
+                                              ErrorLocation(loc), block);
       } else {
         target = ReachBlockTarget::create(block);
       }

lib/Solver/CoreSolver.cpp

@@ -28,7 +28,11 @@ DISABLE_WARNING_POP
 namespace klee {
 
 std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) {
-  bool isTreeSolver = false;
+  bool isTreeSolver = cst == Z3_TREE_SOLVER;
+  if (!isTreeSolver && MaxSolversApproxTreeInc > 0)
+    klee_warning("--%s option is ignored because --%s is not z3-tree",
+                 MaxSolversApproxTreeInc.ArgStr.str().c_str(),
+                 CoreSolverToUse.ArgStr.str().c_str());
   switch (cst) {
   case STP_SOLVER:
 #ifdef ENABLE_STP
@@ -56,7 +60,6 @@ std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) {
   case DUMMY_SOLVER:
     return createDummySolver();
   case Z3_TREE_SOLVER:
-    isTreeSolver = true;
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
     klee_message("Using Z3 solver backend");
@@ -68,8 +71,12 @@ std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) {
     klee_message("Using Z3 core builder");
     type = KLEE_CORE;
 #endif
-    if (isTreeSolver)
-      return std::make_unique<Z3TreeSolver>(type, MaxSolversApproxTreeInc);
+    if (isTreeSolver) {
+      if (MaxSolversApproxTreeInc > 0)
+        return std::make_unique<Z3TreeSolver>(type, MaxSolversApproxTreeInc);
+      klee_warning("--%s is 0, so falling back to non tree-incremental solver",
+                   MaxSolversApproxTreeInc.ArgStr.str().c_str());
+    }
     return std::make_unique<Z3Solver>(type);
 #else
     klee_message("Not compiled with Z3 support");

lib/Solver/IndependentSolver.cpp

@@ -218,7 +218,6 @@ bool IndependentSolver::computeInitialValues(
       // satisfy the query.
       ref<ConstantExpr> arrayConstantSize =
           dyn_cast<ConstantExpr>(retMap.evaluate(arr->size));
-      arrayConstantSize->dump();
       assert(arrayConstantSize &&
              "Array of symbolic size had not receive value for size!");
       SparseStorage<unsigned char> ret(arrayConstantSize->getZExtValue());