From 71c58a8d494eafd847776446b0c246229b2bc9cf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Sep 2019 18:30:25 +0200 Subject: avancement (il faut utiliser Vundef visiblement) --- backend/Tailcallproof.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'backend/Tailcallproof.v') diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 06e314f3..4a5e83a1 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -438,6 +438,19 @@ Proof. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply set_reg_lessdef; auto. + (* TODO *) +- (* load notrap1 *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. + + 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. + - (* store *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. -- cgit From 5710342ba44a451639a6c28aeb61d0fc24d7ee58 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Sep 2019 20:23:29 +0200 Subject: progress on non trapping loads --- backend/Tailcallproof.v | 40 ++++++++++++++++++++++++++++++++-------- 1 file changed, 32 insertions(+), 8 deletions(-) (limited to 'backend/Tailcallproof.v') diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 4a5e83a1..5cb1b980 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -438,19 +438,43 @@ Proof. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply set_reg_lessdef; auto. - (* TODO *) - (* load notrap1 *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. - - 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. + left. + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) 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 <- (default_notrap_load_value chunk)) m'); split. + eapply exec_Iload_notrap2. eassumption. + erewrite eval_addressing_preserved. + eassumption. + exact symbols_preserved. + assumption. + econstructor; eauto. apply set_reg_lessdef; auto. + - (* store *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. -- cgit