klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExecutionState.h
Go to the documentation of this file.
1 //===-- ExecutionState.h ----------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_EXECUTIONSTATE_H
11 #define KLEE_EXECUTIONSTATE_H
12 
13 #include "klee/Constraints.h"
14 #include "klee/Expr.h"
16 
17 // FIXME: We do not want to be exposing these? :(
18 #include "../../lib/Core/AddressSpace.h"
20 
21 #include <map>
22 #include <set>
23 #include <vector>
24 
25 namespace klee {
26  class Array;
27  class CallPathNode;
28  struct Cell;
29  struct KFunction;
30  struct KInstruction;
31  class MemoryObject;
32  class PTreeNode;
33  struct InstructionInfo;
34 
35 llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
36 
37 struct StackFrame {
41 
42  std::vector<const MemoryObject*> allocas;
44 
51 
52  // For vararg functions: arguments not passed via parameter are
53  // stored (packed tightly) in a local (alloca) memory object. This
54  // is setup to match the way the front-end generates vaarg code (it
55  // does not pass vaarg through as expected). VACopy is lowered inside
56  // of intrinsic lowering.
58 
60  StackFrame(const StackFrame &s);
61  ~StackFrame();
62 };
63 
65 public:
66  typedef std::vector<StackFrame> stack_ty;
67 
68 private:
69  // unsupported, use copy constructor
71  std::map< std::string, std::string > fnAliases;
72 
73 public:
74  bool fakeState;
75  // Are we currently underconstrained? Hack: value is size to make fake
76  // objects.
77  unsigned underConstrained;
78  unsigned depth;
79 
80  // pc - pointer to current instruction stream
84  mutable double queryCost;
85  double weight;
88  unsigned instsSinceCovNew;
89  bool coveredNew;
90 
93 
94  std::map<const std::string*, std::set<unsigned> > coveredLines;
96 
98  //
99  // FIXME: Move to a shared list structure (not critical).
100  std::vector< std::pair<const MemoryObject*, const Array*> > symbolics;
101 
103  std::set<std::string> arrayNames;
104 
105  // Used by the checkpoint/rollback methods for fake objects.
106  // FIXME: not freeing things on branch deletion.
108 
109  unsigned incomingBBIndex;
110 
111  std::string getFnAlias(std::string fn);
112  void addFnAlias(std::string old_fn, std::string new_fn);
113  void removeFnAlias(std::string fn);
114 
115 private:
117 
118 public:
120 
121  // XXX total hack, just used to make a state so solver can
122  // use on structure
123  ExecutionState(const std::vector<ref<Expr> > &assumptions);
124 
125  ExecutionState(const ExecutionState& state);
126 
127  ~ExecutionState();
128 
130 
131  void pushFrame(KInstIterator caller, KFunction *kf);
132  void popFrame();
133 
134  void addSymbolic(const MemoryObject *mo, const Array *array);
137  }
138 
139  bool merge(const ExecutionState &b);
140  void dumpStack(llvm::raw_ostream &out) const;
141 };
142 
143 }
144 
145 #endif
bool merge(const ExecutionState &b)
void dumpStack(llvm::raw_ostream &out) const
StackFrame(KInstIterator caller, KFunction *kf)
ExecutionState * branch()
void addConstraint(ref< Expr > e)
std::vector< StackFrame > stack_ty
llvm::raw_ostream & operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
std::vector< std::pair< const MemoryObject *, const Array * > > symbolics
ordered list of symbolics: used to generate test cases.
std::map< const std::string *, std::set< unsigned > > coveredLines
std::vector< const MemoryObject * > allocas
CallPathNode * callPathNode
std::set< std::string > arrayNames
Set of used array names. Used to avoid collisions.
void addFnAlias(std::string old_fn, std::string new_fn)
AddressSpace addressSpace
std::string getFnAlias(std::string fn)
KFunction * kf
void pushFrame(KInstIterator caller, KFunction *kf)
std::map< std::string, std::string > fnAliases
void removeFnAlias(std::string fn)
ConstraintManager constraints
KInstIterator prevPC
bool forkDisabled
Disables forking, set by user code.
KInstIterator caller
void addConstraint(ref< Expr > e)
ImmutableMap< const MemoryObject *, ObjectHolder, MemoryObjectLT > MemoryMap
Definition: AddressSpace.h:34
MemoryObject * varargs
ExecutionState & operator=(const ExecutionState &)
void addSymbolic(const MemoryObject *mo, const Array *array)
unsigned minDistToUncoveredOnReturn