- 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

6 files changed, 19 insertions, 18 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index f589fab..5427ac6 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -435,7 +435,7 @@ Definition do_ef_free
 
 Definition memcpy_args_ok
   (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop :=
-      (al = 1 \/ al = 2 \/ al = 4)
+      (al = 1 \/ al = 2 \/ al = 4 \/ al = 8)
    /\ sz > 0
    /\ (al | sz) /\ (al | osrc) /\ (al | odst)
    /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).
@@ -445,8 +445,9 @@ Remark memcpy_check_args:
   {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}.
 Proof with try (right; intuition omega).
   intros. 
-  assert (X: {al = 1 \/ al = 2 \/ al = 4} + {~(al = 1 \/ al = 2 \/ al = 4)}).
-    destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto...
+  assert (X: {al = 1 \/ al = 2 \/ al = 4 \/ al = 8} + {~(al = 1 \/ al = 2 \/ al = 4 \/ al = 8)}).
+    destruct (zeq al 1); auto. destruct (zeq al 2); auto.
+    destruct (zeq al 4); auto. destruct (zeq al 8); auto...
   unfold memcpy_args_ok. destruct X...
   assert (al > 0) by (intuition omega).
   destruct (zlt 0 sz)...
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 20e7bdb..c6d6fd5 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -219,6 +219,7 @@ Definition of_chunk (chunk: memory_chunk) :=
   | Mint32 => Any
   | Mfloat32 => Float32
   | Mfloat64 => Any
+  | Mfloat64al32 => Any
   end.
 
 Definition unop (op: unary_operation) (a: approx) :=
@@ -322,7 +323,7 @@ Definition var_set_self (cenv: compilenv) (id: ident) (k: stmt): res stmt :=
   | Var_stack_scalar chunk ofs =>
       OK (Sseq (make_store chunk (make_stackaddr ofs) (Evar (for_var id))) k)
   | Var_stack_array ofs sz al =>
-      OK (Sseq (Sbuiltin None (EF_memcpy sz (Zmin al 4))
+      OK (Sseq (Sbuiltin None (EF_memcpy sz al)
                          (make_stackaddr ofs :: Evar (for_var id) :: nil)) k)
   | _ =>
       Error(msg "Cminorgen.var_set_self")
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 7b18d8f..ea5d68e 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1753,6 +1753,8 @@ Proof.
   inv B; auto. inv H0; auto. constructor. auto.
   (* float64 *)
   exists va; auto.
+  (* float64al32 *)
+  exists va; auto.
 Qed.
 
 Lemma storev_mapped_content_inject:
@@ -2069,8 +2071,7 @@ Lemma var_set_self_correct_array:
   val_inject f v tv ->
   Mem.inject f m tm ->
   PTree.get id e = Some(b, Varray sz al) ->
-  extcall_memcpy_sem sz (Zmin al 4) ge
-                             (Vptr b Int.zero :: v :: nil) m E0 Vundef m' ->
+  extcall_memcpy_sem sz al ge (Vptr b Int.zero :: v :: nil) m E0 Vundef m' ->
   te!(for_var id) = Some tv ->
   exists f', exists tm',
     star step tge (State fn a k (Vptr sp Int.zero) te tm)
@@ -2087,7 +2088,7 @@ Proof.
   (* var_stack_array *)
   unfold var_set_self in VS. rewrite <- H in VS. inv VS.
   exploit match_callstack_match_globalenvs; eauto. intros [hi' MG].
-  assert (external_call (EF_memcpy sz0 (Zmin al0 4)) ge (Vptr b0 Int.zero :: v :: nil) m E0 Vundef m').
+  assert (external_call (EF_memcpy sz0 al0) ge (Vptr b0 Int.zero :: v :: nil) m E0 Vundef m').
     assumption.
   exploit external_call_mem_inject; eauto. 
   eapply inj_preserves_globals; eauto.
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 88eb3c7..b4993e7 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -320,8 +320,8 @@ Inductive bind_parameters: env ->
   | bind_parameters_array:
       forall e m id sz al params v1 vl b m1 m2,
       PTree.get id e = Some (b, Varray sz al) ->
-      extcall_memcpy_sem sz (Zmin al 4) 
-                   ge (Vptr b Int.zero :: v1 :: nil) m E0 Vundef m1 ->
+      extcall_memcpy_sem sz al
+                         ge (Vptr b Int.zero :: v1 :: nil) m E0 Vundef m1 ->
       bind_parameters e m1 params vl m2 ->
       bind_parameters e m ((id, Varray sz al) :: params) (v1 :: vl) m2.
 
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 3145681..b635b7d 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -273,7 +273,7 @@ Definition make_vol_load (dst: ident) (addr: expr) (ty: type) :=
   by-copy assignment of a value of Clight type [ty]. *)
 
 Definition make_memcpy (dst src: expr) (ty: type) :=
-  Sbuiltin None (EF_memcpy (Csyntax.sizeof ty) (Zmin (Csyntax.alignof ty) 4))
+  Sbuiltin None (EF_memcpy (Csyntax.sizeof ty) (Csyntax.alignof ty))
                 (dst :: src :: nil).
 
 (** [make_store addr ty rhs] stores the value of the
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 0b8b9a0..47bc1c6 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -727,6 +727,7 @@ Proof.
   rewrite H in MKLOAD. inv MKLOAD. constructor; auto. 
 Qed.
 
+(*
 Remark capped_alignof_divides:
   forall ty n, 
   (alignof ty | n) -> (Zmin (alignof ty) 4 | n).
@@ -743,6 +744,7 @@ Proof.
   intros. generalize (alignof_1248 ty). 
   intros [A|[A|[A|A]]]; rewrite A; auto.
 Qed.
+*)
 
 Lemma make_memcpy_correct:
   forall f dst src ty k e le m b ofs v t m',
@@ -757,11 +759,9 @@ Proof.
   econstructor.
   econstructor. eauto. econstructor. eauto. constructor. 
   econstructor; eauto. 
-  apply capped_alignof_124.
+  apply alignof_1248.
   apply sizeof_pos. 
-  apply capped_alignof_divides. apply sizeof_alignof_compat.
-  apply capped_alignof_divides; auto.
-  apply capped_alignof_divides; auto.
+  apply sizeof_alignof_compat.
 Qed.
  
 Lemma make_store_correct:
@@ -1046,11 +1046,9 @@ Proof.
   apply bind_parameters_array with b m1. 
   exploit me_local; eauto. intros [vk [A B]]. congruence. 
   econstructor; eauto. 
-  apply capped_alignof_124.
+  apply alignof_1248.
   apply sizeof_pos. 
-  apply capped_alignof_divides. apply sizeof_alignof_compat. 
-  apply capped_alignof_divides; auto.
-  apply capped_alignof_divides; auto.
+  apply sizeof_alignof_compat. 
   apply IHbind_parameters; auto.
 Qed.