Description

Interface to Satisfiability Modulo Theory (SMT) solvers.

The purpose of an SMT solver is to determine if an expression is satisfiable. Solvers are reference counted objects that are allocated with instance static methods or create virtual constructors and should not be explicitly deleted.

Definition at line 39 of file SmtSolver.h.

#include <Rose/BinaryAnalysis/SmtSolver.h>

Inheritance diagram for Rose::BinaryAnalysis::SmtSolver:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::SmtSolver:

[legend]

Classes
struct	Exception
	Exceptions for all things SMT related. More...

class	Memoizer
	Memoizes calls to an SMT solver. More...

struct	ParseError
	Exception for parse errors when reading SMT solver output. More...

class	SExpr
	S-Expr parsed from SMT solver text output. More...

struct	Stats
	SMT solver statistics. More...

class	Transaction
	RAII guard for solver stack. More...

Public Types
enum	LinkMode { LM_NONE = 0x0000 , LM_LIBRARY = 0x0001 , LM_EXECUTABLE = 0x0002 , LM_ANY = 0x0003 }
	Bit flags to indicate the kind of solver interface. More...

enum	Type { NO_TYPE , BOOLEAN , BIT_VECTOR , MEM_STATE }
	Type (sort) of expression. More...

enum	Satisfiable { SAT_NO =0 , SAT_YES , SAT_UNKNOWN }
	Satisfiability constants. More...

using	ExprList = std::vector< SymbolicExpression::Ptr >
	Ordered list of expressions.

using	Ptr = SmtSolverPtr
	Reference counting pointer for SMT solvers.

using	Availability = std::map< std::string, bool >
	Solver availability map.

using	StringTypePair = std::pair< std::string, Type >
	Maps expression nodes to term names.

using	TermNames = Sawyer::Container::Map< SymbolicExpression::Ptr, StringTypePair >

using	ExprExprMap = Sawyer::Container::Map< SymbolicExpression::Ptr, SymbolicExpression::Ptr >
	Maps one symbolic expression to another.

using	VariableSet = Sawyer::Container::Set< SymbolicExpression::LeafPtr, CompareLeavesByName >
	Set of variables.

using	Definitions = std::set< uint64_t >
	Free variables that have been defined.

using	SExprTypePair = std::pair< SExpr::Ptr, Type >

using	Evidence = Sawyer::Container::Map< std::string, SymbolicExpression::Ptr >
	Evidence of satisfiability.

Public Member Functions
virtual Ptr	create () const =0
	Virtual constructor.

LinkMode	linkage () const
	Property: How ROSE communicates with the solver.

void	requireLinkage (LinkMode) const
	Assert required linkage.

virtual void	timeout (boost::chrono::duration< double > seconds)=0
	Set the timeout for the solver.

virtual Satisfiable	triviallySatisfiable (const ExprList &exprs)
	Determines if expressions are trivially satisfiable or unsatisfiable.

virtual void	reset ()
	Reset solver state.

virtual void	push ()
	Create a backtracking point.

virtual void	pop ()
	Pop a backtracking point.

virtual size_t	nLevels () const
	Number of backtracking levels.

virtual size_t	nAssertions (size_t backtrackingLevel)
	Number of assertions at a specific backtracking level.

virtual size_t	nAssertions () const
	Total number of assertions across all backtracking levels.

virtual ExprList	assertions () const
	All assertions.

virtual const ExprList &	assertions (size_t level) const
	Assertions for a particular level.

virtual Satisfiable	check ()
	Check satisfiability of current stack.

virtual Satisfiable	checkTrivial ()
	Check whether the stack of assertions is trivially satisfiable.

virtual std::vector< std::string >	evidenceNames () const
	Names of items for which satisfiability evidence exists.

virtual SymbolicExpression::Ptr	evidenceForName (const std::string &) const
	Evidence of satisfiability for a variable or memory address.

virtual void	clearEvidence ()
	Clears evidence information.

virtual SymbolicExpression::Ptr	evidenceForAddress (uint64_t addr)
	Evidence of satisfiability for a memory address.

const Stats &	statistics () const
	Property: Statistics for this solver.

void	resetStatistics ()
	Resets statistics for this solver.

