diff options
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 65 |
1 files changed, 53 insertions, 12 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 0434a4a4..647938f3 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 -> @@ -960,22 +969,54 @@ Proof. apply agree_set_reg; auto. - (* load *) - exploit tr_funbody_inv; eauto. intros TR; inv TR. - exploit eval_addressing_inject. + exploit tr_funbody_inv; eauto. intros TR; inv TR. inv H0. + + 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]]. - exploit Mem.loadv_inject; eauto. intros [v' [U V]]. - assert (eval_addressing tge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). - rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. - left; econstructor; split. - eapply plus_one. eapply exec_Iload; eauto. - econstructor; eauto. - apply match_stacks_inside_set_reg; auto. - apply agree_set_reg; auto. - + fold (saddr ctx addr). intros [a' [P Q]]. + exploit Mem.loadv_inject; eauto. intros [v' [U V]]. + assert (eval_addressing tge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). + { rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. } + left; econstructor; split. + * eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + * econstructor; eauto. apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + + destruct (eval_addressing) eqn:ADDR in LOAD. + * 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. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + 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; eauto. eapply has_loaded_default; eauto. + try (intros a ADDR'; erewrite eval_addressing_preserved in ADDR'; [ rewrite P in ADDR' | + exact symbols_preserved ]; inv ADDR'; assumption). + ++ econstructor; eauto. apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + * left; econstructor; split. + -- eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros. rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge) in H0. + 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. + intros. apply eval_addressing_none in H1. congruence. + 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. |