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/AST.v | 68 +++---- common/Events.v | 15 +- common/Globalenvs.v | 6 +- common/Memdata.v | 529 ++++++++++++++++++++++++++++------------------------ common/Memory.v | 325 +++++++++++++------------------- common/Memtype.v | 20 +- common/PrintAST.ml | 4 + common/Values.v | 139 ++++++++++++-- 8 files changed, 602 insertions(+), 504 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 29d1452..1c46389 100644 --- a/common/AST.v +++ b/common/AST.v @@ -35,22 +35,15 @@ Definition ident_eq := peq. Parameter ident_of_string : String.string -> ident. -(** The intermediate languages are weakly typed, using only four - types: [Tint] for 32-bit integers and pointers, [Tfloat] for 64-bit - floating-point numbers, [Tlong] for 64-bit integers, [Tsingle] - for 32-bit floating-point numbers. *) +(** The intermediate languages are weakly typed, using the following types: *) Inductive typ : Type := - | Tint - | Tfloat - | Tlong - | Tsingle. - -Definition typesize (ty: typ) : Z := - match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 | Tsingle => 4 end. - -Lemma typesize_pos: forall ty, typesize ty > 0. -Proof. destruct ty; simpl; omega. Qed. + | Tint (**r 32-bit integers or pointers *) + | Tfloat (**r 64-bit double-precision floats *) + | Tlong (**r 64-bit integers *) + | Tsingle (**r 32-bit single-precision floats *) + | Tany32 (**r any 32-bit value *) + | Tany64. (**r any 64-bit value, i.e. any value *) Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. Proof. decide equality. Defined. @@ -62,8 +55,22 @@ Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2} Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} := list_eq_dec typ_eq. -(** All values of type [Tsingle] are also of type [Tfloat]. This - corresponds to the following subtyping relation over types. *) +Definition typesize (ty: typ) : Z := + match ty with + | Tint => 4 + | Tfloat => 8 + | Tlong => 8 + | Tsingle => 4 + | Tany32 => 4 + | Tany64 => 8 + end. + +Lemma typesize_pos: forall ty, typesize ty > 0. +Proof. destruct ty; simpl; omega. Qed. + +(** All values of size 32 bits are also of type [Tany32]. All values + are of type [Tany64]. This corresponds to the following subtyping + relation over types. *) Definition subtype (ty1 ty2: typ) : bool := match ty1, ty2 with @@ -71,7 +78,8 @@ Definition subtype (ty1 ty2: typ) : bool := | Tlong, Tlong => true | Tfloat, Tfloat => true | Tsingle, Tsingle => true - | Tsingle, Tfloat => true + | (Tint | Tsingle | Tany32), Tany32 => true + | _, Tany64 => true | _, _ => false end. @@ -133,7 +141,9 @@ Inductive memory_chunk : Type := | Mint32 (**r 32-bit integer, or pointer *) | Mint64 (**r 64-bit integer *) | Mfloat32 (**r 32-bit single-precision float *) - | Mfloat64. (**r 64-bit double-precision float *) + | Mfloat64 (**r 64-bit double-precision float *) + | Many32 (**r any value that fits in 32 bits *) + | Many64. (**r any value *) Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}. Proof. decide equality. Defined. @@ -151,18 +161,8 @@ Definition type_of_chunk (c: memory_chunk) : typ := | Mint64 => Tlong | Mfloat32 => Tsingle | Mfloat64 => Tfloat - end. - -Definition type_of_chunk_use (c: memory_chunk) : typ := - match c with - | Mint8signed => Tint - | Mint8unsigned => Tint - | Mint16signed => Tint - | Mint16unsigned => Tint - | Mint32 => Tint - | Mint64 => Tlong - | Mfloat32 => Tfloat - | Mfloat64 => Tfloat + | Many32 => Tany32 + | Many64 => Tany64 end. (** The chunk that is appropriate to store and reload a value of @@ -174,6 +174,8 @@ Definition chunk_of_type (ty: typ) := | Tfloat => Mfloat64 | Tlong => Mint64 | Tsingle => Mfloat32 + | Tany32 => Many32 + | Tany64 => Many64 end. (** Initialization data for global variables. *) @@ -183,7 +185,7 @@ Inductive init_data: Type := | Init_int16: int -> init_data | Init_int32: int -> init_data | Init_int64: int64 -> init_data - | Init_float32: float -> init_data + | Init_float32: float32 -> init_data | Init_float64: float -> init_data | Init_space: Z -> init_data | Init_addrof: ident -> int -> init_data. (**r address of symbol + offset *) @@ -586,9 +588,9 @@ Definition ef_sig (ef: external_function): signature := | EF_external name sg => sg | EF_builtin name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default - | EF_vstore chunk => mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default + | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) cc_default - | EF_vstore_global chunk _ _ => mksignature (type_of_chunk_use chunk :: nil) None cc_default + | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None cc_default | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default 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 *) diff --git a/common/Globalenvs.v b/common/Globalenvs.v index bd38fa3..a34a05d 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -516,7 +516,7 @@ Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option m | Init_int16 n => Mem.store Mint16unsigned m b p (Vint n) | Init_int32 n => Mem.store Mint32 m b p (Vint n) | Init_int64 n => Mem.store Mint64 m b p (Vlong n) - | Init_float32 n => Mem.store Mfloat32 m b p (Vfloat n) + | Init_float32 n => Mem.store Mfloat32 m b p (Vsingle n) | Init_float64 n => Mem.store Mfloat64 m b p (Vfloat n) | Init_addrof symb ofs => match find_symbol ge symb with @@ -848,7 +848,7 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s Mem.load Mint64 m b p = Some(Vlong n) /\ load_store_init_data m b (p + 8) il' | Init_float32 n :: il' => - Mem.load Mfloat32 m b p = Some(Vfloat(Float.singleoffloat n)) + Mem.load Mfloat32 m b p = Some(Vsingle n) /\ load_store_init_data m b (p + 4) il' | Init_float64 n :: il' => Mem.load Mfloat64 m b p = Some(Vfloat n) @@ -895,7 +895,7 @@ Proof. eapply (A Mint16unsigned (Vint i)); eauto. eapply (A Mint32 (Vint i)); eauto. eapply (A Mint64 (Vlong i)); eauto. - eapply (A Mfloat32 (Vfloat f)); eauto. + eapply (A Mfloat32 (Vsingle f)); eauto. eapply (A Mfloat64 (Vfloat f)); eauto. inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0). eapply store_init_data_list_outside; eauto. right. simpl. xomega. diff --git a/common/Memdata.v b/common/Memdata.v index 1b74705..96278a2 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -39,6 +39,8 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Mint64 => 8 | Mfloat32 => 4 | Mfloat64 => 8 + | Many32 => 4 + | Many64 => 8 end. Lemma size_chunk_pos: @@ -86,6 +88,8 @@ Definition align_chunk (chunk: memory_chunk) : Z := | Mint64 => 8 | Mfloat32 => 4 | Mfloat64 => 4 + | Many32 => 4 + | Many64 => 4 end. Lemma align_chunk_pos: @@ -112,12 +116,27 @@ Proof. | exists 8; reflexivity ]. Qed. +Inductive quantity : Type := Q32 | Q64. + +Definition quantity_eq (q1 q2: quantity) : {q1 = q2} + {q1 <> q2}. +Proof. decide equality. Defined. +Global Opaque quantity_eq. + +Definition size_quantity_nat (q: quantity) := + match q with Q32 => 4%nat | Q64 => 8%nat end. + +Lemma size_quantity_nat_pos: + forall q, exists n, size_quantity_nat q = S n. +Proof. + intros. destruct q; [exists 3%nat | exists 7%nat]; auto. +Qed. + (** * Memory values *) (** A ``memory value'' is a byte-sized quantity that describes the current content of a memory cell. It can be either: - a concrete 8-bit integer; -- a byte-sized fragment of an opaque pointer; +- a byte-sized fragment of an opaque value; - the special constant [Undef] that represents uninitialized memory. *) @@ -126,7 +145,7 @@ Qed. Inductive memval: Type := | Undef: memval | Byte: byte -> memval - | Pointer: block -> int -> nat -> memval. + | Fragment: val -> quantity -> nat -> memval. (** * Encoding and decoding integers *) @@ -311,25 +330,28 @@ Proof. simpl. decEq. auto. Qed. -Fixpoint inj_pointer (n: nat) (b: block) (ofs: int) {struct n}: list memval := +Fixpoint inj_value_rec (n: nat) (v: val) (q: quantity) {struct n}: list memval := match n with | O => nil - | S m => Pointer b ofs m :: inj_pointer m b ofs + | S m => Fragment v q m :: inj_value_rec m v q end. -Fixpoint check_pointer (n: nat) (b: block) (ofs: int) (vl: list memval) +Definition inj_value (q: quantity) (v: val): list memval := + inj_value_rec (size_quantity_nat q) v q. + +Fixpoint check_value (n: nat) (v: val) (q: quantity) (vl: list memval) {struct n} : bool := match n, vl with | O, nil => true - | S m, Pointer b' ofs' m' :: vl' => - eq_block b b' && Int.eq_dec ofs ofs' && beq_nat m m' && check_pointer m b ofs vl' + | S m, Fragment v' q' m' :: vl' => + Val.eq v v' && quantity_eq q q' && beq_nat m m' && check_value m v q vl' | _, _ => false end. -Definition proj_pointer (vl: list memval) : val := +Definition proj_value (q: quantity) (vl: list memval) : val := match vl with - | Pointer b ofs n :: vl' => - if check_pointer 4%nat b ofs vl then Vptr b ofs else Vundef + | Fragment v q' n :: vl' => + if check_value (size_quantity_nat q) v q vl then v else Vundef | _ => Vundef end. @@ -338,10 +360,12 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval := | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n)) | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n)) | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n)) - | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs + | Vptr b ofs, Mint32 => inj_value Q32 v | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n)) - | 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))) + | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) + | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) + | _, Many32 => inj_value Q32 v + | _, Many64 => inj_value Q64 v | _, _ => list_repeat (size_chunk_nat chunk) Undef end. @@ -355,12 +379,15 @@ 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)) | Mint64 => Vlong(Int64.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))) + | Mfloat32 => Vsingle(Float32.of_bits (Int.repr (decode_int bl))) + | Mfloat64 => Vfloat(Float.of_bits (Int64.repr (decode_int bl))) + | Many32 => Vundef + | Many64 => Vundef end | None => match chunk with - | Mint32 => proj_pointer vl + | Mint32 | Many32 => Val.load_result chunk (proj_value Q32 vl) + | Many64 => Val.load_result chunk (proj_value Q64 vl) | _ => Vundef end end. @@ -374,14 +401,40 @@ Proof. | rewrite length_inj_bytes; apply encode_int_length ]. Qed. -Lemma check_inj_pointer: - forall b ofs n, check_pointer n b ofs (inj_pointer n b ofs) = true. +Lemma check_inj_value: + forall v q n, check_value n v q (inj_value_rec n v q) = true. Proof. induction n; simpl. auto. unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_true. rewrite <- beq_nat_refl. simpl; auto. Qed. +Lemma proj_inj_value: + forall q v, proj_value q (inj_value q v) = v. +Proof. + intros. unfold proj_value, inj_value. destruct (size_quantity_nat_pos q) as [n EQ]. + rewrite EQ at 1. simpl. rewrite check_inj_value. auto. +Qed. + +Remark in_inj_value: + forall mv v q, In mv (inj_value q v) -> exists n, mv = Fragment v q n. +Proof. +Local Transparent inj_value. + unfold inj_value; intros until q. generalize (size_quantity_nat q). induction n; simpl; intros. + contradiction. + destruct H. exists n; auto. eauto. +Qed. + +Lemma proj_inj_value_mismatch: + forall q1 q2 v, q1 <> q2 -> proj_value q1 (inj_value q2 v) = Vundef. +Proof. + intros. unfold proj_value. destruct (inj_value q2 v) eqn:V. auto. destruct m; auto. + destruct (in_inj_value (Fragment v0 q n) v q2) as [n' EQ]. + rewrite V; auto with coqlib. inv EQ. + destruct (size_quantity_nat_pos q1) as [p EQ1]; rewrite EQ1; simpl. + unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_false by congruence. auto. +Qed. + Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : Prop := match v1, chunk1, chunk2 with | Vundef, _, _ => v2 = Vundef @@ -394,21 +447,30 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : | Vint n, Mint16signed, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n) | 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, (Mint64 | Mfloat32 | Mfloat64), _ => v2 = Vundef + | Vint n, Many32, (Mint32 | Many32) => v2 = Vint n + | Vint n, Mint32, Mfloat32 => v2 = Vsingle(Float32.of_bits n) + | Vint n, Many64, Many64 => v2 = Vint n + | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Many64), _ => v2 = Vundef | Vint n, _, _ => True (**r nothing meaningful to say about v2 *) - | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs + | Vptr b ofs, (Mint32 | Many32), (Mint32 | Many32) => v2 = Vptr b ofs + | Vptr b ofs, Many64, Many64 => v2 = Vptr b ofs | Vptr b ofs, _, _ => v2 = Vundef | Vlong n, Mint64, Mint64 => v2 = Vlong n - | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.double_of_bits n) - | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64), _ => v2 = Vundef + | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.of_bits n) + | Vlong n, Many64, Many64 => v2 = Vlong n + | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64|Many32), _ => v2 = Vundef | Vlong n, _, _ => True (**r nothing meaningful to say about v2 *) - | 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, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64), _ => v2 = Vundef - | Vfloat f, Mfloat64, Mint64 => v2 = Vlong(Float.bits_of_double f) + | Vfloat f, Mfloat64, Mint64 => v2 = Vlong(Float.to_bits f) + | Vfloat f, Many64, Many64 => v2 = Vfloat f + | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mint64|Many32), _ => v2 = Vundef | Vfloat f, _, _ => True (* nothing interesting to say about v2 *) + | Vsingle f, Mfloat32, Mfloat32 => v2 = Vsingle f + | Vsingle f, Mfloat32, Mint32 => v2 = Vint(Float32.to_bits f) + | Vsingle f, Many32, Many32 => v2 = Vsingle f + | Vsingle f, Many64, Many64 => v2 = Vsingle f + | Vsingle f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64|Mfloat64|Many64), _ => v2 = Vundef + | Vsingle f, _, _ => True (* nothing interesting to say about v2 *) end. Remark decode_val_undef: @@ -417,14 +479,23 @@ Proof. intros. unfold decode_val. simpl. destruct chunk; auto. Qed. +Remark proj_bytes_inj_value: + forall q v, proj_bytes (inj_value q v) = None. +Proof. + intros. destruct q; reflexivity. +Qed. + Lemma decode_encode_val_general: forall v chunk1 chunk2, decode_encode_val v chunk1 chunk2 (decode_val chunk2 (encode_val chunk1 v)). Proof. -Opaque inj_pointer. +Opaque inj_value. intros. - destruct v; destruct chunk1; simpl; try (apply decode_val_undef); - destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes). + destruct v; destruct chunk1 eqn:C1; simpl; try (apply decode_val_undef); + destruct chunk2 eqn:C2; unfold decode_val; auto; + try (rewrite proj_inj_bytes); try (rewrite proj_bytes_inj_value); + try (rewrite proj_inj_value); try (rewrite proj_inj_value_mismatch by congruence); + auto. rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega. rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega. rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega. @@ -437,14 +508,10 @@ Opaque inj_pointer. rewrite decode_encode_int_4. auto. rewrite decode_encode_int_8. auto. rewrite decode_encode_int_8. auto. - rewrite decode_encode_int_4. auto. - rewrite decode_encode_int_4. decEq. apply Float.single_of_bits_of_single. rewrite decode_encode_int_8. auto. - 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. - simpl. intros EQ; rewrite EQ; auto. + rewrite decode_encode_int_8. decEq. apply Float.of_to_bits. + rewrite decode_encode_int_4. auto. + rewrite decode_encode_int_4. decEq. apply Float32.of_to_bits. Qed. Lemma decode_encode_val_similar: @@ -465,12 +532,8 @@ Lemma decode_val_type: Proof. intros. unfold decode_val. destruct (proj_bytes cl). - destruct chunk; simpl; auto. apply Float.single_of_bits_is_single. destruct chunk; simpl; auto. - unfold proj_pointer. destruct cl; try (exact I). - destruct m; try (exact I). - destruct (check_pointer 4%nat b i (Pointer b i n :: cl)); - exact I. + destruct chunk; exact I || apply Val.load_result_type. Qed. Lemma encode_val_int8_signed_unsigned: @@ -518,7 +581,6 @@ Lemma decode_val_cast: | Mint8unsigned => v = Val.zero_ext 8 v | Mint16signed => v = Val.sign_ext 16 v | Mint16unsigned => v = Val.zero_ext 16 v - | Mfloat32 => v = Val.singleoffloat v | _ => True end. Proof. @@ -527,145 +589,132 @@ Proof. unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. - simpl. rewrite Float.singleoffloat_of_bits. auto. Qed. (** Pointers cannot be forged. *) -Definition memval_valid_first (mv: memval) : Prop := - match mv with - | Pointer b ofs n => n = 3%nat - | _ => True - end. - -Definition memval_valid_cont (mv: memval) : Prop := - match mv with - | Pointer b ofs n => n <> 3%nat - | _ => True +Definition quantity_chunk (chunk: memory_chunk) := + match chunk with + | Mint64 | Mfloat64 | Many64 => Q64 + | _ => Q32 end. -Inductive encoding_shape: list memval -> Prop := - | encoding_shape_intro: forall mv1 mvl, - memval_valid_first mv1 -> - (forall mv, In mv mvl -> memval_valid_cont mv) -> - encoding_shape (mv1 :: mvl). - -Lemma encode_val_shape: - forall chunk v, encoding_shape (encode_val chunk v). +Inductive shape_encoding (chunk: memory_chunk) (v: val): list memval -> Prop := + | shape_encoding_f: forall q i mvl, + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + q = quantity_chunk chunk -> + S i = size_quantity_nat q -> + (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) -> + shape_encoding chunk v (Fragment v q i :: mvl) + | shape_encoding_b: forall b mvl, + match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end -> + (forall mv, In mv mvl -> exists b', mv = Byte b') -> + shape_encoding chunk v (Byte b :: mvl) + | shape_encoding_u: forall mvl, + (forall mv, In mv mvl -> mv = Undef) -> + shape_encoding chunk v (Undef :: mvl). + +Lemma encode_val_shape: forall chunk v, shape_encoding chunk v (encode_val chunk v). Proof. intros. - destruct (size_chunk_nat_pos chunk) as [sz1 EQ]. - assert (A: encoding_shape (list_repeat (size_chunk_nat chunk) Undef)). - rewrite EQ; simpl; constructor. exact I. - intros. replace mv with Undef. exact I. symmetry; eapply in_list_repeat; eauto. - assert (B: forall bl, length bl = size_chunk_nat chunk -> - encoding_shape (inj_bytes bl)). - intros. destruct bl; simpl in *. congruence. - constructor. exact I. unfold inj_bytes. intros. - exploit list_in_map_inv; eauto. intros [x [C D]]. subst mv. exact I. - destruct v; auto; destruct chunk; simpl; auto; try (apply B; apply encode_int_length). - constructor. red. auto. - simpl; intros. intuition; subst mv; red; simpl; congruence. -Qed. - -Lemma check_pointer_inv: - forall b ofs n mv, - check_pointer n b ofs mv = true -> mv = inj_pointer n b ofs. -Proof. - induction n; destruct mv; simpl. - auto. - congruence. - congruence. - destruct m; try congruence. intro. - destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - destruct (andb_prop _ _ H2). - decEq. decEq. symmetry; eapply proj_sumbool_true; eauto. - symmetry; eapply proj_sumbool_true; eauto. - symmetry; apply beq_nat_true; auto. - auto. + destruct (size_chunk_nat_pos chunk) as [sz EQ]. + assert (A: forall mv q n, + (n < size_quantity_nat q)%nat -> + In mv (inj_value_rec n v q) -> + exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q). + { + induction n; simpl; intros. contradiction. destruct H0. + exists n; split; auto. omega. apply IHn; auto. omega. + } + assert (B: forall q, + q = quantity_chunk chunk -> + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + shape_encoding chunk v (inj_value q v)). + { +Local Transparent inj_value. + intros. unfold inj_value. destruct (size_quantity_nat_pos q) as [sz' EQ']. + rewrite EQ'. simpl. constructor; auto. + intros; eapply A; eauto. omega. + } + assert (C: forall bl, + match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end -> + length (inj_bytes bl) = size_chunk_nat chunk -> + shape_encoding chunk v (inj_bytes bl)). + { + intros. destruct bl as [|b1 bl]. simpl in H0; congruence. simpl. + constructor; auto. unfold inj_bytes; intros. exploit list_in_map_inv; eauto. + intros (b & P & Q); exists b; auto. + } + assert (D: shape_encoding chunk v (list_repeat (size_chunk_nat chunk) Undef)). + { + intros. rewrite EQ; simpl; constructor; auto. + intros. eapply in_list_repeat; eauto. + } + generalize (encode_val_length chunk v). intros LEN. + unfold encode_val; unfold encode_val in LEN; destruct v; destruct chunk; (apply B || apply C || apply D); auto; red; auto. Qed. -Inductive decoding_shape: list memval -> Prop := - | decoding_shape_intro: forall mv1 mvl, - memval_valid_first mv1 -> mv1 <> Undef -> - (forall mv, In mv mvl -> memval_valid_cont mv /\ mv <> Undef) -> - decoding_shape (mv1 :: mvl). - -Lemma decode_val_shape: - forall chunk mvl, - List.length mvl = size_chunk_nat chunk -> - decode_val chunk mvl = Vundef \/ decoding_shape mvl. +Inductive shape_decoding (chunk: memory_chunk): list memval -> val -> Prop := + | shape_decoding_f: forall v q i mvl, + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + q = quantity_chunk chunk -> + S i = size_quantity_nat q -> + (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) -> + shape_decoding chunk (Fragment v q i :: mvl) (Val.load_result chunk v) + | shape_decoding_b: forall b mvl v, + match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end -> + (forall mv, In mv mvl -> exists b', mv = Byte b') -> + shape_decoding chunk (Byte b :: mvl) v + | shape_decoding_u: forall mvl, + shape_decoding chunk mvl Vundef. + +Lemma decode_val_shape: forall chunk mv1 mvl, + shape_decoding chunk (mv1 :: mvl) (decode_val chunk (mv1 :: mvl)). Proof. - intros. destruct (size_chunk_nat_pos chunk) as [sz EQ]. + intros. + assert (A: forall mv mvs bs, proj_bytes mvs = Some bs -> In mv mvs -> + exists b, mv = Byte b). + { + induction mvs; simpl; intros. + contradiction. + destruct a; try discriminate. destruct H0. exists i; auto. + destruct (proj_bytes mvs); try discriminate. eauto. + } + assert (B: forall v q mv n mvs, + check_value n v q mvs = true -> In mv mvs -> (n < size_quantity_nat q)%nat -> + exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q). + { + induction n; destruct mvs; simpl; intros; try discriminate. + contradiction. + destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst. + destruct H0. subst mv. exists n0; split; auto. omega. + eapply IHn; eauto. omega. + } + assert (U: forall mvs, shape_decoding chunk mvs (Val.load_result chunk Vundef)). + { + intros. replace (Val.load_result chunk Vundef) with Vundef. constructor. + destruct chunk; auto. + } + assert (C: forall q, size_quantity_nat q = size_chunk_nat chunk -> + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + shape_decoding chunk (mv1 :: mvl) (Val.load_result chunk (proj_value q (mv1 :: mvl)))). + { + intros. unfold proj_value. destruct mv1; auto. + destruct (size_quantity_nat_pos q) as [sz EQ]. rewrite EQ. + simpl. unfold proj_sumbool. rewrite dec_eq_true. + destruct (quantity_eq q q0); auto. + destruct (beq_nat sz n) eqn:EQN; auto. + destruct (check_value sz v q mvl) eqn:CHECK; auto. + simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. + destruct H0 as [E|[E|E]]; subst chunk; destruct q; auto || discriminate. + congruence. + intros. eapply B; eauto. omega. + } unfold decode_val. - caseEq (proj_bytes mvl). - intros bl PROJ. right. exploit inj_proj_bytes; eauto. intros. subst mvl. - destruct bl; simpl in H. congruence. simpl. constructor. - red; auto. congruence. - unfold inj_bytes; intros. exploit list_in_map_inv; eauto. intros [b [A B]]. - subst mv. split. red; auto. congruence. - intros. destruct chunk; auto. unfold proj_pointer. - destruct mvl; auto. destruct m; auto. - caseEq (check_pointer 4%nat b i (Pointer b i n :: mvl)); auto. - intros. right. exploit check_pointer_inv; eauto. simpl; intros; inv H2. - constructor. red. auto. congruence. - simpl; intros. intuition; subst mv; simpl; congruence. -Qed. - -Lemma encode_val_pointer_inv: - forall chunk v b ofs n mvl, - encode_val chunk v = Pointer b ofs n :: mvl -> - chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3%nat b ofs. -Proof. - intros until mvl. - assert (A: list_repeat (size_chunk_nat chunk) Undef = Pointer b ofs n :: mvl -> - chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs). - intros. destruct (size_chunk_nat_pos chunk) as [sz SZ]. rewrite SZ in H. simpl in H. discriminate. - assert (B: forall bl, length bl <> 0%nat -> inj_bytes bl = Pointer b ofs n :: mvl -> - chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs). - intros. destruct bl; simpl in *; congruence. - unfold encode_val; destruct v; destruct chunk; - (apply A; assumption) || - (apply B; rewrite encode_int_length; congruence) || idtac. - simpl. intros EQ; inv EQ; auto. -Qed. - -Lemma decode_val_pointer_inv: - forall chunk mvl b ofs, - decode_val chunk mvl = Vptr b ofs -> - chunk = Mint32 /\ mvl = inj_pointer 4%nat b ofs. -Proof. - intros until ofs; unfold decode_val. - destruct (proj_bytes mvl). - destruct chunk; congruence. - destruct chunk; try congruence. - unfold proj_pointer. destruct mvl. congruence. destruct m; try congruence. - case_eq (check_pointer 4%nat b0 i (Pointer b0 i n :: mvl)); intros. - inv H0. split; auto. apply check_pointer_inv; auto. - congruence. -Qed. - -Inductive pointer_encoding_shape: list memval -> Prop := - | pointer_encoding_shape_intro: forall mv1 mvl, - ~memval_valid_cont mv1 -> - (forall mv, In mv mvl -> ~memval_valid_first mv) -> - pointer_encoding_shape (mv1 :: mvl). - -Lemma encode_pointer_shape: - forall b ofs, pointer_encoding_shape (encode_val Mint32 (Vptr b ofs)). -Proof. - intros. simpl. constructor. - unfold memval_valid_cont. red; intro. elim H. auto. - unfold memval_valid_first. simpl; intros; intuition; subst mv; congruence. -Qed. - -Lemma decode_pointer_shape: - forall chunk mvl b ofs, - decode_val chunk mvl = Vptr b ofs -> - chunk = Mint32 /\ pointer_encoding_shape mvl. -Proof. - intros. exploit decode_val_pointer_inv; eauto. intros [A B]. - split; auto. subst mvl. apply encode_pointer_shape. + destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB. + exploit (A mv1); eauto with coqlib. intros [b1 EQ1]; subst mv1. + destruct chunk; (apply shape_decoding_u || apply shape_decoding_b); eauto with coqlib. + destruct chunk; (apply shape_decoding_u || apply C); auto. Qed. (** * Compatibility with memory injections *) @@ -675,18 +724,17 @@ Qed. Inductive memval_inject (f: meminj): memval -> memval -> Prop := | memval_inject_byte: forall n, memval_inject f (Byte n) (Byte n) - | memval_inject_ptr: - forall b1 ofs1 b2 ofs2 delta n, - f b1 = Some (b2, delta) -> - ofs2 = Int.add ofs1 (Int.repr delta) -> - memval_inject f (Pointer b1 ofs1 n) (Pointer b2 ofs2 n) + | memval_inject_frag: + forall v1 v2 q n, + val_inject f v1 v2 -> + memval_inject f (Fragment v1 q n) (Fragment v2 q n) | memval_inject_undef: forall mv, memval_inject f Undef mv. Lemma memval_inject_incr: forall f f' v1 v2, memval_inject f v1 v2 -> inject_incr f f' -> memval_inject f' v1 v2. Proof. - intros. inv H; econstructor. rewrite (H0 _ _ _ H1). reflexivity. auto. + intros. inv H; econstructor. eapply val_inject_incr; eauto. Qed. (** [decode_val], applied to lists of memory values that are pairwise @@ -706,38 +754,33 @@ Proof. congruence. Qed. -Lemma check_pointer_inject: +Lemma check_value_inject: forall f vl vl', list_forall2 (memval_inject f) vl vl' -> - forall n b ofs b' delta, - check_pointer n b ofs vl = true -> - f b = Some(b', delta) -> - check_pointer n b' (Int.add ofs (Int.repr delta)) vl' = true. + forall v v' q n, + check_value n v q vl = true -> + val_inject f v v' -> v <> Vundef -> + check_value n v' q vl' = true. Proof. induction 1; intros; destruct n; simpl in *; auto. inv H; auto. - destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H). - destruct (andb_prop _ _ H5). - assert (n = n0) by (apply beq_nat_true; auto). - assert (b = b0) by (eapply proj_sumbool_true; eauto). - assert (ofs = ofs1) by (eapply proj_sumbool_true; eauto). - subst. rewrite H3 in H2; inv H2. - unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_true. - rewrite <- beq_nat_refl. simpl. eauto. - congruence. + InvBooleans. assert (n = n0) by (apply beq_nat_true; auto). subst v1 q0 n0. + replace v2 with v'. + unfold proj_sumbool; rewrite ! dec_eq_true. rewrite <- beq_nat_refl. simpl; eauto. + inv H2; try discriminate; inv H4; congruence. + discriminate. Qed. -Lemma proj_pointer_inject: - forall f vl1 vl2, +Lemma proj_value_inject: + forall f q vl1 vl2, list_forall2 (memval_inject f) vl1 vl2 -> - val_inject f (proj_pointer vl1) (proj_pointer vl2). + val_inject f (proj_value q vl1) (proj_value q vl2). Proof. - intros. unfold proj_pointer. + intros. unfold proj_value. inversion H; subst. auto. inversion H0; subst; auto. - case_eq (check_pointer 4%nat b0 ofs1 (Pointer b0 ofs1 n :: al)); intros. - exploit check_pointer_inject. eexact H. eauto. eauto. - intro. rewrite H4. econstructor; eauto. - constructor. + destruct (check_value (size_quantity_nat q) v1 q (Fragment v1 q0 n :: al)) eqn:B; auto. + destruct (Val.eq v1 Vundef). subst; auto. + erewrite check_value_inject by eauto. auto. Qed. Lemma proj_bytes_not_inject: @@ -754,9 +797,9 @@ Proof. auto. Qed. -Lemma check_pointer_undef: - forall n b ofs vl, - In Undef vl -> check_pointer n b ofs vl = false. +Lemma check_value_undef: + forall n q v vl, + In Undef vl -> check_value n v q vl = false. Proof. induction n; intros; simpl. destruct vl. elim H. auto. @@ -765,12 +808,12 @@ Proof. rewrite IHn; auto. apply andb_false_r. Qed. -Lemma proj_pointer_undef: - forall vl, In Undef vl -> proj_pointer vl = Vundef. +Lemma proj_value_undef: + forall q vl, In Undef vl -> proj_value q vl = Vundef. Proof. - intros; unfold proj_pointer. + intros; unfold proj_value. destruct vl; auto. destruct m; auto. - rewrite check_pointer_undef. auto. auto. + rewrite check_value_undef. auto. auto. Qed. Theorem decode_val_inject: @@ -779,13 +822,20 @@ Theorem decode_val_inject: val_inject f (decode_val chunk vl1) (decode_val chunk vl2). Proof. intros. unfold decode_val. - case_eq (proj_bytes vl1); intros. - exploit proj_bytes_inject; eauto. intros. rewrite H1. + destruct (proj_bytes vl1) as [bl1|] eqn:PB1. + exploit proj_bytes_inject; eauto. intros PB2. rewrite PB2. destruct chunk; constructor. + assert (A: forall q fn, + val_inject f (Val.load_result chunk (proj_value q vl1)) + (match proj_bytes vl2 with + | Some bl => fn bl + | None => Val.load_result chunk (proj_value q vl2) + end)). + { intros. destruct (proj_bytes vl2) as [bl2|] eqn:PB2. + rewrite proj_value_undef. destruct chunk; auto. eapply proj_bytes_not_inject; eauto. congruence. + apply val_load_result_inject. apply proj_value_inject; auto. + } destruct chunk; auto. - case_eq (proj_bytes vl2); intros. - rewrite proj_pointer_undef. auto. eapply proj_bytes_not_inject; eauto. congruence. - apply proj_pointer_inject; auto. Qed. (** Symmetrically, [encode_val], applied to values related by [val_inject], @@ -805,6 +855,13 @@ Proof. induction vl; simpl; constructor; auto. constructor. Qed. +Lemma repeat_Undef_inject_encode_val: + forall f chunk v, + list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v). +Proof. + intros. rewrite <- (encode_val_length chunk v). apply repeat_Undef_inject_any. +Qed. + Lemma repeat_Undef_inject_self: forall f n, list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef). @@ -812,19 +869,24 @@ Proof. induction n; simpl; constructor; auto. constructor. Qed. +Lemma inj_value_inject: + forall f v1 v2 q, val_inject f v1 v2 -> list_forall2 (memval_inject f) (inj_value q v1) (inj_value q v2). +Proof. + intros. +Local Transparent inj_value. + unfold inj_value. generalize (size_quantity_nat q). induction n; simpl; constructor; auto. + constructor; auto. +Qed. + Theorem encode_val_inject: forall f v1 v2 chunk, val_inject f v1 v2 -> list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2). Proof. - intros. inv H; simpl. - destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self. - destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self. - destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self. - destruct chunk; try (apply repeat_Undef_inject_self). - repeat econstructor; eauto. - replace (size_chunk_nat chunk) with (length (encode_val chunk v2)). - apply repeat_Undef_inject_any. apply encode_val_length. + intros. inversion H; subst; simpl; destruct chunk; + auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val. + unfold encode_val. destruct v2; apply inj_value_inject; auto. + unfold encode_val. destruct v2; apply inj_value_inject; auto. Qed. Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id. @@ -832,8 +894,7 @@ Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id. Lemma memval_lessdef_refl: forall mv, memval_lessdef mv mv. Proof. - red. destruct mv; econstructor. - unfold inject_id; reflexivity. rewrite Int.add_zero; auto. + red. destruct mv; econstructor. apply val_inject_id. auto. Qed. (** [memval_inject] and compositions *) @@ -845,9 +906,8 @@ Lemma memval_inject_compose: 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. + inv H0. econstructor. + eapply val_inject_compose; eauto. constructor. Qed. @@ -905,28 +965,22 @@ Qed. Lemma decode_val_int64: forall l1 l2, length l1 = 4%nat -> length l2 = 4%nat -> - decode_val Mint64 (l1 ++ l2) = - Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2)) - (decode_val Mint32 (if Archi.big_endian then l2 else l1)). + Val.lessdef + (decode_val Mint64 (l1 ++ l2)) + (Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2)) + (decode_val Mint32 (if Archi.big_endian then l2 else l1))). Proof. intros. unfold decode_val. - assert (PP: forall vl, match proj_pointer vl with Vundef => True | Vptr _ _ => True | _ => False end). - intros. unfold proj_pointer. destruct vl; auto. destruct m; auto. - destruct (check_pointer 4 b i (Pointer b i n :: vl)); auto. - assert (PP1: forall vl v2, Val.longofwords (proj_pointer vl) v2 = Vundef). - intros. generalize (PP vl). destruct (proj_pointer vl); reflexivity || contradiction. - assert (PP2: forall v1 vl, Val.longofwords v1 (proj_pointer vl) = Vundef). - intros. destruct v1; simpl; auto. - generalize (PP vl). destruct (proj_pointer vl); reflexivity || contradiction. rewrite proj_bytes_append. - destruct (proj_bytes l1) as [b1|] eqn:B1; destruct (proj_bytes l2) as [b2|] eqn:B2. -- exploit length_proj_bytes. eexact B1. rewrite H; intro L1. + destruct (proj_bytes l1) as [b1|] eqn:B1; destruct (proj_bytes l2) as [b2|] eqn:B2; auto. + exploit length_proj_bytes. eexact B1. rewrite H; intro L1. exploit length_proj_bytes. eexact B2. rewrite H0; intro L2. assert (UR: forall l, length l = 4%nat -> Int.unsigned (Int.repr (int_of_bytes l)) = int_of_bytes l). intros. apply Int.unsigned_repr. generalize (int_of_bytes_range l). rewrite H1. change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). omega. + apply Val.lessdef_same. unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2. + rewrite <- (rev_length b1) in L1. rewrite <- (rev_length b2) in L2. @@ -938,9 +992,6 @@ Proof. + unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal. rewrite !UR by auto. rewrite int_of_bytes_append. rewrite L1. change (Z.of_nat 4 * 8) with 32. ring. -- destruct Archi.big_endian; rewrite B1; rewrite B2; auto. -- destruct Archi.big_endian; rewrite B1; rewrite B2; auto. -- destruct Archi.big_endian; rewrite B1; rewrite B2; auto. Qed. Lemma bytes_of_int_append: diff --git a/common/Memory.v b/common/Memory.v index 9afdfd3..e45df66 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -690,7 +690,6 @@ Theorem load_cast: | Mint8unsigned => v = Val.zero_ext 8 v | Mint16signed => v = Val.sign_ext 16 v | Mint16unsigned => v = Val.zero_ext 16 v - | Mfloat32 => v = Val.singleoffloat v | _ => True end. Proof. @@ -727,24 +726,6 @@ Proof. rewrite pred_dec_false; auto. Qed. -(* -Theorem load_float64al32: - forall m b ofs v, - load Mfloat64 m b ofs = Some v -> load Mfloat64al32 m b ofs = Some v. -Proof. - unfold load; intros. destruct (valid_access_dec m Mfloat64 b ofs Readable); try discriminate. - rewrite pred_dec_true. assumption. - apply valid_access_compat with Mfloat64; auto. simpl; omega. -Qed. - -Theorem loadv_float64al32: - forall m a v, - loadv Mfloat64 m a = Some v -> loadv Mfloat64al32 m a = Some v. -Proof. - unfold loadv; intros. destruct a; auto. apply load_float64al32; auto. -Qed. -*) - (** ** Properties related to [loadbytes] *) Theorem range_perm_loadbytes: @@ -896,7 +877,7 @@ Theorem load_int64_split: exists v1 v2, load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2) /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1) - /\ v = Val.longofwords v1 v2. + /\ Val.lessdef v (Val.longofwords v1 v2). Proof. intros. exploit load_valid_access; eauto. intros [A B]. simpl in *. @@ -927,7 +908,7 @@ Theorem loadv_int64_split: exists v1 v2, loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2) /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1) - /\ v = Val.longofwords v1 v2. + /\ Val.lessdef v (Val.longofwords v1 v2). Proof. intros. destruct a; simpl in H; try discriminate. exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ). @@ -1138,18 +1119,17 @@ Proof. red; intro; elim n0; red; intros; eauto with mem. Qed. -Lemma setN_property: - forall (P: memval -> Prop) vl p q c, - (forall v, In v vl -> P v) -> +Lemma setN_in: + forall vl p q c, p <= q < p + Z_of_nat (length vl) -> - P(ZMap.get q (setN vl p c)). + In (ZMap.get q (setN vl p c)) vl. Proof. induction vl; intros. - simpl in H0. omegaContradiction. - simpl length in H0. rewrite inj_S in H0. simpl. + simpl in H. omegaContradiction. + simpl length in H. rewrite inj_S in H. simpl. destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss. auto with coqlib. omega. - apply IHvl. auto with coqlib. omega. + right. apply IHvl. omega. Qed. Lemma getN_in: @@ -1164,84 +1144,114 @@ Proof. right. apply IHn. omega. Qed. +End STORE. + +Local Hint Resolve perm_store_1 perm_store_2: mem. +Local Hint Resolve store_valid_block_1 store_valid_block_2: mem. +Local Hint Resolve store_valid_access_1 store_valid_access_2 + store_valid_access_3: mem. + +Lemma load_store_overlap: + forall chunk m1 b ofs v m2 chunk' ofs' v', + store chunk m1 b ofs v = Some m2 -> + load chunk' m2 b ofs' = Some v' -> + ofs' + size_chunk chunk' > ofs -> + ofs + size_chunk chunk > ofs' -> + exists mv1 mvl mv1' mvl', + shape_encoding chunk v (mv1 :: mvl) + /\ shape_decoding chunk' (mv1' :: mvl') v' + /\ ( (ofs' = ofs /\ mv1' = mv1) + \/ (ofs' > ofs /\ In mv1' mvl) + \/ (ofs' < ofs /\ In mv1 mvl')). +Proof. + intros. + exploit load_result; eauto. erewrite store_mem_contents by eauto; simpl. + rewrite PMap.gss. + set (c := (mem_contents m1)#b). intros V'. + destruct (size_chunk_nat_pos chunk) as [sz SIZE]. + destruct (size_chunk_nat_pos chunk') as [sz' SIZE']. + destruct (encode_val chunk v) as [ | mv1 mvl] eqn:ENC. + generalize (encode_val_length chunk v); rewrite ENC; simpl; congruence. + set (c' := setN (mv1::mvl) ofs c) in *. + exists mv1, mvl, (ZMap.get ofs' c'), (getN sz' (ofs' + 1) c'). + split. rewrite <- ENC. apply encode_val_shape. + split. rewrite V', SIZE'. apply decode_val_shape. + destruct (zeq ofs' ofs). +- subst ofs'. left; split. auto. unfold c'. simpl. + rewrite setN_outside by omega. apply ZMap.gss. +- right. destruct (zlt ofs ofs'). +(* If ofs < ofs': the load reads (at ofs') a continuation byte from the write. + ofs ofs' ofs+|chunk| + [-------------------] write + [-------------------] read +*) ++ left; split. omega. unfold c'. simpl. apply setN_in. + assert (Z.of_nat (length (mv1 :: mvl)) = size_chunk chunk). + { rewrite <- ENC; rewrite encode_val_length. rewrite size_chunk_conv; auto. } + simpl length in H3. rewrite inj_S in H3. omega. +(* If ofs > ofs': the load reads (at ofs) the first byte from the write. + ofs' ofs ofs'+|chunk'| + [-------------------] write + [----------------] read +*) ++ right; split. omega. replace mv1 with (ZMap.get ofs c'). + apply getN_in. + assert (size_chunk chunk' = Zsucc (Z.of_nat sz')). + { rewrite size_chunk_conv. rewrite SIZE'. rewrite inj_S; auto. } + omega. + unfold c'. simpl. rewrite setN_outside by omega. apply ZMap.gss. +Qed. + +Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop := + match chunk1, chunk2 with + | (Mint32 | Many32), (Mint32 | Many32) => True + | Many64, Many64 => True + | _, _ => False + end. + +Lemma compat_pointer_chunks_true: + forall chunk1 chunk2, + (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Many64) -> + (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Many64) -> + quantity_chunk chunk1 = quantity_chunk chunk2 -> + compat_pointer_chunks chunk1 chunk2. +Proof. + intros. destruct H as [P|[P|P]]; destruct H0 as [Q|[Q|Q]]; + subst; red; auto; discriminate. +Qed. + Theorem load_pointer_store: - forall chunk' b' ofs' v_b v_o, + forall chunk m1 b ofs v m2 chunk' b' ofs' v_b v_o, + store chunk m1 b ofs v = Some m2 -> load chunk' m2 b' ofs' = Some(Vptr v_b v_o) -> - (chunk = Mint32 /\ v = Vptr v_b v_o /\ chunk' = Mint32 /\ b' = b /\ ofs' = ofs) + (v = Vptr v_b v_o /\ compat_pointer_chunks chunk chunk' /\ b' = b /\ ofs' = ofs) \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs'). Proof. - intros. exploit load_result; eauto. rewrite store_mem_contents; simpl. - rewrite PMap.gsspec. destruct (peq b' b); auto. subst b'. intro DEC. + intros. + destruct (peq b' b); auto. subst b'. destruct (zle (ofs' + size_chunk chunk') ofs); auto. destruct (zle (ofs + size_chunk chunk) ofs'); auto. - destruct (size_chunk_nat_pos chunk) as [sz SZ]. - destruct (size_chunk_nat_pos chunk') as [sz' SZ']. - exploit decode_pointer_shape; eauto. intros [CHUNK' PSHAPE]. clear CHUNK'. - generalize (encode_val_shape chunk v). intro VSHAPE. - set (c := m1.(mem_contents)#b) in *. - set (c' := setN (encode_val chunk v) ofs c) in *. - destruct (zeq ofs ofs'). - -(* 1. ofs = ofs': must be same chunks and same value *) - subst ofs'. inv VSHAPE. - exploit decode_val_pointer_inv; eauto. intros [A B]. - subst chunk'. simpl in B. inv B. - generalize H4. unfold c'. rewrite <- H0. simpl. - rewrite setN_outside; try omega. rewrite ZMap.gss. intros. - exploit (encode_val_pointer_inv chunk v v_b v_o). - rewrite <- H0. subst mv1. eauto. intros [C [D E]]. - left; auto. - - destruct (zlt ofs ofs'). - -(* 2. ofs < ofs': - - ofs ofs' ofs+|chunk| - [-------------------] write - [-------------------] read - - The byte at ofs' satisfies memval_valid_cont (consequence of write). - For the read to return a pointer, it must satisfy ~memval_valid_cont. -*) - elimtype False. - assert (~memval_valid_cont (ZMap.get ofs' c')). - rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. auto. - assert (memval_valid_cont (ZMap.get ofs' c')). - inv VSHAPE. unfold c'. rewrite <- H1. simpl. - apply setN_property. auto. - assert (length mvl = sz). - generalize (encode_val_length chunk v). rewrite <- H1. rewrite SZ. - simpl; congruence. - rewrite H4. rewrite size_chunk_conv in *. omega. - contradiction. - -(* 3. ofs > ofs': - - ofs' ofs ofs'+|chunk'| - [-------------------] write - [----------------] read - - The byte at ofs satisfies memval_valid_first (consequence of write). - For the read to return a pointer, it must satisfy ~memval_valid_first. -*) - elimtype False. - assert (memval_valid_first (ZMap.get ofs c')). - inv VSHAPE. unfold c'. rewrite <- H0. simpl. - rewrite setN_outside. rewrite ZMap.gss. auto. omega. - assert (~memval_valid_first (ZMap.get ofs c')). - rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. - apply H4. apply getN_in. rewrite size_chunk_conv in *. - rewrite SZ' in *. rewrite inj_S in *. omega. - contradiction. + exploit load_store_overlap; eauto. + intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES). + inv DEC; try contradiction. + destruct CASES as [(A & B) | [(A & B) | (A & B)]]. +- (* Same offset *) + subst. inv ENC. + assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) + by (destruct chunk; auto || contradiction). + left; split. rewrite H3. + destruct H4 as [P|[P|P]]; subst chunk'; destruct v0; simpl in H3; congruence. + split. apply compat_pointer_chunks_true; auto. + auto. +- (* ofs' > ofs *) + inv ENC. + + exploit H10; eauto. intros (j & P & Q). inv P. congruence. + + exploit H8; eauto. intros (n & P); congruence. + + exploit H2; eauto. congruence. +- (* ofs' < ofs *) + exploit H7; eauto. intros (j & P & Q). subst mv1. inv ENC. congruence. Qed. -End STORE. - -Local Hint Resolve perm_store_1 perm_store_2: mem. -Local Hint Resolve store_valid_block_1 store_valid_block_2: mem. -Local Hint Resolve store_valid_access_1 store_valid_access_2 - store_valid_access_3: mem. - Theorem load_store_pointer_overlap: forall chunk m1 b ofs v_b v_o m2 chunk' ofs' v, store chunk m1 b ofs (Vptr v_b v_o) = Some m2 -> @@ -1251,102 +1261,37 @@ Theorem load_store_pointer_overlap: ofs + size_chunk chunk > ofs' -> v = Vundef. Proof. - intros. - exploit store_mem_contents; eauto. intro ST. - exploit load_result; eauto. intro LD. - rewrite LD; clear LD. -Opaque encode_val. - rewrite ST; simpl. - rewrite PMap.gss. - set (c := m1.(mem_contents)#b). - set (c' := setN (encode_val chunk (Vptr v_b v_o)) ofs c). - destruct (decode_val_shape chunk' (getN (size_chunk_nat chunk') ofs' c')) - as [OK | VSHAPE]. - apply getN_length. - exact OK. - elimtype False. - destruct (size_chunk_nat_pos chunk) as [sz SZ]. - destruct (size_chunk_nat_pos chunk') as [sz' SZ']. - assert (ENC: encode_val chunk (Vptr v_b v_o) = list_repeat (size_chunk_nat chunk) Undef - \/ pointer_encoding_shape (encode_val chunk (Vptr v_b v_o))). - destruct chunk; try (left; reflexivity). - right. apply encode_pointer_shape. - assert (GET: getN (size_chunk_nat chunk) ofs c' = encode_val chunk (Vptr v_b v_o)). - unfold c'. rewrite <- (encode_val_length chunk (Vptr v_b v_o)). - apply getN_setN_same. - destruct (zlt ofs ofs'). - -(* ofs < ofs': - - ofs ofs' ofs+|chunk| - [-------------------] write - [-------------------] read - - The byte at ofs' is Undef or not memval_valid_first (because write of pointer). - The byte at ofs' must be memval_valid_first and not Undef (otherwise load returns Vundef). -*) - assert (memval_valid_first (ZMap.get ofs' c') /\ ZMap.get ofs' c' <> Undef). - rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. auto. - assert (~memval_valid_first (ZMap.get ofs' c') \/ ZMap.get ofs' c' = Undef). - unfold c'. destruct ENC. - right. apply setN_property. rewrite H5. intros. eapply in_list_repeat; eauto. - rewrite encode_val_length. rewrite <- size_chunk_conv. omega. - left. revert H5. rewrite <- GET. rewrite SZ. simpl. intros. inv H5. - apply setN_property. apply H9. rewrite getN_length. - rewrite size_chunk_conv in H3. rewrite SZ in H3. rewrite inj_S in H3. omega. - intuition. - -(* ofs > ofs': - - ofs' ofs ofs'+|chunk'| - [-------------------] write - [----------------] read - - The byte at ofs is Undef or not memval_valid_cont (because write of pointer). - The byte at ofs must be memval_valid_cont and not Undef (otherwise load returns Vundef). -*) - assert (memval_valid_cont (ZMap.get ofs c') /\ ZMap.get ofs c' <> Undef). - rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. - apply H8. apply getN_in. rewrite size_chunk_conv in H2. - rewrite SZ' in H2. rewrite inj_S in H2. omega. - assert (~memval_valid_cont (ZMap.get ofs c') \/ ZMap.get ofs c' = Undef). - elim ENC. - rewrite <- GET. rewrite SZ. simpl. intros. right; congruence. - rewrite <- GET. rewrite SZ. simpl. intros. inv H5. auto. - intuition. + intros. + exploit load_store_overlap; eauto. + intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES). + destruct CASES as [(A & B) | [(A & B) | (A & B)]]. +- congruence. +- inv ENC. + + exploit H9; eauto. intros (j & P & Q). subst mv1'. inv DEC. congruence. auto. + + contradiction. + + exploit H5; eauto. intros; subst. inv DEC; auto. +- inv DEC. + + exploit H10; eauto. intros (j & P & Q). subst mv1. inv ENC. congruence. + + exploit H8; eauto. intros (n & P). subst mv1. inv ENC. contradiction. + + auto. Qed. Theorem load_store_pointer_mismatch: forall chunk m1 b ofs v_b v_o m2 chunk' v, store chunk m1 b ofs (Vptr v_b v_o) = Some m2 -> load chunk' m2 b ofs = Some v -> - chunk <> Mint32 \/ chunk' <> Mint32 -> + ~compat_pointer_chunks chunk chunk' -> v = Vundef. Proof. intros. - exploit store_mem_contents; eauto. intro ST. - exploit load_result; eauto. intro LD. - rewrite LD; clear LD. -Opaque encode_val. - rewrite ST; simpl. - rewrite PMap.gss. - set (c1 := m1.(mem_contents)#b). - set (e := encode_val chunk (Vptr v_b v_o)). - destruct (size_chunk_nat_pos chunk) as [sz SZ]. - destruct (size_chunk_nat_pos chunk') as [sz' SZ']. - assert (match e with - | Undef :: _ => True - | Pointer _ _ _ :: _ => chunk = Mint32 - | _ => False - end). -Transparent encode_val. - unfold e, encode_val. rewrite SZ. destruct chunk; simpl; auto. - destruct e as [ | e1 el]. contradiction. - rewrite SZ'. simpl. rewrite setN_outside. rewrite ZMap.gss. - destruct e1; try contradiction. - destruct chunk'; auto. - destruct chunk'; auto. intuition. - omega. + exploit load_store_overlap; eauto. + generalize (size_chunk_pos chunk'); omega. + generalize (size_chunk_pos chunk); omega. + intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES). + destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try omegaContradiction. + inv ENC; inv DEC; auto. +- elim H1. apply compat_pointer_chunks_true; auto. +- contradiction. Qed. Lemma store_similar_chunks: @@ -1403,16 +1348,6 @@ Theorem store_int16_sign_ext: store Mint16signed m b ofs (Vint n). Proof. intros. apply store_similar_chunks. apply encode_val_int16_sign_ext. auto. Qed. -Theorem store_float32_truncate: - forall m b ofs n, - store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) = - store Mfloat32 m b ofs (Vfloat n). -Proof. - intros. apply store_similar_chunks. simpl. decEq. - repeat rewrite encode_float32_eq. rewrite Float.bits_of_singleoffloat. auto. - auto. -Qed. - (* Theorem store_float64al32: forall m b ofs v m', diff --git a/common/Memtype.v b/common/Memtype.v index 37ab33c..1ab1cb7 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -310,7 +310,6 @@ Axiom load_cast: | Mint8unsigned => v = Val.zero_ext 8 v | Mint16signed => v = Val.sign_ext 16 v | Mint16unsigned => v = Val.zero_ext 16 v - | Mfloat32 => v = Val.singleoffloat v | _ => True end. @@ -443,6 +442,13 @@ Axiom load_store_other: (** Integrity of pointer values. *) +Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop := + match chunk1, chunk2 with + | (Mint32 | Many32), (Mint32 | Many32) => True + | Many64, Many64 => True + | _, _ => False + end. + Axiom load_store_pointer_overlap: forall chunk m1 b ofs v_b v_o m2 chunk' ofs' v, store chunk m1 b ofs (Vptr v_b v_o) = Some m2 -> @@ -455,13 +461,13 @@ Axiom load_store_pointer_mismatch: forall chunk m1 b ofs v_b v_o m2 chunk' v, store chunk m1 b ofs (Vptr v_b v_o) = Some m2 -> load chunk' m2 b ofs = Some v -> - chunk <> Mint32 \/ chunk' <> Mint32 -> + ~compat_pointer_chunks chunk chunk' -> v = Vundef. Axiom load_pointer_store: - forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> - forall chunk' b' ofs' v_b v_o, + forall chunk m1 b ofs v m2 chunk' b' ofs' v_b v_o, + store chunk m1 b ofs v = Some m2 -> load chunk' m2 b' ofs' = Some(Vptr v_b v_o) -> - (chunk = Mint32 /\ v = Vptr v_b v_o /\ chunk' = Mint32 /\ b' = b /\ ofs' = ofs) + (v = Vptr v_b v_o /\ compat_pointer_chunks chunk chunk' /\ b' = b /\ ofs' = ofs) \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs'). (** Load-store properties for [loadbytes]. *) @@ -500,10 +506,6 @@ Axiom store_int16_sign_ext: forall m b ofs n, store Mint16signed m b ofs (Vint (Int.sign_ext 16 n)) = store Mint16signed m b ofs (Vint n). -Axiom store_float32_truncate: - forall m b ofs n, - store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) = - store Mfloat32 m b ofs (Vfloat n). (** ** Properties of [storebytes]. *) diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 329c0c7..c0eab04 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -21,6 +21,8 @@ let name_of_type = function | Tfloat -> "float" | Tlong -> "long" | Tsingle -> "single" + | Tany32 -> "any32" + | Tany64 -> "any64" let name_of_chunk = function | Mint8signed -> "int8s" @@ -31,6 +33,8 @@ let name_of_chunk = function | Mint64 -> "int64" | Mfloat32 -> "float32" | Mfloat64 -> "float64" + | Many32 -> "any32" + | Many64 -> "any64" let name_of_external = function | EF_external(name, sg) -> sprintf "extern %S" (extern_atom name) diff --git a/common/Values.v b/common/Values.v index 5ac9f3e..a12fb63 100644 --- a/common/Values.v +++ b/common/Values.v @@ -38,6 +38,7 @@ Inductive val: Type := | Vint: int -> val | Vlong: int64 -> val | Vfloat: float -> val + | Vsingle: float32 -> val | Vptr: block -> int -> val. Definition Vzero: val := Vint Int.zero. @@ -55,14 +56,28 @@ Definition Vfalse: val := Vint Int.zero. Module Val. +Definition eq (x y: val): {x=y} + {x<>y}. +Proof. + decide equality. + apply Int.eq_dec. + apply Int64.eq_dec. + apply Float.eq_dec. + apply Float32.eq_dec. + apply Int.eq_dec. + apply eq_block. +Defined. +Global Opaque eq. + Definition has_type (v: val) (t: typ) : Prop := match v, t with | Vundef, _ => True | Vint _, Tint => True | Vlong _, Tlong => True | Vfloat _, Tfloat => True - | Vfloat f, Tsingle => Float.is_single f + | Vsingle _, Tsingle => True | Vptr _ _, Tint => True + | (Vint _ | Vptr _ _ | Vsingle _), Tany32 => True + | _, Tany64 => True | _, _ => False end. @@ -83,8 +98,8 @@ Lemma has_subtype: forall ty1 ty2 v, subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2. Proof. - intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac. - unfold has_type in *. destruct v; auto. + intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac; + unfold has_type in *; destruct v; auto. Qed. Lemma has_subtype_list: @@ -126,30 +141,66 @@ Definition absf (v: val) : val := | _ => Vundef end. +Definition negfs (v: val) : val := + match v with + | Vsingle f => Vsingle (Float32.neg f) + | _ => Vundef + end. + +Definition absfs (v: val) : val := + match v with + | Vsingle f => Vsingle (Float32.abs f) + | _ => Vundef + end. + Definition maketotal (ov: option val) : val := match ov with Some v => v | None => Vundef end. Definition intoffloat (v: val) : option val := match v with - | Vfloat f => option_map Vint (Float.intoffloat f) + | Vfloat f => option_map Vint (Float.to_int f) | _ => None end. Definition intuoffloat (v: val) : option val := match v with - | Vfloat f => option_map Vint (Float.intuoffloat f) + | Vfloat f => option_map Vint (Float.to_intu f) | _ => None end. Definition floatofint (v: val) : option val := match v with - | Vint n => Some (Vfloat (Float.floatofint n)) + | Vint n => Some (Vfloat (Float.of_int n)) | _ => None end. Definition floatofintu (v: val) : option val := match v with - | Vint n => Some (Vfloat (Float.floatofintu n)) + | Vint n => Some (Vfloat (Float.of_intu n)) + | _ => None + end. + +Definition intofsingle (v: val) : option val := + match v with + | Vsingle f => option_map Vint (Float32.to_int f) + | _ => None + end. + +Definition intuofsingle (v: val) : option val := + match v with + | Vsingle f => option_map Vint (Float32.to_intu f) + | _ => None + end. + +Definition singleofint (v: val) : option val := + match v with + | Vint n => Some (Vsingle (Float32.of_int n)) + | _ => None + end. + +Definition singleofintu (v: val) : option val := + match v with + | Vint n => Some (Vsingle (Float32.of_intu n)) | _ => None end. @@ -195,7 +246,13 @@ Definition sign_ext (nbits: Z) (v: val) : val := Definition singleoffloat (v: val) : val := match v with - | Vfloat f => Vfloat(Float.singleoffloat f) + | Vfloat f => Vsingle (Float.to_single f) + | _ => Vundef + end. + +Definition floatofsingle (v: val) : val := + match v with + | Vsingle f => Vfloat (Float.of_single f) | _ => Vundef end. @@ -394,6 +451,30 @@ Definition floatofwords (v1 v2: val) : val := | _, _ => Vundef end. +Definition addfs (v1 v2: val): val := + match v1, v2 with + | Vsingle f1, Vsingle f2 => Vsingle(Float32.add f1 f2) + | _, _ => Vundef + end. + +Definition subfs (v1 v2: val): val := + match v1, v2 with + | Vsingle f1, Vsingle f2 => Vsingle(Float32.sub f1 f2) + | _, _ => Vundef + end. + +Definition mulfs (v1 v2: val): val := + match v1, v2 with + | Vsingle f1, Vsingle f2 => Vsingle(Float32.mul f1 f2) + | _, _ => Vundef + end. + +Definition divfs (v1 v2: val): val := + match v1, v2 with + | Vsingle f1, Vsingle f2 => Vsingle(Float32.div f1 f2) + | _, _ => Vundef + end. + (** Operations on 64-bit integers *) Definition longofwords (v1 v2: val) : val := @@ -440,37 +521,49 @@ Definition longofintu (v: val) : val := Definition longoffloat (v: val) : option val := match v with - | Vfloat f => option_map Vlong (Float.longoffloat f) + | Vfloat f => option_map Vlong (Float.to_long f) | _ => None end. Definition longuoffloat (v: val) : option val := match v with - | Vfloat f => option_map Vlong (Float.longuoffloat f) + | Vfloat f => option_map Vlong (Float.to_longu f) + | _ => None + end. + +Definition longofsingle (v: val) : option val := + match v with + | Vsingle f => option_map Vlong (Float32.to_long f) + | _ => None + end. + +Definition longuofsingle (v: val) : option val := + match v with + | Vsingle f => option_map Vlong (Float32.to_longu f) | _ => None end. Definition floatoflong (v: val) : option val := match v with - | Vlong n => Some (Vfloat (Float.floatoflong n)) + | Vlong n => Some (Vfloat (Float.of_long n)) | _ => None end. Definition floatoflongu (v: val) : option val := match v with - | Vlong n => Some (Vfloat (Float.floatoflongu n)) + | Vlong n => Some (Vfloat (Float.of_longu n)) | _ => None end. Definition singleoflong (v: val) : option val := match v with - | Vlong n => Some (Vfloat (Float.singleoflong n)) + | Vlong n => Some (Vsingle (Float32.of_long n)) | _ => None end. Definition singleoflongu (v: val) : option val := match v with - | Vlong n => Some (Vfloat (Float.singleoflongu n)) + | Vlong n => Some (Vsingle (Float32.of_longu n)) | _ => None end. @@ -625,6 +718,12 @@ Definition cmpf_bool (c: comparison) (v1 v2: val): option bool := | _, _ => None end. +Definition cmpfs_bool (c: comparison) (v1 v2: val): option bool := + match v1, v2 with + | Vsingle f1, Vsingle f2 => Some (Float32.cmp c f1 f2) + | _, _ => None + end. + Definition cmpl_bool (c: comparison) (v1 v2: val): option bool := match v1, v2 with | Vlong n1, Vlong n2 => Some (Int64.cmp c n1 n2) @@ -649,6 +748,9 @@ Definition cmpu (c: comparison) (v1 v2: val): val := Definition cmpf (c: comparison) (v1 v2: val): val := of_optbool (cmpf_bool c v1 v2). +Definition cmpfs (c: comparison) (v1 v2: val): val := + of_optbool (cmpfs_bool c v1 v2). + Definition cmpl (c: comparison) (v1 v2: val): option val := option_map of_bool (cmpl_bool c v1 v2). @@ -681,22 +783,23 @@ Definition load_result (chunk: memory_chunk) (v: val) := | Mint32, Vint n => Vint n | Mint32, Vptr b ofs => Vptr b ofs | Mint64, Vlong n => Vlong n - | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f) + | Mfloat32, Vsingle f => Vsingle f | Mfloat64, Vfloat f => Vfloat f + | Many32, (Vint _ | Vptr _ _ | Vsingle _) => v + | Many64, _ => v | _, _ => Vundef end. Lemma load_result_type: forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk). Proof. - intros. destruct chunk; destruct v; simpl; auto. apply Float.singleoffloat_is_single. + intros. destruct chunk; destruct v; simpl; auto. Qed. Lemma load_result_same: forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v. Proof. unfold has_type; intros. destruct v; destruct ty; try contradiction; auto. - simpl. rewrite Float.singleoffloat_of_single; auto. Qed. (** Theorems on arithmetic operations. *) @@ -1388,6 +1491,8 @@ Inductive val_inject (mi: meminj): val -> val -> Prop := forall i, val_inject mi (Vlong i) (Vlong i) | val_inject_float: forall f, val_inject mi (Vfloat f) (Vfloat f) + | val_inject_single: + forall f, val_inject mi (Vsingle f) (Vsingle f) | val_inject_ptr: forall b1 ofs1 b2 ofs2 delta, mi b1 = Some (b2, delta) -> -- cgit v1.2.3