coqemitter.h

// This file if part of the llir-opt project.
// Licensing information can be found in the LICENSE file.
// (C) 2018 Nandor Licker. All rights reserved.
 
#pragma once
 
#include <llvm/Support/raw_ostream.h>
 
#include "core/block.h"
 
class Prog;
class Func;
 
 
 
class CoqEmitter final {
public:
  CoqEmitter(llvm::raw_ostream &os);
 
  void Write(const Prog &prog);
 
private:
  void WriteDefinition(const Func &func);
  void Write(Block::const_iterator it);
  void Unary(Block::const_iterator it, const char *op);
  void Binary(Block::const_iterator it, const char *op);
  void Mov(Block::const_iterator it);
  template<unsigned Bits>
  void MovInt(Block::const_iterator it, const char *op, const APInt &val);
 
  void WriteInversion(const Func &func);
  void WriteDefinedAtInversion(const Func &func);
  void WriteUsedAtInversion(const Func &func);
  void WriteBlocks(const Func &func);
  void WriteDominators(const Func &func);
 
  void WriteUsesHaveDefs(const Func &func);
  void WriteDefsAreUniqe(const Func &func);
  void WriteWellTyped(const Func &func);
 
  void Write(Type ty);
 
  std::string Name(const Func &func);
 
private:
  struct AtomID {
    unsigned Segment;
    unsigned Object;
    unsigned Offset;
  };
  std::unordered_map<const Atom *, AtomID> atoms_;
 
  std::unordered_map<const Func *, unsigned> funcs_;
  std::unordered_map<const Block *, unsigned> blocks_;
  std::unordered_map<ConstRef<Inst>, unsigned> insts_;
  llvm::raw_ostream &os_;
  bool admitted_;
};