From 884756b623fd6031a04102a545d92e4ec905f1cc Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 6 May 2013 15:25:26 +0000 Subject: Revised semantics and compilation of 2-argument C operators to better match "the usual binary conversions" and be more robust towards future extensions e.g. with 32-bit float values. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index de3b8df..953e690 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -377,21 +377,19 @@ Lemma make_binarith_correct: (sem_binarith sem_int sem_long sem_float). Proof. red; unfold make_binarith, sem_binarith; - intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_binarith tya tyb); inv MAKE; - destruct va; try discriminate; destruct vb; try discriminate. + intros until m; intros SEM MAKE EV1 EV2. + set (cls := classify_binarith tya tyb) in *. + set (ty := binarith_type cls) in *. + monadInv MAKE. + destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. + exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. + destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. -- erewrite <- fop_ok in SEM; eauto with cshm. -- erewrite <- fop_ok in SEM; eauto with cshm. -- erewrite <- fop_ok in SEM; eauto with cshm. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s2; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s1; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- erewrite <- fop_ok in SEM; eauto with cshm. - erewrite <- fop_ok in SEM; eauto with cshm. Qed. @@ -401,17 +399,19 @@ Lemma make_binarith_int_correct: (sem_binarith sem_int sem_long (fun x y => None)). Proof. red; unfold make_binarith_int, sem_binarith; - intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_binarith tya tyb); inv MAKE; - destruct va; try discriminate; destruct vb; try discriminate. + intros until m; intros SEM MAKE EV1 EV2. + set (cls := classify_binarith tya tyb) in *. + set (ty := binarith_type cls) in *. + monadInv MAKE. + destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. + exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. + destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s2; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s1; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. Qed. End MAKE_BIN. -- cgit v1.2.3