feat: Add a bunch of features and fixes (#202)

* fix: Terminate only not `CoveredNew` states

* fix: Do not cache ConstantExpr's

* chore(kleef): Add debug option to kleef

* fix: Fix the `cover-error-call` tests

* feat: Add FreezeLower

* chore: Update `constructSolverChain`

* feat: Cache LocationInfo

* fix: Rewrite equalities intermittently

* chore: Bump Bitwuzla version up to 0.7.0

* fix: Fix `eqExpr` in BitwuzlaBuilder

* fix(kleef): Use batching search in kleef script.

fix(kleef): Disable concretizing solver in kleef

fix(kleef): Disable tree-solver

* chore: Get rid of unnecessary constraints

* chore(module): Intern `LocationInfo`

* fix: Fix SubExpr simplify

* feat: Add `MaxCoreSolverMemory` (only for Bitwuzla)

* test: Update tests

* fix(freeze): Add include

* fix(floats): Fix `FPToI` encoding, restrict on the domain of definition

* test(options): Use `--debug` option in `kleef`

* chore(floats): Add description fo `FPToI` workaround

* fix(ci): Disable sanitizers because of bitwuzla crashing with an assertion failure

---------

Co-authored-by: dim8art <dim8art@yandex.ru>

Author: misonijnik

.github/workflows/build.yaml

@@ -37,7 +37,7 @@ env:
   USE_LIBCXX: 1
   Z3_VERSION: 4.8.15
   SQLITE_VERSION: 3400100
-  BITWUZLA_VERSION: 0.3.1
+  BITWUZLA_VERSION: 0.7.0
   JSON_VERSION: v3.11.3
   IMMER_VERSION: v0.8.1
 

build.sh

@@ -56,7 +56,7 @@ Z3_VERSION=4.8.15
 STP_VERSION=2.3.3
 MINISAT_VERSION=master
 
-BITWUZLA_VERSION=0.3.1
+BITWUZLA_VERSION=0.7.0
 
 KEEP_PARSE="true"
 while [ $KEEP_PARSE = "true" ]; do

include/klee/Expr/Constraints.h

@@ -120,29 +120,21 @@ class PathConstraints {
   void advancePath(KInstruction *ki);
   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 Path &path() const;
-  const ExprHashMap<Path::PathIndex> &indexes() const;
-  const ordered_constraints_ty &orderedCS() const;
 
   static PathConstraints concat(const PathConstraints &l,
                                 const PathConstraints &r);
 
 private:
   Path _path;
-  constraints_ty _original;
   ConstraintSet constraints;
-  ExprHashMap<Path::PathIndex> pathIndexes;
-  ordered_constraints_ty orderedConstraints;
-  ExprHashMap<ExprHashSet> _simplificationMap;
+  unsigned long addingCounter = 0UL;
 };
 
 struct Conflict {

include/klee/Expr/Expr.h

@@ -150,13 +150,7 @@ class Expr {
     }
   };
 
-  struct ConstantExprCacheSet {
-    std::unordered_map<llvm::APInt, ConstantExpr *, APIntHash, APIntEq> cache;
-    ~ConstantExprCacheSet();
-  };
-
   static ExprCacheSet cachedExpressions;
-  static ConstantExprCacheSet cachedConstantExpressions;
   static ref<Expr> createCachedExpr(ref<Expr> e);
   bool isCached = false;
   bool toBeCleared = false;
@@ -1538,24 +1532,17 @@ class ConstantExpr : public Expr {
   void toMemory(void *address);
 
   static ref<ConstantExpr> alloc(const llvm::APInt &v) {
-    auto success = cachedConstantExpressions.cache.find(v);
-    if (success == cachedConstantExpressions.cache.end()) {
-      // Cache miss
-      ref<ConstantExpr> r = new ConstantExpr(v);
-      r->computeHash();
-      r->computeHeight();
-      r->isCached = true;
-      cachedConstantExpressions.cache[v] = r.get();
-      return r;
-    }
-    return success->second;
+    ref<ConstantExpr> r = new ConstantExpr(v);
+    r->computeHash();
+    r->computeHeight();
+    return r;
   }
 
   static ref<ConstantExpr> alloc(const llvm::APFloat &f) {
     ref<ConstantExpr> r(new ConstantExpr(f.bitcastToAPInt(), true));
     r->computeHash();
     r->computeHeight();
-    return createCachedExpr(r);
+    return r;
   }
 
   static ref<ConstantExpr> alloc(uint64_t v, Width w) {

include/klee/Module/KInstruction.h

@@ -12,9 +12,11 @@
 
 #include "KModule.h"
 #include "KValue.h"
+#include "LocationInfo.h"
 
 #include "llvm/Support/raw_ostream.h"
 
+#include <optional>
 #include <unordered_map>
 #include <vector>
 
@@ -71,6 +73,7 @@ struct KInstruction : public KValue {
   /// register indices.
   int *operands;
   KBlock *parent;
+  mutable std::optional<ref<LocationInfo>> locationInfo;
 
 private:
   // Instruction index in the basic block

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.
   ///

include/klee/Module/LocationInfo.h

@@ -10,9 +10,13 @@
 #ifndef KLEE_LOCATIONINFO_H
 #define KLEE_LOCATIONINFO_H
 
+#include "klee/ADT/Ref.h"
+
 #include <cstdint>
+#include <functional>
 #include <optional>
 #include <string>
+#include <unordered_set>
 
 namespace llvm {
 class Function;
@@ -23,12 +27,16 @@ class Module;
 
 namespace klee {
 struct PhysicalLocationJson;
-}
+struct LocationInfo;
+} // namespace klee
 
 namespace klee {
 
 /// @brief Immutable struct representing location in source code.
 struct LocationInfo {
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
+
   /// @brief Path to source file for that location.
   const std::string file;
 
@@ -44,14 +52,73 @@ struct LocationInfo {
   /// @return SARIFs representation of location.
   PhysicalLocationJson serialize() const;
 
+  static ref<LocationInfo> create(std::string file, uint64_t line,
+                                  std::optional<uint64_t> column) {
+    LocationInfo *locationInfo = new LocationInfo(file, line, column);
+    return createCachedLocationInfo(locationInfo);
+  }
+
   bool operator==(const LocationInfo &rhs) const {
     return file == rhs.file && line == rhs.line && column == rhs.column;
   }
+
+  bool equals(const LocationInfo &b) const { return *this == b; }
+
+  ~LocationInfo() {
+    if (isCached) {
+      toBeCleared = true;
+      cachedLocationInfo.cache.erase(this);
+    }
+  }
+
+private:
+  LocationInfo(std::string file, uint64_t line, std::optional<uint64_t> column)
+      : file(file), line(line), column(column) {}
+
+  struct LocationInfoHash {
+    std::size_t operator()(LocationInfo *const s) const noexcept {
+      std::size_t r = 0;
+      std::size_t h1 = std::hash<std::string>{}(s->file);
+      std::size_t h2 = std::hash<uint64_t>{}(s->line);
+      std::size_t h3 = std::hash<std::optional<uint64_t>>{}(s->column);
+      r ^= h1 + 0x9e3779b9 + (r << 6) + (r >> 2);
+      r ^= h2 + 0x9e3779b9 + (r << 6) + (r >> 2);
+      r ^= h3 + 0x9e3779b9 + (r << 6) + (r >> 2);
+      return r;
+    }
+  };
+
+  struct LocationInfoCmp {
+    bool operator()(LocationInfo *const a, LocationInfo *const b) const {
+      return *a == *b;
+    }
+  };
+
+  using CacheType =
+      std::unordered_set<LocationInfo *, LocationInfoHash, LocationInfoCmp>;
+
+  struct LocationInfoCacheSet {
+    CacheType cache;
+    ~LocationInfoCacheSet() {
+      while (cache.size() != 0) {
+        ref<LocationInfo> tmp = *cache.begin();
+        tmp->isCached = false;
+        cache.erase(cache.begin());
+      }
+    }
+  };
+
+  static LocationInfoCacheSet cachedLocationInfo;
+  bool isCached = false;
+  bool toBeCleared = false;
+
+  static ref<LocationInfo>
+  createCachedLocationInfo(ref<LocationInfo> locationInfo);
 };
 
-LocationInfo getLocationInfo(const llvm::Function *func);
-LocationInfo getLocationInfo(const llvm::Instruction *inst);
-LocationInfo getLocationInfo(const llvm::GlobalVariable *global);
+ref<LocationInfo> getLocationInfo(const llvm::Function *func);
+ref<LocationInfo> getLocationInfo(const llvm::Instruction *inst);
+ref<LocationInfo> getLocationInfo(const llvm::GlobalVariable *global);
 
 } // namespace klee
 

include/klee/Solver/IncompleteSolver.h

@@ -79,7 +79,7 @@ class StagedSolverImpl : public SolverImpl {
                            bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 

include/klee/Solver/Solver.h

@@ -191,7 +191,7 @@ class Solver {
   getRange(const Query &, time::Span timeout = time::Span());
 
   virtual std::string getConstraintLog(const Query &query);
-  virtual void setCoreSolverTimeout(time::Span timeout);
+  virtual void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
 
   /// @brief Notify the solver that the state with specified id has been
   /// terminated

include/klee/Solver/SolverCmdLine.h

@@ -41,6 +41,8 @@ extern llvm::cl::opt<bool> LogTimedOutQueries;
 
 extern llvm::cl::opt<std::string> MaxCoreSolverTime;
 
+extern llvm::cl::opt<unsigned> MaxCoreSolverMemory;
+
 extern llvm::cl::opt<bool> UseForkedCoreSolver;
 
 extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;