Persistent object state

.github/workflows/build.yaml

@@ -3,9 +3,9 @@ name: CI
 
 on:
   pull_request:
-    branches: [main, utbot-main]
+    branches: [persistent_object_state]
   push:
-    branches: [main, utbot-main]
+    branches: [persistent_object_state]
 
 # Defaults for building KLEE
 env:

CMakeLists.txt

@@ -17,16 +17,16 @@ project(KLEE CXX C)
 # Project version
 ###############################################################################
 set(KLEE_VERSION_MAJOR 3)
-set(KLEE_VERSION_MINOR 0-utbot)
+set(KLEE_VERSION_MINOR 0)
 set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}")
 
 # If a patch is needed, we can add KLEE_VERSION_PATCH
 # set(KLEE_VERSION_PATCH 0)
 # set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}.${KLEE_VERSION_PATCH}")
 
-message(STATUS "KLEE version ${KLEE_VERSION}")
-set(PACKAGE_STRING "\"KLEE ${KLEE_VERSION}\"")
-set(PACKAGE_URL "\"https://klee.github.io\"")
+message(STATUS "KLEEF version ${KLEE_VERSION}")
+set(PACKAGE_STRING "\"KLEEF ${KLEE_VERSION}\"")
+set(PACKAGE_URL "\"https://toolchain-labs.com/projects/kleef.html\"")
 
 ################################################################################
 # Sanity check - Disallow building in source.
@@ -506,19 +506,29 @@ endif()
 # KLEE uclibc support
 ################################################################################
 set(KLEE_UCLIBC_PATH "" CACHE PATH "Path to klee-uclibc root directory")
-set(KLEE_UCLIBC_BCA_NAME "klee-uclibc.bca")
+
+set(KLEE_UCLIBC_BCA_32_NAME "klee-uclibc-32.bca")
+set(KLEE_UCLIBC_BCA_64_NAME "klee-uclibc-64.bca")
+
 if (NOT KLEE_UCLIBC_PATH STREQUAL "")
   # Find the C library bitcode archive
-  set(KLEE_UCLIBC_C_BCA "${KLEE_UCLIBC_PATH}/lib/libc.a")
-  if (NOT EXISTS "${KLEE_UCLIBC_C_BCA}")
+  set(KLEE_UCLIBC_C_32_BCA "${KLEE_UCLIBC_PATH}-32/lib/libc.a")
+  set(KLEE_UCLIBC_C_64_BCA "${KLEE_UCLIBC_PATH}-64/lib/libc.a")
+
+  if (NOT EXISTS "${KLEE_UCLIBC_C_32_BCA}" OR NOT EXISTS "${KLEE_UCLIBC_C_64_BCA}")
     message(FATAL_ERROR
-      "klee-uclibc library not found at \"${KLEE_UCLIBC_C_BCA}\". Set KLEE_UCLIBC_PATH to klee-uclibc root directory or empty string.")
+      "klee-uclibc library not found at \"${KLEE_UCLIBC_C_32_BCA}\" or \"${KLEE_UCLIBC_C_64_BCA}\". Set KLEE_UCLIBC_PATH to klee-uclibc root directory or empty string.")
   endif()
-  message(STATUS "Found klee-uclibc library: \"${KLEE_UCLIBC_C_BCA}\"")
+  message(STATUS "Found klee-uclibc library: \"${KLEE_UCLIBC_C_32_BCA}\" and \"${KLEE_UCLIBC_C_64_BCA}\"")
   # Copy KLEE_UCLIBC_C_BCA so KLEE can find it where it is expected.
+  # Create 32 and 64 bit versions
+  execute_process(COMMAND ${CMAKE_COMMAND} -E copy
+    "${KLEE_UCLIBC_C_32_BCA}"
+    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_32_NAME}"
+  )
   execute_process(COMMAND ${CMAKE_COMMAND} -E copy
-    "${KLEE_UCLIBC_C_BCA}"
-    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_NAME}"
+    "${KLEE_UCLIBC_C_64_BCA}"
+    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_64_NAME}"
   )
 else()
   message(STATUS "Skipping copying of klee-uclibc runtime")
@@ -633,6 +643,12 @@ unset(_flags)
 configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/config.h.cmin
   ${CMAKE_BINARY_DIR}/include/klee/Config/config.h)
 
+################################################################################
+# Generate `klee/klee.h` and `klee-test-comp.c`
+################################################################################
+configure_file(${CMAKE_SOURCE_DIR}/include/klee/klee.h ${CMAKE_BINARY_DIR}/include/klee/klee.h COPYONLY)
+configure_file(${CMAKE_SOURCE_DIR}/include/klee-test-comp.c ${CMAKE_BINARY_DIR}/include/klee-test-comp.c COPYONLY)
+
 ################################################################################
 # Generate `CompileTimeInfo.h`
 ################################################################################

README.md

@@ -1,27 +1,9 @@
-KLEE Symbolic Virtual Machine
+KLEEF Symbolic Virtual Machine
 =============================
 
