ilasynth  1.0
ILASynth: Template-based ILA Synthesis Engine
Classes | Typedefs | Enumerations | Functions | Variables
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< Abstractionabstraction_ptr_t
 
typedef ChoiceExpr< BitvectorExprBitvectorChoice
 
typedef ChoiceExpr< BoolExprBoolChoice
 
typedef ChoiceExpr< MemExprMemChoice
 
typedef boost::shared_ptr< Nodenptr_t
 
typedef std::vector< nptr_tnptr_vec_t
 
typedef std::vector< const Node * > nodevec_t
 
typedef std::set< const Node * > nodeset_t
 
typedef std::map< std::string, npair_tnmap_t
 
typedef std::unordered_map< const Node *, nptr_t, decltype(&nodeHash), decltype(&nodeEqual)> rwmap_t
 
typedef boost::multiprecision::cpp_int mp_int_t
 
typedef HornVarhvptr_t
 
typedef HornLiteralhlptr_t
 
typedef HornClausehcptr_t
 
typedef boost::shared_ptr< SimOutputsimout_ptr_t
 
typedef boost::shared_ptr< DITreeNodedtree_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_tvlg_stmts_t
 
typedef std::pair< vlg_name_t, int > vlg_sig_t
 
typedef std::vector< vlg_sig_tvlg_sigs_t
 
typedef std::tuple< vlg_stmt_t, vlg_stmt_t, vlg_stmt_tvlg_ite_stmt_t
 
typedef std::vector< vlg_ite_stmt_tvlg_ite_stmts_t
 
typedef std::pair< vlg_name_t, vlg_sigs_tvlg_per_mem_access_t
 
typedef std::tuple< vlg_name_t, int, int > vlg_mem_t
 
typedef std::vector< vlg_mem_tvlg_mems_t
 
typedef std::list< mem_write_entry_tmem_write_entry_list_t
 
typedef std::list< mem_write_entry_list_tmem_write_entry_list_stack_t
 
typedef std::list< mem_write_tmem_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

◆ BoolChoice

◆ dtree_ptr_t

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

◆ hcptr_t

◆ hlptr_t

◆ hvptr_t

◆ mem_write_entry_list_stack_t

◆ mem_write_entry_list_t

◆ mem_write_list_t

◆ 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

◆ 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

◆ 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

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