v_eq_check_refinement.h

Go to the documentation of this file.

#ifndef ILANG_ILA_MNGR_V_EQ_CHECK_REFINEMENT_H__
#define ILANG_ILA_MNGR_V_EQ_CHECK_REFINEMENT_H__

#include <z3++.h>

#include <ilang/ila-mngr/u_unroller.h>
#include <ilang/ila/instr_lvl_abs.h>

namespace ilang {

class RefinementMap {
public:
  typedef std::shared_ptr<RefinementMap> RefPtr;

  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  RefinementMap();
  ~RefinementMap();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline InstrLvlAbsPtr coi() const { return coi_; }
  inline InstrLvlAbsPtr ila() const { return coi_; }
  inline ExprPtr appl() const { return appl_; }
  inline ExprPtr flush() const { return flush_; }
  inline ExprPtr cmpl() const { return cmpl_; }
  inline const int& step_appl() const { return step_appl_; }
  inline const int& step_orig() const { return step_orig_; }
  inline const int& step() const { return step_orig(); }
  inline size_t inv_num() const { return invs_.size(); }
  inline ExprPtr inv(const size_t& i) const { return invs_.at(i); }

  void set_tgt(const InstrLvlAbsPtr& tgt);
  void set_tgt(const InstrPtr& tgt);
  void set_appl(const ExprPtr& appl);
  void set_flush(const ExprPtr& flush);
  void set_cmpl(const ExprPtr& cmpl);
  inline void set_step(const int& step) { set_step_orig(step); }
  void set_step_appl(const int& step);
  void set_step_orig(const int& step);
  void add_inv(const ExprPtr& inv);

  // ------------------------- HELPERS -------------------------------------- //
  static RefPtr New();

private:
  // ------------------------- MEMBERS -------------------------------------- //
  InstrLvlAbsPtr coi_ = nullptr;
  ExprPtr appl_ = nullptr;
  ExprPtr flush_ = nullptr;
  ExprPtr cmpl_ = asthub::BoolConst(true);
  int step_appl_ = -1;
  int step_orig_ = -1;
  std::vector<ExprPtr> invs_;

}; // RefinementMap

typedef RefinementMap::RefPtr RefPtr;

class RelationMap {
public:
  typedef std::shared_ptr<RelationMap> RelPtr;

  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  RelationMap();
  ~RelationMap();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  void add(const ExprPtr& rel);
  inline ExprPtr get() const { return acc_; }

  // ------------------------- HELPERS -------------------------------------- //
  static RelPtr New();

private:
  // ------------------------- MEMBERS -------------------------------------- //
  ExprPtr acc_ = asthub::BoolConst(true);

}; // RelationMap

typedef RelationMap::RelPtr RelPtr;

class CompRefRel {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  typedef std::shared_ptr<CompRefRel> CrrPtr;

  CompRefRel(const RefPtr ref_a, const RefPtr ref_b, const RelPtr rel);
  ~CompRefRel();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline RefPtr refine_a() const { return ref_a_; }
  inline RefPtr refine_b() const { return ref_b_; }
  inline RelPtr relation() const { return rel_; }

  // ------------------------- HELPERS -------------------------------------- //
  static CrrPtr New(const RefPtr ref_a = RefinementMap::New(),
                    const RefPtr ref_b = RefinementMap::New(),
                    const RelPtr rel = RelationMap::New());

private:
  // ------------------------- MEMBERS -------------------------------------- //
  RefPtr ref_a_;
  RefPtr ref_b_;
  RelPtr rel_;

}; // CompRefRel

typedef CompRefRel::CrrPtr CrrPtr;

class CommDiag {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  CommDiag(z3::context& ctx, const CrrPtr crr);
  ~CommDiag();

  // ------------------------- METHODS -------------------------------------- //
  bool EqCheck(const int& max = 10);

  bool IncEqCheck(const int& min = 0, const int& max = 10, const int& step = 1);

  bool IncCheck(const int& min = 0, const int& max = 10, const int& step = 1);

