1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Engine_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Engine_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
6 #include <Rose/BinaryAnalysis/ModelChecker/PathQueue.h>
8 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
9 #include <Rose/BinaryAnalysis/SmtSolver.h>
10 #include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
11 #include <Sawyer/Stopwatch.h>
12 #include <boost/filesystem.hpp>
13 #include <boost/thread/thread.hpp>
17 namespace BinaryAnalysis {
18 namespace ModelChecker {
51 explicit InProgress(
const PathPtr&);
56 boost::thread::id threadId;
66 PathQueue interesting_;
67 SemanticCallbacksPtr semantics_;
71 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
73 SAWYER_THREAD_TRAITS::ConditionVariable newWork_;
74 SAWYER_THREAD_TRAITS::ConditionVariable newInteresting_;
75 PathPredicatePtr frontierPredicate_;
76 PathPredicatePtr interestingPredicate_;
77 SettingsPtr settings_;
78 std::vector<std::thread> workers_;
79 size_t workCapacity_ = 0;
81 size_t nPathsExplored_ = 0;
82 size_t nStepsExplored_ = 0;
83 bool stopping_ =
false;
84 std::vector<std::pair<double, size_t>> fanout_;
85 size_t nFanoutRoots_ = 0;
88 mutable size_t nPathsStats_ = 0;
89 size_t nExpressionsTrimmed_ = 0;
90 WorkerStatusPtr workerStatus_;
94 explicit Engine(
const SettingsPtr&);
100 static Ptr instance();
105 static Ptr instance(
const SettingsPtr&);
136 SemanticCallbacksPtr semantics()
const;
137 void semantics(
const SemanticCallbacksPtr&);
154 PathPrioritizerPtr explorationPrioritizer()
const;
155 void explorationPrioritizer(
const PathPrioritizerPtr&);
169 PathPredicatePtr explorationPredicate()
const;
170 void explorationPredicate(
const PathPredicatePtr&);
185 PathPredicatePtr interestingPredicate()
const;
186 void interestingPredicate(
const PathPredicatePtr&);
213 void insertStartingPoint(
const ExecutionUnitPtr&);
214 void insertStartingPoint(
const PathPtr&);
238 void startWorkers(
size_t n = 0);
279 bool workRemains()
const;
288 size_t workCapacity()
const;
296 size_t nWorking()
const;
303 size_t nPathsPending()
const;
321 size_t nPathsExplored()
const;
329 size_t nStepsExplored()
const;
339 const PathQueue& pendingPaths()
const;
346 std::vector<InProgress> inProgress()
const;
353 size_t nExpressionsTrimmed()
const;
358 void showStatistics(std::ostream&,
const std::string &prefix =
"")
const;
368 boost::filesystem::path workerStatusFile()
const;
369 void workerStatusFile(
const boost::filesystem::path&);
386 const PathQueue& interesting()
const;
387 PathQueue& interesting();
402 PathPtr takeNextInteresting();
411 bool insertInteresting(
const PathPtr&);
419 double estimatedForestSize(
size_t k)
const;
432 bool insertWork(
const PathPtr&);
441 void updateFanout(
size_t nChildren,
size_t totalSteps,
size_t lastSteps);
451 void changeState(
size_t workerId, WorkerState ¤tState, WorkerState newState, uint64_t pathHash);
454 void changeStateNS(
size_t workerId, WorkerState ¤tState, WorkerState newState, uint64_t pathHash);
457 void startWorkingNS();
460 void finishWorkingNS();
467 PathPtr takeNextWorkItem(
size_t workerId, WorkerState&);
470 PathPtr takeNextWorkItemNow(WorkerState&);
501 void displaySmtAssertions(
const PathPtr&);
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Settings settings
Command-line settings for the rosebud tool.
Main namespace for the ROSE library.
Rose::BinaryAnalysis::DataFlow::Engine< DfCfg, InstructionSemantics::BaseSemantics::StatePtr, TransferFunction, MergeFunction > Engine
Data-Flow engine.
Sawyer::SharedPointer< Engine > EnginePtr
Shared-ownership pointer for Engine.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Container associating values with keys.
ProgressPtr Ptr
Progress objects are reference counted.