ilang  1.1.4
ILAng: A Modeling and Verification Platform for SoCs
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Friends Macros
Go to the documentation of this file.
7 #include <functional>
8 #include <list>
9 #include <set>
10 #include <stack>
11 #include <vector>
13 #include <z3++.h>
16 #include <ilang/mcm/memory_model.h>
19 namespace ilang {
21 class MemoryModel;
30 public:
47  typedef std::vector<InstrLvlAbsPtr> IlaPtrVec;
49  typedef std::list<ExprPtr> StateVarList;
51  typedef std::map<std::string, StateVarList> SharedStatesSet;
54  typedef std::unique_ptr<MemoryModel> MemoryModelPtr;
57  typedef std::function<MemoryModelPtr(
58  z3::context&, // z3 context
59  ZExprVec&, // constrain list
60  const StateNameSet&, // shared state
61  const ILANameStateNameSetMap&, // private state
62  const InstrLvlAbsPtr& // dummy global ila pointer
63  )>
66  typedef std::shared_ptr<TraceStep> TraceStepPtr;
68  friend class MemoryModel;
69  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
71  InterIlaUnroller(z3::context& ctx, const IlaPtrVec& iv,
72  MemoryModelCreator mm_selector);
74  virtual ~InterIlaUnroller();
76  // ------------------------- METHODS -------------------------------------- //
79  void GenSysInitConstraints();
83  virtual void Unroll(const ProgramTemplate& tmpl);
87  virtual void LinkStates(const std::vector<bool>& ordered);
93  void AddSingleTraceStepProperty(const ExprPtr& property,
94  std::function<bool(const TraceStep&)> filter);
101  void
102  GetSingleTraceStepProperty(const ExprPtr& property,
103  std::function<bool(const TraceStep&)> filter,
104  std::function<void(const z3::expr&)> collector);
108  void SetFinalProperty(const ExprPtr& property);
112  bool CheckSat();
115  z3::model& GetModel();
118  const ZExprVec& DebugAccessConstrList() const;
124  void Push();
126  void Pop();
128 private:
129  // ------------------------- MEMBERS -------------------------------------- //
131  z3::context& ctx_;
133  MemoryModelPtr mm_;
135  std::unique_ptr<z3::model>
136  model_ptr_; // should not shared with any one, you need to assume it will
137  // destroy along with the unroller
139  std::stack<size_t> zexpr_vec_pos_stack_;
141  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
143  inline z3::context& ctx() const { return ctx_; }
145  void createDummyGlobalIla();
147 protected:
148  // ------------------------- HELPERS -------------------------------------- //
151  void FindSharedStates();
153  bool CurrConstrSat();
155  ZExpr ConjPred(const ZExprVec& vec) const;
157  // ------------------------- MEMBERS -------------------------------------- //
174 }; // class InterIlaUnroller
176 /******************************************************************************/
177 // Helper Class
178 /******************************************************************************/
189 public:
191  typedef std::map<ExprPtr, InstrLvlAbsPtr> ExprHostMap;
194  typedef std::function<bool(const ExprPtr&)> ExprJudgeFunc;
195  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
200  // ------------------------- METHODS -------------------------------------- //
202  void RecordAndRemove(ExprPtr exp);
208  void RecordAndReplaceIf(ExprPtr exp, ExprJudgeFunc f, InstrLvlAbsPtr h);
210  void Restore(ExprPtr exp);
212  void RestoreAll(InstrLvlAbsPtr h = nullptr);
214 private:
215  // ------------------------- MEMBERS -------------------------------------- //
217  ExprHostMap map_;
218 }; // class HostRemoveRestore
220 } // namespace ilang
std::vector< InstrVec > ProgramTemplate
Definition: memory_model.h:217
void GenSysInitConstraints()
it generates the initial constraints and put them on to the constraint list and check should be calle...
std::map< ExprPtr, InstrLvlAbsPtr > ExprHostMap
type of the internal map
Definition: inter_ila_unroller.h:191
void RecordAndRemove(ExprPtr exp)
record the host field and remove them
TraceStep::TraceStepPtrSet TraceStepPtrSet
Type of trace steps, we need to collect the set of trace steps (WRITE)
Definition: memory_model.h:206
void SetFinalProperty(const ExprPtr &property)
Set final property (you should only call this function only ONCE)
StateNameSet shared_states_
Set of names of shared states.
Definition: inter_ila_unroller.h:165
Expr::ExprPtr ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:138
std::map< std::string, StateNameSet > ILANameStateNameSetMap
Type of map ila-name to state-set.
Definition: memory_model.h:222
MemoryModel::ProgramTemplate ProgramTemplate
Definition: inter_ila_unroller.h:41
Class to remove and restore the host info This is useful as we want the ast with the same name genera...
Definition: inter_ila_unroller.h:188
bool CurrConstrSat()
Sanity check if the current constraints are satisfiable.
Default destructor: do nothing.
Definition: inter_ila_unroller.h:199
ZExprVec init_shared_vars_z3_
The set of constraints that should be asserted.
Definition: inter_ila_unroller.h:172
ILANameStateNameSetMap private_states_
Map from ila-name to set-of-state-names.
Definition: inter_ila_unroller.h:167
const ZExprVec & DebugAccessConstrList() const
Get access to expr vector, will only be usable if unroller is not destroyed, only for DEBUG use...
The class for trace step (an instance of instruction) As in the unrolling, there may be multiple inst...
Definition: memory_model.h:28
std::function< bool(const ExprPtr &)> ExprJudgeFunc
Definition: inter_ila_unroller.h:194
InterIlaUnroller(z3::context &ctx, const IlaPtrVec &iv, MemoryModelCreator mm_selector)
Default constructor. mm_selector is used to create mm internally.
void RestoreAll(InstrLvlAbsPtr h=nullptr)
restore all the expr recoreded
std::shared_ptr< TraceStep > TraceStepPtr
Type of trace step pointer.
Definition: inter_ila_unroller.h:66
std::function< MemoryModelPtr(z3::context &, ZExprVec &, const StateNameSet &, const ILANameStateNameSetMap &, const InstrLvlAbsPtr &)> MemoryModelCreator
Definition: inter_ila_unroller.h:64
MemoryModel::StateNameSet StateNameSet
Type of state name set.
Definition: inter_ila_unroller.h:36
TraceStep::ZExprVec ZExprVec
Type for containing a vector of z3::expr.
Definition: memory_model.h:202
void Pop()
Restore the previous set of constraints.
std::vector< InstrLvlAbsPtr > IlaPtrVec
Type of vector of pointers to the ILAs involved.
Definition: inter_ila_unroller.h:47
const TraceStepPtrSet & DebugAccessAllTraceStepPtrSet() const
Get access to expr vector, will only be usable if unroller is not destroyed, only for DEBUG use...
std::vector< InstrPtr > InstrVec
Type of an instruction vector to represent a sequence.
Definition: memory_model.h:214
void AddSingleTraceStepProperty(const ExprPtr &property, std::function< bool(const TraceStep &)> filter)
Add a property.
MemoryModel::TraceStepPtrSet TraceStepPtrSet
Type of set of trace step pointers (DEBUG use)
Definition: inter_ila_unroller.h:45
MemoryModel::ILANameStateNameSetMap ILANameStateNameSetMap
Type of map ila-name to state-set.
Definition: inter_ila_unroller.h:43
InstrLvlAbs::InstrLvlAbsPtr InstrLvlAbsPtr
Pointer type for normal use of InstrLvlAbs.
Definition: instr_lvl_abs.h:326
Base class for unrolling multiple ILAs. There are two ways of unrolling: ordered and unordered...
Definition: inter_ila_unroller.h:29
virtual void LinkStates(const std::vector< bool > &ordered)
[Application-specific] Link states, where each trace step read from
void Push()
Push the size of current set of constraints.
std::unique_ptr< MemoryModel > MemoryModelPtr
Definition: inter_ila_unroller.h:54
TraceStep::StateNameSet StateNameSet
Type of set of state names.
Definition: memory_model.h:210
ZExpr ConjPred(const ZExprVec &vec) const
Conjunct (AND) all the predicates in the set.
Default constructor: do nothing.
Definition: inter_ila_unroller.h:197
IlaPtrVec sys_ila_
The ILAs of an SoC.
Definition: inter_ila_unroller.h:160
MemoryModel::ZExprVec ZExprVec
Type for containing a vector of z3::expr.
Definition: inter_ila_unroller.h:34
virtual void Unroll(const ProgramTemplate &tmpl)
[Application-specific] Unroll, currently just use PathUnroller
void FindSharedStates()
It create a name list. There is no need to create an ExprPtr list because their hosts are different a...
virtual ~InterIlaUnroller()
Default destructor.
ZExprVec cstr_
The set of constraints that should be asserted.
Definition: inter_ila_unroller.h:170
std::map< std::string, StateVarList > SharedStatesSet
Type of map of shared states (set of names -&gt; list of exprs)
Definition: inter_ila_unroller.h:51
void GetSingleTraceStepProperty(const ExprPtr &property, std::function< bool(const TraceStep &)> filter, std::function< void(const z3::expr &)> collector)
Get the z3 expression of a property on a trace step, so you can play with it.
void RecordAndRemoveIf(ExprPtr exp, ExprJudgeFunc f)
record the host field and remove them if allowed by the second argument This only provides more const...
void Restore(ExprPtr exp)
add back the host field according to the map
bool CheckSat()
Check and potentially set the model: return true if sat , false o.w.
The base class for memory models.
Definition: memory_model.h:196
MemoryModel::InstrVec InstrVec
Type of an instruction vector to represent a sequence.
Definition: inter_ila_unroller.h:38
std::list< ExprPtr > StateVarList
Type of list of state variables.
Definition: inter_ila_unroller.h:49
TraceStep::ZExpr ZExpr
Type alias for z3::expr.
Definition: memory_model.h:200
MemoryModel::ZExpr ZExpr
Type alias for z3::expr.
Definition: inter_ila_unroller.h:32
InstrLvlAbsPtr global_ila_
The ILA of the system.
Definition: inter_ila_unroller.h:162
z3::model & GetModel()
Get the model: the reference will only be usable if unroller is not destroyed.