Library front_main

The MLCompCert front-end and its proof of semantic preservation

Author:Zaynah Dargaye

Created:29th April 2009

Libraries.


Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Values.

Require Import Integers.

Require Import Globalenvs.

Languages (syntax and semantics).


Require Import Cml.

Require Import Pml.

Require Import Nml.

Require Import Fml.

Require Import Dml.

Require Import Fminor.

Require Import Cminor.

Translation passes.


Require Import c2p.

Require Import p2n.

Require Import n2f.

Require Import f2d.

Require Import d2m.

Require Import Mml_pre.

Require Import M2Fminor.

Require Import FminortoCminor.

Proofs of semantic preservation


Require Import c2pp_pre.

Require Import c2pp.

Require Import p2np.

Require Import n2fp.

Require Import f2dp.

Require Import d2mp.

Require Import M2Fminor_proof.

Require Import Fminor_well.

Require Import FminortoCminor_proof1.

Require Import FminortoCminor_proof2.

Require Import FminortoCminor_proof3.

Require Import FminortoCminor_proof.




Definition Cml2Cminor (p:Cml.program):=

 match (c2p.trad_prg p) with 

 | None => None 

 | Some pp => 

      match  (f2d.transf_program (n2f.trans (p2n.trad pp nil))) with

      | None => None 

      | Some dp => 

          match (germ_cprogram (d2m.transl_prog dp)) with 

          | None =>None

          | Some fp => Some (gen_program fp)

          end

      end

 end.




Definition match_final_val  (v:Cval) (cv:block)

   (g:gamma) (l:list (ident*def)) 

    (l2:list (ident * Mml.funct))

     (l3:list (ident * cfunction))

      (ge:genv)  (ff:block_kind) (m:Mem.mem) :Prop:=

 exists pv, 

   exists nv, 

     exists fv,

       exists dv,

         exists mv,

           exists fmv,

         c2pp.match_val g v pv /\ p2np.match_val pv nv /\

         n2fp.match_val nv fv /\ f2dp.match_val l fv dv/\ 

         d2mp.match_val l dv mv/\

          M2Fminor_proof.match_val l2 l3 mv fmv /\ 

          val_eqv l3 ge ff  m fmv cv.




Theorem Cml2Cminor_correctness: 

 forall  fp fv cp

 (E: Cml.eval_prog fp fv)

 (T: Cml2Cminor fp = Some cp), 

  exists g:gamma, 

    exists l: list (ident*def), 

      exists l2:list (ident * Mml.funct), 

        exists l3: list (ident * cfunction),

          exists ff:block_kind, 

            exists mf:Mem.mem,  

           exists cv:block, 

           exec_program cp Eve (Vptr cv Int.zero)/\ 

           match_final_val fv cv 

                  g l l2 l3 (Genv.globalenv cp) ff mf.