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 35 of file Z3Solver.h.

#include <Rose/BinaryAnalysis/Z3Solver.h>

Inheritance diagram for Rose::BinaryAnalysis::Z3Solver:

[legend]

Collaboration diagram for Rose::BinaryAnalysis::Z3Solver:

[legend]

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

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

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

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

virtual void	reset () override
	Reset solver state.

virtual void	clearEvidence () override
	Clears evidence information.

virtual void	parseEvidence () override
	Parses evidence of satisfiability.

virtual void	pop () override
	Pop a backtracking point.

virtual void	selfTest () override
	Unit tests.

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

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

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

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 (unsigned linkages=LM_ANY)
	Construct Z3 solver preferring library linkage.

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

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.

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
	Z3Solver (unsigned linkages=LM_ANY)

SExprTypePair	outputList (const std::string &name, const SymbolicExpression::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< SymbolicExpression::Ptr > &) override
	Generate definitions for bit-wise XOR functions.

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

virtual SExprTypePair	outputExpression (const SymbolicExpression::Ptr &) override

virtual SExprTypePair	outputArithmeticShiftRight (const SymbolicExpression::InteriorPtr &) 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 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	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.

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

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.

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

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

static Stats	classStats

Constructor & Destructor Documentation

◆ Z3Solver() [1/2]

Rose::BinaryAnalysis::Z3Solver::Z3Solver ( unsigned linkages = LM_ANY )

inlineexplicitprotected

Definition at line 72 of file Z3Solver.h.

◆ ~Z3Solver()

Rose::BinaryAnalysis::Z3Solver::~Z3Solver ( )

inline

Definition at line 86 of file Z3Solver.h.

◆ Z3Solver() [2/2]

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 114 of file Z3Solver.h.

Member Function Documentation

◆ instance()

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 101 of file Z3Solver.h.

◆ create()

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

overridevirtual

Virtual constructor.

Create a new solver just like this one.

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

◆ availableLinkages()

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.

◆ z3Update()

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.

◆ checkLib()

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

overridevirtual

Check satisfiability using a library API.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

◆ reset()

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

◆ clearEvidence()

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

overridevirtual

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.

◆ parseEvidence()

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

overridevirtual

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.

◆ pop()

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

overridevirtual

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.

◆ selfTest()

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

overridevirtual

Unit tests.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

◆ timeout()

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

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

◆ outputBvxorFunctions()

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

overrideprotectedvirtual

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

◆ outputComparisonFunctions()

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

overrideprotectedvirtual

Generate functions for comparison of bitvectors.

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

◆ outputExpression()

virtual SExprTypePair Rose::BinaryAnalysis::Z3Solver::outputExpression ( const SymbolicExpression::Ptr & )

overrideprotectedvirtual

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

◆ outputArithmeticShiftRight()

virtual SExprTypePair Rose::BinaryAnalysis::Z3Solver::outputArithmeticShiftRight ( const SymbolicExpression::InteriorPtr & )

overrideprotectedvirtual

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

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

Z3Solver.h

Description

Public Member Functions

Static Public Member Functions

Protected Member Functions

Additional Inherited Members

Constructor & Destructor Documentation

◆ Z3Solver() [1/2]

◆ ~Z3Solver()

◆ Z3Solver() [2/2]

Member Function Documentation

◆ instance()

◆ create()

◆ availableLinkages()

◆ z3Update()

◆ checkLib()

◆ reset()

◆ clearEvidence()

◆ parseEvidence()

◆ pop()

◆ selfTest()

◆ timeout()

◆ outputBvxorFunctions()

◆ outputComparisonFunctions()

◆ outputExpression()

◆ outputArithmeticShiftRight()