ilasynth::Abstraction Class Reference

#include <abstraction.hpp>

Classes
struct	assump_collector_t
struct	uabstraction_t

Public Types
enum	state_t {   INP, REG, BIT, MEM,   FUN }
typedef std::map< std::string, uabstraction_t >	uabs_map_t

Public Member Functions
	Abstraction (const std::string &name)
	Abstraction (Abstraction *parent, const std::string &name)
	~Abstraction ()
const std::string &	getName () const
NodeRef *	addInp (const std::string &name, int width)
NodeRef *	addBit (const std::string &name)
NodeRef *	addReg (const std::string &name, int width)
NodeRef *	addMem (const std::string &name, int addrW, int dataW)
NodeRef *	addFun (const std::string &name, int retW, const py::list &l)
NodeRef *	getInp (const std::string &name)
NodeRef *	getBit (const std::string &name)
NodeRef *	getReg (const std::string &name)
NodeRef *	getMem (const std::string &name)
NodeRef *	getFun (const std::string &name)
NodeRef *	getStage (const std::string &name)
void	addVar (nptr_t &nref)
void	setInit (const std::string &name, NodeRef *n)
NodeRef *	getInit (const std::string &name) const
void	setIpred (const std::string &name, NodeRef *n)
NodeRef *	getIpred (const std::string &name) const
void	setNext (const std::string &name, NodeRef *n)
NodeRef *	getNext (const std::string &name) const
NodeRef *	getNextI (const std::string &name, int i) const
AbstractionWrapper *	addUAbs (const std::string &name, NodeRef *valid)
AbstractionWrapper *	getUAbs (const std::string &name)
void	connectUInst (const std::string &name, const abstraction_ptr_t &uabs)
NodeRef *	getFetchExpr () const
void	setFetchExpr (NodeRef *expr)
NodeRef *	getFetchValid () const
nptr_t	getFetchValidNode () const
void	setFetchValid (NodeRef *expr)
void	setDecodeExpressions (const py::list &l)
py::list	getDecodeExpressions () const
const nptr_vec_t &	getDecodeNodes () const
void	addAssumption (NodeRef *expr)
py::list	getAllAssumptions () const
void	synthesizeAll (PyObject *fun)
void	synthesizeReg (const std::string &name, PyObject *fun)
NodeRef *	synthesizeElement (const std::string &name, NodeRef *expr, PyObject *fun)
void	exportOneToFile (NodeRef *node, const std::string &fileName) const
void	exportListToFile (const py::list &l, const std::string &fileName) const
void	exportAllToFile (const std::string &fileName) const
void	exportAllToStream (std::ofstream &out) const
void	generateVerilogToFile (const std::string &fileName) const
void	generateVerilogToFile (const std::string &fileName, const std::string &topModName) const
NodeRef *	importOneFromFile (const std::string &fileName)
py::list	importListFromFile (const std::string &fileName)
void	importAllFromFile (const std::string &fileName)
void	importAllFromStream (std::ifstream &in, bool Clear)
void	generateSimToFile (const std::string &fileName) const
void	generateSimToDir (const std::string &dirName) const
void	generateCbmcCtoFile (const std::string &fileName) const
void	generateCbmcCtoDir (const std::string &dirName) const
bool	areEqual (NodeRef *left, NodeRef *right) const
bool	areEqualAssump (NodeRef *assump, NodeRef *left, NodeRef *right)
bool	areEqualUnrolled (unsigned n, NodeRef *reg, NodeRef *exp)
void	toBoogie (const std::string &filename)
void	hornifyAll (const std::string &fileName)
void	hornifyNode (NodeRef *node, const std::string &ruleName)
void	generateHornMapping (const std::string &type)
void	exportHornToFile (const std::string &fileName)
void	hornifyIteAsNode (bool iteAsNode)
void	hornifyBvAsInt (bool bvAsInt)
void	addHornInstr (const std::string &i, NodeRef *d)
void	addHornNext (const std::string &i, const std::string &s, NodeRef *n)
void	addHornChild (const std::string &c, const std::string &i, NodeRef *d)
const nmap_t &	getMems () const
const nmap_t &	getInps () const
const nmap_t &	getRegs () const
const nmap_t &	getBits () const
const nmap_t &	getFuns () const
void	forEachAssump (assump_visitor_i &i) const
void	getAllAssumptions (nptr_vec_t &assump_vec) const
nptr_t	getFetchExprRef () const
nptr_t	getFetchValidRef () const
nptr_vec_t	getDecodeExprs () const
const npair_t *	getMapEntry (const std::string &name) const
bool	isInput (const std::string &name) const

