From 5530915001c3e8b395d731480e5a6618a08af7af Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 10:57:22 +0100 Subject: being more archi-independant --- backend/Deadcodeproof.v | 11 ++++------- backend/Duplicateproof.v | 2 +- backend/Inliningproof.v | 4 ++-- backend/ProfilingExploitproof.v | 4 ++-- backend/RTLTunnelingproof.v | 4 ++-- backend/RTLgenproof.v | 4 ++-- backend/Renumberproof.v | 4 ++-- backend/Tailcallproof.v | 8 ++++---- 8 files changed, 19 insertions(+), 22 deletions(-) (limited to 'backend') diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 305e8eeb..be64a1a7 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -822,9 +822,8 @@ Ltac UseTransfer := intros. apply nlive_add with bc i; assumption. intros (tv & P & Q). econstructor; split. - eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. - eauto. + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + [ rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved | eauto]). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -851,10 +850,8 @@ Ltac UseTransfer := destruct (Mem.loadv chunk tm ta) eqn:Hchunk2. { econstructor; split. - eapply exec_Iload. eauto. eapply has_loaded_normal; eauto. - erewrite eval_addressing_preserved with (ge1 := ge). - assumption. - exact symbols_preserved. + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + erewrite eval_addressing_preserved with (ge1 := ge); [ assumption | exact symbols_preserved]). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index c4270e46..5752f5d2 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -416,7 +416,7 @@ Proof. destruct DUPLIC as (i' & H2 & H3). inv H3. pose symbols_preserved as SYMPRES. inv H0. + eexists; split. - * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. erewrite eval_addressing_preserved; eauto. + * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; erewrite eval_addressing_preserved; eauto). * econstructor; eauto. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). eexists; split. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index a4bf838e..647938f3 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -992,8 +992,8 @@ Proof. 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. eapply has_loaded_normal; eauto. - try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). + ++ 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. diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v index 292acc2a..4308b670 100644 --- a/backend/ProfilingExploitproof.v +++ b/backend/ProfilingExploitproof.v @@ -128,8 +128,8 @@ Proof. (* load *) - inv H0. + econstructor; split. - * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + rewrite <- EVAL; apply eval_addressing_preserved; exact symbols_preserved). * econstructor; eauto. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). econstructor; split. diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 2cef08e2..aa21fc06 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -461,7 +461,7 @@ Proof. left. eexists. split. * eapply exec_Iload. -- exploit instruction_type_preserved; (simpl; eauto)||congruence. - -- eapply has_loaded_normal; eauto. rewrite <- EVAL'. apply eval_addressing_preserved. apply symbols_preserved. + -- try (eapply has_loaded_normal; eauto; rewrite <- EVAL'; apply eval_addressing_preserved; apply symbols_preserved). * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). @@ -473,7 +473,7 @@ Proof. -- left; eexists; split. eapply exec_Iload. ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. - ++ eapply has_loaded_normal; eauto. rewrite <- ADDR. apply eval_addressing_preserved. apply symbols_preserved. + ++ try (eapply has_loaded_normal; eauto; rewrite <- ADDR; apply eval_addressing_preserved; apply symbols_preserved). ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. -- left; eexists; split. eapply exec_Iload. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 59d0a451..2b1349d2 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -586,8 +586,8 @@ Proof. exists (rs1#rd <- v'); exists tm1. (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Iload. eauto. - econstructor; eauto. rewrite <- H3. - apply eval_addressing_preserved. exact symbols_preserved. + econstructor; eauto. try (rewrite <- H3; + apply eval_addressing_preserved; exact symbols_preserved). auto. (* Match-env *) split. eauto with rtlg. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 7c7bc7e3..cd3efe73 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -172,8 +172,8 @@ Proof. (* load *) - inv H0. + econstructor; split. - * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + rewrite <- EVAL; apply eval_addressing_preserved; exact symbols_preserved). * econstructor; eauto. eapply reach_succ; eauto. simpl; auto. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). econstructor; split. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index c8107ad6..4eb0ba23 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -433,16 +433,16 @@ Proof. 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. + * try (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. + ++ try (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. -- cgit