diff options
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 99 |
1 files changed, 43 insertions, 56 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index eb30732b..647938f3 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -969,66 +969,53 @@ Proof. apply agree_set_reg; auto. - (* load *) - 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]]. - 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. - -- (* 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. + 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]]. - - 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. + 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. |