Static Public Member Functions
static int	getObjId ()
static NodeRef *	bvConstLong (py::long_ l, int width)
static NodeRef *	bvConstInt (unsigned int l, int width)
static NodeRef *	boolConstB (bool b)
static NodeRef *	boolConstI (int b)
static NodeRef *	boolConstL (py::long_ b)
static NodeRef *	memConst (const MemValues &mv)
static bool	bmc (unsigned n, Abstraction *a, NodeRef *r, bool init, NodeRef *initAssump)
static bool	bmc (unsigned n1, Abstraction *a1, NodeRef *r1, unsigned n2, Abstraction *a2, NodeRef *r2)
static bool	EQcheckSimple (Abstraction *a1, Abstraction *a2)

Public Attributes
int	paramSyn
int	reduceWhenImport
VlgExportConfig	vlgExpConfig

Protected Member Functions
void	initMap (nmap_t &from_m, nmap_t &to_m)
void	extractModelValues (Z3ExprAdapter &c, z3::model &m, py::dict &result)
NodeRef *	getVar (const nmap_t &m, const std::string &name)
void	addVar (state_t st, nmap_t &m, nptr_t &n)
nptr_t	_synthesize (const std::string &name, const nptr_vec_t &assumps, const nptr_t &expr, PyObject *pyfun)
bool	checkAndInsertName (state_t st, const std::string &name)
bool	doesNextExist (const nmap_t &m) const
nmap_t *	getMap (const std::string &name, NodeRef *n)
nmap_t *	getMap (const std::string &name)
nmap_t::const_iterator	findInMap (const std::string &name) const
nmap_t::iterator	findInMap (const std::string &name)
nmap_t::const_iterator	findInMapNoExcept (const std::string &name) const
nmap_t::iterator	findInMapNoExcept (const std::string &name)
nmap_t::const_iterator	MapEnd () const
nmap_t::iterator	MapEnd ()

Protected Attributes
Abstraction *	parent
const std::string	name
std::map< std::string, state_t >	names
nmap_t	inps
nmap_t	regs
nmap_t	bits
nmap_t	mems
nmap_t	funs
nptr_t	fetchExpr
nptr_t	fetchValid
nptr_vec_t	decodeExprs
nptr_vec_t	assumps
uabs_map_t	uabs

Private Member Functions
CppSimGen *	generateSim (bool hier) const
CVerifGen *	generateCBMCC (bool hier) const
void	addVarToSimulator (CppSimGen *gen) const
void	setUpdateToFunction (CppSimGen *gen, CppFun *fun, nptr_t valid, bool doHier=false) const

Private Attributes
int	MAX_SYN_ITER
FuncReduction	funcReducer
HornTranslator *	_ht

Static Private Attributes
static int	objCnt

Friends
class	Synthesizer
class	BoogieTranslator
class	MicroUnroller
class	AbstractionWrapper
unsigned	DetermineUnrollBound (Abstraction *pAbs, const std::string &nodeName)

Member Typedef Documentation

uabs_map_t

typedef std::map<std::string, uabstraction_t> ilasynth::Abstraction::uabs_map_t

Member Enumeration Documentation

state_t

enum ilasynth::Abstraction::state_t

Enumerator
INP
REG
BIT
MEM
FUN

Constructor & Destructor Documentation

Abstraction() [1/2]

ilasynth::Abstraction::Abstraction

(

const std::string &

name

)

Abstraction() [2/2]

ilasynth::Abstraction::Abstraction	(	Abstraction *	parent,
		const std::string &	name
	)

~Abstraction()

ilasynth::Abstraction::~Abstraction

(

)

Member Function Documentation

_synthesize()

nptr_t ilasynth::Abstraction::_synthesize ( const std::string &  name, const nptr_vec_t &  assumps, const nptr_t &  expr, PyObject *  pyfun  )

protected

addAssumption()

void ilasynth::Abstraction::addAssumption

(

NodeRef *

expr

)

addBit()

NodeRef* ilasynth::Abstraction::addBit

(

const std::string &

name

)

addFun()

NodeRef* ilasynth::Abstraction::addFun	(	const std::string &	name,
		int	retW,
		const py::list &	l
	)

addHornChild()

void ilasynth::Abstraction::addHornChild	(	const std::string &	c,
		const std::string &	i,
		NodeRef *	d
	)

addHornInstr()

void ilasynth::Abstraction::addHornInstr	(	const std::string &	i,
		NodeRef *	d
	)

addHornNext()

