From 29e0c9b2c99a437fc9dfab66e1abdd546a5308d6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Jan 2014 15:59:11 +0000 Subject: 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 --- backend/Deadcode.v | 53 +++++++++------ backend/Deadcodeproof.v | 176 +++++++++++++++++++++++++----------------------- backend/NeedDomain.v | 51 +++++++------- backend/ValueAnalysis.v | 12 ++++ backend/ValueDomain.v | 12 ++++ 5 files changed, 176 insertions(+), 128 deletions(-) (limited to 'backend') 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. -- cgit v1.2.3