virtual void	generateFile (std::ostream &, const ExprList &exprs, Definitions *)=0
	Generates an input file for for the solver.

virtual void	selfTest ()
	Unit tests.


const std::string &	name () const
	Property: Name of solver for debugging.

void	name (const std::string &s)
	Property: Name of solver for debugging.


Memoizer::Ptr	memoizer () const
	Property: Memoizer.

void	memoizer (const Memoizer::Ptr &)
	Property: Memoizer.


virtual Satisfiable	satisfiable (const SymbolicExpression::Ptr &)
	Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.

virtual Satisfiable	satisfiable (const ExprList &)
	Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.


bool	errorIfReset () const
	Property: Throw an exception if the solver is reset.

void	errorIfReset (bool b)
	Property: Throw an exception if the solver is reset.


virtual void	insert (const SymbolicExpression::Ptr &)
	Insert assertions.

virtual void	insert (const ExprList &)
	Insert assertions.


Evidence	evidenceByName () const
	All evidence of satisfiability.

ExprExprMap	evidence () const
	All evidence of satisfiability.


virtual SymbolicExpression::Ptr	evidenceForVariable (const SymbolicExpression::Ptr &var)
	Evidence of satisfiability for a bitvector variable.

virtual SymbolicExpression::Ptr	evidenceForVariable (uint64_t varno)
	Evidence of satisfiability for a bitvector variable.


Progress::Ptr	progress () const
	Progress reporting object.

void	progress (const Progress::Ptr &progress)
	Progress reporting object.

Static Public Member Functions
static Availability	availability ()
	Availability of all known solvers.

static Ptr	instance (const std::string &name)
	Allocate a new solver by name.

static Ptr	bestAvailable ()
	Best available solver.

static LinkMode	bestLinkage (unsigned linkages)
	Given a bit vector of linkages, return the best one.

static Stats	classStatistics ()
	Property: Statistics across all solvers.

static void	resetClassStatistics ()
	Resets statistics for the class.

static void	initDiagnostics ()
	Initialize diagnostic output facilities.

Static Public Attributes
static Sawyer::Message::Facility	mlog
	Diagnostic facility.

Protected Member Functions
	SmtSolver (const std::string &name, unsigned linkages)
	Construct with name and linkage.

virtual Satisfiable	checkExe ()
	Check satisfiability using text files and an executable.

virtual Satisfiable	checkLib ()
	Check satisfiability using a library API.

virtual std::string	getErrorMessage (int exitStatus)
	Error message from running a solver executable.

virtual void	findVariables (const SymbolicExpression::Ptr &, VariableSet &)
	Return all variables that need declarations.

virtual std::string	getCommand (const std::string &config_name)=0
	Given the name of a configuration file, return the command that is needed to run the solver.

std::vector< SExpr::Ptr >	parseSExpressions (const std::string &)
	Parse all SExprs from the specified string.

virtual void	parseEvidence ()
	Parses evidence of satisfiability.

Static Protected Member Functions
static void	printSExpression (std::ostream &, const SExpr::Ptr &)
	Print an S-Expr for debugging.

static ExprList	normalizeVariables (const ExprList &, SymbolicExpression::ExprExprHashMap &index)
	Normalize expressions by renaming variables.

static ExprList	undoNormalization (const ExprList &, const SymbolicExpression::ExprExprHashMap &index)
	Undo the normalizations that were performed earlier.

Protected Attributes
LinkMode	linkage_

std::string	outputText_
	Additional output obtained by satisfiable().

std::vector< SExpr::Ptr >	parsedOutput_

ExprExprMap	evidence_

TermNames	termNames_

Memoizer::Ptr	memoizer_

Progress::Ptr	progress_

Stats	stats

Static Protected Attributes
static boost::mutex	classStatsMutex

static Stats	classStats

Member Typedef Documentation

◆ ExprList

using Rose::BinaryAnalysis::SmtSolver::ExprList = std::vector<SymbolicExpression::Ptr>

Ordered list of expressions.

Definition at line 42 of file SmtSolver.h.

◆ Ptr

using Rose::BinaryAnalysis::SmtSolver::Ptr = SmtSolverPtr

Reference counting pointer for SMT solvers.

Definition at line 45 of file SmtSolver.h.

