source: src/Cminor/initialisation.ma @ 2254

Last change on this file since 2254 was 2252, checked in by campbell, 7 years ago

Use the return statement invariant. Restructure the invariants for Cminor
a bit to make them more understandable.

File size: 4.5 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 (𝚺t:typ. expr t) ≝
9λinit.
10match 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       ⇒ Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))
15| Init_float64 f       ⇒ 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. *)
22definition stmt_inv : stmt → Prop ≝
23  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ∧ match s with [ St_return _ ⇒ False | _ ⇒ True ]).
24 
25discriminator option.
26discriminator DPair.
27
28(* Produces a few extra skips - hopefully the compiler will optimise these
29   away. *)
30
31definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝
32λid,r,init,off.
33match 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/
41cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
42destruct;/4 by stmt_labels_mp, conj/
43qed.
44
45definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
46λid,r,init.
47\snd (foldr ??
48  (λdatum,os.
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| elim init
54  [ % /3/
55  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair
56    %
57    [ /3/
58    | % [ @(pi2 … (init_datum …)) | @IH ]
59    ]
60] qed.
61
62definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
63λvars. foldr ? (Σs:stmt. stmt_inv s)
64  (λ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.
65[ % [ /3/ | % [ @(pi2 … s) | @(pi2 … (init_var …)) ] ]
66| /4/
67] qed.
68
69lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
70#s elim s //
71[ #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
72  >(IH1 H1) >(IH2 H2) @refl
73| #sz #sg #e #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
74  >(IH1 H1) >(IH2 H2) @refl
75| #l #s #IH * * * #_ *
76| #l #s #IH * #_ #H @(IH H)
77] qed.
78
79definition add_statement : ident → (Σs:stmt. stmt_inv s) →
80                              list (ident × (fundef internal_function)) →
81                              list (ident × (fundef internal_function)) ≝
82λid,s. match s with [ mk_Sig s H ⇒
83  map ??
84    (λidf.
85      let 〈id',f'〉 ≝ idf in
86      match ident_eq id id' with
87      [ inl _ ⇒
88          match f' with
89          [ Internal f ⇒ 〈id, Internal ? (mk_internal_function
90                                           (f_return f)
91                                           (f_params f)
92                                           (f_vars f)
93                                           (f_distinct f)
94                                           (f_stacksize f)
95                                           (St_seq s (f_body f))
96                                           ?)〉
97          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
98          ]
99      | inr _ ⇒ 〈id',f'〉 ]) ].
100%
101[ % //
102| %
103  [ @(stmt_P_mp … H) #s * * #V #L #R %
104    [ @(stmt_vars_mp … V) #i #t *
105    | @(stmt_labels_mp … L) #l *
106    | cases s in R ⊢ %; // #x *
107    ]
108  | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
109  ]
110] qed.
111
112definition empty_vars : list (ident × region × (list init_data)) →
113                        list (ident × region × nat) ≝
114map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
115              size_init_data_list (\snd v)〉).
116
117definition replace_init : Cminor_program → Cminor_noinit_program ≝
118λp.
119  mk_program ??
120    (empty_vars (prog_vars ?? p))
121    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
122    (prog_main ?? p).
Note: See TracBrowser for help on using the repository browser.