source: src/Cminor/initialisation.ma @ 1139

Last change on this file since 1139 was 1139, checked in by campbell, 8 years ago

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File size: 3.0 KB
Line 
1
2(* Replace initialisation of global variables with equivalent Cminor code. *)
3
4include "Cminor/syntax.ma".
5include "common/Globalenvs.ma".
6
7(* XXX having to specify the return type in the match is annoying. *)
8definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
9λinit.
10match 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
24definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝
25λid,r,init,off.
26match 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
34definition 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
42definition 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
46definition 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
66definition empty_vars : list (ident × region × (list init_data)) →
67                        list (ident × region × nat) ≝
68map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
69              size_init_data_list (\snd v)〉).
70
71definition replace_init : Cminor_program → Cminor_noinit_program ≝
72λp.
73  mk_program ??
74    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
75    (prog_main ?? p)
76    (empty_vars (prog_vars ?? p)).
77   
Note: See TracBrowser for help on using the repository browser.