From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index 48cd91e..5eee93a 100644 --- a/common/Events.v +++ b/common/Events.v @@ -57,7 +57,7 @@ Inductive eventval: Type := | EVint: int -> eventval | EVlong: int64 -> eventval | EVfloat: float -> eventval - | EVfloatsingle: float -> eventval + | EVsingle: float32 -> eventval | EVptr_global: ident -> int -> eventval. Inductive event: Type := @@ -274,8 +274,7 @@ Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_float: forall f, eventval_match (EVfloat f) Tfloat (Vfloat f) | ev_match_single: forall f, - Float.is_single f -> - eventval_match (EVfloatsingle f) Tsingle (Vfloat f) + eventval_match (EVsingle f) Tsingle (Vsingle f) | ev_match_ptr: forall id b ofs, Genv.find_symbol ge id = Some b -> eventval_match (EVptr_global id ofs) Tint (Vptr b ofs). @@ -388,7 +387,7 @@ Definition eventval_valid (ev: eventval) : Prop := | EVint _ => True | EVlong _ => True | EVfloat _ => True - | EVfloatsingle f => Float.is_single f + | EVsingle _ => True | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b end. @@ -397,7 +396,7 @@ Definition eventval_type (ev: eventval) : typ := | EVint _ => Tint | EVlong _ => Tlong | EVfloat _ => Tfloat - | EVfloatsingle _ => Tsingle + | EVsingle _ => Tsingle | EVptr_global id ofs => Tint end. @@ -412,7 +411,7 @@ Proof. destruct H1 as [b EQ]. exists (Vptr b i1); constructor; auto. exists (Vlong i0); constructor. exists (Vfloat f1); constructor. - exists (Vfloat f1); constructor; auto. + exists (Vsingle f1); constructor; auto. exists (Vint i); constructor. destruct H1 as [b' EQ]. exists (Vptr b' i0); constructor; auto. Qed. @@ -967,7 +966,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default). + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1022,7 +1021,7 @@ Qed. Lemma volatile_store_global_ok: forall chunk id ofs, extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk_use chunk :: nil) None cc_default). + (mksignature (type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) -- cgit v1.2.3