  typedef MonoUnroll Unroll;

private:
  // ------------------------- MEMBERS -------------------------------------- //
  z3::context& ctx_;
  CrrPtr crr_;

  // ------------------------- IncCheck ------------------------------------- //

  void Init();

  enum UID { A_OLD, A_NEW, B_OLD, B_NEW };

  struct UnrlUnit {
    int lo = 0;
    int hi = 0;
  } uu_a_old_, uu_a_new_, uu_b_old_, uu_b_new_;

  Unroll unrl_a_old_ = Unroll(ctx_, k_suff_old_);
  Unroll unrl_a_new_ = Unroll(ctx_, k_suff_new_);
  Unroll unrl_b_old_ = Unroll(ctx_, k_suff_old_);
  Unroll unrl_b_new_ = Unroll(ctx_, k_suff_new_);

  ExprSet stts_a_;
  ExprSet stts_b_;

  Unroll& GetUnrl(const UID& uid);
  Unroll& GetUnrlOld();
  Unroll& GetUnrlNew();
  Unroll& GetUnrlApl();

  RefPtr GetRefine(const UID& uid);
  UnrlUnit& GetUnrlUnit(const UID& uid);
  const ExprSet& GetStts(const UID& uid);

  z3::expr GetZ3IncFlsh(const UID& uid);
  z3::expr GetZ3IncCmpl(const UID& uid);

  // ------------------------- IncEqCheck ----------------------------------- //
  static const std::string k_suff_old_;
  static const std::string k_suff_new_;
  static const std::string k_suff_apl_;
  MonoUnroll unrl_old_ = MonoUnroll(ctx_, k_suff_old_);
  MonoUnroll unrl_new_ = MonoUnroll(ctx_, k_suff_new_);
  MonoUnroll unrl_apl_ = MonoUnroll(ctx_, k_suff_apl_);

  z3::expr GetZ3ApplInstr(const ExprSet& stts, const RefPtr ref);
  z3::expr GetZ3Assm();
  z3::expr GetZ3Prop();
  z3::expr GetZ3Cmpl(const ExprPtr& cmpl, MonoUnroll& un, const int& begin,
                     const int& end) const;
  z3::expr GetZ3IncUnrl(MonoUnroll& un, const RefPtr ref, const int& begin,
                        const int& length, const ExprSet& stts) const;
  bool CheckCmpl(z3::solver& s, z3::expr& cmpl_expr) const;

  // ------------------------- MonoCheck ------------------------------------ //
  static const std::string k_suff_orig_;
  static const std::string k_suff_appl_;
  MonoUnroll unroll_appl_ = MonoUnroll(ctx_, k_suff_appl_);
  MonoUnroll unroll_orig_ = MonoUnroll(ctx_, k_suff_orig_);

  bool SanityCheck();
  bool SanityCheckRefinement(const RefPtr ref);
  bool SanityCheckRelation(const RelPtr rel, const InstrLvlAbsPtr& ma,
                           const InstrLvlAbsPtr& mb) const;

  int DetStepOrig(const RefPtr ref, const int& max);
  int DetStepAppl(const RefPtr ref, const int& max);
  bool CheckStepOrig(const RefPtr ref, const int& k);
  bool CheckStepAppl(const RefPtr ref, const int& k);

  z3::expr GenInit(const RefPtr ref);
  z3::expr GenTranRel(const RefPtr ref, const int& k_orig, const int& k_appl);
  z3::expr GenAssm();
  z3::expr GenProp();

  z3::expr AtLeastOnce(MonoUnroll& unroller, const ExprPtr& cmpl,
                       const int& start, const int& end) const;
  z3::expr AtMostOnce(MonoUnroll& unroller, const ExprPtr& cmpl,
                      const int& start, const int& end) const;
  z3::expr UnrollFlush(MonoUnroll& unroller, const RefPtr ref, const int& base,
                       const int& length, const int& start);

}; // class CommDiag

} // namespace ilang

#endif // ILANG_ILA_MNGR_V_EQ_CHECK_REFINEMENT_H__