ROSE  0.11.82.0
InputVariables.h
1 #ifndef ROSE_BinaryAnalysis_Concolic_InputVariables_H
2 #define ROSE_BinaryAnalysis_Concolic_InputVariables_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_CONCOLIC_TESTING
5 #include <Rose/BinaryAnalysis/Concolic/BasicTypes.h>
6 
7 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
8 
9 namespace Rose {
10 namespace BinaryAnalysis {
11 namespace Concolic {
12 
24 class InputVariables: public Sawyer::SharedObject {
25 public:
26  using Ptr = InputVariablesPtr;
27 
28 private:
29  using Variables = Sawyer::Container::Map<uint64_t, ExecutionEventPtr>; // map symbolic variable ID to program input
30  Variables variables_;
31  SymbolicExpr::ExprExprHashMap bindings_; // used for substitutions
32 
34  // Constructors, etc.
36 protected:
37  InputVariables();
38 
39 public:
41  static Ptr instance();
42 
43  ~InputVariables();
44 
46  // Properties and queries
48 public:
49 
54  const SymbolicExpr::ExprExprHashMap& bindings() const;
55 
62  ExecutionEventPtr event(const std::string &variableName) const;
63  ExecutionEventPtr event(const SymbolicExprPtr &variable) const;
66  // High-level functions.
69 
82  void activate(const ExecutionEventPtr&, InputType, size_t idx1 = INVALID_INDEX, size_t idx2 = INVALID_INDEX);
83 
93  void deactivate(const ExecutionEventPtr&);
94 
100  void playback(const ExecutionEventPtr&);
101 
106  void unplayback(const ExecutionEventPtr&);
107 
109  void addBindingsToSolver(const SmtSolverPtr&) const;
110 
112  void print(std::ostream&, const std::string &prefix = "") const;
113 
115  // Mid-level functions
117 
127  void define(const ExecutionEventPtr&, InputType, size_t idx1 = INVALID_INDEX, size_t idx2 = INVALID_INDEX);
128 
139  void undefine(const ExecutionEventPtr&);
140 
147  void bind(const ExecutionEventPtr&);
148 
158  void unbind(const ExecutionEventPtr&);
159 
161  // Low-level functions.
163 
168  void bindVariableValue(const SymbolicExprPtr &variable, const SymbolicExprPtr &value);
169 
174  void unbindVariableValue(const SymbolicExprPtr &variable);
175 };
176 
177 } // namespace
178 } // namespace
179 } // namespace
180 
181 #endif
182 #endif
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
Definition: SymbolicExpr.h:166
void print(const StackVariables &, const Partitioner2::Partitioner &, std::ostream &out, const std::string &prefix="")
Print info about multiple local variables.
Main namespace for the ROSE library.
Base class for reference counted objects.
Definition: SharedObject.h:64
const size_t INVALID_INDEX(-1)
Invalid array index.
Container associating values with keys.
Definition: Sawyer/Map.h:66
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:26