u_unroller_smt.h

Go to the documentation of this file.

#ifndef ILANG_ILA_MNGR_U_UNROLLER_SMT_H__
#define ILANG_ILA_MNGR_U_UNROLLER_SMT_H__

#include <map>
#include <string>
#include <vector>

#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/target-smt/smt_shim.h>
#include <ilang/util/log.h>

namespace ilang {

template <class Generator> class UnrollerSmt {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  UnrollerSmt(SmtShim<Generator>& smt_shim, const std::string& suffix)
      : smt_gen_(smt_shim), unroller_suffix_(suffix) {}

  // ------------------------- METHODS -------------------------------------- //
  //
  // Control property/predicate beyond the transition.
  //
  inline void AssertGlobal(const ExprPtr& p) { global_pred_.insert(p); }
  inline void AssertInitial(const ExprPtr& p) { initial_pred_.insert(p); }
  inline void AssertStep(const ExprPtr& p, const int& k) {
    step_pred_[k].insert(p);
  }
  inline void ClearGlobalAssertion() { global_pred_.clear(); }
  inline void ClearInitialAssertion() { initial_pred_.clear(); }
  inline void ClearStepAssertion() { step_pred_.clear(); }

  //
  // Access SMT formula in the unrolled execution.
  //
  inline auto GetSmtCurrent(const ExprPtr& expr, const size_t& k) const {
    return smt_gen_.GetShimExpr(expr, SuffixCurrent(k));
  }
  inline auto GetSmtNext(const ExprPtr& expr, const size_t& k) const {
    return smt_gen_.GetShimExpr(expr, SuffixNext(k));
  }
  inline auto GetSmtFuncDecl(const FuncPtr& func) const {
    return smt_gen_.GetShimFunc(func);
  }

private:
  // ------------------------- MEMBERS -------------------------------------- //
  SmtShim<Generator>& smt_gen_;
  const std::string unroller_suffix_;

  ExprSet global_pred_;
  ExprSet initial_pred_;
  std::map<size_t, ExprSet> step_pred_;

  // ------------------------- HELPERS -------------------------------------- //
  inline std::string SuffixCurrent(const size_t& t) const {
    return std::to_string(t) + "_" + unroller_suffix_;
  }
  inline std::string SuffixNext(const size_t& t) const {
    return std::to_string(t) + "_" + unroller_suffix_ + ".nxt";
  }

protected:
  // ------------------------- TYPES ---------------------------------------- //
  typedef decltype(smt_gen_.GetShimExpr(nullptr, "")) SmtExpr;
  typedef decltype(smt_gen_.GetShimFunc(nullptr)) SmtFunc;
  typedef std::vector<ExprPtr> IlaExprVec;
  typedef std::vector<SmtExpr> SmtExprVec;

  // ------------------------- MEMBERS -------------------------------------- //
  IlaExprVec deciding_vars_;
  IlaExprVec update_holder_;
  IlaExprVec assert_holder_;

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

  virtual void MakeOneTransition(const size_t& idx) = 0;

  SmtExpr Unroll_(const size_t& len, const size_t& begin);

  SmtExpr UnrollWithStepsUnconnected_(const size_t& len, const size_t& begin);

private:
  // ------------------------- HELPERS -------------------------------------- //
  inline void InterpIlaExprAndAppend(const IlaExprVec& ila_expr_src,
                                     const std::string& suffix,
                                     SmtExprVec& smt_expr_dst) {
    for (const auto& e : ila_expr_src) {
      smt_expr_dst.push_back(smt_gen_.GetShimExpr(e, suffix));
    }
  }

  inline void InterpIlaExprAndAppend(const ExprSet& ila_expr_src,
                                     const std::string& suffix,
                                     SmtExprVec& smt_expr_dst) {
    for (const auto& e : ila_expr_src) {
      smt_expr_dst.push_back(smt_gen_.GetShimExpr(e, suffix));
    }
  }

  inline void ElementWiseEqualAndAppend(const SmtExprVec& a,
                                        const SmtExprVec& b,
                                        SmtExprVec& smt_expr_dst) {
    ILA_ASSERT(a.size() == b.size());
    for (size_t i = 0; i < a.size(); i++) {
      smt_expr_dst.push_back(smt_gen_.Equal(a.at(i), b.at(i)));
    }
  }

  inline SmtExpr ConjunctAll(const SmtExprVec& vec) const {
    auto conjunct_holder = smt_gen_.GetShimExpr(asthub::BoolConst(true));
    for (const auto& e : vec) {
      conjunct_holder = smt_gen_.BoolAnd(conjunct_holder, e);
    }
    return conjunct_holder;
  }

}; // class UnrollerSmt

template <class Generator> class PathUnroller : public UnrollerSmt<Generator> {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  PathUnroller(SmtShim<Generator>& smt_shim, const std::string& suffix = "")
      : UnrollerSmt<Generator>(smt_shim, suffix) {}

  // ------------------------- METHODS -------------------------------------- //
  auto Unroll(const InstrVec& seq, const size_t& begin = 0) {
    seq_ = seq;
    return this->Unroll_(seq.size(), begin);
  }

  auto UnrollWithStepsUnconnected(const InstrVec& seq, const size_t& begin) {
    seq_ = seq;
    return this->UnrollWithStepsUnconnected_(seq.size(), begin);
  }

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

  void MakeOneTransition(const size_t& idx);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  InstrVec seq_;

}; // class PathUnroller

} // namespace ilang

#endif // ILANG_ILA_MNGR_U_UNROLLER_SMT_H__