More aggressive elimination of conditional branches during constant

propagation, taking better advantage of inferred constants.
Helps with the compilation of && and || operators.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1987 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 228 insertions, 201 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index 19e5d1a..104aa3b 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -239,7 +239,22 @@ Definition analyze (gapp: global_approx) (f: RTL.function): PMap.t D.t :=
     but not all arguments are known are subject to strength reduction,
     and similarly for the addressing modes of load and store instructions.
     Conditional branches and multi-way branches are statically resolved
-    into [Inop] instructions if possible. Other instructions are unchanged. *)
+    into [Inop] instructions if possible. Other instructions are unchanged.
+
+    In addition, we try to jump over conditionals whose condition can
+    be statically resolved based on the abstract state "after" the
+    instruction that branches to the conditional.  A typical example is:
+<<
+          1: x := 0 and goto 2
+          2: if (x == 0) goto 3 else goto 4
+>>
+    where other instructions branch into 2 with different abstract values
+    for [x].  We transform this code into:
+<<
+          1: x := 0 and goto 3
+          2: if (x == 0) goto 3 else goto 4
+>>
+*)
 
 Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
   match ros with
@@ -262,16 +277,40 @@ Definition const_for_result (a: approx) : option operation :=
   | _ => None
   end.
 
-Definition transf_instr (gapp: global_approx) (app: D.t) (instr: instruction) :=
+Fixpoint successor_rec (n: nat) (f: function) (app: D.t) (pc: node) : node :=
+  match n with
+  | O => pc
+  | Datatypes.S n' =>
+      match f.(fn_code)!pc with
+      | Some (Inop s) =>
+          successor_rec n' f app s
+      | Some (Icond cond args s1 s2) =>
+          match eval_static_condition cond (approx_regs app args) with
+          | Some b => if b then s1 else s2
+          | None => pc
+          end
+      | _ => pc
+      end
+  end.
+
+Definition num_iter := 10%nat.
+
+Definition successor (f: function) (app: D.t) (pc: node) : node :=
+  successor_rec num_iter f app pc.
+
+Definition transf_instr (gapp: global_approx) (f: function) (apps: PMap.t D.t)
+                       (pc: node) (instr: instruction) :=
+  let app := apps!!pc in
   match instr with
   | Iop op args res s =>
       let a := eval_static_operation op (approx_regs app args) in
+      let s' := successor f (D.set res a app) s in
       match const_for_result a with
       | Some cop =>
-          Iop cop nil res s
+          Iop cop nil res s'
       | None =>
           let (op', args') := op_strength_reduction op args (approx_regs app args) in
-          Iop op' args' res s
+          Iop op' args' res s'
       end
   | Iload chunk addr args dst s =>
       let a := eval_static_load gapp chunk
@@ -314,8 +353,8 @@ Definition transf_instr (gapp: global_approx) (app: D.t) (instr: instruction) :=
       instr
   end.
 
-Definition transf_code (gapp: global_approx) (app: PMap.t D.t) (instrs: code) : code :=
-  PTree.map (fun pc instr => transf_instr gapp app!!pc instr) instrs.
+Definition transf_code (gapp: global_approx) (f: function) (app: PMap.t D.t) (instrs: code) : code :=
+  PTree.map (transf_instr gapp f app) instrs.
 
 Definition transf_function (gapp: global_approx) (f: function) : function :=
   let approxs := analyze gapp f in
@@ -323,7 +362,7 @@ Definition transf_function (gapp: global_approx) (f: function) : function :=
     f.(fn_sig)
     f.(fn_params)
     f.(fn_stacksize)
-    (transf_code gapp approxs f.(fn_code))
+    (transf_code gapp f approxs f.(fn_code))
     f.(fn_entrypoint).
 
 Definition transf_fundef (gapp: global_approx) (fd: fundef) : fundef :=
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 406e613..8228493 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -324,109 +324,6 @@ Proof.
   intros; red; intros. exploit B; eauto. intros [P Q]. inv Q.
 Qed.
 
