ROSE  0.11.50.0
Path.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Path_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Path_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 
8 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/Types.h>
9 #include <Rose/BinaryAnalysis/SmtSolver.h>
10 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
11 #include <Combinatorics.h>
12 
13 namespace Rose {
14 namespace BinaryAnalysis {
15 namespace ModelChecker {
16 
21 class Path {
22 public:
23  using Ptr = PathPtr;
24 
25 private:
26  PathNodePtr end_;
27 
28 protected:
29  Path() = delete;
30  explicit Path(const PathNodePtr &end);
31 public:
32  ~Path();
33 
34 public:
40  static Ptr instance(const ExecutionUnitPtr&);
41 
49  static Ptr instance(const PathPtr &prefix, const ExecutionUnitPtr&, const SymbolicExpr::Ptr &assertion,
50  const SmtSolver::Evidence&, const InstructionSemantics2::BaseSemantics::StatePtr &parentOutgoingState);
51 
57  bool isEmpty() const;
58 
64  size_t nNodes() const;
65 
71  size_t nSteps() const;
72 
80  double processingTime() const;
81 
90  uint64_t hash() const;
91  void hash(Combinatorics::Hasher&) const;
99  bool executionFailed() const;
100 
106  std::vector<SymbolicExpr::Ptr> assertions() const;
107 
113  PathNodePtr lastNode() const;
114 
123  std::vector<PathNodePtr> nodes() const;
124 
128  std::string printableName() const;
129 
136  void print(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;
137 
144  void toYaml(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;
145 
146 
147 };
148 
149 } // namespace
150 } // namespace
151 } // namespace
152 
153 #endif
154 #endif
uint64_t hash() const
Path hash.
void toYaml(const SettingsPtr &, std::ostream &, const std::string &prefix, size_t maxSteps) const
Multi-line output of path.
size_t nNodes() const
Length of path in nodes.
void print(const SettingsPtr &, std::ostream &, const std::string &prefix, size_t maxSteps) const
Multi-line output of path.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Main namespace for the ROSE library.
static Ptr instance(const ExecutionUnitPtr &)
Construct a path that is one vertex in length.
PathNodePtr lastNode() const
Last node of the path.
bool executionFailed() const
Property: Whether execution has failed.
std::string printableName() const
Short name suitable for printing in diagnostics.
size_t nSteps() const
Length of path in steps.
bool isEmpty() const
Test for empty path.
std::vector< PathNodePtr > nodes() const
Nodes composing path.
std::vector< SymbolicExpr::Ptr > assertions() const
All SMT assertions along the path.
double processingTime() const
Total time to process path.