source: src/Cminor/toRTLabs.ma

Last change on this file was 2992, checked in by campbell, 7 years ago

Add "only one return" invariant to RTLabs functions.

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