Module RTLinjectgen

Require Import
  Utf8 Coqlib Maps
  Integers Registers.

Require Import
  Utils Common DataStructures
  InjectedCode INJECT GCthread
  MIR RTLinject Transcode.

Section RTLINJECTGEN.

Local Notation node := positive (only parsing).

Variable bi : backend_info.
Variable om : object_model.
Variable p : MIR.program.

Definition translate_sig (s : MIR.signature) : Ast.signature :=
  let args := List.map (fun _ => Ast.Tint) s.(sig_args)
    in
    Ast.mksignature
    (if s.(sig_ext) then args else Ast.Tint :: args)
    (Some Ast.Tint).

Section TRINSTR.

  Variables (gv: PTree.t Z)
            (ep: node) (nd: node) (roots: N)
            (md: reg) (tmp1 tmp2: reg).

Definition gvi_of_type (ty: field_type) : Ast.ident :=
  match ty with
    | FPointer => bi.(bi_ptr_globals)
    | FInteger => bi.(bi_int_globals)
  end.

Definition translate_instruction (i: MIR.instruction) : mon unit :=
  match i with
    | Mnop succ => update_instr nd
      (if peq ep nd
       then if roots
            then Inop succ
            else Iinject (prologue_code roots) (md::nil) nil succ
       else if plt nd succ
            then Inop succ
            else Iinject (cooperate_code bi) (md::nil) nil succ)
    | Mop dst (OpIntConst cst) args succ => update_instr nd (Iop (Op.Ointconst cst) args dst succ)
    | Mop dst OpAdd args succ => update_instr nd (Iop (Op.Olea (Op.Aindexed2 Int.zero)) args dst succ)
    | Mop dst OpNull args succ => update_instr nd (Iop (Op.Ointconst Int.zero) args dst succ)
    | Mop dst OpNeg args succ => update_instr nd (Iop Op.Oneg args dst succ)
    | Mop dst (OpShri i) args succ => update_instr nd (Iop (Op.Oshrimm i) args dst succ)
    | Mop dst OpMov (src::nil) succ => update_instr nd
       (if is_ptr_reg roots dst
       then Iinject (saveref_code dst) (src::nil) (dst::nil) succ
       else Iop Op.Omove (src::nil) dst succ)
    | Mop _ OpMov _ succ => error (Errors.msg "Ill-typed move")
    | Mif cmp args if_so if_not => update_instr nd (Icond cmp args if_so if_not)
    | Mget dst src fld succ => update_instr nd (Iinject (read_code (slot_of_reg dst) fld)
                                                        (src::nil) (dst::nil) succ)
    | Mput dst fld src succ => update_instr nd (Iinject (write_code bi fld)
                                                        (md::dst::src::nil) nil succ)
    | Mget_global dst src succ =>
        match p.(prog_vars) ! src, gv ! src with
            | Some (k, ty), Some adr => update_instr nd
               (Iinject (read_global_code (gvi_of_type ty) adr k) nil (dst::nil) succ)
            | _, _ => error (Errors.msg "Wrong global variable identifier")
        end
    | Mput_global dst src succ =>
        match p.(prog_vars) ! dst, gv ! dst with
            | Some (k, ty), Some adr => update_instr nd
                (Iinject (write_global_code (gvi_of_type ty) adr k) (src::nil) nil succ)
            | _, _ => error (Errors.msg "Wrong global variable identifier")
        end
    | Mnew dst hdr succ => update_instr nd
        (Iinject (new_code bi (slot_of_reg dst) hdr) (md::nil) (dst::nil) succ)
    | Mfence succ => update_instr nd
        (Iinject (Make_IC (Sfence false) (Satomic true (Sreturn nil)) nil) nil nil succ)
    | Mspawn sg func param succ =>
        do n <- add_instr (Ithreadcreate tmp1 tmp2 succ);
        update_instr nd (Iinject (spawn_code bi func) (param::nil) (tmp1::tmp2::nil) n)
    | Mlock mn succ => update_instr nd (Iinject lock_code (mn::nil) nil succ)
    | Munlock mn succ => update_instr nd (Iinject unlock_code (mn::nil) nil succ)

    | Mcall dst sg func args succ =>
        do n <- match sg.(sig_res) with
                  | FInteger => ret succ
                  | FPointer => add_instr (Iinject (saveref_code dst) (dst::nil) (tmp1::nil) succ)
                end;
        do n' <- add_instr (Icall (translate_sig sg) (inr _ func)
                                  (if sg.(sig_ext) then args else md::args) dst n);
        update_instr nd (Iinject (cooperate_code bi) (md::nil) nil n')

   | Mret res =>
     if roots
     then update_instr nd (Ireturn res)
     else do n <- add_instr (Ireturn res);
          update_instr nd (Iinject epilogue_code (md::nil) nil n)

  end.

End TRINSTR.

Definition translate_fun gv (f: MIR.fundef) : Errors.res RTLinject.fundef :=
  match f with
    | Ast.External e => Errors.OK (Ast.External e)
    | Ast.Internal i =>
      match i.(MIR.fn_code) ! (i.(MIR.fn_entrypoint)) with
        | Some (Mnop _) =>
          let arg0 : reg := fresh_register i.(MIR.fn_code) in
          let dummy : reg := Psucc arg0 in
          let dummy' : reg := Psucc dummy in
          let is : state := init_state (Psucc (max_key i.(MIR.fn_code))) in
          match
          PTree.fold
            (fun m k j => do _ <- m;
             translate_instruction gv i.(MIR.fn_entrypoint) k i.(MIR.fn_roots) arg0
               dummy dummy' j)
            i.(MIR.fn_code)
            (ret tt)
            is
            with
              | OK _ st _ =>
                  Errors.OK
                  (Ast.Internal (RTLinject.mkfunction
                     (translate_sig i.(MIR.fn_sig))
                     (arg0 :: i.(MIR.fn_params))
                     (match i.(fn_roots) with
                          | N0 => Int.zero
                          | Npos r => Int.repr ((Zpos r + 2) * 4)
                      end)
                     st.(st_code)
                     i.(MIR.fn_entrypoint)))
              | Error msg => Errors.Error msg
          end
        | _ => Errors.Error (Errors.msg "No nop at function entry")
      end
  end.

Definition translate_global (gv: PTree.t (field_kind * field_type))
  : (PTree.t Z * Z * Z)%type :=
  PTree.fold (A := field_kind * field_type) (B := PTree.t Z * Z * Z)
       (fun acc v kt =>
          let '(aloc, max_p, max_i) := acc in
          let '(k, t) := kt in
            match t with
              | FPointer => (aloc ! v <- max_p, max_p + 4, max_i)
              | FInteger => (aloc ! v <- max_i, max_p, max_i + 4)
            end
       )
       gv
       (PTree.empty _, 0, 0)
  .

Definition transf_program : Errors.res RTLinject.program :=
  let '(gv, max_p, max_i) := translate_global p.(prog_vars) in
  Errors.bind
    (Ast.map_partial Ast.prefix_funct_name (translate_fun gv)
        (PTree.elements p.(MIR.prog_funct)))
    (fun fl =>
       Errors.OK
      (Ast.mkprogram
          ( (bi.(bi_thread_main), Ast.Internal (thread_main_func bi))
          ::(bi.(bi_main), Ast.Internal (gc_main_func bi om p max_p))
          ::(bi.(bi_abort), Ast.External (Ast.mkextfun bi.(bi_abort) (Ast.mksignature (Ast.Tint::nil) None)))
          ::fl)
          bi.(bi_main)
          ( (bi.(bi_mutator_lock), Ast.Init_space 4::nil, tt)
          ::(bi.(bi_free_list), Ast.Init_space 4::nil, tt)
          ::(bi.(bi_mutator_data), Ast.Init_space (Int.unsigned (md_size bi))::nil, tt)
          ::(bi.(bi_heap), Ast.Init_space (Int.unsigned (heap_byte_size om))::nil, tt)
          ::(bi.(bi_collector), Ast.Init_space (Int.unsigned sizeof_cd)::nil, tt)
          ::(bi.(bi_collector_stack), Ast.Init_space (Int.unsigned bi.(bi_collector_stack_size))::nil, tt)
          ::(bi.(bi_ptr_globals), Ast.Init_space max_p::nil, tt)
          ::(bi.(bi_int_globals), Ast.Init_space max_i::nil, tt)
          ::nil)
       )).

End RTLINJECTGEN.