source: src/Cminor/initialisation.ma @ 1224

Last change on this file since 1224 was 1224, checked in by sacerdot, 8 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

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    (empty_vars (prog_vars ?? p))
75    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
76    (prog_main ?? p).
Note: See TracBrowser for help on using the repository browser.