ilang++.h

Go to the documentation of this file.

#ifndef ILANG_ILANG_CPP_H__
#define ILANG_ILANG_CPP_H__

#include <cstdint>
#include <map>
#include <memory>
#include <string>
#include <vector>

#include <z3++.h>
#ifdef SMTSWITCH_INTERFACE
#include <smt-switch/smt.h>
#endif // SMTSWITCH_INTERFACE

#include <ilang/config.h>

namespace ilang {

typedef uint64_t NumericType;

/******************************************************************************/
// Logging system.
/******************************************************************************/
void LogLevel(const int& lvl);
void LogPath(const std::string& path);
void LogToErr(bool to_err);
void EnableDebug(const std::string& tag);
void DisableDebug(const std::string& tag);

/******************************************************************************/
// ILA Construction.
/******************************************************************************/
// implementation-specific structure
class Sort;
class Func;
class Expr;
class Instr;
class InstrLvlAbs;
class Unroller;

// forward declaration
class Ila;

class SortRef {
private:
  typedef std::shared_ptr<Sort> SortPtr;
  // ------------------------- MEMBERS -------------------------------------- //
  SortPtr ptr_ = nullptr;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  SortRef(SortPtr ptr);
  ~SortRef();

  // ------------------------- HELPERS -------------------------------------- //
  static SortRef BOOL();
  static SortRef BV(const int& bit_w);
  static SortRef MEM(const int& addr_w, const int& data_w);

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline SortPtr get() const { return ptr_; }
}; // class SortRef

class ExprRef {
private:
  typedef std::shared_ptr<Expr> ExprPtr;
  // ------------------------- MEMBERS -------------------------------------- //
  ExprPtr ptr_ = nullptr;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  ExprRef(ExprPtr ptr);
  ~ExprRef();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline ExprPtr get() const { return ptr_; }
  int bit_width() const;
  int addr_width() const;
  int data_width() const;
  std::string name() const;

  // ------------------------- METHODS -------------------------------------- //
  /****************************************************************************/
  // Memory-related operations
  /****************************************************************************/
  ExprRef Load(const ExprRef& addr) const;
  ExprRef Store(const ExprRef& addr, const ExprRef& data) const;
  ExprRef Load(const NumericType& addr) const;
  ExprRef Store(const NumericType& addr, const NumericType& data) const;

  /****************************************************************************/
  // Bit manipulation for bit-vectors.
  /****************************************************************************/
  ExprRef Append(const ExprRef& lsbv) const;
  ExprRef operator()(const int& hi, const int& lo) const;
  ExprRef operator()(const int& idx) const;
  ExprRef ZExt(const int& length) const;
  ExprRef SExt(const int& length) const;

  /****************************************************************************/
  // Others
  /****************************************************************************/
  void ReplaceArg(const int& i, const ExprRef& new_arg);
  void ReplaceArg(const ExprRef& org_arg, const ExprRef& new_arg);

