diff options
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 151 |
1 files changed, 75 insertions, 76 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b59ee8b4..749add67 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -402,90 +402,89 @@ Proof. - (* Iload *) rename pc'0 into pc. TransfInstr. - set (aa := eval_static_addressing addr (aregs ae args)). - assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va). - set (av := loadv chunk (romem_for cu) am aa). - assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto). - destruct trap. - { - destruct (const_for_result av) as [cop|] eqn:?; intros. -+ (* constant-propagated *) - exploit const_for_result_correct; eauto. intros (v' & A & B). - left; econstructor; econstructor; split. - eapply exec_Iop; eauto. - eapply match_states_succ; eauto. - apply set_reg_lessdef; auto. -+ (* strength-reduced *) - assert (ADDR: - let (addr', args') := addr_strength_reduction addr args (aregs ae args) in - exists a', - eval_addressing ge (Vptr sp0 Ptrofs.zero) addr' rs ## args' = Some a' /\ - Val.lessdef a a'). - { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. } - destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args']. - destruct ADDR as (a' & P & Q). - exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P. - intros (a'' & U & V). - assert (W: eval_addressing tge (Vptr sp0 Ptrofs.zero) addr' rs'##args' = Some a''). - { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. } - exploit Mem.loadv_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto. - intros (v' & X & Y). - left; econstructor; econstructor; split. - eapply exec_Iload; eauto. - eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - } - { - assert (exists v2 : val, - eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Hexist2 as [v2 [Heval2 Hlessdef2]]. - destruct (Mem.loadv_extends chunk m m' a v2 v MEM H1 Hlessdef2) as [vX [Hvx1 Hvx2]]. - left; econstructor; econstructor; split. - eapply exec_Iload with (a := v2); eauto. - try (erewrite eval_addressing_preserved with (ge1:=ge); auto; - exact symbols_preserved). - eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - - } - -- (* Iload notrap1 *) - rename pc'0 into pc. TransfInstr. - assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = None). - rewrite eval_addressing_preserved with (ge1 := ge); eauto. - apply eval_addressing_lessdef_none with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - exact symbols_preserved. - - left; econstructor; econstructor; split. - eapply exec_Iload_notrap1; eauto. - eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - -- (* Iload notrap2 *) - rename pc'0 into pc. TransfInstr. - assert (exists v2 : val, - eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Hexist2 as [a' [Heval' Hlessdef']]. - destruct (Mem.loadv chunk m' a') eqn:Hload'. + inv H0. + + set (aa := eval_static_addressing addr (aregs ae args)). + assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va). + set (av := loadv chunk (romem_for cu) am aa). + assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto). + destruct trap. { + destruct (const_for_result av) as [cop|] eqn:?; intros. + * (* constant-propagated *) + exploit const_for_result_correct; eauto. intros (v' & A & B). + left; econstructor; econstructor; split. + eapply exec_Iop; eauto. + eapply match_states_succ; eauto. + apply set_reg_lessdef; auto. + * (* strength-reduced *) + assert (ADDR: + let (addr', args') := addr_strength_reduction addr args (aregs ae args) in + exists a', + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr' rs ## args' = Some a' /\ + Val.lessdef a a'). + { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. } + destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args']. + destruct ADDR as (a' & P & Q). + exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P. + intros (a'' & U & V). + assert (W: eval_addressing tge (Vptr sp0 Ptrofs.zero) addr' rs'##args' = Some a''). + { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. } + exploit Mem.loadv_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto. + intros (v' & X & Y). left; econstructor; econstructor; split. - eapply exec_Iload; eauto. - - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. eapply match_states_succ; eauto. apply set_reg_lessdef; auto. } { + assert (exists v2 : val, + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Hexist2 as [v2 [Heval2 Hlessdef2]]. + destruct (Mem.loadv_extends chunk m m' a v2 v MEM LOAD Hlessdef2) as [vX [Hvx1 Hvx2]]. left; econstructor; econstructor; split. - eapply exec_Iload_notrap2; eauto. - - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + try (erewrite eval_addressing_preserved with (ge1:=ge); auto; + exact symbols_preserved). eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + assert (exists v2 : val, + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef v v2) as Hexist2. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Hexist2 as [a' [Heval' Hlessdef']]. + destruct (Mem.loadv chunk m' a') eqn:Hload'. + { + left; econstructor; econstructor; split. + eapply exec_Iload; eauto. + + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply has_loaded_normal; eauto. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + { + left; econstructor; econstructor; split. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + try (intros a; rewrite eval_addressing_preserved with (ge1 := ge); [ intros CONTRA; try congruence | exact symbols_preserved ]). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + * assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = None). + rewrite eval_addressing_preserved with (ge1 := ge); eauto. + apply eval_addressing_lessdef_none with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + exact symbols_preserved. + + left; econstructor; econstructor; split. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros; congruence. + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - (* Istore *) rename pc'0 into pc. TransfInstr. |