feat: Add bidirectional mode (#204)

* ci: updated dependencies in ci build and tests

* feat: various adt constructions

* feat: symbolicSizeConstantAddress memory support

* feat: bidirectional execution

* feat: lemmas deduction and persistance in bidirectional mode

* feat: memory constraints in solvers are supported

* feat: added FreezeLower pass

---------

Co-authored-by: Aleksandr Misonizhnik <misonijnik@gmail.com>
Co-authored-by: Aleksei Babushkin <ocelaiwo@gmail.com>

Author: 3 people

.cirrus.yml

@@ -9,7 +9,7 @@ task:
   build_script:
     - mkdir build
     - cd build
-    - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DENABLE_WARNINGS_AS_ERRORS=1 -DENABLE_FP_RUNTIME=1 ..
+    - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DWARNINGS_AS_ERRORS:BOOL=OFF ..
     - gmake
   test_script:
     - sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg

.github/workflows/build.yaml

@@ -156,6 +156,7 @@ jobs:
         env: ${{ matrix.env }}
         run: scripts/build/run-tests.sh --run-docker --debug
 
+
   macOS:
     runs-on: macos-latest
     env:
@@ -173,11 +174,11 @@ jobs:
       - name: Checkout KLEE source code
         uses: actions/checkout@v4
       - name: Create virtualenv for Python3 (PEP 668)
-        run:  python3 -m venv .venv
+        run: python3 -m venv .venv
       - name: Build KLEE
-        run:  source .venv/bin/activate && echo "$(which tabulate)" && scripts/build/build.sh klee --debug --install-system-deps
+        run: source .venv/bin/activate && echo "$(which tabulate)" && scripts/build/build.sh klee --debug --install-system-deps
       - name: Run tests
-        run:  source .venv/bin/activate && scripts/build/run-tests.sh /tmp/klee_build* --debug
+        run: source .venv/bin/activate && scripts/build/run-tests.sh /tmp/klee_build* --debug
 
   Docker:
     runs-on: ubuntu-latest
@@ -230,8 +231,8 @@ jobs:
   clang-format:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v3
-    - uses: actions/setup-python@v4
-      with:
-        python-version: 3.x
-    - uses: pre-commit/action@v3.0.1
+      - uses: actions/checkout@v3
+      - uses: actions/setup-python@v4
+        with:
+          python-version: 3.x
+      - uses: pre-commit/action@v3.0.1

build.sh

@@ -39,7 +39,7 @@ ENABLE_WARNINGS_AS_ERRORS=0
 SOLVERS=BITWUZLA:Z3:STP
 
 ## Google Test Required options
-GTEST_VERSION=1.11.0
+GTEST_VERSION=1.16.0
 
 ## json options
 JSON_VERSION=v3.11.3

include/klee/ADT/ImmutableList.h

@@ -38,6 +38,10 @@ template <typename T> class ImmutableList {
         prev = nullptr;
       }
     }
+
+    ImmutableListNode(std::shared_ptr<ImmutableListNode> prev, size_t prev_len,
+                      std::vector<T> values)
+        : prev(prev), prev_len(prev_len), values(std::move(values)) {}
   };
 
   std::shared_ptr<ImmutableListNode> node;
@@ -97,6 +101,26 @@ template <typename T> class ImmutableList {
     node->values.push_back(value);
   }
 