void ilasynth::Abstraction::addHornNext	(	const std::string &	i,
		const std::string &	s,
		NodeRef *	n
	)

addInp()

NodeRef* ilasynth::Abstraction::addInp	(	const std::string &	name,
		int	width
	)

addMem()

NodeRef* ilasynth::Abstraction::addMem	(	const std::string &	name,
		int	addrW,
		int	dataW
	)

addReg()

NodeRef* ilasynth::Abstraction::addReg	(	const std::string &	name,
		int	width
	)

addUAbs()

AbstractionWrapper* ilasynth::Abstraction::addUAbs	(	const std::string &	name,
		NodeRef *	valid
	)

addVar() [1/2]

void ilasynth::Abstraction::addVar ( state_t  st, nmap_t &  m, nptr_t &  n  )

protected

addVar() [2/2]

void ilasynth::Abstraction::addVar

(

nptr_t &

nref

)

addVarToSimulator()

void ilasynth::Abstraction::addVarToSimulator ( CppSimGen *  gen ) const

private

areEqual()

bool ilasynth::Abstraction::areEqual	(	NodeRef *	left,
		NodeRef *	right
	)		const

areEqualAssump()

bool ilasynth::Abstraction::areEqualAssump	(	NodeRef *	assump,
		NodeRef *	left,
		NodeRef *	right
	)

areEqualUnrolled()

bool ilasynth::Abstraction::areEqualUnrolled	(	unsigned	n,
		NodeRef *	reg,
		NodeRef *	exp
	)

bmc() [1/2]

static bool ilasynth::Abstraction::bmc ( unsigned  n, Abstraction *  a, NodeRef *  r, bool  init, NodeRef *  initAssump  )

static

bmc() [2/2]

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

static

boolConstB()

static NodeRef* ilasynth::Abstraction::boolConstB ( bool  b )

static

boolConstI()

static NodeRef* ilasynth::Abstraction::boolConstI ( int  b )

static

boolConstL()

static NodeRef* ilasynth::Abstraction::boolConstL ( py::long_  b )

static

bvConstInt()

static NodeRef* ilasynth::Abstraction::bvConstInt ( unsigned int  l, int  width  )

static

bvConstLong()

static NodeRef* ilasynth::Abstraction::bvConstLong ( py::long_  l, int  width  )

static

checkAndInsertName()

bool ilasynth::Abstraction::checkAndInsertName ( state_t  st, const std::string &  name  )

protected

connectUInst()

void ilasynth::Abstraction::connectUInst	(	const std::string &	name,
		const abstraction_ptr_t &	uabs
	)

doesNextExist()

bool ilasynth::Abstraction::doesNextExist ( const nmap_t &  m ) const

protected

EQcheckSimple()

static bool ilasynth::Abstraction::EQcheckSimple ( Abstraction *  a1, Abstraction *  a2  )

static

exportAllToFile()

void ilasynth::Abstraction::exportAllToFile

(

const std::string &

fileName

)

const

exportAllToStream()

void ilasynth::Abstraction::exportAllToStream

(

std::ofstream &

out

)

const

exportHornToFile()

void ilasynth::Abstraction::exportHornToFile

(

const std::string &

fileName

)

exportListToFile()

void ilasynth::Abstraction::exportListToFile	(	const py::list &	l,
		const std::string &	fileName
	)		const

exportOneToFile()

void ilasynth::Abstraction::exportOneToFile	(	NodeRef *	node,
		const std::string &	fileName
	)		const

extractModelValues()

void ilasynth::Abstraction::extractModelValues ( Z3ExprAdapter &  c, z3::model &  m, py::dict &  result  )

protected

findInMap() [1/2]

nmap_t::const_iterator ilasynth::Abstraction::findInMap ( const std::string &  name ) const

protected

findInMap() [2/2]

nmap_t::iterator ilasynth::Abstraction::findInMap ( const std::string &  name )

protected

findInMapNoExcept() [1/2]

nmap_t::const_iterator ilasynth::Abstraction::findInMapNoExcept ( const std::string &  name ) const

protected

findInMapNoExcept() [2/2]

nmap_t::iterator ilasynth::Abstraction::findInMapNoExcept ( const std::string &  name )

protected

forEachAssump()

void ilasynth::Abstraction::forEachAssump

(

assump_visitor_i &

i

)

const

generateCBMCC()

CVerifGen* ilasynth::Abstraction::generateCBMCC ( bool  hier ) const

private

generateCbmcCtoDir()

void ilasynth::Abstraction::generateCbmcCtoDir

(

const std::string &

dirName

)

const

