#include <ExprSMTLIBPrinter.h>

Collaboration diagram for klee::ExprSMTLIBPrinter:

[legend]

Public Types
enum	SMTLIBv2Logic { QF_ABV , QF_AUFBV }

enum	SMTLIBboolOptions { PRINT_SUCCESS , PRODUCE_MODELS , INTERACTIVE_MODE }

enum	SMTLIBboolValues { OPTION_TRUE , OPTION_FALSE , OPTION_DEFAULT }

enum	ConstantDisplayMode { BINARY , HEX , DECIMAL }

enum	AbbreviationMode { ABBR_NONE , ABBR_LET , ABBR_NAMED }

enum	SMTLIB_SORT { SORT_BITVECTOR , SORT_BOOL }
	Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV. More...

Public Member Functions
bool	setConstantDisplayMode (ConstantDisplayMode cdm)

ConstantDisplayMode	getConstantDisplayMode ()

void	setAbbreviationMode (AbbreviationMode am)

	ExprSMTLIBPrinter ()
	Create a new printer that will print a query in the SMTLIBv2 language. More...

void	setOutput (llvm::raw_ostream &output)

void	setQuery (const Query &q)

	~ExprSMTLIBPrinter ()

void	generateOutput ()

bool	setLogic (SMTLIBv2Logic l)

void	setHumanReadable (bool hr)

bool	setSMTLIBboolOption (SMTLIBboolOptions option, SMTLIBboolValues value)

void	setArrayValuesToGet (const std::vector< const Array * > &a)

bool	isHumanReadable ()

Protected Types
typedef std::map< const ref< Expr >, int >	BindingMap

Protected Member Functions
SMTLIB_SORT	getSort (const ref< Expr > &e)
	Determine the SMTLIBv2 sort of the expression. More...

void	printCastToSort (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT sort)
	Print an expression but cast it to a particular SMTLIBv2 sort first. More...

void	reset ()

void	scanAll ()

void	printNotice ()

void	printOptions ()

void	printSetLogic ()

void	printArrayDeclarations ()

void	printHumanReadableQuery ()

void	printMachineReadableQuery ()

void	printQueryInSingleAssert ()

void	printAction ()

void	printExit ()
	Print the SMTLIBv2 command to exit. More...

void	printConstant (const ref< ConstantExpr > &e)

void	printExpression (const ref< Expr > &e, SMTLIB_SORT expectedSort)

void	scan (const ref< Expr > &e)

void	scanBindingExprDeps ()

void	printReadExpr (const ref< ReadExpr > &e)

void	printExtractExpr (const ref< ExtractExpr > &e)

void	printCastExpr (const ref< CastExpr > &e)

void	printNotEqualExpr (const ref< NeExpr > &e)

void	printSelectExpr (const ref< SelectExpr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)

void	printAShrExpr (const ref< AShrExpr > &e)

void	printSortArgsExpr (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)

void	printLogicalOrBitVectorExpr (const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)

void	printUpdatesAndArray (const UpdateNode un, const Array root)
	Recursively prints updatesNodes. More...

const char *	getSMTLIBKeyword (const ref< Expr > &e)

void	printSeperator ()

void	scanUpdates (const UpdateNode *un)
	Helper function for scan() that scans the expressions of an update node. More...

Protected Attributes
std::set< const Array * >	usedArrays
	Contains the arrays found during scans. More...

std::set< ref< Expr > >	seenExprs
	Set of expressions seen during scan. More...

BindingMap	bindings

std::vector< BindingMap >	orderedBindings

llvm::raw_ostream *	o
	Output stream to write to. More...

const Query *	query
	The query to print. More...

PrintContext *	p
	Helper printer class. More...

ref< Expr >	queryAssert

bool	haveConstantArray
	Indicates if there were any constant arrays founds during a scan() More...

Private Member Functions
const char *	getSMTLIBOptionString (ExprSMTLIBPrinter::SMTLIBboolOptions option)

void	printFullExpression (const ref< Expr > &e, SMTLIB_SORT expectedSort)
	Print expression without top-level abbreviations. More...

void	printAssert (const ref< Expr > &e)
	Print an assert statement for the given expr. More...

Private Attributes
SMTLIBv2Logic	logicToUse

volatile bool	humanReadable

std::map< SMTLIBboolOptions, bool >	smtlibBoolOptions

const std::vector< const Array * > *	arraysToCallGetValueOn

ConstantDisplayMode	cdm

AbbreviationMode	abbrMode

Detailed Description

Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic. Note however the logic can be set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is set to QF_ABV.

This printer abbreviates expressions according to its abbreviation mode.

