ilang++.h File Reference

#include <cstdint>
#include <map>
#include <memory>
#include <string>
#include <vector>
#include <z3++.h>
#include <ilang/config.h>

Go to the source code of this file.

Classes
class	ilang::SortRef
	The wrapper of Sort (type for different AST nodes). More...
class	ilang::ExprRef
	The wrapper of Expr (e.g. state var, var relation, constant, etc). More...
class	ilang::FuncRef
	The wrapper of Func (uninterpreted function). More...
class	ilang::InstrRef
	The wrapper of Instr (instruction). More...
class	ilang::Ila
	The wrapper of InstrLvlAbs (ILA). More...
class	ilang::IlaZ3Unroller
	The wrapper of generating z3::expr for verification. More...

Namespaces
	ilang

Typedefs
typedef uint64_t	ilang::NumericType
	Data type for numerics. NOTE: SHOULD BE SYNCED WITH BvValType!!

Functions
void	ilang::LogLevel (const int &lvl)
	Set the minimun log level. Log messages at or above this level will be logged. (Default: 0) More...
void	ilang::LogPath (const std::string &path)
	Set the path for log file. If specified, logfiles are written into this directory instead of the default logging directory (/tmp).
void	ilang::LogToErr (bool to_err)
	Pipe log to stderr. Log messages to stderr instead of logfiles, if set to 1.
void	ilang::EnableDebug (const std::string &tag)
	Add a debug tag.
void	ilang::DisableDebug (const std::string &tag)
	Remove a debug tag.
ExprRef	ilang::operator- (const ExprRef &a)
	Arithmetic negate for bit-vectors.
ExprRef	ilang::operator! (const ExprRef &a)
	Logical not for Booleans.
ExprRef	ilang::operator~ (const ExprRef &a)
	Bit-wise complement for bit-vectors.
ExprRef	ilang::operator& (const ExprRef &a, const ExprRef &b)
	Logical AND (bit-wise for bit-vectors).
ExprRef	ilang::operator| (const ExprRef &a, const ExprRef &b)
	Logical OR (bit-wise for bit-vectors).
ExprRef	ilang::operator^ (const ExprRef &a, const ExprRef &b)
	Logical XOR (bit-wise for bit-vectors).
ExprRef	ilang::operator<< (const ExprRef &a, const ExprRef &b)
	Left shift for bit-vectors.
ExprRef	ilang::operator>> (const ExprRef &a, const ExprRef &b)
	Arithmetic right shift for bit-vectors.
ExprRef	ilang::Lshr (const ExprRef &a, const ExprRef &b)
	Logical right shift for bit-vectors.
ExprRef	ilang::operator+ (const ExprRef &a, const ExprRef &b)
	Unsigned addition for bit-vectors.
ExprRef	ilang::operator- (const ExprRef &a, const ExprRef &b)
	Unsigned subtraction for bit-vectors.
ExprRef	ilang::operator* (const ExprRef &a, const ExprRef &b)
	Unsigned multiply for bit-vectors.
ExprRef	ilang::operator/ (const ExprRef &a, const ExprRef &b)
	Unsigned division for bit-vectors.
ExprRef	ilang::operator& (const ExprRef &a, const bool &b)
	Logical AND with Boolean constant.
ExprRef	ilang::operator| (const ExprRef &a, const bool &b)
	Logical OR with Boolean constant.
ExprRef	ilang::operator^ (const ExprRef &a, const bool &b)
	Logical XOR with Boolean constant.
ExprRef	ilang::operator<< (const ExprRef &a, const int &b)
	Left shift with int constant.
ExprRef	ilang::operator>> (const ExprRef &a, const int &b)
	Arithmetic right shift with int constant.
ExprRef	ilang::Lshr (const ExprRef &a, const int &b)
	Logical right shift with int constant.
ExprRef	ilang::operator+ (const ExprRef &a, const NumericType &b)
	Unsigned addition with constant.
ExprRef	ilang::operator- (const ExprRef &a, const NumericType &b)
	Unsigned subtraction with constant.
ExprRef	ilang::operator* (const ExprRef &a, const NumericType &b)
	Unsigned multiply with constant.
ExprRef	ilang::SRem (const ExprRef &a, const ExprRef &b)
	Arithmetic signed remainder.
ExprRef	ilang::URem (const ExprRef &a, const ExprRef &b)
	Arithmetic unsigned remainder.
ExprRef	ilang::SMod (const ExprRef &a, const ExprRef &b)
	Arithmetic signed modular.
void	ilang::SetUnsignedComparison (bool sign)
ExprRef	ilang::operator== (const ExprRef &a, const ExprRef &b)
	Equal.
ExprRef	ilang::operator!= (const ExprRef &a, const ExprRef &b)
	Not equal.
ExprRef	ilang::operator< (const ExprRef &a, const ExprRef &b)
	Signed/Unsigned less than (bit-vectors only).
ExprRef	ilang::operator> (const ExprRef &a, const ExprRef &b)
	Signed/Unsigned greater than (bit-vectors only).
ExprRef	ilang::operator<= (const ExprRef &a, const ExprRef &b)
	Signed/Unsigned less than or equal to (bit-vectors only).
ExprRef	ilang::operator>= (const ExprRef &a, const ExprRef &b)
	Signed/Unsigned greater than or equal to (bit-vectors only).
ExprRef	ilang::Ult (const ExprRef &a, const ExprRef &b)
	Unsigned less than (bit-vectors only).
ExprRef	ilang::Ugt (const ExprRef &a, const ExprRef &b)
	Unsigned greater than (bit-vectors only).
