Module MachIR

Require Mach.
Import Coqlib Maps.
Import AST Op Events.
Import Memory.
Import Values Integers.
Import Mach.
Import Machregs.
Import Annotations.

Notation "a ## b" := (List.map a b) (at level 1).

Definition node := positive.

Inductive instruction: Type :=
  | MIop: operation -> list mreg -> mreg -> node -> instruction
  | MIload: annotation -> memory_chunk -> addressing -> list mreg -> mreg -> node -> instruction
  | MIstore: annotation -> memory_chunk -> addressing -> list mreg -> mreg -> node -> instruction
  | MIbuiltin: external_function -> list (builtin_arg mreg) -> builtin_res mreg -> node -> instruction
  | MIgoto: node -> instruction
  | MIcond: condition -> list mreg -> node -> node -> instruction
  | MIcall: signature -> ident -> node -> instruction
  | MIgetparam: int -> typ -> mreg -> node -> instruction
  | MIreturn: instruction.

Definition code := PTree.t instruction.

Record function: Type := mkfunction
  { fn_sig: signature;
    fn_code: code;
    fn_entrypoint : node;
    fn_stackdata: Z;
    fn_stacksize: Z;
    fn_link_ofs: int;
    fn_retaddr_ofs: int }.

Definition fundef := AST.fundef function.

Definition program := AST.program fundef unit.

Definition funsig (fd: fundef) :=
  match fd with
  | Internal f => fn_sig f
  | External ef => ef_sig ef
  end.

Definition successors (i: instruction) : list node :=
  match i with
  | MIop _ _ _ s
  | MIload _ _ _ _ _ s
  | MIstore _ _ _ _ _ s
  | MIbuiltin _ _ _ s
  | MIgetparam _ _ _ s
  | MIcall _ _ s
  | MIgoto s => s :: nil
  | MIcond _ _ ifso ifnot => ifso :: ifnot :: nil
  | MIreturn => nil
  end.

Section RELSEM.

Variable ge: genv.
Variable f: function.
Variable sp: val.


Inductive state: Type :=
  | State:
      forall (pc: node)
             (rs: regset) (* register state *)
             (m: mem), (* memory state *)
      state.

