fix: Fix the cover-error-call tests

include/klee/Module/KModule.h

@@ -352,8 +352,7 @@ class KModule {
   /// @param forceSourceOutput true if assembly.ll should be created
   ///
   // FIXME: ihandler should not be here
-  void manifest(InterpreterHandler *ih, Interpreter::GuidanceKind guidance,
-                bool forceSourceOutput);
+  void manifest(InterpreterHandler *ih, bool forceSourceOutput);
 
   /// Link the provided modules together as one KLEE module.
   ///

lib/Core/Executor.cpp

@@ -681,8 +681,7 @@ llvm::Module *Executor::setModule(
   // 4.) Manifest the module
   std::swap(kmodule->mainModuleFunctions, mainModuleFunctions);
   std::swap(kmodule->mainModuleGlobals, mainModuleGlobals);
-  kmodule->manifest(interpreterHandler, interpreterOpts.Guidance,
-                    StatsTracker::useStatistics());
+  kmodule->manifest(interpreterHandler, StatsTracker::useStatistics());
 
   kmodule->origInstructions = origInstructions;
 
@@ -7385,8 +7384,8 @@ void Executor::setInitializationGraph(
   return;
 }
 
-bool isReproducible(const klee::Symbolic &symb) {
-  auto arr = symb.array;
+bool isReproducible(const klee::Array *array) {
+  auto arr = array;
   bool bad = IrreproducibleSource::classof(arr->source.get());
   if (auto liSource = dyn_cast<LazyInitializationSource>(arr->source.get())) {
     std::vector<const Array *> arrays;
@@ -7402,6 +7401,10 @@ bool isReproducible(const klee::Symbolic &symb) {
   return !bad;
 }
 
+bool isIrreproducible(const klee::Array *array) {
+  return !isReproducible(array);
+}
+
 bool isUninitialized(const klee::Array *array) {
   bool bad = isa<UninitializedSource>(array->source);
   if (bad)
@@ -7411,7 +7414,11 @@ bool isUninitialized(const klee::Array *array) {
   return bad;
 }
 
-bool isMakeSymbolic(const klee::Symbolic &symb) {
+bool isReproducibleSymbol(const klee::Symbolic &symb) {
+  return isReproducible(symb.array);
+}
+
+bool isMakeSymbolicSymbol(const klee::Symbolic &symb) {
   auto array = symb.array;
   bool good = isa<MakeSymbolicSource>(array->source);
   if (!good)
@@ -7462,20 +7469,23 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
   std::vector<const Array *> uninitObjects;
   std::copy_if(allObjects.begin(), allObjects.end(),
                std::back_inserter(uninitObjects), isUninitialized);
+  std::vector<const Array *> irreproducibleObjects;
+  std::copy_if(allObjects.begin(), allObjects.end(),
+               std::back_inserter(irreproducibleObjects), isIrreproducible);
 
   std::vector<klee::Symbolic> symbolics;
 
   if (OnlyOutputMakeSymbolicArrays) {
     std::copy_if(state.symbolics.begin(), state.symbolics.end(),
-                 std::back_inserter(symbolics), isMakeSymbolic);
+                 std::back_inserter(symbolics), isMakeSymbolicSymbol);
   } else {
     std::copy_if(state.symbolics.begin(), state.symbolics.end(),
-                 std::back_inserter(symbolics), isReproducible);
+                 std::back_inserter(symbolics), isReproducibleSymbol);
   }
 
   // we cannot be sure that an irreproducible state proves the presence of an
   // error
-  if (uninitObjects.size() > 0 || state.symbolics.size() != symbolics.size()) {
+  if (uninitObjects.size() > 0 || irreproducibleObjects.size() > 0) {
     state.error = ReachWithError::None;
   } else if (FunctionCallReproduce != "" &&
              state.error == ReachWithError::Reachable) {

lib/Core/MockBuilder.cpp

@@ -232,7 +232,7 @@ void MockBuilder::buildExternalGlobalsDefinitions() {
     global->setInitializer(zeroInitializer);
     global->setDSOLocal(true);
     auto *localPointer = builder->CreateAlloca(elementType, nullptr);
-    buildCallKleeMakeSymbolic("klee_make_symbolic", localPointer, elementType,
+    buildCallKleeMakeSymbolic("klee_make_mock", localPointer, elementType,
                               "external_" + extName);
     llvm::Value *localValue = builder->CreateLoad(elementType, localPointer);
     builder->CreateStore(localValue, global);

lib/Module/KModule.cpp

@@ -265,9 +265,7 @@ buildInstructionToLineMap(const llvm::Module &m,
   return a.getMapping();
 }
 
-void KModule::manifest(InterpreterHandler *ih,
-                       Interpreter::GuidanceKind guidance,
-                       bool forceSourceOutput) {
+void KModule::manifest(InterpreterHandler *ih, bool forceSourceOutput) {
 
   if (OutputModule) {
     std::unique_ptr<llvm::raw_fd_ostream> f(ih->openOutputFile("final.bc"));
@@ -334,9 +332,7 @@ void KModule::manifest(InterpreterHandler *ih,
       if (isa<InlineAsm>(cs.getCalledOperand())) {
         isInlineAsm = true;
       }
-      if (kcb->calledFunctions.empty() && !isInlineAsm &&
-          (guidance != Interpreter::GuidanceKind::ErrorGuidance ||
-           !inMainModule(*kfp->function()))) {
+      if (kcb->calledFunctions.empty() && !isInlineAsm) {
         kcb->calledFunctions.insert(escapingFunctions.begin(),
                                     escapingFunctions.end());
       }

scripts/kleef

@@ -61,6 +61,9 @@ def klee_options(
         #  "--search=nurs:covnew",
         #  "--search=nurs:md2u", "--search=random-path",
         #  "-const-array-opt",
+        "--use-batching-search",
+        "--batch-instructions=10000",
+        "--batch-time=0",
         "--only-output-make-symbolic-arrays",
         "--memory-backend=mixed",
         "--max-fixed-size-structures-size=64",
@@ -189,6 +192,7 @@ class KLEEF(object):
         use_perf=False,
         use_valgrind=False,
         write_ktests=False,
+        debug=False,
     ):
         self.source = Path(source) if source else None
         self.is32 = is32
@@ -204,6 +208,7 @@ class KLEEF(object):
             self.write_ktests = "true"
         else:
             self.write_ktests = "false"
+        self.debug = debug
 
         # This file is inside the bin directory - use the root as base
         self.bin_directory = Path(__file__).parent
@@ -213,15 +218,21 @@ class KLEEF(object):
         self.linker_path = tryFind(self.bin_directory, "llvm-link")
         self.library_path = self.base_directory / "libraries"
         self.runtime_library_path = self.base_directory / "runtime/lib"
-        self.test_results_path = Path.cwd() / "test-suite"
+        if self.debug:
+            self.test_results_path = Path.cwd() / self.source.name
+        else:
+            self.test_results_path = Path.cwd() / "test-suite"
         self.test_results_path.mkdir(exist_ok=True)
 
         self.callEnv = os.environ.copy()
         self.callEnv["LD_LIBRARY_PATH"] = self.library_path
         self.callEnv["KLEE_RUNTIME_LIBRARY_PATH"] = self.runtime_library_path
 
     def compile(self):
-        self.tempdir = Path(tempfile.mkdtemp())
+        if self.debug:
+            self.tempdir = Path.cwd()
+        else:
+            self.tempdir = Path(tempfile.mkdtemp())
 
         # Compile file for testing
         self.compiled_file = self.tempdir / (self.source.name + ".bc")
@@ -407,6 +418,7 @@ def run(args):
         use_perf=args.perf,
         use_valgrind=args.valgrind,
         write_ktests=args.write_ktests,
+        debug=args.debug,
     )
     wrapper.compile()
     return wrapper.run()
@@ -433,6 +445,12 @@ def main():
         action="store_true",
         default=False,
     )
+    parser.add_argument(
+        "--debug",
+        help="to use for testing",
+        action="store_true",
+        default=False,
+    )
     parser.add_argument(
         "--coverage-only", help="Focus on coverage", action="store_true"
     )

test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c

@@ -1,7 +1,7 @@
 // It requires bitwuzla because the script currently runs with bitwuzla solver backend
 // REQUIRES: bitwuzla
 // REQUIRES: target-x86_64
-// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 --write-ktests %s 2>&1 | FileCheck %s
+// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 --debug %s 2>&1 | FileCheck %s
 // CHECK: KLEE: WARNING: 100.00% Reachable Reachable
 
 // This file is part of the SV-Benchmarks collection of verification tasks: