From 173e6c25b2937d6e6941973aa7b116e1d6405513 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 10:10:34 +0100 Subject: Porting the BTL non-trap loads approach to RTL --- backend/Deadcodeproof.v | 85 +++++++++++++++++++++++-------------------------- 1 file changed, 40 insertions(+), 45 deletions(-) (limited to 'backend/Deadcodeproof.v') diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index be20af0b..305e8eeb 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -797,113 +797,108 @@ Ltac UseTransfer := apply eagree_update; eauto 2 with na. - (* load *) - TransfInstr; UseTransfer. - destruct (is_dead (nreg ne dst)) eqn:DEAD; + TransfInstr; UseTransfer. inv H0. ++ destruct (is_dead (nreg ne dst)) eqn:DEAD; [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; simpl in *. -+ (* dead instruction, turned into a nop *) +* (* dead instruction, turned into a nop *) econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update_dead; auto with na. -+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) +* (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) econstructor; split. eapply exec_Iop with (v := Vint Int.zero); eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; auto. rewrite is_int_zero_sound by auto. destruct v; simpl; auto. apply iagree_zero. -+ (* preserved *) +* (* preserved *) 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. + destruct ta; simpl in EVAL; try discriminate. exploit magree_load; eauto. exploit aaddressing_sound; eauto. intros (bc & A & B & C). 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; eauto. eapply has_loaded_normal; eauto. rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. - -- (* load notrap1 *) - TransfInstr; UseTransfer. ++ destruct (eval_addressing) eqn:EVAL in LOAD. +* specialize (LOAD v). destruct (is_dead (nreg ne dst)) eqn:DEAD; [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; simpl in *. -+ (* dead instruction, turned into a nop *) +** (* dead instruction, turned into a nop *) econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update_dead; auto with na. -+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) +** (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) econstructor; split. eapply exec_Iop with (v := Vint Int.zero); eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; auto. rewrite is_int_zero_sound by auto. constructor. -+ (* preserved *) - exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption. - intro Hnone'. - assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'. +** (* preserved *) + exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. + intros (ta & U & V). + destruct (Mem.loadv chunk tm ta) eqn:Hchunk2. + { + econstructor; split. + eapply exec_Iload. eauto. eapply has_loaded_normal; eauto. erewrite eval_addressing_preserved with (ge1 := ge). assumption. exact symbols_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. + } + { econstructor; split. - eapply exec_Iload_notrap1; eauto. + eapply exec_Iload. eauto. eapply has_loaded_default; eauto. + erewrite eval_addressing_preserved with (ge1 := ge). + intros a EVAL'; rewrite U in EVAL'; inv EVAL'. auto. + exact symbols_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. - -- (* load notrap2 *) - TransfInstr; UseTransfer. - - destruct (is_dead (nreg ne dst)) eqn:DEAD; + } +* destruct (is_dead (nreg ne dst)) eqn:DEAD; [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; simpl in *. -+ (* dead instruction, turned into a nop *) +** (* dead instruction, turned into a nop *) econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update_dead; auto with na. -+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) +** (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) econstructor; split. eapply exec_Iop with (v := Vint Int.zero); eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; auto. rewrite is_int_zero_sound by auto. constructor. -+ (* preserved *) - exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. - intros (ta & U & V). - destruct (Mem.loadv chunk tm ta) eqn:Hchunk2. - { - econstructor; split. - eapply exec_Iload. eauto. +** exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption. + intro Hnone'. + assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'. erewrite eval_addressing_preserved with (ge1 := ge). - eassumption. + assumption. exact symbols_preserved. - eassumption. - eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. - eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. - } - { + econstructor; split. - eapply exec_Iload_notrap2. eauto. - erewrite eval_addressing_preserved with (ge1 := ge). - eassumption. - exact symbols_preserved. - eassumption. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite Hnone2' in EVAL'; inv EVAL'. + eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. - } + - (* store *) TransfInstr; UseTransfer. destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args) -- cgit