u_unroller.h

Go to the documentation of this file.

#ifndef ILANG_ILA_MNGR_U_UNROLLER_H__
#define ILANG_ILA_MNGR_U_UNROLLER_H__

#include <map>
#include <vector>

#include <z3++.h>

#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/target-smt/z3_expr_adapter.h>

namespace ilang {

class Unroller {
protected:
  typedef z3::expr ZExpr;
  typedef z3::expr_vector ZExprVec;
  typedef ExprPtrVec IExprVec;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  Unroller(z3::context& ctx, const std::string& suffix);
  virtual ~Unroller();

  // ------------------------- METHODS -------------------------------------- //
  void AddGlobPred(const ExprPtr& p);
  void AddInitPred(const ExprPtr& p);
  void AddStepPred(const ExprPtr& p, const int& k);
  void ClearGlobPred();
  void ClearInitPred();
  void ClearStepPred();
  void ClearPred();

  // ------------------------- HELPERS -------------------------------------- //
  ZExpr CurrState(const ExprPtr& v, const int& t);
  ZExpr NextState(const ExprPtr& v, const int& t);
  ZExpr GetZ3Expr(const ExprPtr& e, const int& t);
  ZExpr GetZ3Expr(const ExprPtr& e);
  ZExpr Equal(const ExprPtr& va, const int& ta, const ExprPtr& vb,
              const int& tb);
  z3::func_decl GetZ3FuncDecl(const FuncPtr& f) const;

protected:
  // ------------------------- MEMBERS -------------------------------------- //
  IExprVec vars_;
  IExprVec k_pred_;
  IExprVec k_next_;

  // ------------------------- METHODS -------------------------------------- //
  virtual void DefineDepVar() = 0;

  virtual void Transition(const int& idx) = 0;

  ZExpr UnrollSubs(const size_t& len, const int& pos);
  ZExpr UnrollAssn(const size_t& len, const int& pos, bool cache = false);
  ZExpr UnrollNone(const size_t& len, const int& pos);

  // ------------------------- HELPERS -------------------------------------- //
  static ExprPtr StateUpdCmpl(const InstrPtr& instr, const ExprPtr& var);
  static ExprPtr DecodeCmpl(const InstrPtr& instr);

  static ExprPtr NewFreeVar(const ExprPtr& var, const std::string& name);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  z3::context& ctx_;
  Z3ExprAdapter gen_;

  std::string extra_suff_ = "";

  IExprVec g_pred_;
  IExprVec i_pred_;
  std::map<int, IExprVec> s_pred_;

  ZExprVec k_prev_z3_;
  ZExprVec k_curr_z3_;
  ZExprVec k_next_z3_;

  ZExprVec cstr_;

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline z3::context& ctx() const { return ctx_; }
  inline Z3ExprAdapter& gen() { return gen_; }

  // ------------------------- HELPERS -------------------------------------- //
  void BootStrap(const int& pos, bool cache = false);

  void AssertEqual(const ZExprVec& z, const IExprVec& e,
                   const std::string& suffix);

  void Clear(ZExprVec& z3_vec);

  void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix,
                    ZExprVec& z_expr_dst);
  void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix,
                    ZExprVec& z_expr_dst, const ZExprVec& subs_src,
                    const ZExprVec& subs_dst);

  void CopyZExprVec(const ZExprVec& src, ZExprVec& dst);

  ZExpr ConjPred(const ZExprVec& vec) const;

  inline std::string SuffCurr(const int& t) const {
    return std::to_string(t) + "_" + extra_suff_;
  }
  inline std::string SuffNext(const int& t) const {
    return std::to_string(t) + "_" + extra_suff_ + ".nxt";
  }

}; // class Unroller

class PathUnroll : public Unroller {
public:
  typedef std::vector<InstrPtr> InstrVec;

  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  PathUnroll(z3::context& ctx, const std::string& suff = "");
  ~PathUnroll();

  // ------------------------- METHODS -------------------------------------- //
  ZExpr PathSubs(const std::vector<InstrPtr>& seq, const int& pos = 0);

  ZExpr PathAssn(const std::vector<InstrPtr>& seq, const int& pos = 0);

  ZExpr PathNone(const std::vector<InstrPtr>& seq, const int& pos = 0);

protected:
  // ------------------------- METHODS -------------------------------------- //
  void DefineDepVar();

  void Transition(const int& idx);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  InstrVec seq_;
}; // class PathUnroll

class MonoUnroll : public Unroller {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  MonoUnroll(z3::context& ctx, const std::string& suff = "");
  ~MonoUnroll();

  // ------------------------- METHODS -------------------------------------- //
  ZExpr MonoSubs(const InstrLvlAbsPtr& top, const int& length,
                 const int& pos = 0);

  ZExpr MonoAssn(const InstrLvlAbsPtr& top, const int& length,
                 const int& pos = 0);

  ZExpr MonoNone(const InstrLvlAbsPtr& top, const int& length,
                 const int& pos = 0);

  ZExpr MonoIncr(const InstrLvlAbsPtr& top, const int& length, const int& pos);

protected:
  // ------------------------- METHODS -------------------------------------- //
  void DefineDepVar();

  void Transition(const int& idx);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  InstrLvlAbsPtr top_;

}; // class MonoUnroll

} // namespace ilang

#endif // ILANG_ILA_MNGR_U_UNROLLER_H__