Library FminortoCminor

Cminor code generation : last transformation of MLCompCert

Author : Zaynah Dargaye

Created:29th April 2009

Cminor is the first intermediate language of the back-end of CompCert.

Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Mml.
Require Import Mml_pre.
Require Import FSets.
Require Import FSetAVL.
Require Import Ordered.
Require Import Compare_dec.
Require Import EqNat.
Require Import Fminor.
Require Import Cminor.
Require Import Op.
Require Import Integers.
Require Import Cmconstr.

Variable NULL: expr.

I. Smart constructors
Definition addrsymbol (s:ident) := Eop (Oaddrsymbol s Enil.
Definition addrstack (n:int):= Eop (Oaddrstack n) Enil.
Definition intconst (n:Z):= Eop (Ointconst (Int.repr n)) Enil.
Definition addimm (e:expr) (n:Z) :=
 Eop Oadd ( e:::(intconst n):::Enil).
Definition slotaddr (n:nat):= Int.repr (8+(Z_of_nat n)*4).

Definition Sstore (c:memory_chunk) (e1 e2:expr) :=
 (Sexpr (store c e1 e2)).

Definition Scall (id:ident) (s:signature) (e:expr) (l:exprlist) :stmt:=
 Sassign id (Ecall s e l).

Fixpoint match_body (nb:nat):=
 match nb with
 | O => nil
 |S n => (Int.repr (Z_of_nat n) , n)::match_body n

Fixpoint fold_bl_rec (sl:list stmt) (e:stmt) (n:nat) {struct sl}:=
 match sl with | nil => (Sblock e)
 | a::m => fold_bl_rec m (Sseq (Sblock e) (Sseq a (Sexit n)))
         (minus n 1)

Definition folding_blocks (sl:list stmt) (e:stmt):=
    fold_bl_rec sl e ((length sl)-1).

Definition Smatch (e:expr) (sl:list stmt):stmt:=
 let nb:= ( length sl ) in
 folding_blocks sl (Sswitch e (match_body nb) nb ) .

Fixpoint gen_fill_block (dst:ident) (ofs:Z) (al:exprlist )
 {struct al}: stmt:=
 match al with
 | Enil => Sskip
 | ca:::l =>
     (Sseq (Sstore Mint32 (addimm (Evar dst) ofs) ca)
                  (gen_fill_block dst (ofs+4) l ) )

Definition gen_call_signature (A:Set) (l:list A) :=
  mksignature( Tint ::Tint (fun _ => Tint) l) (Some Tint).

Definition alloc_block_signature:=
   mksignature (Tint::Tint::Tint::nil) (Some Tint).

Definition mkmatch (e:expr) (cases: list stmt) :stmt:=
  match cases with
  | s::nil => s
  | s0::s1::nil => Sifthenelse ( condexpr_of_expr e) s1 s0
  | _ => Smatch e cases

Definition Store_stack (n:nat) (a:expr):=
  (Sstore Mint32 (addrstack (slotaddr n)) a).

Definition Store_stsize (z:Z):=
  (Sstore Mint32 (addrstack (Int.repr 4)) (intconst z)).

Definition alloc_call (id:ident) (n:nat):=
 Scall id alloc_block_signature (addrsymbol alloc_block)
        ( (addrstack 2):::
           (intconst (Z_of_nat n)):::Enil).

Definition bind (A B: Set) (f: option A) (g: A -> option B) :=
  match f with None => None | Some x => g x end.

Implicit Arguments bind [A B].

Notation "'do' X <- A ; B" := (bind A (fun X => B))
   (at level 200, X ident, A at level 100, B at level 200).

II. Atoms transformation
Fixpoint gen_atom (a:catom) {struct a}:=
 match a with
 | Cvar x => Evar x
 | Cfield n a1 =>
     let ca1:=gen_atom a1 in
     ( match n with
      | O => load Mint32 ca1
      | S k => load Mint32 (addimm ca1 ((Z_of_nat n)*4))
 | Cslot n =>
        (load Mint32 (addrstack (slotaddr n)))

Fixpoint gen_atomlist (l:list catom):=
 match l with | nil => Enil | a::m => gen_atom a ::: gen_atomlist m

Definition gen_bind_var (p:Param) (a:expr) :=
 match p with
 | VR id => (Sassign id a)
 | SL pos => (Store_stack pos a)

Fixpoint gen_bind_vars (a:expr) (ofs:Z)
 (vars:list Param) {struct vars}: stmt:=
 match vars with
 | nil => Sskip
 | va::rs =>
      let d:= gen_bind_var va (load Mint32 (addimm a ofs)) in
      let dl:= gen_bind_vars a (ofs+4) rs in
        (Sseq d dl)

Definition mk_closure (id:ident) (fid:ident) (z:Z) (size:nat) (l:exprlist):=
 ((Sseq (Store_stsize z)
                (Sseq (alloc_call id size)
                    (Sseq (Sstore Mint32 (Evar id) (addrsymbol fid))
                              (gen_fill_block id 4 l))))) .

Definition mk_constr (id: ident )(cstr:nat) (z:Z) (size:nat) (l:exprlist):=
(Sseq (Store_stsize z)
  (Sseq (alloc_call id size)
     (Sseq (Sstore Mint32 (Evar id) (intconst (Z_of_nat cstr)))
        (gen_fill_block id 4 l)))).

III. Transformation of a term which is not in tail position
Fixpoint gen_term (dst:ident) (f:Cterm) {struct f}:=
 match f with
 | Catom a => (Sassign dst (gen_atom a) )
 | Capp fid af al z =>
      let ca:= gen_atom af in
      (Sseq (Store_stsize (Z_of_nat z))
                (Scall dst ((gen_call_signature catom al))
        (match fid with | None => load Mint32 ca
                                   | Some id => addrsymbol id end)
        ( (addrstack (gen_atomlist al)) )
 |Clet id f1 f2 =>
     (Sseq (gen_term id f1) (gen_term dst f2))
 | Cpush n f1 f2 =>
     (Sseq ( Sseq (gen_term tmp_st f1 )
          (Store_stack n (Evar tmp_st))) (gen_term dst f2 ) )
 |Cmatch a pl =>
     let ca:= (gen_atom a) in
     (mkmatch (load Mint32 ca)
      ( (fun x => gen_pat dst x ca ) pl ))
  |Cclos fid al z=>
     (mk_closure dst fid (Z_of_nat z) (S (length al)) (gen_atomlist al))
 |Ccon n al z=>
    ( mk_constr dst n (Z_of_nat z) (S (length al)) (gen_atomlist al))
 with gen_pat (dst :ident) (p:cpat) (e:expr) {struct p}:=
 match p with |CPatc xl f =>
        let defs:= gen_bind_vars (Evar res) 4 xl in
    (Sseq (Sseq (Sassign res e) defs) (gen_term dst f))

IV. Transformation of term in tail position
Fixpoint gen_term_tail (f:Cterm) {struct f}:=
 match f with
 | Catom a => Sreturn (Some (gen_atom a) )
 | Capp fid af al z =>
      let ca := gen_atom af in
      (Stailcall (gen_call_signature catom al))
        (match fid with | None => load Mint32 ca
                                   | Some id => addrsymbol id end)
        ( (load Mint32 (addrstack al)
 |Clet id f1 f2 =>
      Sseq (gen_term id f1 ) (gen_term_tail f2 )
 | Cpush n f1 f2 =>
      ( Sseq (Sseq (gen_term tmp_st f1 )
                (Store_stack n (Evar tmp_st))) (gen_term_tail f2 ))
  |Cmatch a pl =>
      let ca:= gen_atom a in
      mkmatch (load Mint32 ca)
         ( (fun x => gen_pat_tail x ca) pl)
  |Cclos fid al z=>
     (Sseq ( mk_closure res fid (Z_of_nat z) (S (length al)) (gen_atomlist al))
                               ( Sreturn (Some (Evar res))))
 |Ccon n al z =>
      (Sseq (mk_constr res n (Z_of_nat z) (S (length al)) (gen_atomlist al))
                               ( Sreturn (Some (Evar res))))
 with gen_pat_tail (p:cpat) (e:expr) {struct p}:=
 match p with |CPatc xl f =>
     let defs := gen_bind_vars (Evar res) 4 xl in
    (Sseq (Sseq (Sassign res e) defs) (gen_term_tail f))

Definition gen_fun_signature (A:Set) (l:list A) :=
  mksignature( (fun _ => Tint) l) (Some Tint).

Definition gen_function
    (id_f: ident*cfunction): (ident * AST.fundef function):=
  let (id,f):= id_f in
  let cpar:= (cn_params f) in
  let q:= (8+ (Z_of_nat (cn_stackspace f) )*4 +4)%Z in
  (id ,(Internal(
      mkfunction (gen_fun_signature ident cpar)
                            ( Roots::cpar ) (res::tmp_st::(cn_vars f)) q
        (Sseq (Sstore Mint32 (addrstack (Evar Roots))
                   (gen_term_tail (cn_body f) ) )))) .

Definition gen_program (fp:cprogram):=
  let qmain:= (8+ (Z_of_nat (cn_stackspace
                      (cprog_main fp) ))*4 +4)%Z in
 let cmain:= (xH,
    (Internal (mkfunction ( mksignature nil (Some Tint)) nil
                        (res::tmp_st::(cn_vars (cprog_main fp) )) qmain
 (Sseq (Sstore Mint32 (addrstack NULL)
             (gen_term_tail (cn_body (cprog_main fp))))
  )) ) in
     (cmain::( gen_function (cprog_funct fp)))
            (@nil(ident * list init_data * unit) )).