Updated ARM backend wrt new static analyses and optimizations.

NeedOp, Deadcode: must have distinct needs per argument of an operator.
  This change remains to be propagated to IA32 and PPC.


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

5 files changed, 176 insertions, 128 deletions

diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 9efeca1..98bc14a 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -31,24 +31,34 @@ Require Import NeedOp.
 
 (** * Part 1: the static analysis *)
 
+Definition add_need_all (r: reg) (ne: nenv) : nenv :=
+  NE.set r All ne.
+
 Definition add_need (r: reg) (nv: nval) (ne: nenv) : nenv :=
   NE.set r (nlub nv (NE.get r ne)) ne.
 
-Fixpoint add_needs (rl: list reg) (nv: nval) (ne: nenv) : nenv :=
+Fixpoint add_needs_all (rl: list reg) (ne: nenv) : nenv :=
   match rl with
   | nil => ne
-  | r1 :: rs => add_need r1 nv (add_needs rs nv ne)
+  | r1 :: rs => add_need_all r1 (add_needs_all rs ne)
+  end.
+
+Fixpoint add_needs (rl: list reg) (nvl: list nval) (ne: nenv) : nenv :=
+  match rl, nvl with
+  | nil, _ => ne
+  | r1 :: rs, nil => add_needs_all rl ne
+  | r1 :: rs, nv1 :: nvs => add_need r1 nv1 (add_needs rs nvs ne)
   end.
 
-Definition add_ros_need (ros: reg + ident) (ne: nenv) : nenv :=
+Definition add_ros_need_all (ros: reg + ident) (ne: nenv) : nenv :=
   match ros with
-  | inl r => add_need r All ne
+  | inl r => add_need_all r ne
   | inr s => ne
   end.
 
-Definition add_opt_need (or: option reg) (ne: nenv) : nenv :=
+Definition add_opt_need_all (or: option reg) (ne: nenv) : nenv :=
   match or with
-  | Some r => add_need r All ne
+  | Some r => add_need_all r ne
   | None => ne
   end.
 
