ROSE  0.11.50.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_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/Types.h>
8 #include <Rose/BinaryAnalysis/SmtSolver.h>
9 #include <Rose/BinaryAnalysis/SymbolicExpr.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  InstructionSemantics2::BaseSemantics::StatePtr incomingState_; // shared state before execution, then null afterward
45  InstructionSemantics2::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<SymbolicExpr::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  uint64_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 SymbolicExpr::Ptr &assertion,
67  const SmtSolver::Evidence&, const InstructionSemantics2::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 SymbolicExpr::Ptr &assertion,
88  const SmtSolver::Evidence&, const InstructionSemantics2::BaseSemantics::StatePtr &parentOutgoingState);
89 
95  uint64_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 SymbolicExpr::Ptr&);
146 
150  std::vector<SymbolicExpr::Ptr> assertions() const;
151 
158 
168  void execute(const SettingsPtr&, const SemanticCallbacksPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&,
169  const SmtSolver::Ptr&);
170 
176  bool executionFailed() const;
177 
187 
189  friend class PathNode;
190  private:
191  PathNode* const node;
192  public:
194  private:
195  BorrowedOutgoingState() = delete;
196  BorrowedOutgoingState& operator=(const BorrowedOutgoingState&) = delete;
198  public:
200  };
201 
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 
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 InstructionSemantics2::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:39
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
void appendTags(const std::vector< TagPtr > &)
Append tags.
double sortKey() const
Property: Key for user-defined sorting.
std::vector< SymbolicExpr::Ptr > assertions() const
Returns all the assersions for this node.
void incrementProcessingTime(double seconds)
Add additional time to the processing time.
void releaseOutgoingState()
Release the outgoing state.
std::string printableName() const
Printable name for this node.
PathNodePtr Ptr
Shared-ownership pointer.
Definition: PathNode.h:27
Sawyer::Optional< rose_addr_t > address() const
Address of execution unit.
static Ptr instance(const ExecutionUnitPtr &)
Construct a root node.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
void execute(const SettingsPtr &, const SemanticCallbacksPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &)
Execute this node.
SmtSolver::Evidence evidence() const
Returns the SMT solver evidence for path feasibility.
Main namespace for the ROSE library.
size_t nTags() const
Number of tags attached to this node.
Ptr parent() const
Property: Parent node.
bool executionFailed() const
Property: Whether execution has failed.
double processingTime() const
Time spent processing this node.
BorrowedOutgoingState borrowOutgoingState()
Borrow the state from a node.
size_t nSteps() const
Length of node in steps.
std::vector< TagPtr > tags() const
All tags for this node.
ExecutionUnitPtr executionUnit() const
Property: Unit of execution.
void assertion(const SymbolicExpr::Ptr &)
Insert an assertion for the SMT solver.
InstructionSemantics2::BaseSemantics::StatePtr copyOutgoingState() const
Returns a copy of the outgoing state.
uint64_t id() const
Property: Identifier.
void toYamlSteps(const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const
Output the steps as YAML.
void toYamlHeader(const SettingsPtr &, std::ostream &, const std::string &prefix) const
Output path node header as YAML.
void appendTag(const TagPtr &)
Append tags.