From 0e76ac320601a81a67c700759526d0f8b7a8ed7b Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 23 Feb 2012 14:00:06 +0000
Subject: More aggressive common subexpression elimination (CSE) of memory
 loads.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/CSEproof.v | 477 ++++++++++++++++++++++++++++++++---------------------
 1 file changed, 288 insertions(+), 189 deletions(-)

(limited to 'backend/CSEproof.v')

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index c685ef65..65438264 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -15,6 +15,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Errors.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -25,6 +26,7 @@ Require Import Smallstep.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
+Require Import RTLtyping.
 Require Import Kildall.
 Require Import CSE.
 
@@ -203,25 +205,37 @@ Proof.
   apply Plt_trans_succ. eauto.
 Qed.
 
-Lemma kill_load_eqs_incl:
-  forall eqs, List.incl (kill_load_eqs eqs) eqs.
+Remark kill_eqs_in:
+  forall pred v rhs eqs,
+  In (v, rhs) (kill_eqs pred eqs) -> In (v, rhs) eqs /\ pred rhs = false.
 Proof.
-  induction eqs; simpl; intros.
-  apply incl_refl.
-  destruct a. destruct r. 
-  destruct (op_depends_on_memory o). auto with coqlib. 
-  apply incl_same_head; auto.
-  auto with coqlib.
+  induction eqs; simpl; intros. 
+  tauto.
+  destruct (pred (snd a)) as []_eqn. 
+  exploit IHeqs; eauto. tauto. 
+  simpl in H; destruct H. subst a. auto. exploit IHeqs; eauto. tauto. 
 Qed.
 
-Lemma wf_kill_loads:
-  forall n, wf_numbering n -> wf_numbering (kill_loads n).
+Lemma wf_kill_equations:
+  forall pred n, wf_numbering n -> wf_numbering (kill_equations pred n).
 Proof.
-  intros. inversion H. unfold kill_loads; split; simpl; intros.
-  apply H0. apply kill_load_eqs_incl. auto.
+  intros. inversion H. unfold kill_equations; split; simpl; intros.
+  exploit kill_eqs_in; eauto. intros [A B]. auto. 
   eauto.
 Qed.
 
+Lemma wf_add_store:
+  forall n chunk addr rargs rsrc,
+  wf_numbering n -> wf_numbering (add_store n chunk addr rargs rsrc).
+Proof.
+  intros. unfold add_store. 
+  destruct (valnum_regs n rargs) as [n1 vargs]_eqn.
+  exploit wf_valnum_regs; eauto. intros [A [B C]].
+  assert (wf_numbering (kill_equations (filter_after_store chunk addr vargs) n1)).
+    apply wf_kill_equations. auto.
+  destruct chunk; auto; apply wf_add_rhs; auto.
+Qed.
+
 Lemma wf_transfer:
   forall f pc n, wf_numbering n -> wf_numbering (transfer f pc n).
 Proof.
@@ -230,25 +244,22 @@ Proof.
   destruct i; auto.
   apply wf_add_op; auto.
   apply wf_add_load; auto.
-  apply wf_kill_loads; auto.
+  apply wf_add_store; auto.
   apply wf_empty_numbering.
   apply wf_empty_numbering.
-  apply wf_add_unknown. apply wf_kill_loads; auto.
+  apply wf_add_unknown. apply wf_kill_equations; auto.
 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.
+  forall f approx pc, analyze f = Some approx -> wf_numbering approx!!pc.
 Proof.
   unfold analyze; intros.
-  caseEq (Solver.fixpoint (successors 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 *)
@@ -264,7 +275,6 @@ 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. *)
@@ -303,7 +313,7 @@ Qed.
   extensional with respect to [valu_agree]. *)
 
 Lemma numbering_holds_exten:
-  forall valu1 valu2 n rs,
+  forall valu1 valu2 n rs m,
   valu_agree valu1 valu2 n.(num_next) ->
   wf_numbering n ->
   numbering_holds valu1 ge sp rs m n ->
