source: Deliverables/D3.3/Cminor-experiment/initialisation.ma @ 830

Last change on this file since 830 was 830, checked in by campbell, 10 years ago

Move files that accidentally ended up in the root of the repository.

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.