  bool SetEntryNum(const int& num);
  int GetEntryNum();

}; // class ExprRef

/******************************************************************************/
// Unary operation
/******************************************************************************/
ExprRef operator-(const ExprRef& a);
ExprRef operator!(const ExprRef& a);
ExprRef operator~(const ExprRef& a);

/******************************************************************************/
// Binary operation
/******************************************************************************/
ExprRef operator&(const ExprRef& a, const ExprRef& b);
ExprRef operator|(const ExprRef& a, const ExprRef& b);
ExprRef operator^(const ExprRef& a, const ExprRef& b);
ExprRef operator<<(const ExprRef& a, const ExprRef& b);
ExprRef operator>>(const ExprRef& a, const ExprRef& b);
ExprRef Lshr(const ExprRef& a, const ExprRef& b);
ExprRef operator+(const ExprRef& a, const ExprRef& b);
ExprRef operator-(const ExprRef& a, const ExprRef& b);
ExprRef operator*(const ExprRef& a, const ExprRef& b);
ExprRef operator/(const ExprRef& a, const ExprRef& b);

ExprRef operator&(const ExprRef& a, const bool& b);
ExprRef operator|(const ExprRef& a, const bool& b);
ExprRef operator^(const ExprRef& a, const bool& b);
ExprRef operator<<(const ExprRef& a, const int& b);
ExprRef operator>>(const ExprRef& a, const int& b);
ExprRef Lshr(const ExprRef& a, const int& b);
ExprRef operator+(const ExprRef& a, const NumericType& b);
ExprRef operator-(const ExprRef& a, const NumericType& b);
ExprRef operator*(const ExprRef& a, const NumericType& b);
ExprRef SRem(const ExprRef& a, const ExprRef& b);
ExprRef URem(const ExprRef& a, const ExprRef& b);
ExprRef SMod(const ExprRef& a, const ExprRef& b);

/******************************************************************************/
// Binary comparison
/******************************************************************************/
void SetUnsignedComparison(bool sign);
ExprRef operator==(const ExprRef& a, const ExprRef& b);
ExprRef operator!=(const ExprRef& a, const ExprRef& b);
ExprRef operator<(const ExprRef& a, const ExprRef& b);
ExprRef operator>(const ExprRef& a, const ExprRef& b);
ExprRef operator<=(const ExprRef& a, const ExprRef& b);
ExprRef operator>=(const ExprRef& a, const ExprRef& b);
ExprRef Ult(const ExprRef& a, const ExprRef& b);
ExprRef Ugt(const ExprRef& a, const ExprRef& b);
ExprRef Ule(const ExprRef& a, const ExprRef& b);
ExprRef Uge(const ExprRef& a, const ExprRef& b);
ExprRef Slt(const ExprRef& a, const ExprRef& b);
ExprRef Sgt(const ExprRef& a, const ExprRef& b);
ExprRef Sle(const ExprRef& a, const ExprRef& b);
ExprRef Sge(const ExprRef& a, const ExprRef& b);

// helper functions with constants
#if 0
ExprRef operator==(const ExprRef& a, const bool& b);
#endif
ExprRef operator==(const ExprRef& a, const NumericType& b);
ExprRef operator!=(const ExprRef& a, const NumericType& b);
ExprRef operator<(const ExprRef& a, const NumericType& b);
ExprRef operator>(const ExprRef& a, const NumericType& b);
ExprRef operator<=(const ExprRef& a, const NumericType& b);
ExprRef operator>=(const ExprRef& a, const NumericType& b);
ExprRef Ult(const ExprRef& a, const NumericType& b);
ExprRef Ugt(const ExprRef& a, const NumericType& b);
ExprRef Ule(const ExprRef& a, const NumericType& b);
ExprRef Uge(const ExprRef& a, const NumericType& b);
ExprRef Slt(const ExprRef& a, const NumericType& b);
ExprRef Sgt(const ExprRef& a, const NumericType& b);
ExprRef Sle(const ExprRef& a, const NumericType& b);
ExprRef Sge(const ExprRef& a, const NumericType& b);

/******************************************************************************/
// Memory-related operations
/******************************************************************************/
ExprRef Load(const ExprRef& mem, const ExprRef& addr);
ExprRef Store(const ExprRef& mem, const ExprRef& addr, const ExprRef& data);
ExprRef Load(const ExprRef& mem, const NumericType& addr);
ExprRef Store(const ExprRef& mem, const NumericType& addr,
              const NumericType& data);

/******************************************************************************/
// Bit manipulation for bit-vectors.
/******************************************************************************/
ExprRef Concat(const ExprRef& msbv, const ExprRef& lsbv);
ExprRef Extract(const ExprRef& bv, const int& hi, const int& lo);
ExprRef SelectBit(const ExprRef& bv, const int& idx);
ExprRef ZExt(const ExprRef& bv, const int& length);
ExprRef SExt(const ExprRef& bv, const int& length);
ExprRef LRotate(const ExprRef& bv, const int& immediate);
ExprRef RRotate(const ExprRef& bv, const int& immediate);

/******************************************************************************/
// Others
/******************************************************************************/
ExprRef Imply(const ExprRef& ante, const ExprRef& cons);

ExprRef Ite(const ExprRef& cond, const ExprRef& t, const ExprRef& f);

/******************************************************************************/
// Constant
/******************************************************************************/
ExprRef BoolConst(bool bool_val);

ExprRef BvConst(const NumericType& bv_val, const int& bit_width);

ExprRef MemConst(const NumericType& def_val,
                 const std::map<NumericType, NumericType>& vals,
                 const int& addr_width, const int& data_width);

/******************************************************************************/
// Non-AST-construction
/******************************************************************************/
bool TopEqual(const ExprRef& a, const ExprRef& b);

class FuncRef {
private:
  typedef std::shared_ptr<Func> FuncPtr;
  // ------------------------- MEMBERS -------------------------------------- //
  FuncPtr ptr_ = nullptr;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  FuncRef(const std::string& name, const SortRef& range);
  FuncRef(const std::string& name, const SortRef& range, const SortRef& d0);
  FuncRef(const std::string& name, const SortRef& range, const SortRef& d0,
          const SortRef& d1);
  FuncRef(const std::string& name, const SortRef& range,
          const std::vector<SortRef>& dvec);
  ~FuncRef();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  std::string name() const;
  inline FuncPtr get() const { return ptr_; }

  // ------------------------- METHODS -------------------------------------- //
  ExprRef operator()() const;
  ExprRef operator()(const ExprRef& arg0) const;
  ExprRef operator()(const ExprRef& arg0, const ExprRef& arg1) const;
  ExprRef operator()(const std::vector<ExprRef>& argvec) const;

}; // class FuncRef

class InstrRef {
private:
  typedef std::shared_ptr<Instr> InstrPtr;
  // ------------------------- MEMBERS -------------------------------------- //
  InstrPtr ptr_ = nullptr;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  InstrRef(InstrPtr ptr);
  ~InstrRef();

  // ------------------------- METHODS -------------------------------------- //
  void SetDecode(const ExprRef& decode);

  void SetUpdate(const ExprRef& state, const ExprRef& update);

  void SetProgram(const Ila& prog);

  ExprRef GetDecode() const;

  ExprRef GetUpdate(const ExprRef& state) const;

  // ------------------------- GENERATORS --------------------------------- //
  void ExportToVerilog(std::ostream& fout) const;

  void ExportToVerilogWithChild(std::ostream& fout) const;

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline InstrPtr get() const { return ptr_; }

  std::string name() const;

}; // class InstrRef

class Ila {
private:
  typedef std::shared_ptr<InstrLvlAbs> IlaPtr;
  // ------------------------- MEMBERS -------------------------------------- //
  IlaPtr ptr_ = nullptr;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  Ila(const std::string& name);
  Ila(IlaPtr ptr);
  ~Ila();

  // ------------------------- METHODS -------------------------------------- //
  ExprRef NewBoolState(const std::string& name);
  ExprRef NewBvState(const std::string& name, const int& bit_width);
  ExprRef NewMemState(const std::string& name, const int& addr_width,
                      const int& data_width);

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

  void AddInit(const ExprRef& init);

  void SetFetch(const ExprRef& fetch);

  void SetValid(const ExprRef& valid);

  InstrRef NewInstr(const std::string& name);

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

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  size_t input_num() const;
  size_t state_num() const;
  size_t instr_num() const;
  size_t child_num() const;
  size_t init_num() const;

  std::string name() const;
  ExprRef fetch() const;
  ExprRef valid() const;

  ExprRef input(const size_t& i) const;
  ExprRef state(const size_t& i) const;
  InstrRef instr(const size_t& i) const;
  Ila child(const size_t& i) const;
  ExprRef init(const size_t& i) const;

  ExprRef input(const std::string& name) const;
  ExprRef state(const std::string& name) const;
  InstrRef instr(const std::string& name) const;
  Ila child(const std::string& name) const;

  inline IlaPtr get() const { return ptr_; }

  // ------------------------- UTILITIES ------------------------------------ //
  void ExportToVerilog(std::ostream& fout) const;

  void FlattenHierarchy();

