abst_to_ila.h

Go to the documentation of this file.

#ifndef ILANG_TARGET_ITSY_ABST_TO_ILA_H__
#define ILANG_TARGET_ITSY_ABST_TO_ILA_H__

#include <memory>
#include <string>
#include <vector>

#include <ilang/ila/instr_lvl_abs.h>
#include <ilasynth/abstraction.hpp>

namespace ilang {

class SynthAbsConverter {
public:
  typedef std::shared_ptr<SynthAbsConverter> SynthAbsConverterPtr;

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

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

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //

  // ------------------------- METHODS -------------------------------------- //
  InstrLvlAbsPtr Convert(const ilasynth::Abstraction& abs);

  void Port(const ilasynth::Abstraction& abs, const InstrLvlAbsPtr& ila);

  ExprPtr ConvertSynthNodeToIlangExpr(const ilasynth::nptr_t& node,
                                      const InstrLvlAbsPtr& ila);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  std::map<const ilasynth::Node*, ExprPtr> node_expr_map_;
  std::map<const ilasynth::Node*, FuncPtr> node_func_map_;

  ExprSet decom_entry_;
  std::map<ExprPtr, ExprPtr> decom_match_;
  ExprSet decom_glue_;
  ExprSet decom_else_;

  // ------------------------- HELPERS -------------------------------------- //
  void Reset() {
    node_expr_map_.clear();
    node_func_map_.clear();
    decom_entry_.clear();
    decom_match_.clear();
    decom_glue_.clear();
    decom_else_.clear();
  }

  // ------------------------- METHODS -------------------------------------- //
  void PortInputs(const ilasynth::Abstraction& abs, const InstrLvlAbsPtr& ila);
  void PortStates(const ilasynth::Abstraction& abs, const InstrLvlAbsPtr& ila);
  void PortValid(const ilasynth::Abstraction& abs, const InstrLvlAbsPtr& ila);
  void PortFetch(const ilasynth::Abstraction& abs, const InstrLvlAbsPtr& ila);
  void PortInits(const ilasynth::Abstraction& abs, const InstrLvlAbsPtr& ila);
  void PortFuncs(const ilasynth::Abstraction& abs, const InstrLvlAbsPtr& ila);
  void PortInstructions(const ilasynth::Abstraction& abs,
                        const InstrLvlAbsPtr& ila);

  void DecomposeExpr(const ExprPtr& src);

  void CnvtNodeToExpr(const ilasynth::Node* n);
  void CnvtNodeToExprConst(const ilasynth::Node* n);
  void CnvtNodeToExprBoolOp(const ilasynth::Node* n);
  void CnvtNodeToExprBvOp(const ilasynth::Node* n);
  void CnvtNodeToExprMemOp(const ilasynth::Node* n);

}; // class SynthAbsConverter

typedef SynthAbsConverter::SynthAbsConverterPtr SynthAbsConverterPtr;

}; // namespace ilang

#endif // ILANG_TARGET_ITSY_ABST_TO_ILA_H__