2323#include " klee/util/Assignment.h"
2424#include " IAddressSpaceNotification.h"
2525
26+ #include " IExecutionState.h"
27+ #include " LLVMExecutionState.h"
28+
2629#include < map>
2730#include < set>
2831#include < vector>
@@ -34,88 +37,74 @@ struct KInstruction;
3437
3538llvm::raw_ostream &operator <<(llvm::raw_ostream &os, const MemoryMap &mm);
3639
37- struct StackFrame {
38- KInstIterator caller;
39- KFunction *kf;
40-
41- llvm::SmallVector<ObjectKey, 16 > allocas;
42- llvm::SmallVector<Cell, 16 > locals;
43-
44- // For vararg functions: arguments not passed via parameter are
45- // stored (packed tightly) in a local (alloca) memory object. This
46- // is setup to match the way the front-end generates vaarg code (it
47- // does not pass vaarg through as expected). VACopy is lowered inside
48- // of intrinsic lowering.
49- std::vector<ObjectKey> varargs;
50-
51- StackFrame (KInstIterator _caller, KFunction *_kf) : caller(_caller), kf(_kf), varargs(0 ) {
52- locals.resize (kf->getNumRegisters ());
53- }
54- };
55-
56- class ExecutionState : public IAddressSpaceNotification {
57- friend class AddressSpace ;
58-
40+ class ExecutionState : public IExecutionState , public IAddressSpaceNotification {
5941public:
60- typedef llvm::SmallVector<StackFrame, 16 > stack_ty;
61-
6242 // / Set of objects that should not be merged by the base merge function.
6343 // / Overloaded functions will take care of it.
6444 static std::set<ObjectKey, ObjectKeyLTS> s_ignoredMergeObjects;
6545
6646private:
6747 SolverPtr m_solver;
48+ AddressSpace m_addressSpace;
6849
69- public:
70- // pc - pointer to current instruction stream
71- KInstIterator pc, prevPC;
72- stack_ty stack;
73- AddressSpace addressSpace;
74-
75- // / Disables forking, set by user code.
76- bool forkDisabled;
77-
78- // / ordered list of symbolics: used to generate test cases.
79- std::vector<ArrayPtr> symbolics;
80-
81- AssignmentPtr concolics;
82-
83- unsigned incomingBBIndex;
84-
85- private:
8650 // / Simplifier user to simplify expressions when adding them
8751 static BitfieldSimplifier s_simplifier;
8852
8953 ConstraintManager m_constraints;
9054
91- ExecutionState () : addressSpace (this ) {
55+ ExecutionState () : m_addressSpace( this ), llvm (this ) {
9256 }
9357
9458protected:
59+ // / ordered list of symbolics: used to generate test cases.
60+ std::vector<ArrayPtr> m_symbolics;
61+ AssignmentPtr m_concolics;
62+
9563 virtual void addressSpaceChange (const klee::ObjectKey &key, const ObjectStateConstPtr &oldState,
9664 const ObjectStatePtr &newState);
9765
9866 virtual void addressSpaceObjectSplit (const ObjectStateConstPtr &oldObject,
9967 const std::vector<ObjectStatePtr> &newObjects);
10068
10169public:
70+ // / Disables forking, set by user code.
71+ bool forkDisabled;
72+ LLVMExecutionState llvm;
73+
74+ virtual SolverPtr solver () {
75+ return m_solver;
76+ }
77+
78+ virtual AddressSpace &addressSpace () {
79+ return m_addressSpace;
80+ }
81+
82+ virtual const AddressSpace &addressSpace () const {
83+ return m_addressSpace;
84+ }
85+
86+ virtual const std::vector<ArrayPtr> &symbolics () const {
87+ return m_symbolics;
88+ }
89+
90+ virtual const AssignmentPtr concolics () const {
91+ return m_concolics;
92+ }
93+
94+ virtual void setConcolics (AssignmentPtr concolics) {
95+ m_concolics = concolics;
96+ }
97+
10298 // Fired whenever an object becomes all concrete or gets at least one symbolic byte.
10399 // Only fired in the context of a memory operation (load/store)
104100 virtual void addressSpaceSymbolicStatusChange (const ObjectStatePtr &object, bool becameConcrete);
105101
106102 ExecutionState (KFunction *kf);
107103
108- // XXX total hack, just used to make a state so solver can
109- // use on structure
110- ExecutionState (const std::vector<ref<Expr>> &assumptions);
111-
112104 virtual ~ExecutionState ();
113105
114106 virtual ExecutionState *clone ();
115107
116- void pushFrame (KInstIterator caller, KFunction *kf);
117- void popFrame ();
118-
119108 const ConstraintManager &constraints () const {
120109 return m_constraints;
121110 }
@@ -145,8 +134,6 @@ class ExecutionState : public IAddressSpaceNotification {
145134
146135 virtual bool merge (const ExecutionState &b);
147136
148- void printStack (std::stringstream &msg) const ;
149-
150137 bool getSymbolicSolution (std::vector<std::pair<std::string, std::vector<unsigned char >>> &res);
151138
152139 ref<Expr> simplifyExpr (const ref<Expr> &e) const ;
@@ -168,13 +155,6 @@ class ExecutionState : public IAddressSpaceNotification {
168155
169156 SolverPtr solver () const ;
170157
171- Cell &getArgumentCell (KFunction *kf, unsigned index);
172- Cell &getDestCell (KInstruction *target);
173-
174- void bindLocal (KInstruction *target, ref<Expr> value);
175- void bindArgument (KFunction *kf, unsigned index, ref<Expr> value);
176- void stepInstruction ();
177-
178158 // Given a concrete object in our [klee's] address space, add it to
179159 // objects checked code can reference.
180160 ObjectStatePtr addExternalObject (void *addr, unsigned size, bool isReadOnly, bool isSharedConcrete = false );
@@ -203,7 +183,8 @@ class ExecutionState : public IAddressSpaceNotification {
203183 void executeAlloc (ref<Expr> size, bool isLocal, KInstruction *target, bool zeroMemory = false ,
204184 const ObjectStatePtr &reallocFrom = nullptr );
205185
206- void transferToBasicBlock (llvm::BasicBlock *dst, llvm::BasicBlock *src);
186+ ref<Expr> executeMemoryRead (uint64_t concreteAddress, unsigned bytes);
187+ void executeMemoryWrite (uint64_t concreteAddress, const ref<Expr> &value);
207188};
208189} // namespace klee
209190
0 commit comments