-(**********************
-Definition mem_match_approx_gen (g: genv) (ga: global_approx) (m: mem) : Prop :=
-  forall id il b,
-  ga!id = Some il -> Genv.find_symbol g id = Some b ->
-  Genv.load_store_init_data ge m b 0 il /\
-  Mem.valid_block m b /\
-  (forall ofs, ~Mem.perm m b ofs Max Writable).
-
-Lemma mem_match_approx_alloc_variables:
-  forall vl g ga m m',
-  mem_match_approx_gen g ga m ->
-  Genv.genv_nextvar g = Mem.nextblock m ->
-  Genv.alloc_variables ge m vl = Some m' ->
-  mem_match_approx_gen (Genv.add_variables g vl) (make_global_approx ga vl) m'.
-Proof.
-  induction vl; simpl; intros.
-(* base case *)
-  inv H1. auto.
-(* inductive case *)
-  destruct a as [id gv].
-  set (ga1 := if gv.(gvar_readonly) && negb gv.(gvar_volatile)
-        then PTree.set id gv.(gvar_init) ga
-        else PTree.remove id ga).
-  revert H1. unfold Genv.alloc_variable. simpl.
-  set (il := gvar_init gv) in *.
-  set (sz := Genv.init_data_list_size il) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b]_eqn.
-  destruct (Genv.store_zeros m1 b sz) as [m2|]_eqn; try congruence.
-  destruct (Genv.store_init_data_list ge m2 b 0 il) as [m3|]_eqn; try congruence.
-  destruct (Mem.drop_perm m3 b 0 sz (Genv.perm_globvar gv)) as [m4|]_eqn; try congruence.
-  intros. 
-  exploit Mem.alloc_result; eauto. intro NB. 
-  assert (NB': Mem.nextblock m4 = Mem.nextblock m1).
-  rewrite (Mem.nextblock_drop _ _ _ _ _ _ Heqo1).
-  rewrite (Genv.store_init_data_list_nextblock _ _ _ _ _ Heqo0).
-  rewrite (Genv.store_zeros_nextblock _ _ _ Heqo). 
-  auto.
-  apply IHvl with m4. 
-  (* mem_match_approx for intermediate state *)
-  red; intros.
-  unfold Genv.find_symbol in H3. simpl in H3. 
-  rewrite H0 in H3. rewrite <- NB in H3. 
-  assert (EITHER: id0 <> id /\ ga!id0 = Some il0
-       \/ id0 = id /\ il0 = il /\ gvar_readonly gv = true /\ gvar_volatile gv = false).
-  unfold ga1 in H2. destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn. 
-  rewrite PTree.gsspec in H2. destruct (peq id0 id).
-  inv H2. right. split; auto. split; auto. 
-  destruct (gvar_readonly gv); simpl in Heqb1; try discriminate.
-  destruct (gvar_volatile gv); simpl in Heqb1; try discriminate.
-  auto. auto.
-  rewrite PTree.grspec in H2. destruct (PTree.elt_eq id0 id); try discriminate.
-  auto.   
-  destruct EITHER as [[A B] | [A [B [C D]]]].
-  (* older blocks *)
-  rewrite PTree.gso in H3; auto. exploit H; eauto. intros [P [Q R]].
-  assert (b0 <> b). eapply Mem.valid_not_valid_diff; eauto with mem.
-  split. apply Genv.load_store_init_data_invariant with m; auto. 
-  intros. transitivity (Mem.load chunk m3 b0 ofs). eapply Mem.load_drop; eauto.
-  transitivity (Mem.load chunk m2 b0 ofs). eapply Genv.store_init_data_list_outside; eauto.
-  transitivity (Mem.load chunk m1 b0 ofs). eapply Genv.store_zeros_outside; eauto.
-  eapply Mem.load_alloc_unchanged; eauto.  
-  split. red. rewrite NB'.  change (Mem.valid_block m1 b0). eauto with mem.
-  intros; red; intros. elim (R ofs). 
-  eapply Mem.perm_alloc_4; eauto.
-  rewrite Genv.store_zeros_perm; [idtac|eauto].
-  rewrite Genv.store_init_data_list_perm; [idtac|eauto].
-  eapply Mem.perm_drop_4; eauto.
-  (* same block *)
-  subst id0 il0. rewrite PTree.gss in H3. injection H3; intro EQ; subst b0.
-  unfold Genv.perm_globvar in Heqo1.
-  rewrite D in Heqo1. rewrite C in Heqo1.
-  split. apply Genv.load_store_init_data_invariant with m3.
-  intros. eapply Mem.load_drop; eauto. do 3 right. auto with mem. 
-  eapply Genv.store_init_data_list_charact; eauto. 
-  split. red. rewrite NB'. change (Mem.valid_block m1 b). eauto with mem.
-  intros; red; intros. 
-  assert (0 <= ofs < sz).
-    eapply Mem.perm_alloc_3; eauto.
-    rewrite Genv.store_zeros_perm; [idtac|eauto].
-    rewrite Genv.store_init_data_list_perm; [idtac|eauto].
-    eapply Mem.perm_drop_4; eauto.
-  assert (PO: perm_order Readable Writable).
-    eapply Mem.perm_drop_2; eauto. 
-  inv PO. 
-  (* nextvar hyp *)
-  simpl. rewrite NB'. rewrite (Mem.nextblock_alloc _ _ _ _ _ Heqp).
-  unfold block in *; omega.
-  (* alloc vars hyp *)
-  auto.
-Qed.
-
-Theorem mem_match_approx_init:
-  forall m, Genv.init_mem prog = Some m -> mem_match_approx m.
-Proof.
-  intros. unfold Genv.init_mem in H. 
-  eapply mem_match_approx_alloc_variables; eauto.
-(* mem_match_approx on empty list *)
-  red; intros. rewrite PTree.gempty in H0. discriminate.
-(* nextvar *)
-  rewrite Genv.add_functions_nextvar. auto.
-Qed.
-********************************)
-
 End ANALYSIS.
 
 (** * Correctness of the code transformation *)
