1 | |
---|
2 | (* Replace initialisation of global variables with equivalent Cminor code. *) |
---|
3 | |
---|
4 | include "Cminor/Cminor_syntax.ma". |
---|
5 | include "common/Globalenvs.ma". |
---|
6 | |
---|
7 | (* XXX having to specify the return type in the match is annoying. *) |
---|
8 | definition init_expr : init_data → option (𝚺t:typ. expr t) ≝ |
---|
9 | λinit. |
---|
10 | match init return λ_.option (𝚺t:typ. expr t) with |
---|
11 | [ Init_int8 i ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 Unsigned i))) |
---|
12 | | Init_int16 i ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 Unsigned i))) |
---|
13 | | Init_int32 i ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 Unsigned i))) |
---|
14 | (*| Init_float32 f ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))*) |
---|
15 | | Init_float64 f ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))*)*) |
---|
16 | | Init_space n ⇒ None ? |
---|
17 | | Init_null ⇒ Some ? (mk_DPair ?? ASTptr (Op1 (ASTint I8 Unsigned) ? (Optrofint ??) (Cst ? (Ointconst I8 Unsigned (zero ?))))) |
---|
18 | | Init_addrof id off ⇒ Some ? (mk_DPair ?? ASTptr (Cst ? (Oaddrsymbol id off))) |
---|
19 | ]. |
---|
20 | |
---|
21 | (* None of the additional code introduces locals, labels or returns. *) |
---|
22 | definition stmt_inv : stmt → Prop ≝ |
---|
23 | stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ∧ match s with [ St_return _ ⇒ False | _ ⇒ True ]). |
---|
24 | |
---|
25 | discriminator option. |
---|
26 | discriminator DPair. |
---|
27 | |
---|
28 | (* Produces a few extra skips - hopefully the compiler will optimise these |
---|
29 | away. *) |
---|
30 | |
---|
31 | definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝ |
---|
32 | λid,r,init,off. |
---|
33 | match init_expr init with |
---|
34 | [ None ⇒ St_skip |
---|
35 | | Some x ⇒ |
---|
36 | match x with [ mk_DPair t e ⇒ |
---|
37 | St_store t (Cst ? (Oaddrsymbol id off)) e |
---|
38 | ] |
---|
39 | ]. |
---|
40 | % /3/ |
---|
41 | cases init in p; [ 5: | 6: #a #b | *: #a ] #p normalize in p; |
---|
42 | destruct;/4 by stmt_labels_mp, conj/ |
---|
43 | qed. |
---|
44 | |
---|
45 | definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝ |
---|
46 | λid,r,init. |
---|
47 | \snd (foldl ?? |
---|
48 | (λos,datum. |
---|
49 | let 〈off,s〉 ≝ os in |
---|
50 | 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) |
---|
51 | 〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init). |
---|
52 | [ % /3/ |
---|
53 | | cut (stmt_inv St_skip) [ % /3/ ] |
---|
54 | generalize in match St_skip; |
---|
55 | generalize in match 0; |
---|
56 | elim init |
---|
57 | [ #off #s #H @H |
---|
58 | | #h #t #IH #off #s #H whd in ⊢ (?(???%)); @breakup_pair @IH |
---|
59 | % |
---|
60 | [ /3/ |
---|
61 | | % [ @(pi2 … (init_datum …)) | @H ] |
---|
62 | ] |
---|
63 | ] |
---|
64 | ] qed. |
---|
65 | |
---|
66 | definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝ |
---|
67 | λvars. foldr ? (Σs:stmt. stmt_inv s) |
---|
68 | (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip ?) vars. |
---|
69 | [ % [ /3/ | % [ @(pi2 … s) | @(pi2 … (init_var …)) ] ] |
---|
70 | | /4/ |
---|
71 | ] qed. |
---|
72 | |
---|
73 | lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ]. |
---|
74 | #s elim s // |
---|
75 | [ #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?); |
---|
76 | >(IH1 H1) >(IH2 H2) @refl |
---|
77 | | #sz #sg #e #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?); |
---|
78 | >(IH1 H1) >(IH2 H2) @refl |
---|
79 | | #l #s #IH * * * #_ * |
---|
80 | | #l #s #IH * #_ #H @(IH H) |
---|
81 | ] qed. |
---|
82 | |
---|
83 | (* FIXME: we need to add a new initialisation function instead of augmenting |
---|
84 | main, because this currently breaks a recursive main function. *) |
---|
85 | |
---|
86 | definition add_statement : costlabel → ident → (Σs:stmt. stmt_inv s) → |
---|
87 | list (ident × (fundef internal_function)) → |
---|
88 | list (ident × (fundef internal_function)) ≝ |
---|
89 | λcost,id,s. match s with [ mk_Sig s H ⇒ |
---|
90 | map ?? |
---|
91 | (λidf. |
---|
92 | let 〈id',f'〉 ≝ idf in |
---|
93 | match ident_eq id id' with |
---|
94 | [ inl _ ⇒ |
---|
95 | match f' with |
---|
96 | [ Internal f ⇒ 〈id, Internal ? (mk_internal_function |
---|
97 | (f_return f) |
---|
98 | (f_params f) |
---|
99 | (f_vars f) |
---|
100 | (f_distinct f) |
---|
101 | (f_stacksize f) |
---|
102 | (St_cost cost (St_seq s (f_body f))) |
---|
103 | ?)〉 |
---|
104 | | External f ⇒ 〈id, External ? f〉 (* Error ? *) |
---|
105 | ] |
---|
106 | | inr _ ⇒ 〈id',f'〉 ]) ]. |
---|
107 | % |
---|
108 | [ % // |
---|
109 | | % |
---|
110 | [ % // |
---|
111 | | % [ @(stmt_P_mp … H) #s * * #V #L #R % |
---|
112 | [ @(stmt_vars_mp … V) #i #t * |
---|
113 | | @(stmt_labels_mp … L) #l * |
---|
114 | | cases s in R ⊢ %; // #x * |
---|
115 | ] |
---|
116 | | whd in match (labels_of ?); >(no_labels … H) @(f_inv f) |
---|
117 | ] |
---|
118 | ] |
---|
119 | ] qed. |
---|
120 | |
---|
121 | definition empty_vars : list (ident × region × (list init_data)) → |
---|
122 | list (ident × region × nat) ≝ |
---|
123 | map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉, |
---|
124 | size_init_data_list (\snd v)〉). |
---|
125 | |
---|
126 | definition replace_init : costlabel → Cminor_program → Cminor_noinit_program ≝ |
---|
127 | λcost,p. |
---|
128 | mk_program ?? |
---|
129 | (empty_vars (prog_vars ?? p)) |
---|
130 | (add_statement cost (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p)) |
---|
131 | (prog_main ?? p). |
---|