diff options
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 59 |
1 files changed, 57 insertions, 2 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index a5d08a0f..60663503 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) -> @@ -406,6 +406,8 @@ Proof. 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). @@ -431,6 +433,59 @@ Proof. 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'. + { + left; econstructor; econstructor; split. + eapply exec_Iload; 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_notrap2; eauto. + + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } - (* Istore *) rename pc'0 into pc. TransfInstr. |