From 4297fcb821c3188449b64184af73e41491a6118f Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 23 Jul 2012 15:01:54 +0000 Subject: - Revised non-overflow constraints on memory injections so that injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'powerpc/Asmgenproof.v') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index e7b7385..e99049c 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -827,9 +827,9 @@ Proof. rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. left; eapply exec_straight_steps; eauto with coqlib; destruct chunk; simpl; simpl in H6; - (* all cases but Mint8signed *) + (* all cases but Mint8signed and Mfloat64 *) try (eapply transl_load_correct; eauto; - intros; simpl; unfold preg_of; rewrite H6; auto). + intros; simpl; unfold preg_of; rewrite H6; auto; fail). (* Mint8signed *) exploit loadv_8_signed_unsigned; eauto. intros [v' [LOAD EQ]]. assert (X1: forall (cst : constant) (r1 : ireg) (rs1 : regset), @@ -849,6 +849,10 @@ Proof. eapply agree_set_twice_mireg; eauto. rewrite EQ. apply Val.sign_ext_lessdef. generalize (ireg_val _ _ _ dst AG1 H6). rewrite Regmap.gss. auto. + (* Mfloat64 *) + exploit Mem.loadv_float64al32; eauto. intros. clear H0. + eapply transl_load_correct; eauto; + intros; simpl; unfold preg_of; rewrite H6; auto. Qed. Lemma storev_8_signed_unsigned: @@ -883,6 +887,7 @@ Proof. rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H. left; eapply exec_straight_steps_bis; eauto with coqlib. destruct chunk; simpl; simpl in H6; + try (generalize (Mem.storev_float64al32 _ _ _ _ H0); intros); try (rewrite storev_8_signed_unsigned in H0); try (rewrite storev_16_signed_unsigned in H0); simpl; eapply transl_store_correct; eauto; -- cgit v1.2.3