Changeset 2335 for src/Cminor

Timestamp:

Sep 20, 2012, 6:57:34 PM (7 years ago)

Author:

campbell

Message:

Deal with goto labels in RTLabs to Cminor by fixing up goto statements
after the main translation to avoid generating extra skips in awkward
locations.

File:

• src/Cminor/toRTLabs.ma (modified) (29 diffs)

src/Cminor/toRTLabs.ma

@@ -5 +5 @@
 
 definition env ≝ identifier_map SymbolTag (register × typ).
-definition label_env ≝ identifier_map Label label.
 definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
 λen,gen. foldr ??
@@ -132 +131 @@
 ] qed.
 
-definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
-λen,gen. foldr ??
- (λid,engen.
-   let 〈en,gen〉 ≝ engen in
-   let 〈r,gen'〉 ≝ fresh … gen in
-     〈add ?? en id r, gen'〉) 〈en, gen〉.
-
-lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
-  populate_label_env lbls u ls = 〈lbls',u'〉 →
-  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
-#ls elim ls
-[ #lbls #u #lbls' #u' #E #l *
-| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
-  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
-  lapply (refl ? (populate_label_env lbls u t))
-  cases (populate_label_env lbls u t) in ⊢ (???% → %);
-  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
-  cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?);
-  #E destruct
-  #l *
-  [ #El <El whd >lookup_add_hit % #Er destruct
-  | #H @lookup_add_oblivious @(IH … E1 ? H)
-  ]
-] qed.
-
-lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
-  populate_label_env lbls u ls = 〈lbls',u'〉 →
-  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
-#ls elim ls
-[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
-| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
-  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
-  lapply (refl ? (populate_label_env lbls u t))
-  cases (populate_label_env lbls u t) in ⊢ (???% → %);
-  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
-  cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?);
-  #E destruct
-  #l #H cases (identifier_eq ? l h)
-  [ #El %1 %1 @El 
-  | #NE cases (IH … E1 l ?)
-    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; //  ]
-  ]
-] qed.
-
-definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
-
 (* Check that the domain of one graph is included in another, for monotonicity
    properties.  Note that we don't say anything about the statements. *)
 definition graph_included : graph statement → graph statement → Prop ≝
-λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
+extends_domain ??.
 
 lemma graph_inc_trans : ∀g1,g2,g3.
   graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
-#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
-
-definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
-
-definition partially_closed : label_env → graph statement → Prop ≝ 
- λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
+@extends_dom_trans
+qed.
+
 
 (* Some data structures for the transformation that remain fixed throughout. *)
 record fixed : Type[0] ≝ {
-  fx_lenv   : label_env;
+  fx_gotos  : identifier_set Label;
   fx_env    : env;
   fx_rettyp : option typ
@@ -202 +152 @@
 λty,env.
   match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ].
+
+(* We put in dummy statements for gotos, then change them afterwards once we
+   know their true destinations.  So first we need a mapping between the dummy
+   CFG nodes and the Cminor destination.  (We'll also keep a mapping of goto
+   labels to their RTLabs statements.) *)
+
+record goto_map (fx:fixed) (g:graph statement) : Type[0] ≝ {
+  gm_map :> identifier_map LabelTag (identifier Label);
+  gm_dom : ∀id. present ?? gm_map id → present ?? g id;
+  gm_img : ∀id,l. lookup … gm_map id = Some ? l → present ?? (fx_gotos fx) l
+}.
 
 (* I'd use a single parametrised definition along with internal_function, but
@@ -214 +175 @@
 ; pf_stacksize : nat
 ; pf_graph     : graph statement
-; pf_closed    : partially_closed (fx_lenv … fx) pf_graph
+; pf_closed    : graph_closed pf_graph
+; pf_gotos     : goto_map fx pf_graph
+; pf_labels    : Σm:identifier_map Label (identifier LabelTag). ∀l,l'. lookup … m l = Some ? l' → present ?? pf_graph l'
 ; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
 ; pf_entry     : Σl:label. present ?? pf_graph l
@@ -223 +186 @@
   λfx,f. env_has (pf_locals fx f @ pf_params fx f).
 
+(* TODO: move or use another definition if there's already one *)
+definition map_extends : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝
+λtag,A,m1,m2. ∀id,a. lookup tag A m1 id = Some A a → lookup tag A m2 id = Some A a.
+
+lemma map_extends_trans : ∀tag,A,m1,m2,m3.
+  map_extends tag A m1 m2 →
+  map_extends tag A m2 m3 →
+  map_extends tag A m1 m3.
+/3/
+qed.
+
 record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
 { fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
 ; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty
+; fn_con_labels : extends_domain … (pf_labels … f1) (pf_labels … f2)
 }.
 
@@ -233 +208 @@
 [ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
 | #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
+| @(extends_dom_trans … (fn_con_labels … H1) (fn_con_labels … H2))
 ] qed.
 
@@ -248 +224 @@
 lemma add_statement_inv : ∀fx,l,s.∀f.
   labels_present (pf_graph fx f) s →
-  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
+  graph_closed (add … (pf_graph … f) l s).
 #fx #l #s #f #p
 #l' #s' #H cases (identifier_eq … l l')
 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
-  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
+  @(labels_P_mp … p) #l0 #H @lookup_add_oblivious @H
 | #NE @(labels_P_mp … (pf_closed … f l' s' ?))
-  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
+  [ #lx #H @lookup_add_oblivious @H
   | >lookup_add_miss in H; /2/
   ]
@@ -279 +255 @@
   mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
-                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
+                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ?
+                (mk_goto_map … (pf_gotos … f) ??) «pf_labels … f, ?» ?
                 «pf_entry … f, ?» «pf_exit … f, ?».
 [ @add_statement_inv @p
+| @gm_img
+| #id #PR @lookup_add_oblivious @(gm_dom … PR)
+| #l1 #l2 #L @lookup_add_oblivious @(pi2 … (pf_labels … f) … L)
 | @forall_nodes_add //
-| 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
-| % [ #l' @lookup_add_oblivious | // ] 
+| 6,7: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
+| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ] 
 ] qed.
 
@@ -295 +275 @@
   mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
-                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
+                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ????
                 «l, ?» «pf_exit … f, ?».
 [ @add_statement_inv @p
+| cases (pf_gotos … f) #m #dom #img %
+  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
+| cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
 | @forall_nodes_add //
 | whd >lookup_add_hit % #E destruct
 | @lookup_add_oblivious @(pi2 … (pf_exit … f))
-| % [ #l' @lookup_add_oblivious | // ]
+| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
 ] qed.
 
@@ -315 +298 @@
     (mk_partial_fn fx g (pf_reggen … f)
                    (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
-                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
+                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ????
                    «l, ?» «pf_exit … f, ?»).
-[ % [ #l' @lookup_add_oblivious | // ]
+[ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
+| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
 | @add_statement_inv @p @(pi2 … (pf_entry …))
-| @forall_nodes_add //
-| whd >lookup_add_hit % #E destruct
-| @lookup_add_oblivious @(pi2 … (pf_exit …))
-] qed.
-
-(* Variants for labels which are (goto) labels *)
-
-lemma add_statement_inv' : ∀fx,l,s.∀f.
-  labels_P (λl. present ?? (pf_graph fx f) l ∨ lpresent (fx_lenv … fx) l) s →
-  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
-#fx #l #s #f #p
-#l' #s' #H cases (identifier_eq … l l')
-[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
-  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
-| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
-  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
-  | >lookup_add_miss in H; /2/
-  ]
-] qed.
-
-definition add_fresh_to_graph' : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx. 
-  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent (fx_lenv … fx) l) (s l)) →
-  (∀l. statement_typed_in … f (s l)) →
-  Σf':partial_fn fx. fn_contains … f f' ≝
-λfx,s,f,p,tp.
-  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
-  let s' ≝ s (pf_entry … f) in
-    (mk_partial_fn fx g (pf_reggen … f)
-                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
-                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
-                   «l, ?» «pf_exit … f, ?»).
-[ % [ #l' @lookup_add_oblivious | // ]
-| @add_statement_inv' @p @(pi2 … (pf_entry …))
+| cases (pf_gotos … f) #m #dom #img %
+  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
 | @forall_nodes_add //
 | whd >lookup_add_hit % #E destruct
@@ -385 +338 @@
     «mk_partial_fn fx
        (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
-       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
+       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?»
   in
     ❬f' , ?(*«r, ?»*)❭.
@@ -392 +345 @@
 | #i #t #r1 #H #L %2 @(pf_envok … f … L)
 | lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
-| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
+| % [ #l // | #r' #ty' #H @extend_typ_env @H | // ]
 ] qed.
 
@@ -437 +390 @@
 ]  qed.
 
-lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
-((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
-∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
-#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
-
-
 lemma choose_regs_length : ∀fx,es,f,p,f',rs.
   choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
@@ -452 +399 @@
   present ?? (pf_graph … f) l →
   present ?? (pf_graph … f') l.
-#fx #f #f' #l * #H1 #H2 @H1 qed.
+#fx #f #f' #l * #H1 #H2 #H3 @H1 qed.
 
 (* Some definitions for the add_stmt function later, which we introduce now so
@@ -460 +407 @@
    up in the graph. *)
 definition Cminor_labels_added ≝ λfx,s,f'.
-∀l. Exists ? (λl'.l=l') (labels_of s) →
-∃l'. lookup ?? (fx_lenv fx) l = Some ? l' ∧ present ?? (pf_graph fx f') l'.
+∀l. Exists ? (λl'.l=l') (labels_of s) → present ?? (pf_labels fx f') l.
 
 record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
@@ -609 +555 @@
 λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
 
+(* Invariants about Cminor statements that we'll need *)
+
 record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
   si_vars : stmt_vars (Env_has (fx_env fx)) s;
-  si_labels : stmt_labels (present ?? (fx_lenv fx)) s;
+  si_labels : stmt_labels (present ?? (fx_gotos fx)) s;
   si_return : return_ok (fx_rettyp fx) s
 }.
@@ -630 +578 @@
 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,11,0)".
 
-lemma lookup_label_rev : ∀lenv,l,l',p.
-  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
-#lenv #l #l' #p
-cut (∃lx. lookup ?? lenv l = Some ? lx)
-[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
-  [ * #H cases (H (refl ??))
-  | #lx #_ %{lx} @refl
-  ]
-| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
-] qed.
-
-lemma lookup_label_rev' : ∀lenv,l,p.
-  lookup ?? lenv l = Some ? (lookup_label lenv l p).
-#lenv #l #p @lookup_label_rev [ @p | @refl ]
-qed.
-
-lemma lookup_label_lpresent : ∀lenv,l,p.
-  lpresent lenv (lookup_label lenv l p).
-#le #l #p whd %{l} @lookup_label_rev'
-qed.
-
 lemma empty_Cminor_labels_added : ∀fx,s,f'.
   labels_of s = [ ] → Cminor_labels_added fx s f'.
@@ -667 +594 @@
   Cminor_labels_added … s f'.
 #fx #s #f #f' #INC #ADDED
-#l #E cases (ADDED l E) #l' * #L #P
-%{l'} % [ @L | @(present_included … P) @INC ]
+#l #E
+@(fn_con_labels … INC l (ADDED l E))
 qed.
 
@@ -676 +603 @@
   Cminor_labels_added fx s f'.
 #fx #s #s' #f * #f' * #H1 #H2 #H3
-#l #E cases (H3 l E) #l' * #L #P
-%{l'} % [ @L | @(present_included … P) @H1 ]
+@(Cminor_labels_con … H1) assumption
 qed.
 
@@ -684 +610 @@
   Cminor_labels_added … s f →
   Cminor_labels_added … s f'.
-#fx #s #f * #f' #H1 #H2
-#l #E cases (H2 l E) #l' * #L #P
-%{l'} % [ @L | @(present_included … P) @H1 ]
+#fx #s #f * #f' #H1 @(Cminor_labels_con … H1)
 qed.
 
@@ -716 +640 @@
     ]
   ].
-[ @mk_add_stmt_inv /2/
+[ @mk_add_stmt_inv /2 by refl, empty_Cminor_labels_added, fn_con_sig/
 | inversion H #A #B #C destruct
 | @mk_add_stmt_inv
@@ -728 +652 @@
 ] qed.
 
+(* Record the mapping for a Cminor goto label so that we can put it in the skips
+   for the goto statements later. *)
+
+definition record_goto_label : ∀fx. partial_fn fx → identifier Label → partial_fn fx ≝
+λfx,f,l. mk_partial_fn fx
+  (pf_labgen … f) (pf_reggen … f) (pf_params … f) (pf_locals … f)
+  (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f)
+  (pf_closed … f) (pf_gotos …  f) «add … (pf_labels … f) l (pf_entry … f), ?»
+  (pf_typed … f) (pf_entry … f) (pf_exit … f).
+#l1 #l2 cases (identifier_eq … l2 (pf_entry … f))
+[ #E destruct #L @(pi2 … (pf_entry … f))
+| #NE cases (identifier_eq … l l1)
+  [ #E destruct >lookup_add_hit #E destruct /2/
+  | #NE' >lookup_add_miss [ @(pi2 … (pf_labels … f)) | /2/ ]
+  ]
+] qed.
+
+(* Add a dummy statement for each goto so that we can put the real destination
+   in at the end once we've recorded them all. *)
+
+definition add_goto_dummy : ∀fx. ∀f:partial_fn fx. ∀l. present … (fx_gotos fx) l → Σf':partial_fn fx. fn_contains … f f' ≝
+λfx,f,dest,PR.
+  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
+    (mk_partial_fn fx g (pf_reggen … f)
+                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
+                   (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ?
+                   (mk_goto_map … (add … (pf_gotos … f) l dest) ??)
+                   «pf_labels … f, ?» ?
+                   «l, ?» «pf_exit … f, ?»).
+[ % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
+| @add_statement_inv @I
+| #l1 #l2 cases (identifier_eq … l1 l)
+  [ #E destruct >lookup_add_hit #E destruct @PR
+  | #NE >lookup_add_miss [ @(gm_img … (pf_gotos … f)) | // ]
+  ]
+| #id cases (identifier_eq … id l)
+  [ #E destruct //
+  | #NE whd in ⊢ (% → %); >lookup_add_miss [ >lookup_add_miss [ @(gm_dom … (pf_gotos … f)) | // ] | // ]
+  ]
+| cases (pf_labels … f) #m #PR #l1 #l2 #L @lookup_add_oblivious @(PR … L)
+| @forall_nodes_add //
+| whd >lookup_add_hit % #E destruct
+| @lookup_add_oblivious @(pi2 … (pf_exit …))
+] qed.
+
+(* It's important for correctness that recursive calls to add_stmt happen in
+   reverse order.  This is because Cminor and Clight programs allow goto labels
+   to occur multiple times, but only use the first one to appear in the
+   function.  It would be nice to rule these programs out entirely, but that
+   means establishing and maintaining another invariant on Cminor programs,
+   which I'd like to avoid. *)
 
 let 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' ≝
@@ -773 +748 @@
 | St_label l s' ⇒ λEnv.
     let f ≝ add_stmt … s' (π2 Env) f in
-    let l' ≝ lookup_label (fx_lenv fx) l ? in
-    «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
+    «record_goto_label … f l, ?»
 | St_goto l ⇒ λEnv.
-    let l' ≝ lookup_label (fx_lenv fx) l ? in
-    «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
+    «add_goto_dummy … f l ?, ?»
 | St_cost l s' ⇒ λEnv.
     let f ≝ add_stmt … s' (π2 Env) f in
@@ -826 +799 @@
 | #l whd % [2: @(pi2 ?? r) | skip ] 
 | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
-| @(pi2 … (pf_entry …))
-| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
-        | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f))
+| cases (pi2 … f) * #INC #ENV #LBLE #LBLA %
+  [ @INC | @ENV | @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ]
+| #l1 * [ #E >E //
+        | @(Cminor_labels_con … (stmt_labels_added ???? (pi2 … f)))
+          % [ // | // | #x #PR @lookup_add_oblivious @PR ]
         ]
 | @(si_labels … (π1 Env))
-| #l1 #H whd %2 @lookup_label_lpresent
-| @(si_labels … (π1 Env))
 | @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
+] qed.
+
+
+
+definition patch_gotos : ∀fx. ∀f:partial_fn fx.
+ (∀l,l'. lookup ?? (pf_gotos … f) l = Some ? l' → present ?? (pf_labels … f) l') →
+ Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l ≝
+λfx,f,PR.
+fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f)
+  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?»)
+  «f, λx,H.H».
+[ #l #PR' @(pi2 … f') @PR'
+| @(pi2 … f') @(PR … H)
+| @(pi2 … (pf_labels … f')) [ @l' | @lookup_lookup_present ]
+| %
 ] qed.
 
@@ -851 +839 @@
 let locals ≝ \fst locals_reggen in
 let reggen ≝ \snd locals_reggen in
-let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
-let 〈l,labgen〉 ≝ fresh … labgen1 in
-let fixed ≝ mk_fixed label_env env (f_return f) in
+let 〈l,labgen〉 ≝ fresh … labgen0 in
+let fixed ≝ mk_fixed (set_of_list … (labels_of (f_body f))) env (f_return f) in
 let emptyfn ≝
   mk_partial_fn fixed
@@ -865 +852 @@
     (add ?? (empty_map …) l St_return)
     ?
+    (mk_goto_map ?? (empty_map …) ??)
+    «empty_map …, ?»
     ?
     l
     l in
 let f ≝ add_stmt fixed (f_body f) ? emptyfn in
+let f ≝ patch_gotos … f ? in
   mk_internal_function
     (pf_labgen … f)
@@ -877 +867 @@
     (pf_stacksize … f)
     (pf_graph … f)
-    ?
+    (pf_closed … f)
     (pf_typed … f)
     (pf_entry … f)
     (pf_exit … f)
   .
-[ #l #s #E @(labels_P_mp … (pf_closed … f l s E))
-  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
-  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ] 
-  #P' @P'
-  | cases (label_env_contents … (sym_eq ??? El) l ?)
-    [ #H @H
-    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
-    | whd >H % #E' destruct (E')
-    ]
-  ]
-  ]
+[ #l1 #l2 #L
+  lapply (gm_img … (pf_gotos … f) … L)
+  whd in match fixed;
+  #PR
+  lapply (in_set_of_list' … PR)
+  @(stmt_labels_added … (pi2 … f))
 | -emptyfn @(stmt_P_mp … (f_inv f))
   #s * #V #L #R %
@@ -905 +890 @@
     ]
   | @(stmt_labels_mp … L)
-    #l #H @(populates_label_env … (sym_eq … El)) @H
+    #l #H whd in match fixed; @in_set_of_list assumption
   | cases s in R ⊢ %; //
   ]
@@ -923 +908 @@
   | whd in ⊢ (??%? → ?); #E' destruct (E')
   ]
+| #id #l #E normalize in E; destruct
+| #id normalize * #H cases (H (refl ??))
+| #l #l' normalize #E destruct
 | #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
   [ * #E1 #E2 >E2 @I
   | whd in ⊢ (??%? → ?); #E' destruct (E')
   ]
-| 6,7: whd >lookup_add_hit % #E destruct
+| 9,10: whd >lookup_add_hit % #E destruct
 | % @refl
 ]