-[![Build Status](https://github.com/klee/klee/workflows/CI/badge.svg)](https://github.com/klee/klee/actions?query=workflow%3ACI)
-[![Build Status](https://api.cirrus-ci.com/github/klee/klee.svg)](https://cirrus-ci.com/github/klee/klee)
-[![Coverage](https://codecov.io/gh/klee/klee/branch/master/graph/badge.svg)](https://codecov.io/gh/klee/klee)
+[![Build Status](https://github.com/UnitTestBot/klee/workflows/CI/badge.svg)](https://github.com/UnitTestBot/klee/actions?query=workflow%3ACI)
+[![Coverage](https://codecov.io/gh/UnitTestBot/klee/branch/main/graph/badge.svg)](https://codecov.io/gh/UnitTestBot/klee)
 
-`KLEE` is a symbolic virtual machine built on top of the LLVM compiler
-infrastructure. Currently, there are two primary components:
+`KLEEF` is a complete overhaul of the KLEE symbolic execution engine for LLVM, fine-tuned for a robust analysis of industrial C/C++ code.
 
-  1. The core symbolic virtual machine engine; this is responsible for
-     executing LLVM bitcode modules with support for symbolic
-     values. This is comprised of the code in lib/.
-
-  2. A POSIX/Linux emulation layer oriented towards supporting uClibc,
-     with additional support for making parts of the operating system
-     environment symbolic.
-
-Additionally, there is a simple library for replaying computed inputs
-on native code (for closed programs). There is also a more complicated
-infrastructure for replaying the inputs generated for the POSIX/Linux
-emulation layer, which handles running native programs in an
-environment that matches a computed test input, including setting up
-files, pipes, environment variables, and passing command line
-arguments.
-
-For further information, see the [webpage](http://klee.github.io/).
+For further information, see the [webpage](https://toolchain-labs.com/projects/kleef.html).

build.sh

@@ -29,9 +29,9 @@ SQLITE_VERSION="3400100"
 ## LLVM Required options
 LLVM_VERSION=14
 ENABLE_OPTIMIZED=1
-ENABLE_DEBUG=1
+ENABLE_DEBUG=0
 DISABLE_ASSERTIONS=1
-REQUIRES_RTTI=1
+REQUIRES_RTTI=0
 
 ## Solvers Required options
 # SOLVERS=STP

include/klee-test-comp.c

@@ -7,31 +7,42 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include <stdint.h>
 #ifdef EXTERNAL
 #include "klee.h"
 #include <assert.h>
 #include <stddef.h>
-#include <stdint.h>
 #include <stdlib.h>
 #else
 void klee_make_symbolic(void *addr, unsigned int nbytes, const char *name);
 void klee_assume(_Bool condition);
 __attribute__((noreturn)) void klee_silent_exit(int status);
 void __assert_fail(const char *assertion, const char *file, unsigned int line,
                    const char *function);
+void klee_prefer_cex(void *, uintptr_t);
 #endif
 
 int __VERIFIER_nondet_int(void) {
   int x;
   klee_make_symbolic(&x, sizeof(x), "int");
+  klee_prefer_cex(&x, x < 1024);
   return x;
 }
 
 unsigned int __VERIFIER_nondet_uint(void) {
   unsigned int x;
   klee_make_symbolic(&x, sizeof(x), "unsigned int");
+  klee_prefer_cex(&x, x < 1024);
+  return x;
+}
+
+#ifdef __x86_64__
+unsigned __int128 __VERIFIER_nondet_uint128(void) {
+  unsigned __int128 x;
+  klee_make_symbolic(&x, sizeof(x), "unsigned __int128");
   return x;
 }
+#endif
 
 unsigned __VERIFIER_nondet_unsigned(void) {
   unsigned x;
@@ -82,7 +93,7 @@ unsigned long __VERIFIER_nondet_ulong(void) {
 }
 
 double __VERIFIER_nondet_double(void) {
-  long x;
+  double x;
   klee_make_symbolic(&x, sizeof(x), "double");
   return x;
 }
@@ -96,7 +107,7 @@ void *__VERIFIER_nondet_pointer(void) {
 }
 
 float __VERIFIER_nondet_float(void) {
-  int x;
+  float x;
   klee_make_symbolic(&x, sizeof(x), "float");
   return x;
 }

include/klee/ADT/DisjointSetUnion.h

@@ -0,0 +1,172 @@
+#ifndef KLEE_DISJOINEDSETUNION_H
+#define KLEE_DISJOINEDSETUNION_H
+
+#include "klee/ADT/Either.h"
+#include "klee/ADT/PersistentMap.h"
+#include "klee/ADT/PersistentSet.h"
+#include "klee/ADT/Ref.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/Symcrete.h"
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
+
+#include <map>
+#include <set>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+namespace klee {
+using ExprEitherSymcrete = either<Expr, Symcrete>;
+
+template <typename ValueType, typename SetType,
+          typename HASH = std::hash<ValueType>,
+          typename PRED = std::equal_to<ValueType>,
+          typename CMP = std::less<ValueType>>
+class DisjointSetUnion {
+public:
+  using internal_storage_ty = std::unordered_set<ValueType, HASH, PRED>;
+  using disjoint_sets_ty =
+      std::unordered_map<ValueType, ref<const SetType>, HASH, PRED>;
+  using iterator = typename internal_storage_ty::iterator;
+
+protected:
+  std::unordered_map<ValueType, ValueType, HASH, PRED> parent;
+  std::set<ValueType, CMP> roots;
+  std::unordered_map<ValueType, size_t, HASH, PRED> rank;
+
+  std::unordered_set<ValueType, HASH, PRED> internalStorage;
+  std::unordered_map<ValueType, ref<const SetType>, HASH, PRED> disjointSets;
+
+  ValueType find(const ValueType &v) { // findparent
+    assert(parent.find(v) != parent.end());
+    if (v == parent.at(v))
+      return v;
+    parent.insert_or_assign(v, find(parent.at(v)));
+    return parent.at(v);
+  }
+
+  ValueType constFind(const ValueType &v) const {
+    assert(parent.find(v) != parent.end());
+    ValueType v1 = parent.at(v);
+    if (v == v1)
+      return v;
+    return constFind(v1);
+  }
+
+  void merge(ValueType a, ValueType b) {
+    a = find(a);
+    b = find(b);
+    if (a == b) {
+      return;
+    }
+
+    if (rank.at(a) < rank.at(b)) {
+      std::swap(a, b);
+    }
+    parent.insert_or_assign(b, a);
+    if (rank.at(a) == rank.at(b)) {
+      rank.insert_or_assign(a, rank.at(a) + 1);
+    }
+
+    roots.erase(b);
+    disjointSets.insert_or_assign(
+        a, SetType::merge(disjointSets.at(a), disjointSets.at(b)));
+    disjointSets.erase(b);
+  }
+
+  bool areJoined(const ValueType &i, const ValueType &j) const {
+    return constFind(i) == constFind(j);
+  }
+
+public:
+  iterator begin() const { return internalStorage.begin(); }
+  iterator end() const { return internalStorage.end(); }
+
+  size_t numberOfValues() const noexcept { return internalStorage.size(); }
+
+  size_t numberOfGroups() const noexcept { return disjointSets.size(); }
+
+  bool empty() const noexcept { return numberOfValues() == 0; }
+
+  ref<const SetType> findGroup(const ValueType &i) const {
+    return disjointSets.find(constFind(i))->second;
+  }
+
+  ref<const SetType> findGroup(iterator it) const {
+    return disjointSets.find(constFind(*it))->second;
+  }
+
+  void addValue(const ValueType value) {
+    if (internalStorage.find(value) != internalStorage.end()) {
+      return;
+    }
+    parent.insert({value, value});
+    roots.insert(value);
+    rank.insert({value, 0});
+    disjointSets.insert({value, new SetType(value)});
+
+    internalStorage.insert(value);
+    std::set<ValueType, CMP> oldRoots = roots;
+    for (ValueType v : oldRoots) {
+      if (!areJoined(v, value) &&
+          SetType::intersects(disjointSets.at(find(v)),
+                              disjointSets.at(find(value)))) {
+        merge(v, value);
+      }
+    }
+  }
+  void getAllIndependentSets(std::vector<ref<const SetType>> &result) const {
+    for (ValueType v : roots)
+      result.push_back(findGroup(v));
+  }
+
+  void add(const DisjointSetUnion &b) {
+    std::set<ValueType, CMP> oldRoots = roots;
+    std::set<ValueType, CMP> newRoots = b.roots;
+    for (auto it : b.parent) {
+      parent.insert(it);
+    }
+    for (auto it : b.roots) {
+      roots.insert(it);
+    }
+    for (auto it : b.rank) {
+      rank.insert(it);
+    }
+    for (auto it : b.internalStorage) {
+      internalStorage.insert(it);
+    }
+    for (auto it : b.disjointSets) {
+      disjointSets.insert(it);
+    }
+    for (ValueType nv : newRoots) {
+      for (ValueType ov : oldRoots) {
+        if (!areJoined(ov, nv) &&
+            SetType::intersects(disjointSets.at(find(ov)),
+                                disjointSets.at(find(nv)))) {
+          merge(ov, nv);
+        }
+      }
+    }
+  }
+
+  DisjointSetUnion() {}
+
+  DisjointSetUnion(const internal_storage_ty &is) {
+    for (ValueType v : is) {
+      addValue(v);
+    }
+  }
+
+public:
+  internal_storage_ty is() const { return internalStorage; }
+
+  disjoint_sets_ty ds() const { return disjointSets; }
+};
+} // namespace klee
+
+#endif /* KLEE_DISJOINEDSETUNION_H */