ROSE  0.11.51.0
Classes | Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | List of all members
Rose::BinaryAnalysis::ModelChecker::Engine Class Referencefinal

Description

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 38 of file ModelChecker/Engine.h.

#include <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 PathQueuependingPaths () const
 Property: Paths waiting to be explored. More...
 
PathPtr takeNextInteresting ()
 Take next interesting result. More...
 
void finishPath ()
 Indicates that a path has been finished. More...
 
std::vector< InProgressinProgress () const
 Paths that are currently in progress. 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...
 
void showStatistics (std::ostream &, const std::string &prefix="") const
 Print some statistics. 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...
 
const PathQueueinteresting () const
 Property: The interesting results queue. More...
 
PathQueueinteresting ()
 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 &)
 

Member Typedef Documentation

Reference counting pointer.

Definition at line 44 of file ModelChecker/Engine.h.

Constructor & Destructor Documentation

Rose::BinaryAnalysis::ModelChecker::Engine::~Engine ( )

Destructor.

The destructor will wait for all worker threads to finish before this object is destroyed.

Member Function Documentation

static Ptr Rose::BinaryAnalysis::ModelChecker::Engine::instance ( )
static

Allocating constructor.

Creates a model checker engine with default settings.

static Ptr Rose::BinaryAnalysis::ModelChecker::Engine::instance ( const SettingsPtr &  )
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.

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.

void Rose::BinaryAnalysis::ModelChecker::Engine::finishPath ( )

Indicates that a path has been finished.

This should be called by a worker thread whenever its work on a path finishes, regardless of whether the work was successful or not. It removes the path from the inProgress list.

Thread safety: This method is thread safe.

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.

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.

void Rose::BinaryAnalysis::ModelChecker::Engine::showStatistics ( std::ostream &  ,
const std::string &  prefix = "" 
) const

Print some statistics.

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.


The documentation for this class was generated from the following file: