source: src/Cminor/initialisation.ma @ 880

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

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File size: 3.2 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 i)))
12| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
13| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst 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 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 → init_data → int (*offset?*) → stmt ≝
25λid,init,off.
26match init_expr init with
27[ None ⇒ St_skip
28| Some x ⇒
29    match x with [ dp chunk e ⇒
30      St_store ? chunk (Cst ? (Oaddrsymbol id off)) e
31    ]
32].
33
34definition init_var : ident → list init_data → stmt ≝
35λid,init.
36\snd (foldr ??
37  (λdatum,os.
38   let 〈off,s〉 ≝ os in
39     〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id datum off) s〉)
40  〈zero, St_skip〉 init).
41
42definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
43λvars. foldr ??
44  (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst (\fst 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_sig f)
58                                           (f_params f)
59                                           (f_vars f)
60                                           (f_ptrs f)
61                                           (f_stacksize f)
62                                           (St_seq s (f_body f)))〉
63          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
64          ]
65      | inr _ ⇒ 〈id',f'〉 ]).
66
67definition empty_vars : list (ident × (list init_data) × region × unit) →
68                        list (ident × (list init_data) × region × unit) ≝
69map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
70               [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
71              \snd (\fst v)〉,
72              \snd v〉).
73
74definition replace_init : Cminor_program → Cminor_program ≝
75λp.
76  mk_program ??
77    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
78    (prog_main ?? p)
79    (empty_vars (prog_vars ?? p)).
80   
Note: See TracBrowser for help on using the repository browser.