ROSE  0.11.145.0
PathNode.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_PathNode_H
2 #define ROSE_BinaryAnalysis_ModelChecker_PathNode_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
8 #include <Rose/BinaryAnalysis/SmtSolver.h>
9 #include <Rose/BinaryAnalysis/SymbolicExpression.h>
10 
11 namespace Rose {
12 namespace BinaryAnalysis {
13 namespace ModelChecker {
14 
15 /* One node of an execution path.
16  *
17  * An execution path node points to its predecessor, but the predecessor does not point back. Execution paths must always
18  * be referenced according to their final node, and all references are counted. This method of organizing the nodes has
19  * a number of advantages over bi-directional pointing.
20  *
21  * The execution nodes form a tree data structure. A worklist points to the leaves of the tree and worker threads try to
22  * advance the frontier. The tree is dynamically created by the workers, and parts of it are deleted when no longer
23  * required. */
24 class PathNode {
25 public:
27  using Ptr = PathNodePtr;
28 
29 private:
30  const Ptr parent_; // Previous node in execution path. Null for root node.
31  const ExecutionUnitPtr executionUnit_; // The thing to execute, non-null
32 
33  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects all following data members
34 
35  // Path states are used as follows:
36  //
37  // When a path is executed, its incomingState_ is copied, modified by the thread's semantics operators, and the
38  // resulting state is stored as outgoingState_. The incomingState_ (which is shared among paths, see next bullet) is
39  // then set to null.
40  //
41  // When a path is extended by creating new paths each with an additional node, the new nodes' incomingState_ points to
42  // the original path's outgoingState_, then the original path's outgoingState_ is set to null. Thus the new paths all
43  // point to a shared incoming state.
44  InstructionSemantics::BaseSemantics::StatePtr incomingState_; // shared state before execution, then null afterward
45  InstructionSemantics::BaseSemantics::StatePtr outgoingState_; // state after execution, or null if error during execution
46 
47  bool executionFailed_ = false; // true iff execution failed (and outgoingState_ therefore null)
48  std::vector<SymbolicExpression::Ptr> assertions_; // assertions for the model checker for this node of the path
49  SmtSolver::Evidence evidence_; // SMT evidence that path to and including this node is feasible
50  std::vector<TagPtr> tags_; // tags associated with this node of the path
51  uint32_t id_ = 0; // a random path ID number
52  double processingTime_ = NAN; // time required to execute and extend this node
53  double sortKey_ = NAN; // field for user-defined sorting
54 
55 protected:
56  PathNode() = delete;
57 
61  PathNode(const ExecutionUnitPtr&);
62 
66  PathNode(const Ptr &parent, const ExecutionUnitPtr&, const SymbolicExpression::Ptr &assertion,
67  const SmtSolver::Evidence&, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState);
68 
69 public:
70  ~PathNode();
71 
72 public:
78  static Ptr instance(const ExecutionUnitPtr&);
79 
87  static Ptr instance(const Ptr &parent, const ExecutionUnitPtr&, const SymbolicExpression::Ptr &assertion,
88  const SmtSolver::Evidence&, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState);
89 
95  uint32_t id() const;
96 
107  double sortKey() const;
108  void sortKey(double);
119  Ptr parent() const;
120 
129  ExecutionUnitPtr executionUnit() const;
130 
137  size_t nSteps() const;
138 
145  void assertion(const SymbolicExpression::Ptr&);
146 
150  std::vector<SymbolicExpression::Ptr> assertions() const;
151 
157  SmtSolver::Evidence evidence() const;
158 
168  void execute(const SettingsPtr&, const SemanticCallbacksPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
169  const SmtSolver::Ptr&);
170 
176  bool executionFailed() const;
177 
186  InstructionSemantics::BaseSemantics::StatePtr copyOutgoingState() const;
187 
188  class BorrowedOutgoingState {
189  friend class PathNode;
190  private:
191  PathNode* const node;
192  public:
194  private:
195  BorrowedOutgoingState() = delete;
196  BorrowedOutgoingState& operator=(const BorrowedOutgoingState&) = delete;
197  BorrowedOutgoingState(PathNode*, const InstructionSemantics::BaseSemantics::StatePtr&);
198  public:
199  ~BorrowedOutgoingState();
200  };
201 
221  BorrowedOutgoingState borrowOutgoingState();
222 
230  void releaseOutgoingState();
231 
239  void appendTag(const TagPtr&);
240  void appendTags(const std::vector<TagPtr>&);
246  size_t nTags() const;
247 
251  std::vector<TagPtr> tags() const;
252 
258  double processingTime() const;
259 
265  void incrementProcessingTime(double seconds);
266 
270  Sawyer::Optional<rose_addr_t> address() const;
271 
277  std::string printableName() const;
278 
282  void toYamlHeader(const SettingsPtr&, std::ostream&, const std::string &prefix) const;
283 
285  void toYamlSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
286  size_t stepOrigin, size_t maxSteps) const;
287 
288 private:
289  void restoreOutgoingState(const InstructionSemantics::BaseSemantics::StatePtr&);
290 };
291 
292 } // namespace
293 } // namespace
294 } // namespace
295 
296 #endif
297 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Main namespace for the ROSE library.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Id id(const std::string &name)
Returns the ID for an attribute name.
Sawyer::Container::Map< std::string, SymbolicExpression::Ptr > Evidence
Evidence of satisfiability.
Definition: SmtSolver.h:566
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.