[fix] Tests for states with mocks

UnitTestBot · Oct 3, 2023 · 621aadf · 621aadf
1 parent 390866f
commit 621aadf
Show file tree

Hide file tree

Showing 5 changed files with 35 additions and 8 deletions.
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
@@ -57,7 +57,7 @@ class InterpreterHandler {
   virtual void incPathsCompleted() = 0;
   virtual void incPathsExplored(std::uint32_t num = 1) = 0;
 
-  virtual void processTestCase(const ExecutionState &state, const char *message,
+  virtual void processTestCase(ExecutionState &state, const char *message,
                                const char *suffix, bool isError = false) = 0;
 };
 
@@ -187,7 +187,7 @@ class Interpreter {
   virtual void getConstraintLog(const ExecutionState &state, std::string &res,
                                 LogType logFormat = STP) = 0;
 
-  virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 0;
+  virtual bool getSymbolicSolution(ExecutionState &state, KTest &res) = 0;
 
   virtual void logState(const ExecutionState &state, int id,
                         std::unique_ptr<llvm::raw_fd_ostream> &f) = 0;

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -7081,7 +7081,17 @@ Assignment Executor::computeConcretization(const ConstraintSet &constraints,
   return concretization;
 }
 
-bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
+bool isIrreproducible(const klee::Symbolic &symb) {
+  auto arr = symb.array;
+  bool bad = IrreproducibleSource::classof(arr->source.get());
+  if (bad)
+    klee_warning_once(arr->source.get(),
+                      "A irreproducible symbolic %s reaches a test",
+                      arr->getIdentifier().c_str());
+  return bad;
+}
+
+bool Executor::getSymbolicSolution(ExecutionState &state, KTest &res) {
   solver->setTimeout(coreSolverTimeout);
 
   PathConstraints extendedConstraints(state.constraints);
@@ -7117,6 +7127,10 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     }
   }
 
+  state.symbolics.erase(std::remove_if(state.symbolics.begin(),
+                                       state.symbolics.end(), isIrreproducible),
+                        state.symbolics.end());
+
   std::vector<SparseStorage<unsigned char>> values;
   std::vector<const Array *> objects;
   for (unsigned i = 0; i != state.symbolics.size(); ++i)

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
@@ -798,7 +798,7 @@ class Executor : public Interpreter {
   void logState(const ExecutionState &state, int id,
                 std::unique_ptr<llvm::raw_fd_ostream> &f) override;
 
-  bool getSymbolicSolution(const ExecutionState &state, KTest &res) override;
+  bool getSymbolicSolution(ExecutionState &state, KTest &res) override;
 
   void getCoveredLines(
       const ExecutionState &state,

diff --git a/test/regression/2023-10-02-test-from-mocked-global.c b/test/regression/2023-10-02-test-from-mocked-global.c
@@ -0,0 +1,14 @@
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --mock-all-externals --write-xml-tests --output-dir=%t.klee-out %t1.bc
+// RUN: FileCheck --input-file %t.klee-out/test000001.xml %s
+
+extern void *__crc_mc44s803_attach __attribute__((__weak__));
+static unsigned long const __kcrctab_mc44s803_attach __attribute__((__used__, __unused__,
+                                                                    __section__("___kcrctab+mc44s803_attach"))) = (unsigned long const)((unsigned long)(&__crc_mc44s803_attach));
+
+int main() {
+  return 0;
+}
+
+// CHECK-NOT: <input
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
@@ -406,7 +406,7 @@ class KleeHandler : public InterpreterHandler {
 
   void setInterpreter(Interpreter *i);
 
-  void processTestCase(const ExecutionState &state, const char *message,
+  void processTestCase(ExecutionState &state, const char *message,
                        const char *suffix, bool isError = false);
 
   void writeTestCaseXML(bool isError, const KTest &out, unsigned id);
@@ -575,9 +575,8 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id) {
 }
 
 /* Outputs all files (.ktest, .kquery, .cov etc.) describing a test case */
-void KleeHandler::processTestCase(const ExecutionState &state,
-                                  const char *message, const char *suffix,
-                                  bool isError) {
+void KleeHandler::processTestCase(ExecutionState &state, const char *message,
+                                  const char *suffix, bool isError) {
   unsigned id = ++m_numTotalTests;
   if (!WriteNone &&
       (FunctionCallReproduce == "" || strcmp(suffix, "assert.err") == 0 ||