source: src/Cminor/initialisation.ma @ 1383

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

Put type information into front-end unary ops.
Slight change to semantics: booleans produced by Onotbool can be any given
integer size.

File size: 4.4 KB
Line 
1
2(* Replace initialisation of global variables with equivalent Cminor code. *)
3
4include "Cminor/syntax.ma".
5include "common/Globalenvs.ma".
6include "utilities/pair.ma".
7include "utilities/deppair.ma".
8
9(* XXX having to specify the return type in the match is annoying. *)
10definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
11λinit.
12match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
13[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
14| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
15| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
16| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
17| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
18| Init_space n         ⇒ None ?
19| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
20| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
21].
22
23(* None of the additional code introduces locals or labels. *)
24definition stmt_inv : stmt → Prop ≝
25  stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
26
27(* Produces a few extra skips - hopefully the compiler will optimise these
28   away. *)
29
30definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝
31λid,r,init,off.
32match init_expr init with
33[ None ⇒ St_skip
34| Some x ⇒
35    match x with [ dp chunk e ⇒
36      St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
37    ]
38].
39% //
40cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
41qed.
42
43definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
44λid,r,init.
45\snd (foldr ??
46  (λdatum,os.
47   let 〈off,s〉 ≝ os in
48     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
49  〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init).
50[ % //
51| elim init
52  [ % //
53  | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
54] qed.
55
56definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
57λvars. foldr ? (Σs:stmt. stmt_inv s)
58  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
59% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
60qed.
61
62lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
63#s elim s //
64[ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
65  >(IH1 H1) >(IH2 H2) @refl
66| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
67  >(IH1 H1) >(IH2 H2) @refl
68| #s #IH * * #_ #_ #H @(IH H)
69| #s #IH * * #_ #_ #H @(IH H)
70| #l #s #IH * * #_ *
71| #l #s #IH * * #_ #_ #H @(IH H)
72] qed.
73
74definition add_statement : ident → (Σs:stmt. stmt_inv s) →
75                              list (ident × (fundef internal_function)) →
76                              list (ident × (fundef internal_function)) ≝
77λid,s. match s with [ dp s H ⇒
78  map ??
79    (λidf.
80      let 〈id',f'〉 ≝ idf in
81      match ident_eq id id' with
82      [ inl _ ⇒
83          match f' with
84          [ Internal f ⇒ 〈id, Internal ? (mk_internal_function
85                                           (f_return f)
86                                           (f_params f)
87                                           (f_vars f)
88                                           (f_stacksize f)
89                                           (St_seq s (f_body f))
90                                           ?)〉
91          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
92          ]
93      | inr _ ⇒ 〈id',f'〉 ]) ].
94%
95[ % [ % // |
96  @(stmt_P_mp … H) #s * #V #L %
97  [ @(stmt_vars_mp … V) #i *
98  | @(stmt_labels_mp … L) #l *
99  ]
100  ]
101| whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f)
102] qed.
103
104definition empty_vars : list (ident × region × (list init_data)) →
105                        list (ident × region × nat) ≝
106map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
107              size_init_data_list (\snd v)〉).
108
109definition replace_init : Cminor_program → Cminor_noinit_program ≝
110λp.
111  mk_program ??
112    (empty_vars (prog_vars ?? p))
113    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
114    (prog_main ?? p).
Note: See TracBrowser for help on using the repository browser.