ilasynth Namespace Reference

Classes
class	Abstraction
struct	AbstractionWrapper
struct	assump_visitor_i
class	BitvectorConst
class	BitvectorExpr
class	BitvectorOp
class	BitvectorVar
class	BoogieTranslator
class	BoolConst
class	BoolExpr
class	BoolOp
class	BoolVar
class	BVInRange
class	CFun
struct	Choice
class	ChoiceExpr
class	CppFun
class	CppSimGen
class	CppVar
class	CVar
class	CVerifGen
struct	DistInput
struct	DITree
struct	DITreeNode
class	FuncExpr
class	FuncReduction
class	FuncVar
class	HornClause
class	HornDB
class	HornLiteral
class	HornRewriter
class	HornTranslator
class	HornVar
class	ImExport
class	ITESimplifier
struct	mem_write_entry_t
struct	mem_write_t
struct	MemConst
class	MemExpr
class	MemOp
struct	MemValues
class	MemVar
class	MicroUnroller
class	Node
struct	NodeEqual
struct	NodeEqual< const Node * >
struct	NodeHash
struct	NodeHash< const Node * >
struct	NodeRef
struct	NodeType
struct	NodeVisitorI
struct	npair_t
struct	PyILAException
class	ReadSlice
class	Rewriter
struct	SimoutAdapter
struct	SimOutput
class	SMTExport
struct	SupportVars
class	SynRewriter
class	Synthesizer
class	Unroller
class	VerilogExport
struct	VlgExportConfig
class	WriteSlice
class	Z3ExprAdapter
class	Z3ExprRewritingAdapter
class	Z3FixedpointAdapter

Typedefs
typedef boost::shared_ptr< Abstraction >	abstraction_ptr_t
typedef ChoiceExpr< BitvectorExpr >	BitvectorChoice
typedef ChoiceExpr< BoolExpr >	BoolChoice
typedef ChoiceExpr< MemExpr >	MemChoice
typedef boost::shared_ptr< Node >	nptr_t
typedef std::vector< nptr_t >	nptr_vec_t
typedef std::vector< const Node * >	nodevec_t
typedef std::set< const Node * >	nodeset_t
typedef std::map< std::string, npair_t >	nmap_t
typedef std::unordered_map< const Node *, nptr_t, decltype(&nodeHash), decltype(&nodeEqual)>	rwmap_t
typedef boost::multiprecision::cpp_int	mp_int_t
typedef HornVar *	hvptr_t
typedef HornLiteral *	hlptr_t
typedef HornClause *	hcptr_t
typedef boost::shared_ptr< SimOutput >	simout_ptr_t
typedef boost::shared_ptr< DITreeNode >	dtree_ptr_t
typedef std::string	vlg_name_t
typedef std::string	vlg_stmt_t
typedef std::string	vlg_addr_t
typedef std::string	vlg_data_t
typedef std::vector< vlg_name_t >	vlg_stmts_t
typedef std::pair< vlg_name_t, int >	vlg_sig_t
typedef std::vector< vlg_sig_t >	vlg_sigs_t
typedef std::tuple< vlg_stmt_t, vlg_stmt_t, vlg_stmt_t >	vlg_ite_stmt_t
typedef std::vector< vlg_ite_stmt_t >	vlg_ite_stmts_t
typedef std::pair< vlg_name_t, vlg_sigs_t >	vlg_per_mem_access_t
typedef std::tuple< vlg_name_t, int, int >	vlg_mem_t
typedef std::vector< vlg_mem_t >	vlg_mems_t
typedef std::list< mem_write_entry_t >	mem_write_entry_list_t
typedef std::list< mem_write_entry_list_t >	mem_write_entry_list_stack_t
typedef std::list< mem_write_t >	mem_write_list_t

Enumerations
enum	endianness_t { UNKNOWN_E, LITTLE_E, BIG_E }

Functions
std::size_t	hash_value (const Node &n)
std::size_t	hash_value (const NodeType &ntype)
std::size_t	compute_hash_value (const NodeType &ntype)
template<typename T >
void	choice_hash_combine (std::size_t &seed, const ChoiceExpr< T > *c)
std::ostream &	operator<< (std::ostream &out, const Node &that)
bool	nodeEqual (const Node *left, const Node *right)
size_t	nodeHash (const Node *n)
std::ostream &	operator<< (std::ostream &out, const NodeRef &node)
bool	NEQVarNotExist (const std::string &a1name, const std::string &a2name, const std::string &notExistVarName)
bool	NEQVarTypeMismatch (const std::string &a1name, const std::string &a2name, const std::string &VarName)
bool	NEQArchVarUpdateMismatch (const std::string &a1name, const std::string &a2name, const std::string &VarName)
unsigned	DetermineUnrollBound (Abstraction *pAbs, const std::string &nodeName)
bool	bmc (unsigned n1, Abstraction *a1, NodeRef *r1, unsigned n2, Abstraction *a2, NodeRef *r2)
bool	checkMiter (z3::solver &S, z3::expr &e1, z3::expr &e2)
void	translateILAException (PyILAException const &ex)
std::ostream &	info (const char *s)
std::ostream &	log1 (const char *s)
std::ostream &	log2 (const char *s)
void	initLogging ()
void	setLogLevel (int l, const std::string &name)
void	enableLog (const std::string &name)
void	disableLog (const std::string &name)
void	clearLogs ()
std::ostream &	operator<< (std::ostream &out, const MemValues &mv)
std::ostream &	operator<< (std::ostream &out, const DistInput &di)
std::ostream &	operator<< (std::ostream &out, const SimOutput &simout)
std::ostream &	operator<< (std::ostream &out, NodeType const &ntype)
void	ila_assert (bool b, const char *msg, const char *file, int line)
void	ila_assert (bool b, const std::string &msg, const char *file, int line)
void	dump_trace ()
std::string	to_string (const py::object &l)
std::string	to_string (const mp_int_t &i)
mp_int_t	to_cpp_int (const py::object &l)
py::object	to_pyint (const mp_int_t &i)
py::object	to_pyint (const std::string &s)
bool	is_py_int (const py::object &l)
bool	is_py_int_or_long (const py::object &l)
void	set_logging_level (int level)
std::ostream &	operator<< (std::ostream &out, const mem_write_entry_t &mwe)
std::ostream &	operator<< (std::ostream &out, const mem_write_entry_list_t &mwel)
std::ostream &	operator<< (std::ostream &out, const mem_write_entry_list_stack_t &mwel)
std::ostream &	operator<< (std::ostream &out, const mem_write_t &mw)
std::ostream &	operator<< (std::ostream &out, const mem_write_list_t &mwl)

Variables
const int	NUM_HASHTABLE_BUCKETS = 1023
const int	NUM_HASHTABLE_BUCKETS_SMALL = 63

Typedef Documentation

abstraction_ptr_t

typedef boost::shared_ptr<Abstraction> ilasynth::abstraction_ptr_t

BitvectorChoice

typedef ChoiceExpr<BitvectorExpr> ilasynth::BitvectorChoice

BoolChoice

typedef ChoiceExpr<BoolExpr> ilasynth::BoolChoice

dtree_ptr_t

typedef boost::shared_ptr<DITreeNode> ilasynth::dtree_ptr_t

hcptr_t

typedef HornClause* ilasynth::hcptr_t

hlptr_t

typedef HornLiteral* ilasynth::hlptr_t

hvptr_t

typedef HornVar* ilasynth::hvptr_t

mem_write_entry_list_stack_t

typedef std::list<mem_write_entry_list_t> ilasynth::mem_write_entry_list_stack_t

mem_write_entry_list_t

typedef std::list<mem_write_entry_t> ilasynth::mem_write_entry_list_t

mem_write_list_t

typedef std::list<mem_write_t> ilasynth::mem_write_list_t

MemChoice

typedef ChoiceExpr<MemExpr> ilasynth::MemChoice

mp_int_t

typedef boost::multiprecision::cpp_int ilasynth::mp_int_t

nmap_t

typedef std::map<std::string, npair_t> ilasynth::nmap_t

nodeset_t

typedef std::set<const Node*> ilasynth::nodeset_t

nodevec_t

typedef std::vector<const Node*> ilasynth::nodevec_t

nptr_t

typedef boost::shared_ptr<Node> ilasynth::nptr_t

nptr_vec_t

typedef std::vector<nptr_t> ilasynth::nptr_vec_t

rwmap_t

typedef std::unordered_map<const Node*, nptr_t, decltype(&nodeHash), decltype(&nodeEqual)> ilasynth::rwmap_t

simout_ptr_t

typedef boost::shared_ptr<SimOutput> ilasynth::simout_ptr_t

vlg_addr_t

typedef std::string ilasynth::vlg_addr_t

vlg_data_t

typedef std::string ilasynth::vlg_data_t

vlg_ite_stmt_t

typedef std::tuple<vlg_stmt_t, vlg_stmt_t, vlg_stmt_t> ilasynth::vlg_ite_stmt_t

vlg_ite_stmts_t

typedef std::vector<vlg_ite_stmt_t> ilasynth::vlg_ite_stmts_t

vlg_mem_t

typedef std::tuple<vlg_name_t, int, int> ilasynth::vlg_mem_t

vlg_mems_t

typedef std::vector<vlg_mem_t> ilasynth::vlg_mems_t

vlg_name_t

typedef std::string ilasynth::vlg_name_t

vlg_per_mem_access_t

typedef std::pair<vlg_name_t, vlg_sigs_t> ilasynth::vlg_per_mem_access_t

vlg_sig_t

typedef std::pair<vlg_name_t, int> ilasynth::vlg_sig_t

vlg_sigs_t

typedef std::vector<vlg_sig_t> ilasynth::vlg_sigs_t

vlg_stmt_t