Inductive step: state -> trace -> state -> Prop :=
  | exec_MIop:
      forall op args res rs m v pc pc',
      (fn_code f)!pc = Some (MIop op args res pc') ->
      eval_operation ge sp op rs##args m = Some v ->
      step (State pc rs m)
        E0 (State pc' (rs#res <- v) m)
  | exec_MIload:
      forall α chunk addr args dst rs m a v pc pc',
      (fn_code f)!pc = Some (MIload α chunk addr args dst pc') ->
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.loadv chunk m a = Some v ->
      step (State pc rs m)
        E0 (State pc' (rs#dst <- v) m)
  | exec_MIstore:
      forall α chunk addr args src rs m m' a pc pc',
      (fn_code f)!pc = Some (MIstore α chunk addr args src pc') ->
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.storev chunk m a (rs src) = Some m' ->
      step (State pc rs m)
        E0 (State pc' rs m')
  | exec_MIgoto:
      forall rs m pc pc',
      (fn_code f)!pc = Some (MIgoto pc') ->
      step (State pc rs m)
        E0 (State pc' rs m)
  | exec_MIcond_true:
      forall cond args rs m pc pc1 pc2,
      (fn_code f)!pc = Some (MIcond cond args pc1 pc2) ->
      eval_condition cond rs##args m = Some true ->
      step (State pc rs m)
        E0 (State pc1 rs m)
  | exec_MIcond_false:
      forall cond args rs m pc pc1 pc2,
      (fn_code f)!pc = Some (MIcond cond args pc1 pc2) ->
      eval_condition cond rs##args m = Some false ->
      step (State pc rs m)
        E0 (State pc2 rs m)
  | exec_MIreturn:
      forall rs m pc,
      (fn_code f)!pc = Some MIreturn ->
      step (State pc rs m)
        E0 (State pc rs m).

End RELSEM.


Definition find_pc_label (lbl: label) (f:Mach.function) : option node :=
  match find_label lbl (Mach.fn_code f) with
      | None => None
      | Some c => Some (Ppred (Pos.of_succ_nat (length c)))
  end.

Definition stack_annot f ofs : annotation :=
  let ofs := Int.sub ofs (Int.repr (Mach.fn_stackdata f)) in
  (xH, ABlocal O xH (ofs, ofs) :: nil).

Import Globalenvs.

Definition transl_instr (ge:Mach.genv) (f: Mach.function) (pc:node) (i: Mach.instruction) :=
  let pc' := Ppred pc in
  match i with
  | Mgetstack ofs ty dst => Some (MIload (stack_annot f ofs) (chunk_of_type ty) (Ainstack ofs) nil dst pc')
  | Msetstack src ofs ty => Some (MIstore (stack_annot f ofs) (chunk_of_type ty) (Ainstack ofs) nil src pc')
  | Mgetparam ofs ty dst => Some (MIgetparam ofs ty dst pc')
  | Mop op args res => Some (MIop op args res pc')
  | Mload α chunk addr args dst => Some (MIload α chunk addr args dst pc')
  | Mstore α chunk addr args src => Some (MIstore α chunk addr args src pc')
  | Mcall sg (inr f) => Some (MIcall sg f pc')
  | Mcall _ (inl _) => None
  | Mtailcall sig _ => None
  | Mlabel lbl => Some (MIgoto pc')
  | Mgoto lbl =>
    match find_pc_label lbl f with
      | None => None
      | Some pc_lbl => Some (MIgoto pc_lbl)
    end
  | Mcond cond args lbl =>
    match find_pc_label lbl f with
      | None => None
      | Some pc_lbl => Some (MIcond cond args pc_lbl pc')
    end
  | Mjumptable arg tbl => None
  | Mreturn => Some MIreturn
  | Mbuiltin ef args dst => Some (MIbuiltin ef args dst pc')
  end.

Fixpoint transl_fun_aux ge (f: Mach.function) (c:Mach.code)
: option (node * code) :=
  match c with
    | nil => Some (xH, PTree.empty _)
    | i::q =>
      match transl_fun_aux ge f q with
        | None => None
        | Some (pc,c') =>
          match transl_instr ge f pc i with
            | None => None
            | Some i' => Some (Psucc pc, PTree.set pc i' c')
          end
      end
  end.

Definition transl_fun ge (f: Mach.function) : option (node*code) :=
  transl_fun_aux ge f f.(Mach.fn_code) .

Definition checker (ge:Mach.genv) (f:Mach.function) : bool :=
  match Mach.fn_code f with
  | nil => false
  | code =>
  List.forallb
    (fun ins =>
       match ins with
         | Mach.Mcall _ (inl _)
         | Mach.Mtailcall _ _
         | Mach.Mjumptable _ _
           => false
         | Mach.Mgoto lbl
         | Mach.Mcond _ _ lbl =>
           match find_label lbl f.(Mach.fn_code) with
             | Some _ => true
             | None => false
           end
         | Mach.Mop _ _ _
         | Mach.Mload _ _ _ _ _
         | Mach.Mstore _ _ _ _ _
         | Mach.Mlabel _
         | Mach.Mcall _ (inr _)
         | Mach.Mgetparam _ _ _
         | Mach.Mreturn
         | Mach.Mgetstack _ _ _
         | Mach.Msetstack _ _ _
         | Mach.Mbuiltin _ _ _
           => true
       end)
    code
  end.

Import Errors.
Local Open Scope error_monad_scope.
Definition transl_function ge (f: Mach.function) : res function :=
  if checker ge f then
    match transl_fun ge f with
      | None => Errors.Error (Errors.MSG "MachIR conversion failed" :: nil)
      | Some (pc,c) =>
        Errors.OK {|
            fn_sig := f.(Mach.fn_sig);
            fn_code := c;
            fn_entrypoint := Ppred pc;
            fn_stackdata := f.(Mach.fn_stackdata);
            fn_stacksize := f.(Mach.fn_stacksize);
            fn_link_ofs := f.(Mach.fn_link_ofs);
            fn_retaddr_ofs := f.(Mach.fn_retaddr_ofs)
          |}
    end
  else Errors.Error (Errors.MSG "MachIR conversion failed : checker" :: nil).

Definition transl_fundef ge (fd: Mach.fundef) : res fundef :=
  match fd with
  | Internal fn => do fn' <- transl_function ge fn; OK (Internal fn')
  | External ef => OK (External ef)
  end.

Definition transl_program (p: Mach.program) : res program :=
  let ge := Genv.globalenv p in
  transform_partial_program (transl_fundef ge) p.