1 #ifndef ROSE_BinaryAnalysis_ModelChecker_PathNode_H
2 #define ROSE_BinaryAnalysis_ModelChecker_PathNode_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
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>
12 namespace BinaryAnalysis {
13 namespace ModelChecker {
27 using Ptr = PathNodePtr;
31 const ExecutionUnitPtr executionUnit_;
33 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
47 bool executionFailed_ =
false;
48 std::vector<SymbolicExpression::Ptr> assertions_;
50 std::vector<TagPtr> tags_;
52 double processingTime_ = NAN;
53 double sortKey_ = NAN;
61 PathNode(
const ExecutionUnitPtr&);
78 static Ptr instance(
const ExecutionUnitPtr&);
107 double sortKey()
const;
108 void sortKey(
double);
129 ExecutionUnitPtr executionUnit()
const;
137 size_t nSteps()
const;
150 std::vector<SymbolicExpression::Ptr> assertions()
const;
176 bool executionFailed()
const;
188 class BorrowedOutgoingState {
189 friend class PathNode;
191 PathNode*
const node;
195 BorrowedOutgoingState() =
delete;
196 BorrowedOutgoingState& operator=(
const BorrowedOutgoingState&) =
delete;
199 ~BorrowedOutgoingState();
221 BorrowedOutgoingState borrowOutgoingState();
230 void releaseOutgoingState();
239 void appendTag(
const TagPtr&);
240 void appendTags(
const std::vector<TagPtr>&);
246 size_t nTags()
const;
251 std::vector<TagPtr> tags()
const;
258 double processingTime()
const;
265 void incrementProcessingTime(
double seconds);
277 std::string printableName()
const;
282 void toYamlHeader(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const;
285 void toYamlSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
286 size_t stepOrigin,
size_t maxSteps)
const;
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
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.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.