memory_model.h

Go to the documentation of this file.

#ifndef ILANG_MCM_MEMORY_MODEL_H__
#define ILANG_MCM_MEMORY_MODEL_H__

#include <ilang/mcm/ast_helper.h>
#include <ilang/mcm/axiom_helper.h>
#include <ilang/target-smt/z3_expr_adapter.h>

namespace ilang {

#define FINAL_STEP_SUFFIX "final"

enum AccessType { READ, WRITE, EITHER };
class MemoryModel;
// used when query the type of accesses (in register trace step)

// HZ note: accessors like w1.wfe.global should be interpreted as an accessor
// function e.g., _wfe_global(w1) This function may either convert to a derived
// class or access a fixed member to extract the attribute HZ note: In a memory
// model, usually a derived class of TraceStep is used.
class TraceStep {
  friend class MemoryModel;

public:
  typedef z3::expr ZExpr;
  typedef std::vector<ZExpr> ZExprVec;
  typedef std::shared_ptr<TraceStep> TraceStepPtr;
  typedef std::set<TraceStepPtr> TraceStepPtrSet;
  typedef std::set<std::string> StateNameSet;
  enum TraceStepType { INST_EVT, FACET_EVT, INIT_EVT, FINAL_EVT };
  // ------------------------- MEMREAD BOOKKEEPING
  // -------------------------------------- //
  typedef std::vector<std::pair<ExprPtr, ExprPtr>> AddrDataVec;
  typedef std::unordered_map<std::string, AddrDataVec> MRFVal;

private:
  // ------------------------- HELPERS -------------------------------------- //
  std::string
  GetName(); // This is the helper function to generate unique names,
             // this is private and usshould not be used to return the name of
             // the current trace step. Please use name()
  static unsigned trace_step_seq_no;
  void InitReadWriteSet(const InstrPtr& inst);
  void InitReadSetForProperty(const ExprPtr& e);

  // ------------------------- MEMREAD BOOKKEEPING
  // -------------------------------------- //
  mutable MRFVal nad_map_;
  mutable bool already_searched_for_memreadpair_;
  void
  FindAddrDataPairVecInExpr(const ExprPtr& node,
                            NestedMemAddrDataAvoider& nested_finder_) const;
  void VisitNodeForMemoryRead(const ExprPtr& node,
                              NestedMemAddrDataAvoider& nested_finder_) const;
  const AddrDataVec&
  FindAddrDataPairVecInInst(const std::string& sname,
                            NestedMemAddrDataAvoider& nested_finder_) const;

protected:
  // ------------------------- MEMBERS -------------------------------------- //
  TraceStepType _type;
  // Type : INST_EVT
  InstrPtr _inst; // I assume it is nullptr by default
  // Type : FACET_EVT
  InstrPtr _parent_inst;
  StateNameSet _read_state_set;
  StateNameSet _write_state_set;

  StateNameSet _inst_read_set; // this applies to both inst-evt and facet-evt
  StateNameSet _inst_write_set; // this applies to both inst-evt and facet-evt

  ZExprVec& _cstr;
  std::string _name;
  z3::expr timestamp;
  size_t _pos_suffix;
  mutable Z3ExprAdapter _expr2z3_;
  z3::context& _ctx_;
  InstrLvlAbsPtr _host_final_;
  ExprPtr _final_property;

public:
  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  InstrLvlAbsPtr host() const;
  std::string name() const { return _name; }
  const StateNameSet& get_inst_read_set() const { return _inst_read_set; }
  const StateNameSet& get_inst_write_set() const { return _inst_write_set; }
  const TraceStepType& type() const { return _type; }
  bool is_init_tracestep() const { return _type == TraceStepType::INIT_EVT; }
  bool is_facet_tracestep() const { return _type == TraceStepType::FACET_EVT; }
  bool is_final_tracestep() const { return _type == TraceStepType::FINAL_EVT; }