◆ Availability

using Rose::BinaryAnalysis::SmtSolver::Availability = std::map<std::string, bool>

Solver availability map.

Definition at line 48 of file SmtSolver.h.

◆ StringTypePair

using Rose::BinaryAnalysis::SmtSolver::StringTypePair = std::pair<std::string, Type>

Maps expression nodes to term names.

This map is populated for common subexpressions.

Definition at line 66 of file SmtSolver.h.

◆ TermNames

using Rose::BinaryAnalysis::SmtSolver::TermNames = Sawyer::Container::Map<SymbolicExpression::Ptr, StringTypePair>

Definition at line 67 of file SmtSolver.h.

◆ ExprExprMap

using Rose::BinaryAnalysis::SmtSolver::ExprExprMap = Sawyer::Container::Map<SymbolicExpression::Ptr, SymbolicExpression::Ptr>

Maps one symbolic expression to another.

Definition at line 70 of file SmtSolver.h.

◆ VariableSet

using Rose::BinaryAnalysis::SmtSolver::VariableSet = Sawyer::Container::Set<SymbolicExpression::LeafPtr, CompareLeavesByName>

Set of variables.

Definition at line 178 of file SmtSolver.h.

◆ Definitions

using Rose::BinaryAnalysis::SmtSolver::Definitions = std::set<uint64_t>

Free variables that have been defined.

Definition at line 180 of file SmtSolver.h.

◆ SExprTypePair

using Rose::BinaryAnalysis::SmtSolver::SExprTypePair = std::pair<SExpr::Ptr, Type>

Definition at line 202 of file SmtSolver.h.

◆ Evidence

using Rose::BinaryAnalysis::SmtSolver::Evidence = Sawyer::Container::Map<std::string , SymbolicExpression::Ptr >

Evidence of satisfiability.

Definition at line 566 of file SmtSolver.h.

Member Enumeration Documentation

◆ LinkMode

enum Rose::BinaryAnalysis::SmtSolver::LinkMode

Bit flags to indicate the kind of solver interface.

Enumerator
LM_NONE	No available linkage.
LM_LIBRARY	A runtime library is available.
LM_EXECUTABLE	An executable is available.
LM_ANY	Any available mode.

Definition at line 51 of file SmtSolver.h.

◆ Type

enum Rose::BinaryAnalysis::SmtSolver::Type

Type (sort) of expression.

ROSE uses bit constants "#b1" and "#b0" (in SMT-LIB syntax) to represent Boolean true and false, but most solvers distinguish between bit vector and Boolean types and don't allow them to be mixed (e.g., "(and #b1 true)" is an error).

Definition at line 63 of file SmtSolver.h.

◆ Satisfiable

enum Rose::BinaryAnalysis::SmtSolver::Satisfiable

Satisfiability constants.

Enumerator
SAT_NO	Provably unsatisfiable.
SAT_YES	Satisfiable and evidence of satisfiability may be available.
SAT_UNKNOWN	Could not be proved satisfiable or unsatisfiable.

Definition at line 87 of file SmtSolver.h.

Constructor & Destructor Documentation

◆ SmtSolver()

Rose::BinaryAnalysis::SmtSolver::SmtSolver	(	const std::string &	name,
		unsigned	linkages
	)

inlineprotected

Construct with name and linkage.

Every solver should have a name that will appear in diagnostic messages, such as "z3", and a linkage mode that describes how ROSE communicates with the solver. The linkage mode is chosen as the least significant set bit of linkages, therefore the subclass should ensure that linkages contains only valid bits. If linkages is zero then the constructed object will be useless since it has no way to communicate with the solver. You can check for this situation by reading the linkage property, or just wait for one of the other methods to throw an SmtSolver::Exception.

Definition at line 359 of file SmtSolver.h.

Member Function Documentation

◆ create()

virtual Ptr Rose::BinaryAnalysis::SmtSolver::create ( ) const

pure virtual

Virtual constructor.

The new solver will have the same settings as the source solver.

Implemented in Rose::BinaryAnalysis::SmtlibSolver, and Rose::BinaryAnalysis::Z3Solver.

◆ availability()

static Availability Rose::BinaryAnalysis::SmtSolver::availability ( )

static

