From 132e36fa0be63eb5672eda9168403d3fb74af2fa Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 26 May 2012 07:32:01 +0000 Subject: CSE: add recognition of some combined operators, conditions, and addressing modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Memory.v | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) (limited to 'common/Memory.v') diff --git a/common/Memory.v b/common/Memory.v index 0fc663f..49dcd7b 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -659,7 +659,8 @@ Proof. set (cl := getN (size_chunk_nat Mint8unsigned) ofs m.(mem_contents)#b). destruct (valid_access_dec m Mint8signed b ofs Readable). rewrite pred_dec_true; auto. unfold decode_val. - destruct (proj_bytes cl); auto. rewrite decode_int8_signed_unsigned. auto. + destruct (proj_bytes cl); auto. + simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto. rewrite pred_dec_false; auto. Qed. @@ -672,7 +673,8 @@ Proof. set (cl := getN (size_chunk_nat Mint16unsigned) ofs m.(mem_contents)#b). destruct (valid_access_dec m Mint16signed b ofs Readable). rewrite pred_dec_true; auto. unfold decode_val. - destruct (proj_bytes cl); auto. rewrite decode_int16_signed_unsigned. auto. + destruct (proj_bytes cl); auto. + simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto. rewrite pred_dec_false; auto. Qed. @@ -939,13 +941,20 @@ Proof. apply inj_eq_rev; auto. Qed. +Theorem load_store_similar_2: + forall chunk', + size_chunk chunk' = size_chunk chunk -> + type_of_chunk chunk' = type_of_chunk chunk -> + load chunk' m2 b ofs = Some (Val.load_result chunk' v). +Proof. + intros. destruct (load_store_similar chunk') as [v' [A B]]. auto. + rewrite A. decEq. eapply decode_encode_val_similar with (chunk1 := chunk); eauto. +Qed. + Theorem load_store_same: - Val.has_type v (type_of_chunk chunk) -> load chunk m2 b ofs = Some (Val.load_result chunk v). Proof. - intros. - destruct (load_store_similar chunk) as [v' [A B]]. auto. - rewrite A. decEq. eapply decode_encode_val_similar; eauto. + apply load_store_similar_2; auto. Qed. Theorem load_store_other: @@ -1276,7 +1285,10 @@ Theorem store_float32_truncate: forall m b ofs n, store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) = store Mfloat32 m b ofs (Vfloat n). -Proof. intros. apply store_similar_chunks. simpl. decEq. apply encode_float32_cast. Qed. +Proof. + intros. apply store_similar_chunks. simpl. decEq. + repeat rewrite encode_float32_eq. rewrite Float.bits_of_singleoffloat. auto. +Qed. (** ** Properties related to [storebytes]. *) -- cgit v1.2.3