inter_ila_unroller.h

Go to the documentation of this file.

#ifndef ILANG_MCM_INTER_ILA_UNROLLER_H__
#define ILANG_MCM_INTER_ILA_UNROLLER_H__

#include <functional>
#include <list>
#include <set>
#include <stack>
#include <vector>

#include <z3++.h>

#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/mcm/memory_model.h>

namespace ilang {

class MemoryModel;

class InterIlaUnroller {
public:
  using ZExpr = MemoryModel::ZExpr;
  using ZExprVec = MemoryModel::ZExprVec;
  using StateNameSet = MemoryModel::StateNameSet;
  using InstrVec = MemoryModel::InstrVec;
  using ProgramTemplate = MemoryModel::ProgramTemplate;
  using ILANameStateNameSetMap = MemoryModel::ILANameStateNameSetMap;
  using TraceStepPtrSet = MemoryModel::TraceStepPtrSet;
  typedef std::vector<InstrLvlAbsPtr> IlaPtrVec;
  typedef std::list<ExprPtr> StateVarList;
  typedef std::map<std::string, StateVarList> SharedStatesSet;
  typedef std::unique_ptr<MemoryModel> MemoryModelPtr;
  typedef std::function<MemoryModelPtr(
      z3::context&,                  // z3 context
      ZExprVec&,                     // constrain list
      const StateNameSet&,           // shared state
      const ILANameStateNameSetMap&, // private state
      const InstrLvlAbsPtr&          // dummy global ila pointer
      )>
      MemoryModelCreator;
  typedef std::shared_ptr<TraceStep> TraceStepPtr;

  friend class MemoryModel;
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  InterIlaUnroller(z3::context& ctx, const IlaPtrVec& iv,
                   MemoryModelCreator mm_selector);
  virtual ~InterIlaUnroller();

  // ------------------------- METHODS -------------------------------------- //
  void GenSysInitConstraints();

  virtual void Unroll(const ProgramTemplate& tmpl);

  virtual void LinkStates(const std::vector<bool>& ordered);

  void AddSingleTraceStepProperty(const ExprPtr& property,
                                  std::function<bool(const TraceStep&)> filter);

  void
  GetSingleTraceStepProperty(const ExprPtr& property,
                             std::function<bool(const TraceStep&)> filter,
                             std::function<void(const z3::expr&)> collector);

  void SetFinalProperty(const ExprPtr& property);

  bool CheckSat();
  z3::model& GetModel();
  const ZExprVec& DebugAccessConstrList() const;
  const TraceStepPtrSet& DebugAccessAllTraceStepPtrSet() const;

  void Push();
  void Pop();

private:
  // ------------------------- MEMBERS -------------------------------------- //
  z3::context& ctx_;
  MemoryModelPtr mm_;
  std::unique_ptr<z3::model>
      model_ptr_; // should not shared with any one, you need to assume it will
                  // destroy along with the unroller
  std::stack<size_t> zexpr_vec_pos_stack_;

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline z3::context& ctx() const { return ctx_; }
  void createDummyGlobalIla();

protected:
  // ------------------------- HELPERS -------------------------------------- //
  void FindSharedStates();
  bool CurrConstrSat();
  ZExpr ConjPred(const ZExprVec& vec) const;

  // ------------------------- MEMBERS -------------------------------------- //

  IlaPtrVec sys_ila_;
  InstrLvlAbsPtr global_ila_;

  StateNameSet shared_states_;
  ILANameStateNameSetMap private_states_;

  ZExprVec cstr_;
  ZExprVec init_shared_vars_z3_;

}; // class InterIlaUnroller

/******************************************************************************/
// Helper Class
/******************************************************************************/


class HostRemoveRestore {
public:
  typedef std::map<ExprPtr, InstrLvlAbsPtr> ExprHostMap;
  typedef std::function<bool(const ExprPtr&)> ExprJudgeFunc;
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  HostRemoveRestore() {}
  ~HostRemoveRestore() {}
  // ------------------------- METHODS -------------------------------------- //
  void RecordAndRemove(ExprPtr exp);
  void RecordAndRemoveIf(ExprPtr exp, ExprJudgeFunc f);
  void RecordAndReplaceIf(ExprPtr exp, ExprJudgeFunc f, InstrLvlAbsPtr h);
  void Restore(ExprPtr exp);
  void RestoreAll(InstrLvlAbsPtr h = nullptr);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  ExprHostMap map_;
}; // class HostRemoveRestore

} // namespace ilang

#endif // ILANG_MCM_INTER_ILA_UNROLLER_H__