source: src/Cminor/toRTLabs.ma @ 2936

Last change on this file since 2936 was 2936, checked in by campbell, 5 years ago

Disable initialisation code generation in Cminor, propogate init data
through RTLabs.

File size: 39.8 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "Cminor/Cminor_syntax.ma".
4include "RTLabs/RTLabs_syntax.ma".
5
6definition env ≝ identifier_map SymbolTag (register × typ).
7definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
8λen,gen. foldr ??
9 (λidt,rsengen.
10   let 〈id,ty〉 ≝ idt in
11   let 〈rs,en,gen〉 ≝ rsengen in
12   let 〈r,gen'〉 ≝ fresh … gen in
13     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.
14
15definition Env_has : env → ident → typ → Prop ≝
16λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
17
18lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
19#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
20[ * | * #r #t' #E % #E' destruct ]
21qed.
22
23lemma populates_env : ∀l,e,u,l',e',u'.
24  distinct_env ?? l →
25  populate_env e u l = 〈l',e',u'〉 →
26  ∀i,t. Exists ? (λx.x = 〈i,t〉) l →
27      Env_has e' i t.
28#l elim l
29[ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) *
30| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?);
31  * [ #E1 destruct (E1)
32      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
33      whd in ⊢ (??%? → ?);
34      lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %);
35      #r #gen' #E1 #E2
36      whd in E2:(??%?); destruct;
37      whd >lookup_add_hit %
38    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
39      lapply (refl ? (populate_env e u tl))
40      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
41      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?);
42      lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2
43      whd in ⊢ (??%? → ?); #E destruct
44      whd >lookup_add_miss
45      [ @(IH … E1 ?? H) @(proj2 … D)
46      | cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/
47      ]
48    ]
49] qed.
50
51lemma populates_env_distinct : ∀r,l,e,u,l',e',u'.
52  distinct_env ?? (l@r) →
53  populate_env e u l = 〈l',e',u'〉 →
54  All ? (λit. fresh_for_map … (\fst it) e) r →
55  All ? (λit. fresh_for_map … (\fst it) e') r.
56#r #l elim l
57[ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) //
58| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?);
59  change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?);
60  lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?);
61  * #x #y #z #E2 >E2 in E;
62  whd in ⊢ (??%? → ?);
63  elim (fresh ? z)
64  #rg #gen' #E
65  whd in E:(??%?); destruct
66  #F lapply (IH … E2 F)
67  [ @(proj2 … D)
68  | lapply (All_append_r … (proj1 … D))
69    elim r
70    [ //
71    | * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 %
72      [ @fresh_for_map_add /2/
73      | @IH //
74      ]
75    ]
76  ]
77] qed.
78
79lemma populate_extends : ∀l,e,u,l',e',u'.
80  All ? (λit. fresh_for_map ?? (\fst it) e) l →
81  populate_env e u l = 〈l',e',u'〉 →
82  ∀i,t. Env_has e i t → Env_has e' i t.
83#l elim l
84[ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct //
85| * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?);
86  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
87  lapply (refl ? (populate_env e u tl))
88  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
89  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
90  destruct
91  #i #t #H whd >lookup_add_miss
92  [ @(IH … E0) [ @(proj2 … F) | @H ]
93  | @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; * | @(proj1 … F) ]
94] qed.
95
96definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
97/2/ qed.
98
99lemma populate_env_list : ∀l,e,u,l',e',u'.
100  populate_env e u l = 〈l',e',u'〉 →
101  ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r →
102    (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t.
103#l elim l
104[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L
105| * #id #ty #tl #IH #e #u #l' #e' #u' #E
106  whd in E:(??%?);
107  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
108  lapply (refl ? (populate_env e u tl))
109  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
110  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
111  destruct
112  #i #r #t cases (identifier_eq ? i id)
113  [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????);
114    generalize in ⊢ (??(??? (?%))? → ?);
115    whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct
116    %2 %1 %
117  | #NE #H #L cases (IH … E0 i r t ??)
118    [ /2/
119    | #X %2 %2 @X
120    | whd in H ⊢ %; >lookup_add_miss in H; //
121    | whd in L:(??%?); whd in match (lookup_present ?????) in L;
122      lapply L -L
123      generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?);
124      generalize in ⊢ (? → ? → ??(????%)?);
125      >lookup_add_miss // #H0 #p
126      change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?);
127      whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?);
128      #p' #X @X
129    ]
130  ]
131] qed.
132
133(* Check that the domain of one graph is included in another, for monotonicity
134   properties.  Note that we don't say anything about the statements. *)
135definition graph_included : graph statement → graph statement → Prop ≝
136extends_domain ??.
137
138lemma graph_inc_trans : ∀g1,g2,g3.
139  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
140@extends_dom_trans
141qed.
142
143
144(* Some data structures for the transformation that remain fixed throughout. *)
145record fixed : Type[0] ≝ {
146  fx_gotos  : identifier_set Label;
147  fx_env    : env;
148  fx_rettyp : option typ
149}.
150
151definition resultok : option typ → list (register × typ) → Type[0] ≝
152λty,env.
153  match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ].
154
155(* We put in dummy statements for gotos, then change them afterwards once we
156   know their true destinations.  So first we need a mapping between the dummy
157   CFG nodes and the Cminor destination.  (We'll also keep a mapping of goto
158   labels to their RTLabs statements.) *)
159
160record goto_map (fx:fixed) (g:graph statement) : Type[0] ≝ {
161  gm_map :> identifier_map LabelTag (identifier Label);
162  gm_dom : ∀id. present ?? gm_map id → present ?? g id;
163  gm_img : ∀id,l. lookup … gm_map id = Some ? l → present ?? (fx_gotos fx) l
164}.
165
166(* I'd use a single parametrised definition along with internal_function, but
167   it's a pain without implicit parameters. *)
168record partial_fn (fx:fixed) : Type[0] ≝
169{ pf_labgen    : universe LabelTag
170; pf_reggen    : universe RegisterTag
171; pf_params    : list (register × typ)
172; pf_locals    : list (register × typ)
173; pf_result    : resultok (fx_rettyp … fx) (pf_locals @ pf_params)
174; pf_envok     : ∀id,ty,r,H. lookup_reg (fx_env … fx) id ty H = r → env_has (pf_locals @ pf_params) r ty
175; pf_stacksize : nat
176; pf_graph     : graph statement
177; pf_closed    : graph_closed pf_graph
178; pf_gotos     : goto_map fx pf_graph
179; pf_labels    : Σm:identifier_map Label (identifier LabelTag). ∀l,l'. lookup … m l = Some ? l' → present ?? pf_graph l'
180; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
181; pf_entry     : Σl:label. present ?? pf_graph l
182; pf_exit      : Σl:label. present ?? pf_graph l
183}.
184
185definition fn_env_has ≝
186  λfx,f. env_has (pf_locals fx f @ pf_params fx f).
187
188(* TODO: move or use another definition if there's already one *)
189definition map_extends : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝
190λtag,A,m1,m2. ∀id,a. lookup tag A m1 id = Some A a → lookup tag A m2 id = Some A a.
191
192lemma map_extends_trans : ∀tag,A,m1,m2,m3.
193  map_extends tag A m1 m2 →
194  map_extends tag A m2 m3 →
195  map_extends tag A m1 m3.
196/3/
197qed.
198
199record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
200{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
201; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty
202; fn_con_labels : extends_domain … (pf_labels … f1) (pf_labels … f2)
203}.
204
205lemma fn_con_trans : ∀fx,f1,f2,f3.
206  fn_contains fx f1 f2 → fn_contains … f2 f3 → fn_contains … f1 f3.
207#fx #f1 #f2 #f3 #H1 #H2 %
208[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
209| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
210| @(extends_dom_trans … (fn_con_labels … H1) (fn_con_labels … H2))
211] qed.
212
213lemma fn_con_refl : ∀fx,f.
214  fn_contains fx f f.
215#fx #f % #l // qed.
216
217lemma fn_con_sig : ∀fx,f,f0.
218  ∀f':Σf':partial_fn fx. fn_contains … f0 f'.
219  fn_contains fx f f0 →
220  fn_contains fx f f'.
221#fx #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
222qed.
223
224lemma add_statement_inv : ∀fx,l,s.∀f.
225  labels_present (pf_graph fx f) s →
226  graph_closed (add … (pf_graph … f) l s).
227#fx #l #s #f #p
228#l' #s' #H cases (identifier_eq … l l')
229[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
230  @(labels_P_mp … p) #l0 #H @lookup_add_oblivious @H
231| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
232  [ #lx #H @lookup_add_oblivious @H
233  | >lookup_add_miss in H; /2/
234  ]
235] qed.
236
237definition statement_typed_in ≝
238λfx,f,s. statement_typed (pf_locals fx f @ pf_params fx f) s.
239
240lemma forall_nodes_add : ∀A,P,l,a,g.
241  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
242#A #P #l #a #g #ALL #NEW
243#l' #a'
244cases (identifier_eq … l' l)
245[ #E destruct >lookup_add_hit #E destruct @NEW
246| #ne >lookup_add_miss /2/
247] qed.
248
249(* Add a statement to the graph, *without* updating the entry label. *)
250definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
251  labels_present (pf_graph … f) s →
252  statement_typed_in … f s →
253  Σf':partial_fn fx. fn_contains … f f' ≝
254λfx,l,s,f,p,tp.
255  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
256                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
257                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ?
258                (mk_goto_map … (pf_gotos … f) ??) «pf_labels … f, ?» ?
259                «pf_entry … f, ?» «pf_exit … f, ?».
260[ @add_statement_inv @p
261| @gm_img
262| #id #PR @lookup_add_oblivious @(gm_dom … PR)
263| #l1 #l2 #L @lookup_add_oblivious @(pi2 … (pf_labels … f) … L)
264| @forall_nodes_add //
265| 6,7: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
266| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
267] qed.
268
269(* Add a statement to the graph, making it the entry label. *)
270definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
271  labels_present (pf_graph … f) s →
272  statement_typed_in … f s →
273  Σf':partial_fn fx. fn_contains … f f' ≝
274λfx,l,s,f,p,tl.
275  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
276                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
277                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ????
278                «l, ?» «pf_exit … f, ?».
279[ @add_statement_inv @p
280| cases (pf_gotos … f) #m #dom #img %
281  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
282| cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
283| @forall_nodes_add //
284| whd >lookup_add_hit % #E destruct
285| @lookup_add_oblivious @(pi2 … (pf_exit … f))
286| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
287] qed.
288
289(* Change the entry point to the function (i.e., the successor for any new
290   instructions that we add). *)
291definition change_entry : ∀fx. ∀f:partial_fn fx.
292  ∀l. present ?? (pf_graph … f) l →
293  Σf':partial_fn fx. fn_contains … f f' ≝
294λfx,f,l,PR.
295  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
296                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
297                (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f)
298                (pf_labels … f) (pf_typed … f)
299                «l, PR» (pf_exit … f).
300% //
301qed.
302
303(* Add a statement with a fresh label to the start of the function.  The
304   statement is parametrised by the *next* instruction's label. *)
305definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
306  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
307  (∀l. statement_typed_in … f (s l)) →
308  Σf':partial_fn fx. fn_contains … f f' ≝
309λfx,s,f,p,tp.
310  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
311  let s' ≝ s (pf_entry … f) in
312    (mk_partial_fn fx g (pf_reggen … f)
313                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
314                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ????
315                   «l, ?» «pf_exit … f, ?»).
316[ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
317| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
318| @add_statement_inv @p @(pi2 … (pf_entry …))
319| cases (pf_gotos … f) #m #dom #img %
320  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
321| @forall_nodes_add //
322| whd >lookup_add_hit % #E destruct
323| @lookup_add_oblivious @(pi2 … (pf_exit …))
324] qed.
325
326lemma extend_typ_env : ∀te,r,t,r',t'.
327  env_has te r t → env_has (〈r',t'〉::te) r t.
328#tw #r #t #r' #t' #H %2 @H
329qed.
330
331lemma stmt_extend_typ_env : ∀te,r,t,s.
332  statement_typed te s → statement_typed (〈r,t〉::te) s.
333#tw #r #t *
334[ 1,2: //
335| #t' #r #cst #l #H %2 @H
336| #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
337| #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
338| 6,7: #t' #r1 #r2 #l * /3/
339| #id #rs * [ 2: #dst ] #l * #RS [ * #td ] #DST % [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ | // ]
340| #fnptr #rs * [ 2: #dst ] #l * * #FNPTR #RS [ * #td ] #DST % try @conj /2/ [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ ]
341| #r' #l1 #l2 * #t' #E /3/
342| //
343] qed.
344
345(* A little more nesting in the result type than I'd like, but it keeps the
346   function closely paired with the proof that it contains f. *)
347definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ.
348  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
349λfx,f,ty.
350  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
351  let f' ≝
352    «mk_partial_fn fx
353       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
354       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?»
355  in
356    ❬f' , ?(*«r, ?»*)❭.
357[ @(«r, ?») % @refl
358| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
359| #i #t #r1 #H #L %2 @(pf_envok … f … L)
360| lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
361| % [ #l // | #r' #ty' #H @extend_typ_env @H | // ]
362] qed.
363
364definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
365  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
366λfx,ty,e,f.
367  match e return λty,e. expr_vars ty e (Env_has (fx_env fx)) → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) with
368  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭
369  | _ ⇒ λ_.fresh_reg … f ?
370  ].
371[ % //
372| @(pf_envok … Env) @refl
373] qed.
374 
375let 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 ≝ 
376 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.
377 
378let rec foldr_all' (A:Type[0]) (P:A → Prop) (B:list A → Type[0]) (f:∀a:A. P a → ∀l. B l → B (a::l)) (b:B [ ]) (l:list A) (H:All ? P l) on l :B l ≝ 
379 match l return λx.All ? P x → B x with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) l (foldr_all' A P B f b l (proj2 … H))] H.
380
381definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
382
383definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
384λA,P,x. match x with [ mk_DPair a _ ⇒ a].
385
386definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t).
387                         ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es →
388                         𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es) ≝
389λfx,es,f,Env.
390  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es))
391    (λe,p,tl,acc.
392      match acc return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
393        match e return λe.exprtyp_present (fx_env fx) e → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
394          match choose_reg fx t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
395            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
396          ]
397        ] p
398      ]) ❬«f, ?», «[ ], I»❭ es Env.
399[ @p
400| cases r #r' #Hr' cases rs #rs' #Hrs'
401  % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
402| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
403| @fn_con_refl
404]  qed.
405
406lemma choose_regs_length : ∀fx,es,f,p,f',rs.
407  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
408#fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
409qed.
410
411lemma present_included : ∀fx,f,f',l.
412  fn_contains fx f f' →
413  present ?? (pf_graph … f) l →
414  present ?? (pf_graph … f') l.
415#fx #f #f' #l * #H1 #H2 #H3 @H1 qed.
416
417(* Some definitions for the add_stmt function later, which we introduce now so
418   that we can build the whole fn_graph_included machinery at once. *)
419
420(* We need to show that the graph only grows, and that Cminor labels will end
421   up in the graph. *)
422definition Cminor_labels_added ≝ λfx,s,f'.
423∀l. Exists ? (λl'.l=l') (labels_of s) → present ?? (pf_labels fx f') l.
424
425record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
426{ stmt_graph_con : fn_contains … f f'
427; stmt_labels_added : Cminor_labels_added … s f'
428}.
429
430(* Build some machinery to solve fn_contains goals. *)
431
432(* A datatype saying how we intend to prove a step. *)
433inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝
434| fn_con_eq : ∀f. fn_con_because fx f
435| fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
436    ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3
437| fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
438    ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3
439.
440
441(* Extract the starting function for a step. *)
442let rec fn_con_because_left fx f0  (b:fn_con_because ? f0) on b : partial_fn fx ≝
443  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
444
445(* Some unification hints to pick the right step to apply.  The dummy variable
446   is there to provide goal that the lemma can't apply to, which causes an error
447   and forces the "repeat" tactical to stop.  The first hint recognises that we
448   have reached the desired starting point. *)
449
450unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True;
451  f' ≟ f,
452  b  ≟ fn_con_eq fx f
453
454  fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f'
455.
456
457unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, f3:(Σf3:partial_fn fx. fn_contains fx f2 f3);
458  b ≟ fn_con_sig fx f1 f2 H12 f3
459
460  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
461.
462
463unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, s:stmt, f3:(Σf3:partial_fn fx. add_stmt_inv fx s f2 f3);
464  b ≟ fn_con_addinv fx f1 f2 H12 s f3
465
466  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
467.
468
469(* A lemma to perform a step of the proof.  We can repeat this to do the whole
470   proof. *) 
471lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f.
472#fx #f *
473[ #f @fn_con_refl
474| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
475| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
476] qed.
477
478
479let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
480  (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx)
481  (dst:Σdst. fn_env_has … f dst ty)
482  on e: Σf':partial_fn fx. fn_contains … f f' ≝
483match e return λty,e.expr_vars ty e (Env_has ?) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn fx. fn_contains … f f' with
484[ Id t i ⇒ λEnv,dst.
485    let r ≝ lookup_reg (fx_env fx) i t Env in
486    match register_eq r dst with
487    [ inl _ ⇒ «f, ?»
488    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
489    ]
490| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
491| Op1 t t' op e' ⇒ λEnv,dst.
492    let ❬f,r❭ ≝ choose_reg … e' f Env in
493    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
494    let f ≝ add_expr … ? e' Env f «r, ?» in
495      «pi1 … f, ?»
496| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
497    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
498    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
499    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
500    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
501    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
502      «pi1 … f, ?»
503| Mem t e' ⇒ λEnv,dst.
504    let ❬f,r❭ ≝ choose_reg … e' f Env in
505    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
506    let f ≝ add_expr … ? e' Env f «r,?» in
507      «pi1 … f, ?»
508| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
509    let resume_at ≝ pf_entry … f in
510    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
511    let lfalse ≝ pf_entry … f in
512    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
513    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
514    let ❬f,r❭ ≝ choose_reg … e' f ? in
515    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
516    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
517      «pi1 … f, ?»
518| Ecost _ l e' ⇒ λEnv,dst.
519    let f ≝ add_expr … ? e' Env f dst in
520    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
521      «f, ?»
522] Env dst.
523(* For new labels, we need to step back through the definitions of f until we
524   hit the point that it was added. *)
525try (repeat @fn_contains_step @I)
526try (#l #H @H)
527try (#l @I)
528[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
529| #l @(pi2 … dst)
530| 3,8,10: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
531| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
532| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
533| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
534| #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
535| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
536| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
537| #l % [2: @(pi2 ?? r) | skip ]
538| @(π1 (π1 Env))
539| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
540| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
541] qed.
542
543let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es)
544                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx)
545                  (Hdsts:All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn fx. fn_contains … f f' ≝
546match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
547[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
548| cons e et ⇒ λEnv.
549    match dsts return λx. All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
550    [ nil ⇒ λ_.λpf.⊥
551    | cons r rt ⇒ λHdsts,pf.
552        let f' ≝ add_exprs … et ? rt ? f ? in
553        match e return λe.exprtyp_present ? e → fn_env_has … f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
554          let f'' ≝ add_expr … ty e ? f' r in
555            «pi1 … f'', ?»
556        ] (proj1 ?? Env) (π1 Hdsts)
557    ]
558] Env Hdsts pf.
559try (repeat @fn_contains_step @I)
560[ 1,2: normalize in pf; destruct
561| @Env
562| @(fn_con_env … Hr) repeat @fn_contains_step @I
563| @(proj2 … Env)
564| normalize in pf; destruct @e0
565| @(π2 Hdsts)
566] qed.
567
568definition return_ok ≝
569λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
570
571(* Invariants about Cminor statements that we'll need *)
572
573record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
574  si_vars : stmt_vars (Env_has (fx_env fx)) s;
575  si_labels : stmt_labels (present ?? (fx_gotos fx)) s;
576  si_return : return_ok (fx_rettyp fx) s
577}.
578
579definition stmts_inv : fixed → stmt → Prop ≝
580λfx. stmt_P (stmt_inv fx).
581
582(* Trick to avoid multiplying the proof obligations for the non-constant ident cases. *)
583definition expr_is_cst_ident : ∀t. expr t → option ident ≝
584λt,e. match e with
585[ Cst _ c ⇒
586  match c with
587  [ Oaddrsymbol id n ⇒
588    match n with [ O ⇒ Some ? id | _ ⇒ None ? ]
589  | _ ⇒ None ?
590  ]
591| _ ⇒ None ?
592].
593
594(* XXX Work around odd disambiguation errors. *)
595alias id "R_skip" = "cic:/matita/cerco/RTLabs/RTLabs_syntax/statement.con(0,1,0)".
596(* If reenabling tailcalls, change 12 to 14. *)
597alias id "R_return" = "cic:/matita/cerco/RTLabs/RTLabs_syntax/statement.con(0,11,0)".
598
599lemma empty_Cminor_labels_added : ∀fx,s,f'.
600  labels_of s = [ ] → Cminor_labels_added fx s f'.
601#fx #s #f' #E whd >E #l *;
602qed.
603
604lemma equal_Cminor_labels_added : ∀fx,s,s',f.
605  labels_of s = labels_of s' → Cminor_labels_added … s' f →
606  Cminor_labels_added fx s f.
607#fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H
608qed.
609
610lemma Cminor_labels_con : ∀fx,s,f,f'.
611  fn_contains fx f f' →
612  Cminor_labels_added … s f →
613  Cminor_labels_added … s f'.
614#fx #s #f #f' #INC #ADDED
615#l #E
616@(fn_con_labels … INC l (ADDED l E))
617qed.
618
619lemma Cminor_labels_inv : ∀fx,s,s',f.
620  ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'.
621  Cminor_labels_added fx s f →
622  Cminor_labels_added fx s f'.
623#fx #s #s' #f * #f' * #H1 #H2 #H3
624@(Cminor_labels_con … H1) assumption
625qed.
626
627lemma Cminor_labels_sig : ∀fx,s,f.
628  ∀f':Σf':partial_fn fx. fn_contains … f f'.
629  Cminor_labels_added … s f →
630  Cminor_labels_added … s f'.
631#fx #s #f * #f' #H1 @(Cminor_labels_con … H1)
632qed.
633
634discriminator option.
635discriminator DPair.
636
637(* Return statements need a little careful treatment to avoid errors using the
638   invariant about the return type. *)
639
640definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
641  Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝
642λfx,opt_e,f.
643  let f0 ≝ f in
644  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
645  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
646  [ None ⇒ λEnv. «pi1 … f, ?»
647  | Some et ⇒
648    match et return λe.stmts_inv fx (St_return (Some ? e)) → Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f' with
649    [ mk_DPair ty e ⇒ λEnv.
650      match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with
651      [ None ⇒ λH. ⊥
652      | Some t ⇒ λH,R.
653        match R with
654        [ mk_Sig r Hr ⇒
655            let f ≝ add_expr fx ty e ? f «r, ?» in
656            «pi1 … f, ?»
657        ]
658      ] (si_return … (π1 Env)) (pf_result fx f)
659    ]
660  ].
661[ @mk_add_stmt_inv /2 by refl, empty_Cminor_labels_added, fn_con_sig/
662| inversion H #A #B #C destruct
663| @mk_add_stmt_inv
664  [ repeat @fn_contains_step @I
665  | @empty_Cminor_labels_added //
666  ]
667| @(si_vars … (π1 Env))
668| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
669| #l #H @I
670| #l //
671] qed.
672
673(* Record the mapping for a Cminor goto label so that we can put it in the skips
674   for the goto statements later. *)
675
676definition record_goto_label : ∀fx. partial_fn fx → identifier Label → partial_fn fx ≝
677λfx,f,l. mk_partial_fn fx
678  (pf_labgen … f) (pf_reggen … f) (pf_params … f) (pf_locals … f)
679  (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f)
680  (pf_closed … f) (pf_gotos …  f) «add … (pf_labels … f) l (pf_entry … f), ?»
681  (pf_typed … f) (pf_entry … f) (pf_exit … f).
682#l1 #l2 cases (identifier_eq … l2 (pf_entry … f))
683[ #E destruct #L @(pi2 … (pf_entry … f))
684| #NE cases (identifier_eq … l l1)
685  [ #E destruct >lookup_add_hit #E destruct /2/
686  | #NE' >lookup_add_miss [ @(pi2 … (pf_labels … f)) | /2/ ]
687  ]
688] qed.
689
690(* Add a dummy statement for each goto so that we can put the real destination
691   in at the end once we've recorded them all. *)
692
693definition add_goto_dummy : ∀fx. ∀f:partial_fn fx. ∀l. present … (fx_gotos fx) l → Σf':partial_fn fx. fn_contains … f f' ≝
694λfx,f,dest,PR.
695  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
696    (mk_partial_fn fx g (pf_reggen … f)
697                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
698                   (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ?
699                   (mk_goto_map … (add … (pf_gotos … f) l dest) ??)
700                   «pf_labels … f, ?» ?
701                   «l, ?» «pf_exit … f, ?»).
702[ % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
703| @add_statement_inv @I
704| #l1 #l2 cases (identifier_eq … l1 l)
705  [ #E destruct >lookup_add_hit #E destruct @PR
706  | #NE >lookup_add_miss [ @(gm_img … (pf_gotos … f)) | // ]
707  ]
708| #id cases (identifier_eq … id l)
709  [ #E destruct //
710  | #NE whd in ⊢ (% → %); >lookup_add_miss [ >lookup_add_miss [ @(gm_dom … (pf_gotos … f)) | // ] | // ]
711  ]
712| cases (pf_labels … f) #m #PR #l1 #l2 #L @lookup_add_oblivious @(PR … L)
713| @forall_nodes_add //
714| whd >lookup_add_hit % #E destruct
715| @lookup_add_oblivious @(pi2 … (pf_exit …))
716] qed.
717
718(* It's important for correctness that recursive calls to add_stmt happen in
719   reverse order.  This is because Cminor and Clight programs allow goto labels
720   to occur multiple times, but only use the first one to appear in the
721   function.  It would be nice to rule these programs out entirely, but that
722   means establishing and maintaining another invariant on Cminor programs,
723   which I'd like to avoid. *)
724
725let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : Σf':partial_fn fx. add_stmt_inv fx s f f' ≝
726match s return λs.stmts_inv fx s → Σf':partial_fn fx. add_stmt_inv … s f f' with
727[ St_skip ⇒ λ_. «f, ?»
728| St_assign t x e ⇒ λEnv.
729    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
730    «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
731| St_store t e1 e2 ⇒ λEnv.
732    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
733    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
734    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
735    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
736    «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
737| St_call return_opt_id e args ⇒ λEnv.
738    let return_opt_reg ≝
739      match return_opt_id return λo. ? → ? with
740      [ None ⇒ λ_. None ?
741      | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?)
742      ] Env in
743    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
744    let f ≝
745      match expr_is_cst_ident ? e with
746      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
747      | None ⇒
748        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
749        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
750        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
751      ] in
752    «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
753| St_seq s1 s2 ⇒ λEnv.
754    let f2 ≝ add_stmt … s2 ? f in
755    let f1 ≝ add_stmt … s1 ? f2 in
756      «pi1 … f1, ?»
757| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
758    let l_next ≝ pf_entry … f in
759    let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in
760    let l2 ≝ pf_entry … f2 in
761    let f ≝ change_entry … f2 l_next ? in
762    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
763    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
764    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
765    «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
766| St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
767| St_label l s' ⇒ λEnv.
768    let f ≝ add_stmt … s' (π2 Env) f in
769    «record_goto_label … f l, ?»
770| St_goto l ⇒ λEnv.
771    «add_goto_dummy … f l ?, ?»
772| St_cost l s' ⇒ λEnv.
773    let f ≝ add_stmt … s' (π2 Env) f in
774    «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
775] Env.
776try @(π2 Env)
777try @(π1 (π2 Env))
778try @(π2 (π2 Env))
779try @mk_add_stmt_inv
780try (repeat @fn_contains_step @I)
781try (@empty_Cminor_labels_added @refl)
782try (#l #H @I)
783try (#l #H @H)
784try (#l @I)
785[ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl
786| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
787| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
788| #l % [ @(fn_con_env … (pi2 ?? val_reg)) | @(pi2 ?? addr_reg) ] repeat @fn_contains_step @I
789| @sym_eq @(All2_length … (pi2 ?? args_regs))
790| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
791| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
792| #l % try @conj
793  [ @(pi2 ?? fnr)
794  | @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
795  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
796    [ #Env @I
797    | * #retid #retty * #Env #moo %{retty} /2/
798    ]
799  ]
800| #l %
801  [ @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
802  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
803    [ #Env @I
804    | * #retid #retty * #Env #moo %{retty} /2/
805    ]
806  ]
807| @(π1 (π1 (si_vars … (π1 Env))))
808| #l #H cases (Exists_append … H)
809  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
810  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
811  ]
812| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
813| #l #H cases (Exists_append … H)
814  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1))
815  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2))
816  ]
817| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
818| #l whd % [2: @(pi2 ?? r) | skip ]
819| @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
820| cases (pi2 … f) * #INC #ENV #LBLE #LBLA %
821  [ @INC | @ENV | @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ]
822| #l1 * [ #E >E //
823        | @(Cminor_labels_con … (stmt_labels_added ???? (pi2 … f)))
824          % [ // | // | #x #PR @lookup_add_oblivious @PR ]
825        ]
826| @(si_labels … (π1 Env))
827| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
828] qed.
829
830
831
832definition patch_gotos : ∀fx. ∀f:partial_fn fx.
833 (∀l,l'. lookup ?? (pf_gotos … f) l = Some ? l' → present ?? (pf_labels … f) l') →
834 Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l ≝
835λfx,f,PR.
836fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f)
837  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?»)
838  «f, λx,H.H».
839[ #l #PR' @(pi2 … f') @PR'
840| @(pi2 … f') @(PR … H)
841| @(pi2 … (pf_labels … f')) [ @l' | @lookup_lookup_present ]
842| %
843] qed.
844
845definition c2ra_function (*: internal_function → internal_function*) ≝
846λf.
847let labgen0 ≝ new_universe LabelTag in
848let reggen0 ≝ new_universe RegisterTag in
849let cminor_labels ≝ labels_of (f_body f) in
850let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
851let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
852let ❬locals_reggen, result❭ as E3 ≝
853  match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with
854  [ None ⇒ ❬〈locals0, reggen2〉, I❭
855  | Some ty ⇒
856      let 〈r,gen〉 ≝ fresh … reggen2 in
857        mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in
858let locals ≝ \fst locals_reggen in
859let reggen ≝ \snd locals_reggen in
860let 〈l,labgen〉 ≝ fresh … labgen0 in
861let fixed ≝ mk_fixed (set_of_list … (labels_of (f_body f))) env (f_return f) in
862let emptyfn ≝
863  mk_partial_fn fixed
864    labgen
865    reggen
866    params
867    locals
868    result
869    ?
870    (f_stacksize f)
871    (add ?? (empty_map …) l St_return)
872    ?
873    (mk_goto_map ?? (empty_map …) ??)
874    «empty_map …, ?»
875    ?
876    l
877    l in
878let f ≝ add_stmt fixed (f_body f) ? emptyfn in
879let f ≝ patch_gotos … f ? in
880  mk_internal_function
881    (pf_labgen … f)
882    (pf_reggen … f)
883    (match fx_rettyp fixed return λt. match t with [ Some t ⇒ Σr:register. env_has ? r t | _ ⇒ True ] → ? with [ None ⇒ λ_. None ? | Some t ⇒ λR. Some ? 〈(pi1 … R),t〉 ] (pf_result … f))
884    (pf_params … f)
885    (pf_locals … f)
886    (pf_stacksize … f)
887    (pf_graph … f)
888    (pf_closed … f)
889    (pf_typed … f)
890    (pf_entry … f)
891    (pf_exit … f)
892  .
893[ #l1 #l2 #L
894  lapply (gm_img … (pf_gotos … f) … L)
895  whd in match fixed;
896  #PR
897  lapply (in_set_of_list' … PR)
898  @(stmt_labels_added … (pi2 … f))
899| -emptyfn @(stmt_P_mp … (f_inv f))
900  #s * #V #L #R %
901  [ @(stmt_vars_mp … V)
902    #i #t #H cases (Exists_append … H)
903    [ #H1 @(populate_extends … (sym_eq … E2))
904      [ @(populates_env_distinct … (sym_eq … E1)) //
905        @All_alt //
906      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
907      ]
908    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
909    ]
910  | @(stmt_labels_mp … L)
911    #l #H whd in match fixed; @in_set_of_list assumption
912  | cases s in R ⊢ %; //
913  ]
914| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
915  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
916    [ * * | normalize @Exists_append_r ]
917  | (* gave up with     cases (f_return f) in result E3; *)
918    @(match f_return f return λx.∀R:resultok x ((\fst locals_reggen)@params). ❬locals_reggen,R❭ = match x with [None ⇒ ?|Some _ ⇒ ?] → ? with [ None ⇒ λres1.? | Some rty ⇒ λres1.?] result E3)
919    [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
920      @Exists_append_l
921    | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
922      #H' @Exists_append_l %2 @H'
923    ]
924  ]
925| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
926  [ * #E1 #E2 >E2 @I
927  | whd in ⊢ (??%? → ?); #E' destruct (E')
928  ]
929| #id #l #E normalize in E; destruct
930| #id normalize * #H cases (H (refl ??))
931| #l #l' normalize #E destruct
932| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
933  [ * #E1 #E2 >E2 @I
934  | whd in ⊢ (??%? → ?); #E' destruct (E')
935  ]
936| 9,10: whd >lookup_add_hit % #E destruct
937| % @refl
938]
939qed.
940
941definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
942λp.transform_program … p (λ_. transf_fundef … c2ra_function).
943
Note: See TracBrowser for help on using the repository browser.