From 4297fcb821c3188449b64184af73e41491a6118f Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 23 Jul 2012 15:01:54 +0000 Subject: - 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 --- cfrontend/Cexec.v | 7 ++++--- cfrontend/Cminorgen.v | 3 ++- cfrontend/Cminorgenproof.v | 7 ++++--- cfrontend/Csharpminor.v | 4 ++-- cfrontend/Cshmgen.v | 2 +- cfrontend/Cshmgenproof.v | 14 ++++++-------- 6 files changed, 19 insertions(+), 18 deletions(-) (limited to 'cfrontend') 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. -- cgit v1.2.3