diff options
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 225 |
1 files changed, 108 insertions, 117 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 556b44b3..72b52375 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1098,135 +1098,126 @@ Proof. destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). - destruct trap. - - (* TRAP *) - { - destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. -+ (* replaced by move *) - exploit find_rhs_sound; eauto. intros (v' & EV & LD). - assert (v' = v) by (inv EV; congruence). subst v'. - econstructor; split. - eapply exec_Iop; eauto. simpl; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_load_holds; eauto. - apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. -+ (* load is preserved, but addressing is possibly simplified *) - destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. - assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). - { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. - intros; eapply combine_addr_sound; eauto. } - exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. - intros [a' [A B]]. - assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a'). - { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. } - exploit Mem.loadv_extends; eauto. - intros [v' [X Y]]. - econstructor; split. - eapply exec_Iload; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_load_holds; eauto. - apply set_reg_lessdef; auto. - } - - (* NOTRAP *) - { - assert (exists a' : val, - eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') - as Haa'. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Haa' as [a' [Ha'1 Ha'2]]. - - assert ( - exists v' : val, - Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by - (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption). - destruct Hload' as [v' [Hv'1 Hv'2]]. - - econstructor. split. - eapply exec_Iload; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). - - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; eauto. - unfold transfer. rewrite H. - exists valu1. - apply set_unknown_holds. - assumption. - apply set_reg_lessdef; assumption. - } - -- (* Iload notrap 1*) - destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - destruct SAT as [valu1 NH1]. - exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). - - econstructor. split. - eapply exec_Iload_notrap1; eauto. - rewrite eval_addressing_preserved with (ge1 := ge). - apply eval_addressing_lessdef_none with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - exact symbols_preserved. - - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; eauto. - unfold transfer. rewrite H. - exists valu1. - apply set_unknown_holds. - assumption. - apply set_reg_lessdef. - constructor. assumption. - -- (* Iload notrap 2*) - destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - destruct SAT as [valu1 NH1]. - exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). - - assert (exists a' : val, - eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') - as Haa'. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Haa' as [a' [Ha'1 Ha'2]]. + destruct trap; inv H0. + + + (* TRAP *) + { destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. + * (* replaced by move *) + exploit find_rhs_sound; eauto. intros (v' & EV & LD). + assert (v' = v) by (inv EV; congruence). subst v'. + econstructor; split. + eapply exec_Iop; eauto. simpl; eauto. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + eapply add_load_holds; eauto. + apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. + * (* load is preserved, but addressing is possibly simplified *) + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. + assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). + { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + intros; eapply combine_addr_sound; eauto. } + exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. + intros [a' [A B]]. + assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a'). + { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. } + exploit Mem.loadv_extends; eauto. + intros [v' [X Y]]. + econstructor; split. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + eapply add_load_holds; eauto. + apply set_reg_lessdef; auto. } + + + (* NOTRAP1 *) + { assert (exists a' : val, + eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') + as Haa'. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Haa' as [a' [Ha'1 Ha'2]]. - destruct (Mem.loadv chunk m' a') eqn:Hload'. + assert ( + exists v' : val, + Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by + (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption). + destruct Hload' as [v' [Hv'1 Hv'2]]. - { econstructor. split. - eapply exec_Iload; eauto. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). - + econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. unfold transfer. rewrite H. exists valu1. apply set_unknown_holds. assumption. - apply set_reg_lessdef; eauto. + apply set_reg_lessdef; assumption. } - { - econstructor. split. - eapply exec_Iload_notrap2; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). - - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; eauto. - unfold transfer. rewrite H. - exists valu1. - apply set_unknown_holds. + + + (* NOTRAP2 *) + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + assert (exists a' : val, + eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef v a') + as Haa'. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. assumption. - apply set_reg_lessdef. - constructor. assumption. - } - + destruct Haa' as [a' [Ha'1 Ha'2]]. + + destruct (Mem.loadv chunk m' a') eqn:Hload'. + + { + econstructor. split. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef; eauto. + } + { + econstructor. split. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + try (intros a EVAL'; + rewrite eval_addressing_preserved with (ge1 := ge) in EVAL'; [| exact symbols_preserved]; + inv Ha'2; rewrite Ha'1 in EVAL'; inv EVAL'; auto). + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. + } + * econstructor. split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1 := ge). + intros a EVAL'. eapply eval_addressing_lessdef_none with (vl1 := rs ## args) in EVAL. + erewrite EVAL in EVAL'. congruence. + apply regs_lessdef_regs; assumption. + exact symbols_preserved. + + -- econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. + - (* Istore *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. |