ROSE  0.11.109.0
ModelChecker/Engine.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_Engine_H
2 #define ROSE_BinaryAnalysis_ModelChecker_Engine_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/PathQueue.h>
7 
8 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/Types.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>
14 #include <thread>
15 
16 namespace Rose {
17 namespace BinaryAnalysis {
18 namespace ModelChecker {
19 
40 class Engine final {
42  // Types
44 public:
46  using Ptr = EnginePtr;
47 
49  struct InProgress {
50  InProgress();
51  explicit InProgress(const PathPtr&);
52  ~InProgress();
53 
54  PathPtr path;
55  Sawyer::Stopwatch elapsed;
56  boost::thread::id threadId;
57  int tid = 0;
58  };
59 
61  // Data members
63 private:
64  PathQueue frontier_; // paths with work remaining
65  PathQueue interesting_; // paths that are interesting, placed here by workers
66  SemanticCallbacksPtr semantics_; // various configurable semantic operations
67 
68  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects all following data members
69  Sawyer::Container::Map<boost::thread::id, InProgress> inProgress_;// work that is in progress
70  SAWYER_THREAD_TRAITS::ConditionVariable newWork_; // signaled when work arrives or thread finishes
71  SAWYER_THREAD_TRAITS::ConditionVariable newInteresting_; // signaled when interesting paths arrive or threads finish
72  PathPredicatePtr frontierPredicate_; // predicate for inserting paths into the "frontier" queue
73  PathPredicatePtr interestingPredicate_; // predicate for inserting paths into the "interesting" queue
74  SettingsPtr settings_; // overall settings
75  std::vector<std::thread> workers_; // managed worker threads
76  size_t workCapacity_ = 0; // managed workers plus user threads
77  size_t nWorking_ = 0; // number of threads currently doing work
78  size_t nPathsExplored_ = 0; // number of path nodes executed, i.e., number of paths explored
79  size_t nStepsExplored_ = 0; // number of steps executed
80  bool stopping_ = false; // when true, workers stop even if there is still work remaining
81  std::vector<std::pair<double, size_t>> fanout_; // total fanout and number of nodes for each level of the forest
82  size_t nFanoutRoots_ = 0; // number of execution trees for calculating total forest size
83  Sawyer::Stopwatch elapsedTime_; // time since model checking started
84  mutable Sawyer::Stopwatch timeSinceStats_; // time since last statistics were reported
85  mutable size_t nPathsStats_ = 0; // number of paths reported in last statistics output
86  size_t nExpressionsTrimmed_ = 0; // number of symbolic expressions trimmed down to a new variable
87  WorkerStatusPtr workerStatus_; // mostly for debugging
88 
89 protected:
90  Engine() = delete;
91  explicit Engine(const SettingsPtr&);
92 
93 public:
97  static Ptr instance();
98 
102  static Ptr instance(const SettingsPtr&);
103 
107  ~Engine();
108 
110  // Configuration functions
112 public:
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&);
187  // Initialization functions
190 public:
196  void reset();
197 
210  void insertStartingPoint(const ExecutionUnitPtr&);
211  void insertStartingPoint(const PathPtr&);
215  // Model checker execution
218 public:
235  void startWorkers(size_t n = 0);
236 
248  void run();
249 
256  void stop();
257 
266  bool step();
267 
276  bool workRemains() const;
277 
285  size_t workCapacity() const;
286 
293  size_t nWorking() const;
294 
300  size_t nPathsPending() const;
301 
303  // Model checker status
305 public:
311  Sawyer::Stopwatch elapsedTime() const;
312 
318  size_t nPathsExplored() const;
319 
326  size_t nStepsExplored() const;
327 
336  const PathQueue& pendingPaths() const;
337 
343  std::vector<InProgress> inProgress() const;
344 
350  size_t nExpressionsTrimmed() const;
351 
355  void showStatistics(std::ostream&, const std::string &prefix = "") const;
356 
365  boost::filesystem::path workerStatusFile() const;
366  void workerStatusFile(const boost::filesystem::path&);
369  // Model checker results
372 public:
383  const PathQueue& interesting() const;
384  PathQueue& interesting();
399  PathPtr takeNextInteresting();
400 
408  bool insertInteresting(const PathPtr&);
409 
416  double estimatedForestSize(size_t k) const;
417 
419  // Worker functions. It is useful to call these from user code.
421 public:
429  bool insertWork(const PathPtr&);
430 
432  // Internal stuff.
434 private:
435  // Update the fanout parameters used to estimate execution tree size. The nChildren are the number of new paths created by
436  // extending the current path, totalSteps is the number of steps in the whole path, and lastSteps is the number of steps in
437  // the last node of the path.
438  void updateFanout(size_t nChildren, size_t totalSteps, size_t lastSteps);
439 
440  // Called by each worker thread when they start. Users should not call this even though it's public. The ID is the index
441  // of the managed worker in the workers_ vector.
442  void worker(size_t id, const Progress::Ptr&);
443 
444  // Change state. The thread should hold its current state in a local variable. The state transition edges affect how
445  // various counters are updated. All threads must start by initializing their current state to STARTING and then calling
446  // changeState to also specify the new state is STARTING. Only certain transitions are allowed--read the source.
447  void changeState(size_t workerId, WorkerState &currentState, WorkerState newState);
448 
449  // Non-synchronized version of changeState
450  void changeStateNS(size_t workerId, WorkerState &currentState, WorkerState newState);
451 
452  // Do things that should be done when work is started.
453  void startWorkingNS();
454 
455  // Called by changeState when a worker has finished.
456  void finishWorkingNS();
457 
458  // Get the next path on which to work. This function blocks until either more work is available, or no more work can
459  // possibly be available. In the former case, it removes the highest priority path from the work queue, changes the work
460  // state to WORKING, and returns the path. In the latter case, it returns a null pointer.
461  //
462  // Thread safety: This method is thread safe.
463  PathPtr takeNextWorkItem(size_t workerId, WorkerState&);
464 
465  // Non-blocking version of takeNextWorkItem.
466  PathPtr takeNextWorkItemNow(WorkerState&);
467 
468  // Execute a path. This goes back as far as necessary to get a known state, and then executes from there to the end
469  // of the path.
470  //
471  // After a path is executed, it is conditionally added to the "interesting" queue according to the @ref
472  // interestingPredicate.
473  //
474  // The solver argument is the solver used by model checker, which might be different than the optional solver already
475  // attached to the RiscOperators object.
476  //
477  // Thread safety: The RISC operators must be thread-local, otherwise thread safe. All paths will have an identical
478  // set of states for this path after this returns.
479  void execute(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);
480 
481  // Produce more work, typically by looking at the instruction pointer register for the outgoing state of a previous
482  // path (which is not currently in the work queue) and creating new paths.
483  void extend(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);
484 
485  // Perform one step of model checking.
486  void doOneStep(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);
487 
488  // Indicates that a path has been finished.
489  //
490  // This should be called by a worker thread whenever its work on a path finishes, regardless of whether the work was
491  // successful or not. It removes the path from the @ref inProgress list.
492  //
493  // Thread safety: This method is thread safe.
495 
496  // Display diagnostics about where variables appear in path constraints.
497  void displaySmtAssertions(const PathPtr&);
498 };
499 
500 
501 } // namespace
502 } // namespace
503 } // namespace
504 
505 #endif
506 #endif
Rose::BinaryAnalysis::DataFlow::Engine< DfCfg, BaseSemantics::StatePtr, TransferFunction, MergeFunction > Engine
Data-Flow engine.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Main namespace for the ROSE library.
Simple elapsed time.
Definition: Stopwatch.h:41
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Container associating values with keys.
Definition: Sawyer/Map.h:66
Sawyer::SharedPointer< Progress > Ptr
Progress objects are reference counted.
Definition: Progress.h:168