typedef std::string ilasynth::vlg_stmt_t

vlg_stmts_t

typedef std::vector<vlg_name_t> ilasynth::vlg_stmts_t

Enumeration Type Documentation

endianness_t

enum ilasynth::endianness_t

Enumerator
UNKNOWN_E
LITTLE_E
BIG_E

Function Documentation

bmc()

bool ilasynth::bmc	(	unsigned	n1,
		Abstraction *	a1,
		NodeRef *	r1,
		unsigned	n2,
		Abstraction *	a2,
		NodeRef *	r2
	)

checkMiter()

bool ilasynth::checkMiter	(	z3::solver &	S,
		z3::expr &	e1,
		z3::expr &	e2
	)

choice_hash_combine()

template<typename T >

void ilasynth::choice_hash_combine	(	std::size_t &	seed,
		const ChoiceExpr< T > *	c
	)

clearLogs()

void ilasynth::clearLogs

(

)

compute_hash_value()

std::size_t ilasynth::compute_hash_value

(

const NodeType &

ntype

)

DetermineUnrollBound()

unsigned ilasynth::DetermineUnrollBound	(	Abstraction *	pAbs,
		const std::string &	nodeName
	)

disableLog()

void ilasynth::disableLog

(

const std::string &

name

)

dump_trace()

void ilasynth::dump_trace

(

)

enableLog()

void ilasynth::enableLog

(

const std::string &

name

)

hash_value() [1/2]

std::size_t ilasynth::hash_value

(

const Node &

n

)

hash_value() [2/2]

std::size_t ilasynth::hash_value

(

const NodeType &

ntype

)

ila_assert() [1/2]

void ilasynth::ila_assert	(	bool	b,
		const char *	msg,
		const char *	file,
		int	line
	)

ila_assert() [2/2]

void ilasynth::ila_assert	(	bool	b,
		const std::string &	msg,
		const char *	file,
		int	line
	)

info()

std::ostream& ilasynth::info

(

const char *

s

)

initLogging()

void ilasynth::initLogging

(

)

is_py_int()

bool ilasynth::is_py_int

(

const py::object &

l

)

is_py_int_or_long()

bool ilasynth::is_py_int_or_long

(

const py::object &

l

)

log1()

std::ostream& ilasynth::log1

(

const char *

s

)

log2()

std::ostream& ilasynth::log2

(

const char *

s

)

NEQArchVarUpdateMismatch()

bool ilasynth::NEQArchVarUpdateMismatch	(	const std::string &	a1name,
		const std::string &	a2name,
		const std::string &	VarName
	)

NEQVarNotExist()

bool ilasynth::NEQVarNotExist	(	const std::string &	a1name,
		const std::string &	a2name,
		const std::string &	notExistVarName
	)

NEQVarTypeMismatch()

bool ilasynth::NEQVarTypeMismatch	(	const std::string &	a1name,
		const std::string &	a2name,
		const std::string &	VarName
	)

nodeEqual()

bool ilasynth::nodeEqual	(	const Node *	left,
		const Node *	right
	)

nodeHash()

size_t ilasynth::nodeHash

(

const Node *

n

)

operator<<() [1/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const mem_write_entry_t &	mwe
	)

operator<<() [2/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const mem_write_entry_list_t &	mwel
	)

operator<<() [3/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const mem_write_entry_list_stack_t &	mwel
	)

operator<<() [4/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const mem_write_t &	mw
	)

operator<<() [5/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const mem_write_list_t &	mwl
	)

operator<<() [6/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		NodeType const &	ntype
	)

operator<<() [7/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const DistInput &	di
	)

operator<<() [8/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const MemValues &	mv
	)

operator<<() [9/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const SimOutput &	simout
	)

operator<<() [10/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const Node &	that
	)

operator<<() [11/11]

std::ostream& ilasynth::operator<<	(	std::ostream &	out,
		const NodeRef &	node
	)

set_logging_level()

void ilasynth::set_logging_level

(

int

level

)

setLogLevel()

void ilasynth::setLogLevel	(	int	l,
		const std::string &	name
	)

to_cpp_int()

mp_int_t ilasynth::to_cpp_int

(

const py::object &

l

)

to_pyint() [1/2]

py::object ilasynth::to_pyint

(

const mp_int_t &

i

)

to_pyint() [2/2]

py::object ilasynth::to_pyint

(

const std::string &

s

)

to_string() [1/2]

std::string ilasynth::to_string

(

const py::object &

l

)

to_string() [2/2]

std::string ilasynth::to_string

(

const mp_int_t &

i

)

translateILAException()

void ilasynth::translateILAException

(

PyILAException const &

ex

)

Variable Documentation

NUM_HASHTABLE_BUCKETS

const int ilasynth::NUM_HASHTABLE_BUCKETS = 1023

NUM_HASHTABLE_BUCKETS_SMALL

const int ilasynth::NUM_HASHTABLE_BUCKETS_SMALL = 63