Description

Wrapper around solvers that speak SMT-LIB.

Definition at line 14 of file SmtlibSolver.h.

#include <Rose/BinaryAnalysis/SmtlibSolver.h>

Inheritance diagram for Rose::BinaryAnalysis::SmtlibSolver:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::SmtlibSolver:

[legend]

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

virtual void	reset () override
	Reset solver state.

virtual void	generateFile (std::ostream &, const std::vector< SymbolicExpression::Ptr > &exprs, Definitions *) override

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

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

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

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

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

void	requireLinkage (LinkMode) const
	Assert required linkage.

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

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

Static Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
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.

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

virtual void	parseEvidence () override
	Parses evidence of satisfiability.

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

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

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 SymbolicExpression::Ptr &)

virtual SExprTypePair	outputExpression (const SymbolicExpression::Ptr &)

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

virtual SExprTypePair	outputLeaf (const SymbolicExpression::LeafPtr &)

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

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

virtual SExprTypePair	outputArithmeticShiftRight (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputLogicalShiftRight0 (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputLogicalShiftRight1 (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputShiftLeft0 (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputShiftLeft1 (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputRotateLeft (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputRotateRight (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputXor (const SymbolicExpression::InteriorPtr &)

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

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

virtual SExprTypePair	outputExtract (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputSignExtend (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputUnsignedExtend (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputIte (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputNotEqual (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputSignedCompare (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputUnsignedCompare (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputZerop (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputMultiply (const SymbolicExpression::InteriorPtr &)

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

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

virtual SExprTypePair	outputRead (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputWrite (const SymbolicExpression::InteriorPtr &)

virtual SExprTypePair	outputSet (const SymbolicExpression::InteriorPtr &)

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

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

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

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


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

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

Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
	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.

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

Protected Attributes
Sawyer::Optional< boost::chrono::duration< double > >	timeout_

Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver
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

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

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.

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

Static Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
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.

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

static Stats	classStats

Constructor & Destructor Documentation

◆ SmtlibSolver()

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

inlineexplicitprotected

Definition at line 25 of file SmtlibSolver.h.

Member Function Documentation

◆ instance()

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 SmtlibSolver.h.

References Rose::BinaryAnalysis::SmtSolver::name().

◆ create()

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

overridevirtual

Virtual constructor.

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

Implements Rose::BinaryAnalysis::SmtSolver.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

◆ reset()

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

overridevirtual

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.

◆ getCommand()

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

overridevirtual

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.

◆ getErrorMessage()

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

overridevirtual

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.

◆ findVariables()

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

overridevirtual

Return all variables that need declarations.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

◆ timeout()

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

overridevirtual

Set the timeout for the solver.

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

Implements Rose::BinaryAnalysis::SmtSolver.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

◆ varForSet() [1/2]

void Rose::BinaryAnalysis::SmtlibSolver::varForSet	(	const SymbolicExpression::InteriorPtr &	set,
		const SymbolicExpression::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.

◆ varForSet() [2/2]

SymbolicExpression::LeafPtr Rose::BinaryAnalysis::SmtlibSolver::varForSet ( const SymbolicExpression::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.

◆ parseEvidence()

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

overrideprotectedvirtual

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.

◆ outputBvxorFunctions()

virtual void Rose::BinaryAnalysis::SmtlibSolver::outputBvxorFunctions	(	std::ostream &	,
		const std::vector< SymbolicExpression::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.

◆ outputComparisonFunctions()

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

protectedvirtual

Generate functions for comparison of bitvectors.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

Member Data Documentation

◆ timeout_

Sawyer::Optional<boost::chrono::duration<double> > Rose::BinaryAnalysis::SmtlibSolver::timeout_

protected

Definition at line 21 of file SmtlibSolver.h.

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

SmtlibSolver.h

Description

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Constructor & Destructor Documentation

◆ SmtlibSolver()

Member Function Documentation

◆ instance()

◆ create()

◆ reset()

◆ getCommand()

◆ getErrorMessage()

◆ findVariables()

◆ timeout()

◆ varForSet() [1/2]

◆ varForSet() [2/2]

◆ parseEvidence()

◆ outputBvxorFunctions()

◆ outputComparisonFunctions()

Member Data Documentation

◆ timeout_