Add DistanceCalculator and fix performance bugs

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,45 @@
+{
+    "inputs" : {
+        "buildPath" : "",
+        "sarifTracesFilePath" : ".json",
+        "bytecodeFilePath" : ".bc",
+        "maxTime" : "240",
+        "maxSolverTime" : "5",
+        "maxForks" : "200",
+        "maxSymAlloc" : "32",
+        "symbolicAllocationThreshhold" : "2048"
+    },
+    "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",
+                "--use-lazy-initialization=only",
+                "--rewrite-equalities=simple",
+                "--symbolic-allocation-threshhold=${symbolicAllocationThreshhold}",
+                "--analysis-reproduce=${sarifTracesFilePath}",
+                "${bytecodeFilePath}"
+            ]
+        }
+    ]
+}

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

@@ -84,7 +84,10 @@ typedef std::set<ref<Symcrete>, SymcreteLess> SymcreteOrderedSet;
 
 class AddressSymcrete : public Symcrete {
 public:
-  AddressSymcrete(ref<Expr> s, SymcreteKind kind) : Symcrete(s, kind) {
+  const Array *addressArray;
+
+  AddressSymcrete(const Array *_addressArray, ref<Expr> s, SymcreteKind kind)
+      : Symcrete(s, kind), addressArray(_addressArray) {
     assert((kind == SymcreteKind::SK_ALLOC_ADDRESS ||
             kind == SymcreteKind::SK_LI_ADDRESS) &&
            "wrong kind");
@@ -98,8 +101,8 @@ class AddressSymcrete : public Symcrete {
 
 class AllocAddressSymcrete : public AddressSymcrete {
 public:
-  AllocAddressSymcrete(ref<Expr> s)
-      : AddressSymcrete(s, SymcreteKind::SK_ALLOC_ADDRESS) {}
+  AllocAddressSymcrete(const Array *addressArray, ref<Expr> s)
+      : AddressSymcrete(addressArray, s, SymcreteKind::SK_ALLOC_ADDRESS) {}
 
   static bool classof(const Symcrete *symcrete) {
     return symcrete->getKind() == SymcreteKind::SK_ALLOC_ADDRESS;
@@ -108,8 +111,8 @@ class AllocAddressSymcrete : public AddressSymcrete {
 
 class LazyInitializedAddressSymcrete : public AddressSymcrete {
 public:
-  LazyInitializedAddressSymcrete(ref<Expr> s)
-      : AddressSymcrete(s, SymcreteKind::SK_LI_ADDRESS) {}
+  LazyInitializedAddressSymcrete(const Array *addressArray, ref<Expr> s)
+      : AddressSymcrete(addressArray, s, SymcreteKind::SK_LI_ADDRESS) {}
 
   static bool classof(const Symcrete *symcrete) {
     return symcrete->getKind() == SymcreteKind::SK_LI_ADDRESS;

include/klee/Module/TargetForest.h

@@ -298,6 +298,7 @@ class TargetForest {
   void add(ref<Target>);
   void remove(ref<Target>);
   void blockIn(ref<Target>, ref<Target>);
+  void block(const ref<Target> &);
   const ref<History> getHistory() { return history; };
   const ref<Layer> getTargets() { return forest; };
   void dump() const;

lib/Core/CMakeLists.txt

@@ -13,6 +13,7 @@ klee_add_component(kleeCore
   Context.cpp
   CoreStats.cpp
   CXXTypeSystem/CXXTypeManager.cpp
+  DistanceCalculator.cpp
   ExecutionState.cpp
   Executor.cpp
   ExecutorUtil.cpp