@@ -539,15 +436,48 @@ Proof.
   simpl. congruence.
 Qed.
 
+Inductive match_pc (f: function) (app: D.t): nat -> node -> node -> Prop :=
+  | match_pc_base: forall n pc,
+      match_pc f app n pc pc
+  | match_pc_nop: forall n pc s pcx,
+      f.(fn_code)!pc = Some (Inop s) ->
+      match_pc f app n s pcx ->
+      match_pc f app (Datatypes.S n) pc pcx
+  | match_pc_cond: forall n pc cond args s1 s2 b,
+      f.(fn_code)!pc = Some (Icond cond args s1 s2) ->
+      eval_static_condition cond (approx_regs app args) = Some b ->
+      match_pc f app (Datatypes.S n) pc (if b then s1 else s2).
+
+Lemma match_successor_rec:
+  forall f app n pc, match_pc f app n pc (successor_rec n f app pc).
+Proof.
+  induction n; simpl; intros.
+  apply match_pc_base.
+  destruct (fn_code f)!pc as [i|]_eqn; try apply match_pc_base.
+  destruct i; try apply match_pc_base.
+  eapply match_pc_nop; eauto. 
+  destruct (eval_static_condition c (approx_regs app l)) as [b|]_eqn.
+  eapply match_pc_cond; eauto.
+  apply match_pc_base.
+Qed.
+
+Lemma match_successor:
+  forall f app pc, match_pc f app num_iter pc (successor f app pc).
+Proof.
+  unfold successor; intros. apply match_successor_rec.
+Qed.
+
 (** The proof of semantic preservation is a simulation argument
-  based on diagrams of the following form:
+  based on "option" diagrams of the following form:
 <<
-           st1 --------------- st2
-            |                   |
-           t|                   |t
-            |                   |
-            v                   v
-           st1'--------------- st2'
+                 n
+       st1 --------------- st2
+        |                   |
+       t|                   |t or (? and n' < n)
+        |                   |
+        v                   v
+       st1'--------------- st2'
+                 n'
 >>
   The left vertical arrow represents a transition in the
   original RTL code.  The top horizontal bar is the [match_states]
@@ -573,24 +503,26 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop :=
         (Stackframe res f sp pc rs)
         (Stackframe res (transf_function gapp f) sp pc rs').
 
-Inductive match_states: state -> state -> Prop :=
+Inductive match_states: nat -> state -> state -> Prop :=
   | match_states_intro:
-      forall s sp pc rs m f s' rs' m'
-           (MATCH: regs_match_approx sp (analyze gapp f)!!pc rs)
+      forall s sp pc rs m f s' pc' rs' m' app n
+           (MATCH1: regs_match_approx sp app rs)
+           (MATCH2: regs_match_approx sp (analyze gapp f)!!pc rs)
            (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
+           (PC: match_pc f app n pc pc')
            (REGS: regs_lessdef rs rs')
            (MEM: Mem.extends m m'),
-      match_states (State s f sp pc rs m)
-                   (State s' (transf_function gapp f) sp pc rs' m')
+      match_states n (State s f sp pc rs m)
+                    (State s' (transf_function gapp f) sp pc' rs' m')
   | match_states_call:
       forall s f args m s' args' m'
            (GMATCH: mem_match_approx m)
            (STACKS: list_forall2 match_stackframes s s')
            (ARGS: Val.lessdef_list args args')
            (MEM: Mem.extends m m'),
-      match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef gapp f) args' m')
+      match_states O (Callstate s f args m)
+                    (Callstate s' (transf_fundef gapp f) args' m')
   | match_states_return:
       forall s v m s' v' m'
            (GMATCH: mem_match_approx m)
@@ -598,16 +530,40 @@ Inductive match_states: state -> state -> Prop :=
            (RES: Val.lessdef v v')
            (MEM: Mem.extends m m'),
       list_forall2 match_stackframes s s' ->
-      match_states (Returnstate s v m)
-                   (Returnstate s' v' m').
+      match_states O (Returnstate s v m)
+                    (Returnstate s' v' m').
+
+Lemma match_states_succ:
+  forall s f sp pc2 rs m s' rs' m' pc1 i,
+  f.(fn_code)!pc1 = Some i ->
+  In pc2 (successors_instr i) ->
+  regs_match_approx sp (transfer gapp f pc1 (analyze gapp f)!!pc1) rs ->
+  mem_match_approx m ->
+  list_forall2 match_stackframes s s' ->
+  regs_lessdef rs rs' ->
+  Mem.extends m m' ->
+  match_states O (State s f sp pc2 rs m)
+                (State s' (transf_function gapp f) sp pc2 rs' m').
+Proof.
+  intros. 
+  assert (regs_match_approx sp (analyze gapp f)!!pc2 rs).
+    eapply analyze_correct_1; eauto.
+  apply match_states_intro with (app := (analyze gapp f)!!pc2); auto.
+  constructor.
+Qed.
+
+Lemma transf_instr_at:
+  forall f pc i,
+  f.(fn_code)!pc = Some i ->
+  (transf_function gapp f).(fn_code)!pc = Some(transf_instr gapp f (analyze gapp f) pc i).
+Proof.
+  intros. simpl. unfold transf_code. rewrite PTree.gmap. rewrite H. auto. 
+Qed.
 
 Ltac TransfInstr :=
   match goal with
-  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_function gapp f).(fn_code)!pc = Some(transf_instr gapp (analyze gapp f)!!pc instr));
-      [ simpl transf_instr
-      | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
-        unfold option_map; rewrite H1; reflexivity ]
+  | H: (PTree.get ?pc (fn_code ?f) = Some ?instr) |- _ =>
+      generalize (transf_instr_at _ _ _ H); simpl
   end.
 
 (** The proof of simulation proceeds by case analysis on the transition
@@ -616,49 +572,64 @@ Ltac TransfInstr :=
 Lemma transf_step_correct:
   forall s1 t s2,
   step ge s1 t s2 ->
-  forall s1' (MS: match_states s1 s1'),
-  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
+  forall n1 s1' (MS: match_states n1 s1 s1'),
+  (exists n2, exists s2', step tge s1' t s2' /\ match_states n2 s2 s2')
+  \/ (exists n2, n2 < n1 /\ t = E0 /\ match_states n2 s2 s1')%nat.
 Proof.
-  induction 1; intros; inv MS.
+  induction 1; intros; inv MS; try (inv PC; try congruence).
 
-  (* Inop *)
-  exists (State s' (transf_function gapp f) sp pc' rs' m'); split.
-  TransfInstr; intro. eapply exec_Inop; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1 with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. auto.
+  (* Inop, preserved *)
+  rename pc'0 into pc. TransfInstr; intro.
+  left; econstructor; econstructor; split.
+  eapply exec_Inop; eauto.
+  eapply match_states_succ; eauto. simpl; auto.
+  unfold transfer; rewrite H. auto. 
+
+  (* Inop, skipped over *)
+  rewrite H0 in H; inv H. 
+  right; exists n; split. omega. split. auto.
+  apply match_states_intro with app; auto.
+  eapply analyze_correct_1; eauto. simpl; auto. 
+  unfold transfer; rewrite H0. auto. 
 
   (* Iop *)
-  TransfInstr.
-  set (a := eval_static_operation op (approx_regs (analyze gapp f)#pc args)).
+  rename pc'0 into pc. TransfInstr.
+  set (app_before := (analyze gapp f)#pc).
+  set (a := eval_static_operation op (approx_regs app_before args)).
+  set (app_after := D.set res a app_before).
   assert (VMATCH: val_match_approx ge sp a v).  
     eapply eval_static_operation_correct; eauto.
     apply approx_regs_val_list; auto.
-  assert (MATCH': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v).
+  assert (MATCH': regs_match_approx sp app_after rs#res <- v).
+    apply regs_match_approx_update; auto.
+  assert (MATCH'': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v).
     eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
-    unfold transfer; rewrite H. 
-    apply regs_match_approx_update; auto. 
+    unfold transfer; rewrite H. auto.  
   destruct (const_for_result a) as [cop|]_eqn; intros.
   (* constant is propagated *)
-  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v) m'); split.
+  left; econstructor; econstructor; split.
   eapply exec_Iop; eauto. 
   eapply const_for_result_correct; eauto.
-  econstructor; eauto. 
+  apply match_states_intro with app_after; auto.
+  apply match_successor. 
   apply set_reg_lessdef; auto.
   (* operator is strength-reduced *)
-  exploit op_strength_reduction_correct. eexact MATCH. reflexivity. eauto. 
-  destruct (op_strength_reduction op args (approx_regs (analyze gapp f) # pc args)) as [op' args'].
+  exploit op_strength_reduction_correct. eexact MATCH2. reflexivity. eauto. 
+  fold app_before.
+  destruct (op_strength_reduction op args (approx_regs app_before args)) as [op' args'].
   intros [v' [EV' LD']].
   assert (EV'': exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v'').
   eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto.
   destruct EV'' as [v'' [EV'' LD'']].
-  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v'') m'); split.
-  econstructor. eauto. rewrite <- EV''. apply eval_operation_preserved. exact symbols_preserved.
-  econstructor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
+  left; econstructor; econstructor; split.
+  eapply exec_Iop; eauto.
+  erewrite eval_operation_preserved. eexact EV''. exact symbols_preserved.
+  apply match_states_intro with app_after; auto.
+  apply match_successor.
+  apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
 
   (* Iload *)
-  TransfInstr. 
+  rename pc'0 into pc. TransfInstr. 
   set (ap1 := eval_static_addressing addr
                (approx_regs (analyze gapp f) # pc args)).
   set (ap2 := eval_static_load gapp chunk ap1).
@@ -667,18 +638,16 @@ Proof.
     eapply approx_regs_val_list; eauto.
   assert (VM2: val_match_approx ge sp ap2 v).
     eapply eval_static_load_sound; eauto.
-  assert (MATCH': regs_match_approx sp (analyze gapp f) # pc' rs # dst <- v).
-    eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
-    unfold transfer; rewrite H. 
-    apply regs_match_approx_update; auto. 
   destruct (const_for_result ap2) as [cop|]_eqn; intros.
   (* constant-propagated *)
-  exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v) m'); split.
+  left; econstructor; econstructor; split.
   eapply exec_Iop; eauto. eapply const_for_result_correct; eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
+  eapply match_states_succ; eauto. simpl; auto.
+  unfold transfer; rewrite H. apply regs_match_approx_update; auto.
+  apply set_reg_lessdef; auto.
   (* strength-reduced *)
   generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
-                  MATCH addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+                  MATCH2 addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
   destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args'].
   rewrite H0. intros P.
   assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
@@ -687,15 +656,16 @@ Proof.
   assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
     rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
   exploit Mem.loadv_extends; eauto. intros [v' [D E]].
-  exists (State s' (transf_function gapp f) sp pc' (rs'#dst <- v') m'); split.
+  left; econstructor; econstructor; split.
   eapply exec_Iload; eauto.
-  econstructor; eauto. 
-  apply set_reg_lessdef; auto. 
+  eapply match_states_succ; eauto. simpl; auto.
+  unfold transfer; rewrite H. apply regs_match_approx_update; auto.
+  apply set_reg_lessdef; auto.
 
   (* Istore *)
-  TransfInstr.
+  rename pc'0 into pc. TransfInstr.
   generalize (addr_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
-                  MATCH addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+                  MATCH2 addr args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
   destruct (addr_strength_reduction addr args (approx_regs (analyze gapp f) # pc args)) as [addr' args'].
   intros P Q. rewrite H0 in P.
   assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
@@ -704,17 +674,17 @@ Proof.
   assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
     rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
   exploit Mem.storev_extends; eauto. intros [m2' [D E]].
-  exists (State s' (transf_function gapp f) sp pc' rs' m2'); split.
+  left; econstructor; econstructor; split.
   eapply exec_Istore; eauto.
-  econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
+  eapply match_states_succ; eauto. simpl; auto.
   unfold transfer; rewrite H. auto. 
   eapply mem_match_approx_store; eauto.
 
   (* Icall *)
+  rename pc'0 into pc.
   exploit transf_ros_correct; eauto. intro FIND'.
   TransfInstr; intro.
-  econstructor; split.
+  left; econstructor; econstructor; split.
   eapply exec_Icall; eauto. apply sig_function_translated; auto.
   constructor; auto. constructor; auto.
   econstructor; eauto. 
@@ -727,39 +697,39 @@ Proof.
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   exploit transf_ros_correct; eauto. intros FIND'.
   TransfInstr; intro.
-  econstructor; split.
+  left; econstructor; econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
   constructor; auto. 
   eapply mem_match_approx_free; eauto.
   apply regs_lessdef_regs; auto. 
 
   (* Ibuiltin *)
+  rename pc'0 into pc.
 Opaque builtin_strength_reduction.
   destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args']_eqn.
   generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
-                  MATCH ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0).
+                  MATCH2 ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0).
   rewrite Heqp. intros P.
   exploit external_call_mem_extends; eauto. 
   instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto.
   intros [v' [m2' [A [B [C D]]]]].
-  exists (State s' (transf_function gapp f) sp pc' (rs'#res <- v') m2'); split.
+  left; econstructor; econstructor; split.
   eapply exec_Ibuiltin. TransfInstr. rewrite Heqp. eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
-  econstructor; eauto. 
-  eapply analyze_correct_1; eauto. simpl; auto. 
+  eapply match_states_succ; eauto. simpl; auto.
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
   eapply mem_match_approx_extcall; eauto. 
   apply set_reg_lessdef; auto.
 
-  (* Icond *)
-  TransfInstr. 
+  (* Icond, preserved *)
+  rename pc'0 into pc. TransfInstr. 
   generalize (cond_strength_reduction_correct ge sp (analyze gapp f)#pc rs m
-                    MATCH cond args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
+                    MATCH2 cond args (approx_regs (analyze gapp f) # pc args) (refl_equal _)).
   destruct (cond_strength_reduction cond args (approx_regs (analyze gapp f) # pc args)) as [cond' args'].
-  intros EV1. 
-  exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. 
+  intros EV1 TCODE.
+  left; exists O; exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. 
   destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) as []_eqn.
   assert (eval_condition cond rs ## args m = Some b0).
     eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto.
@@ -767,28 +737,39 @@ Opaque builtin_strength_reduction.
   destruct b; eapply exec_Inop; eauto. 
   eapply exec_Icond; eauto.
   eapply eval_condition_lessdef with (vl1 := rs##args'); eauto. eapply regs_lessdef_regs; eauto. congruence.
-  econstructor; eauto. 
-  eapply analyze_correct_1; eauto. destruct b; simpl; auto. 
-  unfold transfer; rewrite H. auto. 
+  eapply match_states_succ; eauto. 
+  destruct b; simpl; auto.
+  unfold transfer; rewrite H. auto.
+
+  (* Icond, skipped over *)
+  rewrite H1 in H; inv H. 
+  assert (eval_condition cond rs ## args m = Some b0).
+    eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto.
+  assert (b = b0) by congruence. subst b0.
+  right; exists n; split. omega. split. auto. 
+  assert (MATCH': regs_match_approx sp (analyze gapp f) # (if b then ifso else ifnot) rs).
+    eapply analyze_correct_1; eauto. destruct b; simpl; auto.
+    unfold transfer; rewrite H1; auto.
+  econstructor; eauto. constructor. 
 
   (* Ijumptable *)
+  rename pc'0 into pc.
   assert (A: (fn_code (transf_function gapp f))!pc = Some(Ijumptable arg tbl)
              \/ (fn_code (transf_function gapp f))!pc = Some(Inop pc')).
   TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) as []_eqn; auto.
-  generalize (MATCH arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. 
+  generalize (MATCH2 arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. 
   simpl. intro EQ; inv EQ. rewrite H1. auto.
   assert (B: rs'#arg = Vint n).
   generalize (REGS arg); intro LD; inv LD; congruence.
-  exists (State s' (transf_function gapp f) sp pc' rs' m'); split.
-  destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. 
-  econstructor; eauto.
-  eapply analyze_correct_1; eauto.
+  left; exists O; exists (State s' (transf_function gapp f) sp pc' rs' m'); split.
+  destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto.
+  eapply match_states_succ; eauto.
   simpl. eapply list_nth_z_in; eauto.
   unfold transfer; rewrite  H; auto.
 
   (* Ireturn *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
-  exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split.
+  left; exists O; exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split.
   eapply exec_Ireturn; eauto. TransfInstr; auto.
   constructor; auto.
   eapply mem_match_approx_free; eauto.
@@ -798,17 +779,19 @@ Opaque builtin_strength_reduction.
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
   intros [m2' [A B]].
   simpl. unfold transf_function.
-  econstructor; split.
+  left; exists O; econstructor; split.
   eapply exec_function_internal; simpl; eauto.
   simpl. econstructor; eauto.
   apply analyze_correct_3; auto.
+  apply analyze_correct_3; auto.
   eapply mem_match_approx_alloc; eauto.
+  instantiate (1 := f). constructor.
   apply init_regs_lessdef; auto.
 
   (* external function *)
   exploit external_call_mem_extends; eauto. 
   intros [v' [m2' [A [B [C D]]]]].
-  simpl. econstructor; split.
+  simpl. left; econstructor; econstructor; split.
   eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
@@ -816,19 +799,19 @@ Opaque builtin_strength_reduction.
   eapply mem_match_approx_extcall; eauto.
 
   (* return *)
-  inv H3. inv H1. 
-  econstructor; split.
+  inv H4. inv H1. 
+  left; exists O; econstructor; split.
   eapply exec_return; eauto. 
-  econstructor; eauto. apply set_reg_lessdef; auto. 
+  econstructor; eauto. constructor. apply set_reg_lessdef; auto. 
 Qed.
 
 Lemma transf_initial_states:
   forall st1, initial_state prog st1 ->
-  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+  exists n, exists st2, initial_state tprog st2 /\ match_states n st1 st2.
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef gapp f) nil m0); split.
+  exists O; exists (Callstate nil (transf_fundef gapp f) nil m0); split.
   econstructor; eauto.
   apply Genv.init_mem_transf; auto.
   replace (prog_main tprog) with (prog_main prog).
@@ -841,8 +824,8 @@ Proof.
 Qed.
 
 Lemma transf_final_states:
-  forall st1 st2 r, 
-  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+  forall n st1 st2 r, 
+  match_states n st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
   intros. inv H0. inv H. inv STACKS. inv RES. constructor. 
 Qed.
@@ -853,11 +836,16 @@ Qed.
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
-  eapply forward_simulation_step.
-  eexact symbols_preserved.
+  eapply Forward_simulation with (fsim_order := lt); simpl.
+  apply lt_wf. 
   eexact transf_initial_states.
   eexact transf_final_states.
-  exact transf_step_correct. 
+  fold ge; fold tge. intros. 
+    exploit transf_step_correct; eauto. 
+    intros [ [n2 [s2' [A B]]] | [n2 [A [B C]]]].
+    exists n2; exists s2'; split; auto. left; apply plus_one; auto.
+    exists n2; exists s2; split; auto. right; split; auto. subst t; apply star_refl. 
+  eexact symbols_preserved.
 Qed.
 
 End PRESERVATION.