diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-09 14:51:52 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-09 14:51:52 +0100 |
commit | 37de1399449067121a8bb9a51a7cc7a043ad17e2 (patch) | |
tree | 11429171ae1f49b57f8d7f98a09d5ea0511680c0 /backend/Inliningproof.v | |
parent | dd1c78c840bf5eb1ad7e101f2da05578245c5998 (diff) | |
parent | e2c64b54bf5df0927c684a70167378c91cba0ff4 (diff) | |
download | compcert-kvx-37de1399449067121a8bb9a51a7cc7a043ad17e2.tar.gz compcert-kvx-37de1399449067121a8bb9a51a7cc7a043ad17e2.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge
Diffstat (limited to 'backend/Inliningproof.v')
-rw-r--r-- | backend/Inliningproof.v | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index cc84b1cc..c4efaf18 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -929,6 +929,15 @@ Proof. intros. inv H. eauto. Qed. +Lemma eval_addressing_none: + forall sp' ctx addr rs, + eval_addressing ge (Vptr sp' (Ptrofs.repr (dstk ctx))) addr rs = None -> + eval_addressing ge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs = None. +Proof. + intros until rs; intro Heval. + destruct addr; destruct rs as [| r0 rs1]; simpl in *; trivial; discriminate. +Qed. + Theorem step_simulation: forall S1 t S2, step ge S1 t S2 -> @@ -976,6 +985,51 @@ Proof. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. +- (* load notrap1 *) + exploit tr_funbody_inv; eauto. intros TR; inv TR. + left; econstructor; split. + eapply plus_one. eapply exec_Iload_notrap1. eassumption. + rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge). + exploit eval_addressing_inj_none. + 4: eassumption. + intros. eapply symbol_address_inject. + eapply match_stacks_inside_globals; eauto. + eauto. + instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. + rewrite Ptrofs.add_zero_l. + apply eval_addressing_none. + exact symbols_preserved. + econstructor; eauto. + apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + +- (* load notrap2 *) + exploit tr_funbody_inv; eauto. intros TR; inv TR. + + exploit eval_addressing_inject. + eapply match_stacks_inside_globals; eauto. + eexact SP. + instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. + eauto. + fold (saddr ctx addr). intros [a' [P Q]]. + + destruct (Mem.loadv chunk m' a') eqn:Hload'. + + left; econstructor; split. + eapply plus_one. + eapply exec_Iload; eauto. + try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). + econstructor; eauto. + apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + + + left; econstructor; split. + eapply plus_one. + eapply exec_Iload_notrap2; eauto. + try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). + econstructor; eauto. + apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + - (* store *) exploit tr_funbody_inv; eauto. intros TR; inv TR. exploit eval_addressing_inject. |