Description

Interface to the Z3 SMT solver.

This interface has two modes: it can either talk to a "z3" executable using the SMT-LIB2 format, or it can connect directly to the z3 shared library. The former is easier to debug, but the latter is much faster since it avoids translating to an intermediate text representation both when sending data to the solver and when getting data from the solver. The mode is selected at runtime with the linkage property.

If memoization is enabled, then the Z3 state may lag behind the ROSE state in order to avoid making any calls to Z3 until after the memoization check. If the caller wants to make the Z3 state up-to-date with the ROSE state then he should invoke the z3Update function.

Definition at line 33 of file Z3Solver.h.

#include <Z3Solver.h>

Inheritance diagram for Rose::BinaryAnalysis::Z3Solver:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::Z3Solver:

[legend]

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

	Z3Solver (const boost::filesystem::path &exe, const std::string &shellArgs="")
	Construct Z3 solver using a specified executable. More...

virtual void	z3Update ()
	Updates the Z3 state to match the ROSE state. More...

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

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

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

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

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

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

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

Public Member Functions inherited from Rose::BinaryAnalysis::SmtlibSolver
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 void	findVariables (const SymbolicExpr::Ptr &, VariableSet &) 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	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...

Sawyer::Optional< 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 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 size_t	nAssertions () const
	Total number of assertions across all backtracking levels. 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...

Evidence	evidence ()
	All evidence of satisfiability. 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...

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

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

void	errorIfReset (bool b)
	Property: Throw an exception if the solver is reset. 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...

Static Public Member Functions
static Ptr	instance (unsigned linkages=LM_ANY)
	Construct Z3 solver preferring library linkage. More...

static unsigned	availableLinkages ()
	Returns a bit vector of linkage capabilities. More...

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

Protected Member Functions
	Z3Solver (unsigned linkages=LM_ANY)

SExprTypePair	outputList (const std::string &name, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)

SExprTypePair	outputList (const std::string &name, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE)

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

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

virtual SExprTypePair	outputExpression (const SymbolicExpr::Ptr &) ROSE_OVERRIDE

virtual SExprTypePair	outputArithmeticShiftRight (const SymbolicExpr::InteriorPtr &) ROSE_OVERRIDE

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

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

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

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	Ptr = SmtSolverPtr
	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

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

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

Protected Types inherited from Rose::BinaryAnalysis::SmtlibSolver
typedef boost::unordered_map< SymbolicExpr::Hash, ExprExprMap >	MemoizedEvidence

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

Protected Attributes inherited from Rose::BinaryAnalysis::SmtlibSolver
ExprExprMap	evidence

MemoizedEvidence	memoizedEvidence

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

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_

Sawyer::Optional< SymbolicExpr::Hash >	latestMemoizationId_

SymbolicExpr::ExprExprHashMap	latestMemoizationRewrite_

Stats	stats

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

static Stats	classStats

Constructor & Destructor Documentation

Rose::BinaryAnalysis::Z3Solver::Z3Solver	(	const boost::filesystem::path &	exe,
		const std::string &	shellArgs = `""`
	)

inlineexplicit

Construct Z3 solver using a specified executable.

The exe should be only the name of the Z3 executable. The shellArgs are the rest of the command-line, all of which will be passed through a shell. The caller is responsible for appropriately escaping shell meta characters.

Definition at line 108 of file Z3Solver.h.

Member Function Documentation

static Ptr Rose::BinaryAnalysis::Z3Solver::instance ( unsigned linkages = LM_ANY )

inlinestatic

Construct Z3 solver preferring library linkage.

If executable (LM_EXECUTABLE) linkage is specified then the executable is that which was detected by the ROSE configuration script.

Definition at line 93 of file Z3Solver.h.

Referenced by create().

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

inlinevirtual

Virtual constructor.

Create a new solver just like this one.

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 100 of file Z3Solver.h.

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

static unsigned Rose::BinaryAnalysis::Z3Solver::availableLinkages ( )

static

Returns a bit vector of linkage capabilities.

Returns a vector of LinkMode bits that say what possible modes of communicating with the Z3 SMT solver are available. A return value of zero means the Z3 solver is not supported in this configuration of ROSE.

virtual void Rose::BinaryAnalysis::Z3Solver::z3Update ( )

virtual

Updates the Z3 state to match the ROSE state.

ROSE tries to avoid making any Z3 calls until it knows they're necessary. Therefore the Z3 state may lag behind the ROSE state. This function's purpose is to bring the Z3 state up-to-date with the ROSE state. You may call it as often as you like, and it is called automatically by some other functions in this API.

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

virtual

Check satisfiability using a library API.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

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

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

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

virtual

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

virtual void Rose::BinaryAnalysis::Z3Solver::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.

Description

Public Member Functions

Static Public Member Functions

Protected Member Functions

Additional Inherited Members

Constructor & Destructor Documentation

Member Function Documentation