It is intended to be used as follows

Create instance of this class
Set output ( setOutput() )
Set query to print ( setQuery() )
Set options using the methods prefixed with the word "set".
Call generateOutput()

The class can then be used again on another query ( setQuery() ). The options set are persistent across queries (apart from setArrayValuesToGet() and PRODUCE_MODELS).

Note that in KLEE at the lowest level the solver checks for validity of the query, i.e.

$\forall X constraints(X) \to query(X)$

Where is some assignment, are the constraints in the query and is the query expression. If the above formula is true the query is said to be valid, otherwise it is invalid.

The SMTLIBv2 language works in terms of satisfiability rather than validity so instead this class must ask the equivalent query but in terms of satisfiability which is:

$\lnot \exists X constraints(X) \land \lnot query(X)$

The printed SMTLIBv2 query actually asks the following:

$\exists X constraints(X) \land \lnot query(X)$

Hence the printed SMTLIBv2 query will just assert the constraints and the negation of the query expression.

If a SMTLIBv2 solver says the printed query is satisfiable the then original query passed to this class was invalid and if a SMTLIBv2 solver says the printed query is unsatisfiable then the original query passed to this class was valid.

Definition at line 79 of file ExprSMTLIBPrinter.h.

Member Typedef Documentation

◆ BindingMap

typedef std::map<const ref<Expr>, int> klee::ExprSMTLIBPrinter::BindingMap

protected

Definition at line 220 of file ExprSMTLIBPrinter.h.

Member Enumeration Documentation

◆ AbbreviationMode

enum klee::ExprSMTLIBPrinter::AbbreviationMode

How to abbreviate repeatedly mentioned expressions. Some solvers do not understand all of them, hence the flexibility.

Enumerator
ABBR_NONE	Do not abbreviate.
ABBR_LET	Abbreviate with let.
ABBR_NAMED	Abbreviate with :named annotations.

Definition at line 114 of file ExprSMTLIBPrinter.h.

◆ ConstantDisplayMode

enum klee::ExprSMTLIBPrinter::ConstantDisplayMode

Enumerator
BINARY	Display bit vector constants in binary e.g. #b00101101.
HEX	Display bit vector constants in Hexidecimal e.g.#x2D.
DECIMAL	Display bit vector constants in Decimal e.g. (_ bv45 8)

Definition at line 106 of file ExprSMTLIBPrinter.h.

◆ SMTLIB_SORT

enum klee::ExprSMTLIBPrinter::SMTLIB_SORT

Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV.

Enumerator
SORT_BITVECTOR
SORT_BOOL

Definition at line 121 of file ExprSMTLIBPrinter.h.

◆ SMTLIBboolOptions

enum klee::ExprSMTLIBPrinter::SMTLIBboolOptions

Different SMTLIBv2 options that have a boolean value that can be set

See also: setSMTLIBboolOption

Enumerator
PRINT_SUCCESS	print-success SMTLIBv2 option
PRODUCE_MODELS	produce-models SMTLIBv2 option
INTERACTIVE_MODE	interactive-mode SMTLIBv2 option

Definition at line 91 of file ExprSMTLIBPrinter.h.

◆ SMTLIBboolValues

enum klee::ExprSMTLIBPrinter::SMTLIBboolValues

Different SMTLIBv2 bool option values

See also: setSMTLIBboolOption

Enumerator
OPTION_TRUE	Set option to true.
OPTION_FALSE	Set option to false.
OPTION_DEFAULT	Use solver's defaults (the option will not be set in output)

Definition at line 99 of file ExprSMTLIBPrinter.h.

◆ SMTLIBv2Logic

enum klee::ExprSMTLIBPrinter::SMTLIBv2Logic

Different SMTLIBv2 logics supported by this class

See also: setLogic()

Enumerator
QF_ABV	Logic using Theory of Arrays and Theory of Bitvectors.
QF_AUFBV	Logic using Theory of Arrays and Theory of Bitvectors and has uninterpreted functions

Definition at line 83 of file ExprSMTLIBPrinter.h.

Constructor & Destructor Documentation

◆ ExprSMTLIBPrinter()

klee::ExprSMTLIBPrinter::ExprSMTLIBPrinter ( )

Create a new printer that will print a query in the SMTLIBv2 language.

Definition at line 56 of file ExprSMTLIBPrinter.cpp.

References ExprSMTLIBOptions::abbreviationMode(), ExprSMTLIBOptions::argConstantDisplayMode(), setAbbreviationMode(), and setConstantDisplayMode().

Here is the call graph for this function:

