- 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

1 files changed, 24 insertions, 1 deletions

diff --git a/common/Values.v b/common/Values.v
index f0b125a..bcb7c4f 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -429,7 +429,7 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
   | Mint32, Vint n => Vint n
   | Mint32, Vptr b ofs => Vptr b ofs
   | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f)
-  | Mfloat64, Vfloat f => Vfloat f
+  | (Mfloat64 | Mfloat64al32), Vfloat f => Vfloat f
   | _, _ => Vundef
   end.
 
@@ -1168,3 +1168,26 @@ Proof.
   constructor.
 Qed.
 
+(** Composing two memory injections *)
+
+Definition compose_meminj (f f': meminj) : meminj :=
+  fun b =>
+    match f b with
+    | None => None
+    | Some(b', delta) =>
+        match f' b' with
+        | None => None
+        | Some(b'', delta') => Some(b'', delta + delta')
+        end
+    end.
+
+Lemma val_inject_compose:
+  forall f f' v1 v2 v3,
+  val_inject f v1 v2 -> val_inject f' v2 v3 ->
+  val_inject (compose_meminj f f') v1 v3.
+Proof.
+  intros. inv H; auto; inv H0; auto. econstructor.
+  unfold compose_meminj; rewrite H1; rewrite H3; eauto. 
+  rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints.
+Qed. 
+