@@ -328,7 +338,7 @@ Qed.
   value numbers. *)
 
 Lemma valnum_reg_holds:
-  forall valu1 rs n r n' v,
+  forall valu1 rs n r n' v m,
   wf_numbering n ->
   numbering_holds valu1 ge sp rs m n ->
   valnum_reg n r = (n', v) ->
@@ -351,22 +361,21 @@ Proof.
   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.
+  destruct (numbering_holds_exten _ _ _ _ _ AG H0 H1) as [A B].
   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. 
+  rewrite PTree.gsspec in H5. destruct (peq r0 r).
+  inv H5. rewrite peq_true. auto.
+  rewrite peq_false. auto. 
+  assert (Plt vn (num_next n)). inv H0. eauto. 
+  red; intros; subst; eapply Plt_strict; eauto. 
+  split. unfold valu2. rewrite VMap.gss. auto. 
   auto.
 Qed.
 
 Lemma valnum_regs_holds:
-  forall rs rl valu1 n n' vl,
+  forall rs rl valu1 n n' vl m,
   wf_numbering n ->
   numbering_holds valu1 ge sp rs m n ->
   valnum_regs n rl = (n', vl) ->
@@ -378,15 +387,15 @@ Proof.
   induction rl; simpl; intros.
   (* base case *)
   inversion H1; subst n'; subst vl.
-  exists valu1. split. auto. split. reflexivity. apply valu_agree_refl.
+  exists valu1. split. auto. split. auto. 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).
+  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). 
+  generalize (IHrl _ _ _ _ _ D A EQs). 
   intros [valu3 [P [Q R]]].
   exists valu3. 
   split. auto. 
@@ -398,7 +407,7 @@ Qed.
   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 :=
+    (valu: valnum -> val) (rh: rhs) (m: mem) (v: val) : Prop :=
   match rh with
   | Op op vl => 
       eval_operation ge sp op (List.map valu vl) m = Some v
@@ -409,23 +418,23 @@ Definition rhs_evals_to
   end.
 
 Lemma equation_evals_to_holds_1:
-  forall valu rh v vres,
-  rhs_evals_to valu rh v ->
+  forall valu rh v vres m,
+  rhs_evals_to valu rh m v ->
   equation_holds valu ge sp m vres rh ->
   valu vres = v.
 Proof.
-  intros until vres. unfold rhs_evals_to, equation_holds.
+  intros until m. 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,
+  forall valu rh v vres m,
   wf_rhs vres rh ->
-  rhs_evals_to valu rh v ->
+  rhs_evals_to valu rh m 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.
+  intros until m. unfold wf_rhs, rhs_evals_to, equation_holds.
   rewrite VMap.gss. 
   assert (forall vl: list valnum,
             (forall v, In v vl -> Plt v vres) ->
@@ -438,13 +447,14 @@ 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,
+Lemma add_rhs_satisfiable_gen:
+  forall n rh valu1 rs rd rs' m,
   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).