+  void pop_back() {
+    while (node && node->values.empty()) {
+      node = node->prev;
+    }
+    if (!node) {
+      return;
+    }
+    node = std::make_shared<ImmutableListNode>(node->prev, node->prev_len,
+                                               node->values);
+    node->values.pop_back();
+  }
+
+  T at(size_t index) const {
+    auto cur = node;
+    while (cur && cur->prev_len > index) {
+      cur = cur->prev;
+    }
+    return cur->values[index - cur->prev_len];
+  }
+
   bool empty() const { return size() == 0; }
 
   const T &back() const {
@@ -106,6 +130,55 @@ template <typename T> class ImmutableList {
     return *it;
   }
 
+  const T &front() const { return at(0); }
+
+  friend bool operator==(const ImmutableList<T> &lhs,
+                         const ImmutableList<T> &rhs) {
+    if (lhs.size() != rhs.size()) {
+      return false;
+    }
+
+    auto li = lhs.begin();
+    auto ri = rhs.begin();
+    while (li != lhs.end() && ri != rhs.end()) {
+      if (*li != *ri) {
+        return false;
+      }
+      ++li;
+      ++ri;
+    }
+
+    return true;
+  }
+
+  friend bool operator!=(const ImmutableList<T> &lhs,
+                         const ImmutableList<T> &rhs) {
+    return !(lhs == rhs);
+  }
+
+  friend bool operator<(const ImmutableList<T> &lhs,
+                        const ImmutableList<T> &rhs) {
+    if (lhs.size() < rhs.size()) {
+      return true;
+    } else if (lhs.size() > rhs.size()) {
+      return false;
+    }
+
+    auto li = lhs.begin();
+    auto ri = rhs.begin();
+    while (li != lhs.end() && ri != rhs.end()) {
+      if (*li < *ri) {
+        return true;
+      } else if (*ri < *li) {
+        return false;
+      }
+      ++li;
+      ++ri;
+    }
+
+    return false;
+  }
+
   ImmutableList() : node(){};
   ImmutableList(const ImmutableList<T> &il)
       : node(std::make_shared<ImmutableListNode>(il)) {}

include/klee/ADT/Ticker.h

@@ -0,0 +1,57 @@
+// -*- C++ -*-
+#ifndef KLEE_TICKER_H
+#define KLEE_TICKER_H
+
+#include "klee/Support/ErrorHandling.h"
+
+#include <cassert>
+#include <vector>
+
+class Ticker {
+  std::vector<unsigned> ticks;
+  unsigned index = 0;
+  unsigned counter = 0;
+
+public:
+  Ticker(std::vector<unsigned> ticks) : ticks(ticks) {
+    bool atLeastOneNonZero = false;
+    for (auto i : ticks) {
+      if (i > 0) {
+        atLeastOneNonZero = true;
+      }
+    }
+    if (!atLeastOneNonZero) {
+      klee::klee_warning("All ticker entries are 0, using 1 for every entry");
+      ticks = std::vector<unsigned>(ticks.size(), 1);
+    }
+    while (ticks[index] == 0) {
+      index += 1;
+    }
+  }
+
+  unsigned getCurrent() {
+    unsigned current = index;
+    counter += 1;
+    if (counter == ticks[index]) {
+      moveToNext();
+    }
+    return current;
+  }
+
+  void moveToNext() {
+    assert(ticks[index] != 0);
+
+    if (counter != 0) {
+      index = (index + 1) % ticks.size();
+      counter = 0;
+    }
+
+    while (ticks[index] == 0) {
+      index = (index + 1) % ticks.size();
+    }
+  }
+
+  const std::vector<unsigned> &getTicks() { return ticks; }
+};
+
+#endif

include/klee/Core/Interpreter.h

@@ -85,6 +85,8 @@ enum class MockMutableGlobalsPolicy {
   All,  // Mock globals on module build stage and generate bc module for it
 };
 
+enum class ExecutionKind { Forward, Bidirectional };
+
 class Interpreter {
 public:
   enum class GuidanceKind {

include/klee/Core/TerminationTypes.h

@@ -97,6 +97,7 @@ enum Reason {
   MaxForks,
   CovCheck,
   NoMoreStates,
+  UnreachedTarget,
   ReachedTarget,
   ErrorOnWhichShouldExit,
   Interrupt,

include/klee/Expr/Constraints.h

@@ -117,23 +117,34 @@ class PathConstraints {
   using ordered_constraints_ty =
       PersistentMap<Path::PathIndex, constraints_ty, Path::PathIndexCompare>;
 
-  void advancePath(KInstruction *ki);
+  void advancePath(KInstruction *prevPC, KInstruction *pc);
+  void retractPath();
   void advancePath(const Path &path);
 
+  ExprHashSet addConstraint(ref<Expr> e, Path::PathIndex currIndex);
   ExprHashSet addConstraint(ref<Expr> e);
   bool isSymcretized(ref<Expr> expr) const;
   void addSymcrete(ref<Symcrete> s);
   void rewriteConcretization(const Assignment &a);
 
+  const constraints_ty &original() const;
+  const ExprHashMap<ExprHashSet> &simplificationMap() const;
   const ConstraintSet &cs() const;
+  const ConstraintSet &withAssumptions(const ExprHashSet &assumptions) const;
   const Path &path() const;
 
-  static PathConstraints concat(const PathConstraints &l,
-                                const PathConstraints &r);
+  const ordered_constraints_ty &orderedCS() const;
+  PathConstraints() = default;
+  PathConstraints(KInstruction *initpc) : _path(initpc) {}
 
 private:
   Path _path;
+  constraints_ty _original;
   ConstraintSet constraints;
+  mutable ConstraintSet tmpConstraints;
+  ExprHashMap<Path::PathIndex> pathIndexes;
+  ordered_constraints_ty orderedConstraints;
+  ExprHashMap<ExprHashSet> _simplificationMap;
   unsigned long addingCounter = 0UL;
 };
 

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;
@@ -74,6 +75,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/Lemma.h

@@ -0,0 +1,63 @@
+// -*- C++ -*-
+#ifndef KLEE_LEMMA_H
+#define KLEE_LEMMA_H
+
+#include "klee/Core/Interpreter.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/Path.h"
+
+#include <fstream>
+#include <memory>
+#include <string>
+
+namespace klee {
+class KModule;
+
+struct Lemma {
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
+
+  Path path;
+  ExprOrderedSet constraints;
+
+  Lemma(Path path, ExprOrderedSet constraints)
+      : path(path), constraints(constraints) {}
+
+  bool operator==(const Lemma &other) {
+    return this->path == other.path && this->constraints == other.constraints;
+  }
+
+  bool operator!=(const Lemma &other) { return !(*this == other); }
+
+  ref<Expr> asExpr();
+
+  int compare(const Lemma &b) const {
+    if (path == b.path && constraints == b.constraints) {
+      return 0;
+    }
+    return (path < b.path || (path == b.path && constraints < b.constraints))
+               ? -1
+               : 1;
+  }
+};
+
+class Summary {
+public:
+  void addLemma(ref<Lemma> lemma);
+  void dumpToFile(KModule *km);
+  void readFromFile(KModule *km);
+
+  Summary(InterpreterHandler *ih) : ih(ih) {}
+
+private:
+  std::set<ref<Lemma>> lemmas;
+  std::set<ref<Lemma>> dumped;
+
+  std::string getFilename();
+
+  InterpreterHandler *ih;
+};
+
+}; // namespace klee
+
+#endif