Description

Wrapper around solvers that speak SMT-LIB.

Definition at line 12 of file BinarySmtlibSolver.h.

#include <BinarySmtlibSolver.h>

Inheritance diagram for Rose::BinaryAnalysis::SmtlibSolver:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::SmtlibSolver:

[legend]

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

virtual void	reset () ROSE_OVERRIDE
	Reset solver state. More...

virtual void	generateFile (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_OVERRIDE
	Generates an input file for for the solver. More...

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

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

virtual VariableSet	findVariables (const SymbolicExpr::Ptr &) ROSE_OVERRIDE
	Return all variables that need declarations. More...

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

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

virtual void	clearEvidence () ROSE_OVERRIDE
	Clears evidence information. More...

virtual void	clearMemoization () ROSE_OVERRIDE
	Clear memoization table. More...

Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
LinkMode	linkage () const
	Property: How ROSE communicates with the solver. More...

void	requireLinkage (LinkMode) const
	Assert required linkage. More...

SymbolicExpr::Hash	latestMemoizationId () const
	Id for latest memoized result, or zero. More...

virtual size_t	memoizationNEntries () const
	Size of memoization table. More...

virtual Satisfiable	triviallySatisfiable (const std::vector< SymbolicExpr::Ptr > &exprs)
	Determines if expressions are trivially satisfiable or unsatisfiable. More...

virtual void	push ()
	Create a backtracking point. More...

virtual void	pop ()
	Pop a backtracking point. More...

virtual size_t	nLevels () const
	Number of backtracking levels. More...

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

virtual std::vector < SymbolicExpr::Ptr >	assertions () const
	All assertions. More...

virtual std::vector < SymbolicExpr::Ptr >	assertions (size_t level) const
	Assertions for a particular level. More...

virtual Satisfiable	check ()
	Check satisfiability of current stack. More...

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

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

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

void	resetStatistics ()
	Resets statistics for this solver. More...

virtual void	selfTest ()
	Unit tests. More...

virtual Satisfiable	trivially_satisfiable (const std::vector< SymbolicExpr::Ptr > &exprs) ROSE_DEPRECATED("use triviallySatisfiable")

virtual SymbolicExpr::Ptr	evidence_for_variable (uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable")

virtual SymbolicExpr::Ptr	evidence_for_variable (const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable")

virtual SymbolicExpr::Ptr	evidence_for_name (const std::string &) ROSE_DEPRECATED("use evidenceForName")

virtual SymbolicExpr::Ptr	evidence_for_address (uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress")

virtual std::vector< std::string >	evidence_names () ROSE_DEPRECATED("use evidenceNames")

virtual void	clear_evidence () ROSE_DEPRECATED("use clearEvidence")

const Stats &	get_stats () const ROSE_DEPRECATED("use statistics")

void	reset_stats () ROSE_DEPRECATED("use resetStatistics")

void	reset_class_stats () ROSE_DEPRECATED("use resetClassStatistics")

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

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

bool	memoization () const
	Property: Perform memoization. More...

void	memoization (bool b)
	Property: Perform memoization. More...

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

virtual Satisfiable	satisfiable (const std::vector< SymbolicExpr::Ptr > &)
	Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More...

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

virtual void	insert (const std::vector< SymbolicExpr::Ptr > &)
	Insert assertions. More...

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

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

Public Member Functions inherited from Sawyer::SharedObject
	SharedObject ()
	Default constructor. More...

	SharedObject (const SharedObject &)
	Copy constructor. More...

virtual	~SharedObject ()
	Virtual destructor. More...

SharedObject &	operator= (const SharedObject &)
	Assignment. More...

Static Public Member Functions
static Ptr	instance (const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE)
	Construct a solver using the specified program. More...

Static Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
static Availability	availability ()
	Availability of all known solvers. More...

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

static Ptr	bestAvailable ()
	Best available solver. More...

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

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

static void	resetClassStatistics ()
	Resets statistics for the class. More...

static void	initDiagnostics ()
	Initialize diagnostic output facilities. More...

static Stats	get_class_stats () ROSE_DEPRECATED("use classStatistics")

Protected Types
typedef boost::unordered_map < SymbolicExpr::Hash, ExprExprMap >	MemoizedEvidence

Protected Member Functions
	SmtlibSolver (const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE)

virtual void	parseEvidence () ROSE_OVERRIDE
	Parses evidence of satisfiability. More...

virtual void	outputBvxorFunctions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
	Generate definitions for bit-wise XOR functions. More...

virtual void	outputComparisonFunctions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
	Generate functions for comparison of bitvectors. More...

virtual Type	mostType (const std::vector< SExprTypePair > &)

virtual SExprTypePair	outputCast (const SExprTypePair &, Type to)

virtual std::vector < SExprTypePair >	outputCast (const std::vector< SExprTypePair > &, Type to)

virtual std::string	typeName (const SymbolicExpr::Ptr &)

virtual SExprTypePair	outputExpression (const SymbolicExpr::Ptr &)

virtual std::vector < SmtSolver::SExprTypePair >	outputExpressions (const std::vector< SymbolicExpr::Ptr > &)

virtual SExprTypePair	outputLeaf (const SymbolicExpr::LeafPtr &)

virtual SExprTypePair	outputLeftAssoc (const std::string &func, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)

virtual SExprTypePair	outputLeftAssoc (const std::string &func, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE)

virtual SExprTypePair	outputArithmeticShiftRight (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputLogicalShiftRight (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputShiftLeft (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputRotateLeft (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputRotateRight (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputXor (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputBinary (const std::string &func, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)

virtual SExprTypePair	outputUnary (const std::string &funcName, const SExprTypePair &arg)

virtual SExprTypePair	outputExtract (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputSignExtend (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputUnsignedExtend (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputIte (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputNotEqual (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputSignedCompare (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputUnsignedCompare (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputZerop (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputMultiply (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputDivide (const SymbolicExpr::InteriorPtr &, const std::string &operation)

virtual SExprTypePair	outputModulo (const SymbolicExpr::InteriorPtr &, const std::string &operation)

virtual SExprTypePair	outputRead (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputWrite (const SymbolicExpr::InteriorPtr &)

virtual SExprTypePair	outputSet (const SymbolicExpr::InteriorPtr &)

virtual void	outputVariableDeclarations (std::ostream &, const VariableSet &)

virtual void	outputComments (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)

virtual void	outputCommonSubexpressions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)

virtual void	outputAssertion (std::ostream &, const SymbolicExpr::Ptr &)


void	varForSet (const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var)
	Specify variable to use for OP_SET. More...

SymbolicExpr::LeafPtr	varForSet (const SymbolicExpr::InteriorPtr &set)
	Specify variable to use for OP_SET. More...

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

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

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

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

virtual void	generate_file (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_DEPRECATED("use generateFile")

virtual std::string	get_command (const std::string &config_name) ROSE_DEPRECATED("use getCommand")

virtual void	parse_evidence () ROSE_DEPRECATED("use parseEvidence")

Protected Attributes
ExprExprMap	evidence

MemoizedEvidence	memoizedEvidence

Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver
LinkMode	linkage_

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

std::vector< SExpr::Ptr >	parsedOutput_

TermNames	termNames_

Memoization	memoization_

bool	doMemoization_

SymbolicExpr::Hash	latestMemoizationId_

SymbolicExpr::ExprExprHashMap	latestMemoizationRewrite_

Stats	stats

Additional Inherited Members
Public Types inherited from Rose::BinaryAnalysis::SmtSolver
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...

typedef Sawyer::SharedPointer < SmtSolver >	Ptr
	Reference counting pointer for SMT solvers. More...

typedef std::map< std::string, bool >	Availability
	Solver availability map. More...

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

typedef Sawyer::Container::Map < SymbolicExpr::Ptr, StringTypePair >	TermNames

typedef Sawyer::Container::Map < SymbolicExpr::Ptr, SymbolicExpr::Ptr >	ExprExprMap
	Maps one symbolic expression to another. More...

typedef Sawyer::Container::Set < SymbolicExpr::LeafPtr, CompareLeavesByName >	VariableSet
	Set of variables. More...

typedef std::set< uint64_t >	Definitions
	Free variables that have been defined. More...

typedef std::pair< SExpr::Ptr, Type >	SExprTypePair

typedef boost::unordered_map < SymbolicExpr::Hash, Satisfiable >	Memoization

Static Public Attributes inherited from Rose::BinaryAnalysis::SmtSolver
static Sawyer::Message::Facility	mlog
	Diagnostic facility. More...

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

static std::vector < SymbolicExpr::Ptr >	normalizeVariables (const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index)
	Normalize expressions by renaming variables. More...

static std::vector < SymbolicExpr::Ptr >	undoNormalization (const std::vector< SymbolicExpr::Ptr > &, const SymbolicExpr::ExprExprHashMap &index)
	Undo the normalizations that were performed earlier. More...

Static Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver
static boost::mutex	classStatsMutex

static Stats	classStats

Member Function Documentation

static Ptr Rose::BinaryAnalysis::SmtlibSolver::instance	(	const std::string &	name,
		const boost::filesystem::path &	executable,
		const std::string &	shellArgs = `""`,
		unsigned	linkages = `LM_EXECUTABLE`
	)

inlinestatic

Construct a solver using the specified program.

This object will communicate with the SMT solver using SMT-LIB version 2 text files, both for input to the solver and expected output from the solver. Diagnostics from the solver (standard error) are not redirected by the ROSE library. A separate invocation of the solver is used for each satisfiability check.

The executable should be the name of the solver executable, either to be found in $PATH or an absolute file name. Beware that some tools might change directories as they run, so absolute names are usually best. The optional shellArgs are the list of extra arguments to pass to the solver. WARNING: the entire command is pass to popen, which will invoke a shell to process the executable name and arguments; appropriate escaping of shell meta characters is the responsibility of the caller.

Definition at line 41 of file BinarySmtlibSolver.h.

Referenced by create().

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

inlinevirtual

Virtual constructor.

Creates a new solver like this one.

Implements Rose::BinaryAnalysis::SmtSolver.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

Definition at line 49 of file BinarySmtlibSolver.h.

References instance(), Rose::BinaryAnalysis::SmtSolver::linkage(), and Rose::BinaryAnalysis::SmtSolver::name().

virtual void Rose::BinaryAnalysis::SmtlibSolver::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 from Rose::BinaryAnalysis::SmtSolver.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

virtual void Rose::BinaryAnalysis::SmtlibSolver::generateFile	(	std::ostream &	,
		const std::vector< SymbolicExpr::Ptr > &	exprs,
		Definitions *
	)

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.

Implements Rose::BinaryAnalysis::SmtSolver.

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

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".

Implements Rose::BinaryAnalysis::SmtSolver.

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

virtual

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 from Rose::BinaryAnalysis::SmtSolver.

virtual VariableSet Rose::BinaryAnalysis::SmtlibSolver::findVariables ( const SymbolicExpr::Ptr & )

virtual

Return all variables that need declarations.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SmtlibSolver::evidenceForName ( const std::string & )

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.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

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

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.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::SmtlibSolver::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 from Rose::BinaryAnalysis::SmtSolver.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

virtual void Rose::BinaryAnalysis::SmtlibSolver::clearMemoization ( )

virtual

Clear memoization table.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

void Rose::BinaryAnalysis::SmtlibSolver::varForSet	(	const SymbolicExpr::InteriorPtr &	set,
		const SymbolicExpr::LeafPtr &	var
	)

protected

Specify variable to use for OP_SET.

Each OP_SET needs a free variable to choose from the available members of the set. This function sets (two arguments) or retrives (one argument) the variable associated with a set.

SymbolicExpr::LeafPtr Rose::BinaryAnalysis::SmtlibSolver::varForSet ( const SymbolicExpr::InteriorPtr & set )

protected

Specify variable to use for OP_SET.

Each OP_SET needs a free variable to choose from the available members of the set. This function sets (two arguments) or retrives (one argument) the variable associated with a set.

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

protectedvirtual

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 from Rose::BinaryAnalysis::SmtSolver.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

virtual void Rose::BinaryAnalysis::SmtlibSolver::outputBvxorFunctions	(	std::ostream &	,
		const std::vector< SymbolicExpr::Ptr > &
	)

protectedvirtual

Generate definitions for bit-wise XOR functions.

This method scans the supplied list of expressiosn and for each bit-wise XOR operation taking arguments of width n, it emits a binary function definition named "bvxor<em>n</em>".

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

virtual void Rose::BinaryAnalysis::SmtlibSolver::outputComparisonFunctions	(	std::ostream &	,
		const std::vector< SymbolicExpr::Ptr > &
	)

protectedvirtual

Generate functions for comparison of bitvectors.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

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

BinarySmtlibSolver.h

Description

Public Member Functions

Static Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Member Function Documentation