source: Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma @ 1105

Last change on this file since 1105 was 1105, checked in by campbell, 10 years ago

Show that RTLabs graphs are closed on branch (i.e., all labels in
instructions are in the graph). Rather time consuming and fiddly.

File size: 30.6 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5include "utilities/pair.ma".
6include "utilities/deppair.ma".
7
8definition env ≝ identifier_map SymbolTag register.
9definition label_env ≝ identifier_map Label label.
10definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
11λen,gen. foldr ??
12 (λidt,rsengen.
13   let 〈id,ty〉 ≝ idt in
14   let 〈rs,en,gen〉 ≝ rsengen in
15   let 〈r,gen'〉 ≝ fresh … gen in
16     〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.
17
18lemma populates_env : ∀l,e,u,l',e',u'.
19  populate_env e u l = 〈l',e',u'〉 →
20  ∀i. Exists ? (λx.\fst x = i) l →
21      present ?? e' i.
22#l elim l
23[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
24| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
25  * [ whd in ⊢ (??%? → ?) #E1 <E1
26      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
27      whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
28      whd in E:(??%?);
29      >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
30      whd >lookup_add_hit % #A destruct
31    | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
32      lapply (refl ? (populate_env e u tl))
33      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
34      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
35      whd in ⊢ (??%? → ?) #E
36      >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
37      @lookup_add_oblivious
38      @(IH … E1 ? H)
39    ]
40] qed.
41
42lemma populate_extends : ∀l,e,u,l',e',u'.
43  populate_env e u l = 〈l',e',u'〉 →
44  ∀i. present ?? e i → present ?? e' i.
45#l elim l
46[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
47| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
48  change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
49  lapply (refl ? (populate_env e u tl))
50  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
51  >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E
52  whd in E:(??%?)
53  >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ]
54  #i #H @lookup_add_oblivious @(IH … E0) @H
55] qed.
56
57definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
58λen,gen. foldr ??
59 (λid,engen.
60   let 〈en,gen〉 ≝ engen in
61   let 〈r,gen'〉 ≝ fresh … gen in
62     〈add ?? en id r, gen'〉) 〈en, gen〉.
63
64lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
65  populate_label_env lbls u ls = 〈lbls',u'〉 →
66  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
67#ls elim ls
68[ #lbls #u #lbls' #u' #E #l *
69| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
70  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
71  lapply (refl ? (populate_label_env lbls u t))
72  cases (populate_label_env lbls u t) in ⊢ (???% → %)
73  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
74  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
75  #l *
76  [ #El <El whd >lookup_add_hit % #Er destruct
77  | #H @lookup_add_oblivious @(IH … E1 ? H)
78  ]
79] qed.
80
81lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
82  populate_label_env lbls u ls = 〈lbls',u'〉 →
83  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
84#ls elim ls
85[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
86| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
87  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
88  lapply (refl ? (populate_label_env lbls u t))
89  cases (populate_label_env lbls u t) in ⊢ (???% → %)
90  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
91  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
92  #l #H cases (identifier_eq ? l h)
93  [ #El %1 %1 @El
94  | #NE cases (IH … E1 l ?)
95    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ ]
96  ]
97] qed.
98
99definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
100definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
101
102(* Check that the domain of one graph is included in another, for monotonicity
103   properties.  Note that we don't say anything about the statements. *)
104definition graph_included : graph statement → graph statement → Prop ≝
105λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
106
107lemma graph_inc_trans : ∀g1,g2,g3.
108  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
109#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
110
111definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
112
113definition partially_closed : label_env → graph statement → Prop ≝
114 λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s.
115
116(* I'd use a single parametrised definition along with internal_function, but
117   it's a pain without implicit parameters. *)
118record partial_fn (lenv:label_env) : Type[0] ≝
119{ pf_labgen    : universe LabelTag
120; pf_reggen    : universe RegisterTag
121; pf_result    : option (register × typ)
122; pf_params    : list (register × typ)
123; pf_locals    : list (register × typ)
124; pf_stacksize : nat
125; pf_graph     : graph statement
126; pf_closed    : partially_closed lenv pf_graph
127; pf_entry     : Σl:label. present ?? pf_graph l
128; pf_exit      : Σl:label. present ?? pf_graph l
129}.
130
131inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝
132| fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2.
133
134lemma fn_graph_inc_trans : ∀le,f1,f2,f3.
135  fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3.
136#le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed.
137
138lemma fn_graph_included_refl : ∀label_env,f.
139  fn_graph_included label_env f f.
140#le #f % #l #H @H qed.
141
142lemma fn_graph_included_sig : ∀label_env,f,f0.
143  ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'.
144  fn_graph_included label_env f f0 →
145  fn_graph_included label_env f f'.
146#le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1)
147qed.
148
149lemma add_statement_inv : ∀le,l,s.∀f.
150  labels_present (pf_graph le f) s →
151  partially_closed le (add … (pf_graph ? f) l s).
152#le #l #s #f #p
153#l' #s' #H cases (identifier_eq … l l')
154[ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
155  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
156| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
157  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
158  | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
159  ]
160] qed.
161
162(* Add a statement to the graph, *without* updating the entry label. *)
163definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
164λle,l,s,f,p.
165  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
166                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
167                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
168                «pf_entry ? f, ?» «pf_exit ? f, ?».
169[ @add_statement_inv @p
170| 2,3: @lookup_add_oblivious @use_sig
171| % #l' @lookup_add_oblivious
172] qed.
173
174(* Add a statement to the graph, making it the entry label. *)
175definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
176λle,l,s,f,p.
177  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
178                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
179                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
180                «l, ?» «pf_exit ? f, ?».
181[ @add_statement_inv @p
182| whd >lookup_add_hit % #E destruct
183| @lookup_add_oblivious @use_sig
184| % #l' @lookup_add_oblivious
185] qed.
186
187(* Add a statement with a fresh label to the start of the function.  The
188   statement is parametrised by the *next* instruction's label. *)
189definition add_fresh_to_graph : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
190λle,s,f,p.
191  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
192  let s' ≝ s (pf_entry ? f) in
193    (mk_partial_fn le g (pf_reggen ? f)
194                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
195                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
196                   «l, ?» «pf_exit ? f, ?»).
197[ % #l' @lookup_add_oblivious
198| @add_statement_inv @p @use_sig
199| whd >lookup_add_hit % #E destruct
200| @lookup_add_oblivious @use_sig
201] qed.
202
203(* Variants for labels which are (goto) labels *)
204
205lemma add_statement_inv' : ∀le,l,s.∀f.
206  labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s →
207  partially_closed le (add … (pf_graph ? f) l s).
208#le #l #s #f #p
209#l' #s' #H cases (identifier_eq … l l')
210[ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
211  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
212| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
213  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
214  | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
215  ]
216] qed.
217
218definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
219λle,s,f,p.
220  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
221  let s' ≝ s (pf_entry ? f) in
222    (mk_partial_fn le g (pf_reggen ? f)
223                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
224                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
225                   «l, ?» «pf_exit ? f, ?»).
226[ % #l' @lookup_add_oblivious
227| @add_statement_inv' @p @use_sig
228| whd >lookup_add_hit % #E destruct
229| @lookup_add_oblivious @use_sig
230] qed.
231
232definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
233λle,f,ty.
234  let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in
235    〈r, «mk_partial_fn le (pf_labgen ? f) g
236                       (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f))
237                       (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉.
238% #l // qed.
239
240axiom UnknownVariable : String.
241
242definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
243λle,env,ty,e,f.
244  match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with
245  [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉
246  | _ ⇒ λ_.fresh_reg le f ty
247  ].
248% // qed.
249 
250let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝ 
251 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.
252
253definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
254
255definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t).
256                         ∀f:partial_fn le. All ? (exprtyp_present env) es →
257                         list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
258λle,env,es,f,Env.
259  foldr_all (Σt:typ.expr t) ??
260    (λe,p,acc. let 〈rs,f〉 ≝ acc in
261             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg le env t e (eject … f) ? ] p in
262             〈r::rs,«eject … f', ?»〉) 〈[ ], «f, ?»〉 es Env.
263[ @p
264| @fn_graph_inc_trans [ 3: @(use_sig ?? f') | skip | @(use_sig ?? f) ]
265| % //
266]  qed.
267
268lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
269((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
270∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
271#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
272
273
274lemma choose_regs_length : ∀le,env,es,f,p,rs,f'.
275  choose_regs le env es f p = 〈rs,f'〉 → |es| = |rs|.
276#le #env #es #f elim es
277[ #p #rs #f normalize #E destruct @refl
278| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
279  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
280  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
281  destruct (E4) skip (E1 E3) @eq_f @IH
282  [ @(proj2 … p)
283  | 3: @sym_eq @E1
284  | 2: skip
285  ]
286] qed.
287
288lemma present_inc : ∀le,f,l.
289  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
290  present ?? (pf_graph le f) l →
291  present ?? (pf_graph le f') l.
292#le #f #l * #f' * #H1 #H2 @H1 @H2 qed.
293
294axiom BadCminorProgram : String.
295
296let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝
297match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
298[ Id _ i ⇒ λEnv.
299    let r ≝ lookup_reg env i Env in
300    match register_eq r dst with
301    [ inl _ ⇒ «f, ?»
302    | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 Oid dst r) f ?), ?»
303    ]
304| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
305| Op1 _ _ op e' ⇒ λEnv.
306    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
307    let f ≝ add_fresh_to_graph ? (St_op1 op dst r) f ? in
308    let f ≝ add_expr ? env ? e' Env r f in
309      «eject … f, ?»
310| Op2 _ _ _ op e1 e2 ⇒ λEnv.
311    let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
312    let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in
313    let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in
314    let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
315    let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
316      «eject … f, ?»
317| Mem _ _ q e' ⇒ λEnv.
318    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
319    let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
320    let f ≝ add_expr ? env ? e' Env r f in
321      «eject … f, ?»
322| Cond _ _ _ e' e1 e2 ⇒ λEnv.
323    let resume_at ≝ pf_entry ? f in
324    let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in
325    let lfalse ≝ pf_entry ? f in
326    let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in
327    let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in
328    let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
329    let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
330    let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
331      «eject … f, ?»
332| Ecost _ l e' ⇒ λEnv.
333    let f ≝ add_expr ? env ? e' Env dst f in
334    let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
335      «f, ?»
336] Env.
337(* For new labels, we need to step back through the definitions of f until we
338   hit the point that it was added. *)
339try @fn_graph_included_refl
340try (#l #H @H)
341[ 7: #l #H whd % [ @H |
342    @present_inc
343    @present_inc
344    @present_inc
345    @(use_sig ? (present ???)) ]
346| 8: #l #H
347    @present_inc
348    @(use_sig ? (present ???))
349(* For the monotonicity properties, we just keep going back until we're at the
350   start.  The repeat tactical helps here. *)
351| *: repeat @fn_graph_included_sig @fn_graph_included_refl
352] qed.
353
354let rec add_exprs (le:label_env) (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
355                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
356match es return λes.All ?? es → |es|=|dsts| → ? with
357[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
358| cons e et ⇒ λEnv.
359    match dsts return λx. ?=|x| → ? with
360    [ nil ⇒ λpf.⊥
361    | cons r rt ⇒ λpf.
362        let f ≝ add_exprs ? env et ? rt ? f in
363        match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv.
364          let f ≝ add_expr ? env ty e ? r f in
365            «eject … f, ?» ] (proj1 ?? Env)
366    ]
367] Env pf.
368[ //
369| 2,3: normalize in pf; destruct
370| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
371| @Env
372| @(proj2 … Env)
373| normalize in pf; destruct @e0 ] qed.
374
375axiom UnknownLabel : String.
376axiom ReturnMismatch : String.
377
378definition stmt_inv : env → label_env → stmt → Prop ≝
379λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
380
381(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
382definition expr_is_Id : ∀t. expr t → option ident ≝
383λt,e. match e with
384[ Id _ id ⇒ Some ? id
385| _ ⇒ None ?
386].
387
388(* XXX Work around odd disambiguation errors. *)
389alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
390alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
391
392definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
393λA,P,m,l,n.
394  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
395  [ None ⇒ λ_. Error ? m
396  | Some a ⇒ λH'. OK ? «a, ?»
397  ] (All_nth A P n l (use_sig … l)).
398@H' @refl qed.
399
400lemma lookup_label_rev : ∀lenv,l,l',p.
401  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
402#lenv #l #l' #p
403cut (∃lx. lookup ?? lenv l = Some ? lx)
404[ whd in p; cases (lookup ?? lenv l) in p ⊢ %
405  [ * #H cases (H (refl ??))
406  | #lx #_ %{lx} @refl
407  ]
408| * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl
409] qed.
410
411lemma lookup_label_rev' : ∀lenv,l,p.
412  lookup ?? lenv l = Some ? (lookup_label lenv l p).
413#lenv #l #p @lookup_label_rev [ @p | @refl ]
414qed.
415
416lemma lookup_label_lpresent : ∀lenv,l,p.
417  lpresent lenv (lookup_label lenv l p).
418#le #l #p whd %{l} @lookup_label_rev'
419qed.
420
421(* We need to show that the graph only grows, and that Cminor labels will end
422   up in the graph. *)
423definition Cminor_labels_added ≝ λle,s,f'.
424∀l. Exists ? (λl'.l=l') (labels_of s) →
425∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
426
427record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
428{ stmt_graph_inc : fn_graph_included ? f f'
429; stmt_labels_added : Cminor_labels_added le s f'
430}.
431
432lemma empty_Cminor_labels_added : ∀le,s,f'.
433  labels_of s = [ ] → Cminor_labels_added le s f'.
434#le #s #f' #E whd >E #l *;
435qed.
436
437lemma equal_Cminor_labels_added : ∀le,s,s',f.
438  labels_of s = labels_of s' → Cminor_labels_added le s' f →
439  Cminor_labels_added le s f.
440#le #s #s' #f #E whd in ⊢ (% → %) > E #H @H
441qed.
442
443lemma fn_graph_included_inv : ∀label_env,s,f,f0.
444  ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'.
445  fn_graph_included label_env f f0 →
446  fn_graph_included label_env f f'.
447#label_env #s #f #f0 * #f' * #H1 #H2 #H3
448@(fn_graph_inc_trans … H3 H1)
449qed.
450
451lemma present_inc' : ∀le,s,f,l.
452  ∀f':(Σf':partial_fn le. add_stmt_inv le s f f').
453  present ?? (pf_graph le f) l →
454  present ?? (pf_graph le f') l.
455#le #s #f #l * #f' * * #H1 #H2 #H3
456@H1 @H3
457qed.
458
459lemma Cminor_labels_inv : ∀le,s,s',f.
460  ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
461  Cminor_labels_added le s f →
462  Cminor_labels_added le s f'.
463#le #s #s' #f * #f' * #H1 #H2 #H3
464#l #E cases (H3 l E) #l' * #L #P
465%{l'} % [ @L | @present_inc' @P ]
466qed.
467
468lemma Cminor_labels_sig : ∀le,s,f.
469  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
470  Cminor_labels_added le s f →
471  Cminor_labels_added le s f'.
472#le #s #f * #f' #H1 #H2
473#l #E cases (H2 l E) #l' * #L #P
474%{l'} % [ @L | @present_inc @P ]
475qed.
476
477let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
478match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
479[ St_skip ⇒ λ_. OK ? «f, ?»
480| St_assign _ x e ⇒ λEnv.
481    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
482    OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
483| St_store _ _ q e1 e2 ⇒ λEnv.
484    let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
485    let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
486    let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
487    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
488    OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
489| St_call return_opt_id e args ⇒ λEnv.
490    let return_opt_reg ≝
491      match return_opt_id return λo. ? → ? with
492      [ None ⇒ λ_. None ?
493      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
494      ] Env in
495    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
496    let f ≝
497      match expr_is_Id ? e with
498      [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ?
499      | None ⇒
500        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
501        let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
502        «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
503      ] in
504    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
505| St_tailcall e args ⇒ λEnv.
506    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
507    let f ≝
508      match expr_is_Id ? e with
509      [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ?
510      | None ⇒
511        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
512        let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
513        «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
514      ] in
515    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
516| St_seq s1 s2 ⇒ λEnv.
517    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
518    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
519      OK ? «eject … f1, ?»
520| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
521    let l_next ≝ pf_entry ? f in
522    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
523    let l2 ≝ pf_entry ? f2 in
524    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in
525    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
526    let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
527    let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
528    OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
529| St_loop s ⇒ λEnv.
530    let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
531    let l_loop ≝ pf_entry ? f in
532    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
533    OK ? «eject … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
534| St_block s ⇒ λEnv.
535    do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
536    OK ? «eject … f, ?»
537| St_exit n ⇒ λEnv.
538    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
539    OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
540| St_switch sz sg e tab n ⇒ λEnv.
541    let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
542    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
543    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in
544    do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f.
545      do f ← f;
546      let 〈i,n〉 ≝ cs in
547      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
548      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
549      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
550      let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in
551      let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
552      let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
553        OK ? «eject … f, ?») (OK ? f) tab;
554    OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?»
555| St_return opt_e ⇒ let f0 ≝ f in
556    let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
557    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with
558    [ None ⇒ λEnv. OK ? «eject … f, ?»
559    | Some e ⇒
560        match pf_result ? f with
561        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
562        | Some r ⇒
563            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with
564            [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
565                              OK ? «eject … f, ?» ]
566        ]
567    ]
568| St_label l s' ⇒ λEnv.
569    do f ← add_stmt env label_env s' (π2 Env) f exits;
570    let l' ≝ lookup_label label_env l ? in
571    OK ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
572| St_goto l ⇒ λEnv.
573    let l' ≝ lookup_label label_env l ? in
574    OK ? «eject … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
575| St_cost l s' ⇒ λEnv.
576    do f ← add_stmt env label_env s' (π2 Env) f exits;
577    OK ? «eject … (add_fresh_to_graph ? (St_cost l) f ?), ?»
578] Env.
579try @(π1 Env)
580try @(π2 Env)
581try @(π1 (π1 Env))
582try @(π2 (π1 Env))
583try @mk_add_stmt_inv
584try (@empty_Cminor_labels_added @refl)
585try (@(All_mp … (use_sig ?? exits)))
586try @fn_graph_included_refl
587try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl)
588try (#l #H @I)
589try (#l #H @H)
590[ -f @(choose_regs_length … (sym_eq … Eregs))
591| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
592| whd in Env @(π1 (π1 (π1 Env)))
593| -f @(choose_regs_length … (sym_eq … Eregs))
594| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
595| #l #H cases (Exists_append … H)
596  [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
597  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2))
598  ]
599| #l #H @present_inc' @H
600| #l #H @present_inc' @use_sig
601| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
602| #l #H cases (Exists_append … H)
603  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1))
604  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2))
605  ]
606| #l #H % [ @H | @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ]
607| #l #H @present_inc @present_inc' @H
608| #l #H @present_inc @H
609| @(use_sig ?? (pf_entry ??))
610| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl
611| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
612| % [ @use_sig | @(use_sig ?? exits) ]
613| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
614| #l #H @use_sig
615| #l #H @present_inc @use_sig
616| #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig | @H ]
617| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
618| @use_sig
619| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
620| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
621        |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
622        ]
623| #l1 #H whd %2 @lookup_label_lpresent
624| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
625| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
626] qed.
627
628(*
629definition mk_fn : ∀le. partial_fn le → internal_function ≝
630λle, f.
631  mk_internal_function
632    (pf_labgen ? f)
633    (pf_reggen ? f)
634    (pf_result ? f)
635    (pf_params ? f)
636    (pf_locals ? f)
637    (pf_stacksize ? f)
638    (pf_graph ? f)
639    ?
640    (pf_entry ? f)
641    (pf_exit ? f).
642#l #s #E @(labels_P_mp … (pf_closed ? f l s E))
643#l' * [ // | #H
644*)
645
646definition c2ra_function (*: internal_function → internal_function*) ≝
647λf.
648let labgen0 ≝ new_universe LabelTag in
649let reggen0 ≝ new_universe RegisterTag in
650let cminor_labels ≝ labels_of (f_body f) in
651let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
652let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
653let 〈result, locals, reggen〉 ≝
654  match f_return f with
655  [ None ⇒ 〈None ?, locals0, reggen2〉
656  | Some ty ⇒
657      let 〈r,gen〉 ≝ fresh … reggen2 in
658        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
659let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
660let 〈l,labgen〉 ≝ fresh … labgen1 in
661let emptyfn ≝
662  mk_partial_fn
663    label_env
664    labgen
665    reggen
666    result
667    params
668    locals
669    (f_stacksize f)
670    (add ?? (empty_map …) l St_return)
671    ?
672    l
673    l in
674do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
675do u1 ← check_universe_ok ? (pf_labgen ? f);
676do u2 ← check_universe_ok ? (pf_reggen ? f);
677OK ? (mk_internal_function
678    (pf_labgen ? f)
679    (pf_reggen ? f)
680    (pf_result ? f)
681    (pf_params ? f)
682    (pf_locals ? f)
683    (pf_stacksize ? f)
684    (pf_graph ? f)
685    ?
686    (pf_entry ? f)
687    (pf_exit ? f)
688  ).
689[ @I
690| -emptyfn @(stmt_P_mp … (f_inv f))
691  #s * #V #L %
692  [ @(stmt_vars_mp … V)
693    #i #H cases (Exists_append … H)
694    [ #H1 @(populate_extends ?????? (sym_eq … E2))
695          @(populates_env … (sym_eq … E1)) @H1
696    | #H1 @(populates_env … (sym_eq … E2)) @H1
697    ]
698  | @(stmt_labels_mp … L)
699    #l #H @(populates_label_env … (sym_eq … El)) @H
700  ]
701| #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
702  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
703  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
704  #P' @P'
705  | cases (label_env_contents … (sym_eq ??? El) l ?)
706    [ #H @H
707    | whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??))
708    | whd >H % #E' destruct (E')
709    ]
710  ]
711  ]
712| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
713  [ * #E1 #E2 >E2 @I
714  | whd in ⊢ (??%? → ?) #E' destruct (E')
715  ]
716| *: whd >lookup_add_hit % #E destruct
717]
718qed.
719
720definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
721transform_partial_program ???
722  (transf_partial_fundef ?? c2ra_function).
723
724include "Cminor/initialisation.ma".
725
726definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
727λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.