ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | List of all members
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, InstrLvlAbsPtrExprHostMap
 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

◆ ExprJudgeFunc

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: