Small fixes

include/klee/Expr/AlphaBuilder.h

@@ -16,7 +16,7 @@
 
 namespace klee {
 
-class AlphaBuilder : public ExprVisitor {
+class AlphaBuilder final : public ExprVisitor {
 public:
   ExprHashMap<ref<Expr>> reverseExprMap;
   ArrayCache::ArrayHashMap<const Array *> reverseAlphaArrayMap;
@@ -28,7 +28,8 @@ class AlphaBuilder : public ExprVisitor {
 
   const Array *visitArray(const Array *arr);
   UpdateList visitUpdateList(UpdateList u);
-  Action visitRead(const ReadExpr &re);
+  Action visitRead(const ReadExpr &re) override;
+  using ExprVisitor::visitExpr;
 
 public:
   AlphaBuilder(ArrayCache &_arrayCache);

include/klee/Expr/Expr.h

@@ -304,8 +304,8 @@ class Expr {
   std::string toString() const;
 
   /// Returns the pre-computed hash of the current expression
-  virtual unsigned hash() const { return hashValue; }
-  virtual unsigned height() const { return heightValue; }
+  unsigned hash() const { return hashValue; }
+  unsigned height() const { return heightValue; }
 
   /// (Re)computes the hash of the current expression.
   /// Returns the hash value.

lib/Core/Executor.cpp

@@ -249,10 +249,10 @@ cl::opt<bool> CoverOnTheFly(
              "(default=false, i.e. one per (error,instruction) pair)"),
     cl::cat(TestGenCat));
 
-cl::opt<unsigned> DelayCoverOnTheFly(
-    "delay-cover-on-the-fly", cl::init(10000),
-    cl::desc("Start on the fly tests generation after this many instructions "
-             "(default=10000)"),
+cl::opt<std::string> DelayCoverOnTheFly(
+    "delay-cover-on-the-fly", cl::init("0s"),
+    cl::desc("Start on the fly tests generation after the specified duration. "
+             "Set to 0s to disable (default=0s)"),
     cl::cat(TestGenCat));
 
 cl::opt<unsigned> UninitMemoryTestMultiplier(
@@ -487,15 +487,23 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       targetedExecutionManager(
           new TargetedExecutionManager(*codeGraphInfo, *targetManager)),
       replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false),
-      inhibitForking(false), haltExecution(HaltExecution::NotHalt),
-      ivcEnabled(false), debugLogBuffer(debugBufferString) {
+      inhibitForking(false), coverOnTheFly(false),
+      haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
+      debugLogBuffer(debugBufferString) {
   const time::Span maxTime{MaxTime};
   if (maxTime)
     timers.add(std::make_unique<Timer>(maxTime, [&] {
       klee_message("HaltTimer invoked");
       setHaltExecution(HaltExecution::MaxTime);
     }));
 
+  if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance) {
+    const time::Span delayTime{DelayCoverOnTheFly};
+    if (delayTime)
+      timers.add(
+          std::make_unique<Timer>(delayTime, [&] { coverOnTheFly = true; }));
+  }
+
   coreSolverTimeout = time::Span{MaxCoreSolverTime};
   if (coreSolverTimeout)
     UseForkedCoreSolver = true;
@@ -4381,8 +4389,8 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
 
 void Executor::executeStep(ExecutionState &state) {
   KFunction *initKF = state.initPC->parent->parent;
-  if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance &&
-      stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) {
+
+  if (coverOnTheFly && shouldWriteTest(state)) {
     state.clearCoveredNew();
     interpreterHandler->processTestCase(
         state, nullptr,

lib/Core/Executor.h

@@ -208,6 +208,9 @@ class Executor : public Interpreter {
   /// Disables forking, set by client. \see setInhibitForking()
   bool inhibitForking;
 
+  /// Should it generate test cases for each new covered block or branch
+  bool coverOnTheFly;
+
   /// Signals the executor to halt execution at the next instruction
   /// step.
   HaltExecution::Reason haltExecution = HaltExecution::NotHalt;

lib/Expr/Constraints.cpp

@@ -423,27 +423,23 @@ Simplificator::simplifyExpr(const constraints_ty &constraints,
 
   for (auto &constraint : constraints) {
     if (const EqExpr *ee = dyn_cast<EqExpr>(constraint)) {
-      ref<Expr> left = ee->left;
-      ref<Expr> right = ee->right;
-      if (right->height() < left->height()) {
-        left = ee->right;
-        right = ee->left;
-      }
-      if (isa<ConstantExpr>(ee->left)) {
-        equalities.insert(std::make_pair(ee->right, ee->left));
-        equalitiesParents.insert({ee->right, constraint});
-      } else {
-        equalities.insert(std::make_pair(constraint, Expr::createTrue()));
-        equalities.insert(std::make_pair(right, left));
-        equalitiesParents.insert({constraint, constraint});
-        equalitiesParents.insert({right, constraint});
+      ref<Expr> small = ee->left;
+      ref<Expr> big = ee->right;
+      if (!isa<ConstantExpr>(small)) {
+        auto hr = big->height(), hl = small->height();
+        if (hr < hl || (hr == hl && big < small))
+          std::swap(small, big);
+        equalities.emplace(constraint, Expr::createTrue());
+        equalitiesParents.emplace(constraint, constraint);
       }
+      equalities.emplace(big, small);
+      equalitiesParents.emplace(big, constraint);
     } else {
-      equalities.insert(std::make_pair(constraint, Expr::createTrue()));
-      equalitiesParents.insert({constraint, constraint});
+      equalities.emplace(constraint, Expr::createTrue());
+      equalitiesParents.emplace(constraint, constraint);
       if (const NotExpr *ne = dyn_cast<NotExpr>(constraint)) {
-        equalities.insert(std::make_pair(ne->expr, Expr::createFalse()));
-        equalitiesParents.insert({ne->expr, constraint});
+        equalities.emplace(ne->expr, Expr::createFalse());
+        equalitiesParents.emplace(ne->expr, constraint);
       }
     }
   }

lib/Expr/Expr.cpp

@@ -153,11 +153,13 @@ int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
     return 0;
 
   Kind ak = getKind(), bk = b.getKind();
-  if (ak != bk)
-    return (ak < bk) ? -1 : 1;
+  int kc = (ak > bk) - (ak < bk);
+  if (kc)
+    return kc;
 
-  if (hashValue != b.hashValue)
-    return (hashValue < b.hashValue) ? -1 : 1;
+  int hc = (hashValue > b.hashValue) - (hashValue < b.hashValue);
+  if (hc)
+    return hc;
 
   if (int res = compareContents(b))
     return res;

lib/Module/CMakeLists.txt

@@ -8,6 +8,7 @@
 #===------------------------------------------------------------------------===#
 set(KLEE_MODULE_COMPONENT_SRCS
   CallSplitter.cpp
+  CallRemover.cpp
   Checks.cpp
   CodeGraphInfo.cpp
   FunctionAlias.cpp

lib/Module/CallRemover.cpp

@@ -0,0 +1,36 @@
+//===-- CallRemover.cpp----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Passes.h"
+#include <unordered_set>
+
+namespace klee {
+
+using namespace llvm;
+
+char CallRemover::ID;
+
+bool CallRemover::runOnModule(llvm::Module &M) {
+  std::vector<std::string> badFuncs = {"llvm.dbg.declare", "llvm.dbg.label"};
+
+  for (const auto &f : badFuncs) {
+    auto Declare = M.getFunction(f);
+    if (!Declare)
+      continue;
+    while (!Declare->use_empty()) {
+      auto CI = cast<CallInst>(Declare->user_back());
+      assert(CI->use_empty() && "deleted function must have void result");
+      CI->eraseFromParent();
+    }
+    Declare->eraseFromParent();
+  }
+
+  return true;
+}
+} // namespace klee

lib/Module/CallSplitter.cpp

@@ -1,5 +1,4 @@
-//===-- CallSplitter.cpp
-//-------------------------------------------------------===//
+//===-- CallSplitter.cpp --------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -46,8 +45,9 @@ bool CallSplitter::runOnFunction(Function &F) {
         if (callInst != firstInst) {
           fbb = fbb->splitBasicBlock(callInst);
         }
-        if (isa<BranchInst>(afterCallInst) &&
-            cast<BranchInst>(afterCallInst)->isUnconditional()) {
+        if ((isa<BranchInst>(afterCallInst) &&
+             cast<BranchInst>(afterCallInst)->isUnconditional()) ||
+            isa<UnreachableInst>(afterCallInst)) {
           break;
         }
         fbb = fbb->splitBasicBlock(afterCallInst);

lib/Module/KModule.cpp

@@ -117,6 +117,11 @@ cl::opt<bool>
                cl::desc("Split each call in own basic block (default=true)"),
                cl::init(true), cl::cat(klee::ModuleCat));
 
+static cl::opt<bool>
+    StripUnwantedCalls("strip-unwanted-calls",
+                       cl::desc("Strip all unwanted calls (llvm.dbg.* stuff)"),
+                       cl::init(false), cl::cat(klee::ModuleCat));
+
 cl::opt<bool> SplitReturns(
     "split-returns",
     cl::desc("Split each return in own basic block (default=true)"),
@@ -332,6 +337,8 @@ void KModule::optimiseAndPrepare(
   pm3.add(createScalarizerPass());
   pm3.add(new PhiCleanerPass());
   pm3.add(new FunctionAliasPass());
+  if (StripUnwantedCalls)
+    pm3.add(new CallRemover());
   if (SplitCalls) {
     pm3.add(new CallSplitter());
   }

lib/Module/Optimize.cpp

@@ -72,11 +72,6 @@ static cl::opt<bool>
                cl::desc("Strip debugger symbol info from executable"),
                cl::init(false), cl::cat(klee::ModuleCat));
 
-static cl::opt<bool>
-    StripDebugDeclare("strip-debug-declare",
-                      cl::desc("Strip all llvm.dbg.declare intrinsics"),
-                      cl::init(true), cl::cat(klee::ModuleCat));
-
 static cl::alias A1("S", cl::desc("Alias for --strip-debug"),
                     cl::aliasopt(StripDebug));
 
@@ -103,8 +98,6 @@ static void AddStandardCompilePasses(legacy::PassManager &PM) {
   // If the -strip-debug command line option was specified, do it.
   if (StripDebug)
     addPass(PM, createStripSymbolsPass(true));
-  if (StripDebugDeclare)
-    addPass(PM, createStripDebugDeclarePass());
 
   addPass(PM, createCFGSimplificationPass());       // Clean up disgusting code
   addPass(PM, createPromoteMemoryToRegisterPass()); // Kill useless allocas

lib/Module/Passes.h

@@ -206,6 +206,14 @@ class CallSplitter : public llvm::FunctionPass {
   bool runOnFunction(llvm::Function &F) override;
 };
 
+/// Remove unwanted calls
+class CallRemover : public llvm::ModulePass {
+public:
+  static char ID;
+  CallRemover() : llvm::ModulePass(ID) {}
+  bool runOnModule(llvm::Module &M) override;
+};
+
 class ReturnSplitter : public llvm::FunctionPass {
 public:
   static char ID;

test/Feature/CoverOnTheFly.c

@@ -2,11 +2,10 @@
 // REQUIRES: not-asan
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --only-output-states-covering-new --max-instructions=2000 --delay-cover-on-the-fly=500 --dump-states-on-halt=false --cover-on-the-fly --search=bfs --use-guided-search=none --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --only-output-states-covering-new --max-instructions=2000 --timer-interval=1ms --delay-cover-on-the-fly=1ms --dump-states-on-halt=false --cover-on-the-fly --search=bfs --use-guided-search=none --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 
-#define a (2)
 int main() {
   int res = 0;
   for (;;) {
@@ -31,5 +30,4 @@ int main() {
   }
 }
 
-// CHECK: KLEE: done: completed paths = 0
-// CHECK: KLEE: done: generated tests = 5
+// CHECK-NOT: KLEE: done: generated tests = 0

test/Feature/SymbolicSizes/IntArray.c

@@ -1,5 +1,5 @@
-// REQUIRES: not-darwin
-// Disabling darwin because it overflows stack on CI
+// REQUIRES: not-darwin, not-metasmt
+// Disabling darwin and metasmt because test has flaky behaviour on CI
 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-sym-size-alloc --use-sym-size-li --min-number-elements-li=1 --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s