diff options
Diffstat (limited to 'backend/Deadcodeproof.v')
-rw-r--r-- | backend/Deadcodeproof.v | 85 |
1 files changed, 76 insertions, 9 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 7be12c69..52332a82 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -797,34 +797,101 @@ 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. - rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. - eauto. + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); 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. ++ 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 *) + 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. *) + 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. + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); 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. + } + { + econstructor; split. + 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. + } +* 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 *) + 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. *) + 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. +** 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). + assumption. + exact symbols_preserved. + + econstructor; split. + 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. |