◆ ~ExprSMTLIBPrinter()

klee::ExprSMTLIBPrinter::~ExprSMTLIBPrinter ( )

Definition at line 65 of file ExprSMTLIBPrinter.cpp.

References p.

Member Function Documentation

◆ generateOutput()

void klee::ExprSMTLIBPrinter::generateOutput ( )

Print the query to the llvm::raw_ostream setOutput() and setQuery() must be called before calling this.

All options should be set before calling this.

See also: setConstantDisplayMode; setLogic(); setHumanReadable; setSMTLIBboolOption; setArrayValuesToGet

Mostly it does not matter what order the options are set in. However calling setArrayValuesToGet() implies PRODUCE_MODELS is set so, if a call to setSMTLIBboolOption() is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet() then the setSMTLIBboolOption() call will be ineffective.

Definition at line 517 of file ExprSMTLIBPrinter.cpp.

References humanReadable, o, p, printAction(), printArrayDeclarations(), printExit(), printHumanReadableQuery(), printMachineReadableQuery(), printNotice(), printOptions(), printSetLogic(), and query.

Referenced by klee::Executor::getConstraintLog(), printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::printQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getConstantDisplayMode()

ConstantDisplayMode klee::ExprSMTLIBPrinter::getConstantDisplayMode ( )

inline

Definition at line 128 of file ExprSMTLIBPrinter.h.

References cdm.

◆ getSMTLIBKeyword()

const char * klee::ExprSMTLIBPrinter::getSMTLIBKeyword ( const ref< Expr > & e )

protected

This method does the translation between Expr classes and SMTLIBv2 keywords

Returns: A C-string of the SMTLIBv2 keyword

Definition at line 407 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::Add, klee::Expr::Concat, klee::Expr::Eq, klee::Expr::Extract, klee::Expr::getKind(), klee::Expr::LShr, klee::Expr::Mul, klee::Expr::Ne, klee::Expr::Read, klee::Expr::SDiv, klee::Expr::Select, klee::Expr::SExt, klee::Expr::Sge, klee::Expr::Sgt, klee::Expr::Shl, klee::Expr::Sle, klee::Expr::Slt, klee::Expr::SRem, klee::Expr::Sub, klee::Expr::UDiv, klee::Expr::Uge, klee::Expr::Ugt, klee::Expr::Ule, klee::Expr::Ult, klee::Expr::URem, and klee::Expr::ZExt.

Referenced by printCastExpr(), printExtractExpr(), printReadExpr(), printSelectExpr(), and printSortArgsExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getSMTLIBOptionString()

const char * klee::ExprSMTLIBPrinter::getSMTLIBOptionString ( ExprSMTLIBPrinter::SMTLIBboolOptions option )

private

Definition at line 1153 of file ExprSMTLIBPrinter.cpp.

References INTERACTIVE_MODE, PRINT_SUCCESS, and PRODUCE_MODELS.

Referenced by printOptions().

Here is the caller graph for this function:

◆ getSort()

ExprSMTLIBPrinter::SMTLIB_SORT klee::ExprSMTLIBPrinter::getSort ( const ref< Expr > & e )

protected

Determine the SMTLIBv2 sort of the expression.

Definition at line 930 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::And, klee::Expr::Bool, klee::Expr::Constant, klee::Expr::Eq, klee::Expr::getKid(), klee::Expr::getKind(), getSort(), klee::Expr::getWidth(), klee::Expr::Ne, klee::Expr::Not, klee::Expr::NotOptimized, klee::Expr::Or, klee::Expr::Sge, klee::Expr::Sgt, klee::Expr::Sle, klee::Expr::Slt, SORT_BITVECTOR, SORT_BOOL, klee::Expr::Uge, klee::Expr::Ugt, klee::Expr::Ule, klee::Expr::Ult, and klee::Expr::Xor.

Referenced by getSort(), printAssert(), printExpression(), and printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isHumanReadable()

bool klee::ExprSMTLIBPrinter::isHumanReadable ( )

Returns: True if human readable mode is switched on

Definition at line 99 of file ExprSMTLIBPrinter.cpp.

References humanReadable.

◆ printAction()

void klee::ExprSMTLIBPrinter::printAction ( )

protected

Print the SMTLIBv2 command to check satisfiability and also optionally request for values

See also: setArrayValuesToGet()

Definition at line 667 of file ExprSMTLIBPrinter.cpp.

References arraysToCallGetValueOn, klee::Array::getDomain(), o, and klee::Array::size.

Referenced by generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printArrayDeclarations()

void klee::ExprSMTLIBPrinter::printArrayDeclarations ( )

