ROSE  0.11.58.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/thread/thread.hpp>
13 #include <thread>
14 
15 namespace Rose {
16 namespace BinaryAnalysis {
17 namespace ModelChecker {
18 
39 class Engine final {
41  // Types
43 public:
45  using Ptr = EnginePtr;
46 
48  struct InProgress {
49  InProgress();
50  explicit InProgress(const PathPtr&);
51  ~InProgress();
52 
53  PathPtr path;
55  boost::thread::id threadId;
56  int tid = 0;
57  };
58 
60  // Data members
62 private:
63  PathQueue frontier_; // paths with work remaining
64  PathQueue interesting_; // paths that are interesting, placed here by workers
65  SemanticCallbacksPtr semantics_; // various configurable semantic operations
66 
67  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects all following data members
68  Sawyer::Container::Map<boost::thread::id, InProgress> inProgress_;// work that is in progress
69  SAWYER_THREAD_TRAITS::ConditionVariable newWork_; // signaled when work arrives or thread finishes
70  SAWYER_THREAD_TRAITS::ConditionVariable newInteresting_; // signaled when interesting paths arrive or threads finish
71  PathPredicatePtr frontierPredicate_; // predicate for inserting paths into the "frontier" queue
72  PathPredicatePtr interestingPredicate_; // predicate for inserting paths into the "interesting" queue
73  SettingsPtr settings_; // overall settings
74  std::vector<std::thread> workers_; // managed worker threads
75  size_t workCapacity_ = 0; // managed workers plus user threads
76  size_t nWorking_ = 0; // number of threads currently doing work
77  size_t nPathsExplored_ = 0; // number of path nodes executed, i.e., number of paths explored
78  size_t nStepsExplored_ = 0; // number of steps executed
79  bool stopping_ = false; // when true, workers stop even if there is still work remaining
80  std::vector<std::pair<double, size_t>> fanout_; // total fanout and number of nodes for each level of the forest
81  size_t nFanoutRoots_ = 0; // number of execution trees for calculating total forest size
82  Sawyer::Stopwatch elapsedTime_; // time since model checking started
83  mutable Sawyer::Stopwatch timeSinceStats_; // time since last statistics were reported
84  mutable size_t nPathsStats_ = 0; // number of paths reported in last statistics output
85  size_t nExpressionsTrimmed_ = 0; // number of symbolic expressions trimmed down to a new variable
86 
87 protected:
88  Engine() = delete;
89  explicit Engine(const SettingsPtr&);
90 
91 public:
95  static Ptr instance();
96 
100  static Ptr instance(const SettingsPtr&);
101 
105  ~Engine();
106 
108  // Configuration functions
110 public:
119  SettingsPtr settings() const;
120  void settings(const SettingsPtr&);
131  SemanticCallbacksPtr semantics() const;
132  void semantics(const SemanticCallbacksPtr&);
149  PathPrioritizerPtr explorationPrioritizer() const;
150  void explorationPrioritizer(const PathPrioritizerPtr&);
164  PathPredicatePtr explorationPredicate() const;
165  void explorationPredicate(const PathPredicatePtr&);
180  PathPredicatePtr interestingPredicate() const;
181  void interestingPredicate(const PathPredicatePtr&);
185  // Initialization functions
188 public:
194  void reset();
195 
208  void insertStartingPoint(const ExecutionUnitPtr&);
209  void insertStartingPoint(const PathPtr&);
213  // Model checker execution
216 public:
233  void startWorkers(size_t n = 0);
234 
246  void run();
247 
254  void stop();
255 
264  bool step();
265 
274  bool workRemains() const;
275 
283  size_t workCapacity() const;
284 
291  size_t nWorking() const;
292 
298  size_t nPathsPending() const;
299 
301  // Model checker status
303 public:
310 
316  size_t nPathsExplored() const;
317 
324  size_t nStepsExplored() const;
325 
334  const PathQueue& pendingPaths() const;
335 
341  std::vector<InProgress> inProgress() const;
342 
348  size_t nExpressionsTrimmed() const;
349 
353  void showStatistics(std::ostream&, const std::string &prefix = "") const;
354 
356  // Model checker results
358 public:
369  const PathQueue& interesting() const;
385  PathPtr takeNextInteresting();
386 
394  bool insertInteresting(const PathPtr&);
395 
402  double estimatedForestSize(size_t k) const;
403 
405  // Worker functions. It is useful to call these from user code.
407 public:
415  bool insertWork(const PathPtr&);
416 
418  // Internal stuff.
420 private:
421  // Update the fanout parameters used to estimate execution tree size. The nChildren are the number of new paths created by
422  // extending the current path, totalSteps is the number of steps in the whole path, and lastSteps is the number of steps in
423  // the last node of the path.
424  void updateFanout(size_t nChildren, size_t totalSteps, size_t lastSteps);
425 
426  // Called by each worker thread when they start. Users should not call this even though it's public.
427  void worker();
428 
429  // Worker states.
430  enum class WorkerState {
431  STARTING, // thread is initializing
432  WAITING, // thread is looking for new work
433  WORKING, // thread is actively working on a path
434  FINISHED // thread will never work again and is cleaning up
435  };
436 
437  // Change state. The thread should hold its current state in a local variable. The state transition edges affect how
438  // various counters are updated. All threads must start by initializing their current state to STARTING and then calling
439  // changeState to also specify the new state is STARTING. Only certain transitions are allowed--read the source.
440  void changeState(WorkerState &currentState, WorkerState newState);
441 
442  // Non-synchronized version of changeState
443  void changeStateNS(WorkerState &currentState, WorkerState newState);
444 
445  // Do things that should be done when work is started.
446  void startWorkingNS();
447 
448  // Called by changeState when a worker has finished.
449  void finishWorkingNS();
450 
451  // Get the next path on which to work. This function blocks until either more work is available, or no more work can
452  // possibly be available. In the former case, it removes the highest priority path from the work queue, changes the work
453  // state to WORKING, and returns the path. In the latter case, it returns a null pointer.
454  //
455  // Thread safety: This method is thread safe.
456  PathPtr takeNextWorkItem(WorkerState&);
457 
458  // Non-blocking version of takeNextWorkItem.
459  PathPtr takeNextWorkItemNow(WorkerState&);
460 
461  // Execute a path. This goes back as far as necessary to get a known state, and then executes from there to the end
462  // of the path.
463  //
464  // After a path is executed, it is conditionally added to the "interesting" queue according to the @ref
465  // interestingPredicate.
466  //
467  // The solver argument is the solver used by model checker, which might be different than the optional solver already
468  // attached to the RiscOperators object.
469  //
470  // Thread safety: The RISC operators must be thread-local, otherwise thread safe. All paths will have an identical
471  // set of states for this path after this returns.
472  void execute(const PathPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);
473 
474  // Produce more work, typically by looking at the instruction pointer register for the outgoing state of a previous
475  // path (which is not currently in the work queue) and creating new paths.
476  void extend(const PathPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);
477 
478  // Perform one step of model checking.
479  void doOneStep(const PathPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);
480 
481  // Indicates that a path has been finished.
482  //
483  // This should be called by a worker thread whenever its work on a path finishes, regardless of whether the work was
484  // successful or not. It removes the path from the @ref inProgress list.
485  //
486  // Thread safety: This method is thread safe.
488 
489  // Display diagnostics about where variables appear in path constraints.
490  void displaySmtAssertions(const PathPtr&);
491 };
492 
493 
494 } // namespace
495 } // namespace
496 } // namespace
497 
498 #endif
499 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
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.
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