summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-08-17 15:28:52 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-08-17 15:28:52 +0000
commita8fc4625c2c172484341b9105c1aa8ea1c6a49f3 (patch)
treea368cd0147c3eb8669f89a084f13f22582a6d375 /backend
parent2199fd1838ab1c32d55c760e92b97077d8eaae50 (diff)
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
Diffstat (limited to 'backend')
-rw-r--r--backend/Constprop.v235
-rw-r--r--backend/Constpropproof.v445
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.