diff options
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 44 |
1 files changed, 35 insertions, 9 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index 6f1ad67..611a32b 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -37,6 +37,7 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Mint32 => 4 | Mfloat32 => 4 | Mfloat64 => 8 + | Mfloat64al32 => 8 end. Lemma size_chunk_pos: @@ -80,7 +81,10 @@ Definition align_chunk (chunk: memory_chunk) : Z := | Mint8unsigned => 1 | Mint16signed => 2 | Mint16unsigned => 2 - | _ => 4 + | Mint32 => 4 + | Mfloat32 => 4 + | Mfloat64 => 8 + | Mfloat64al32 => 4 end. Lemma align_chunk_pos: @@ -95,12 +99,16 @@ Proof. intros. destruct chunk; simpl; try apply Zdivide_refl. exists 2; auto. Qed. -Lemma align_chunk_compat: +Lemma align_le_divides: forall chunk1 chunk2, - size_chunk chunk1 = size_chunk chunk2 -> align_chunk chunk1 = align_chunk chunk2. + align_chunk chunk1 <= align_chunk chunk2 -> (align_chunk chunk1 | align_chunk chunk2). Proof. - intros chunk1 chunk2. - destruct chunk1; destruct chunk2; simpl; congruence. + intros. destruct chunk1; destruct chunk2; simpl in *; + solve [ omegaContradiction + | apply Zdivide_refl + | exists 2; reflexivity + | exists 4; reflexivity + | exists 8; reflexivity ]. Qed. (** * Memory values *) @@ -331,7 +339,7 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval := | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n)) | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs | Vfloat n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float.bits_of_single n))) - | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n))) + | Vfloat n, (Mfloat64 | Mfloat64al32) => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n))) | _, _ => list_repeat (size_chunk_nat chunk) Undef end. @@ -345,7 +353,7 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := | Mint16unsigned => Vint(Int.zero_ext 16 (Int.repr (decode_int bl))) | Mint32 => Vint(Int.repr(decode_int bl)) | Mfloat32 => Vfloat(Float.single_of_bits (Int.repr (decode_int bl))) - | Mfloat64 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl))) + | Mfloat64 | Mfloat64al32 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl))) end | None => match chunk with @@ -384,13 +392,13 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n) | Vint n, Mint32, Mint32 => v2 = Vint n | Vint n, Mint32, Mfloat32 => v2 = Vfloat(Float.single_of_bits n) - | Vint n, (Mfloat32 | Mfloat64), _ => v2 = Vundef + | Vint n, (Mfloat32 | Mfloat64 | Mfloat64al32), _ => v2 = Vundef | Vint n, _, _ => True (**r nothing meaningful to say about v2 *) | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs | Vptr b ofs, _, _ => v2 = Vundef | Vfloat f, Mfloat32, Mfloat32 => v2 = Vfloat(Float.singleoffloat f) | Vfloat f, Mfloat32, Mint32 => v2 = Vint(Float.bits_of_single f) - | Vfloat f, Mfloat64, Mfloat64 => v2 = Vfloat f + | Vfloat f, (Mfloat64 | Mfloat64al32), (Mfloat64 | Mfloat64al32) => v2 = Vfloat f | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32), _ => v2 = Vundef | Vfloat f, _, _ => True (* nothing interesting to say about v2 *) end. @@ -423,6 +431,9 @@ Opaque inj_pointer. rewrite decode_encode_int_4. auto. rewrite decode_encode_int_4. decEq. apply Float.single_of_bits_of_single. rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. + rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. + rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. + rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. change (proj_bytes (inj_pointer 4 b i)) with (@None (list byte)). simpl. unfold proj_pointer. generalize (check_inj_pointer b i 4%nat). Transparent inj_pointer. @@ -816,3 +827,18 @@ Proof. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. Qed. +(** [memval_inject] and compositions *) + +Lemma memval_inject_compose: + forall f f' v1 v2 v3, + memval_inject f v1 v2 -> memval_inject f' v2 v3 -> + memval_inject (compose_meminj f f') v1 v3. +Proof. + intros. inv H. + inv H0. constructor. + inv H0. econstructor. + unfold compose_meminj; rewrite H1; rewrite H5; eauto. + rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints. + constructor. +Qed. + |