generateCbmcCtoFile()

void ilasynth::Abstraction::generateCbmcCtoFile

(

const std::string &

fileName

)

const

generateHornMapping()

void ilasynth::Abstraction::generateHornMapping

(

const std::string &

type

)

generateSim()

CppSimGen* ilasynth::Abstraction::generateSim ( bool  hier ) const

private

generateSimToDir()

void ilasynth::Abstraction::generateSimToDir

(

const std::string &

dirName

)

const

generateSimToFile()

void ilasynth::Abstraction::generateSimToFile

(

const std::string &

fileName

)

const

generateVerilogToFile() [1/2]

void ilasynth::Abstraction::generateVerilogToFile

(

const std::string &

fileName

)

const

generateVerilogToFile() [2/2]

void ilasynth::Abstraction::generateVerilogToFile	(	const std::string &	fileName,
		const std::string &	topModName
	)		const

getAllAssumptions() [1/2]

py::list ilasynth::Abstraction::getAllAssumptions

(

)

const

getAllAssumptions() [2/2]

void ilasynth::Abstraction::getAllAssumptions

(

nptr_vec_t &

assump_vec

)

const

getBit()

NodeRef* ilasynth::Abstraction::getBit

(

const std::string &

name

)

getBits()

const nmap_t& ilasynth::Abstraction::getBits ( ) const

inline

getDecodeExpressions()

py::list ilasynth::Abstraction::getDecodeExpressions

(

)

const

getDecodeExprs()

nptr_vec_t ilasynth::Abstraction::getDecodeExprs ( ) const

inline

getDecodeNodes()

const nptr_vec_t& ilasynth::Abstraction::getDecodeNodes

(

)

const

getFetchExpr()

NodeRef* ilasynth::Abstraction::getFetchExpr

(

)

const

getFetchExprRef()

nptr_t ilasynth::Abstraction::getFetchExprRef ( ) const

inline

getFetchValid()

NodeRef* ilasynth::Abstraction::getFetchValid

(

)

const

getFetchValidNode()

nptr_t ilasynth::Abstraction::getFetchValidNode

(

)

const

getFetchValidRef()

nptr_t ilasynth::Abstraction::getFetchValidRef ( ) const

inline

getFun()

NodeRef* ilasynth::Abstraction::getFun

(

const std::string &

name

)

getFuns()

const nmap_t& ilasynth::Abstraction::getFuns ( ) const

inline

getInit()

NodeRef* ilasynth::Abstraction::getInit

(

const std::string &

name

)

const

getInp()

NodeRef* ilasynth::Abstraction::getInp

(

const std::string &

name

)

getInps()

const nmap_t& ilasynth::Abstraction::getInps ( ) const

inline

getIpred()

NodeRef* ilasynth::Abstraction::getIpred

(

const std::string &

name

)

const

getMap() [1/2]

nmap_t* ilasynth::Abstraction::getMap ( const std::string &  name, NodeRef *  n  )

protected

getMap() [2/2]

nmap_t* ilasynth::Abstraction::getMap ( const std::string &  name )

protected

getMapEntry()

const npair_t* ilasynth::Abstraction::getMapEntry

(

const std::string &

name

)

const

getMem()

NodeRef* ilasynth::Abstraction::getMem

(

const std::string &

name

)

getMems()

const nmap_t& ilasynth::Abstraction::getMems ( ) const

inline

getName()

const std::string& ilasynth::Abstraction::getName ( ) const

inline

getNext()

NodeRef* ilasynth::Abstraction::getNext

(

const std::string &

name

)

const

getNextI()

NodeRef* ilasynth::Abstraction::getNextI	(	const std::string &	name,
		int	i
	)		const

getObjId()

static int ilasynth::Abstraction::getObjId ( )

static

getReg()

NodeRef* ilasynth::Abstraction::getReg

(

const std::string &

name

)

getRegs()

const nmap_t& ilasynth::Abstraction::getRegs ( ) const

inline

getStage()

NodeRef* ilasynth::Abstraction::getStage

(

const std::string &

name

)

getUAbs()

AbstractionWrapper* ilasynth::Abstraction::getUAbs

(

const std::string &

name

)

getVar()

NodeRef* ilasynth::Abstraction::getVar ( const nmap_t &  m, const std::string &  name  )

protected

hornifyAll()

void ilasynth::Abstraction::hornifyAll

(

const std::string &

fileName

)

hornifyBvAsInt()

void ilasynth::Abstraction::hornifyBvAsInt

(

bool

bvAsInt

)

hornifyIteAsNode()

