Various refactorings (round #1)

Dockerfile

@@ -26,7 +26,7 @@ FROM ubuntu:22.04 AS s2e-build-env
 # The unzip and libgomp1 dependencies are needed to unzip and run binary Z3
 # distributions.
 
-RUN dpkg --add-architecture i386 && apt-get update &&                       \
+RUN apt-get update && dpkg --add-architecture i386 && apt-get update &&                       \
     apt-get -y install sudo git ca-certificates build-essential cmake curl wget texinfo flex bison  \
     python-is-python3 python3-dev python3-venv python3-distro mingw-w64 lsb-release \
     autoconf libtool libprotobuf-dev protobuf-compiler protobuf-c-compiler \

guest/CMakeLists.txt

@@ -39,7 +39,7 @@ include_directories("common/include")
 
 # Determine the architecture to build for. By default build for 64-bit
 set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -std=gnu99 -Werror -g")
-set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -std=c++17 -Werror -g")
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -std=c++20 -Werror -g")
 if(NOT BITS)
   message(FATAL_ERROR "BITS is not set")
 endif()

klee/CMakeLists.txt

@@ -211,11 +211,11 @@ endif()
 # C++ version
 ################################################################################
 
-message(STATUS "Enabling C++17")
+message(STATUS "Enabling C++20")
 # FIXME: Use CMake's own mechanism for managing C++ version.
 # Set globally because it is unlikely we would want to compile
 # using mixed C++ versions.
-add_global_cxx_flag("-std=c++17" REQUIRED)
+add_global_cxx_flag("-std=c++20" REQUIRED)
 
 # Uncomment this to enable code coverage recording
 # set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fprofile-instr-generate -fcoverage-mapping")

klee/include/klee/AddressSpace.h

@@ -82,6 +82,9 @@ class AddressSpace {
     using IterateWriteCb = std::function<bool(ObjectStatePtr &, unsigned offset, unsigned size)>;
     bool iterateWrite(uintptr_t hostAddress, size_t size, IterateWriteCb cb, AddressTranslator tr);
 
+    /// ExecutionState that owns this AddressSpace
+    IAddressSpaceNotification *m_state = nullptr;
+
 protected:
     /// Unsupported, use copy constructor
     AddressSpace &operator=(const AddressSpace &);
@@ -103,19 +106,20 @@ class AddressSpace {
     /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey
     MemoryMap objects;
 
-    /// ExecutionState that owns this AddressSpace
-    IAddressSpaceNotification *state;
-
 public:
-    AddressSpace(IAddressSpaceNotification *_state) : cowKey(1), state(_state) {
+    AddressSpace(IAddressSpaceNotification *state) : cowKey(1), m_state(state) {
     }
 
-    AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) {
+    AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), m_state(b.m_state), objects(b.objects) {
     }
 
     ~AddressSpace() {
     }
 
+    void setState(IAddressSpaceNotification *state) {
+        m_state = state;
+    }
+
     /// Add a binding to the address space.
     void bindObject(const ObjectStatePtr &os);
 

klee/include/klee/ExecutionState.h

@@ -23,6 +23,9 @@
 #include "klee/util/Assignment.h"
 #include "IAddressSpaceNotification.h"
 
+#include "IExecutionState.h"
+#include "LLVMExecutionState.h"
+
 #include <map>
 #include <set>
 #include <vector>
@@ -34,88 +37,74 @@ struct KInstruction;
 
 llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
 
-struct StackFrame {
-    KInstIterator caller;
-    KFunction *kf;
-
-    llvm::SmallVector<ObjectKey, 16> allocas;
-    llvm::SmallVector<Cell, 16> locals;
-
-    // For vararg functions: arguments not passed via parameter are
-    // stored (packed tightly) in a local (alloca) memory object. This
-    // is setup to match the way the front-end generates vaarg code (it
-    // does not pass vaarg through as expected). VACopy is lowered inside
-    // of intrinsic lowering.
-    std::vector<ObjectKey> varargs;
-
-    StackFrame(KInstIterator _caller, KFunction *_kf) : caller(_caller), kf(_kf), varargs(0) {
-        locals.resize(kf->getNumRegisters());
-    }
-};
-
-class ExecutionState : public IAddressSpaceNotification {
-    friend class AddressSpace;
-
+class ExecutionState : public IExecutionState, public IAddressSpaceNotification {
 public:
-    typedef llvm::SmallVector<StackFrame, 16> stack_ty;
-
     /// Set of objects that should not be merged by the base merge function.
     /// Overloaded functions will take care of it.
     static std::set<ObjectKey, ObjectKeyLTS> s_ignoredMergeObjects;
 
 private:
     SolverPtr m_solver;
+    AddressSpace m_addressSpace;
 
-public:
-    // pc - pointer to current instruction stream
-    KInstIterator pc, prevPC;
-    stack_ty stack;
-    AddressSpace addressSpace;
-
-    /// Disables forking, set by user code.
-    bool forkDisabled;
-
-    /// ordered list of symbolics: used to generate test cases.
-    std::vector<ArrayPtr> symbolics;
-
-    AssignmentPtr concolics;
-
-    unsigned incomingBBIndex;
-
-private:
     /// Simplifier user to simplify expressions when adding them
     static BitfieldSimplifier s_simplifier;
 
     ConstraintManager m_constraints;
 
-    ExecutionState() : addressSpace(this) {
+    ExecutionState() : m_addressSpace(this), llvm(this) {
     }
 
 protected:
+    /// ordered list of symbolics: used to generate test cases.
+    std::vector<ArrayPtr> m_symbolics;
+    AssignmentPtr m_concolics;
+
     virtual void addressSpaceChange(const klee::ObjectKey &key, const ObjectStateConstPtr &oldState,
                                     const ObjectStatePtr &newState);
 
     virtual void addressSpaceObjectSplit(const ObjectStateConstPtr &oldObject,
                                          const std::vector<ObjectStatePtr> &newObjects);
 
 public:
+    /// Disables forking, set by user code.
+    bool forkDisabled;
+    LLVMExecutionState llvm;
+
+    virtual SolverPtr solver() {
+        return m_solver;
+    }
+
+    virtual AddressSpace &addressSpace() {
+        return m_addressSpace;
+    }
+
+    virtual const AddressSpace &addressSpace() const {
+        return m_addressSpace;
+    }
+
+    virtual const std::vector<ArrayPtr> &symbolics() const {
+        return m_symbolics;
+    }
+
+    virtual const AssignmentPtr concolics() const {
+        return m_concolics;
+    }
+
+    virtual void setConcolics(AssignmentPtr concolics) {
+        m_concolics = concolics;
+    }
+
     // Fired whenever an object becomes all concrete or gets at least one symbolic byte.
     // Only fired in the context of a memory operation (load/store)
     virtual void addressSpaceSymbolicStatusChange(const ObjectStatePtr &object, bool becameConcrete);
 
     ExecutionState(KFunction *kf);
 
-    // XXX total hack, just used to make a state so solver can
-    // use on structure
-    ExecutionState(const std::vector<ref<Expr>> &assumptions);
-
     virtual ~ExecutionState();
 
     virtual ExecutionState *clone();
 
-    void pushFrame(KInstIterator caller, KFunction *kf);
-    void popFrame();
-
     const ConstraintManager &constraints() const {
         return m_constraints;
     }
@@ -145,8 +134,6 @@ class ExecutionState : public IAddressSpaceNotification {
 
     virtual bool merge(const ExecutionState &b);
 
-    void printStack(std::stringstream &msg) const;
-
     bool getSymbolicSolution(std::vector<std::pair<std::string, std::vector<unsigned char>>> &res);
 
     ref<Expr> simplifyExpr(const ref<Expr> &e) const;
@@ -168,13 +155,6 @@ class ExecutionState : public IAddressSpaceNotification {
 
     SolverPtr solver() const;
 
-    Cell &getArgumentCell(KFunction *kf, unsigned index);
-    Cell &getDestCell(KInstruction *target);
-
-    void bindLocal(KInstruction *target, ref<Expr> value);
-    void bindArgument(KFunction *kf, unsigned index, ref<Expr> value);
-    void stepInstruction();
-
     // Given a concrete object in our [klee's] address space, add it to
     // objects checked code can reference.
     ObjectStatePtr addExternalObject(void *addr, unsigned size, bool isReadOnly, bool isSharedConcrete = false);
@@ -203,7 +183,8 @@ class ExecutionState : public IAddressSpaceNotification {
     void executeAlloc(ref<Expr> size, bool isLocal, KInstruction *target, bool zeroMemory = false,
                       const ObjectStatePtr &reallocFrom = nullptr);
 
-    void transferToBasicBlock(llvm::BasicBlock *dst, llvm::BasicBlock *src);
+    ref<Expr> executeMemoryRead(uint64_t concreteAddress, unsigned bytes);
+    void executeMemoryWrite(uint64_t concreteAddress, const ref<Expr> &value);
 };
 } // namespace klee
 

klee/include/klee/Executor.h

@@ -60,42 +60,52 @@ class BitfieldSimplifier;
 class SolverFactory;
 template <class T> class ref;
 
+class LLVMExecutorException : public std::runtime_error {
+public:
+    LLVMExecutorException(const std::string &msg) : std::runtime_error(msg) {
+    }
+};
+
 class Executor {
 public:
     typedef std::pair<ExecutionState *, ExecutionState *> StatePair;
 
 protected:
-    KModulePtr kmodule;
-    Searcher *searcher;
+    // ======= LLVM management =======
+    KModulePtr m_kmodule;
+    /// The set of functions that must be handled via custom function handlers
+    /// instead of being called directly.
+    std::set<llvm::Function *> m_overridenInternalFunctions;
+
+    /// Map of globals to their bound address. This also includes
+    /// globals that have no representative object (i.e. functions).
+    GlobalAddresses m_globalAddresses;
+
+    /// Map of globals to their representative memory object.
+    std::map<const llvm::GlobalValue *, ObjectKey> m_globalObjects;
+
+    /// Map of predefined global values
+    std::map<std::string, void *> m_predefinedSymbols;
+
+    std::unique_ptr<SpecialFunctionHandler> m_specialFunctionHandler;
+
+    // ======= Misc =======
 
-    ExternalDispatcher *externalDispatcher;
-    StateSet states;
-    SpecialFunctionHandler *specialFunctionHandler;
+    std::unique_ptr<ExternalDispatcher> m_externalDispatcher;
 
+    // ======= Execution state management =======
+    Searcher *m_searcher;
+    StateSet m_states;
     /// Used to track states that have been added during the current
     /// instructions step.
     /// \invariant \ref addedStates is a subset of \ref states.
     /// \invariant \ref addedStates and \ref removedStates are disjoint.
-    StateSet addedStates;
+    StateSet m_addedStates;
     /// Used to track states that have been removed during the current
     /// instructions step.
     /// \invariant \ref removedStates is a subset of \ref states.
     /// \invariant \ref addedStates and \ref removedStates are disjoint.
-    StateSet removedStates;
-
-    /// Map of predefined global values
-    std::map<std::string, void *> predefinedSymbols;
-
-    /// Map of globals to their representative memory object.
-    std::map<const llvm::GlobalValue *, ObjectKey> globalObjects;
-
-    /// Map of globals to their bound address. This also includes
-    /// globals that have no representative object (i.e. functions).
-    GlobalAddresses globalAddresses;
-
-    /// The set of functions that must be handled via custom function handlers
-    /// instead of being called directly.
-    std::set<llvm::Function *> overridenInternalFunctions;
+    StateSet m_removedStates;
 
     llvm::Function *getTargetFunction(llvm::Value *calledVal);
 
@@ -112,9 +122,6 @@ class Executor {
 
     void executeCall(ExecutionState &state, KInstruction *ki, llvm::Function *f, std::vector<ref<Expr>> &arguments);
 
-    ref<Expr> executeMemoryOperation(ExecutionState &state, bool isWrite, uint64_t concreteAddress,
-                                     ref<Expr> value /* undef if read */, unsigned bytes);
-
     // do address resolution / object binding / out of bounds checking
     // and perform the operation
     void executeMemoryOperation(ExecutionState &state, bool isWrite, ref<Expr> address,
@@ -131,13 +138,11 @@ class Executor {
     /// allows plugins to kill states and exit to the CPU loop safely.
     virtual void notifyFork(ExecutionState &originalState, ref<Expr> &condition, Executor::StatePair &targets);
 
-    const Cell &eval(KInstruction *ki, unsigned index, ExecutionState &state) const;
+    const Cell &eval(KInstruction *ki, unsigned index, LLVMExecutionState &state) const;
 
     // delete the state (called internally by terminateState and updateStates)
     virtual void deleteState(ExecutionState *state);
 
-    void handlePointsToObj(ExecutionState &state, KInstruction *target, const std::vector<ref<Expr>> &arguments);
-
     typedef void (*FunctionHandler)(Executor *executor, ExecutionState *state, KInstruction *target,
                                     std::vector<ref<Expr>> &arguments);
 
@@ -170,26 +175,22 @@ class Executor {
 
     /*** State accessor methods ***/
     size_t getStatesCount() const {
-        return states.size();
+        return m_states.size();
     }
     const StateSet &getStates() {
-        return states;
+        return m_states;
     }
 
     const StateSet &getAddedStates() {
-        return addedStates;
+        return m_addedStates;
     }
 
     const StateSet &getRemovedStates() {
-        return removedStates;
-    }
-
-    ExternalDispatcher *getDispatcher() const {
-        return externalDispatcher;
+        return m_removedStates;
     }
 
     KModulePtr getModule() const {
-        return kmodule;
+        return m_kmodule;
     }
 };