From 173e6c25b2937d6e6941973aa7b116e1d6405513 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 10:10:34 +0100 Subject: Porting the BTL non-trap loads approach to RTL --- backend/Tailcallproof.v | 73 +++++++++++++++++++------------------------------ 1 file changed, 28 insertions(+), 45 deletions(-) (limited to 'backend/Tailcallproof.v') diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 39fc10fb..c8107ad6 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -427,51 +427,34 @@ Proof. - (* load *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. - exploit eval_addressing_lessdef; eauto. - intros [a' [ADDR' ALD]]. - exploit Mem.loadv_extends; eauto. - intros [v' [LOAD' VLD]]. - left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split. - eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. - apply eval_addressing_preserved. exact symbols_preserved. eauto. - econstructor; eauto. apply set_reg_lessdef; auto. - -- (* load notrap1 *) - TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. - left. - exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. - eapply exec_Iload_notrap1. - eassumption. - eapply eval_addressing_lessdef_none. eassumption. - erewrite eval_addressing_preserved. - eassumption. exact symbols_preserved. - - econstructor; eauto. apply set_reg_lessdef; auto. - -- (* load notrap2 *) - TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. - left. - - exploit eval_addressing_lessdef; eauto. - intros [a' [ADDR' ALD]]. - - destruct (Mem.loadv chunk m' a') eqn:Echunk2. - + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v) m'); split. - eapply exec_Iload with (a:=a'). eassumption. - erewrite eval_addressing_preserved. - eassumption. - exact symbols_preserved. - assumption. - econstructor; eauto. apply set_reg_lessdef; auto. - + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. - eapply exec_Iload_notrap2. eassumption. - erewrite eval_addressing_preserved. - eassumption. - exact symbols_preserved. - assumption. - econstructor; eauto. apply set_reg_lessdef; auto. + inv H0. + + exploit eval_addressing_lessdef; eauto. + intros [a' [EVAL' ALD]]. + exploit Mem.loadv_extends; eauto. + intros [v' [LOAD' VLD]]. + left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split. + * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + rewrite <- EVAL'. apply eval_addressing_preserved. exact symbols_preserved. + * econstructor; eauto. apply set_reg_lessdef; auto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * left. exploit eval_addressing_lessdef; eauto. + intros [a' [EVAL' ALD]]. specialize (LOAD v). + destruct (Mem.loadv chunk m' a') eqn:Echunk2. + -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v0) m'); split. + ++ eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + erewrite eval_addressing_preserved; eauto. exact symbols_preserved. + ++ econstructor; eauto. apply set_reg_lessdef; auto. + -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. + ++ eapply exec_Iload; eauto. eapply has_loaded_default; intuition. + erewrite (eval_addressing_preserved ge tge) in H2; [ idtac | exact symbols_preserved]. + rewrite EVAL' in H2; inv H2. assumption. + ++ econstructor; eauto. apply set_reg_lessdef; auto. + * left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. + -- eapply exec_Iload; eauto. apply has_loaded_default; auto; intros. + eapply eval_addressing_lessdef_none in EVAL; eauto. + erewrite (eval_addressing_preserved ge tge) in H0; [ idtac | exact symbols_preserved]. + congruence. + -- econstructor; eauto. apply set_reg_lessdef; auto. - (* store *) TransfInstr. -- cgit