1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Engine_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Engine_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <Rose/BinaryAnalysis/ModelChecker/PathQueue.h>
8 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/Types.h>
9 #include <Rose/BinaryAnalysis/SmtSolver.h>
10 #include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
11 #include <Sawyer/Stopwatch.h>
15 namespace BinaryAnalysis {
16 namespace ModelChecker {
44 using Ptr = EnginePtr;
63 SemanticCallbacksPtr semantics_;
65 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
67 SAWYER_THREAD_TRAITS::ConditionVariable newWork_;
68 SAWYER_THREAD_TRAITS::ConditionVariable newInteresting_;
69 PathPredicatePtr frontierPredicate_;
70 PathPredicatePtr interestingPredicate_;
71 SettingsPtr settings_;
72 std::vector<std::thread> workers_;
73 size_t workCapacity_ = 0;
75 size_t nPathsExplored_ = 0;
76 size_t nStepsExplored_ = 0;
77 bool stopping_ =
false;
78 std::vector<std::pair<double, size_t>> fanout_;
79 size_t nFanoutRoots_ = 0;
82 mutable size_t nPathsStats_ = 0;
86 explicit Engine(
const SettingsPtr&);
129 void semantics(
const SemanticCallbacksPtr&);
396 void showStatistics(std::ostream&,
const std::string &prefix =
"")
const;
418 void updateFanout(
size_t nChildren,
size_t totalSteps,
size_t lastSteps);
424 enum class WorkerState {
434 void changeState(WorkerState ¤tState, WorkerState newState);
437 void changeStateNS(WorkerState ¤tState, WorkerState newState);
440 void startWorkingNS();
443 void finishWorkingNS();
450 PathPtr takeNextWorkItem(WorkerState&);
453 PathPtr takeNextWorkItemNow(WorkerState&);
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
void reset()
Reset engine to initial state.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Sawyer::Stopwatch elapsed
Wall clock time elapsed for this work.
SemanticCallbacksPtr semantics() const
Property: Adjustments to semantic operations.
PathPrioritizerPtr explorationPrioritizer() const
Property: Path exploration prioritizer.
void showStatistics(std::ostream &, const std::string &prefix="") const
Print some statistics.
void finishPath()
Indicates that a path has been finished.
boost::thread::id threadId
Identifier for thread doing the work.
void insertStartingPoint(const ExecutionUnitPtr &)
Insert a path starting point.
size_t nPathsExplored() const
Property: Number of paths explored.
void run()
Complete all work.
Information about a path that is in progress.
const PathQueue & pendingPaths() const
Property: Paths waiting to be explored.
Main class for model checking.
size_t workCapacity() const
Work capacity.
PathPtr path
The path being worked on.
const PathQueue & interesting() const
Property: The interesting results queue.
Main namespace for the ROSE library.
double estimatedForestSize(size_t k) const
Estimated execution forest size to K levels.
EnginePtr Ptr
Reference counting pointer.
List of path endpoints in an execution tree.
SettingsPtr settings() const
Property: Settings.
PathPredicatePtr interestingPredicate() const
Property: Interesting insertion predicate.
PathPredicatePtr explorationPredicate() const
Property: Work insertion predicate.
size_t nWorking() const
Number of threads that are working.
bool insertWork(const PathPtr &)
Insert a path into the execution tree.
size_t nPathsPending() const
Number of paths to explore.
bool insertInteresting(const PathPtr &)
Potentially insert a path into the interesting queue.
std::vector< InProgress > inProgress() const
Paths that are currently in progress.
void stop()
Complete all current work and then stop.
void startWorkers(size_t n=0)
Start multiple worker threads.
PathPtr takeNextInteresting()
Take next interesting result.
bool workRemains() const
Test whether work remains to be done.
static Ptr instance()
Allocating constructor.
bool step()
Run one step of checking in the calling thread.
size_t nStepsExplored() const
Property: Number of steps explored.
Sawyer::Stopwatch elapsedTime() const
Property: Elapsed time for model checking.
Container associating values with keys.