| 1 | |
|---|
| 2 | (* Replace initialisation of global variables with equivalent Cminor code. *) |
|---|
| 3 | |
|---|
| 4 | include "Cminor/syntax.ma". |
|---|
| 5 | include "common/Globalenvs.ma". |
|---|
| 6 | |
|---|
| 7 | definition init_expr : init_data → option (memory_chunk × expr) ≝ |
|---|
| 8 | λinit. |
|---|
| 9 | match init with |
|---|
| 10 | [ Init_int8 i ⇒ Some ? 〈Mint8unsigned, Cst (Ointconst i)〉 |
|---|
| 11 | | Init_int16 i ⇒ Some ? 〈Mint16unsigned, Cst (Ointconst i)〉 |
|---|
| 12 | | Init_int32 i ⇒ Some ? 〈Mint32, Cst (Ointconst i)〉 |
|---|
| 13 | | Init_float32 f ⇒ Some ? 〈Mfloat32, Cst (Ofloatconst f)〉 |
|---|
| 14 | | Init_float64 f ⇒ Some ? 〈Mfloat64, Cst (Ofloatconst f)〉 |
|---|
| 15 | | Init_space n ⇒ None ? |
|---|
| 16 | | Init_null r ⇒ Some ? 〈Mpointer r, Op1 (Optrofint r) (Cst (Ointconst zero))〉 |
|---|
| 17 | | Init_addrof r id off ⇒ Some ? 〈Mpointer r, Cst (Oaddrsymbol id off)〉 |
|---|
| 18 | ]. |
|---|
| 19 | |
|---|
| 20 | (* Produces a few extra skips - hopefully the compiler will optimise these |
|---|
| 21 | away. *) |
|---|
| 22 | |
|---|
| 23 | definition init_datum : ident → init_data → int (*offset?*) → stmt ≝ |
|---|
| 24 | λid,init,off. |
|---|
| 25 | match init_expr init with |
|---|
| 26 | [ None ⇒ St_skip |
|---|
| 27 | | Some x ⇒ |
|---|
| 28 | let 〈chunk, e〉 ≝ x in |
|---|
| 29 | St_store chunk (Cst (Oaddrsymbol id off)) e |
|---|
| 30 | ]. |
|---|
| 31 | |
|---|
| 32 | definition init_var : ident → list init_data → stmt ≝ |
|---|
| 33 | λid,init. |
|---|
| 34 | \snd (foldr ?? |
|---|
| 35 | (λdatum,os. |
|---|
| 36 | let 〈off,s〉 ≝ os in |
|---|
| 37 | 〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id datum off) s〉) |
|---|
| 38 | 〈zero, St_skip〉 init). |
|---|
| 39 | |
|---|
| 40 | definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝ |
|---|
| 41 | λvars. foldr ?? |
|---|
| 42 | (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst (\fst var))))) St_skip vars. |
|---|
| 43 | |
|---|
| 44 | definition add_statement : ident → stmt → |
|---|
| 45 | list (ident × (fundef internal_function)) → |
|---|
| 46 | list (ident × (fundef internal_function)) ≝ |
|---|
| 47 | λid,s. |
|---|
| 48 | map ?? |
|---|
| 49 | (λidf. |
|---|
| 50 | let 〈id',f'〉 ≝ idf in |
|---|
| 51 | match ident_eq id id' with |
|---|
| 52 | [ inl _ ⇒ |
|---|
| 53 | match f' with |
|---|
| 54 | [ Internal f ⇒ 〈id, Internal ? (mk_internal_function |
|---|
| 55 | (f_sig f) |
|---|
| 56 | (f_params f) |
|---|
| 57 | (f_vars f) |
|---|
| 58 | (f_ptrs f) |
|---|
| 59 | (f_stacksize f) |
|---|
| 60 | (St_seq s (f_body f)))〉 |
|---|
| 61 | | External f ⇒ 〈id, External ? f〉 (* Error ? *) |
|---|
| 62 | ] |
|---|
| 63 | | inr _ ⇒ 〈id',f'〉 ]). |
|---|
| 64 | |
|---|
| 65 | definition empty_vars : list (ident × (list init_data) × region × unit) → |
|---|
| 66 | list (ident × (list init_data) × region × unit) ≝ |
|---|
| 67 | map ?? (λv. 〈〈〈\fst (\fst (\fst v)), |
|---|
| 68 | [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉, |
|---|
| 69 | \snd (\fst v)〉, |
|---|
| 70 | \snd v〉). |
|---|
| 71 | |
|---|
| 72 | definition replace_init : Cminor_program → Cminor_program ≝ |
|---|
| 73 | λp. |
|---|
| 74 | mk_program ?? |
|---|
| 75 | (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p)) |
|---|
| 76 | (prog_main ?? p) |
|---|
| 77 | (empty_vars (prog_vars ?? p)). |
|---|
| 78 | |
|---|
