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 {
46 using Ptr = EnginePtr;
51 explicit InProgress(
const PathPtr&);
56 boost::thread::id threadId;
65 PathQueue interesting_;
66 SemanticCallbacksPtr semantics_;
68 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
70 SAWYER_THREAD_TRAITS::ConditionVariable newWork_;
71 SAWYER_THREAD_TRAITS::ConditionVariable newInteresting_;
72 PathPredicatePtr frontierPredicate_;
73 PathPredicatePtr interestingPredicate_;
74 SettingsPtr settings_;
75 std::vector<std::thread> workers_;
76 size_t workCapacity_ = 0;
78 size_t nPathsExplored_ = 0;
79 size_t nStepsExplored_ = 0;
80 bool stopping_ =
false;
81 std::vector<std::pair<double, size_t>> fanout_;
82 size_t nFanoutRoots_ = 0;
85 mutable size_t nPathsStats_ = 0;
86 size_t nExpressionsTrimmed_ = 0;
87 WorkerStatusPtr workerStatus_;
91 explicit Engine(
const SettingsPtr&);
97 static Ptr instance();
102 static Ptr instance(
const SettingsPtr&);
121 SettingsPtr settings()
const;
122 void settings(
const SettingsPtr&);
133 SemanticCallbacksPtr semantics()
const;
134 void semantics(
const SemanticCallbacksPtr&);
151 PathPrioritizerPtr explorationPrioritizer()
const;
152 void explorationPrioritizer(
const PathPrioritizerPtr&);
166 PathPredicatePtr explorationPredicate()
const;
167 void explorationPredicate(
const PathPredicatePtr&);
182 PathPredicatePtr interestingPredicate()
const;
183 void interestingPredicate(
const PathPredicatePtr&);
210 void insertStartingPoint(
const ExecutionUnitPtr&);
211 void insertStartingPoint(
const PathPtr&);
235 void startWorkers(
size_t n = 0);
276 bool workRemains()
const;
285 size_t workCapacity()
const;
293 size_t nWorking()
const;
300 size_t nPathsPending()
const;
318 size_t nPathsExplored()
const;
326 size_t nStepsExplored()
const;
336 const PathQueue& pendingPaths()
const;
343 std::vector<InProgress> inProgress()
const;
350 size_t nExpressionsTrimmed()
const;
355 void showStatistics(std::ostream&,
const std::string &prefix =
"")
const;
365 boost::filesystem::path workerStatusFile()
const;
366 void workerStatusFile(
const boost::filesystem::path&);
383 const PathQueue& interesting()
const;
384 PathQueue& interesting();
399 PathPtr takeNextInteresting();
408 bool insertInteresting(
const PathPtr&);
416 double estimatedForestSize(
size_t k)
const;
429 bool insertWork(
const PathPtr&);
438 void updateFanout(
size_t nChildren,
size_t totalSteps,
size_t lastSteps);
447 void changeState(
size_t workerId, WorkerState ¤tState, WorkerState newState);
450 void changeStateNS(
size_t workerId, WorkerState ¤tState, WorkerState newState);
453 void startWorkingNS();
456 void finishWorkingNS();
463 PathPtr takeNextWorkItem(
size_t workerId, WorkerState&);
466 PathPtr takeNextWorkItemNow(WorkerState&);
497 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.
Main namespace for the ROSE library.
Rose::BinaryAnalysis::DataFlow::Engine< DfCfg, InstructionSemantics::BaseSemantics::StatePtr, TransferFunction, MergeFunction > Engine
Data-Flow engine.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Container associating values with keys.
ProgressPtr Ptr
Progress objects are reference counted.