(* Replace initialisation of global variables with equivalent Cminor code. *) include "Cminor/syntax.ma". include "common/Globalenvs.ma". include "utilities/pair.ma". include "utilities/deppair.ma". (* XXX having to specify the return type in the match is annoying. *) definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝ λinit. match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with [ Init_int8 i ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i))) | Init_int16 i ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i))) | Init_int32 i ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i))) | Init_float32 f ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f))) | Init_float64 f ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f))) | Init_space n ⇒ None ? | Init_null r ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?))))) | Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off))) ]. (* None of the additional code introduces locals or labels. *) definition stmt_inv : stmt → Prop ≝ stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s). discriminator option. discriminator Sig. (* Produces a few extra skips - hopefully the compiler will optimise these away. *) definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝ λid,r,init,off. match init_expr init with [ None ⇒ St_skip | Some x ⇒ match x with [ dp chunk e ⇒ St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e ] ]. % // cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct;/2/ qed. definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝ λid,r,init. \snd (foldr ?? (λdatum,os. let 〈off,s〉 ≝ os in 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init). [ % // | elim init [ % // | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ] ] qed. definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝ λvars. foldr ? (Σs:stmt. stmt_inv s) (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars. % [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ] qed. lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. #s elim s // [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) >(IH1 H1) >(IH2 H2) @refl | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?) >(IH1 H1) >(IH2 H2) @refl | #s #IH * * #_ #_ #H @(IH H) | #s #IH * * #_ #_ #H @(IH H) | #l #s #IH * * #_ * | #l #s #IH * * #_ #_ #H @(IH H) ] qed. definition add_statement : ident → (Σs:stmt. stmt_inv s) → list (ident × (fundef internal_function)) → list (ident × (fundef internal_function)) ≝ λid,s. match s with [ dp s H ⇒ map ?? (λidf. let 〈id',f'〉 ≝ idf in match ident_eq id id' with [ inl _ ⇒ match f' with [ Internal f ⇒ 〈id, Internal ? (mk_internal_function (f_return f) (f_params f) (f_vars f) (f_stacksize f) (St_seq s (f_body f)) ?)〉 | External f ⇒ 〈id, External ? f〉 (* Error ? *) ] | inr _ ⇒ 〈id',f'〉 ]) ]. % [ % [ % // | @(stmt_P_mp … H) #s * #V #L % [ @(stmt_vars_mp … V) #i * | @(stmt_labels_mp … L) #l * ] ] | whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f) ] qed. definition empty_vars : list (ident × region × (list init_data)) → list (ident × region × nat) ≝ map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉, size_init_data_list (\snd v)〉). definition replace_init : Cminor_program → Cminor_noinit_program ≝ λp. mk_program ?? (empty_vars (prog_vars ?? p)) (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p)) (prog_main ?? p).