Availability of all known solvers.

Returns a map whose keys are the names of the SMT solver APIs and whose value is true if the solver is avilable or false if not available.

◆ instance()

static Ptr Rose::BinaryAnalysis::SmtSolver::instance ( const std::string & name )

static

Allocate a new solver by name.

Create a new solver using one of the names returned by availability. The special name "" means no solver (return null) and "best" means return bestAvailable (which might also be null). It may be possible to create solvers by name that are not available, but attempting to use such a solver will fail loudly by calling requireLinkage. If an invalid name is supplied then an SmtSolver::Exception is thrown.

◆ bestAvailable()

static Ptr Rose::BinaryAnalysis::SmtSolver::bestAvailable ( )

static

Best available solver.

Returns a new solver, an instance of the best available solver. If no solver is possible then returns null.

◆ name() [1/2]

const std::string & Rose::BinaryAnalysis::SmtSolver::name ( ) const

inline

Property: Name of solver for debugging.

This name gets printed in various diagnostic messages. It's initialized to something reasonable by constructors, but can be changed at any time by the user.

Definition at line 404 of file SmtSolver.h.

Referenced by Rose::BinaryAnalysis::SmtlibSolver::instance().

◆ name() [2/2]

void Rose::BinaryAnalysis::SmtSolver::name ( const std::string & s )

inline

Property: Name of solver for debugging.

This name gets printed in various diagnostic messages. It's initialized to something reasonable by constructors, but can be changed at any time by the user.

Definition at line 405 of file SmtSolver.h.

◆ linkage()

LinkMode Rose::BinaryAnalysis::SmtSolver::linkage ( ) const

inline

Property: How ROSE communicates with the solver.

The linkage is set when the solver object is created, and is read-only.

Definition at line 411 of file SmtSolver.h.

◆ requireLinkage()

void Rose::BinaryAnalysis::SmtSolver::requireLinkage ( LinkMode ) const

Assert required linkage.

If the specified linkage is not available, then throw an exception.

◆ bestLinkage()

static LinkMode Rose::BinaryAnalysis::SmtSolver::bestLinkage ( unsigned linkages )

static

Given a bit vector of linkages, return the best one.

"Best" is defined as that with the best performance, which is usually direct calls to the solver's API.

◆ memoizer() [1/2]

Memoizer::Ptr Rose::BinaryAnalysis::SmtSolver::memoizer ( ) const

Property: Memoizer.

The value of this property is a pointer to the object that caches the memoization for this solver. Setting it to a non-null pointer turns on memoization (using that object) and setting it to a null pointer turns off memoization. Memoization can be turned on or off at any time, and multiple SMT solvers can share the same memoizer.

◆ memoizer() [2/2]

void Rose::BinaryAnalysis::SmtSolver::memoizer ( const Memoizer::Ptr & )

Property: Memoizer.

The value of this property is a pointer to the object that caches the memoization for this solver. Setting it to a non-null pointer turns on memoization (using that object) and setting it to a null pointer turns off memoization. Memoization can be turned on or off at any time, and multiple SMT solvers can share the same memoizer.

◆ timeout()

virtual void Rose::BinaryAnalysis::SmtSolver::timeout ( boost::chrono::duration< double > seconds )

pure virtual

Set the timeout for the solver.

This sets the maximum time that the solver will try to find a solution before returning "unknown".

Implemented in Rose::BinaryAnalysis::SmtlibSolver, and Rose::BinaryAnalysis::Z3Solver.

◆ triviallySatisfiable()

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::triviallySatisfiable ( const ExprList & exprs )

virtual

Determines if expressions are trivially satisfiable or unsatisfiable.

If all expressions are known 1-bit values that are true, then this function returns SAT_YES. If any expression is a known 1-bit value that is false, then this function returns SAT_NO. Otherwise this function returns SAT_UNKNOWN.

This is a high-level abstraction that resets this object state so it contains a single assertion set on its stack, and clears evidence of satisfiability.

◆ satisfiable() [1/2]

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::satisfiable ( const SymbolicExpression::Ptr & )

virtual

Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.

This is a high-level abstraction that starts a new SMT solver session. For text-based interfaces, this solver object is reset, a temporary text file is created, the solver is run with the file as input, text output is read, and the evidence of satisfiability is parsed and stored in this object.

