source: src/Cminor/initialisation.ma @ 758

Last change on this file since 758 was 758, checked in by campbell, 9 years ago

Implement replacement of global var initialisation data by code in Cminor.

File size: 2.9 KB
Line 
1
2(* Replace initialisation of global variables with equivalent Cminor code. *)
3
4include "Cminor/syntax.ma".
5include "common/Globalenvs.ma".
6
7definition init_expr : init_data → option (memory_chunk × expr) ≝
8λinit.
9match 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
23definition init_datum : ident → init_data → int (*offset?*) → stmt ≝
24λid,init,off.
25match 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
32definition 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
40definition 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
44definition 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
65definition empty_vars : list (ident × (list init_data) × region × unit) →
66                        list (ident × (list init_data) × region × unit) ≝
67map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
68               [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
69              \snd (\fst v)〉,
70              \snd v〉).
71
72definition 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   
Note: See TracBrowser for help on using the repository browser.