protected

Definition at line 562 of file ExprSMTLIBPrinter.cpp.

References PrintContext::breakLineI(), klee::Array::constantValues, klee::Array::getDomain(), haveConstantArray, humanReadable, klee::Array::isConstantArray(), klee::Array::name, o, p, PrintContext::popIndent(), printConstant(), printSeperator(), PrintContext::pushIndent(), and usedArrays.

Referenced by generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printAShrExpr()

void klee::ExprSMTLIBPrinter::printAShrExpr ( const ref< AShrExpr > & e )

protected

Definition at line 340 of file ExprSMTLIBPrinter.cpp.

References klee::ConstantExpr::create(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.

Referenced by printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printAssert()

void klee::ExprSMTLIBPrinter::printAssert ( const ref< Expr > & e )

private

Print an assert statement for the given expr.

Definition at line 859 of file ExprSMTLIBPrinter.cpp.

References ABBR_LET, abbrMode, bindings, PrintContext::breakLineI(), getSort(), orderedBindings, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BOOL.

Referenced by printHumanReadableQuery(), and printQueryInSingleAssert().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printCastExpr()

void klee::ExprSMTLIBPrinter::printCastExpr ( const ref< CastExpr > & e )

protected

Definition at line 309 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.

Referenced by printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printCastToSort()

void klee::ExprSMTLIBPrinter::printCastToSort	(	const ref< Expr > &	e,
		ExprSMTLIBPrinter::SMTLIB_SORT	sort
	)

protected

Print an expression but cast it to a particular SMTLIBv2 sort first.

Definition at line 963 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::Bool, PrintContext::breakLine(), PrintContext::breakLineI(), klee::Expr::getWidth(), humanReadable, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), SORT_BITVECTOR, and SORT_BOOL.

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printConstant()

void klee::ExprSMTLIBPrinter::printConstant ( const ref< ConstantExpr > & e )

protected

Print a Constant in the format specified by the current "Constant Display Mode"

Definition at line 109 of file ExprSMTLIBPrinter.cpp.

References BINARY, cdm, DECIMAL, HEX, and p.

Referenced by printArrayDeclarations(), and printFullExpression().

Here is the caller graph for this function:

◆ printExit()

void klee::ExprSMTLIBPrinter::printExit ( )

protected

Print the SMTLIBv2 command to exit.

Definition at line 826 of file ExprSMTLIBPrinter.cpp.

References o.

Referenced by generateOutput().

Here is the caller graph for this function:

◆ printExpression()

void klee::ExprSMTLIBPrinter::printExpression	(	const ref< Expr > &	e,
		ExprSMTLIBPrinter::SMTLIB_SORT	expectedSort
	)

protected

Recursively print expression

Parameters

e	is the expression to print
expectedSort	is the sort we want. If "e" is not of the right type a cast will be performed.
abbrMode	the abbreviation mode to use for this expression

Definition at line 167 of file ExprSMTLIBPrinter.cpp.

References ABBR_LET, ABBR_NAMED, ABBR_NONE, abbrMode, bindings, getSort(), p, printCastToSort(), and printFullExpression().