◆ satisfiable() [2/2]

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::satisfiable ( const ExprList & )

virtual

Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.

This is a high-level abstraction that starts a new SMT solver session. For text-based interfaces, this solver object is reset, a temporary text file is created, the solver is run with the file as input, text output is read, and the evidence of satisfiability is parsed and stored in this object.

◆ reset()

virtual void Rose::BinaryAnalysis::SmtSolver::reset ( )

virtual

Reset solver state.

Resets the solver to an initial state containing no assertions. The evidence of satisfiability is cleared. For API-based solvers, this function might also create a new solver and/or solver context.

Reimplemented in Rose::BinaryAnalysis::SmtlibSolver, and Rose::BinaryAnalysis::Z3Solver.

◆ errorIfReset() [1/2]

bool Rose::BinaryAnalysis::SmtSolver::errorIfReset ( ) const

inline

Property: Throw an exception if the solver is reset.

This is used mostly for debugging solvers that are intending to use transactions. If the solver is ever reset, say by accidentally invoking its satisfiable method, then an exception is thrown.

Definition at line 485 of file SmtSolver.h.

◆ errorIfReset() [2/2]

void Rose::BinaryAnalysis::SmtSolver::errorIfReset ( bool b )

inline

Property: Throw an exception if the solver is reset.

This is used mostly for debugging solvers that are intending to use transactions. If the solver is ever reset, say by accidentally invoking its satisfiable method, then an exception is thrown.

Definition at line 488 of file SmtSolver.h.

◆ push()

virtual void Rose::BinaryAnalysis::SmtSolver::push ( )

virtual

Create a backtracking point.

Pushes a new, empty set of assertions onto the solver stack.

Note that although text-based solvers (executables) accept push and pop methods, they have no effect on the speed of the solver because ROSE invokes the executable in batch mode. In this case the push and pop apply to the stack within this solver object in ROSE.

◆ pop()

virtual void Rose::BinaryAnalysis::SmtSolver::pop ( )

virtual

Pop a backtracking point.

Pops the top set of assertions from the solver stack. It is not legal to call pop when the assertion stack is only one level deep; use reset in that case instead.

◆ nLevels()

virtual size_t Rose::BinaryAnalysis::SmtSolver::nLevels ( ) const

inlinevirtual

Number of backtracking levels.

This is the number of sets of assertions. The push and pop increment and decrement this number. The return valued is always positive.

Definition at line 516 of file SmtSolver.h.

◆ nAssertions()

virtual size_t Rose::BinaryAnalysis::SmtSolver::nAssertions ( size_t backtrackingLevel )

virtual

Number of assertions at a specific backtracking level.

Backtracking levels are numbered starting at zero up to one less than the value returned by nLevels.

◆ insert() [1/2]

virtual void Rose::BinaryAnalysis::SmtSolver::insert ( const SymbolicExpression::Ptr & )

virtual

Insert assertions.

Inserts assertions into the set of assertions at the top of the backtracking stack.

◆ insert() [2/2]

virtual void Rose::BinaryAnalysis::SmtSolver::insert ( const ExprList & )

virtual

Insert assertions.

Inserts assertions into the set of assertions at the top of the backtracking stack.

◆ assertions() [1/2]

virtual ExprList Rose::BinaryAnalysis::SmtSolver::assertions ( ) const

virtual

All assertions.

Returns the list of all assertions across all backtracking points.

◆ assertions() [2/2]

virtual const ExprList & Rose::BinaryAnalysis::SmtSolver::assertions ( size_t level ) const

virtual

Assertions for a particular level.

Returns the assertions associated with a particular level of the stack. Level zero is the oldest entry in the stack; all smt objects have a level zero. See also, nLevels.

◆ check()

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::check ( )

virtual

Check satisfiability of current stack.

Checks whether all assertions in the entire stack of assertion sets are satisfiable. A set of no assertions is trivially satisfiable. Errors are emitted on mlog once per error message and returned as SAT_UNKNOWN.

◆ checkTrivial()

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::checkTrivial ( )

virtual

Check whether the stack of assertions is trivially satisfiable.