  InstrPtr inst() const;
  size_t pos_suffix() const;
  inline Z3ExprAdapter& z3adapter() const { return _expr2z3_; }
  z3::context& ctx() { return _ctx_; }
  ExprPtr final_property() { return _final_property; }

  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  TraceStep(const InstrPtr& inst, ZExprVec& cstr, z3::context& ctx, size_t pos);
  TraceStep(const InstrPtr& inst, ZExprVec& cstr, z3::context& ctx,
            ZExpr _ts_overwrite, size_t pos);
  TraceStep(const InstrPtr& ref_inst, ZExprVec& cstr, z3::context& ctx,
            const std::string& fevt_name, size_t pos);
  TraceStep(const ExprPtr& property, ZExprVec& cstr, z3::context& ctx,
            const InstrLvlAbsPtr& host);
  virtual ~TraceStep() {}
  // ------------------------- MEMBERS -------------------------------------- //
  void AddStateAccess(const std::string& name, AccessType acc_type);
  void AddStateAccess(const StateNameSet& s, AccessType acc_type);
  ZExpr ConvertZ3OnThisStep(const ExprPtr& ast) const;

  // ------------------------- HELPERS -------------------------------------- //
  bool Access(AccessType acc_type, const std::string& name) const;
  bool Access(AccessType acc_type, const StateNameSet& stateset) const;

  // ------------------------- HELPERS -------------------------------------- //
  std::string Print(z3::model& m) const;

}; // class TraceStep

class MemoryModel {

public:
  using ZExpr = TraceStep::ZExpr;
  using ZExprVec = TraceStep::ZExprVec;
  using TraceStepPtr = TraceStep::TraceStepPtr;
  using TraceStepPtrSet = TraceStep::TraceStepPtrSet;
  using TraceStepType = TraceStep::TraceStepType;
  using StateNameSet = TraceStep::StateNameSet;
  using AddrDataVec = TraceStep::AddrDataVec;
  typedef std::vector<InstrPtr> InstrVec;
  typedef std::vector<InstrVec> ProgramTemplate;
  typedef std::vector<std::vector<TraceStepPtr>> PerILATraceStepPtrSet;
  typedef std::map<std::string, StateNameSet> ILANameStateNameSetMap;

protected:
  // ------------------------- MEMBERS -------------------------------------- //
  TraceStepPtr
      _init_trace_step; // will be assigned by function CreateGlobalInitStep
  TraceStepPtr
      _final_trace_step; // will be assigned by function CreateGlobalFinalStep
  TraceStepPtrSet _all_trace_steps; // will be assigned by specific memory model
  TraceStepPtrSet
      _all_inst_trace_steps; // will be assigned by specific memory model
  PerILATraceStepPtrSet _ila_trace_steps;
  const StateNameSet&
      m_shared_state_names; // will get a copy from the given set
  const ILANameStateNameSetMap&
      m_ila_private_state_names; // will get a copy from the given set
  InstrLvlAbsPtr m_p_global_ila;
  // For passing argument, we need to keep track of the following info:
  z3::context& _ctx_;
  ZExprVec& _constr;
  mutable Z3ExprAdapter _expr2z3_;

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  z3::context& ctx() const { return _ctx_; }

public:
  ZExpr ConvertZ3(const ExprPtr& ast, const std::string& suffix) const {
    return _expr2z3_.GetExpr(ast, suffix);
  }

public:
  void virtual InitSize(const ProgramTemplate& _tmpl);
  void virtual RegisterSteps(size_t regIdx, const InstrVec& _inst_seq) = 0;
  void virtual FinishRegisterSteps() = 0;
  void virtual ApplyAxioms() = 0;
  void virtual SetLocalState(const std::vector<bool>& ordered);
  // HZ note: All the steps should be registered through the first function:
  // RegisterSteps
  void virtual AddSingleTraceStepProperty(
      const ExprPtr& property, std::function<bool(const TraceStep&)> filter);
  void virtual GetSingleTraceStepProperty(
      const ExprPtr& property, std::function<bool(const TraceStep&)> filter,
      std::function<void(const z3::expr&)> collector);
  void virtual SetFinalProperty(const ExprPtr& property) = 0;
  void virtual AddDoubleTraceStepProperty(
      std::function<z3::expr(const TraceStep&, const TraceStep&)>,
      std::function<bool(const TraceStep&, const TraceStep&)>);
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  // we will need a wrapper on the outside
  MemoryModel(z3::context& ctx, ZExprVec& _cstrlist,
              const StateNameSet& shared_states,
              const ILANameStateNameSetMap& private_states,
              const InstrLvlAbsPtr& global_ila_ptr);
  // make destructor virtual
  virtual ~MemoryModel() {}
  // ------------------------- HELPERS -------------------------------------- //
  // bool AccessShared ( const InstrPtr & ip, AccessType acc_type );  //
  // (deprecated)

