diff options
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 116 |
1 files changed, 85 insertions, 31 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index a3592c4d..749add67 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -142,8 +142,8 @@ Inductive match_pc (f: function) (rs: regset) (m: mem): nat -> node -> node -> P f.(fn_code)!pc = Some (Inop s) -> match_pc f rs m n s pcx -> match_pc f rs m (S n) pc pcx - | match_pc_cond: forall n pc cond args s1 s2 pcx, - f.(fn_code)!pc = Some (Icond cond args s1 s2) -> + | match_pc_cond: forall n pc cond args s1 s2 pcx i, + f.(fn_code)!pc = Some (Icond cond args s1 s2 i) -> (forall b, eval_condition cond rs##args m = Some b -> match_pc f rs m n (if b then s1 else s2) pcx) -> @@ -402,35 +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 (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. + 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. 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; 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. |