  typedef enum PassID {
    SANITY_CHECK_AND_FIX = 0,
    SIMPLIFY_SYNTACTIC,
    SIMPLIFY_SEMANTIC,
    REWRITE_CONDITIONAL_STORE,
    REWRITE_LOAD_FROM_STORE
  } PassID;

  bool ExecutePass(const std::vector<PassID>& passes) const;

}; // class Ila

/******************************************************************************/
// Output stream helper
/******************************************************************************/
std::ostream& operator<<(std::ostream& out, const ExprRef& expr);
std::ostream& operator<<(std::ostream& out, const InstrRef& instr);
std::ostream& operator<<(std::ostream& out, const Ila& ila);

/******************************************************************************/
// Converters
/******************************************************************************/
bool ExportIlaPortable(const Ila& ila, const std::string& file_name);

Ila ImportIlaPortable(const std::string& file_name);

#ifdef SYNTH_INTERFACE
Ila ImportSynthAbstraction(const std::string& file_name,
                           const std::string& ila_name);

void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent,
                                 const std::string& ila_name);
#endif // SYNTH_INTERFACE

void ExportSysCSim(const Ila& ila, const std::string& dir_path,
                   bool optimize = false);

/******************************************************************************/
// Verification.
/******************************************************************************/
class IlaZ3Unroller {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  IlaZ3Unroller(z3::context& ctx, const std::string& suff = "");
  ~IlaZ3Unroller();

  // ------------------------- METHODS -------------------------------------- //
  inline void AddGlobPred(const ExprRef& p) { glob_pred_.push_back(p); }
  inline void AddInitPred(const ExprRef& p) { init_pred_.push_back(p); }
  inline void AddStepPred(const int& k, const ExprRef& p) {
    step_pred_.push_back({k, p});
  }
  inline void ClearGlobPred() { glob_pred_.clear(); }
  inline void ClearInitPred() { init_pred_.clear(); }
  inline void ClearStepPred() { step_pred_.clear(); }

  z3::expr UnrollMonoConn(const Ila& top, const int& k, const int& init = 0);

  z3::expr UnrollMonoFree(const Ila& top, const int& k, const int& init = 0);

  z3::expr UnrollPathConn(const std::vector<InstrRef>& path,
                          const int& init = 0);

  z3::expr UnrollPathSubs(const std::vector<InstrRef>& path,
                          const int& init = 0);

  z3::expr UnrollPathFree(const std::vector<InstrRef>& path,
                          const int& init = 0);

  // ------------------------- HELPERS -------------------------------------- //
  z3::expr CurrState(const ExprRef& v, const int& t);
  z3::expr NextState(const ExprRef& v, const int& t);
  z3::expr GetZ3Expr(const ExprRef& v, const int& t = 0);
  z3::expr Equal(const ExprRef& va, const int& ta, const ExprRef& vb,
                 const int& tb);
  z3::func_decl GetZ3FuncDecl(const FuncRef& f) const;

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

  std::vector<ExprRef> glob_pred_;
  std::vector<ExprRef> init_pred_;
  std::vector<std::pair<int, ExprRef>> step_pred_;
  std::string extra_suff_;

  std::shared_ptr<Unroller> univ_ = nullptr;

  // ------------------------- HELPERS -------------------------------------- //
  template <class T> void InitializeUnroller(T unroller) {
    for (auto it = glob_pred_.begin(); it != glob_pred_.end(); it++) {
      unroller->AddGlobPred(it->get());
    }
    for (auto it = init_pred_.begin(); it != init_pred_.end(); it++) {
      unroller->AddInitPred(it->get());
    }
    for (auto it = step_pred_.begin(); it != step_pred_.end(); it++) {
      unroller->AddStepPred(it->second.get(), it->first);
    }
    // unroller->SetExtraSuffix(extra_suff_);
  }

}; // class IlaZ3Unroller

#ifdef SMTSWITCH_INTERFACE

smt::Term ResetAndGetSmtTerm(smt::SmtSolver& solver, const ExprRef& expr,
                             const std::string& suffix = "");

#endif // SMTSWITCH_INTERFACE

} // namespace ilang

#endif // ILANG_ILANG_CPP_H__