|
ROSE
0.11.102.0
|
Main class for model checking.
This class holds or references everything needed for model checking and runs the model checker. Most interaction with the model checker framework is through this object.
The engine maintains a priority queue of paths on which to work, and the work is farmed out to some combination of managed worker threads and/or unmanaged user threads. A unit of work is generally one node (the last node) of a path, which consists of executing the node symbolically, finding a list of control flow successor nodes, creating a new path for each of those successors, testing whether any of the new paths are feasible (using an SMT solver), and adding the feasible paths to the priority queue. The new paths are thus one node longer than the original path.
Part of the execution of a node involves checking execution state against a model specification. For instance, checking that no memory reads or writes occur to addresses within the first reserved page of memory. If a violation of the specification is detected, then a tag describing the violation can be attached to the path and the path can be added to a second priority queue that holds the "interesting" paths.
The engine is mainly responsible containing the prioritiy queues, managing worker threads and knowing about user threads, and handing work out to the threads. Many of the components of model checking are user-defined specializations of model checker base classes, and the Engine is reponsible for pointing to all of them so their virtual functions can be called at the appropriate times.
Definition at line 40 of file ModelChecker/Engine.h.
#include <Rose/BinaryAnalysis/ModelChecker/Engine.h>
Classes | |
| struct | InProgress |
| Information about a path that is in progress. More... | |
Public Types | |
| using | Ptr = EnginePtr |
| Reference counting pointer. More... | |
Public Member Functions | |
| ~Engine () | |
| Destructor. More... | |
| void | reset () |
| Reset engine to initial state. More... | |
| void | startWorkers (size_t n=0) |
| Start multiple worker threads. More... | |
| void | run () |
| Complete all work. More... | |
| void | stop () |
| Complete all current work and then stop. More... | |
| bool | step () |
| Run one step of checking in the calling thread. More... | |
| bool | workRemains () const |
| Test whether work remains to be done. More... | |
| size_t | workCapacity () const |
| Work capacity. More... | |
| size_t | nWorking () const |
| Number of threads that are working. More... | |
| size_t | nPathsPending () const |
| Number of paths to explore. More... | |
| Sawyer::Stopwatch | elapsedTime () const |
| Property: Elapsed time for model checking. More... | |
| size_t | nPathsExplored () const |
| Property: Number of paths explored. More... | |
| size_t | nStepsExplored () const |
| Property: Number of steps explored. More... | |
| const PathQueue & | pendingPaths () const |
| Property: Paths waiting to be explored. More... | |
| std::vector< InProgress > | inProgress () const |
| Paths that are currently in progress. More... | |
| size_t | nExpressionsTrimmed () const |
| Number of symbolic expressions trimmed to a new variable. More... | |
| void | showStatistics (std::ostream &, const std::string &prefix="") const |
| Print some statistics. More... | |
| PathPtr | takeNextInteresting () |
| Take next interesting result. More... | |
| bool | insertInteresting (const PathPtr &) |
| Potentially insert a path into the interesting queue. More... | |
| double | estimatedForestSize (size_t k) const |
| Estimated execution forest size to K levels. More... | |
| bool | insertWork (const PathPtr &) |
| Insert a path into the execution tree. More... | |
| SettingsPtr | settings () const |
| Property: Settings. More... | |
| void | settings (const SettingsPtr &) |
| Property: Settings. More... | |
| SemanticCallbacksPtr | semantics () const |
| Property: Adjustments to semantic operations. More... | |
| void | semantics (const SemanticCallbacksPtr &) |
| Property: Adjustments to semantic operations. More... | |
| PathPrioritizerPtr | explorationPrioritizer () const |
| Property: Path exploration prioritizer. More... | |
| void | explorationPrioritizer (const PathPrioritizerPtr &) |
| Property: Path exploration prioritizer. More... | |
| PathPredicatePtr | explorationPredicate () const |
| Property: Work insertion predicate. More... | |
| void | explorationPredicate (const PathPredicatePtr &) |
| Property: Work insertion predicate. More... | |
| PathPredicatePtr | interestingPredicate () const |
| Property: Interesting insertion predicate. More... | |
| void | interestingPredicate (const PathPredicatePtr &) |
| Property: Interesting insertion predicate. More... | |
| void | insertStartingPoint (const ExecutionUnitPtr &) |
| Insert a path starting point. More... | |
| void | insertStartingPoint (const PathPtr &) |
| Insert a path starting point. More... | |
| boost::filesystem::path | workerStatusFile () const |
| Write worker status to a text file. More... | |
| void | workerStatusFile (const boost::filesystem::path &) |
| Write worker status to a text file. More... | |
| const PathQueue & | interesting () const |
| Property: The interesting results queue. More... | |
| PathQueue & | interesting () |
| Property: The interesting results queue. More... | |
Static Public Member Functions | |
| static Ptr | instance () |
| Allocating constructor. More... | |
| static Ptr | instance (const SettingsPtr &) |
| Allocating constructor. More... | |
Protected Member Functions | |
| Engine (const SettingsPtr &) | |
| using Rose::BinaryAnalysis::ModelChecker::Engine::Ptr = EnginePtr |
Reference counting pointer.
Definition at line 46 of file ModelChecker/Engine.h.
| Rose::BinaryAnalysis::ModelChecker::Engine::~Engine | ( | ) |
Destructor.
The destructor will wait for all worker threads to finish before this object is destroyed.
|
static |
Allocating constructor.
Creates a model checker engine with default settings.
|
static |
Allocating constructor.
Creates a model checker engine with specified settings.
| SettingsPtr Rose::BinaryAnalysis::ModelChecker::Engine::settings | ( | ) | const |
Property: Settings.
Various settings used throughout the model checking framework.
Thread safety: This property accessor is thread safe. The settings themselves are not thread safe and should generally not be modified once worker threads are created.
| void Rose::BinaryAnalysis::ModelChecker::Engine::settings | ( | const SettingsPtr & | ) |
Property: Settings.
Various settings used throughout the model checking framework.
Thread safety: This property accessor is thread safe. The settings themselves are not thread safe and should generally not be modified once worker threads are created.
| SemanticCallbacksPtr Rose::BinaryAnalysis::ModelChecker::Engine::semantics | ( | ) | const |
Property: Adjustments to semantic operations.
All configurable semantic operations are encapsulated in this property. This should be set before running the engine, and not changed once the engine is running.
Thread safety: This property accessor is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::semantics | ( | const SemanticCallbacksPtr & | ) |
Property: Adjustments to semantic operations.
All configurable semantic operations are encapsulated in this property. This should be set before running the engine, and not changed once the engine is running.
Thread safety: This property accessor is thread safe.
| PathPrioritizerPtr Rose::BinaryAnalysis::ModelChecker::Engine::explorationPrioritizer | ( | ) | const |
Property: Path exploration prioritizer.
The specified prioritizer will be used to specify the order by which outstanding work is performed. The default is to explore the virtual execution tree with a depth-first search.
The prioritizer can be changed while the model checker is running, which has the effect of immediately re-sorting the outstanding work. Any worker threads that are already working on a particular path will continue to do so even if other paths now have higher priority.
The path prioritizer cannot be a null pointer.
Thread safety: This property accesor is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::explorationPrioritizer | ( | const PathPrioritizerPtr & | ) |
Property: Path exploration prioritizer.
The specified prioritizer will be used to specify the order by which outstanding work is performed. The default is to explore the virtual execution tree with a depth-first search.
The prioritizer can be changed while the model checker is running, which has the effect of immediately re-sorting the outstanding work. Any worker threads that are already working on a particular path will continue to do so even if other paths now have higher priority.
The path prioritizer cannot be a null pointer.
Thread safety: This property accesor is thread safe.
| PathPredicatePtr Rose::BinaryAnalysis::ModelChecker::Engine::explorationPredicate | ( | ) | const |
Property: Work insertion predicate.
This predicate is the gatekeeper for inserting paths into the work queue. Any path other than those inserted as part of initialization gets checked by this predicate and inserted only if the predicate returns true. The predicate will be called exactly once for each attempt to insert a path.
The predicate cannot be null. The default predicate always returns true.
Thread safety: This property accessor is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::explorationPredicate | ( | const PathPredicatePtr & | ) |
Property: Work insertion predicate.
This predicate is the gatekeeper for inserting paths into the work queue. Any path other than those inserted as part of initialization gets checked by this predicate and inserted only if the predicate returns true. The predicate will be called exactly once for each attempt to insert a path.
The predicate cannot be null. The default predicate always returns true.
Thread safety: This property accessor is thread safe.
| PathPredicatePtr Rose::BinaryAnalysis::ModelChecker::Engine::interestingPredicate | ( | ) | const |
Property: Interesting insertion predicate.
This predicate is the gatekeeper for inserting paths into the "interesting" queue. Each attempt to insert an interesting path through the model checker's API will result in exactly one call to this predicate. If the predicate returns true, then the path is inserted. Inserting a path using the interesting PathQueue directly bypasses this predicate.
The predicate cannot be null. The default predicate returns true if the path's final node has one or more associated tags.
Thread safety: This property accessor is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::interestingPredicate | ( | const PathPredicatePtr & | ) |
Property: Interesting insertion predicate.
This predicate is the gatekeeper for inserting paths into the "interesting" queue. Each attempt to insert an interesting path through the model checker's API will result in exactly one call to this predicate. If the predicate returns true, then the path is inserted. Inserting a path using the interesting PathQueue directly bypasses this predicate.
The predicate cannot be null. The default predicate returns true if the path's final node has one or more associated tags.
Thread safety: This property accessor is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::reset | ( | ) |
Reset engine to initial state.
Resets this engine to its initial state without changing settings. Counters, queues, etc. are cleared.
Thread safety: This method is not thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::insertStartingPoint | ( | const ExecutionUnitPtr & | ) |
Insert a path starting point.
Each starting point represents the root of a virtual execution tree that will be explored in parallel with all other work according to a user-defined path prioritizer. As many starting points as desired can be inserted, but no starting point should be inserted more than once.
Insertion of starting points is not limited by the explorationPredicate.
Thread safety: This method is thread safe. New starting points can be inserted before the model checker starts executing, or during execution.
| void Rose::BinaryAnalysis::ModelChecker::Engine::insertStartingPoint | ( | const PathPtr & | ) |
Insert a path starting point.
Each starting point represents the root of a virtual execution tree that will be explored in parallel with all other work according to a user-defined path prioritizer. As many starting points as desired can be inserted, but no starting point should be inserted more than once.
Insertion of starting points is not limited by the explorationPredicate.
Thread safety: This method is thread safe. New starting points can be inserted before the model checker starts executing, or during execution.
| void Rose::BinaryAnalysis::ModelChecker::Engine::startWorkers | ( | size_t | n = 0 | ) |
Start multiple worker threads.
Model checker can be done with any combination of worker threads managed by the model checking framework, and user threads that call model checker functions to do their own work.
This function starts n worker threads that perform model checking, and then immediately returns. When there is no work left to be done, all worker threads exit. Thus it's important to create work first (by inserting some starting points) before calling this function, otherwise all the workers will just immediately exit without doing anything.
Although it's usually called once per round of work, this function can be called more than once to increase the number of workers by n each time. If n is zero, then workers will be increased only up to the hardware parallelism. No workers are ever killed by this function.
See also, workCapacity.
Thread safety: This method is thread safe. In fact, it can even be called from within another worker.
| void Rose::BinaryAnalysis::ModelChecker::Engine::run | ( | ) |
Complete all work.
Blocks until all work is completed.
If there are managed workers, then the calling thread blocks without doing any work until all the workers are finished. On the other hand, if there are no managed workers then the calling thread will participate in the work even if other user threads are also working. This method can be called by as many user threads as desired, each of which will either block waiting for workers to exit, or will itself participate in the work.
Thread safety: This method is thread safe. However, it must not be called recursively or from within a managed worker.
| void Rose::BinaryAnalysis::ModelChecker::Engine::stop | ( | ) |
Complete all current work and then stop.
Blocks until the current work in progress finishes, joins the worker threads, and then returns. Work pending on the work queue is not removed.
Thread safety: This method is thread safe.
| bool Rose::BinaryAnalysis::ModelChecker::Engine::step | ( | ) |
Run one step of checking in the calling thread.
When work is immediately available, this function performs that work and returns true.
When work is not immediately available (even if another thread might create work later), this function does nothing and returns false.
Thread safety: This method is thread safe.
| bool Rose::BinaryAnalysis::ModelChecker::Engine::workRemains | ( | ) | const |
Test whether work remains to be done.
Returns true if there is work left to be done according to the work queue, or any threads are working and might still add more items to the work queue. If this method is called from a thread that is working (in the WORKING state) then it must necessarily return true since this thread could still create more work.
Thread safety: This method is thread safe. However, if it's pointless to call it from a thread that's doing work since it will always return true in that situation.
| size_t Rose::BinaryAnalysis::ModelChecker::Engine::workCapacity | ( | ) | const |
Work capacity.
This is the total number of workers working or waiting for work, plus the number of user threads currently doing work in this model checker. The simple act of calling this function does not necessarily mean the caller is doing work. In order to be "doing work", a thread needs to actually be working on a path (see step and run).
Thread safety: This method is thread safe.
| size_t Rose::BinaryAnalysis::ModelChecker::Engine::nWorking | ( | ) | const |
Number of threads that are working.
Returns the number of managed workers and user threads that are doing work. This does not count managed workers that are blocked waiting for work to become available.
Thread safety: This method is thread safe.
| size_t Rose::BinaryAnalysis::ModelChecker::Engine::nPathsPending | ( | ) | const |
Number of paths to explore.
Returns the number of paths waiting to be explored.
Thread safety: This method is thread safe.
| Sawyer::Stopwatch Rose::BinaryAnalysis::ModelChecker::Engine::elapsedTime | ( | ) | const |
Property: Elapsed time for model checking.
Returns the time in seconds since model checking started.
Thread safety: This method is thread safe.
| size_t Rose::BinaryAnalysis::ModelChecker::Engine::nPathsExplored | ( | ) | const |
Property: Number of paths explored.
This read-only property contains the number of paths explored.
Thread safety: This method is thread safe.
| size_t Rose::BinaryAnalysis::ModelChecker::Engine::nStepsExplored | ( | ) | const |
Property: Number of steps explored.
This is similar to the number of paths explored (nPathsExplored) except it measures individual steps. Some path components (such as basic blocks) have multiple steps (instructions).
Thread safety: This method is thread safe.
| const PathQueue& Rose::BinaryAnalysis::ModelChecker::Engine::pendingPaths | ( | ) | const |
Property: Paths waiting to be explored.
Returns the (read-only) queue of paths that are waiting to be explored. From this, one can count the number of pending paths, and measure various properties of those paths.
Thread safety: This method is thread safe. The returned object is a reference valid while this model checker Engine object exists. The referenced returned object may be changing by other threads, so only thread-safe methods should be called.
| std::vector<InProgress> Rose::BinaryAnalysis::ModelChecker::Engine::inProgress | ( | ) | const |
Paths that are currently in progress.
Returns a copy of the information about paths that are in progress at the time this function is called.
Thread safety: This method is thread safe.
| size_t Rose::BinaryAnalysis::ModelChecker::Engine::nExpressionsTrimmed | ( | ) | const |
Number of symbolic expressions trimmed to a new variable.
This is the number of times a large symbolic expression was replaced by a new variable.
Thread safety: This method is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::showStatistics | ( | std::ostream & | , |
| const std::string & | prefix = "" |
||
| ) | const |
Print some statistics.
Thread safety: This method is thread safe.
| boost::filesystem::path Rose::BinaryAnalysis::ModelChecker::Engine::workerStatusFile | ( | ) | const |
Write worker status to a text file.
The specified file is created or truncated, and then updated continuously until this object is destroyed or this method is called with a different file name. An empty file name turns this feature off.
Thread safety: This method is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::Engine::workerStatusFile | ( | const boost::filesystem::path & | ) |
Write worker status to a text file.
The specified file is created or truncated, and then updated continuously until this object is destroyed or this method is called with a different file name. An empty file name turns this feature off.
Thread safety: This method is thread safe.
| const PathQueue& Rose::BinaryAnalysis::ModelChecker::Engine::interesting | ( | ) | const |
Property: The interesting results queue.
As workers discover interesting things, they will insert those paths into the "interesting" queue. The queue can be accessed directly using this method.
The interesting results can be re-sorted at any time by changing the prioritizer property of the returned path queue.
Thread safety: This method is thread safe, but the returned queue is valid only as long as this model checker is valid.
| PathQueue& Rose::BinaryAnalysis::ModelChecker::Engine::interesting | ( | ) |
Property: The interesting results queue.
As workers discover interesting things, they will insert those paths into the "interesting" queue. The queue can be accessed directly using this method.
The interesting results can be re-sorted at any time by changing the prioritizer property of the returned path queue.
Thread safety: This method is thread safe, but the returned queue is valid only as long as this model checker is valid.
| PathPtr Rose::BinaryAnalysis::ModelChecker::Engine::takeNextInteresting | ( | ) |
Take next interesting result.
This takes the next path from the interesting queue if the queue is not empty. If the queue is empty, then this call blocks until something is placed on the queue or until all work has completed. If all work has completed without anything being placed on the queue, this function returns a null pointer.
If a non-null path is returned, then that path is also atomically inserted into the inProgress set.
Do not call this in a single-threaded application or it may deadlock since there are no other threads creating interesting results. Instead, use interesting()->takeNext() which does not block.
Thread safety: This method is thread safe.
| bool Rose::BinaryAnalysis::ModelChecker::Engine::insertInteresting | ( | const PathPtr & | ) |
Potentially insert a path into the interesting queue.
The specified path is checked by the interestingPredicate and if the predicate returns true then the path is inserted into the interesting queue. Returns true if inserted, false if rejected. To unconditionally insert a path, insert it using the interesting PathQueue directly.
Thread safety: This method is thread safe.
| double Rose::BinaryAnalysis::ModelChecker::Engine::estimatedForestSize | ( | size_t | k | ) | const |
Estimated execution forest size to K levels.
Returns the estimated number of nodes in the execution trees to K levels (execution steps) deep based on the average fanout per step.
Thread safety: This method is thread safe.
| bool Rose::BinaryAnalysis::ModelChecker::Engine::insertWork | ( | const PathPtr & | ) |
Insert a path into the execution tree.
The insertion is subject to the explorationPredicate. If the predicate returns false then the path is not inserted.
Returns true if inserted, false if not inserted.
Thread safety: This method is thread safe.
1.8.10