Initial import of compcert

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

1 files changed, 845 insertions, 0 deletions

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
new file mode 100644
index 00000000..db8a973b
--- /dev/null
+++ b/backend/CSEproof.v
@@ -0,0 +1,845 @@
+(** Correctness proof for common subexpression elimination. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import Kildall.
+Require Import CSE.
+
+(** * Semantic properties of value numberings *)
+
+(** ** Well-formedness of numberings *)
+
+(** A numbering is well-formed if all registers mentioned in equations
+  are less than the ``next'' register number given in the numbering.
+  This guarantees that the next register is fresh with respect to
+  the equations. *)
+
+Definition wf_rhs (next: valnum) (rh: rhs) : Prop :=
+  match rh with
+  | Op op vl => forall v, In v vl -> Plt v next
+  | Load chunk addr vl => forall v, In v vl -> Plt v next
+  end.
+
+Definition wf_equation (next: valnum) (vr: valnum) (rh: rhs) : Prop :=
+  Plt vr next /\ wf_rhs next rh.
+
+Definition wf_numbering (n: numbering) : Prop :=
+  (forall v rh,
+    In (v, rh) n.(num_eqs) -> wf_equation n.(num_next) v rh)
+/\
+  (forall r v,
+    PTree.get r n.(num_reg) = Some v -> Plt v n.(num_next)).
+
+Lemma wf_empty_numbering:
+  wf_numbering empty_numbering.
+Proof.
+  unfold empty_numbering; split; simpl; intros.
+  elim H.
+  rewrite PTree.gempty in H. congruence.
+Qed.
+
+Lemma wf_rhs_increasing:
+  forall next1 next2 rh,
+  Ple next1 next2 ->
+  wf_rhs next1 rh -> wf_rhs next2 rh.
+Proof.
+  intros; destruct rh; simpl; intros; apply Plt_Ple_trans with next1; auto.
+Qed.
+
+Lemma wf_equation_increasing:
+  forall next1 next2 vr rh,
+  Ple next1 next2 ->
+  wf_equation next1 vr rh -> wf_equation next2 vr rh.
+Proof.
+  intros. elim H0; intros. split. 
+  apply Plt_Ple_trans with next1; auto.
+  apply wf_rhs_increasing with next1; auto.
+Qed.
+
+(** We now show that all operations over numberings 
+  preserve well-formedness. *)
+
+Lemma wf_valnum_reg:
+  forall n r n' v,
+  wf_numbering n ->
+  valnum_reg n r = (n', v) ->
+  wf_numbering n' /\ Plt v n'.(num_next) /\ Ple n.(num_next) n'.(num_next).
+Proof.
+  intros until v. intros WF. inversion WF.
+  generalize (H0 r v).
+  unfold valnum_reg. destruct ((num_reg n)!r).
+  intros. replace n' with n. split. auto. 
+  split. apply H1. congruence. 
+  apply Ple_refl.
+  congruence. 
+  intros. inversion H2. simpl. split.
+  split; simpl; intros. 
+  apply wf_equation_increasing with (num_next n). apply Ple_succ. auto. 
+  rewrite PTree.gsspec in H3. destruct (peq r0 r). 
+  replace v0 with (num_next n). apply Plt_succ. congruence.
+  apply Plt_trans_succ; eauto. 
+  split. apply Plt_succ. apply Ple_succ.
+Qed.
+
+Lemma wf_valnum_regs:
+  forall rl n n' vl,
+  wf_numbering n ->
+  valnum_regs n rl = (n', vl) ->
+  wf_numbering n' /\
+  (forall v, In v vl -> Plt v n'.(num_next)) /\
+  Ple n.(num_next) n'.(num_next).
+Proof.
+  induction rl; intros.
+  simpl in H0. inversion H0. subst n'; subst vl. 
+  simpl. intuition. 
+  simpl in H0. 
+  caseEq (valnum_reg n a). intros n1 v1 EQ1.
+  caseEq (valnum_regs n1 rl). intros ns vs EQS.
+  rewrite EQ1 in H0; rewrite EQS in H0; simpl in H0.
+  inversion H0. subst n'; subst vl. 
+  generalize (wf_valnum_reg _ _ _ _ H EQ1); intros [A1 [B1 C1]].
+  generalize (IHrl _ _ _ A1 EQS); intros [As [Bs Cs]].
+  split. auto.
+  split. simpl; intros. elim H1; intro.
+    subst v. eapply Plt_Ple_trans; eauto.
+    auto.
+  eapply Ple_trans; eauto.
+Qed.
+
+Lemma find_valnum_rhs_correct:
+  forall rh vn eqs,
+  find_valnum_rhs rh eqs = Some vn -> In (vn, rh) eqs.
+Proof.
+  induction eqs; simpl.
+  congruence.
+  case a; intros v r'. case (eq_rhs rh r'); intro.
+  intro. left. congruence.
+  intro. right. auto.
+Qed.
+
+Lemma wf_add_rhs:
+  forall n rd rh,
+  wf_numbering n ->
+  wf_rhs n.(num_next) rh ->
+  wf_numbering (add_rhs n rd rh).
+Proof.
+  intros. inversion H. unfold add_rhs. 
+  caseEq (find_valnum_rhs rh n.(num_eqs)); intros.
+  split; simpl. assumption. 
+  intros r v0. rewrite PTree.gsspec. case (peq r rd); intros.
+  inversion H4. subst v0. 
+  elim (H1 v rh (find_valnum_rhs_correct _ _ _ H3)). auto.
+  eauto.
+  split; simpl.
+  intros v rh0 [A1|A2]. inversion A1. subst rh0. 
+  split. apply Plt_succ. apply wf_rhs_increasing with n.(num_next).
+  apply Ple_succ. auto.
+  apply wf_equation_increasing with n.(num_next). apply Ple_succ. auto.
+  intros r v. rewrite PTree.gsspec. case (peq r rd); intro.
+  intro. inversion H4. apply Plt_succ.
+  intro. apply Plt_trans_succ. eauto. 
+Qed.
+
+Lemma wf_add_op:
+  forall n rd op rs,
+  wf_numbering n ->
+  wf_numbering (add_op n rd op rs).
+Proof.
+  intros. unfold add_op. 
+  case (is_move_operation op rs).
+  intro r. caseEq (valnum_reg n r); intros n' v EQ.
+  destruct (wf_valnum_reg _ _ _ _ H EQ) as [[A1 A2] [B C]].
+  split; simpl. assumption. intros until v0. rewrite PTree.gsspec.
+  case (peq r0 rd); intros. replace v0 with v. auto. congruence.
+  eauto.
+  caseEq (valnum_regs n rs). intros n' vl EQ. 
+  generalize (wf_valnum_regs _ _ _ _ H EQ). intros [A [B C]].
+  apply wf_add_rhs; auto.
+Qed.
+
+Lemma wf_add_load:
+  forall n rd chunk addr rs,
+  wf_numbering n ->
+  wf_numbering (add_load n rd chunk addr rs).
+Proof.
+  intros. unfold add_load. 
+  caseEq (valnum_regs n rs). intros n' vl EQ. 
+  generalize (wf_valnum_regs _ _ _ _ H EQ). intros [A [B C]].
+  apply wf_add_rhs; auto.
+Qed.
+
+Lemma kill_load_eqs_incl:
+  forall eqs, List.incl (kill_load_eqs eqs) eqs.
+Proof.
+  induction eqs; simpl; intros.
+  apply incl_refl.
+  destruct a. destruct r. apply incl_same_head; auto.
+  auto.
+  apply incl_tl. auto.
+Qed.
+
+Lemma wf_kill_loads:
+  forall n, wf_numbering n -> wf_numbering (kill_loads n).
+Proof.
+  intros. inversion H. unfold kill_loads; split; simpl; intros.
+  apply H0. apply kill_load_eqs_incl. auto.
+  eauto.
+Qed.
+
+Lemma wf_transfer:
+  forall f pc n, wf_numbering n -> wf_numbering (transfer f pc n).
+Proof.
+  intros. unfold transfer. 
+  destruct (f.(fn_code)!pc); auto.
+  destruct i; auto.
+  apply wf_add_op; auto.
+  apply wf_add_load; auto.
+  apply wf_kill_loads; auto.
+  apply wf_empty_numbering.
+Qed.
+
+(** As a consequence, the numberings computed by the static analysis
+  are well formed. *)
+
+Theorem wf_analyze:
+  forall f pc, wf_numbering (analyze f)!!pc.
+Proof.
+  unfold analyze; intros.
+  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
+                          (transfer f) (fn_entrypoint f)).
+  intros approx EQ.
+  eapply Solver.fixpoint_invariant with (P := wf_numbering); eauto.
+  exact wf_empty_numbering.   
+  exact (wf_transfer f).
+  intro. rewrite PMap.gi. apply wf_empty_numbering.
+Qed.
+
+(** ** Properties of satisfiability of numberings *)
+
+Module ValnumEq.
+  Definition t := valnum.
+  Definition eq := peq.
+End ValnumEq.
+
+Module VMap := EMap(ValnumEq).
+
+Section SATISFIABILITY.
+
+Variable ge: genv.
+Variable sp: val.
+Variable m: mem.
+
+(** Agremment between two mappings from value numbers to values
+  up to a given value number. *)
+
+Definition valu_agree (valu1 valu2: valnum -> val) (upto: valnum) : Prop :=
+  forall v, Plt v upto -> valu2 v = valu1 v.
+
+Lemma valu_agree_refl:
+  forall valu upto, valu_agree valu valu upto.
+Proof.
+  intros; red; auto.
+Qed.
+
+Lemma valu_agree_trans:
+  forall valu1 valu2 valu3 upto12 upto23,
+  valu_agree valu1 valu2 upto12 ->
+  valu_agree valu2 valu3 upto23 ->
+  Ple upto12 upto23 ->
+  valu_agree valu1 valu3 upto12.
+Proof.
+  intros; red; intros. transitivity (valu2 v).
+  apply H0. apply Plt_Ple_trans with upto12; auto.
+  apply H; auto.
+Qed.
+
+Lemma valu_agree_list:
+  forall valu1 valu2 upto vl,
+  valu_agree valu1 valu2 upto ->
+  (forall v, In v vl -> Plt v upto) ->
+  map valu2 vl = map valu1 vl.
+Proof.
+  intros. apply list_map_exten. intros. symmetry. apply H. auto.
+Qed.
+
+(** The [numbering_holds] predicate (defined in file [CSE]) is
+  extensional with respect to [valu_agree]. *)
+
+Lemma numbering_holds_exten:
+  forall valu1 valu2 n rs,
+  valu_agree valu1 valu2 n.(num_next) ->
+  wf_numbering n ->
+  numbering_holds valu1 ge sp rs m n ->
+  numbering_holds valu2 ge sp rs m n.
+Proof.
+  intros. inversion H0. inversion H1. split; intros.
+  generalize (H2 _ _ H6). intro WFEQ.
+  generalize (H4 _ _ H6). 
+  unfold equation_holds; destruct rh.
+  elim WFEQ; intros.
+  rewrite (valu_agree_list valu1 valu2 n.(num_next)). 
+  rewrite H. auto. auto. auto. exact H8. 
+  elim WFEQ; intros.
+  rewrite (valu_agree_list valu1 valu2 n.(num_next)). 
+  rewrite H. auto. auto. auto. exact H8. 
+  rewrite H. auto. eauto.
+Qed.
+
+(** [valnum_reg] and [valnum_regs] preserve the [numbering_holds] predicate.
+  Moreover, it is always the case that the returned value number has
+  the value of the given register in the final assignment of values to
+  value numbers. *)
+
+Lemma valnum_reg_holds:
+  forall valu1 rs n r n' v,
+  wf_numbering n ->
+  numbering_holds valu1 ge sp rs m n ->
+  valnum_reg n r = (n', v) ->
+  exists valu2,
+    numbering_holds valu2 ge sp rs m n' /\
+    valu2 v = rs#r /\
+    valu_agree valu1 valu2 n.(num_next).
+Proof.
+  intros until v. unfold valnum_reg. 
+  caseEq (n.(num_reg)!r).
+  (* Register already has a value number *)
+  intros. inversion H2. subst n'; subst v0. 
+  inversion H1. 
+  exists valu1. split. auto. 
+  split. symmetry. auto.
+  apply valu_agree_refl.
+  (* Register gets a fresh value number *)
+  intros. inversion H2. subst n'. subst v. inversion H1.
+  set (valu2 := VMap.set n.(num_next) rs#r valu1).
+  assert (AG: valu_agree valu1 valu2 n.(num_next)).
+    red; intros. unfold valu2. apply VMap.gso. 
+    auto with coqlib.
+  elim (numbering_holds_exten _ _ _ _ AG H0 H1); intros.
+  exists valu2. 
+  split. split; simpl; intros. auto. 
+  unfold valu2, VMap.set, ValnumEq.eq. 
+  rewrite PTree.gsspec in H7. destruct (peq r0 r).
+  inversion H7. rewrite peq_true. congruence.
+  case (peq vn (num_next n)); intro. 
+  inversion H0. generalize (H9 _ _ H7).  rewrite e. intro.
+  elim (Plt_strict _ H10). 
+  auto.
+  split. unfold valu2. apply VMap.gss. 
+  auto.
+Qed.
+
+Lemma valnum_regs_holds:
+  forall rs rl valu1 n n' vl,
+  wf_numbering n ->
+  numbering_holds valu1 ge sp rs m n ->
+  valnum_regs n rl = (n', vl) ->
+  exists valu2,
+    numbering_holds valu2 ge sp rs m n' /\
+    List.map valu2 vl = rs##rl /\
+    valu_agree valu1 valu2 n.(num_next).
+Proof.
+  induction rl; simpl; intros.
+  (* base case *)
+  inversion H1; subst n'; subst vl.
+  exists valu1. split. auto. split. reflexivity. apply valu_agree_refl.
+  (* inductive case *)
+  caseEq (valnum_reg n a); intros n1 v1 EQ1.
+  caseEq (valnum_regs n1 rl); intros ns vs EQs.
+  rewrite EQ1 in H1; rewrite EQs in H1. inversion H1. subst vl; subst n'.
+  generalize (valnum_reg_holds _ _ _ _ _ _ H H0 EQ1).
+  intros [valu2 [A [B C]]].
+  generalize (wf_valnum_reg _ _ _ _ H EQ1). intros [D [E F]].
+  generalize (IHrl _ _ _ _ D A EQs). 
+  intros [valu3 [P [Q R]]].
+  exists valu3. 
+  split. auto. 
+  split. simpl. rewrite R. congruence. auto.
+  eapply valu_agree_trans; eauto.
+Qed.
+
+(** A reformulation of the [equation_holds] predicate in terms
+  of the value to which a right-hand side of an equation evaluates. *)
+
+Definition rhs_evals_to
+    (valu: valnum -> val) (rh: rhs) (v: val) : Prop :=
+  match rh with
+  | Op op vl => 
+      eval_operation ge sp op (List.map valu vl) = Some v
+  | Load chunk addr vl =>
+      exists a,
+      eval_addressing ge sp addr (List.map valu vl) = Some a /\
+      loadv chunk m a = Some v
+  end.
+
+Lemma equation_evals_to_holds_1:
+  forall valu rh v vres,
+  rhs_evals_to valu rh v ->
+  equation_holds valu ge sp m vres rh ->
+  valu vres = v.
+Proof.
+  intros until vres. unfold rhs_evals_to, equation_holds.
+  destruct rh. congruence.
+  intros [a1 [A1 B1]] [a2 [A2 B2]]. congruence.
+Qed.
+
+Lemma equation_evals_to_holds_2:
+  forall valu rh v vres,
+  wf_rhs vres rh ->
+  rhs_evals_to valu rh v ->
+  equation_holds (VMap.set vres v valu) ge sp m vres rh.
+Proof.
+  intros until vres. unfold wf_rhs, rhs_evals_to, equation_holds.
+  rewrite VMap.gss. 
+  assert (forall vl: list valnum,
+            (forall v, In v vl -> Plt v vres) ->
+            map (VMap.set vres v valu) vl = map valu vl).
+    intros. apply list_map_exten. intros. 
+    symmetry. apply VMap.gso. apply Plt_ne. auto.
+  destruct rh; intros; rewrite H; auto.
+Qed.
+
+(** The numbering obtained by adding an equation [rd = rhs] is satisfiable
+  in a concrete register set where [rd] is set to the value of [rhs]. *)
+
+Lemma add_rhs_satisfiable:
+  forall n rh valu1 rs rd v,
+  wf_numbering n ->
+  wf_rhs n.(num_next) rh ->
+  numbering_holds valu1 ge sp rs m n ->
+  rhs_evals_to valu1 rh v ->
+  numbering_satisfiable ge sp (rs#rd <- v) m (add_rhs n rd rh).
+Proof.
+  intros. unfold add_rhs. 
+  caseEq (find_valnum_rhs rh n.(num_eqs)).
+  (* RHS found *)
+  intros vres FINDVN. inversion H1.
+  exists valu1. split; simpl; intros.
+  auto. 
+  rewrite Regmap.gsspec. 
+  rewrite PTree.gsspec in H5.
+  destruct (peq r rd).
+  symmetry. eapply equation_evals_to_holds_1; eauto.
+  apply H3. apply find_valnum_rhs_correct. congruence.
+  auto.
+  (* RHS not found *)
+  intro FINDVN. 
+  set (valu2 := VMap.set n.(num_next) v valu1).
+  assert (AG: valu_agree valu1 valu2 n.(num_next)).
+    red; intros. unfold valu2. apply VMap.gso. 
+    auto with coqlib.
+  elim (numbering_holds_exten _ _ _ _ AG H H1); intros.
+  exists valu2. split; simpl; intros.
+  elim H5; intro.
+  inversion H6; subst vn; subst rh0. 
+  unfold valu2. eapply equation_evals_to_holds_2; eauto.
+  auto.
+  rewrite Regmap.gsspec. rewrite PTree.gsspec in H5. destruct (peq r rd).
+  unfold valu2. inversion H5. symmetry. apply VMap.gss.
+  auto.
+Qed.
+
+(** [add_op] returns a numbering that is satisfiable in the register
+  set after execution of the corresponding [Iop] instruction. *)
+
+Lemma add_op_satisfiable:
+  forall n rs op args dst v,
+  wf_numbering n ->
+  numbering_satisfiable ge sp rs m n ->
+  eval_operation ge sp op rs##args = Some v ->
+  numbering_satisfiable ge sp (rs#dst <- v) m (add_op n dst op args).
+Proof.
+  intros. inversion H0.
+  unfold add_op.
+  caseEq (@is_move_operation reg op args).
+  intros arg EQ. 
+  destruct (is_move_operation_correct _ _ EQ) as [A B]. subst op args.
+  caseEq (valnum_reg n arg). intros n1 v1 VL.
+  generalize (valnum_reg_holds _ _ _ _ _ _ H H2 VL). intros [valu2 [A [B C]]].
+  generalize (wf_valnum_reg _ _ _ _ H VL). intros [D [E F]].  
+  elim A; intros. exists valu2; split; simpl; intros.
+  auto. rewrite Regmap.gsspec. rewrite PTree.gsspec in H5.
+  destruct (peq r dst). simpl in H1. congruence. auto.
+  intro NEQ. caseEq (valnum_regs n args). intros n1 vl VRL.
+  generalize (valnum_regs_holds _ _ _ _ _ _ H H2 VRL). intros [valu2 [A [B C]]].
+  generalize (wf_valnum_regs _ _ _ _ H VRL). intros [D [E F]].
+  apply add_rhs_satisfiable with valu2; auto.
+  simpl. congruence. 
+Qed.
+
+(** [add_load] returns a numbering that is satisfiable in the register
+  set after execution of the corresponding [Iload] instruction. *)
+
+Lemma add_load_satisfiable:
+  forall n rs chunk addr args dst a v,
+  wf_numbering n ->
+  numbering_satisfiable ge sp rs m n ->
+  eval_addressing ge sp addr rs##args = Some a ->
+  loadv chunk m a = Some v ->
+  numbering_satisfiable ge sp 
+     (rs#dst <- v)
+     m (add_load n dst chunk addr args).
+Proof.
+  intros. inversion H0.
+  unfold add_load.
+  caseEq (valnum_regs n args). intros n1 vl VRL.
+  generalize (valnum_regs_holds _ _ _ _ _ _ H H3 VRL). intros [valu2 [A [B C]]].
+  generalize (wf_valnum_regs _ _ _ _ H VRL). intros [D [E F]].
+  apply add_rhs_satisfiable with valu2; auto.
+  simpl. exists a; split; congruence. 
+Qed.
+
+(** [kill_load] preserves satisfiability.  Moreover, the resulting numbering
+  is satisfiable in any concrete memory state. *)
+
+Lemma kill_load_eqs_ops:
+  forall v rhs eqs,
+  In (v, rhs) (kill_load_eqs eqs) ->
+  match rhs with Op _ _ => True | Load _ _ _ => False end.
+Proof.
+  induction eqs; simpl; intros.
+  elim H.
+  destruct a. destruct r. 
+  elim H; intros. inversion H0; subst v0; subst rhs. auto.
+  apply IHeqs. auto. 
+  apply IHeqs. auto.
+Qed.
+
+Lemma kill_load_satisfiable:
+  forall n rs m',
+  numbering_satisfiable ge sp rs m n ->
+  numbering_satisfiable ge sp rs m' (kill_loads n).
+Proof.
+  intros. inversion H. inversion H0.
+  generalize (kill_load_eqs_incl n.(num_eqs)). intro.
+  exists x. split; intros.
+  generalize (H1 _ _ (H3 _ H4)). 
+  generalize (kill_load_eqs_ops _ _ _ H4).
+  destruct rh; simpl. auto. tauto.
+  apply H2. assumption.
+Qed.
+
+(** Correctness of [reg_valnum]: if it returns a register [r],
+  that register correctly maps back to the given value number. *)
+
+Lemma reg_valnum_correct:
+  forall n v r, reg_valnum n v = Some r -> n.(num_reg)!r = Some v.
+Proof.
+  intros until r. unfold reg_valnum. rewrite PTree.fold_spec.
+  assert(forall l acc0,
+    List.fold_left
+     (fun (acc: option reg) (p: reg * valnum) => 
+        if peq (snd p) v then Some (fst p) else acc)
+     l acc0 = Some r ->
+     In (r, v) l \/ acc0 = Some r).
+  induction l; simpl.
+  intros. tauto.
+  case a; simpl; intros r1 v1 acc0 FL.
+  generalize (IHl _ FL). 
+  case (peq v1 v); intro. 
+    subst v1. intros [A|B]. tauto. inversion B; subst r1. tauto.
+    tauto.
+  intro. elim (H _ _ H0); intro. 
+  apply PTree.elements_complete; auto.
+  discriminate.
+Qed.
+
+(** Correctness of [find_op] and [find_load]: if successful and in a
+  satisfiable numbering, the returned register does contain the 
+  result value of the operation or memory load. *)
+
+Lemma find_rhs_correct:
+  forall valu rs n rh r,
+  numbering_holds valu ge sp rs m n ->
+  find_rhs n rh = Some r ->
+  rhs_evals_to valu rh rs#r.
+Proof.
+  intros until r.  intros NH. 
+  unfold find_rhs. 
+  caseEq (find_valnum_rhs rh n.(num_eqs)); intros.
+  generalize (find_valnum_rhs_correct _ _ _ H); intro.
+  generalize (reg_valnum_correct _ _ _ H0); intro.
+  inversion NH. 
+  generalize (H3 _ _ H1). rewrite (H4 _ _ H2). 
+  destruct rh; simpl; auto.
+  discriminate.
+Qed.
+
+Lemma find_op_correct:
+  forall rs n op args r,
+  wf_numbering n ->
+  numbering_satisfiable ge sp rs m n ->
+  find_op n op args = Some r ->
+  eval_operation ge sp op rs##args = Some rs#r.
+Proof.
+  intros until r. intros WF [valu NH].
+  unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND.
+  generalize (valnum_regs_holds _ _ _ _ _ _ WF NH VR).
+  intros [valu2 [NH2 [EQ AG]]].
+  rewrite <- EQ. 
+  change (rhs_evals_to valu2 (Op op vl) rs#r).
+  eapply find_rhs_correct; eauto.
+Qed.
+
+Lemma find_load_correct:
+  forall rs n chunk addr args r,
+  wf_numbering n ->
+  numbering_satisfiable ge sp rs m n ->
+  find_load n chunk addr args = Some r ->
+  exists a,
+  eval_addressing ge sp addr rs##args = Some a /\
+  loadv chunk m a = Some rs#r.
+Proof.
+  intros until r. intros WF [valu NH].
+  unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND.
+  generalize (valnum_regs_holds _ _ _ _ _ _ WF NH VR).
+  intros [valu2 [NH2 [EQ AG]]].
+  rewrite <- EQ. 
+  change (rhs_evals_to valu2 (Load chunk addr vl) rs#r).
+  eapply find_rhs_correct; eauto.
+Qed.
+
+End SATISFIABILITY.
+
+(** The transfer function preserves satisfiability of numberings. *)
+
+Lemma transfer_correct:
+  forall ge c sp pc rs m pc' rs' m' f n,
+  exec_instr ge c sp pc rs m pc' rs' m' ->
+  c = f.(fn_code) ->
+  wf_numbering n ->
+  numbering_satisfiable ge sp rs m n ->
+  numbering_satisfiable ge sp rs' m' (transfer f pc n).
+Proof.
+  induction 1; intros; subst c; unfold transfer; rewrite H; auto.
+  (* Iop *)
+  eapply add_op_satisfiable; eauto.
+  (* Iload *)
+  eapply add_load_satisfiable; eauto.
+  (* Istore *)
+  eapply kill_load_satisfiable; eauto.
+  (* Icall *)
+  apply empty_numbering_satisfiable.
+Qed.
+
+(** The numberings associated to each instruction by the static analysis
+  are inductively satisfiable, in the following sense: the numbering
+  at the function entry point is satisfiable, and for any RTL execution 
+  from [pc] to [pc'], satisfiability at [pc] implies 
+  satisfiability at [pc']. *)
+
+Theorem analysis_correct_1:
+  forall ge c sp pc rs m pc' rs' m' f,
+  exec_instr ge c sp pc rs m pc' rs' m' ->
+  c = f.(fn_code) ->
+  numbering_satisfiable ge sp rs m (analyze f)!!pc ->
+  numbering_satisfiable ge sp rs' m' (analyze f)!!pc'.
+Proof.
+  intros until f. intros EXEC CODE.
+  generalize (wf_analyze f pc).
+  unfold analyze.
+  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
+                          (transfer f) (fn_entrypoint f)).
+  intros res FIXPOINT WF NS.
+  assert (numbering_satisfiable ge sp rs' m' (transfer f pc res!!pc)).
+    eapply transfer_correct; eauto.
+  assert (Numbering.ge res!!pc' (transfer f pc res!!pc)).
+    eapply Solver.fixpoint_solution; eauto.
+    elim (fn_code_wf f pc); intro. auto.
+    rewrite <- CODE in H0.
+    elim (exec_instr_present _ _ _ _ _ _ _ _ _ EXEC H0).
+    rewrite CODE in EXEC. eapply successors_correct; eauto.
+  apply H0. auto.
+  intros. rewrite PMap.gi. apply empty_numbering_satisfiable.
+Qed.
+
+Theorem analysis_correct_N:
+  forall ge c sp pc rs m pc' rs' m' f,
+  exec_instrs ge c sp pc rs m pc' rs' m' ->
+  c = f.(fn_code) ->
+  numbering_satisfiable ge sp rs m (analyze f)!!pc ->
+  numbering_satisfiable ge sp rs' m' (analyze f)!!pc'.
+Proof.
+  induction 1; intros.
+  assumption.
+  eapply analysis_correct_1; eauto.
+  eauto.
+Qed.
+
+Theorem analysis_correct_entry:
+  forall ge sp rs m f,
+  numbering_satisfiable ge sp rs m (analyze f)!!(f.(fn_entrypoint)).
+Proof.
+  intros. 
+  replace ((analyze f)!!(f.(fn_entrypoint)))
+          with empty_numbering.
+  apply empty_numbering_satisfiable.
+  unfold analyze.
+  caseEq (Solver.fixpoint (successors f) (fn_nextpc f) 
+                          (transfer f) (fn_entrypoint f)).
+  intros res FIXPOINT. 
+  symmetry. change empty_numbering with Solver.L.top.
+  eapply Solver.fixpoint_entry; eauto.
+  intros. symmetry. apply PMap.gi. 
+Qed.
+
+(** * Semantic preservation *)
+
+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 (Genv.find_symbol_transf transf_function prog).
+
+Lemma functions_translated:
+  forall (v: val) (f: RTL.function),
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_function f).
+Proof (@Genv.find_funct_transf _ _ transf_function prog).
+
+Lemma funct_ptr_translated:
+  forall (b: block) (f: RTL.function),
+  Genv.find_funct_ptr ge b = Some f ->
+  Genv.find_funct_ptr tge b = Some (transf_function f).
+Proof (@Genv.find_funct_ptr_transf _ _ transf_function prog).
+
+(** The proof of semantic preservation is a simulation argument using
+  diagrams of the following form:
+<<
+      pc, rs, m ------------------------ pc, rs, m
+          |                                  |
+          |                                  |
+          v                                  v
+     pc', rs', m' --------------------- pc', rs', m'
+>>
+  Left: RTL execution in the original program.  Right: RTL execution in
+  the optimized program.  Precondition (top): the numbering at [pc]
+  (returned by the static analysis) is satisfiable.  Postcondition: none. 
+*)
+
+Definition exec_instr_prop
+        (c: code) (sp: val)
+        (pc: node) (rs: regset) (m: mem)
+        (pc': node) (rs': regset) (m': mem) : Prop :=
+  forall f
+         (CF: c = f.(RTL.fn_code))
+         (SAT: numbering_satisfiable ge sp rs m (analyze f)!!pc),
+  exec_instr tge (transf_code (analyze f) c) sp pc rs m pc' rs' m'.
+
+Definition exec_instrs_prop
+        (c: code) (sp: val)
+        (pc: node) (rs: regset) (m: mem)
+        (pc': node) (rs': regset) (m': mem) : Prop :=
+  forall f
+         (CF: c = f.(RTL.fn_code))
+         (SAT: numbering_satisfiable ge sp rs m (analyze f)!!pc),
+  exec_instrs tge (transf_code (analyze f) c) sp pc rs m pc' rs' m'.
+
+Definition exec_function_prop
+        (f: RTL.function) (args: list val) (m: mem)
+        (res: val) (m': mem) : Prop :=
+  exec_function tge (transf_function f) args m res 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 is by structural induction on the evaluation
+  derivation for the source program. *)
+
+Lemma transf_function_correct:
+  forall f args m res m',
+  exec_function ge f args m res m' ->
+  exec_function_prop f args m res m'.
+Proof.
+  apply (exec_function_ind_3 ge
+          exec_instr_prop exec_instrs_prop exec_function_prop);
+  intros; red; intros; try TransfInstr.
+  (* Inop *)
+  intro; apply exec_Inop; auto.
+  (* Iop *)
+  assert (eval_operation tge sp op rs##args = Some v).
+    rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  case (is_trivial_op op).
+  intro. eapply exec_Iop'; eauto. 
+  caseEq (find_op (analyze f)!!pc op args). intros r FIND CODE.
+  eapply exec_Iop'; eauto. simpl. 
+  assert (eval_operation ge sp op rs##args = Some rs#r).
+    eapply find_op_correct; eauto.
+    eapply wf_analyze; eauto.
+  congruence.
+  intros. eapply exec_Iop'; eauto. 
+  (* Iload *)
+  assert (eval_addressing tge sp addr rs##args = Some a).
+    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  caseEq (find_load (analyze f)!!pc chunk addr args). intros r FIND CODE.
+  eapply exec_Iop'; eauto. simpl. 
+  assert (exists a, eval_addressing ge sp addr rs##args = Some a
+                 /\ loadv chunk m a = Some rs#r).
+    eapply find_load_correct; eauto.
+    eapply wf_analyze; eauto.
+  elim H3; intros a' [A B].
+  congruence.
+  intros. eapply exec_Iload'; eauto. 
+  (* Istore *)
+  assert (eval_addressing tge sp addr rs##args = Some a).
+    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  intro; eapply exec_Istore; eauto. 
+  (* Icall *)
+  assert (find_function tge ros rs = Some (transf_function f)).
+    destruct ros; simpl in H0; simpl.
+    apply functions_translated; auto.
+    rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
+    apply funct_ptr_translated; auto. discriminate.
+  intro; eapply exec_Icall with (f := transf_function f); eauto. 
+  (* Icond true *)
+  intro; eapply exec_Icond_true; eauto. 
+  (* Icond false *)
+  intro; eapply exec_Icond_false; eauto. 
+  (* refl *)
+  apply exec_refl.
+  (* one *)
+  apply exec_one; auto.
+  (* trans *)
+  eapply exec_trans; eauto. apply H2; auto. 
+  eapply analysis_correct_N; eauto.
+  (* function *)
+  intro. unfold transf_function; eapply exec_funct; simpl; eauto. 
+  eapply H1; eauto. eapply analysis_correct_entry; eauto.
+Qed.
+
+Theorem transf_program_correct:
+  forall (r: val),
+  exec_program prog r -> exec_program tprog r.
+Proof.
+  intros r [fptr [f [m [FINDS [FINDF [SIG EXEC]]]]]].
+  red. exists fptr; exists (transf_function f); exists m. 
+  split. change (prog_main tprog) with (prog_main prog).
+  rewrite symbols_preserved. assumption.
+  split. apply funct_ptr_translated; auto.
+  split. unfold transf_function. 
+  rewrite <- SIG. destruct (analyze f); reflexivity.
+  apply transf_function_correct. 
+  unfold tprog, transf_program. rewrite Genv.init_mem_transf. 
+  exact EXEC.
+Qed.
+
+End PRESERVATION.