Referenced by printAShrExpr(), printAssert(), printCastExpr(), printCastToSort(), printExtractExpr(), printFullExpression(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSortArgsExpr(), and printUpdatesAndArray().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printExtractExpr()

void klee::ExprSMTLIBPrinter::printExtractExpr ( const ref< ExtractExpr > & e )

protected

Definition at line 291 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BITVECTOR.

Referenced by printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printFullExpression()

void klee::ExprSMTLIBPrinter::printFullExpression	(	const ref< Expr > &	e,
		ExprSMTLIBPrinter::SMTLIB_SORT	expectedSort
	)

private

Print expression without top-level abbreviations.

Definition at line 208 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::And, klee::Expr::AShr, klee::Expr::Constant, klee::Expr::Eq, klee::Expr::Extract, klee::Expr::getKid(), klee::Expr::getKind(), getSort(), klee::Expr::Ne, klee::Expr::Not, klee::Expr::NotOptimized, klee::Expr::Or, printAShrExpr(), printCastExpr(), printConstant(), printExpression(), printExtractExpr(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSortArgsExpr(), klee::Expr::Read, klee::Expr::Select, klee::Expr::SExt, SORT_BITVECTOR, klee::Expr::Xor, and klee::Expr::ZExt.

Referenced by printExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printHumanReadableQuery()

void klee::ExprSMTLIBPrinter::printHumanReadableQuery ( )

protected

Definition at line 623 of file ExprSMTLIBPrinter.cpp.

References ABBR_LET, abbrMode, klee::Query::constraints, klee::Expr::createIsZero(), klee::Query::expr, humanReadable, o, printAssert(), printQueryInSingleAssert(), query, and queryAssert.

Referenced by generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printLogicalOrBitVectorExpr()

void klee::ExprSMTLIBPrinter::printLogicalOrBitVectorExpr	(	const ref< Expr > &	e,
		ExprSMTLIBPrinter::SMTLIB_SORT	s
	)

protected

For the set of operators that come in two sorts (e.g. (and () ()) (bvand () ()) ) These are and,xor,or,not

Parameters

e	the Expression to print
s	the sort of the expression we want

Definition at line 1064 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::And, klee::Expr::getKid(), klee::Expr::getKind(), klee::Expr::getNumKids(), klee::Expr::Not, klee::Expr::Or, p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), SORT_BITVECTOR, and klee::Expr::Xor.

Referenced by printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printMachineReadableQuery()

void klee::ExprSMTLIBPrinter::printMachineReadableQuery ( )

protected

Definition at line 645 of file ExprSMTLIBPrinter.cpp.

References humanReadable, and printQueryInSingleAssert().

Referenced by generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printNotEqualExpr()

void klee::ExprSMTLIBPrinter::printNotEqualExpr ( const ref< NeExpr > & e )

protected

◆ printNotice()

void klee::ExprSMTLIBPrinter::printNotice ( )

protected

Definition at line 843 of file ExprSMTLIBPrinter.cpp.

References o.

Referenced by generateOutput().

Here is the caller graph for this function:

◆ printOptions()

void klee::ExprSMTLIBPrinter::printOptions ( )

protected

Definition at line 849 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBOptionString(), o, and smtlibBoolOptions.

Referenced by generateOutput().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printQueryInSingleAssert()

void klee::ExprSMTLIBPrinter::printQueryInSingleAssert ( )

protected

Definition at line 651 of file ExprSMTLIBPrinter.cpp.

References klee::ConstraintSet::begin(), klee::Query::constraints, klee::Expr::createIsZero(), klee::ConstraintSet::end(), klee::Query::expr, printAssert(), query, and queryAssert.

Referenced by printHumanReadableQuery(), and printMachineReadableQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printReadExpr()

void klee::ExprSMTLIBPrinter::printReadExpr ( const ref< ReadExpr > & e )

protected

Definition at line 273 of file ExprSMTLIBPrinter.cpp.

References klee::ref< T >::get(), getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), printUpdatesAndArray(), PrintContext::pushIndent(), and SORT_BITVECTOR.

Referenced by printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printSelectExpr()

void klee::ExprSMTLIBPrinter::printSelectExpr	(	const ref< SelectExpr > &	e,
		ExprSMTLIBPrinter::SMTLIB_SORT	s
	)

protected

Definition at line 1020 of file ExprSMTLIBPrinter.cpp.

References getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), PrintContext::pushIndent(), and SORT_BOOL.

Referenced by printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printSeperator()

void klee::ExprSMTLIBPrinter::printSeperator ( )

protected

Definition at line 836 of file ExprSMTLIBPrinter.cpp.

References PrintContext::breakLineI(), humanReadable, p, and PrintContext::write().