+  rhs_evals_to valu1 rh m (rs'#rd) ->
+  (forall r, r <> rd -> rs'#r = rs#r) ->
+  numbering_satisfiable ge sp rs' m (add_rhs n rd rh).
 Proof.
   intros. unfold add_rhs. 
   caseEq (find_valnum_rhs rh n.(num_eqs)).
@@ -452,34 +462,45 @@ Proof.
   intros vres FINDVN. inversion H1.
   exists valu1. split; simpl; intros.
   auto. 
-  rewrite Regmap.gsspec. 
-  rewrite PTree.gsspec in H5.
+  rewrite PTree.gsspec in H6.
   destruct (peq r rd).
+  inv H6. 
   symmetry. eapply equation_evals_to_holds_1; eauto.
-  apply H3. apply find_valnum_rhs_correct. congruence.
-  auto.
+  apply H4. apply find_valnum_rhs_correct. congruence.
+  rewrite H3; auto.
   (* RHS not found *)
   intro FINDVN. 
-  set (valu2 := VMap.set n.(num_next) v valu1).
+  set (valu2 := VMap.set n.(num_next) (rs'#rd) 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.
+  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.
+  destruct H6. 
+  inv H6. unfold valu2. eapply equation_evals_to_holds_2; eauto. auto. 
+  rewrite PTree.gsspec in H6. destruct (peq r rd).
+  unfold valu2. inv H6. rewrite VMap.gss. auto.
+  rewrite H3; auto.
+Qed.
+
+Lemma add_rhs_satisfiable:
+  forall n rh valu1 rs rd v m,
+  wf_numbering n ->
+  wf_rhs n.(num_next) rh ->
+  numbering_holds valu1 ge sp rs m n ->
+  rhs_evals_to valu1 rh m v ->
+  numbering_satisfiable ge sp (rs#rd <- v) m (add_rhs n rd rh).
+Proof.
+  intros. eapply add_rhs_satisfiable_gen; eauto. 
+  rewrite Regmap.gss; auto.
+  intros. apply Regmap.gso; 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,
+  forall n rs op args dst v m,
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
   eval_operation ge sp op rs##args m = Some v ->
@@ -491,13 +512,13 @@ Proof.
   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 (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 (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. 
@@ -507,19 +528,17 @@ Qed.
   set after execution of the corresponding [Iload] instruction. *)
 
 Lemma add_load_satisfiable:
-  forall n rs chunk addr args dst a v,
+  forall n rs chunk addr args dst a v m,
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
   eval_addressing ge sp addr rs##args = Some a ->
   Mem.loadv chunk m a = Some v ->
-  numbering_satisfiable ge sp 
-     (rs#dst <- v)
-     m (add_load n dst chunk addr args).
+  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 (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. 
@@ -529,11 +548,10 @@ Qed.
   register set after setting the target register to any value. *)
 
 Lemma add_unknown_satisfiable:
-  forall n rs dst v,
+  forall n rs dst v m,
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
-  numbering_satisfiable ge sp 
-     (rs#dst <- v) m (add_unknown n dst).
+  numbering_satisfiable ge sp (rs#dst <- v) m (add_unknown n dst).
 Proof.
   intros. destruct H0 as [valu A]. 
   set (valu' := VMap.set n.(num_next) v valu).
@@ -548,39 +566,77 @@ Proof.
   eauto.
 Qed.
 
-(** [kill_load] preserves satisfiability.  Moreover, the resulting numbering
-  is satisfiable in any concrete memory state. *)
+(** Satisfiability of [kill_equations]. *)
 
-Lemma kill_load_eqs_ops:
-  forall v rhs eqs,
-  In (v, rhs) (kill_load_eqs eqs) ->
-  match rhs with
-  | Op op _ => op_depends_on_memory op = false
-  | Load _ _ _ => False
-  end.
+Lemma kill_equations_holds:
+  forall pred valu n rs m m',
+  (forall v r,
+   equation_holds valu ge sp m v r -> pred r = false -> equation_holds valu ge sp m' v r) ->
+  numbering_holds valu ge sp rs m n ->
+  numbering_holds valu ge sp rs m' (kill_equations pred n).
 Proof.
-  induction eqs; simpl; intros.
-  elim H.
-  destruct a. destruct r. destruct (op_depends_on_memory o) as [] _eqn.
-  apply IHeqs; auto.
-  simpl in H; destruct H. inv H. auto. 
-  apply IHeqs. auto. 
-  apply IHeqs. auto.
+  intros. destruct H0 as [A B]. red; simpl. split; intros. 
+  exploit kill_eqs_in; eauto. intros [C D]. eauto. 
+  auto.
 Qed.
 
-Lemma kill_load_satisfiable:
-  forall n rs m',
+(** [kill_loads] preserves satisfiability.  Moreover, the resulting numbering
+  is satisfiable in any concrete memory state. *)
+
+Lemma kill_loads_satisfiable:
+  forall n rs m m',
   numbering_satisfiable ge sp rs m n ->
   numbering_satisfiable ge sp rs m' (kill_loads n).
 Proof.
-  intros. inv H. destruct H0. generalize (kill_load_eqs_incl n.(num_eqs)). intro.
-  exists x. split; intros.
-  generalize (H _ _ (H1 _ H2)). 
-  generalize (kill_load_eqs_ops _ _ _ H2).
-  destruct rh; simpl.
-  intros. rewrite <- H4. apply op_depends_on_memory_correct; auto.
-  tauto.
-  apply H0. auto. 
+  intros. destruct H as [valu A]. exists valu. eapply kill_equations_holds with (m := m); eauto.
+  intros. destruct r; simpl in *. rewrite <- H. apply op_depends_on_memory_correct; auto. 
+  congruence.
+Qed.
+
+(** [add_store] returns a numbering that is satisfiable in the memory state
+  after execution of the corresponding [Istore] instruction. *)
+
+Lemma add_store_satisfiable:
+  forall n rs chunk addr args src a m m',
+  wf_numbering n ->
+  numbering_satisfiable ge sp rs m n ->
+  eval_addressing ge sp addr rs##args = Some a ->
+  Mem.storev chunk m a (rs#src) = Some m' ->
+  Val.has_type (rs#src) (type_of_chunk chunk) ->
+  numbering_satisfiable ge sp rs m' (add_store n chunk addr args src).
+Proof.
+  intros. unfold add_store. destruct H0 as [valu A].
+  destruct (valnum_regs n args) as [n1 vargs]_eqn.
+  exploit valnum_regs_holds; eauto. intros [valu' [B [C D]]].
+  exploit wf_valnum_regs; eauto. intros [U [V W]].
+  set (n2 := kill_equations (filter_after_store chunk addr vargs) n1).
+  assert (numbering_holds valu' ge sp rs m' n2).
+    apply kill_equations_holds with (m := m); auto.
+    intros. destruct r; simpl in *. 
+    rewrite <- H0. apply op_depends_on_memory_correct; auto.
+    destruct H0 as [a' [P Q]]. 
+    destruct (eq_list_valnum vargs l); simpl in H4; try congruence. subst l.
+    rewrite negb_false_iff in H4.
+    exists a'; split; auto. 
+    destruct a; simpl in H2; try congruence.
+    destruct a'; simpl in Q; try congruence.
+    simpl. rewrite <- Q. 
+    rewrite C in P. eapply Mem.load_store_other; eauto.
+    exploit addressing_separated_sound; eauto. intuition congruence.
+  assert (N2: numbering_satisfiable ge sp rs m' n2).
+    exists valu'; auto.
+  set (n3 := add_rhs n2 src (Load chunk addr vargs)).
+  assert (N3: Val.load_result chunk (rs#src) = rs#src -> numbering_satisfiable ge sp rs m' n3).
+    intro EQ. unfold n3. apply add_rhs_satisfiable_gen with valu' rs.
+    apply wf_kill_equations; auto.
+    red. auto. auto.
+    red. exists a; split. congruence. 
+    rewrite <- EQ. destruct a; simpl in H2; try discriminate. simpl. 
+    eapply Mem.load_store_same; eauto. 
+    auto.
+  destruct chunk; auto; apply N3. 
+  simpl in H3. destruct (rs#src); auto || contradiction.
+  simpl in H3. destruct (rs#src); auto || contradiction.
 Qed.
 
 (** Correctness of [reg_valnum]: if it returns a register [r],
@@ -613,10 +669,10 @@ Qed.
   result value of the operation or memory load. *)
 
 Lemma find_rhs_correct:
-  forall valu rs n rh r,
+  forall valu rs m n rh r,
   numbering_holds valu ge sp rs m n ->
   find_rhs n rh = Some r ->
-  rhs_evals_to valu rh rs#r.
+  rhs_evals_to valu rh m rs#r.
 Proof.
   intros until r.  intros NH. 
   unfold find_rhs. 
@@ -630,7 +686,7 @@ Proof.
 Qed.
 
 Lemma find_op_correct:
-  forall rs n op args r,
+  forall rs m n op args r,
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
   find_op n op args = Some r ->
@@ -638,15 +694,15 @@ Lemma find_op_correct:
 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).
+  generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR).
   intros [valu2 [NH2 [EQ AG]]].
   rewrite <- EQ. 
-  change (rhs_evals_to valu2 (Op op vl) rs#r).
+  change (rhs_evals_to valu2 (Op op vl) m rs#r).
   eapply find_rhs_correct; eauto.
 Qed.
 
 Lemma find_load_correct:
-  forall rs n chunk addr args r,
+  forall rs m n chunk addr args r,
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
   find_load n chunk addr args = Some r ->
@@ -656,10 +712,10 @@ Lemma find_load_correct:
 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).
+  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).
+  change (rhs_evals_to valu2 (Load chunk addr vl) m rs#r).
   eapply find_rhs_correct; eauto.
 Qed.
 
@@ -672,38 +728,29 @@ End SATISFIABILITY.
   satisfiability at [pc']. *)
 
 Theorem analysis_correct_1:
-  forall ge sp rs m f pc pc' i,
+  forall ge sp rs m f approx pc pc' i,
+  analyze f = Some approx ->
   f.(fn_code)!pc = Some i -> In pc' (successors_instr i) ->
-  numbering_satisfiable ge sp rs m (transfer f pc (analyze f)!!pc) ->
-  numbering_satisfiable ge sp rs m (analyze f)!!pc'.
-Proof.
-  intros until i.
-  generalize (wf_analyze f pc).
-  unfold analyze.
-  caseEq (Solver.fixpoint (successors f) (transfer f) (fn_entrypoint f)).
-  intros res FIXPOINT WF AT SUCC.
-  assert (Numbering.ge res!!pc' (transfer f pc res!!pc)).
+  numbering_satisfiable ge sp rs m (transfer f pc approx!!pc) ->
+  numbering_satisfiable ge sp rs m approx!!pc'.
+Proof.
+  intros.
+  assert (Numbering.ge approx!!pc' (transfer f pc approx!!pc)).
     eapply Solver.fixpoint_solution; eauto.
     unfold successors_list, successors. rewrite PTree.gmap1.
-    rewrite AT. auto.
-  apply H.
-  intros. rewrite PMap.gi. apply empty_numbering_satisfiable.
+    rewrite H0. auto.
+  apply H3. auto.
 Qed.
 
 Theorem analysis_correct_entry:
-  forall ge sp rs m f,
-  numbering_satisfiable ge sp rs m (analyze f)!!(f.(fn_entrypoint)).
+  forall ge sp rs m f approx,
+  analyze f = Some approx ->
+  numbering_satisfiable ge sp rs m approx!!(f.(fn_entrypoint)).
 Proof.
   intros. 
-  replace ((analyze f)!!(f.(fn_entrypoint)))
-          with empty_numbering.
+  replace (approx!!(f.(fn_entrypoint))) with Solver.L.top.
   apply empty_numbering_satisfiable.
-  unfold analyze.
-  caseEq (Solver.fixpoint (successors 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. 
+  symmetry. eapply Solver.fixpoint_entry; eauto.
 Qed.
 
 (** * Semantic preservation *)
@@ -711,40 +758,43 @@ Qed.
 Section PRESERVATION.
 
 Variable prog: program.
-Let tprog := transf_program prog.
+Variable tprog : program.
+Hypothesis TRANSF: transf_program prog = OK tprog.
 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_fundef prog).
+Proof (Genv.find_symbol_transf_partial transf_fundef prog TRANSF).
 
 Lemma varinfo_preserved:
   forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof (Genv.find_var_info_transf transf_fundef prog).
+Proof (Genv.find_var_info_transf_partial transf_fundef prog TRANSF).
 
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog).
+  exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_transf_partial transf_fundef prog TRANSF).
 
 Lemma funct_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (transf_fundef f).
-Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog).
+  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial transf_fundef prog TRANSF).
 
 Lemma sig_preserved:
-  forall f, funsig (transf_fundef f) = funsig f.
+  forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f.
 Proof.
-  destruct f; reflexivity.
+  unfold transf_fundef; intros. destruct f; monadInv H; auto.
+  unfold transf_function in EQ. destruct (type_function f); try discriminate. 
+  destruct (analyze f); try discriminate. inv EQ; auto. 
 Qed.
 
 Lemma find_function_translated:
   forall ros rs f,
   find_function ge ros rs = Some f ->
-  find_function tge ros rs = Some (transf_fundef f).
+  exists tf, find_function tge ros rs = Some tf /\ transf_fundef f = OK tf.
 Proof.
   intros until f; destruct ros; simpl.
   intro. apply functions_translated; auto.
@@ -753,6 +803,14 @@ Proof.
   discriminate.
 Qed.
 
+Definition transf_function' (f: function) (approxs: PMap.t numbering) : function :=
+  mkfunction
+    f.(fn_sig)
+    f.(fn_params)
+    f.(fn_stacksize)
+    (transf_code approxs f.(fn_code))
+    f.(fn_entrypoint).
+
 (** The proof of semantic preservation is a simulation argument using
   diagrams of the following form:
 <<
@@ -769,38 +827,52 @@ Qed.
   the numbering at [pc] (returned by the static analysis) is satisfiable.
 *)
 
-Inductive match_stackframes: stackframe -> stackframe -> Prop :=
-  match_stackframes_intro:
-    forall res sp pc rs f,
-    (forall v m, numbering_satisfiable ge sp (rs#res <- v) m (analyze f)!!pc) ->
+Inductive match_stackframes: list stackframe -> list stackframe -> typ -> Prop :=
+  | match_stackframes_nil:
+      match_stackframes nil nil Tint
+  | match_stackframes_cons:
+      forall res sp pc rs f approx tyenv s s' ty
+           (ANALYZE: analyze f = Some approx)
+           (WTF: wt_function f tyenv)
+           (WTREGS: wt_regset tyenv rs)
+           (TYRES: tyenv res = ty)
+           (SAT: forall v m, numbering_satisfiable ge sp (rs#res <- v) m approx!!pc)
+           (STACKS: match_stackframes s s' (proj_sig_res (fn_sig f))),
     match_stackframes
-      (Stackframe res f sp pc rs)
-      (Stackframe res (transf_function f) sp pc rs).
+      (Stackframe res f sp pc rs :: s)
+      (Stackframe res (transf_function' f approx) sp pc rs :: s')
+      ty.
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
-      forall s sp pc rs m s' f
-             (SAT: numbering_satisfiable ge sp rs m (analyze f)!!pc)
-             (STACKS: list_forall2 match_stackframes s s'),
+      forall s sp pc rs m s' f approx tyenv
+             (ANALYZE: analyze f = Some approx)
+             (WTF: wt_function f tyenv)
+             (WTREGS: wt_regset tyenv rs)
+             (SAT: numbering_satisfiable ge sp rs m approx!!pc)
+             (STACKS: match_stackframes s s' (proj_sig_res (fn_sig f))),
       match_states (State s f sp pc rs m)
-                   (State s' (transf_function f) sp pc rs m)
+                   (State s' (transf_function' f approx) sp pc rs m)
   | match_states_call:
-      forall s f args m s',
-      list_forall2 match_stackframes s s' ->
+      forall s f tf args m s',
+      match_stackframes s s' (proj_sig_res (funsig f)) ->
+      Val.has_type_list args (sig_args (funsig f)) ->
+      transf_fundef f = OK tf ->
       match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef f) args m)
+                   (Callstate s' tf args m)
   | match_states_return:
-      forall s s' v m,
-      list_forall2 match_stackframes s s' ->
+      forall s s' ty v m,
+      match_stackframes s s' ty ->
+      Val.has_type v ty ->
       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_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr));
+  | H1: (PTree.get ?pc ?c = Some ?instr), f: function, approx: PMap.t numbering |- _ =>
+      cut ((transf_function' f approx).(fn_code)!pc = Some(transf_instr approx!!pc instr));
       [ simpl transf_instr
-      | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
+      | unfold transf_function', transf_code; simpl; rewrite PTree.gmap; 
         unfold option_map; rewrite H1; reflexivity ]
   end.
 
@@ -815,89 +887,105 @@ Proof.
   induction 1; intros; inv MS; try (TransfInstr; intro C).
 
   (* Inop *)
-  exists (State s' (transf_function f) sp pc' rs m); split.
+  exists (State s' (transf_function' f approx) sp pc' rs m); split.
   apply exec_Inop; auto.
   econstructor; eauto. 
   eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H; auto.
 
   (* Iop *)
-  exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
+  exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split.
   assert (eval_operation tge sp op rs##args m = Some v).
     rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
-  generalize C; clear C.
-  case (is_trivial_op op).
-  intro. eapply exec_Iop'; eauto. 
-  caseEq (find_op (analyze f)!!pc op args). intros r FIND CODE.
+  destruct (is_trivial_op op) as []_eqn.
+  eapply exec_Iop'; eauto. 
+  destruct (find_op approx!!pc op args) as [r|]_eqn. 
   eapply exec_Iop'; eauto. simpl. 
   assert (eval_operation ge sp op rs##args m = Some rs#r).
     eapply find_op_correct; eauto.
     eapply wf_analyze; eauto.
   congruence.
-  intros. eapply exec_Iop'; eauto.
+  eapply exec_Iop'; eauto.
   econstructor; eauto.
+  apply wt_regset_assign; auto. 
+  generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
+  simpl in H0. inv H0. rewrite <- H3. apply WTREGS.
+  replace (tyenv res) with (snd (type_of_operation op)).
+  eapply type_of_operation_sound; eauto.
+  rewrite <- H6. reflexivity.
   eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H. 
-  eapply add_op_satisfiable; eauto. apply wf_analyze.
+  eapply add_op_satisfiable; eauto. eapply wf_analyze; eauto.
 
   (* Iload *)
-  exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split.
+  exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split.
   assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  generalize C; clear C.
-  caseEq (find_load (analyze f)!!pc chunk addr args). intros r FIND CODE.
+  destruct (find_load approx!!pc chunk addr args) as [r|]_eqn.
   eapply exec_Iop'; eauto. simpl. 
   assert (exists a, eval_addressing ge sp addr rs##args = Some a
                  /\ Mem.loadv chunk m a = Some rs#r).
     eapply find_load_correct; eauto.
     eapply wf_analyze; eauto.
-  elim H3; intros a' [A B].
+  destruct H3 as [a' [A B]].
   congruence.
-  intros. eapply exec_Iload'; eauto.
+  eapply exec_Iload'; eauto.
   econstructor; eauto.
+  generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
+  apply wt_regset_assign. auto. rewrite H8. eapply type_of_chunk_correct; eauto.
   eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
-  eapply add_load_satisfiable; eauto. apply wf_analyze.
+  eapply add_load_satisfiable; eauto. eapply wf_analyze; eauto.
 
   (* Istore *)
-  exists (State s' (transf_function f) sp pc' rs m'); split.
+  exists (State s' (transf_function' f approx) sp pc' rs m'); split.
   assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Istore; eauto.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H.
-  eapply kill_load_satisfiable; eauto. 
+  eapply add_store_satisfiable; eauto. eapply wf_analyze; eauto.
+  generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
+  rewrite <- H8. auto.
 
   (* Icall *)
-  exploit find_function_translated; eauto. intro FIND'.
+  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. 
   econstructor; split.
   eapply exec_Icall; eauto.
-  apply sig_preserved. 
+  apply sig_preserved; auto.
+  generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
   econstructor; eauto. 
-  constructor; auto. 
   econstructor; eauto. 
   intros. eapply analysis_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply empty_numbering_satisfiable.
+  rewrite <- H7. apply wt_regset_list; auto. 
 
   (* Itailcall *)
-  exploit find_function_translated; eauto. intro FIND'.
+  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. 
   econstructor; split.
   eapply exec_Itailcall; eauto.
-  apply sig_preserved. 
-  econstructor; eauto.
+  apply sig_preserved; auto.
+  generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
+  econstructor; eauto. 
+  replace (proj_sig_res (funsig fd)) with (proj_sig_res (fn_sig f)). auto. 
+  unfold proj_sig_res. rewrite H6; auto.
+  rewrite <- H7. apply wt_regset_list; auto.
 
   (* Ibuiltin *)
   econstructor; split.
   eapply exec_Ibuiltin; eauto. 
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
+  generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
   econstructor; eauto.
+  apply wt_regset_assign; auto. 
+  rewrite H6. eapply external_call_well_typed; eauto. 
   eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H. 
-  apply add_unknown_satisfiable. apply wf_kill_loads. apply wf_analyze.
-  eapply kill_load_satisfiable; eauto. 
+  apply add_unknown_satisfiable. apply wf_kill_equations. eapply wf_analyze; eauto.
+  eapply kill_loads_satisfiable; eauto. 
 
   (* Icond *)
   econstructor; split.
@@ -916,26 +1004,36 @@ Proof.
   (* Ireturn *)
   econstructor; split.
   eapply exec_Ireturn; eauto.
-  constructor; auto.
+  econstructor; eauto.
+  generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
+  unfold proj_sig_res. rewrite <- H2. destruct or; simpl; auto. 
 
   (* internal function *)
-  simpl. econstructor; split.
+  monadInv H7. unfold transf_function in EQ. 
+  destruct (type_function f) as [tyenv|]_eqn; try discriminate.
+  destruct (analyze f) as [approx|]_eqn; inv EQ. 
+  assert (WTF: wt_function f tyenv). apply type_function_correct; auto.
+  econstructor; split.
   eapply exec_function_internal; eauto. 
   simpl. econstructor; eauto.
-  apply analysis_correct_entry. 
+  apply wt_init_regs. inv WTF. rewrite wt_params; auto.
+  apply analysis_correct_entry; auto.
 
   (* external function *)
-  simpl. econstructor; split.
+  monadInv H7. 
+  econstructor; split.
   eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
+  simpl. eapply external_call_well_typed; eauto. 
 
   (* return *)
-  inv H3. inv H1.
+  inv H3.
   econstructor; split.
   eapply exec_return; eauto.
-  econstructor; eauto. 
+  econstructor; eauto.
+  apply wt_regset_assign; auto. 
 Qed.
 
 Lemma transf_initial_states:
@@ -943,14 +1041,15 @@ Lemma transf_initial_states:
   exists st2, initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. 
-  exists (Callstate nil (transf_fundef f) nil m0); split.
+  exploit funct_ptr_translated; eauto. intros [tf [A B]].
+  exists (Callstate nil tf nil m0); split.
   econstructor; eauto.
-  apply Genv.init_mem_transf; auto.
-  change (prog_main tprog) with (prog_main prog).
+  eapply Genv.init_mem_transf_partial; eauto.
+  replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
-  apply funct_ptr_translated; auto.
-  rewrite <- H3. apply sig_preserved. 
-  constructor. constructor.
+  symmetry. eapply transform_partial_program_main; eauto.
+  rewrite <- H3. apply sig_preserved; auto.
+  constructor. rewrite H3. constructor. rewrite H3. constructor. auto.
 Qed.
 
 Lemma transf_final_states:
-- 
cgit