ilang::HostRemoveRestore Class Reference

Class to remove and restore the host info This is useful as we want the ast with the same name generates the same z3 expr. This framework is based on an assumption that if we call z3 to create the variable of the same name multiple times they refer to the same one internally. FIXME: Need to check this assumption if we want to support other SMT solvers! More...

#include <inter_ila_unroller.h>

Public Types
typedef std::map< ExprPtr, InstrLvlAbsPtr >	ExprHostMap
	type of the internal map
typedef std::function< bool(const ExprPtr &)>	ExprJudgeFunc

Public Member Functions
	HostRemoveRestore ()
	Default constructor: do nothing.
	~HostRemoveRestore ()
	Default destructor: do nothing.
void	RecordAndRemove (ExprPtr exp)
	record the host field and remove them
void	RecordAndRemoveIf (ExprPtr exp, ExprJudgeFunc f)
	record the host field and remove them if allowed by the second argument This only provides more constraints in additional to RecordAndRemove (var type, not recorded or compatible with old records) This is useful as we only need to replace the host() of shared variables
void	RecordAndReplaceIf (ExprPtr exp, ExprJudgeFunc f, InstrLvlAbsPtr h)
void	Restore (ExprPtr exp)
	add back the host field according to the map
void	RestoreAll (InstrLvlAbsPtr h=nullptr)
	restore all the expr recoreded

Detailed Description

Class to remove and restore the host info This is useful as we want the ast with the same name generates the same z3 expr. This framework is based on an assumption that if we call z3 to create the variable of the same name multiple times they refer to the same one internally. FIXME: Need to check this assumption if we want to support other SMT solvers!

Member Typedef Documentation

typedef std::function<bool(const ExprPtr&)> ilang::HostRemoveRestore::ExprJudgeFunc

type of function object from to decide if we should remove the host of a expr or not

---

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

• inter_ila_unroller.h