Referenced by printArrayDeclarations(), printAShrExpr(), printAssert(), printCastExpr(), printCastToSort(), printExtractExpr(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSortArgsExpr(), and printUpdatesAndArray().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printSetLogic()

void klee::ExprSMTLIBPrinter::printSetLogic ( )

protected

Definition at line 539 of file ExprSMTLIBPrinter.cpp.

References logicToUse, o, QF_ABV, and QF_AUFBV.

Referenced by generateOutput().

Here is the caller graph for this function:

◆ printSortArgsExpr()

void klee::ExprSMTLIBPrinter::printSortArgsExpr	(	const ref< Expr > &	e,
		ExprSMTLIBPrinter::SMTLIB_SORT	s
	)

protected

Definition at line 1048 of file ExprSMTLIBPrinter.cpp.

References klee::Expr::getKid(), klee::Expr::getNumKids(), getSMTLIBKeyword(), p, PrintContext::popIndent(), printExpression(), printSeperator(), and PrintContext::pushIndent().

Referenced by printFullExpression().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printUpdatesAndArray()

void klee::ExprSMTLIBPrinter::printUpdatesAndArray	(	const UpdateNode *	un,
		const Array *	root
	)

protected

Recursively prints updatesNodes.

Definition at line 476 of file ExprSMTLIBPrinter.cpp.

References klee::UpdateNode::index, klee::Array::name, klee::UpdateNode::next, p, PrintContext::popIndent(), printExpression(), printSeperator(), printUpdatesAndArray(), PrintContext::pushIndent(), SORT_BITVECTOR, and klee::UpdateNode::value.

Referenced by printReadExpr(), and printUpdatesAndArray().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reset()

void klee::ExprSMTLIBPrinter::reset ( )

protected

Definition at line 82 of file ExprSMTLIBPrinter.cpp.

References arraysToCallGetValueOn, bindings, haveConstantArray, OPTION_DEFAULT, orderedBindings, PRODUCE_MODELS, seenExprs, setSMTLIBboolOption(), and usedArrays.

Referenced by setQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ scan()

void klee::ExprSMTLIBPrinter::scan ( const ref< Expr > & e )

protected

Scan Expression recursively for Arrays in expressions. Found arrays are added to the usedArrays vector.

Definition at line 692 of file ExprSMTLIBPrinter.cpp.

References bindings, klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getNumKids(), haveConstantArray, scan(), scanUpdates(), seenExprs, and usedArrays.

Referenced by scan(), scanAll(), and scanUpdates().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ scanAll()

void klee::ExprSMTLIBPrinter::scanAll ( )

protected

Definition at line 504 of file ExprSMTLIBPrinter.cpp.

References ABBR_LET, abbrMode, klee::Query::constraints, klee::Query::expr, query, scan(), and scanBindingExprDeps().

Referenced by setQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ scanBindingExprDeps()

void klee::ExprSMTLIBPrinter::scanBindingExprDeps ( )

protected

Scan bindings for expression intra-dependencies. The result is written to the orderedBindings vector that is later used for nested expression printing in the let abbreviation mode.

Definition at line 726 of file ExprSMTLIBPrinter.cpp.

References bindings, klee::Expr::getKid(), klee::Expr::getNumKids(), and orderedBindings.

Referenced by scanAll().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ scanUpdates()

void klee::ExprSMTLIBPrinter::scanUpdates ( const UpdateNode * un )

protected

Helper function for scan() that scans the expressions of an update node.

Definition at line 818 of file ExprSMTLIBPrinter.cpp.

References klee::UpdateNode::index, klee::UpdateNode::next, scan(), and klee::UpdateNode::value.

Referenced by scan().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setAbbreviationMode()

void klee::ExprSMTLIBPrinter::setAbbreviationMode ( AbbreviationMode am )

inline

Definition at line 130 of file ExprSMTLIBPrinter.h.

References abbrMode.

Referenced by ExprSMTLIBPrinter().

Here is the caller graph for this function:

◆ setArrayValuesToGet()

void klee::ExprSMTLIBPrinter::setArrayValuesToGet ( const std::vector< const Array * > & a )

Set the array names that the SMTLIBv2 solver will be asked to determine. Calling this method implies the PRODUCE_MODELS option is true and will change any previously set value.

If no call is made to this function before ExprSMTLIBPrinter::generateOutput() then the solver will only be asked to check satisfiability.

If the passed vector is not empty then the values of those arrays will be requested via (get-value ()) SMTLIBv2 command in the output stream in the same order as vector.

Definition at line 1134 of file ExprSMTLIBPrinter.cpp.

References arraysToCallGetValueOn, OPTION_TRUE, PRODUCE_MODELS, setSMTLIBboolOption(), and usedArrays.

Referenced by printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::printQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setConstantDisplayMode()

bool klee::ExprSMTLIBPrinter::setConstantDisplayMode ( ConstantDisplayMode cdm )

Allows the way Constant bitvectors are printed to be changed. This setting is persistent across queries.

Returns: true if setting the mode was successful

Definition at line 101 of file ExprSMTLIBPrinter.cpp.

References cdm, and DECIMAL.

Referenced by ExprSMTLIBPrinter().

Here is the caller graph for this function:

◆ setHumanReadable()

void klee::ExprSMTLIBPrinter::setHumanReadable ( bool hr )

Sets how readable the printed SMTLIBv2 commands are.

Parameters

hr	If set to true the printed commands are made more human readable.

The printed commands are made human readable by...

Indenting and line breaking.
Adding comments

Definition at line 847 of file ExprSMTLIBPrinter.cpp.

References humanReadable.

◆ setLogic()

bool klee::ExprSMTLIBPrinter::setLogic ( SMTLIBv2Logic l )

Set which SMTLIBv2 logic to use. This only affects what logic is used in the (set-logic <logic>) command. The rest of the printed SMTLIBv2 commands are the same regardless of the logic used.

Returns: true if setting logic was successful.

Definition at line 828 of file ExprSMTLIBPrinter.cpp.

References logicToUse, and QF_AUFBV.

◆ setOutput()

void klee::ExprSMTLIBPrinter::setOutput ( llvm::raw_ostream & output )

Set the output stream that will be printed to. This call is persistent across queries.

Definition at line 69 of file ExprSMTLIBPrinter.cpp.

References o, and p.

Referenced by klee::Executor::getConstraintLog(), printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::SMTLIBLoggingSolver().

Here is the caller graph for this function:

◆ setQuery()

void klee::ExprSMTLIBPrinter::setQuery ( const Query & q )

Set the query to print. This will setArrayValuesToGet() to none (i.e. no array values will be requested using the SMTLIBv2 (get-value ()) command).

Definition at line 76 of file ExprSMTLIBPrinter.cpp.

References query, reset(), and scanAll().

Referenced by klee::Executor::getConstraintLog(), printInputAsSMTLIBv2(), and SMTLIBLoggingSolver::printQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setSMTLIBboolOption()

bool klee::ExprSMTLIBPrinter::setSMTLIBboolOption	(	SMTLIBboolOptions	option,
		SMTLIBboolValues	value
	)

Set SMTLIB options. These options will be printed when generateOutput() is called via the SMTLIBv2 command (set-option :option-name

)

By default no options will be printed so the SMTLIBv2 solver will use its default values for all options.

Returns: true if option was successfully set.

The options set are persistent across calls to setQuery() apart from the PRODUCE_MODELS option which this printer may automatically set/unset.

Definition at line 1104 of file ExprSMTLIBPrinter.cpp.

References INTERACTIVE_MODE, OPTION_DEFAULT, OPTION_TRUE, PRINT_SUCCESS, PRODUCE_MODELS, and smtlibBoolOptions.

Referenced by reset(), and setArrayValuesToGet().

Here is the caller graph for this function:

Member Data Documentation

◆ abbrMode

AbbreviationMode klee::ExprSMTLIBPrinter::abbrMode

private

Definition at line 383 of file ExprSMTLIBPrinter.h.

Referenced by printAssert(), printExpression(), printHumanReadableQuery(), scanAll(), and setAbbreviationMode().

◆ arraysToCallGetValueOn

const std::vector<const Array *>* klee::ExprSMTLIBPrinter::arraysToCallGetValueOn

private

Definition at line 380 of file ExprSMTLIBPrinter.h.

Referenced by printAction(), reset(), and setArrayValuesToGet().

◆ bindings

BindingMap klee::ExprSMTLIBPrinter::bindings

protected

Let expression binding number map. Under the :named abbreviation mode, negative binding numbers indicate that the abbreviation has already been emitted, so it may be used.

Definition at line 225 of file ExprSMTLIBPrinter.h.

Referenced by printAssert(), printExpression(), reset(), scan(), and scanBindingExprDeps().

◆ cdm

ConstantDisplayMode klee::ExprSMTLIBPrinter::cdm

private

Definition at line 382 of file ExprSMTLIBPrinter.h.

Referenced by getConstantDisplayMode(), printConstant(), and setConstantDisplayMode().

◆ haveConstantArray

bool klee::ExprSMTLIBPrinter::haveConstantArray

protected

Indicates if there were any constant arrays founds during a scan()

Definition at line 358 of file ExprSMTLIBPrinter.h.

Referenced by printArrayDeclarations(), reset(), and scan().

◆ humanReadable

volatile bool klee::ExprSMTLIBPrinter::humanReadable

private

Definition at line 363 of file ExprSMTLIBPrinter.h.

Referenced by generateOutput(), isHumanReadable(), printArrayDeclarations(), printCastToSort(), printHumanReadableQuery(), printMachineReadableQuery(), printSeperator(), and setHumanReadable().

◆ logicToUse

SMTLIBv2Logic klee::ExprSMTLIBPrinter::logicToUse

private

Definition at line 361 of file ExprSMTLIBPrinter.h.

Referenced by printSetLogic(), and setLogic().

◆ o

llvm::raw_ostream* klee::ExprSMTLIBPrinter::o

protected

Output stream to write to.

Definition at line 233 of file ExprSMTLIBPrinter.h.

Referenced by generateOutput(), printAction(), printArrayDeclarations(), printExit(), printHumanReadableQuery(), printNotice(), printOptions(), printSetLogic(), and setOutput().

◆ orderedBindings

std::vector<BindingMap> klee::ExprSMTLIBPrinter::orderedBindings

protected

An ordered list of expression bindings. Exprs in BindingMap at index i depend on Exprs in BindingMap at i-1. Exprs in orderedBindings[0] have no dependencies.

Definition at line 230 of file ExprSMTLIBPrinter.h.

Referenced by printAssert(), reset(), and scanBindingExprDeps().

◆ p

PrintContext* klee::ExprSMTLIBPrinter::p

protected

Helper printer class.

Definition at line 351 of file ExprSMTLIBPrinter.h.

Referenced by generateOutput(), printArrayDeclarations(), printAShrExpr(), printAssert(), printCastExpr(), printCastToSort(), printConstant(), printExpression(), printExtractExpr(), printLogicalOrBitVectorExpr(), printReadExpr(), printSelectExpr(), printSeperator(), printSortArgsExpr(), printUpdatesAndArray(), setOutput(), and ~ExprSMTLIBPrinter().

◆ query

const Query* klee::ExprSMTLIBPrinter::query

protected

The query to print.

Definition at line 236 of file ExprSMTLIBPrinter.h.

Referenced by generateOutput(), printHumanReadableQuery(), printQueryInSingleAssert(), scanAll(), and setQuery().

◆ queryAssert

ref<Expr> klee::ExprSMTLIBPrinter::queryAssert

protected

This contains the query from the solver but negated for our purposes.

See also: negateQueryExpression()

Definition at line 355 of file ExprSMTLIBPrinter.h.

Referenced by printHumanReadableQuery(), and printQueryInSingleAssert().

◆ seenExprs

std::set<ref<Expr> > klee::ExprSMTLIBPrinter::seenExprs

protected

Set of expressions seen during scan.

Definition at line 218 of file ExprSMTLIBPrinter.h.

Referenced by reset(), and scan().

◆ smtlibBoolOptions

std::map<SMTLIBboolOptions, bool> klee::ExprSMTLIBPrinter::smtlibBoolOptions

private

Definition at line 366 of file ExprSMTLIBPrinter.h.

Referenced by printOptions(), and setSMTLIBboolOption().

◆ usedArrays

std::set<const Array *> klee::ExprSMTLIBPrinter::usedArrays

protected

Contains the arrays found during scans.

Definition at line 215 of file ExprSMTLIBPrinter.h.

Referenced by printArrayDeclarations(), reset(), scan(), and setArrayValuesToGet().

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

/Users/cristic/klee/include/klee/Expr/ExprSMTLIBPrinter.h
/Users/cristic/klee/lib/Expr/ExprSMTLIBPrinter.cpp

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ BindingMap

Member Enumeration Documentation

◆ AbbreviationMode

◆ ConstantDisplayMode

◆ SMTLIB_SORT

◆ SMTLIBboolOptions

◆ SMTLIBboolValues

◆ SMTLIBv2Logic

Constructor & Destructor Documentation

◆ ExprSMTLIBPrinter()

◆ ~ExprSMTLIBPrinter()

Member Function Documentation

◆ generateOutput()

◆ getConstantDisplayMode()

◆ getSMTLIBKeyword()

◆ getSMTLIBOptionString()

◆ getSort()

◆ isHumanReadable()

◆ printAction()

◆ printArrayDeclarations()

◆ printAShrExpr()

◆ printAssert()

◆ printCastExpr()

◆ printCastToSort()

◆ printConstant()

◆ printExit()

◆ printExpression()

◆ printExtractExpr()

◆ printFullExpression()

◆ printHumanReadableQuery()

◆ printLogicalOrBitVectorExpr()

◆ printMachineReadableQuery()

◆ printNotEqualExpr()

◆ printNotice()

◆ printOptions()

◆ printQueryInSingleAssert()

◆ printReadExpr()

◆ printSelectExpr()

◆ printSeperator()

◆ printSetLogic()

◆ printSortArgsExpr()

◆ printUpdatesAndArray()

◆ reset()

◆ scan()

◆ scanAll()

◆ scanBindingExprDeps()

◆ scanUpdates()

◆ setAbbreviationMode()

◆ setArrayValuesToGet()

◆ setConstantDisplayMode()

◆ setHumanReadable()

◆ setLogic()

◆ setOutput()

◆ setQuery()

◆ setSMTLIBboolOption()

Member Data Documentation

◆ abbrMode

◆ arraysToCallGetValueOn

◆ bindings

◆ cdm

◆ haveConstantArray

◆ humanReadable

◆ logicToUse

◆ o

◆ orderedBindings

◆ p

◆ query

◆ queryAssert

◆ seenExprs

◆ smtlibBoolOptions

◆ usedArrays