  // ------------------------- DEBUG USE ONLY --------------------------------
  // //
  const TraceStepPtrSet& GetAllTraceSteps() const { return _all_trace_steps; }

  // ------------------------- AXIOM HELPERS -------------------------------- //
protected:
  // ------------------------- MEMBERS -------------------------------------- //
  mutable NestedMemAddrDataAvoider nested_finder_;
  // ------------------------- HELPERS -------------------------------------- //
  TraceStepPtr CreateGlobalInitStep();
  TraceStepPtr CreateGlobalFinalStep(const ExprPtr& property);
  // ------------------------- AXIOM HELPERS
  // -------------------------------------- // The implementation of the
  // following functions can be found in axiom_helper.cpp The type of results
  // that can statically determined
  enum StaticResult { STATIC_TRUE = 1, STATIC_FALSE, STATIC_UNKNOWN };
  // The type of hints given to the functions to tell what kind of mem ops to
  // look for
  enum AxiomFuncHint {
    HINT_NONE = 0,
    HINT_READ = 1,
    HINT_WRITE
  }; // if read disable write-set, if write disable read-set // should only used
     // for SameAddr/SameData
  // Happen-before
  z3::expr HB(const TraceStep& l, const TraceStep& r) const;
  // At the same time
  z3::expr Sync(const TraceStep& l, const TraceStep& r) const;
  // Program-order
  z3::expr PO(const TraceStep& l, const TraceStep& r) const;
  // Same address
  z3::expr SameAddress(const TraceStep& l, const TraceStep& r,
                       const std::string& sname,
                       AxiomFuncHint lhint = HINT_NONE,
                       AxiomFuncHint rhint = HINT_NONE) const;
  // Get decode (z3 not ast)
  z3::expr Decode(const TraceStep& l) const;
  // Enforce same data
  z3::expr SameData(const TraceStep& l, const TraceStep& r,
                    const std::string& sname, AxiomFuncHint lhint = HINT_NONE,
                    AxiomFuncHint rhint = HINT_NONE) const;
  // Enforcing same core constraint
  bool SameCore(const TraceStep& l, const TraceStep& r) const;
  // STATICALLY DETERMINED // not implemented
  StaticResult SameAddressStatic(const TraceStep& l, const TraceStep& r) const;
  // STATICALLY DETERMINED // not implemented
  StaticResult DecodeStatic(const TraceStep& l) const;
  // STATICALLY DETERMINED // not implemented
  StaticResult SameCoreStatic(const TraceStep& l, const TraceStep& r) const;

  z3::expr Z3ForallList(const ZExprVec& l) const; // move into mcm class
  z3::expr Z3ExistsList(const ZExprVec& l) const;

private:
  z3::expr MemVarSameAddress(const ExprPtr& leftWAddr,
                             const AddrDataVec& leftRAddrDataVec,
                             const ExprPtr& rightWAddr,
                             const AddrDataVec& rightRAddrDataVec,
                             const TraceStep& traceL,
                             const TraceStep& traceR) const;
  z3::expr MemVarSameData(const std::pair<ExprPtr, ExprPtr>& leftAddrDataPair,
                          const AddrDataVec& leftRAddrDataVec,
                          const std::pair<ExprPtr, ExprPtr>& rightAddrDataPair,
                          const AddrDataVec& rightRAddrDataVec,
                          const TraceStep& traceL, const TraceStep& traceR,
                          const ExprPtr& memVar) const;
  ExprPtr CheckAndPeel(const ExprPtr& e, const std::string& type,
                       size_t argn) const;
  z3::expr NonMemVarSameData(const TraceStep& l, const TraceStep& r,
                             const std::string& sname, AxiomFuncHint lhint,
                             AxiomFuncHint rhint) const;
  void SameAddrDataSanityCheck(const TraceStep& l, const TraceStep& r,
                               const std::string& sname) const;

}; // class MemoryModel

} // namespace ilang

#endif // ILANG_MCM_MEMORY_MODEL_H__