ROSE  0.11.87.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_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/PathQueue.h>
7 
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>
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;
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:
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;
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 InstructionSemantics2::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 InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);
484 
485  // Perform one step of model checking.
486  void doOneStep(const PathPtr&, const InstructionSemantics2::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
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:48
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.
boost::filesystem::path workerStatusFile() const
Write worker status to a text file.
PathPrioritizerPtr explorationPrioritizer() const
Property: Path exploration prioritizer.
void showStatistics(std::ostream &, const std::string &prefix="") const
Print some statistics.
boost::thread::id threadId
Identifier for thread doing the work.
void insertStartingPoint(const ExecutionUnitPtr &)
Insert a path starting point.
size_t nExpressionsTrimmed() const
Number of symbolic expressions trimmed to a new variable.
size_t nPathsExplored() const
Property: Number of paths explored.
Information about a path that is in progress.
const PathQueue & pendingPaths() const
Property: Paths waiting to be explored.
size_t workCapacity() const
Work capacity.
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.
Simple elapsed time.
Definition: Stopwatch.h:41
List of path endpoints in an execution tree.
Definition: PathQueue.h:16
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.
Definition: Sawyer/Map.h:66