instr_lvl_abs.h

Go to the documentation of this file.

#ifndef ILANG_ILA_INSTR_LVL_ABS_H__
#define ILANG_ILA_INSTR_LVL_ABS_H__

#include <map>
#include <memory>
#include <ostream>
#include <stack>
#include <string>

#include <ilang/ila/ast/func.h>
#include <ilang/ila/ast_hub.h>
#include <ilang/ila/hash_ast.h>
#include <ilang/ila/instr.h>
#include <ilang/ila/object.h>
#include <ilang/ila/transition.h>
#include <ilang/util/container.h>

namespace ilang {

class InstrLvlAbs : public Object,
                    public std::enable_shared_from_this<InstrLvlAbs> {
public:
  typedef std::shared_ptr<InstrLvlAbs> InstrLvlAbsPtr;
  typedef std::shared_ptr<const InstrLvlAbs> InstrLvlAbsCnstPtr;
  typedef KeyVec<Symbol, InstrLvlAbsPtr> InstrLvlAbsMap;

private:
  typedef KeyVec<Symbol, ExprPtr> VarMap;
  typedef KeyVec<Symbol, InstrPtr> InstrMap;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  InstrLvlAbs(const std::string& name = "",
              const InstrLvlAbsPtr& parent = nullptr);
  ~InstrLvlAbs();

  // ------------------------- HELPERS -------------------------------------- //
  static InstrLvlAbsPtr New(const std::string& name,
                            const InstrLvlAbsPtr& parent = nullptr);

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  bool is_instr_lvl_abs() const { return true; }

  inline bool is_spec() const { return is_spec_; }
  inline const InstrLvlAbsPtr parent() const { return parent_; }
  inline const ExprMngrPtr expr_mngr() const { return expr_mngr_; }

  inline void set_spec(bool spec) { is_spec_ = spec; }
  inline void set_expr_mngr(const ExprMngrPtr expr_mngr) {
    expr_mngr_ = expr_mngr;
  }

  inline size_t input_num() const { return inputs_.size(); }
  inline size_t state_num() const { return states_.size(); }
  inline size_t instr_num() const { return instrs_.size(); }
  inline size_t child_num() const { return childs_.size(); }
  inline size_t init_num() const { return inits_.size(); }

  inline const ExprPtr fetch() const { return fetch_; }
  inline const ExprPtr valid() const { return valid_; }

  inline const ExprPtr input(const size_t& i) const { return inputs_[i]; }
  inline const ExprPtr state(const size_t& i) const { return states_[i]; }
  inline const InstrPtr instr(const size_t& i) const { return instrs_[i]; }
  inline const InstrLvlAbsPtr child(const size_t& i) const {
    return childs_[i];
  }
  const ExprPtr init(const size_t& i) const { return inits_[i]; }

  const ExprPtr input(const std::string& name) const;
  const ExprPtr state(const std::string& name) const;
  const InstrPtr instr(const std::string& name) const;
  const InstrLvlAbsPtr child(const std::string& name) const;

  const ExprPtr find_input(const Symbol& name) const;
  const ExprPtr find_state(const Symbol& name) const;
  const InstrPtr find_instr(const Symbol& name) const;
  const InstrLvlAbsPtr find_child(const Symbol& name) const;

  const InstrSeqPtr& instr_seq() const { return instr_seq_; }

  // ------------------------- METHODS -------------------------------------- //
  void AddInput(const ExprPtr& input_var);

  void AddState(const ExprPtr& state_var);

  void AddInit(const ExprPtr& cntr_expr);

  void SetFetch(const ExprPtr& fetch_expr);

  void SetValid(const ExprPtr& valid_expr);

  void AddInstr(const InstrPtr& instr);

  void AddChild(const InstrLvlAbsPtr& child);

  const ExprPtr NewBoolInput(const std::string& name);

  const ExprPtr NewBvInput(const std::string& name, const int& bit_width);

  const ExprPtr NewMemInput(const std::string& name, const int& addr_width,
                            const int& data_width);

  const ExprPtr NewBoolState(const std::string& name);

  const ExprPtr NewBvState(const std::string& name, const int& bit_width);

  const ExprPtr NewMemState(const std::string& name, const int& addr_width,
                            const int& data_width);

  const ExprPtr NewBoolFreeVar(const std::string& name);

  const ExprPtr NewBvFreeVar(const std::string& name, const int& bit_width);

  const ExprPtr NewMemFreeVar(const std::string& name, const int& addr_width,
                              const int& data_width);

  const InstrPtr NewInstr(const std::string& name = "");

  const InstrLvlAbsPtr NewChild(const std::string& name);

  void ForceSetFetch(const ExprPtr& fetch_expr);

  void ForceSetValid(const ExprPtr& valid_expr);

  void AddSeqTran(const InstrPtr& src, const InstrPtr& dst, const ExprPtr& cnd);

  std::string GetRootName() const;

  std::ostream& Print(std::ostream& out) const;

  friend std::ostream& operator<<(std::ostream& out, InstrLvlAbs& ila);
  friend std::ostream& operator<<(std::ostream& out, InstrLvlAbsPtr ila);
  friend std::ostream& operator<<(std::ostream& out, InstrLvlAbsCnstPtr ila);

  friend class Instr;

  template <class F> void DepthFirstVisit(F& func) const {
    // traverse child
    for (decltype(child_num()) i = 0; i != child_num(); i++) {
      auto child_i = this->child(i);
      child_i->DepthFirstVisit<F>(func);
    }
    // apply function ()
    func(shared_from_this());
  }

  template <class F> void DepthFirstVisitPrePost(F& func) const {
    // pre
    if (func.pre(shared_from_this())) { // break if return true
      return;
    }
    // traverse child
    for (decltype(child_num()) i = 0; i != child_num(); i++) {
      auto child_i = this->child(i);
      child_i->DepthFirstVisitPrePost<F>(func);
    }
    // post
    func.post(shared_from_this());
  }

private:
  // ------------------------- MEMBERS -------------------------------------- //
  InstrLvlAbsPtr parent_;
  VarMap inputs_;
  VarMap states_;
  ExprPtrVec inits_;
  ExprPtr fetch_ = nullptr;
  ExprPtr valid_ = nullptr;
  InstrMap instrs_;
  InstrLvlAbsMap childs_;
  // child-instr sequencing
  InstrSeqPtr instr_seq_ = nullptr;

  bool is_spec_ = true;

  ExprMngrPtr expr_mngr_ = nullptr;

  // ------------------------- HELPERS -------------------------------------- //
  ExprPtr Unify(const ExprPtr& e);
  void InitObject();
  void CheckInstr(const InstrPtr& instr);
  void SimplifyInstr(const InstrPtr& instr);

}; // class InstrLvlAbs

typedef InstrLvlAbs::InstrLvlAbsPtr InstrLvlAbsPtr;
typedef InstrLvlAbs::InstrLvlAbsCnstPtr InstrLvlAbsCnstPtr;
typedef std::map<InstrLvlAbsCnstPtr, InstrLvlAbsPtr> CnstIlaMap;

} // namespace ilang

#endif // ILANG_ILA_INSTR_LVL_ABS_H__