ExprRef	ilang::Ule (const ExprRef &a, const ExprRef &b)
	Unsigned less than or equal to (bit-vectors only).
ExprRef	ilang::Uge (const ExprRef &a, const ExprRef &b)
	Unsigned greater than or equal to (bit-vectors only).
ExprRef	ilang::Slt (const ExprRef &a, const ExprRef &b)
	Signed less than (bit-vectors only).
ExprRef	ilang::Sgt (const ExprRef &a, const ExprRef &b)
	Signed greater than (bit-vectors only).
ExprRef	ilang::Sle (const ExprRef &a, const ExprRef &b)
	Signed less than or equal to (bit-vectors only).
ExprRef	ilang::Sge (const ExprRef &a, const ExprRef &b)
	Signed greater than or equal to (bit-vectors only).
ExprRef	ilang::operator== (const ExprRef &a, const NumericType &b)
	Equal to constant.
ExprRef	ilang::operator!= (const ExprRef &a, const NumericType &b)
	Not equal to constant.
ExprRef	ilang::operator< (const ExprRef &a, const NumericType &b)
	Signed/Unsigned less than constant (bit-vectors only).
ExprRef	ilang::operator> (const ExprRef &a, const NumericType &b)
	Signed/Unsigned greater than constant (bit-vectors only).
ExprRef	ilang::operator<= (const ExprRef &a, const NumericType &b)
	Signed/Unsigned less than or equal to constant (bit-vectors only).
ExprRef	ilang::operator>= (const ExprRef &a, const NumericType &b)
	Signed/Unsigned greater than or equal to constant (bit-vectors only).
ExprRef	ilang::Ult (const ExprRef &a, const NumericType &b)
	Unsigned less than constant (bit-vectors only).
ExprRef	ilang::Ugt (const ExprRef &a, const NumericType &b)
	Unsigned greater than constant (bit-vectors only).
ExprRef	ilang::Ule (const ExprRef &a, const NumericType &b)
	Unsigned less than or equal to constant (bit-vectors only).
ExprRef	ilang::Uge (const ExprRef &a, const NumericType &b)
	Unsigned greater than or equal to constant (bit-vectors only).
ExprRef	ilang::Slt (const ExprRef &a, const NumericType &b)
	Signed less than constant (bit-vectors only).
ExprRef	ilang::Sgt (const ExprRef &a, const NumericType &b)
	Signed greater than constant (bit-vectors only).
ExprRef	ilang::Sle (const ExprRef &a, const NumericType &b)
	Signed less than or equal to constant (bit-vectors only).
ExprRef	ilang::Sge (const ExprRef &a, const NumericType &b)
	Signed greater than or equal to constant (bit-vectors only).
ExprRef	ilang::Load (const ExprRef &mem, const ExprRef &addr)
	Load from memory.
ExprRef	ilang::Store (const ExprRef &mem, const ExprRef &addr, const ExprRef &data)
	Store to memory.
ExprRef	ilang::Load (const ExprRef &mem, const NumericType &addr)
	Load from memory with constant address.
ExprRef	ilang::Store (const ExprRef &mem, const NumericType &addr, const NumericType &data)
	Store to memory at constant address and data.
ExprRef	ilang::Concat (const ExprRef &msbv, const ExprRef &lsbv)
	Concatenate two bit-vectors. More...
ExprRef	ilang::Extract (const ExprRef &bv, const int &hi, const int &lo)
	Extract bit-field in the bit-vector. More...
ExprRef	ilang::SelectBit (const ExprRef &bv, const int &idx)
	Extract single bit in the bit-vector. More...
ExprRef	ilang::ZExt (const ExprRef &bv, const int &length)
	Zero-extend the bit-vector to the specified length. More...
ExprRef	ilang::SExt (const ExprRef &bv, const int &length)
	Sign-extend the bit-vector to the specified length. More...
ExprRef	ilang::LRotate (const ExprRef &bv, const int &immediate)
	Left-rotate the bit-vector with immediate number of times. More...
ExprRef	ilang::RRotate (const ExprRef &bv, const int &immediate)
	Right-rotate the bit-vector with immediate number of times. More...
ExprRef	ilang::Imply (const ExprRef &ante, const ExprRef &cons)
	Logical imply for Booleans. More...
ExprRef	ilang::Ite (const ExprRef &cond, const ExprRef &t, const ExprRef &f)
	If-then-else on the Boolean condition. More...
ExprRef	ilang::BoolConst (bool bool_val)
	Return a Boolean constant. More...
ExprRef	ilang::BvConst (const NumericType &bv_val, const int &bit_width)
	Return a bit-vector constant. More...
ExprRef	ilang::MemConst (const NumericType &def_val, const std::map< NumericType, NumericType > &vals, const int &addr_width, const int &data_width)
	Return a memory constant. More...
bool	ilang::TopEqual (const ExprRef &a, const ExprRef &b)
	Topologically equivalent.
std::ostream &	ilang::operator<< (std::ostream &out, const ExprRef &expr)
	Print out the ExprRef.
std::ostream &	ilang::operator<< (std::ostream &out, const InstrRef &instr)
	Print out the Instruction.
std::ostream &	ilang::operator<< (std::ostream &out, const Ila &ila)
	Print out the ILA.
bool	ilang::ExportIlaPortable (const Ila &ila, const std::string &file_name)
	Export the ILA portable to file. More...
Ila	ilang::ImportIlaPortable (const std::string &file_name)
	Import the ILA portable from file. More...
void	ilang::ExportSysCSim (const Ila &ila, const std::string &dir_path, bool optimize=false)
	Generate the SystemC simulator. More...

Detailed Description

The header for the c++ API.