Refactoring of Constprop and Constpropproof into a machine-dependent part and a machine-independent part.

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

2 files changed, 680 insertions, 0 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
new file mode 100644
index 0000000..cccce9a
--- /dev/null
+++ b/backend/Constprop.v
@@ -0,0 +1,235 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Constant propagation over RTL.  This is one of the optimizations
+  performed at RTL level.  It proceeds by a standard dataflow analysis
+  and the corresponding code rewriting. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Lattice.
+Require Import Kildall.
+Require Import ConstpropOp.
+
+(** * Static analysis *)
+
+(** The type [approx] of compile-time approximations of values is
+  defined in the machine-dependent part [ConstpropOp]. *)
+
+(** We equip this type of approximations with a semi-lattice structure.
+  The ordering is inclusion between the sets of values denoted by
+  the approximations. *)
+
+Module Approx <: SEMILATTICE_WITH_TOP.
+  Definition t := approx.
+  Definition eq (x y: t) := (x = y).
+  Definition eq_refl: forall x, eq x x := (@refl_equal t).
+  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
+  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
+  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
+  Proof.
+    decide equality.
+    apply Int.eq_dec.
+    apply Float.eq_dec.
+    apply Int.eq_dec.
+    apply ident_eq.
+  Qed.
+  Definition beq (x y: t) := if eq_dec x y then true else false.
+  Lemma beq_correct: forall x y, beq x y = true -> x = y.
+  Proof.
+    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
+  Qed.
+  Definition ge (x y: t) : Prop :=
+    x = Unknown \/ y = Novalue \/ x = y.
+  Lemma ge_refl: forall x y, eq x y -> ge x y.
+  Proof.
+    unfold eq, ge; tauto.
+  Qed.
+  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Proof.
+    unfold ge; intuition congruence.
+  Qed.
+  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
+  Proof.
+    unfold eq, ge; intros; congruence.
+  Qed.
+  Definition bot := Novalue.
+  Definition top := Unknown.
+  Lemma ge_bot: forall x, ge x bot.
+  Proof.
+    unfold ge, bot; tauto.
+  Qed.
+  Lemma ge_top: forall x, ge top x.
+  Proof.
+    unfold ge, bot; tauto.
+  Qed.
+  Definition lub (x y: t) : t :=
+    if eq_dec x y then x else
+    match x, y with
+    | Novalue, _ => y
+    | _, Novalue => x
+    | _, _ => Unknown
+    end.
+  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
+  Proof.
+    unfold lub, eq; intros.
+    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
+    destruct x; destruct y; auto.
+  Qed.
+  Lemma ge_lub_left: forall x y, ge (lub x y) x.
+  Proof.
+    unfold lub; intros.
+    case (eq_dec x y); intro.
+    apply ge_refl. apply eq_refl.
+    destruct x; destruct y; unfold ge; tauto.
+  Qed.
+End Approx.
+
+Module D := LPMap Approx.
+
+(** The transfer function for the dataflow analysis is straightforward:
+  for [Iop] instructions, we set the approximation of the destination
+  register to the result of executing abstractly the operation;
+  for [Iload] and [Icall], we set the approximation of the destination
+  to [Unknown]. *)
+
+Definition approx_reg (app: D.t) (r: reg) := 
+  D.get r app.
+
+Definition approx_regs (app: D.t) (rl: list reg):=
+  List.map (approx_reg app) rl.
+
+Definition transfer (f: function) (pc: node) (before: D.t) :=
+  match f.(fn_code)!pc with
+  | None => before
+  | Some i =>
+      match i with
+      | Inop s =>
+          before
+      | Iop op args res s =>
+          let a := eval_static_operation op (approx_regs before args) in
+          D.set res a before
+      | Iload chunk addr args dst s =>
+          D.set dst Unknown before
+      | Istore chunk addr args src s =>
+          before
+      | Icall sig ros args res s =>
+          D.set res Unknown before
+      | Itailcall sig ros args =>
+          before
+(*
+      | Ialloc arg res s =>
+          D.set res Unknown before
+*)
+      | Icond cond args ifso ifnot =>
+          before
+      | Ireturn optarg =>
+          before
+      end
+  end.
+
+(** The static analysis itself is then an instantiation of Kildall's
+  generic solver for forward dataflow inequations. [analyze f]
+  returns a mapping from program points to mappings of pseudo-registers
+  to approximations.  It can fail to reach a fixpoint in a reasonable
+  number of iterations, in which case [None] is returned. *)
+
+Module DS := Dataflow_Solver(D)(NodeSetForward).
+
+Definition analyze (f: RTL.function): PMap.t D.t :=
+  match DS.fixpoint (successors f) (transfer f) 
+                    ((f.(fn_entrypoint), D.top) :: nil) with
+  | None => PMap.init D.top
+  | Some res => res
+  end.
+
+(** * Code transformation *)
+
+(** The code transformation proceeds instruction by instruction.
+    Operators whose arguments are all statically known are turned
+    into ``load integer constant'', ``load float constant'' or
+    ``load symbol address'' operations.  Operators for which some
+    but not all arguments are known are subject to strength reduction,
+    and similarly for the addressing modes of load and store instructions.
+    Other instructions are unchanged. *)
+
+Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
+  match ros with
+  | inl r =>
+      match D.get r app with
+      | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
+      | _ => ros
+      end
+  | inr s => ros
+  end.
+
+Definition transf_instr (app: D.t) (instr: instruction) :=
+  match instr with
+  | Iop op args res s =>
+      match eval_static_operation op (approx_regs app args) with
+      | I n =>
+          Iop (Ointconst n) nil res s
+      | F n =>
+          Iop (Ofloatconst n) nil res s
+      | S symb ofs =>
+          Iop (Oaddrsymbol symb ofs) nil res s
+      | _ =>
+          let (op', args') := op_strength_reduction (approx_reg app) op args in
+          Iop op' args' res s
+      end
+  | Iload chunk addr args dst s =>
+      let (addr', args') := addr_strength_reduction (approx_reg app) addr args in
+      Iload chunk addr' args' dst s      
+  | Istore chunk addr args src s =>
+      let (addr', args') := addr_strength_reduction (approx_reg app) addr args in
+      Istore chunk addr' args' src s      
+  | Icall sig ros args res s =>
+      Icall sig (transf_ros app ros) args res s
+  | Itailcall sig ros args =>
+      Itailcall sig (transf_ros app ros) args
+  | Icond cond args s1 s2 =>
+      match eval_static_condition cond (approx_regs app args) with
+      | Some b =>
+          if b then Inop s1 else Inop s2
+      | None =>
+          let (cond', args') := cond_strength_reduction (approx_reg app) cond args in
+          Icond cond' args' s1 s2
+      end
+  | _ =>
+      instr
+  end.
+
+Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
+  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
+
+Definition transf_function (f: function) : function :=
+  let approxs := analyze f in
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (transf_code approxs f.(fn_code))
+    f.(fn_entrypoint).
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
new file mode 100644
index 0000000..e628d42
--- /dev/null
+++ b/backend/Constpropproof.v
@@ -0,0 +1,445 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for constant propagation. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Events.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Smallstep.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Lattice.
+Require Import Kildall.
+Require Import ConstpropOp.
+Require Import Constprop.
+Require Import ConstpropOpproof.
+
+(** * Correctness of the static analysis *)
+
+Section ANALYSIS.
+
+Variable ge: genv.
+
+Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
+  forall r, val_match_approx ge (D.get r a) rs#r.
+
+Lemma regs_match_approx_top:
+  forall rs, regs_match_approx D.top rs.
+Proof.
+  intros. red; intros. simpl. rewrite PTree.gempty. 
+  unfold Approx.top, val_match_approx. auto.
+Qed.
+
+Lemma regs_match_approx_increasing:
+  forall a1 a2 rs,
+  D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.
+Proof.
+  unfold D.ge, regs_match_approx. intros.
+  apply val_match_approx_increasing with (D.get r a2); auto.
+Qed.
+
+Lemma regs_match_approx_update:
+  forall ra rs a v r,
+  val_match_approx ge a v ->
+  regs_match_approx ra rs ->
+  regs_match_approx (D.set r a ra) (rs#r <- v).
+Proof.
+  intros; red; intros. rewrite Regmap.gsspec. 
+  case (peq r0 r); intro.
+  subst r0. rewrite D.gss. auto.
+  rewrite D.gso; auto. 
+Qed.
+
+Lemma approx_regs_val_list:
+  forall ra rs rl,
+  regs_match_approx ra rs ->
+  val_list_match_approx ge (approx_regs ra rl) rs##rl.
+Proof.
+  induction rl; simpl; intros.
+  constructor.
+  constructor. apply H. auto.
+Qed.
+
+
+(** The correctness of the static analysis follows from the results
+  of module [ConstpropOpproof] and the fact that the result of
+  the static analysis is a solution of the forward dataflow inequations. *)
+
+Lemma analyze_correct_1:
+  forall f pc rs pc' i,
+  f.(fn_code)!pc = Some i ->
+  In pc' (successors_instr i) ->
+  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
+  regs_match_approx (analyze f)!!pc' rs.
+Proof.
+  intros until i. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
+                      ((fn_entrypoint f, D.top) :: nil)).
+  intros approxs; intros.
+  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
+  eapply DS.fixpoint_solution; eauto.
+  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
+  auto.
+  intros. rewrite PMap.gi. apply regs_match_approx_top. 
+Qed.
+
+Lemma analyze_correct_3:
+  forall f rs,
+  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
+Proof.
+  intros. unfold analyze. 
+  caseEq (DS.fixpoint (successors f) (transfer f)
+                      ((fn_entrypoint f, D.top) :: nil)).
+  intros approxs; intros.
+  apply regs_match_approx_increasing with D.top.
+  eapply DS.fixpoint_entry; eauto. auto with coqlib.
+  apply regs_match_approx_top. 
+  intros. rewrite PMap.gi. apply regs_match_approx_top.
+Qed.
+
+End ANALYSIS.
+
+(** * Correctness of the code transformation *)
+
+(** We now show that the transformed code after constant propagation
+  has the same semantics as the original code. *)
+
+Section PRESERVATION.
+
+Variable prog: program.
+Let tprog := transf_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  intros; unfold ge, tge, tprog, transf_program. 
+  apply Genv.find_symbol_transf.
+Qed.
+
+Lemma functions_translated:
+  forall (v: val) (f: fundef),
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof.  
+  intros.
+  exact (Genv.find_funct_transf transf_fundef H).
+Qed.
+
+Lemma function_ptr_translated:
+  forall (b: block) (f: fundef),
+  Genv.find_funct_ptr ge b = Some f ->
+  Genv.find_funct_ptr tge b = Some (transf_fundef f).
+Proof.  
+  intros. 
+  exact (Genv.find_funct_ptr_transf transf_fundef H).
+Qed.
+
+Lemma sig_function_translated:
+  forall f,
+  funsig (transf_fundef f) = funsig f.
+Proof.
+  intros. destruct f; reflexivity.
+Qed.
+
+Lemma transf_ros_correct:
+  forall ros rs f approx,
+  regs_match_approx ge approx rs ->
+  find_function ge ros rs = Some f ->
+  find_function tge (transf_ros approx ros) rs = Some (transf_fundef f).
+Proof.
+  intros until approx; intro MATCH.
+  destruct ros; simpl.
+  intro.
+  exploit functions_translated; eauto. intro FIND.  
+  caseEq (D.get r approx); intros; auto.
+  generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto.
+  generalize (MATCH r). rewrite H0. intros [b [A B]].
+  rewrite <- symbols_preserved in A.
+  rewrite B in FIND. rewrite H1 in FIND. 
+  rewrite Genv.find_funct_find_funct_ptr in FIND.
+  simpl. rewrite A. auto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
+  intro. apply function_ptr_translated. auto.
+  congruence.
+Qed.
+
+(** The proof of semantic preservation is a simulation argument
+  based on diagrams of the following form:
+<<
+           st1 --------------- st2
+            |                   |
+           t|                   |t
+            |                   |
+            v                   v
+           st1'--------------- st2'
+>>
+  The left vertical arrow represents a transition in the
+  original RTL code.  The top horizontal bar is the [match_states]
+  invariant between the initial state [st1] in the original RTL code
+  and an initial state [st2] in the transformed code.
+  This invariant expresses that all code fragments appearing in [st2]
+  are obtained by [transf_code] transformation of the corresponding
+  fragments in [st1].  Moreover, the values of registers in [st1]
+  must match their compile-time approximations at the current program
+  point.
+  These two parts of the diagram are the hypotheses.  In conclusions,
+  we want to prove the other two parts: the right vertical arrow,
+  which is a transition in the transformed RTL code, and the bottom
+  horizontal bar, which means that the [match_state] predicate holds
+  between the final states [st1'] and [st2']. *)
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+   match_stackframe_intro:
+      forall res c sp pc rs f,
+      c = f.(RTL.fn_code) ->
+      (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) ->
+    match_stackframes
+        (Stackframe res c sp pc rs)
+        (Stackframe res (transf_code (analyze f) c) sp pc rs).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro:
+      forall s c sp pc rs m f s'
+           (CF: c = f.(RTL.fn_code))
+           (MATCH: regs_match_approx ge (analyze f)!!pc rs)
+           (STACKS: list_forall2 match_stackframes s s'),
+      match_states (State s c sp pc rs m)
+                   (State s' (transf_code (analyze f) c) sp pc rs m)
+  | match_states_call:
+      forall s f args m s',
+      list_forall2 match_stackframes s s' ->
+      match_states (Callstate s f args m)
+                   (Callstate s' (transf_fundef f) args m)
+  | match_states_return:
+      forall s s' v m,
+      list_forall2 match_stackframes s s' ->
+      match_states (Returnstate s v m)
+                   (Returnstate s' v m).
+
+Ltac TransfInstr :=
+  match goal with
+  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
+      cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr));
+      [ simpl
+      | unfold transf_code; rewrite PTree.gmap; 
+        unfold option_map; rewrite H1; reflexivity ]
+  end.
+
+(** The proof of simulation proceeds by case analysis on the transition
+  taken in the source code. *)
+
+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'.
+Proof.
+  induction 1; intros; inv MS.
+
+  (* Inop *)
+  exists (State s' (transf_code (analyze f) (fn_code 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.
+
+  (* Iop *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split.
+  TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args);
+  intros op' args' OSR.
+  assert (eval_operation tge sp op' rs##args' = Some v).
+    rewrite (eval_operation_preserved symbols_preserved). 
+    generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
+                  MATCH op args v).
+    rewrite OSR; simpl. auto.
+  generalize (eval_static_operation_correct ge op sp
+               (approx_regs (analyze f)!!pc args) rs##args v
+               (approx_regs_val_list _ _ _ args MATCH) H0).
+  case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros;
+  simpl in H2;
+  eapply exec_Iop; eauto; simpl.
+  congruence.
+  congruence.
+  elim H2; intros b [A B]. rewrite symbols_preserved. 
+  rewrite A; rewrite B; auto.
+  econstructor; eauto. 
+  eapply analyze_correct_1 with (pc := pc); eauto.
+  simpl; auto.
+  unfold transfer; rewrite H. 
+  apply regs_match_approx_update; auto. 
+  eapply eval_static_operation_correct; eauto.
+  apply approx_regs_val_list; auto.
+
+  (* Iload *)
+  caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
+  intros addr' args' ASR.
+  assert (eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite (eval_addressing_preserved symbols_preserved). 
+    generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
+                  MATCH addr args).
+    rewrite ASR; simpl. congruence. 
+  TransfInstr. rewrite ASR. intro.
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split.
+  eapply exec_Iload; eauto.
+  econstructor; eauto. 
+  eapply analyze_correct_1; eauto. simpl; auto. 
+  unfold transfer; rewrite H. 
+  apply regs_match_approx_update; auto. simpl; auto.
+
+  (* Istore *)
+  caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
+  intros addr' args' ASR.
+  assert (eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite (eval_addressing_preserved symbols_preserved). 
+    generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
+                  MATCH addr args).
+    rewrite ASR; simpl. congruence. 
+  TransfInstr. rewrite ASR. intro.
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split.
+  eapply exec_Istore; eauto.
+  econstructor; eauto. 
+  eapply analyze_correct_1; eauto. simpl; auto. 
+  unfold transfer; rewrite H. auto. 
+
+  (* Icall *)
+  exploit transf_ros_correct; eauto. intro FIND'.
+  TransfInstr; intro.
+  econstructor; split.
+  eapply exec_Icall; eauto. apply sig_function_translated; auto.
+  constructor; auto. constructor; auto.
+  econstructor; eauto. 
+  intros. eapply analyze_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H.
+  apply regs_match_approx_update; auto. simpl. auto.
+
+  (* Itailcall *)
+  exploit transf_ros_correct; eauto. intros FIND'.
+  TransfInstr; intro.
+  econstructor; split.
+  eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
+  constructor; auto. 
+
+  (* Icond, true *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. 
+  caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
+  intros cond' args' CSR.
+  assert (eval_condition cond' rs##args' = Some true).
+    generalize (cond_strength_reduction_correct
+                  ge (approx_reg (analyze f)!!pc) rs MATCH cond args).
+    rewrite CSR.  intro. congruence.
+  TransfInstr. rewrite CSR. 
+  caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
+  intros b ESC. 
+  generalize (eval_static_condition_correct ge cond _ _ _
+               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
+  replace b with true. intro; eapply exec_Inop; eauto. congruence.
+  intros. eapply exec_Icond_true; eauto.
+  econstructor; eauto.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
+  unfold transfer; rewrite H; auto.
+
+  (* Icond, false *)
+  exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. 
+  caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
+  intros cond' args' CSR.
+  assert (eval_condition cond' rs##args' = Some false).
+    generalize (cond_strength_reduction_correct
+                  ge (approx_reg (analyze f)!!pc) rs MATCH cond args).
+    rewrite CSR.  intro. congruence.
+  TransfInstr. rewrite CSR. 
+  caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
+  intros b ESC. 
+  generalize (eval_static_condition_correct ge cond _ _ _
+               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
+  replace b with false. intro; eapply exec_Inop; eauto. congruence.
+  intros. eapply exec_Icond_false; eauto.
+  econstructor; eauto.
+  eapply analyze_correct_1; eauto.
+  simpl; auto.
+  unfold transfer; rewrite H; auto.
+
+  (* Ireturn *)
+  exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split.
+  eapply exec_Ireturn; eauto. TransfInstr; auto.
+  constructor; auto.
+
+  (* internal function *)
+  simpl. unfold transf_function.
+  econstructor; split.
+  eapply exec_function_internal; simpl; eauto.
+  simpl. econstructor; eauto.
+  apply analyze_correct_3; auto.
+
+  (* external function *)
+  simpl. econstructor; split.
+  eapply exec_function_external; eauto.
+  constructor; auto.
+
+  (* return *)
+  inv H3. inv H1. 
+  econstructor; split.
+  eapply exec_return; eauto. 
+  econstructor; eauto. 
+Qed.
+
+Lemma transf_initial_states:
+  forall st1, initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inversion H.
+  exploit function_ptr_translated; eauto. intro FIND.
+  exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split.
+  econstructor; eauto.
+  replace (prog_main tprog) with (prog_main prog).
+  rewrite symbols_preserved. eauto.
+  reflexivity.
+  rewrite <- H2. apply sig_function_translated.
+  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
+  constructor. constructor. auto.
+  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. 
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r, 
+  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+Proof.
+  intros. inv H0. inv H. inv H4. constructor. 
+Qed.
+
+(** The preservation of the observable behavior of the program then
+  follows, using the generic preservation theorem
+  [Smallstep.simulation_step_preservation]. *)
+
+Theorem transf_program_correct:
+  forall (beh: program_behavior), not_wrong beh ->
+  exec_program prog beh -> exec_program tprog beh.
+Proof.
+  unfold exec_program; intros.
+  eapply simulation_step_preservation; eauto.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact transf_step_correct. 
+Qed.
+
+End PRESERVATION.