This function returns true if all assertions have already been simplified in ROSE to the single bit "1", and returns true if so; false otherwise. If no assertions are present, this function returns true. This function does not invoke any functions in the underlying SMT solver.

◆ evidenceNames()

virtual std::vector< std::string > Rose::BinaryAnalysis::SmtSolver::evidenceNames ( ) const

virtual

Names of items for which satisfiability evidence exists.

Returns a vector of strings (variable names or memory addresses) that can be passed to evidenceForName. Not all SMT solvers can return this information, in which case they return an empty vector.

The returned names are only for those variables and addresses whose evidence of satisfiability can be parsed by ROSE. The subclasses provide additional methods for obtaining more detailed information.

◆ evidenceForName()

virtual SymbolicExpression::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForName ( const std::string & ) const

virtual

Evidence of satisfiability for a variable or memory address.

If the string starts with the letter 'v' then variable evidence is returned, otherwise the string must be an address. Valid strings are those returned by the evidenceNames method; other strings result in a null return value. Subclasses might define additional methods for obtaining evidence of satisfiability.

Referenced by evidenceForVariable().

◆ evidenceByName()

Evidence Rose::BinaryAnalysis::SmtSolver::evidenceByName ( ) const

All evidence of satisfiability.

The version that returns a map indexed by variable name is the same as calling evidenceNames and then evidenceForName for each of those names.

The version that returns a map indexed by symbolic expression returns all the evidence in symbolic form. The keys for that return value are symbolic expressions that are simply variables.

Evidence is only returned if the previous check was satisfiable. Otherwise the return value is an empty map.

◆ evidence()

ExprExprMap Rose::BinaryAnalysis::SmtSolver::evidence ( ) const

All evidence of satisfiability.

The version that returns a map indexed by variable name is the same as calling evidenceNames and then evidenceForName for each of those names.

The version that returns a map indexed by symbolic expression returns all the evidence in symbolic form. The keys for that return value are symbolic expressions that are simply variables.

Evidence is only returned if the previous check was satisfiable. Otherwise the return value is an empty map.

◆ clearEvidence()

virtual void Rose::BinaryAnalysis::SmtSolver::clearEvidence ( )

virtual

Clears evidence information.

Evidence of satisfiability is cleared by calling this function or by calling any function that changes the state of the solver, such as pushing or popping assertion sets, inserting new assertions, or checking satisfiability. Checking satisfiability re-initializes the evidence.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

◆ evidenceForVariable() [1/2]

virtual SymbolicExpression::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForVariable ( const SymbolicExpression::Ptr & var )

inlinevirtual

Evidence of satisfiability for a bitvector variable.

If an expression is satisfiable, this function will return a value for the specified bitvector variable that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the variable.

Definition at line 617 of file SmtSolver.h.

References evidenceForVariable().

Referenced by evidenceForVariable().

◆ evidenceForVariable() [2/2]

virtual SymbolicExpression::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForVariable ( uint64_t varno )

inlinevirtual

Evidence of satisfiability for a bitvector variable.

If an expression is satisfiable, this function will return a value for the specified bitvector variable that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the variable.

Definition at line 622 of file SmtSolver.h.

References evidenceForName().

◆ evidenceForAddress()

virtual SymbolicExpression::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForAddress ( uint64_t addr )

virtual

Evidence of satisfiability for a memory address.

If an expression is satisfiable, this function will return a value for the specified memory address that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the memory address.

◆ statistics()

const Stats & Rose::BinaryAnalysis::SmtSolver::statistics ( ) const

inline

Property: Statistics for this solver.

The statistics are not reset by this call, but continue to accumulate.

Definition at line 645 of file SmtSolver.h.

◆ classStatistics()

static Stats Rose::BinaryAnalysis::SmtSolver::classStatistics ( )

static

Property: Statistics across all solvers.

The class statistics are updated whenever a solver is destroyed or its resetStatistics method is invoked. However, the nSolversCreated member is updated as soon as a solver is created.

The statistics are not reset by this call, but continue to accumulate.

◆ resetClassStatistics()

static void Rose::BinaryAnalysis::SmtSolver::resetClassStatistics ( )

static

Resets statistics for the class.

