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 Int.zero) 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
end.
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)
end.
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 ) )
end.
Definition gen_call_signature (A:Set) (l:list A) :=
mksignature( Tint ::Tint ::List.map (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
end.
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 Int.zero):::(intconst 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))
end)
| Cslot n =>
(load Mint32 (addrstack (slotaddr n)))
end.
Fixpoint gen_atomlist (l:list catom):=
match l with | nil => Enil | a::m => gen_atom a ::: gen_atomlist m
end.
Definition gen_bind_var (p:Param) (a:expr) :=
match p with
| VR id => (Sassign id a)
| SL pos => (Store_stack pos a)
end.
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)
end.
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 Int.zero):::ca::: (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)
(List.map (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))
end
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))
end.
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 Int.zero)):::ca:::gen_atomlist 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)
(List.map (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))))
end
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))
end.
Definition gen_fun_signature (A:Set) (l:list A) :=
mksignature( Tint::List.map (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 Int.zero) (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 Int.zero) NULL)
(gen_term_tail (cn_body (cprog_main fp))))
)) ) in
(mkprogram
(cmain::(List.map gen_function (cprog_funct fp)))
xH
(@nil(ident * list init_data * unit) )).