diff options
-rw-r--r-- | backend/Constprop.v | 4 | ||||
-rw-r--r-- | backend/Constpropproof.v | 20 |
2 files changed, 22 insertions, 2 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index cf1a9171..eda41b39 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -181,7 +181,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) let (op', args') := op_strength_reduction op args aargs in Iop op' args' res s' end - | Iload trap chunk addr args dst s => + | Iload TRAP chunk addr args dst s => let aargs := aregs ae args in let a := ValueDomain.loadv chunk rm am (eval_static_addressing addr aargs) in match const_for_result a with @@ -189,7 +189,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) Iop cop nil dst s | None => let (addr', args') := addr_strength_reduction addr args aargs in - Iload trap chunk addr' args' dst s + Iload TRAP chunk addr' args' dst s end | Istore chunk addr args src s => let aargs := aregs ae args in diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index a5d08a0f..eb1faa2d 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -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,7 +433,25 @@ 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. + erewrite eval_addressing_preserved with (ge1:=ge); auto. + exact symbols_preserved. + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + + } +- (* Iload notrap2 *) + (* TODO *) - (* Istore *) rename pc'0 into pc. TransfInstr. assert (ADDR: |