Statistics are reset to initial values for the class as a whole. Resetting statistics for the class does not affect statistics of any particular SMT solver object.

◆ progress() [1/2]

Progress::Ptr Rose::BinaryAnalysis::SmtSolver::progress ( ) const

Progress reporting object.

If non-null, certain types of actions are reported to this progress object by pushing subtask progress objects.

◆ progress() [2/2]

void Rose::BinaryAnalysis::SmtSolver::progress ( const Progress::Ptr & progress )

Progress reporting object.

If non-null, certain types of actions are reported to this progress object by pushing subtask progress objects.

◆ generateFile()

virtual void Rose::BinaryAnalysis::SmtSolver::generateFile	(	std::ostream &	,
		const ExprList &	exprs,
		Definitions *
	)

pure virtual

Generates an input file for for the solver.

Usually the input file will be SMT-LIB format, but subclasses might override this to generate some other kind of input. Throws Excecption if the solver does not support an operation that is necessary to determine the satisfiability.

This function is also useful for debugging because it will convert ROSE's symbolic expressions to whatever format is used by the SMT solver.

◆ checkLib()

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::checkLib ( )

protectedvirtual

Check satisfiability using a library API.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

◆ getErrorMessage()

virtual std::string Rose::BinaryAnalysis::SmtSolver::getErrorMessage ( int exitStatus )

protectedvirtual

Error message from running a solver executable.

Given the solver exit status and (implicitly) the output of the solver, either return an error message or the empty string. This can be overridden by subclasses because some solvers exit with non-zero status if you try to get the model when (check-sat) returns not-satisfiable.

Reimplemented in Rose::BinaryAnalysis::SmtlibSolver.

◆ findVariables()

virtual void Rose::BinaryAnalysis::SmtSolver::findVariables	(	const SymbolicExpression::Ptr &	,
		VariableSet &
	)

inlineprotectedvirtual

Return all variables that need declarations.

Reimplemented in Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 703 of file SmtSolver.h.

◆ printSExpression()

static void Rose::BinaryAnalysis::SmtSolver::printSExpression	(	std::ostream &	,
		const SExpr::Ptr &
	)

staticprotected

Print an S-Expr for debugging.

A null pointer is printed as "nil" and an empty list is printed as "()" in order to distinguish the two cases. There should be no null pointers though in well-formed S-Exprs.

◆ getCommand()

virtual std::string Rose::BinaryAnalysis::SmtSolver::getCommand ( const std::string & config_name )

protectedpure virtual

Given the name of a configuration file, return the command that is needed to run the solver.

The first line of stdout emitted by the solver should be the word "sat" or "unsat".

Implemented in Rose::BinaryAnalysis::SmtlibSolver.

◆ parseEvidence()

virtual void Rose::BinaryAnalysis::SmtSolver::parseEvidence ( )

inlineprotectedvirtual

Parses evidence of satisfiability.

Some solvers can emit information about what variable bindings satisfy the expression. This information is parsed by this function and added to a mapping of variable to value.

Reimplemented in Rose::BinaryAnalysis::SmtlibSolver, and Rose::BinaryAnalysis::Z3Solver.

Definition at line 720 of file SmtSolver.h.

◆ normalizeVariables()

static ExprList Rose::BinaryAnalysis::SmtSolver::normalizeVariables	(	const ExprList &	,
		SymbolicExpression::ExprExprHashMap &	index
	)

staticprotected

Normalize expressions by renaming variables.

This is used during memoization to rename all the variables. It performs a depth-first search and renames each variable it encounters. The variables are renumbered starting at zero. The return value is a vector new new expressions, some of which may be the unmodified original expressions if there were no variables. The index is also a return value which indicates how original variables were mapped to new variables.

◆ undoNormalization()

static ExprList Rose::BinaryAnalysis::SmtSolver::undoNormalization	(	const ExprList &	,
		const SymbolicExpression::ExprExprHashMap &	index
	)

staticprotected

Undo the normalizations that were performed earlier.

Each of the specified expressions are rewritten by undoing the variable renaming that was done by normalizeVariables. The index is the same index as returned by normalizeVariables, although the input expressions need not be those same expressions. For each input expression, the expression is rewritten by substituting the inverse of the index. That is, a depth first search is performed on the expression and if the subexpression matches a value of the index, then it's replaced by the corresponding key.

