ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
inter_ila_unroller.h
Go to the documentation of this file.
1 
4 #ifndef ILANG_MCM_INTER_ILA_UNROLLER_H__
5 #define ILANG_MCM_INTER_ILA_UNROLLER_H__
6 
7 #include <functional>
8 #include <list>
9 #include <set>
10 #include <stack>
11 #include <vector>
12 
15 #include "ilang/mcm/memory_model.h"
16 #include "z3++.h"
17 
19 namespace ilang {
20 
21 class MemoryModel;
22 
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;
67 
68  friend class MemoryModel;
69  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
71  InterIlaUnroller(z3::context& ctx, const IlaPtrVec& iv,
72  MemoryModelCreator mm_selector);
74  virtual ~InterIlaUnroller();
75 
76  // ------------------------- METHODS -------------------------------------- //
79  void GenSysInitConstraints();
80 
83  virtual void Unroll(const ProgramTemplate& tmpl);
84 
87  virtual void LinkStates(const std::vector<bool>& ordered);
88 
93  void AddSingleTraceStepProperty(const ExprPtr& property,
94  std::function<bool(const TraceStep&)> filter);
95 
101  void
102  GetSingleTraceStepProperty(const ExprPtr& property,
103  std::function<bool(const TraceStep&)> filter,
104  std::function<void(const z3::expr&)> collector);
105 
108  void SetFinalProperty(const ExprPtr& property);
109 
112  bool CheckSat();
115  z3::model& GetModel();
118  const ZExprVec& DebugAccessConstrList() const;
122 
124  void Push();
126  void Pop();
127 
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_;
140 
141  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
143  inline z3::context& ctx() const { return ctx_; }
145  void createDummyGlobalIla();
146 
147 protected:
148  // ------------------------- HELPERS -------------------------------------- //
151  void FindSharedStates();
153  bool CurrConstrSat();
155  ZExpr ConjPred(const ZExprVec& vec) const;
156 
157  // ------------------------- MEMBERS -------------------------------------- //
158 
163 
168 
173 
174 }; // class InterIlaUnroller
175 
176 /******************************************************************************/
177 // Helper Class
178 /******************************************************************************/
179 
187 
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);
213 
214 private:
215  // ------------------------- MEMBERS -------------------------------------- //
217  ExprHostMap map_;
218 }; // class HostRemoveRestore
219 
220 } // namespace ilang
221 
222 #endif // ILANG_MCM_INTER_ILA_UNROLLER_H__
ilang::InterIlaUnroller::sys_ila_
IlaPtrVec sys_ila_
The ILAs of an SoC.
Definition: inter_ila_unroller.h:160
ilang::HostRemoveRestore::RecordAndRemove
void RecordAndRemove(ExprPtr exp)
record the host field and remove them
ilang::InterIlaUnroller::MemoryModelPtr
std::unique_ptr< MemoryModel > MemoryModelPtr
Definition: inter_ila_unroller.h:54
ilang::TraceStep
The class for trace step (an instance of instruction) As in the unrolling, there may be multiple inst...
Definition: memory_model.h:27
ilang::InterIlaUnroller::StateNameSet
MemoryModel::StateNameSet StateNameSet
Type of state name set.
Definition: inter_ila_unroller.h:36
ilang::MemoryModel::StateNameSet
TraceStep::StateNameSet StateNameSet
Type of set of state names.
Definition: memory_model.h:209
ilang::InterIlaUnroller::TraceStepPtr
std::shared_ptr< TraceStep > TraceStepPtr
Type of trace step pointer.
Definition: inter_ila_unroller.h:66
ilang::InterIlaUnroller::ILANameStateNameSetMap
MemoryModel::ILANameStateNameSetMap ILANameStateNameSetMap
Type of map ila-name to state-set.
Definition: inter_ila_unroller.h:43
ilang::InterIlaUnroller::LinkStates
virtual void LinkStates(const std::vector< bool > &ordered)
[Application-specific] Link states, where each trace step read from
ilang::ExprPtr
Expr::ExprPtr ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:133
ilang::InterIlaUnroller::CheckSat
bool CheckSat()
Check and potentially set the model: return true if sat , false o.w.
ilang::HostRemoveRestore::~HostRemoveRestore
~HostRemoveRestore()
Default destructor: do nothing.
Definition: inter_ila_unroller.h:199
ilang::InterIlaUnroller::cstr_
ZExprVec cstr_
The set of constraints that should be asserted.
Definition: inter_ila_unroller.h:170
ilang::InterIlaUnroller::AddSingleTraceStepProperty
void AddSingleTraceStepProperty(const ExprPtr &property, std::function< bool(const TraceStep &)> filter)
Add a property.
ilang::InterIlaUnroller::ZExprVec
MemoryModel::ZExprVec ZExprVec
Type for containing a vector of z3::expr.
Definition: inter_ila_unroller.h:34
ilang::InterIlaUnroller::Unroll
virtual void Unroll(const ProgramTemplate &tmpl)
[Application-specific] Unroll, currently just use PathUnroller
ilang::InterIlaUnroller::MemoryModelCreator
std::function< MemoryModelPtr(z3::context &, ZExprVec &, const StateNameSet &, const ILANameStateNameSetMap &, const InstrLvlAbsPtr &)> MemoryModelCreator
Definition: inter_ila_unroller.h:64
ilang::HostRemoveRestore::ExprJudgeFunc
std::function< bool(const ExprPtr &)> ExprJudgeFunc
Definition: inter_ila_unroller.h:194
ilang::InterIlaUnroller::DebugAccessAllTraceStepPtrSet
const TraceStepPtrSet & DebugAccessAllTraceStepPtrSet() const
Get access to expr vector, will only be usable if unroller is not destroyed, only for DEBUG use.
ilang::MemoryModel::TraceStepPtrSet
TraceStep::TraceStepPtrSet TraceStepPtrSet
Type of trace steps, we need to collect the set of trace steps (WRITE)
Definition: memory_model.h:205
ilang::InterIlaUnroller::ConjPred
ZExpr ConjPred(const ZExprVec &vec) const
Conjunct (AND) all the predicates in the set.
ilang::InterIlaUnroller::SharedStatesSet
std::map< std::string, StateVarList > SharedStatesSet
Type of map of shared states (set of names -> list of exprs)
Definition: inter_ila_unroller.h:51
ilang::MemoryModel::ZExprVec
TraceStep::ZExprVec ZExprVec
Type for containing a vector of z3::expr.
Definition: memory_model.h:201
ilang::InterIlaUnroller::private_states_
ILANameStateNameSetMap private_states_
Map from ila-name to set-of-state-names.
Definition: inter_ila_unroller.h:167
ilang::InterIlaUnroller::TraceStepPtrSet
MemoryModel::TraceStepPtrSet TraceStepPtrSet
Type of set of trace step pointers (DEBUG use)
Definition: inter_ila_unroller.h:45
ilang::HostRemoveRestore::RestoreAll
void RestoreAll(InstrLvlAbsPtr h=nullptr)
restore all the expr recoreded
ilang::InterIlaUnroller::StateVarList
std::list< ExprPtr > StateVarList
Type of list of state variables.
Definition: inter_ila_unroller.h:49
ilang::InterIlaUnroller::ZExpr
MemoryModel::ZExpr ZExpr
Type alias for z3::expr.
Definition: inter_ila_unroller.h:32
ilang::InterIlaUnroller::global_ila_
InstrLvlAbsPtr global_ila_
The ILA of the system.
Definition: inter_ila_unroller.h:162
ilang::InterIlaUnroller::shared_states_
StateNameSet shared_states_
Set of names of shared states.
Definition: inter_ila_unroller.h:165
ilang
ilang::InterIlaUnroller::GetSingleTraceStepProperty
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.
ilang::InterIlaUnroller::GenSysInitConstraints
void GenSysInitConstraints()
it generates the initial constraints and put them on to the constraint list and check should be calle...
ilang::InstrLvlAbsPtr
InstrLvlAbs::InstrLvlAbsPtr InstrLvlAbsPtr
Pointer type for normal use of InstrLvlAbs.
Definition: instr_lvl_abs.h:326
ilang::InterIlaUnroller::CurrConstrSat
bool CurrConstrSat()
Sanity check if the current constraints are satisfiable.
ilang::InterIlaUnroller::DebugAccessConstrList
const ZExprVec & DebugAccessConstrList() const
Get access to expr vector, will only be usable if unroller is not destroyed, only for DEBUG use.
ilang::MemoryModel::InstrVec
std::vector< InstrPtr > InstrVec
Type of an instruction vector to represent a sequence.
Definition: memory_model.h:213
ilang::MemoryModel::ZExpr
TraceStep::ZExpr ZExpr
Type alias for z3::expr.
Definition: memory_model.h:199
ilang::HostRemoveRestore
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
z3_expr_adapter.h
ilang::InterIlaUnroller::IlaPtrVec
std::vector< InstrLvlAbsPtr > IlaPtrVec
Type of vector of pointers to the ILAs involved.
Definition: inter_ila_unroller.h:47
ilang::MemoryModel::ProgramTemplate
std::vector< InstrVec > ProgramTemplate
Definition: memory_model.h:216
ilang::InterIlaUnroller::InstrVec
MemoryModel::InstrVec InstrVec
Type of an instruction vector to represent a sequence.
Definition: inter_ila_unroller.h:38
ilang::HostRemoveRestore::HostRemoveRestore
HostRemoveRestore()
Default constructor: do nothing.
Definition: inter_ila_unroller.h:197
ilang::InterIlaUnroller::Pop
void Pop()
Restore the previous set of constraints.
ilang::InterIlaUnroller::GetModel
z3::model & GetModel()
Get the model: the reference will only be usable if unroller is not destroyed.
ilang::MemoryModel::ILANameStateNameSetMap
std::map< std::string, StateNameSet > ILANameStateNameSetMap
Type of map ila-name to state-set.
Definition: memory_model.h:221
ilang::InterIlaUnroller::ProgramTemplate
MemoryModel::ProgramTemplate ProgramTemplate
Definition: inter_ila_unroller.h:41
ilang::InterIlaUnroller::Push
void Push()
Push the size of current set of constraints.
ilang::InterIlaUnroller::init_shared_vars_z3_
ZExprVec init_shared_vars_z3_
The set of constraints that should be asserted.
Definition: inter_ila_unroller.h:172
ilang::InterIlaUnroller::InterIlaUnroller
InterIlaUnroller(z3::context &ctx, const IlaPtrVec &iv, MemoryModelCreator mm_selector)
Default constructor. mm_selector is used to create mm internally.
memory_model.h
instr_lvl_abs.h
ilang::InterIlaUnroller::FindSharedStates
void FindSharedStates()
It create a name list. There is no need to create an ExprPtr list because their hosts are different a...
ilang::HostRemoveRestore::Restore
void Restore(ExprPtr exp)
add back the host field according to the map
ilang::InterIlaUnroller::~InterIlaUnroller
virtual ~InterIlaUnroller()
Default destructor.
ilang::MemoryModel
The base class for memory models.
Definition: memory_model.h:195
ilang::InterIlaUnroller::SetFinalProperty
void SetFinalProperty(const ExprPtr &property)
Set final property (you should only call this function only ONCE)
ilang::InterIlaUnroller
Base class for unrolling multiple ILAs. There are two ways of unrolling: ordered and unordered....
Definition: inter_ila_unroller.h:29
ilang::HostRemoveRestore::RecordAndRemoveIf
void RecordAndRemoveIf(ExprPtr exp, ExprJudgeFunc f)
record the host field and remove them if allowed by the second argument This only provides more const...
ilang::HostRemoveRestore::ExprHostMap
std::map< ExprPtr, InstrLvlAbsPtr > ExprHostMap
type of the internal map
Definition: inter_ila_unroller.h:191