From 54f97d1988f623ba7422e13a504caeb5701ba93c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 11:05:36 +0200 Subject: Refactoring of builtins and annotations in the back-end. Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations. --- backend/Deadcodeproof.v | 294 +++++++++++++++++++++++++++++------------------- 1 file changed, 176 insertions(+), 118 deletions(-) (limited to 'backend/Deadcodeproof.v') diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index b998c631..a45869d7 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -262,6 +262,16 @@ Proof. simpl. eapply ma_nextblock; eauto. Qed. +Lemma magree_valid_access: + forall m1 m2 (P: locset) chunk b ofs p, + magree m1 m2 P -> + Mem.valid_access m1 chunk b ofs p -> + Mem.valid_access m2 chunk b ofs p. +Proof. + intros. destruct H0; split; auto. + red; intros. eapply ma_perm; eauto. +Qed. + (** * Properties of the need environment *) Lemma add_need_all_eagree: @@ -547,33 +557,43 @@ Proof. eapply magree_monotone; eauto. intros; apply B; auto. Qed. -(** Annotation arguments *) +(** Builtin arguments and results *) -Lemma transfer_annot_arg_sound: +Lemma eagree_set_res: + forall e1 e2 v1 v2 res ne, + Val.lessdef v1 v2 -> + eagree e1 e2 (kill_builtin_res res ne) -> + eagree (regmap_setres res v1 e1) (regmap_setres res v2 e2) ne. +Proof. + intros. destruct res; simpl in *; auto. + apply eagree_update; eauto. apply vagree_lessdef; auto. +Qed. + +Lemma transfer_builtin_arg_sound: forall bc e e' sp m m' a v, - eval_annot_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v -> - forall ne1 nm1 ne2 nm2, - transfer_annot_arg (ne1, nm1) a = (ne2, nm2) -> + eval_builtin_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v -> + forall nv ne1 nm1 ne2 nm2, + transfer_builtin_arg nv (ne1, nm1) a = (ne2, nm2) -> eagree e e' ne2 -> magree m m' (nlive ge sp nm2) -> genv_match bc ge -> bc sp = BCstack -> exists v', - eval_annot_arg ge (fun r => e'#r) (Vptr sp Int.zero) m' a v' - /\ Val.lessdef v v' + eval_builtin_arg ge (fun r => e'#r) (Vptr sp Int.zero) m' a v' + /\ vagree v v' nv /\ eagree e e' ne1 /\ magree m m' (nlive ge sp nm1). Proof. induction 1; simpl; intros until nm2; intros TR EA MA GM SPM; inv TR. - exists e'#x; intuition auto. constructor. eauto 2 with na. eauto 2 with na. -- exists (Vint n); intuition auto. constructor. -- exists (Vlong n); intuition auto. constructor. -- exists (Vfloat n); intuition auto. constructor. -- exists (Vsingle n); intuition auto. constructor. +- exists (Vint n); intuition auto. constructor. apply vagree_same. +- exists (Vlong n); intuition auto. constructor. apply vagree_same. +- exists (Vfloat n); intuition auto. constructor. apply vagree_same. +- exists (Vsingle n); intuition auto. constructor. apply vagree_same. - simpl in H. exploit magree_load; eauto. intros. eapply nlive_add; eauto with va. rewrite Int.add_zero_l in H0; auto. intros (v' & A & B). - exists v'; intuition auto. constructor; auto. + exists v'; intuition auto. constructor; auto. apply vagree_lessdef; auto. eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto. - exists (Vptr sp (Int.add Int.zero ofs)); intuition auto with na. constructor. - unfold Senv.symbol_address in H; simpl in H. @@ -583,40 +603,80 @@ Proof. intros (v' & A & B). exists v'; intuition auto. constructor. simpl. unfold Senv.symbol_address; simpl; rewrite FS; auto. + apply vagree_lessdef; auto. eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto. - exists (Senv.symbol_address ge id ofs); intuition auto with na. constructor. -- destruct (transfer_annot_arg (ne1, nm1) hi) as [ne' nm'] eqn:TR. - exploit IHeval_annot_arg2; eauto. intros (vlo' & A & B & C & D). - exploit IHeval_annot_arg1; eauto. intros (vhi' & P & Q & R & S). +- destruct (transfer_builtin_arg All (ne1, nm1) hi) as [ne' nm'] eqn:TR. + exploit IHeval_builtin_arg2; eauto. intros (vlo' & A & B & C & D). + exploit IHeval_builtin_arg1; eauto. intros (vhi' & P & Q & R & S). exists (Val.longofwords vhi' vlo'); intuition auto. constructor; auto. - apply Val.longofwords_lessdef; auto. + apply vagree_lessdef. + apply Val.longofwords_lessdef; apply lessdef_vagree; auto. Qed. -Lemma transfer_annot_args_sound: +Lemma transfer_builtin_args_sound: forall e sp m e' m' bc al vl, - eval_annot_args ge (fun r => e#r) (Vptr sp Int.zero) m al vl -> + eval_builtin_args ge (fun r => e#r) (Vptr sp Int.zero) m al vl -> forall ne1 nm1 ne2 nm2, - List.fold_left transfer_annot_arg al (ne1, nm1) = (ne2, nm2) -> + transfer_builtin_args (ne1, nm1) al = (ne2, nm2) -> eagree e e' ne2 -> magree m m' (nlive ge sp nm2) -> genv_match bc ge -> bc sp = BCstack -> exists vl', - eval_annot_args ge (fun r => e'#r) (Vptr sp Int.zero) m' al vl' + eval_builtin_args ge (fun r => e'#r) (Vptr sp Int.zero) m' al vl' /\ Val.lessdef_list vl vl' /\ eagree e e' ne1 /\ magree m m' (nlive ge sp nm1). Proof. -Local Opaque transfer_annot_arg. +Local Opaque transfer_builtin_arg. induction 1; simpl; intros. - inv H. exists (@nil val); intuition auto. constructor. -- destruct (transfer_annot_arg (ne1, nm1) a1) as [ne' nm'] eqn:TR. +- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR. exploit IHlist_forall2; eauto. intros (vs' & A1 & B1 & C1 & D1). - exploit transfer_annot_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2). + exploit transfer_builtin_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2). exists (v1' :: vs'); intuition auto. constructor; auto. Qed. +Lemma can_eval_builtin_arg: + forall sp e m e' m' P, + magree m m' P -> + forall a v, + eval_builtin_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v -> + exists v', eval_builtin_arg tge (fun r => e'#r) (Vptr sp Int.zero) m' a v'. +Proof. + intros until P; intros MA. + assert (LD: forall chunk addr v, + Mem.loadv chunk m addr = Some v -> + exists v', Mem.loadv chunk m' addr = Some v'). + { + intros. destruct addr; simpl in H; try discriminate. + eapply Mem.valid_access_load. eapply magree_valid_access; eauto. + eapply Mem.load_valid_access; eauto. } + induction 1; try (econstructor; now constructor). +- exploit LD; eauto. intros (v' & A). exists v'; constructor; auto. +- exploit LD; eauto. intros (v' & A). exists v'; constructor. + unfold Senv.symbol_address, Senv.find_symbol. rewrite symbols_preserved. assumption. +- destruct IHeval_builtin_arg1 as (v1' & A1). + destruct IHeval_builtin_arg2 as (v2' & A2). + exists (Val.longofwords v1' v2'); constructor; auto. +Qed. + +Lemma can_eval_builtin_args: + forall sp e m e' m' P, + magree m m' P -> + forall al vl, + eval_builtin_args ge (fun r => e#r) (Vptr sp Int.zero) m al vl -> + exists vl', eval_builtin_args tge (fun r => e'#r) (Vptr sp Int.zero) m' al vl'. +Proof. + induction 2. +- exists (@nil val); constructor. +- exploit can_eval_builtin_arg; eauto. intros (v' & A). + destruct IHlist_forall2 as (vl' & B). + exists (v' :: vl'); constructor; eauto. +Qed. + (** Properties of volatile memory accesses *) Lemma transf_volatile_store: @@ -821,168 +881,166 @@ Ltac UseTransfer := 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 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). + inv H0. inv H6. rename b1 into v1. + destruct (transfer_builtin_arg All + (kill_builtin_res res ne, + nmem_add nm (aaddr_arg (vanalyze rm f) # pc a1) + (size_chunk chunk)) a1) as (ne1, nm1) eqn: TR. + inversion SS; subst. exploit transfer_builtin_arg_sound; eauto. + intros (tv1 & A & B & C & D). + inv H1. simpl in B. inv B. + assert (X: exists tvres, volatile_load ge chunk tm b ofs t tvres /\ Val.lessdef vres tvres). { inv H2. - * exists (Val.load_result chunk v0); split; auto. constructor; auto. + * exists (Val.load_result chunk v); split; auto. constructor; auto. * exploit magree_load; eauto. - exploit aaddr_sound; eauto. intros (bc & A & B & C). + exploit aaddr_arg_sound_1; eauto. rewrite <- AN. intros. intros. eapply nlive_add; eassumption. intros (tv & P & Q). exists tv; split; auto. constructor; auto. } - destruct X as (tv & A & B). + destruct X as (tvres & P & Q). econstructor; split. eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. + constructor. eauto. constructor. eapply external_call_symbols_preserved. - simpl. rewrite <- H4. constructor. eauto. + constructor. simpl. eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. - eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. -+ (* volatile global load *) - inv H0. - assert (X: exists tv, volatile_load ge chunk tm b ofs t tv /\ Val.lessdef v tv). - { - inv H2. - * exists (Val.load_result chunk v0); split; auto. constructor; auto. - * exploit magree_load; eauto. - inv SS. intros. eapply nlive_add; eauto. constructor. apply GE. auto. - intros (tv & P & Q). - exists tv; split; auto. constructor; auto. - } - destruct X as (tv & A & B). - econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved. - simpl. econstructor; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. + apply eagree_set_res; auto. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. + (* volatile store *) - exploit transf_volatile_store. eauto. - instantiate (1 := te#a1). eauto 3 with na. - instantiate (1 := te#a2). eauto 3 with na. - eauto. - intros (EQ & tm' & A & B). subst v. + inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. + destruct (transfer_builtin_arg (store_argument chunk) + (kill_builtin_res res ne, nm) a2) as (ne2, nm2) eqn: TR2. + destruct (transfer_builtin_arg All (ne2, nm2) a1) as (ne1, nm1) eqn: TR1. + inversion SS; subst. + exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto. + intros (tv1 & A1 & B1 & C1 & D1). + exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto. + intros (tv2 & A2 & B2 & C2 & D2). + exploit transf_volatile_store; eauto. + intros (EQ & tm' & P & Q). subst vres. econstructor; split. eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. + constructor. eauto. constructor. eauto. constructor. eapply external_call_symbols_preserved. simpl; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - 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 2 with na. - eauto. - intros (EQ & tm' & A & B). subst v. - econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved. simpl. - rewrite volatile_store_global_charact. exists b; split; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. + apply eagree_set_res; auto. + (* memcpy *) rewrite e1 in TI. - inv H0. - set (adst := aaddr (vanalyze rm f) # pc dst) in *. - set (asrc := aaddr (vanalyze rm f) # pc src) in *. - exploit magree_loadbytes. eauto. eauto. - exploit aaddr_sound. eauto. symmetry; eexact H2. - intros (bc & A & B & C). - intros. eapply nlive_add; eassumption. + inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. + set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *. + set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *. + destruct (transfer_builtin_arg All + (kill_builtin_res res ne, + nmem_add (nmem_remove nm adst sz) asrc sz) dst) + as (ne2, nm2) eqn: TR2. + destruct (transfer_builtin_arg All (ne2, nm2) src) as (ne1, nm1) eqn: TR1. + inversion SS; subst. + exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto. + intros (tv1 & A1 & B1 & C1 & D1). + exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto. + intros (tv2 & A2 & B2 & C2 & D2). + inv H1. + exploit magree_loadbytes. eauto. eauto. + intros. eapply nlive_add; eauto. + unfold asrc, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto. intros (tbytes & P & Q). exploit magree_storebytes_parallel. - eapply magree_monotone. eexact MEM. + eapply magree_monotone. eexact D2. instantiate (1 := nlive ge sp0 (nmem_remove nm adst sz)). intros. apply incl_nmem_add; auto. eauto. - instantiate (1 := nlive ge sp0 nm). - exploit aaddr_sound. eauto. symmetry; eexact H1. - intros (bc & A & B & C). - intros. eapply nlive_remove; eauto. - erewrite Mem.loadbytes_length in H10 by eauto. - rewrite nat_of_Z_eq in H10 by omega. auto. + instantiate (1 := nlive ge sp0 nm). + intros. eapply nlive_remove; eauto. + unfold adst, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto. + erewrite Mem.loadbytes_length in H1 by eauto. + rewrite nat_of_Z_eq in H1 by omega. auto. eauto. intros (tm' & A & B). - 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. + apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. + constructor. eauto. constructor. eauto. constructor. eapply external_call_symbols_preserved. simpl. - inv LD1. inv LD2. econstructor; eauto. + simpl in B1; inv B1. simpl in B2; inv B2. econstructor; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 3 with na. + apply eagree_set_res; auto. + (* memcpy eliminated *) - rewrite e1 in TI. inv H0. - set (adst := aaddr (vanalyze rm f) # pc dst) in *. - set (asrc := aaddr (vanalyze rm f) # pc src) in *. + rewrite e1 in TI. + inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. + set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *. + set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *. + inv H1. econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. - apply eagree_set_undef; auto. + destruct res; auto. apply eagree_set_undef; auto. eapply magree_storebytes_left; eauto. - exploit aaddr_sound. eauto. symmetry; eexact H1. + exploit aaddr_arg_sound. eauto. eauto. intros (bc & A & B & C). intros. eapply nlive_contains; eauto. erewrite Mem.loadbytes_length in H0 by eauto. rewrite nat_of_Z_eq in H0 by omega. auto. + (* annot *) - inv H0. + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + inversion SS; subst. + exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). + inv H1. econstructor; split. - eapply exec_Ibuiltin; eauto. + eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_list_match_lessdef; eauto 2 with na. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. -+ (* annot val *) - inv H0. destruct _x; inv H1. destruct _x; inv H4. + apply eagree_set_res; auto. ++ (* annot val *) + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + inversion SS; subst. + exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). + inv H1. inv B. inv H6. econstructor; split. eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_match_lessdef; eauto 2 with na. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 3 with na. + apply eagree_set_res; auto. ++ (* debug *) + inv H1. + exploit can_eval_builtin_args; eauto. intros (vargs' & A). + econstructor; split. + eapply exec_Ibuiltin; eauto. constructor. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_set_res; auto. + (* 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. + clear y TI. + destruct (transfer_builtin_args (kill_builtin_res res ne, nmem_all) _x0) as (ne1, nm1) eqn:TR. + inversion SS; subst. + exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). 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). + intros (v' & tm' & P & Q & R & S & T). econstructor; split. - eapply exec_Ibuiltin; eauto. + eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved. eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 3 with na. + apply eagree_set_res; auto. eapply mextends_agree; eauto. -- (* annot *) - TransfInstr; UseTransfer. - destruct (fold_left transfer_annot_arg args (ne, nm)) as [ne1 nm1] eqn:TR; simpl in *. - inv SS. exploit transfer_annot_args_sound; eauto. intros (vargs' & A & B & C & D). - assert (EC: m' = m /\ external_call ef ge vargs' tm t Vundef tm). - { destruct ef; try contradiction. inv H2. split; auto. simpl. constructor. - eapply eventval_list_match_lessdef; eauto. } - destruct EC as [EC1 EC2]; subst m'. - econstructor; split. - eapply exec_Iannot. eauto. auto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved with (ge1 := ge); eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_succ_states; eauto. simpl; auto. - - (* conditional *) TransfInstr; UseTransfer. econstructor; split. -- cgit