Library FminortoCminor_proof

Semantics preservation of the generation of Cminor Code



Author:Zaynah Dargaye

Created:29th April 2009

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.
Require Import Values.
Require Import Cmconstrproof.
Require Import Mem.
Require Import FminortoCminor.
Require Import Switch.
Require Import FminortoCminor_proof1.
Require Import Fminor_well.
Require Import FminortoCminor_proof2.
Require Import FminortoCminor_proof3.
I. Initialisation of inviariants

Definition block_kind_empty:= fun b:block =>
 if (zeq 0 b) then Some RB else (@None Bkind).

Lemma recup_In:
forall l fid d,
    recup_cfunct fid l = Some d -> In (fid,d) l .

Lemma gen_function_same_id:
 forall l,
 (map (fst (A:=ident) (B:=AST.fundef function))
     (map gen_function l)) =
  (map (fst (A:=ident) (B:=cfunction)) l).

Definition finit := fun b =>
 if (zeq b 0) then Some RB else
  if (Z_lt_dec b 0) then Some GB
   else None.

Axiom next_init_mem_program:
 forall p,
 nextblock (Genv.init_mem (gen_program p)) = 1.

Lemma mem_block_init:
 forall p,
 mem_block_kind (Genv.init_mem (gen_program p)) finit.



Lemma match_glo1 :
 forall p v ,
     ceval_prog p v ->
    well_bound_program p ->
  (forall fid d,
    recup_cfunct fid (cprog_funct p) = Some d ->
     exists b, exists f,
          Genv.find_symbol (Genv.globalenv (gen_program p)) fid = Some b/\
          Genv.find_funct (Genv.globalenv (gen_program p)) (Vptr b Int.zero)= Some f/\
          gen_function (fid,d)= (fid,f)/\
           ( finit b = Some GB)/\
          well_bound_func d)/\
  (exists bm, exists fm,
    fm =
    (Internal (mkfunction ( mksignature nil (Some Tint)) nil
                        (res::tmp_st::(cn_vars (cprog_main p) ))
                        (8+ (Z_of_nat (cn_stackspace
                      (cprog_main p) ))*4 +4)%Z
                      (Sseq (Sstore Mint32 (addrstack Int.zero) NULL)
                      (gen_term_tail (cn_body (cprog_main p)))
    ))) /\
   Genv.find_symbol (Genv.globalenv (gen_program p)) xH = Some bm /\
   Genv.find_funct (Genv.globalenv (gen_program p)) (Vptr bm Int.zero)=
   Some fm).


Axiom Eval_null:
 forall ge sp le e m ,
   eval_expr ge sp le e m NULL Eve m (Vptr 0 Int.zero).
II. Semantics preservation of a program transformation in Cminor
Theorem cminor_generation_correctness:
  forall p v
     (WB:well_bound_program p)
     (Ev: ceval_prog p v ),
  exists ff,
   exists mf,
        exists cv,
           exec_program (gen_program p) Eve (Vptr cv Int.zero)/\
           val_eqv (cprog_funct p) (Genv.globalenv (gen_program p))
                         ff mf v cv.