void ilasynth::Abstraction::hornifyIteAsNode

(

bool

iteAsNode

)

hornifyNode()

void ilasynth::Abstraction::hornifyNode	(	NodeRef *	node,
		const std::string &	ruleName
	)

importAllFromFile()

void ilasynth::Abstraction::importAllFromFile

(

const std::string &

fileName

)

importAllFromStream()

void ilasynth::Abstraction::importAllFromStream	(	std::ifstream &	in,
		bool	Clear
	)

importListFromFile()

py::list ilasynth::Abstraction::importListFromFile

(

const std::string &

fileName

)

importOneFromFile()

NodeRef* ilasynth::Abstraction::importOneFromFile

(

const std::string &

fileName

)

initMap()

void ilasynth::Abstraction::initMap ( nmap_t &  from_m, nmap_t &  to_m  )

protected

isInput()

bool ilasynth::Abstraction::isInput ( const std::string &  name ) const

inline

MapEnd() [1/2]

nmap_t::const_iterator ilasynth::Abstraction::MapEnd ( ) const

protected

MapEnd() [2/2]

nmap_t::iterator ilasynth::Abstraction::MapEnd ( )

protected

memConst()

static NodeRef* ilasynth::Abstraction::memConst ( const MemValues &  mv )

static

setDecodeExpressions()

void ilasynth::Abstraction::setDecodeExpressions

(

const py::list &

l

)

setFetchExpr()

void ilasynth::Abstraction::setFetchExpr

(

NodeRef *

expr

)

setFetchValid()

void ilasynth::Abstraction::setFetchValid

(

NodeRef *

expr

)

setInit()

void ilasynth::Abstraction::setInit	(	const std::string &	name,
		NodeRef *	n
	)

setIpred()

void ilasynth::Abstraction::setIpred	(	const std::string &	name,
		NodeRef *	n
	)

setNext()

void ilasynth::Abstraction::setNext	(	const std::string &	name,
		NodeRef *	n
	)

setUpdateToFunction()

void ilasynth::Abstraction::setUpdateToFunction ( CppSimGen *  gen, CppFun *  fun, nptr_t  valid, bool  doHier = false  ) const

private

synthesizeAll()

void ilasynth::Abstraction::synthesizeAll

(

PyObject *

fun

)

synthesizeElement()

NodeRef* ilasynth::Abstraction::synthesizeElement	(	const std::string &	name,
		NodeRef *	expr,
		PyObject *	fun
	)

synthesizeReg()

void ilasynth::Abstraction::synthesizeReg	(	const std::string &	name,
		PyObject *	fun
	)

toBoogie()

void ilasynth::Abstraction::toBoogie

(

const std::string &

filename

)

Friends And Related Function Documentation

AbstractionWrapper

friend class AbstractionWrapper

friend

BoogieTranslator

friend class BoogieTranslator

friend

DetermineUnrollBound

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

friend

MicroUnroller

friend class MicroUnroller

friend

Synthesizer

friend class Synthesizer

friend

Member Data Documentation

_ht

HornTranslator* ilasynth::Abstraction::_ht

private

assumps

nptr_vec_t ilasynth::Abstraction::assumps

protected

bits

nmap_t ilasynth::Abstraction::bits

protected

decodeExprs

nptr_vec_t ilasynth::Abstraction::decodeExprs

protected

fetchExpr

nptr_t ilasynth::Abstraction::fetchExpr

protected

fetchValid

nptr_t ilasynth::Abstraction::fetchValid

protected

funcReducer

FuncReduction ilasynth::Abstraction::funcReducer

mutableprivate

funs

nmap_t ilasynth::Abstraction::funs

protected

inps

nmap_t ilasynth::Abstraction::inps

protected

MAX_SYN_ITER

int ilasynth::Abstraction::MAX_SYN_ITER

private

mems

nmap_t ilasynth::Abstraction::mems

protected

name

const std::string ilasynth::Abstraction::name

protected

names

std::map<std::string, state_t> ilasynth::Abstraction::names

protected

objCnt

int ilasynth::Abstraction::objCnt

staticprivate

paramSyn

int ilasynth::Abstraction::paramSyn

parent

Abstraction* ilasynth::Abstraction::parent

protected

reduceWhenImport

int ilasynth::Abstraction::reduceWhenImport

regs

nmap_t ilasynth::Abstraction::regs

protected

uabs

uabs_map_t ilasynth::Abstraction::uabs

protected

vlgExpConfig

VlgExportConfig ilasynth::Abstraction::vlgExpConfig

---

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

• abstraction.hpp