Ocelaiwo/bidirectional klee

build.sh

@@ -1,35 +1,51 @@
-#!/bin/bash
-# This script is used to build KLEE as UTBot backend
-
-set -e
-set -o pipefail
-mkdir -p build
-cd build
-
-$UTBOT_CMAKE_BINARY -G Ninja \
-  -DCMAKE_PREFIX_PATH=$UTBOT_INSTALL_DIR/lib/cmake/z3 \
-  -DCMAKE_LIBRARY_PATH=$UTBOT_INSTALL_DIR/lib \
-  -DCMAKE_INCLUDE_PATH=$UTBOT_INSTALL_DIR/include \
-  -DENABLE_SOLVER_Z3=TRUE \
-  -DENABLE_POSIX_RUNTIME=TRUE \
-  -DENABLE_KLEE_UCLIBC=ON \
-  -DKLEE_UCLIBC_PATH=$UTBOT_ALL/klee-uclibc \
-  -DENABLE_FLOATING_POINT=TRUE \
-  -DENABLE_FP_RUNTIME=TRUE \
-  -DLLVM_CONFIG_BINARY=$UTBOT_INSTALL_DIR/bin/llvm-config \
-  -DLLVMCC=/utbot_distr/install/bin/clang \
-  -DLLVMCXX=/utbot_distr/install/bin/clang++ \
-  -DENABLE_UNIT_TESTS=TRUE \
-  -DENABLE_SYSTEM_TESTS=TRUE \
-  -DGTEST_SRC_DIR=$UTBOT_ALL/gtest \
-  -DGTEST_INCLUDE_DIR=$UTBOT_ALL/gtest/googletest/include \
-  -DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/klee \
-  -DENABLE_KLEE_LIBCXX=TRUE \
-  -DKLEE_LIBCXX_DIR=$UTBOT_ALL/libcxx/install \
-  -DKLEE_LIBCXX_INCLUDE_DIR=$UTBOT_ALL/libcxx/install/include/c++/v1 \
-  -DENABLE_KLEE_EH_CXX=TRUE \
-  -DKLEE_LIBCXXABI_SRC_DIR=$UTBOT_ALL/libcxx/libcxxabi \
-   ..
-
-$UTBOT_CMAKE_BINARY --build .
-$UTBOT_CMAKE_BINARY --install .
+#!/bin/sh
+
+# For more build options, visit
+# https://klee.github.io/build-script/
+
+# Base folder where dependencies and KLEE itself are installed
+BASE=$HOME/klee_build
+
+## KLEE Required options
+# Build type for KLEE. The options are:
+# Release
+# Release+Debug
+# Release+Asserts
+# Release+Debug+Asserts
+# Debug
+# Debug+Asserts
+# KLEE_RUNTIME_BUILD="Debug+Asserts"
+KLEE_RUNTIME_BUILD="Debug" # "Debug+Asserts"
+
+COVERAGE=0
+ENABLE_DOXYGEN=0
+USE_TCMALLOC=0
+USE_LIBCXX=1
+# Also required despite not being mentioned in the guide
+SQLITE_VERSION="3370200"
+
+
+## LLVM Required options
+LLVM_VERSION=11
+ENABLE_OPTIMIZED=1
+ENABLE_DEBUG=0
+DISABLE_ASSERTIONS=1
+REQUIRES_RTTI=1
+
+## Solvers Required options
+# SOLVERS=STP
+SOLVERS=Z3
+
+## Google Test Required options
+GTEST_VERSION=1.11.0
+
+## UClibC Required options
+UCLIBC_VERSION=klee_0_9_29
+# LLVM_VERSION is also required for UClibC
+
+## Z3 Required options
+Z3_VERSION=4.8.15
+STP_VERSION=2.3.3
+MINISAT_VERSION=master
+
+BASE="$BASE" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION SQLITE_VERSION=$SQLITE_VERSION ./scripts/build/build.sh klee --install-system-deps

configs/options.json