@@ -64,26 +74,26 @@ Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (
                           (ne: NE.t) (nm: nmem) : NA.t :=
   match ef, args with
   | EF_vload chunk, a1::nil =>
-      (add_needs args All (kill res ne),
+      (add_needs_all args (kill res ne),
        nmem_add nm (aaddr app a1) (size_chunk chunk))
   | EF_vload_global chunk id ofs, nil =>
-      (add_needs args All (kill res ne),
+      (add_needs_all args (kill res ne),
        nmem_add nm (Gl id ofs) (size_chunk chunk))
   | EF_vstore chunk, a1::a2::nil =>
-      (add_need a1 All (add_need a2 (store_argument chunk) (kill res ne)), nm)
+      (add_need_all a1 (add_need a2 (store_argument chunk) (kill res ne)), nm)
   | EF_vstore_global chunk id ofs, a1::nil =>
       (add_need a1 (store_argument chunk) (kill res ne), nm)
   | EF_memcpy sz al, dst::src::nil =>
       if nmem_contains nm (aaddr app dst) sz then
-       (add_needs args All (kill res ne),
+       (add_needs_all args (kill res ne),
         nmem_add (nmem_remove nm (aaddr app dst) sz) (aaddr app src) sz)
       else (ne, nm)
   | EF_annot txt targs, _ =>
-      (add_needs args All (kill res ne), nm)
+      (add_needs_all args (kill res ne), nm)
   | EF_annot_val txt targ, _ =>
-      (add_needs args All (kill res ne), nm)
+      (add_needs_all args (kill res ne), nm)
   | _, _ =>
-      (add_needs args All (kill res ne), nmem_all) 
+      (add_needs_all args (kill res ne), nmem_all) 
   end.
 
 Definition transfer (f: function) (approx: PMap.t VA.t)
@@ -103,27 +113,27 @@ Definition transfer (f: function) (approx: PMap.t VA.t)
       let ndst := nreg ne dst in
       if is_dead ndst then after
       else if is_int_zero ndst then (kill dst ne, nm)
-      else (add_needs args All (kill dst ne),
+      else (add_needs_all args (kill dst ne),
             nmem_add nm (aaddressing approx!!pc addr args) (size_chunk chunk))
   | Some (Istore chunk addr args src s) =>
       let p := aaddressing approx!!pc addr args in
       if nmem_contains nm p (size_chunk chunk)
-      then (add_needs args All (add_need src (store_argument chunk) ne),
+      then (add_needs_all args (add_need src (store_argument chunk) ne),
             nmem_remove nm p (size_chunk chunk))
       else after
   | Some(Icall sig ros args res s) =>
-      (add_needs args All (add_ros_need ros (kill res ne)), nmem_all)
+      (add_needs_all args (add_ros_need_all ros (kill res ne)), nmem_all)
   | Some(Itailcall sig ros args) =>
-      (add_needs args All (add_ros_need ros NE.bot),
+      (add_needs_all args (add_ros_need_all ros NE.bot),
        nmem_dead_stack f.(fn_stacksize))
   | Some(Ibuiltin ef args res s) =>
       transfer_builtin approx!!pc ef args res ne nm
   | Some(Icond cond args s1 s2) =>
       (add_needs args (needs_of_condition cond) ne, nm)
   | Some(Ijumptable arg tbl) =>
-      (add_need arg All ne, nm)
+      (add_need_all arg ne, nm)
   | Some(Ireturn optarg) =>
-      (add_opt_need optarg ne, nmem_dead_stack f.(fn_stacksize))
+      (add_opt_need_all optarg ne, nmem_dead_stack f.(fn_stacksize))
   end.
 
 Module DS := Backward_Dataflow_Solver(NA)(NodeSetBackward).
@@ -144,7 +154,10 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t)
       else if is_int_zero nres then
         Iop (Ointconst Int.zero) nil res s
       else if operation_is_redundant op nres then 
-        match args with arg :: _ => Iop Omove (arg :: nil) res s | nil => instr end
+        match args with
+        | arg :: _ => Iop Omove (arg :: nil) res s
+        | nil => instr
+        end
       else
         instr
   | Iload chunk addr args dst s =>
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index deb8628..2fdedc6 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -264,83 +264,90 @@ Qed.
 
 (** * Properties of the need environment *)
 
-Lemma add_need_ge:
-  forall r nv ne,
-  nge (NE.get r (add_need r nv ne)) nv /\ NE.ge (add_need r nv ne) ne.
+Lemma add_need_all_eagree:
+  forall e e' r ne,
+  eagree e e' (add_need_all r ne) -> eagree e e' ne.
 Proof.
-  intros. unfold add_need. split. 
-  rewrite NE.gsspec; rewrite peq_true. apply nge_lub_l. 
-  red. intros. rewrite NE.gsspec. destruct (peq p r).
-  subst. apply NVal.ge_lub_right. 
-  apply NVal.ge_refl. apply NVal.eq_refl. 
+  intros; red; intros. generalize (H r0). unfold add_need_all. 
+  rewrite NE.gsspec. destruct (peq r0 r); auto with na. 
 Qed.
 
-Lemma add_needs_ge:
-  forall rl nv ne,
-  (forall r, In r rl -> nge (NE.get r (add_needs rl nv ne)) nv)
-  /\ NE.ge (add_needs rl nv ne) ne.
+Lemma add_need_all_lessdef:
+  forall e e' r ne,
+  eagree e e' (add_need_all r ne) -> Val.lessdef e#r e'#r.
 Proof.
-  induction rl; simpl; intros. 
-  split. tauto. apply NE.ge_refl. apply NE.eq_refl.
-  destruct (IHrl nv ne) as [A B].
-  split; intros. 
-  destruct H. subst a. apply add_need_ge. 
-  apply nge_trans with (NE.get r (add_needs rl nv ne)). 
-  apply add_need_ge. apply A; auto.
-  eapply NE.ge_trans; eauto. apply add_need_ge.
+  intros. generalize (H r); unfold add_need_all. 
+  rewrite NE.gsspec, peq_true. auto with na.
 Qed.
 
 Lemma add_need_eagree:
-  forall e e' r nv ne, eagree e e' (add_need r nv ne) -> eagree e e' ne.
+  forall e e' r nv ne,
+  eagree e e' (add_need r nv ne) -> eagree e e' ne.
 Proof.
-  intros. eapply eagree_ge; eauto. apply add_need_ge. 
+  intros; red; intros. generalize (H r0); unfold add_need.
+  rewrite NE.gsspec. destruct (peq r0 r); auto.
+  subst r0. intros. eapply nge_agree; eauto. apply nge_lub_r.
 Qed.
 
 Lemma add_need_vagree:
-  forall e e' r nv ne, eagree e e' (add_need r nv ne) -> vagree e#r e'#r nv.
+  forall e e' r nv ne,
+  eagree e e' (add_need r nv ne) -> vagree e#r e'#r nv.
 Proof.
-  intros. eapply nge_agree. eapply add_need_ge. apply H. 
+  intros. generalize (H r); unfold add_need.
+  rewrite NE.gsspec, peq_true. intros. eapply nge_agree; eauto. apply nge_lub_l.
 Qed.
 
-Lemma add_needs_eagree:
-  forall nv rl e e' ne, eagree e e' (add_needs rl nv ne) -> eagree e e' ne.
+Lemma add_needs_all_eagree:
+  forall rl e e' ne,
+  eagree e e' (add_needs_all rl ne) -> eagree e e' ne.
 Proof.
-  intros. eapply eagree_ge; eauto. apply add_needs_ge. 
+  induction rl; simpl; intros.
+  auto.
+  apply IHrl. eapply add_need_all_eagree; eauto. 
 Qed.
 
-Lemma add_needs_vagree:
-  forall nv rl e e' ne, eagree e e' (add_needs rl nv ne) -> vagree_list e##rl e'##rl nv.
+Lemma add_needs_all_lessdef:
+  forall rl e e' ne,
+  eagree e e' (add_needs_all rl ne) -> Val.lessdef_list e##rl e'##rl.
 Proof.
-  intros. destruct (add_needs_ge rl nv ne) as [A B].
-  set (ne' := add_needs rl nv ne) in *. 
-  revert A; generalize rl. induction rl0; simpl; intros.
+  induction rl; simpl; intros. 
   constructor.
-  constructor. eapply nge_agree; eauto. apply IHrl0. auto. 
+  constructor. eapply add_need_all_lessdef; eauto. 
+  eapply IHrl. eapply add_need_all_eagree; eauto. 
 Qed.
 
-Lemma add_need_lessdef:
-  forall e e' r ne, eagree e e' (add_need r All ne) -> Val.lessdef e#r e'#r.
+Lemma add_needs_eagree:
+  forall rl nvl e e' ne,
+  eagree e e' (add_needs rl nvl ne) -> eagree e e' ne.
 Proof.
-  intros. apply lessdef_vagree. eapply add_need_vagree; eauto. 
+  induction rl; simpl; intros.
+  auto.
+  destruct nvl. apply add_needs_all_eagree with (a :: rl); auto.
+  eapply IHrl. eapply add_need_eagree; eauto. 
 Qed.
 
-Lemma add_needs_lessdef:
-  forall e e' rl ne, eagree e e' (add_needs rl All ne) -> Val.lessdef_list e##rl e'##rl.
+Lemma add_needs_vagree:
+  forall rl nvl e e' ne,
+  eagree e e' (add_needs rl nvl ne) -> vagree_list e##rl e'##rl nvl.
 Proof.
-  intros. exploit add_needs_vagree; eauto. 
-  generalize rl. induction rl0; simpl; intros V; inv V. 
+  induction rl; simpl; intros.
   constructor.
-  constructor; auto.
+  destruct nvl.
+  apply vagree_lessdef_list. eapply add_needs_all_lessdef with (rl := a :: rl); eauto.
+  constructor. eapply add_need_vagree; eauto. 
+  eapply IHrl. eapply add_need_eagree; eauto. 
 Qed.
 
 Lemma add_ros_need_eagree:
-  forall e e' ros ne, eagree e e' (add_ros_need ros ne) -> eagree e e' ne.
+  forall e e' ros ne, eagree e e' (add_ros_need_all ros ne) -> eagree e e' ne.
 Proof.
-  intros. destruct ros; simpl in *. eapply add_need_eagree; eauto. auto. 
+  intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto. 
 Qed.
 
-Hint Resolve add_need_eagree add_need_vagree add_need_lessdef
-             add_needs_eagree add_needs_vagree add_needs_lessdef
+Hint Resolve add_need_all_eagree add_need_all_lessdef
+             add_need_eagree add_need_vagree
+             add_needs_all_eagree add_needs_all_lessdef
+             add_needs_eagree add_needs_vagree
              add_ros_need_eagree: na.
 
 Lemma eagree_init_regs:
@@ -449,7 +456,7 @@ Qed.
 Lemma find_function_translated:
   forall ros rs fd trs ne,
   find_function ge ros rs = Some fd ->
-  eagree rs trs (add_ros_need ros ne) ->
+  eagree rs trs (add_ros_need_all ros ne) ->
   exists tfd, find_function tge ros trs = Some tfd /\ transf_fundef rm fd = OK tfd.
 Proof.
   intros. destruct ros as [r|id]; simpl in *.
@@ -659,22 +666,23 @@ Ltac UseTransfer :=
   eapply match_succ_states; eauto. simpl; auto. 
   apply eagree_update; auto.
   * (* turned into a move *)
-  simpl in *. 
-  exploit operation_is_redundant_sound. eauto. eauto. eapply add_need_vagree. eauto. 
-  intros VA.
+  unfold fst in ENV. unfold snd in MEM. simpl in H0.
+  assert (VA: vagree v te#r (nreg ne res)).
+  { eapply operation_is_redundant_sound with (arg1' := te#r) (args' := te##args).
+    eauto. eauto. exploit add_needs_vagree; eauto. }
   econstructor; split.
   eapply exec_Iop; eauto. simpl; reflexivity. 
   eapply match_succ_states; eauto. simpl; auto. 
-  eapply eagree_update; eauto with na. 
+  eapply eagree_update; eauto 2 with na. 
 + (* preserved operation *)
   simpl in *.
-  exploit needs_of_operation_sound. eapply ma_perm; eauto. eauto. eauto with na. eauto with na.
+  exploit needs_of_operation_sound. eapply ma_perm; eauto. eauto. eauto 2 with na. eauto with na.
   intros [tv [A B]].
   econstructor; split. 
   eapply exec_Iop with (v := tv); eauto.
   rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
   eapply match_succ_states; eauto. simpl; auto. 
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
 
 - (* load *)
   TransfInstr; UseTransfer.
@@ -694,7 +702,7 @@ Ltac UseTransfer :=
   rewrite is_int_zero_sound by auto.
   destruct v; simpl; auto. apply iagree_zero.
 + (* preserved *)
-  exploit eval_addressing_lessdef. eapply add_needs_lessdef; eauto. eauto. 
+  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. 
   intros (ta & U & V). inv V; try discriminate.
   destruct ta; simpl in H1; try discriminate.
   exploit magree_load; eauto. 
@@ -702,10 +710,11 @@ Ltac UseTransfer :=
   intros. apply nlive_add with bc i; assumption. 
   intros (tv & P & Q).
   econstructor; split.
-  eapply exec_Iload with (a := Vptr b i); eauto.
+  eapply exec_Iload with (a := Vptr b i). eauto. 
   rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto. 
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na. 
+  apply eagree_update; eauto 2 with na. 
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. 
 
 - (* store *)
@@ -714,7 +723,7 @@ Ltac UseTransfer :=
              (size_chunk chunk)) eqn:CONTAINS.
 + (* preserved *)
   simpl in *. 
-  exploit eval_addressing_lessdef. eapply add_needs_lessdef; eauto. eauto. 
+  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. 
   intros (ta & U & V). inv V; try discriminate.
   destruct ta; simpl in H1; try discriminate.
   exploit magree_store_parallel. eauto. eauto. instantiate (1 := te#src). eauto with na.
@@ -723,10 +732,11 @@ Ltac UseTransfer :=
   intros. apply nlive_remove with bc b i; assumption. 
   intros (tm' & P & Q).
   econstructor; split.
-  eapply exec_Istore with (a := Vptr b i); eauto.
+  eapply exec_Istore with (a := Vptr b i). eauto. 
   rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto.
   eapply match_succ_states; eauto. simpl; auto.
-  eauto with na. 
+  eauto 3 with na. 
 + (* dead instruction, turned into a nop *)
   destruct a; simpl in H1; try discriminate.
   econstructor; split.
@@ -738,7 +748,7 @@ Ltac UseTransfer :=
 
 - (* call *)
   TransfInstr; UseTransfer.
-  exploit find_function_translated; eauto with na. intros (tfd & A & B).
+  exploit find_function_translated; eauto 2 with na. intros (tfd & A & B).
   econstructor; split.
   eapply exec_Icall; eauto. apply sig_function_translated; auto. 
   constructor. 
@@ -747,25 +757,25 @@ Ltac UseTransfer :=
   edestruct analyze_successors; eauto. simpl; eauto. 
   eapply eagree_ge; eauto. rewrite ANPC. simpl. 
   apply eagree_update; eauto with na.
-  auto. eauto with na. eapply magree_extends; eauto. apply nlive_all. 
+  auto. eauto 2 with na. eapply magree_extends; eauto. apply nlive_all. 
 
 - (* tailcall *)
   TransfInstr; UseTransfer.
-  exploit find_function_translated; eauto with na. intros (tfd & A & B).
+  exploit find_function_translated; eauto 2 with na. intros (tfd & A & B).
   exploit magree_free. eauto. eauto. instantiate (1 := nlive ge stk nmem_all). 
   intros; eapply nlive_dead_stack; eauto. 
   intros (tm' & C & D). 
   econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto. 
   erewrite stacksize_translated by eauto. eexact C.
-  constructor; eauto with na. eapply magree_extends; eauto. apply nlive_all.
+  constructor; eauto 2 with na. eapply magree_extends; eauto. apply nlive_all.
 
 - (* builtin *)
   TransfInstr; UseTransfer. revert ENV MEM TI. 
   functional induction (transfer_builtin (vanalyze rm f)#pc ef args res ne nm);
   simpl in *; intros.
 + (* volatile load *)
-  assert (LD: Val.lessdef rs#a1 te#a1) by eauto with na.
+  assert (LD: Val.lessdef rs#a1 te#a1) by eauto 2 with na.
   inv H0. rewrite <- H1 in LD; inv LD.
   assert (X: exists tv, volatile_load ge chunk tm b ofs t tv /\ Val.lessdef v tv).
   {
@@ -784,7 +794,7 @@ Ltac UseTransfer :=
   simpl. rewrite <- H4. constructor. eauto.   
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. 
 + (* volatile global load *)
   inv H0. 
@@ -804,12 +814,12 @@ Ltac UseTransfer :=
   simpl. econstructor; eauto.   
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. 
 + (* volatile store *)
   exploit transf_volatile_store. eauto. 
-  instantiate (1 := te#a1). eauto with na.
-  instantiate (1 := te#a2). eauto with na. 
+  instantiate (1 := te#a1). eauto 3 with na.
+  instantiate (1 := te#a2). eauto 3 with na. 
   eauto.
   intros (EQ & tm' & A & B). subst v. 
   econstructor; split.
@@ -817,11 +827,11 @@ Ltac UseTransfer :=
   eapply external_call_symbols_preserved. simpl; eauto. 
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
 + (* volatile global store *)
   rewrite volatile_store_global_charact in H0. destruct H0 as (b & P & Q).
   exploit transf_volatile_store. eauto. eauto. 
-  instantiate (1 := te#a1). eauto with na. 
+  instantiate (1 := te#a1). eauto 2 with na. 
   eauto.
   intros (EQ & tm' & A & B). subst v. 
   econstructor; split.
@@ -830,7 +840,7 @@ Ltac UseTransfer :=
   rewrite volatile_store_global_charact. exists b; split; eauto. 
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
 + (* memcpy *)
   rewrite e1 in TI.
   inv H0. 
@@ -854,15 +864,15 @@ Ltac UseTransfer :=
   rewrite nat_of_Z_eq in H10 by omega. auto.
   eauto. 
   intros (tm' & A & B).
-  assert (LD1: Val.lessdef rs#src te#src) by eauto with na. rewrite <- H2 in LD1.
-  assert (LD2: Val.lessdef rs#dst te#dst) by eauto with na. rewrite <- H1 in LD2.
+  assert (LD1: Val.lessdef rs#src te#src) by eauto 3 with na. rewrite <- H2 in LD1.
+  assert (LD2: Val.lessdef rs#dst te#dst) by eauto 3 with na. rewrite <- H1 in LD2.
   econstructor; split.
   eapply exec_Ibuiltin; eauto.
   eapply external_call_symbols_preserved. simpl.
   inv LD1. inv LD2. econstructor; eauto.  
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
 + (* memcpy eliminated *)
   rewrite e1 in TI. inv H0.
   set (adst := aaddr (vanalyze rm f) # pc dst) in *.
@@ -882,26 +892,26 @@ Ltac UseTransfer :=
   econstructor; split. 
   eapply exec_Ibuiltin; eauto. 
   eapply external_call_symbols_preserved. simpl; constructor. 
-  eapply eventval_list_match_lessdef; eauto with na.
+  eapply eventval_list_match_lessdef; eauto 2 with na.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 2 with na.
 + (* annot val *)  
   inv H0. destruct _x; inv H1. destruct _x; inv H4.
   econstructor; split. 
   eapply exec_Ibuiltin; eauto. 
   eapply external_call_symbols_preserved. simpl; constructor. 
-  eapply eventval_match_lessdef; eauto with na.
+  eapply eventval_match_lessdef; eauto 2 with na.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
 + (* all other builtins *)
   assert ((fn_code tf)!pc = Some(Ibuiltin _x _x0 res pc')).
   {
     destruct _x; auto. destruct _x0; auto. destruct _x0; auto. destruct _x0; auto. contradiction. 
   }
   clear y TI. 
-  exploit external_call_mem_extends; eauto with na. 
+  exploit external_call_mem_extends; eauto 2 with na. 
   eapply magree_extends; eauto. intros. apply nlive_all. 
   intros (v' & tm' & A & B & C & D & E). 
   econstructor; split.
@@ -909,7 +919,7 @@ Ltac UseTransfer :=
   eapply external_call_symbols_preserved. eauto.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto with na.
+  apply eagree_update; eauto 3 with na.
   eapply mextends_agree; eauto. 
 
 - (* conditional *)
@@ -917,16 +927,16 @@ Ltac UseTransfer :=
   econstructor; split.
   eapply exec_Icond; eauto. 
   eapply needs_of_condition_sound. eapply ma_perm; eauto. eauto. eauto with na. 
-  eapply match_succ_states; eauto with na. 
+  eapply match_succ_states; eauto 2 with na. 
   simpl; destruct b; auto. 
 
 - (* jumptable *)
   TransfInstr; UseTransfer.
-  assert (LD: Val.lessdef rs#arg te#arg) by eauto with na. 
+  assert (LD: Val.lessdef rs#arg te#arg) by eauto 2 with na. 
   rewrite H0 in LD. inv LD. 
   econstructor; split.
   eapply exec_Ijumptable; eauto. 
-  eapply match_succ_states; eauto with na. 
+  eapply match_succ_states; eauto 2 with na. 
   simpl. eapply list_nth_z_in; eauto. 
 
 - (* return *)
@@ -938,7 +948,7 @@ Ltac UseTransfer :=
   eapply exec_Ireturn; eauto. 
   erewrite stacksize_translated by eauto. eexact A. 
   constructor; auto.
-  destruct or; simpl; eauto with na.
+  destruct or; simpl; eauto 2 with na.
   eapply magree_extends; eauto. apply nlive_all.
 
 - (* internal function *)
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 568c80e..99d70a8 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -82,19 +82,28 @@ Qed.
 
 Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
 
-Definition vagree_list (vl1 vl2: list val) (nv: nval) : Prop :=
-  list_forall2 (fun v1 v2 => vagree v1 v2 nv) vl1 vl2.
+Inductive vagree_list: list val -> list val -> list nval -> Prop :=
+  | vagree_list_nil: forall nvl,
+      vagree_list nil nil nvl
+  | vagree_list_default: forall v1 vl1 v2 vl2,
+      vagree v1 v2 All -> vagree_list vl1 vl2 nil ->
+      vagree_list (v1 :: vl1) (v2 :: vl2) nil
+  | vagree_list_cons: forall v1 vl1 v2 vl2 nv1 nvl,
+      vagree v1 v2 nv1 -> vagree_list vl1 vl2 nvl ->
+      vagree_list (v1 :: vl1) (v2 :: vl2) (nv1 :: nvl).
 
 Lemma lessdef_vagree_list:
-  forall vl1 vl2, vagree_list vl1 vl2 All -> Val.lessdef_list vl1 vl2.
+  forall vl1 vl2, vagree_list vl1 vl2 nil -> Val.lessdef_list vl1 vl2.
 Proof.
-  induction 1; constructor; auto with na.
+  induction vl1; intros; inv H; constructor; auto with na.
 Qed.
 
 Lemma vagree_lessdef_list:
-  forall x vl1 vl2, Val.lessdef_list vl1 vl2 -> vagree_list vl1 vl2 x.
+  forall vl1 vl2, Val.lessdef_list vl1 vl2 -> forall nvl, vagree_list vl1 vl2 nvl.
 Proof.
-  induction 1; constructor; auto with na.
+  induction 1; intros.
+  constructor.
+  destruct nvl; constructor; auto with na.
 Qed.
 
 Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
@@ -621,14 +630,6 @@ Proof.
   destruct nv; simpl; auto. f_equal; apply complete_mask_idem.
 Qed.
 
-Lemma add_sound_2:
-  forall v1 w1 v2 w2 x,
-  vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
-  vagree (Val.add v1 v2) (Val.add w1 w2) (modarith x).
-Proof.
-  intros. apply add_sound; rewrite modarith_idem; auto.
-Qed.
-
 Lemma mul_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
@@ -641,14 +642,6 @@ Proof.
 - inv H; auto. inv H0; auto. destruct w1; auto. 
 Qed.
 
-Lemma mul_sound_2:
-  forall v1 w1 v2 w2 x,
-  vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
-  vagree (Val.mul v1 v2) (Val.mul w1 w2) (modarith x).
-Proof.
-  intros. apply mul_sound; rewrite modarith_idem; auto.
-Qed.
-
 (** Conversions: zero extension, sign extension, single-of-float *)
 
 Definition zero_ext (n: Z) (x: nval) :=
@@ -880,7 +873,7 @@ Qed.
 Lemma default_needs_of_condition_sound:
   forall cond args1 b args2,
   eval_condition cond args1 m1 = Some b ->
-  vagree_list args1 args2 All ->
+  vagree_list args1 args2 nil ->
   eval_condition cond args2 m2 = Some b.
 Proof.
   intros. apply eval_condition_inj with (f := inject_id) (m1 := m1) (vl1 := args1); auto.
@@ -890,7 +883,9 @@ Qed.
 Lemma default_needs_of_operation_sound:
   forall op args1 v1 args2 nv,
   eval_operation ge (Vptr sp Int.zero) op args1 m1 = Some v1 ->
-  vagree_list args1 args2 (default nv) ->
+  vagree_list args1 args2 nil 
+  \/ vagree_list args1 args2 (default nv :: nil)
+  \/ vagree_list args1 args2 (default nv :: default nv :: nil) ->
   nv <> Nothing ->
   exists v2,
      eval_operation ge (Vptr sp Int.zero) op args2 m2 = Some v2
@@ -898,11 +893,17 @@ Lemma default_needs_of_operation_sound:
 Proof.
   intros. assert (default nv = All) by (destruct nv; simpl; congruence). 
   rewrite H2 in H0.
+  assert (Val.lessdef_list args1 args2).
+  {
+    destruct H0. auto with na. 
+    destruct H0. inv H0; constructor; auto with na. 
+    inv H0; constructor; auto with na. inv H8; constructor; auto with na.
+  }
   exploit (@eval_operation_inj _ _ ge inject_id).
   intros. apply val_inject_lessdef. auto.
   eassumption. auto. auto. auto.
   apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto.
-  apply val_list_inject_lessdef. apply lessdef_vagree_list. eauto.
+  apply val_list_inject_lessdef. eauto.
   eauto. 
   intros (v2 & A & B). exists v2; split; auto.
   apply vagree_lessdef. apply val_inject_lessdef. auto. 
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 0709f5d..f580438 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 5d0e3ae..f11cd52 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
 Require Import Coqlib.
 Require Import Zwf.
 Require Import Maps.