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