◆ selfTest()

virtual void Rose::BinaryAnalysis::SmtSolver::selfTest ( )

virtual

Unit tests.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

◆ initDiagnostics()

static void Rose::BinaryAnalysis::SmtSolver::initDiagnostics ( )

static

Initialize diagnostic output facilities.

Called when the ROSE library is initialized.

Member Data Documentation

◆ linkage_

LinkMode Rose::BinaryAnalysis::SmtSolver::linkage_

protected

Definition at line 312 of file SmtSolver.h.

◆ outputText_

std::string Rose::BinaryAnalysis::SmtSolver::outputText_

protected

Additional output obtained by satisfiable().

Definition at line 313 of file SmtSolver.h.

◆ parsedOutput_

std::vector<SExpr::Ptr> Rose::BinaryAnalysis::SmtSolver::parsedOutput_

protected

Definition at line 314 of file SmtSolver.h.

◆ evidence_

ExprExprMap Rose::BinaryAnalysis::SmtSolver::evidence_

protected

Definition at line 315 of file SmtSolver.h.

◆ termNames_

TermNames Rose::BinaryAnalysis::SmtSolver::termNames_

protected

Definition at line 316 of file SmtSolver.h.

◆ memoizer_

Memoizer::Ptr Rose::BinaryAnalysis::SmtSolver::memoizer_

protected

Definition at line 317 of file SmtSolver.h.

◆ progress_

Progress::Ptr Rose::BinaryAnalysis::SmtSolver::progress_

protected

Definition at line 318 of file SmtSolver.h.

◆ classStatsMutex

boost::mutex Rose::BinaryAnalysis::SmtSolver::classStatsMutex

staticprotected

Definition at line 321 of file SmtSolver.h.

◆ classStats

Stats Rose::BinaryAnalysis::SmtSolver::classStats

staticprotected

Definition at line 322 of file SmtSolver.h.

◆ stats

Stats Rose::BinaryAnalysis::SmtSolver::stats

protected

Definition at line 323 of file SmtSolver.h.

◆ mlog

Sawyer::Message::Facility Rose::BinaryAnalysis::SmtSolver::mlog

static

Diagnostic facility.

Definition at line 327 of file SmtSolver.h.

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

SmtSolver.h

Description

Classes

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Static Protected Attributes

Member Typedef Documentation

◆ ExprList

◆ Ptr

◆ Availability

◆ StringTypePair

◆ TermNames

◆ ExprExprMap

◆ VariableSet

◆ Definitions

◆ SExprTypePair

◆ Evidence

Member Enumeration Documentation

◆ LinkMode

◆ Type

◆ Satisfiable

Constructor & Destructor Documentation

◆ SmtSolver()

Member Function Documentation

◆ create()

◆ availability()

◆ instance()

◆ bestAvailable()

◆ name() [1/2]

◆ name() [2/2]

◆ linkage()

◆ requireLinkage()

◆ bestLinkage()

◆ memoizer() [1/2]

◆ memoizer() [2/2]

◆ timeout()

◆ triviallySatisfiable()

◆ satisfiable() [1/2]

◆ satisfiable() [2/2]

◆ reset()

◆ errorIfReset() [1/2]

◆ errorIfReset() [2/2]

◆ push()

◆ pop()

◆ nLevels()

◆ nAssertions()

◆ insert() [1/2]

◆ insert() [2/2]

◆ assertions() [1/2]

◆ assertions() [2/2]

◆ check()

◆ checkTrivial()

◆ evidenceNames()

◆ evidenceForName()

◆ evidenceByName()

◆ evidence()

◆ clearEvidence()

◆ evidenceForVariable() [1/2]

◆ evidenceForVariable() [2/2]

◆ evidenceForAddress()

◆ statistics()

◆ classStatistics()

◆ resetClassStatistics()

◆ progress() [1/2]

◆ progress() [2/2]

◆ generateFile()

◆ checkLib()

◆ getErrorMessage()

◆ findVariables()

◆ printSExpression()

◆ getCommand()

◆ parseEvidence()

◆ normalizeVariables()

◆ undoNormalization()

◆ selfTest()

◆ initDiagnostics()