@@ -0,0 +1,52 @@
+{
+    "inputs" : {
+        "buildPath" : "",
+        "sarifTracesFilePath" : ".json",
+        "bytecodeFilePath" : ".bc",
+        "maxTime" : "240",
+        "maxSolverTime" : "5",
+        "maxForks" : "200",
+        "maxSymAlloc" : "32",
+        "SymbolicAllocationThreshold" : "2048",
+        "minNumberElements" : "4",
+        "maxCycles" : 10,
+        "useSymbolicSizeLI" : false,
+        "writeKpaths": false
+    },
+    "configurations": [
+        {
+            "program": "${buildPath}/bin/klee",
+            "args": [
+                "--use-guided-search=error",
+                "--mock-external-calls",
+                "--posix-runtime",
+                "--check-out-of-memory",
+                "--suppress-external-warnings",
+                "--libc=klee",
+                "--skip-not-lazy-initialized",
+                "--external-calls=all",
+                "--output-source=false",
+                "--output-istats=false",
+                "--output-stats=false",
+                "--max-time=${maxTime}s",
+                "--max-sym-alloc=${maxSymAlloc}",
+                "--max-forks=${maxForks}",
+                "--max-solver-time=${maxSolverTime}s",
+                "--mock-all-externals",
+                "--smart-resolve-entry-function",
+                "--extern-calls-can-return-null",
+                "--align-symbolic-pointers=false",
+                "--write-no-tests",
+                "--write-kpaths=${writeKpaths}",
+                "--use-lazy-initialization=only",
+                "--min-number-elements-li=${minNumberElements}",
+                "--use-sym-size-li=${useSymbolicSizeLI}",
+                "--max-cycles-before-stuck=${maxCycles}",
+                "--rewrite-equalities=simple",
+                "--symbolic-allocation-threshold=${SymbolicAllocationThreshold}",
+                "--analysis-reproduce=${sarifTracesFilePath}",
+                "${bytecodeFilePath}"
+            ]
+        }
+    ]
+}

include/klee/ADT/Ticker.h

@@ -0,0 +1,33 @@
+// -*- C++ -*-
+#ifndef KLEE_TICKER_H
+#define KLEE_TICKER_H
+
+#include <vector>
+
+class Ticker {
+  std::vector<unsigned> ticks;
+  unsigned index = 0;
+  unsigned counter = 0;
+
+public:
+  Ticker(std::vector<unsigned> ticks) : ticks(ticks) {}
+
+  unsigned getCurrent() {
+    unsigned current = index;
+    counter += 1;
+    if (counter == ticks[index]) {
+      index = (index + 1) % ticks.size();
+      counter = 0;
+    }
+    return current;
+  }
+
+  void moveToNext() {
+    if (counter != 0) {
+      index = (index + 1) % ticks.size();
+      counter = 0;
+    }
+  }
+};
+
+#endif

include/klee/Core/Interpreter.h

@@ -56,9 +56,15 @@ class InterpreterHandler {
 
   virtual void incPathsCompleted() = 0;
   virtual void incPathsExplored(std::uint32_t num = 1) = 0;
+  virtual void incSummarizedLocations() = 0;
 
-  virtual void processTestCase(const ExecutionState &state, const char *err,
-                               const char *suffix) = 0;
+  virtual void processTestCase(const ExecutionState &state, const char *message,
+                               const char *suffix, bool isError = false) = 0;
+};
+
+enum class ExecutionKind {
+  Forward,
+  Bidirectional
 };
 
 class Interpreter {

include/klee/Core/TargetedExecutionReporter.h

@@ -30,7 +30,7 @@ ty min(ty left, ty right);
 }; // namespace confidence
 
 void reportFalsePositive(confidence::ty confidence,
-                         const std::set<ReachWithError> &errors, unsigned id,
+                         const std::vector<ReachWithError> &errors, unsigned id,
                          std::string whatToIncrease);
 
 } // namespace klee

include/klee/Core/TerminationTypes.h

@@ -20,7 +20,9 @@
   TTYPE(MaxDepth, 3U, "early")                                                 \
   TTYPE(OutOfMemory, 4U, "early")                                              \
   TTYPE(OutOfStackMemory, 5U, "early")                                         \
-  MARK(EARLY, 5U)                                                              \
+  TTYPE(MaxCycles, 6U, "early")                                                \
+  TTYPE(MissedAllTargets, 7U, "miss_all_targets.early")                        \
+  MARK(EARLY, 7U)                                                              \
   TTYPE(Solver, 8U, "solver.err")                                              \
   MARK(SOLVERERR, 8U)                                                          \
   TTYPE(Abort, 10U, "abort.err")                                               \
@@ -33,7 +35,7 @@
   TTYPE(ReadOnly, 17U, "read_only.err")                                        \
   TTYPE(ReportError, 18U, "report_error.err")                                  \
   TTYPE(UndefinedBehavior, 19U, "undefined_behavior.err")                      \
-  TTYPE(InternalOutOfMemory, 20U, "out_of_memory.er")                          \
+  TTYPE(InternalOutOfMemory, 20U, "out_of_memory.err")                         \
   MARK(PROGERR, 20U)                                                           \
   TTYPE(User, 23U, "user.err")                                                 \
   MARK(USERERR, 23U)                                                           \
@@ -60,6 +62,7 @@ enum Reason {
   MaxInstructions,
   MaxSteppedInstructions,
   MaxTime,
+  MaxCycles,
   CovCheck,
   NoMoreStates,
   ReachedTarget,

include/klee/Expr/Assignment.h

@@ -66,6 +66,7 @@ class Assignment {
 
   bindings_ty::const_iterator begin() const { return bindings.begin(); }
   bindings_ty::const_iterator end() const { return bindings.end(); }
+  bool isEmpty() { return begin() == end(); }
 
   std::vector<const Array *> keys() const;
   std::vector<SparseStorage<unsigned char>> values() const;

include/klee/Expr/Constraints.h

@@ -73,8 +73,9 @@ class ConstraintSet {
 
 class PathConstraints {
 public:
-  using ordered_constraints_ty =
-      std::map<Path::PathIndex, constraints_ty, Path::PathIndexCompare>;
+  using ordered_constraints_ty = std::vector<ref<Expr>>;
+  using path_ordered_constraints_ty =
+      std::map<Path::PathIndex, ordered_constraints_ty, Path::PathIndexCompare>;
 
   void advancePath(KInstruction *ki);
   void advancePath(const Path &path);
@@ -90,7 +91,7 @@ class PathConstraints {
   const ConstraintSet &cs() const;
   const Path &path() const;
   const ExprHashMap<Path::PathIndex> &indexes() const;
-  const ordered_constraints_ty &orderedCS() const;
+  const path_ordered_constraints_ty &orderedCS() const;
 
   static PathConstraints concat(const PathConstraints &l,
                                 const PathConstraints &r);
@@ -100,7 +101,7 @@ class PathConstraints {
   constraints_ty _original;
   ConstraintSet constraints;
   ExprHashMap<Path::PathIndex> pathIndexes;
-  ordered_constraints_ty orderedConstraints;
+  path_ordered_constraints_ty orderedConstraints;
   ExprHashMap<ExprHashSet> _simplificationMap;
 };
 

include/klee/Expr/Expr.h

@@ -123,7 +123,7 @@ class Expr {
   };
 
   static ExprCacheSet cachedExpressions;
-  static ref<Expr> createCachedExpr(const ref<Expr> &e);
+  static ref<Expr> createCachedExpr(ref<Expr> e);
   bool isCached = false;
   bool toBeCleared = false;
 
@@ -321,6 +321,9 @@ class Expr {
   /// isZero - Is this a constant zero.
   bool isZero() const;
 
+  /// isZero - Is this a constant one.
+  bool isOne() const;
+
   /// isTrue - Is this the true expression.
   bool isTrue() const;
 
@@ -391,7 +394,7 @@ struct Expr::CreateArg {
 // Comparison operators
 
 inline bool operator==(const Expr &lhs, const Expr &rhs) {
-  return lhs.compare(rhs) == 0;
+  return lhs.equals(rhs);
 }
 
 inline bool operator<(const Expr &lhs, const Expr &rhs) {
@@ -1553,6 +1556,12 @@ inline bool Expr::isZero() const {
   return false;
 }
 
+inline bool Expr::isOne() const {
+  if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
+    return CE->isOne();
+  return false;
+}
+
 inline bool Expr::isTrue() const {
   assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))

include/klee/Expr/ExprEvaluator.h

@@ -17,15 +17,16 @@ namespace klee {
 class ExprEvaluator : public ExprVisitor {
 protected:
   Action evalRead(const UpdateList &ul, unsigned index);
-  Action visitRead(const ReadExpr &re);
-  Action visitExpr(const Expr &e);
+  Action visitRead(const ReadExpr &re) override;
+  Action visitSelect(const SelectExpr &se) override;
+  Action visitExpr(const Expr &e) override;
 
   Action protectedDivOperation(const BinaryExpr &e);
-  Action visitUDiv(const UDivExpr &e);
-  Action visitSDiv(const SDivExpr &e);
-  Action visitURem(const URemExpr &e);
-  Action visitSRem(const SRemExpr &e);
-  Action visitExprPost(const Expr &e);
+  Action visitUDiv(const UDivExpr &e) override;
+  Action visitSDiv(const SDivExpr &e) override;
+  Action visitURem(const URemExpr &e) override;
+  Action visitSRem(const SRemExpr &e) override;
+  Action visitExprPost(const Expr &e) override;
 
 public:
   ExprEvaluator() {}

include/klee/Expr/ExprPPrinter.h

@@ -11,6 +11,7 @@
 #define KLEE_EXPRPPRINTER_H
 
 #include "klee/Expr/Expr.h"
+#include "klee/Expr/Lemma.h"
 
 namespace llvm {
 class raw_ostream;
@@ -69,6 +70,8 @@ class ExprPPrinter {
                          const Array *const *evalArraysBegin = 0,
                          const Array *const *evalArraysEnd = 0,
                          bool printArrayDecls = true);
+
+  static void printLemma(llvm::raw_ostream &os, const Lemma &l);
 };
 
 } // namespace klee

include/klee/Expr/ExprVisitor.h

@@ -137,10 +137,9 @@ class ExprVisitor {
   virtual Action visitFNeg(const FNegExpr &);
   virtual Action visitFRint(const FRintExpr &);
 
-protected:
-  VisitorHash visited;
-
 private:
+  typedef ExprHashMap<ref<Expr>> visited_ty;
+  visited_ty visited;
   bool recursive;
 
   ref<Expr> visitActual(const ref<Expr> &e);