source: Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma @ 1101

Last change on this file since 1101 was 1101, checked in by campbell, 9 years ago

Label preservation in Cminor initialisation and RTLabs translation
on branch.

File size: 4.8 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(* None of the additional code introduces locals or labels. *)
22definition stmt_inv : stmt → Prop ≝
23  stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
24
25(* Produces a few extra skips - hopefully the compiler will optimise these
26   away. *)
27
28definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝
29λid,r,init,off.
30match init_expr init with
31[ None ⇒ St_skip
32| Some x ⇒
33    match x with [ dp chunk e ⇒
34      St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
35    ]
36].
37% //
38cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
39qed.
40
41lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
42  let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.
43#A #B #C #D * // qed.
44
45lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.
46  R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).
47#A #B #C #D *; normalize /2/
48qed.
49
50lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.
51  stmt_inv s.
52* #s #p @p
53qed.
54
55definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
56λid,r,init.
57\snd (foldr ??
58  (λdatum,os.
59   let 〈off,s〉 ≝ os in
60     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
61  〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init).
62[ % //
63| elim init
64  [ % //
65  | #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % // | @sig_stmt_inv ] | @IH ]
66] qed.
67
68definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_inv s ≝
69λvars. foldr ? (Σs:stmt. stmt_inv s)
70  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
71% [ % [ % // | @sig_stmt_inv ] | @sig_stmt_inv ]
72qed.
73
74lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
75#s elim s //
76[ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
77  >(IH1 H1) >(IH2 H2) @refl
78| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
79  >(IH1 H1) >(IH2 H2) @refl
80| #s #IH * * #_ #_ #H @(IH H)
81| #s #IH * * #_ #_ #H @(IH H)
82| #l #s #IH * * #_ *
83| #l #s #IH * * #_ #_ #H @(IH H)
84] qed.
85
86definition add_statement : ident → (Σs:stmt. stmt_inv s) →
87                              list (ident × (fundef internal_function)) →
88                              list (ident × (fundef internal_function)) ≝
89λid,s. match s with [ dp 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_stacksize f)
101                                           (St_seq s (f_body f))
102                                           ?)〉
103          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
104          ]
105      | inr _ ⇒ 〈id',f'〉 ]) ].
106%
107[ % [ % // |
108  @(stmt_P_mp … H) #s * #V #L %
109  [ @(stmt_vars_mp … V) #i *
110  | @(stmt_labels_mp … L) #l *
111  ]
112  ]
113| whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f)
114] qed.
115
116definition empty_vars : list (ident × (list init_data) × region × unit) →
117                        list (ident × (list init_data) × region × unit) ≝
118map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
119               [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
120              \snd (\fst v)〉,
121              \snd v〉).
122
123definition replace_init : Cminor_program → Cminor_program ≝
124λp.
125  mk_program ??
126    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
127    (prog_main ?? p)
128    (empty_vars (prog_vars ?? p)).
129   
Note: See TracBrowser for help on using the repository browser.