From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 39 +++++--- common/Errors.v | 48 +++------- common/Events.v | 197 ++++++++++++++++++++++++++++++++++++++- common/Globalenvs.v | 6 ++ common/Memdata.v | 164 +++++++++++++++++++++++++++++++- common/Memory.v | 92 ++++++++++++++++++ common/PrintAST.ml | 3 +- common/Values.v | 262 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 8 files changed, 741 insertions(+), 70 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 8595b95..1f7f7d3 100644 --- a/common/AST.v +++ b/common/AST.v @@ -17,6 +17,7 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import Coqlib. +Require String. Require Import Errors. Require Import Integers. Require Import Floats. @@ -32,16 +33,19 @@ Definition ident := positive. Definition ident_eq := peq. -(** The intermediate languages are weakly typed, using only two types: - [Tint] for integers and pointers, and [Tfloat] for floating-point - numbers. *) +Parameter ident_of_string : String.string -> ident. + +(** The intermediate languages are weakly typed, using only three + types: [Tint] for 32-bit integers and pointers, [Tfloat] for 64-bit + floating-point numbers, [Tlong] for 64-bit integers. *) Inductive typ : Type := - | Tint : typ - | Tfloat : typ. + | Tint + | Tfloat + | Tlong. Definition typesize (ty: typ) : Z := - match ty with Tint => 4 | Tfloat => 8 end. + match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 end. Lemma typesize_pos: forall ty, typesize ty > 0. Proof. destruct ty; simpl; omega. Qed. @@ -54,6 +58,9 @@ Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}. Proof. decide equality. apply typ_eq. Defined. Global Opaque opt_typ_eq. +Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} + := list_eq_dec typ_eq. + (** Additionally, function definitions and function calls are annotated by function signatures indicating the number and types of arguments, as well as the type of the returned value if any. These signatures @@ -76,14 +83,15 @@ Definition proj_sig_res (s: signature) : typ := chunk of memory being accessed. *) Inductive memory_chunk : Type := - | Mint8signed : memory_chunk (**r 8-bit signed integer *) - | Mint8unsigned : memory_chunk (**r 8-bit unsigned integer *) - | Mint16signed : memory_chunk (**r 16-bit signed integer *) - | Mint16unsigned : memory_chunk (**r 16-bit unsigned integer *) - | Mint32 : memory_chunk (**r 32-bit integer, or pointer *) - | Mfloat32 : memory_chunk (**r 32-bit single-precision float *) - | Mfloat64 : memory_chunk (**r 64-bit double-precision float *) - | Mfloat64al32 : memory_chunk. (**r 64-bit double-precision float, 4-aligned *) + | Mint8signed (**r 8-bit signed integer *) + | Mint8unsigned (**r 8-bit unsigned integer *) + | Mint16signed (**r 16-bit signed integer *) + | Mint16unsigned (**r 16-bit unsigned integer *) + | 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 *) + | Mfloat64al32. (**r 64-bit double-precision float, 4-aligned *) (** The type (integer/pointer or float) of a chunk. *) @@ -94,6 +102,7 @@ Definition type_of_chunk (c: memory_chunk) : typ := | Mint16signed => Tint | Mint16unsigned => Tint | Mint32 => Tint + | Mint64 => Tlong | Mfloat32 => Tfloat | Mfloat64 => Tfloat | Mfloat64al32 => Tfloat @@ -105,6 +114,7 @@ Inductive init_data: Type := | Init_int8: int -> init_data | Init_int16: int -> init_data | Init_int32: int -> init_data + | Init_int64: int64 -> init_data | Init_float32: float -> init_data | Init_float64: float -> init_data | Init_space: Z -> init_data @@ -549,4 +559,3 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := end. End TRANSF_PARTIAL_FUNDEF. - diff --git a/common/Errors.v b/common/Errors.v index 6b863a0..78e1199 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -96,30 +96,11 @@ Qed. (** Assertions *) -Definition assertion (b: bool) : res unit := - if b then OK tt else Error(msg "Assertion failed"). +Definition assertion_failed {A: Type} : res A := Error(msg "Assertion failed"). -Remark assertion_inversion: - forall b x, assertion b = OK x -> b = true. -Proof. - unfold assertion; intros. destruct b; inv H; auto. -Qed. - -Remark assertion_inversion_1: - forall (P Q: Prop) (a: {P}+{Q}) x, - assertion (proj_sumbool a) = OK x -> P. -Proof. - intros. exploit assertion_inversion; eauto. - unfold proj_sumbool. destruct a. auto. congruence. -Qed. - -Remark assertion_inversion_2: - forall (P Q: Prop) (a: {P}+{Q}) x, - assertion (negb(proj_sumbool a)) = OK x -> Q. -Proof. - intros. exploit assertion_inversion; eauto. - unfold proj_sumbool. destruct a; simpl. congruence. auto. -Qed. +Notation "'assertion' A ; B" := (if A then B else assertion_failed) + (at level 200, A at level 100, B at level 200) + : error_monad_scope. (** This is the familiar monadic map iterator. *) @@ -180,26 +161,19 @@ Ltac monadInv1 H := destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]]; clear H; try (monadInv1 EQ2))))) - | (assertion (negb (proj_sumbool ?a)) = OK ?X) => - let A := fresh "A" in (generalize (assertion_inversion_2 _ H); intro A); - clear H - | (assertion (proj_sumbool ?a) = OK ?X) => - let A := fresh "A" in (generalize (assertion_inversion_1 _ H); intro A); - clear H - | (assertion ?b = OK ?X) => - let A := fresh "A" in (generalize (assertion_inversion _ H); intro A); - clear H + | (match ?X with left _ => _ | right _ => assertion_failed end = OK _) => + destruct X; [try (monadInv1 H) | discriminate] + | (match (negb ?X) with true => _ | false => assertion_failed end = OK _) => + destruct X as [] eqn:?; [discriminate | try (monadInv1 H)] + | (match ?X with true => _ | false => assertion_failed end = OK _) => + destruct X as [] eqn:?; [try (monadInv1 H) | discriminate] | (mmap ?F ?L = OK ?M) => generalize (mmap_inversion F L H); intro end. Ltac monadInv H := + monadInv1 H || match type of H with - | (OK _ = OK _) => monadInv1 H - | (Error _ = OK _) => monadInv1 H - | (bind ?F ?G = OK ?X) => monadInv1 H - | (bind2 ?F ?G = OK ?X) => monadInv1 H - | (assertion _ = OK _) => monadInv1 H | (?F _ _ _ _ _ _ _ _ = OK _) => ((progress simpl in H) || unfold F in H); monadInv1 H | (?F _ _ _ _ _ _ _ = OK _) => diff --git a/common/Events.v b/common/Events.v index e310bfe..f342799 100644 --- a/common/Events.v +++ b/common/Events.v @@ -55,6 +55,7 @@ Require Import Globalenvs. Inductive eventval: Type := | EVint: int -> eventval + | EVlong: int64 -> eventval | EVfloat: float -> eventval | EVptr_global: ident -> int -> eventval. @@ -267,6 +268,8 @@ Variable ge: Genv.t F V. Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_int: forall i, eventval_match (EVint i) Tint (Vint i) + | ev_match_long: forall i, + eventval_match (EVlong i) Tlong (Vlong i) | ev_match_float: forall f, eventval_match (EVfloat f) Tfloat (Vfloat f) | ev_match_ptr: forall id b ofs, @@ -327,7 +330,7 @@ Lemma eventval_match_inject: forall ev ty v1 v2, eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2. Proof. - intros. inv H; inv H0. constructor. constructor. + intros. inv H; inv H0; try constructor. destruct glob_pres as [A [B C]]. exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ. rewrite Int.add_zero. econstructor; eauto. @@ -337,7 +340,7 @@ Lemma eventval_match_inject_2: forall ev ty v, eventval_match ev ty v -> val_inject f v v. Proof. - induction 1. constructor. constructor. + induction 1; auto. destruct glob_pres as [A [B C]]. exploit A; eauto. intro EQ. econstructor; eauto. rewrite Int.add_zero; auto. @@ -379,6 +382,7 @@ Qed. Definition eventval_valid (ev: eventval) : Prop := match ev with | EVint _ => True + | EVlong _ => True | EVfloat _ => True | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b end. @@ -386,6 +390,7 @@ Definition eventval_valid (ev: eventval) : Prop := Definition eventval_type (ev: eventval) : typ := match ev with | EVint _ => Tint + | EVlong _ => Tlong | EVfloat _ => Tfloat | EVptr_global id ofs => Tint end. @@ -396,6 +401,7 @@ Lemma eventval_valid_match: Proof. intros. subst ty. destruct ev; simpl in *. exists (Vint i); constructor. + exists (Vlong i); constructor. exists (Vfloat f0); constructor. destruct H as [b A]. exists (Vptr b i0); constructor; auto. Qed. @@ -1693,3 +1699,190 @@ Proof. intros. exploit external_call_determ. eexact H. eexact H0. intuition. Qed. +(** Late in the back-end, calling conventions for external calls change: + arguments and results of type [Tlong] are passed as two integers. + We now wrap [external_call] to adapt to this convention. *) + +Fixpoint decode_longs (tyl: list typ) (vl: list val) : list val := + match tyl with + | nil => nil + | Tlong :: tys => + match vl with + | v1 :: v2 :: vs => Val.longofwords v1 v2 :: decode_longs tys vs + | _ => nil + end + | ty :: tys => + match vl with + | v1 :: vs => v1 :: decode_longs tys vs + | _ => nil + end + end. + +Definition encode_long (oty: option typ) (v: val) : list val := + match oty with + | Some Tlong => Val.hiword v :: Val.loword v :: nil + | _ => v :: nil + end. + +Definition proj_sig_res' (s: signature) : list typ := + match s.(sig_res) with + | Some Tlong => Tint :: Tint :: nil + | Some ty => ty :: nil + | None => Tint :: nil + end. + +Inductive external_call' + (ef: external_function) (F V: Type) (ge: Genv.t F V) + (vargs: list val) (m1: mem) (t: trace) (vres: list val) (m2: mem) : Prop := + external_call'_intro: forall v, + external_call ef ge (decode_longs (sig_args (ef_sig ef)) vargs) m1 t v m2 -> + vres = encode_long (sig_res (ef_sig ef)) v -> + external_call' ef ge vargs m1 t vres m2. + +Lemma decode_longs_lessdef: + forall tyl vl1 vl2, Val.lessdef_list vl1 vl2 -> Val.lessdef_list (decode_longs tyl vl1) (decode_longs tyl vl2). +Proof. + induction tyl; simpl; intros. + auto. + destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma decode_longs_inject: + forall f tyl vl1 vl2, val_list_inject f vl1 vl2 -> val_list_inject f (decode_longs tyl vl1) (decode_longs tyl vl2). +Proof. + induction tyl; simpl; intros. + auto. + destruct a; inv H; auto. inv H1; auto. constructor; auto. apply val_longofwords_inject; auto. +Qed. + +Lemma encode_long_lessdef: + forall oty v1 v2, Val.lessdef v1 v2 -> Val.lessdef_list (encode_long oty v1) (encode_long oty v2). +Proof. + intros. destruct oty as [[]|]; simpl; auto. + constructor. apply Val.hiword_lessdef; auto. constructor. apply Val.loword_lessdef; auto. auto. +Qed. + +Lemma encode_long_inject: + forall f oty v1 v2, val_inject f v1 v2 -> val_list_inject f (encode_long oty v1) (encode_long oty v2). +Proof. + intros. destruct oty as [[]|]; simpl; auto. + constructor. apply val_hiword_inject; auto. constructor. apply val_loword_inject; auto. auto. +Qed. + +Lemma encode_long_has_type: + forall v sg, + Val.has_type v (proj_sig_res sg) -> + Val.has_type_list (encode_long (sig_res sg) v) (proj_sig_res' sg). +Proof. + unfold proj_sig_res, proj_sig_res', encode_long; intros. + destruct (sig_res sg) as [[] | ]; simpl; auto. + destruct v; simpl; auto. +Qed. + +Lemma external_call_well_typed': + forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2, + external_call' ef ge vargs m1 t vres m2 -> + Val.has_type_list vres (proj_sig_res' (ef_sig ef)). +Proof. + intros. inv H. apply encode_long_has_type. + eapply external_call_well_typed; eauto. +Qed. + +Lemma external_call_symbols_preserved': + forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, + external_call' ef ge1 vargs m1 t vres m2 -> + (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> + external_call' ef ge2 vargs m1 t vres m2. +Proof. + intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto. +Qed. + +Lemma external_call_valid_block': + forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2 b, + external_call' ef ge vargs m1 t vres m2 -> + Mem.valid_block m1 b -> Mem.valid_block m2 b. +Proof. + intros. inv H. eapply external_call_valid_block; eauto. +Qed. + +Lemma external_call_mem_extends': + forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2 m1' vargs', + external_call' ef ge vargs m1 t vres m2 -> + Mem.extends m1 m1' -> + Val.lessdef_list vargs vargs' -> + exists vres' m2', + external_call' ef ge vargs' m1' t vres' m2' + /\ Val.lessdef_list vres vres' + /\ Mem.extends m2 m2' + /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'. +Proof. + intros. inv H. + exploit external_call_mem_extends; eauto. + eapply decode_longs_lessdef; eauto. + intros (v' & m2' & A & B & C & D). + exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition. + econstructor; eauto. + eapply encode_long_lessdef; eauto. +Qed. + +Lemma external_call_mem_inject': + forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', + meminj_preserves_globals ge f -> + external_call' ef ge vargs m1 t vres m2 -> + Mem.inject f m1 m1' -> + val_list_inject f vargs vargs' -> + exists f' vres' m2', + external_call' ef ge vargs' m1' t vres' m2' + /\ val_list_inject f' vres vres' + /\ Mem.inject f' m2 m2' + /\ mem_unchanged_on (loc_unmapped f) m1 m2 + /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ inject_incr f f' + /\ inject_separated f f' m1 m1'. +Proof. + intros. inv H0. + exploit external_call_mem_inject; eauto. + eapply decode_longs_inject; eauto. + intros (f' & v' & m2' & A & B & C & D & E & P & Q). + exists f'; exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition. + econstructor; eauto. + apply encode_long_inject; auto. +Qed. + +Lemma external_call_determ': + forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2, + external_call' ef ge vargs m t1 vres1 m1 -> + external_call' ef ge vargs m t2 vres2 m2 -> + match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2). +Proof. + intros. inv H; inv H0. exploit external_call_determ. eexact H1. eexact H. + intros [A B]. split. auto. intros. destruct B as [C D]; auto. subst. auto. +Qed. + +Lemma external_call_match_traces': + forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2, + external_call' ef ge vargs m t1 vres1 m1 -> + external_call' ef ge vargs m t2 vres2 m2 -> + match_traces ge t1 t2. +Proof. + intros. inv H; inv H0. eapply external_call_match_traces; eauto. +Qed. + +Lemma external_call_deterministic': + forall ef (F V : Type) (ge : Genv.t F V) vargs m t vres1 m1 vres2 m2, + external_call' ef ge vargs m t vres1 m1 -> + external_call' ef ge vargs m t vres2 m2 -> + vres1 = vres2 /\ m1 = m2. +Proof. + intros. inv H; inv H0. + exploit external_call_deterministic. eexact H1. eexact H. intros [A B]. + split; congruence. +Qed. + + + + + + + diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 3d9f499..a082819 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -491,6 +491,7 @@ Definition init_data_size (i: init_data) : Z := | Init_int8 _ => 1 | Init_int16 _ => 2 | Init_int32 _ => 4 + | Init_int64 _ => 8 | Init_float32 _ => 4 | Init_float64 _ => 8 | Init_addrof _ _ => 4 @@ -508,6 +509,7 @@ Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option m | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n) | 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_float64 n => Mem.store Mfloat64 m b p (Vfloat n) | Init_addrof symb ofs => @@ -761,6 +763,9 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s | Init_int32 n :: il' => Mem.load Mint32 m b p = Some(Vint n) /\ load_store_init_data m b (p + 4) il' + | Init_int64 n :: il' => + 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)) /\ load_store_init_data m b (p + 4) il' @@ -795,6 +800,7 @@ Proof. eapply (A Mint8unsigned (Vint i)); eauto. 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 Mfloat64 (Vfloat f)); eauto. destruct (find_symbol ge i); try congruence. exists b0; split; auto. diff --git a/common/Memdata.v b/common/Memdata.v index 3de5f39..c62ba99 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -35,6 +35,7 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Mint16signed => 2 | Mint16unsigned => 2 | Mint32 => 4 + | Mint64 => 8 | Mfloat32 => 4 | Mfloat64 => 8 | Mfloat64al32 => 8 @@ -82,6 +83,7 @@ Definition align_chunk (chunk: memory_chunk) : Z := | Mint16signed => 2 | Mint16unsigned => 2 | Mint32 => 4 + | Mint64 => 8 | Mfloat32 => 4 | Mfloat64 => 8 | Mfloat64al32 => 4 @@ -96,7 +98,7 @@ Qed. Lemma align_size_chunk_divides: forall chunk, (align_chunk chunk | size_chunk chunk). Proof. - intros. destruct chunk; simpl; try apply Zdivide_refl. exists 2; auto. + intros. destruct chunk; simpl; try apply Zdivide_refl; exists 2; auto. Qed. Lemma align_le_divides: @@ -340,6 +342,7 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval := | 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 + | 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 | Mfloat64al32) => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n))) | _, _ => list_repeat (size_chunk_nat chunk) Undef @@ -354,6 +357,7 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := | Mint16signed => Vint(Int.sign_ext 16 (Int.repr (decode_int bl))) | 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 | Mfloat64al32 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl))) end @@ -394,14 +398,19 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : | 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, (Mfloat32 | Mfloat64 | Mfloat64al32), _ => v2 = Vundef + | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Mfloat64al32), _ => v2 = Vundef | Vint n, _, _ => True (**r nothing meaningful to say about v2 *) | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs | Vptr b ofs, _, _ => v2 = Vundef + | Vlong n, Mint64, Mint64 => v2 = Vlong n + | Vlong n, Mint64, (Mfloat64 | Mfloat64al32) => v2 = Vfloat(Float.double_of_bits n) + | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64|Mfloat64al32), _ => 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 | Mfloat64al32), (Mfloat64 | Mfloat64al32) => v2 = Vfloat f - | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32), _ => v2 = Vundef + | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64), _ => v2 = Vundef + | Vfloat f, (Mfloat64 | Mfloat64al32), Mint64 => v2 = Vlong(Float.bits_of_double f) | Vfloat f, _, _ => True (* nothing interesting to say about v2 *) end. @@ -419,7 +428,6 @@ Opaque inj_pointer. intros. destruct v; destruct chunk1; simpl; try (apply decode_val_undef); destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes). - (* int-int *) 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. @@ -430,10 +438,15 @@ Opaque inj_pointer. rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega. rewrite decode_encode_int_4. auto. rewrite decode_encode_int_4. auto. + rewrite decode_encode_int_8. 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_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. rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. + rewrite decode_encode_int_8. auto. rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. 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. @@ -815,6 +828,7 @@ 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)). @@ -845,3 +859,143 @@ Proof. constructor. Qed. +(** * Breaking 64-bit memory accesses into two 32-bit accesses *) + +Lemma int_of_bytes_append: + forall l2 l1, + int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z_of_nat (length l1) * 8). +Proof. + induction l1; simpl int_of_bytes; intros. + simpl. ring. + simpl length. rewrite inj_S. + replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z_of_nat (length l1) * 8 + 8) by omega. + rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring. + omega. omega. +Qed. + +Lemma int_of_bytes_range: + forall l, 0 <= int_of_bytes l < two_p (Z_of_nat (length l) * 8). +Proof. + induction l; intros. + simpl. omega. + simpl length. rewrite inj_S. + replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega. + rewrite two_p_is_exp. change (two_p 8) with 256. + simpl int_of_bytes. generalize (Byte.unsigned_range a). + change Byte.modulus with 256. omega. + omega. omega. +Qed. + +Lemma length_proj_bytes: + forall l b, proj_bytes l = Some b -> length b = length l. +Proof. + induction l; simpl; intros. + inv H; auto. + destruct a; try discriminate. + destruct (proj_bytes l) eqn:E; inv H. + simpl. f_equal. auto. +Qed. + +Lemma proj_bytes_append: + forall l2 l1, + proj_bytes (l1 ++ l2) = + match proj_bytes l1, proj_bytes l2 with + | Some b1, Some b2 => Some (b1 ++ b2) + | _, _ => None + end. +Proof. + induction l1; simpl. + destruct (proj_bytes l2); auto. + destruct a; auto. rewrite IHl1. + destruct (proj_bytes l1); auto. destruct (proj_bytes l2); auto. +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 big_endian then l1 else l2)) + (decode_val Mint32 (if 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. + 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. + unfold decode_int, rev_if_be. destruct big_endian; rewrite B1; rewrite B2. + + rewrite <- (rev_length b1) in L1. + rewrite <- (rev_length b2) in L2. + rewrite rev_app_distr. + set (b1' := rev b1) in *; set (b2' := rev b2) in *. + unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal. + rewrite !UR by auto. rewrite int_of_bytes_append. + rewrite L2. change (Z.of_nat 4 * 8) with 32. ring. + + 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 big_endian; rewrite B1; rewrite B2; auto. +- destruct big_endian; rewrite B1; rewrite B2; auto. +- destruct big_endian; rewrite B1; rewrite B2; auto. +Qed. + +Lemma bytes_of_int_append: + forall n2 x2 n1 x1, + 0 <= x1 < two_p (Z_of_nat n1 * 8) -> + bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z_of_nat n1 * 8)) = + bytes_of_int n1 x1 ++ bytes_of_int n2 x2. +Proof. + induction n1; intros. +- simpl in *. f_equal. omega. +- assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256). + { + rewrite inj_S. change 256 with (two_p 8). rewrite <- two_p_is_exp. + f_equal. omega. omega. omega. + } + rewrite E in *. simpl. f_equal. + apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)). + change Byte.modulus with 256. ring. + rewrite Zmult_assoc. rewrite Z_div_plus. apply IHn1. + apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega. + assumption. omega. +Qed. + +Lemma bytes_of_int64: + forall i, + bytes_of_int 8 (Int64.unsigned i) = + bytes_of_int 4 (Int.unsigned (Int64.loword i)) ++ bytes_of_int 4 (Int.unsigned (Int64.hiword i)). +Proof. + intros. transitivity (bytes_of_int (4 + 4) (Int64.unsigned (Int64.ofwords (Int64.hiword i) (Int64.loword i)))). + f_equal. f_equal. rewrite Int64.ofwords_recompose. auto. + rewrite Int64.ofwords_add'. + change 32 with (Z_of_nat 4 * 8). + rewrite Zplus_comm. apply bytes_of_int_append. apply Int.unsigned_range. +Qed. + +Lemma encode_val_int64: + forall v, + encode_val Mint64 v = + encode_val Mint32 (if big_endian then Val.hiword v else Val.loword v) + ++ encode_val Mint32 (if big_endian then Val.loword v else Val.hiword v). +Proof. + intros. destruct v; destruct big_endian eqn:BI; try reflexivity; + unfold Val.loword, Val.hiword, encode_val. + unfold inj_bytes. rewrite <- map_app. f_equal. + unfold encode_int, rev_if_be. rewrite BI. rewrite <- rev_app_distr. f_equal. + apply bytes_of_int64. + unfold inj_bytes. rewrite <- map_app. f_equal. + unfold encode_int, rev_if_be. rewrite BI. + apply bytes_of_int64. +Qed. diff --git a/common/Memory.v b/common/Memory.v index 12a0f45..54d50f7 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -862,6 +862,60 @@ Proof. rewrite inj_S. omega. Qed. +Theorem load_int64_split: + forall m b ofs v, + load Mint64 m b ofs = Some v -> + exists v1 v2, + load Mint32 m b ofs = Some (if big_endian then v1 else v2) + /\ load Mint32 m b (ofs + 4) = Some (if big_endian then v2 else v1) + /\ v = Val.longofwords v1 v2. +Proof. + intros. + exploit load_valid_access; eauto. intros [A B]. simpl in *. + exploit load_loadbytes. eexact H. simpl. intros [bytes [LB EQ]]. + change 8 with (4 + 4) in LB. + exploit loadbytes_split. eexact LB. omega. omega. + intros (bytes1 & bytes2 & LB1 & LB2 & APP). + change 4 with (size_chunk Mint32) in LB1. + exploit loadbytes_load. eexact LB1. + simpl. apply Zdivides_trans with 8; auto. exists 2; auto. + intros L1. + change 4 with (size_chunk Mint32) in LB2. + exploit loadbytes_load. eexact LB2. + simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. + intros L2. + exists (decode_val Mint32 (if big_endian then bytes1 else bytes2)); + exists (decode_val Mint32 (if big_endian then bytes2 else bytes1)). + split. destruct big_endian; auto. + split. destruct big_endian; auto. + rewrite EQ. rewrite APP. apply decode_val_int64. + erewrite loadbytes_length; eauto. reflexivity. + erewrite loadbytes_length; eauto. reflexivity. +Qed. + +Theorem loadv_int64_split: + forall m a v, + loadv Mint64 m a = Some v -> + exists v1 v2, + loadv Mint32 m a = Some (if big_endian then v1 else v2) + /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if big_endian then v2 else v1) + /\ 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). + assert (NV: Int.unsigned (Int.add i (Int.repr 4)) = Int.unsigned i + 4). + rewrite Int.add_unsigned. apply Int.unsigned_repr. + exploit load_valid_access. eexact H. intros [P Q]. simpl in Q. + exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8). + omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. + unfold Int.max_unsigned. omega. + exists v1; exists v2. +Opaque Int.repr. + split. auto. + split. simpl. rewrite NV. auto. + auto. +Qed. + (** ** Properties related to [store] *) Theorem valid_access_store: @@ -1581,6 +1635,44 @@ Proof. exists m1; split; auto. Qed. +Theorem store_int64_split: + forall m b ofs v m', + store Mint64 m b ofs v = Some m' -> + exists m1, + store Mint32 m b ofs (if big_endian then Val.hiword v else Val.loword v) = Some m1 + /\ store Mint32 m1 b (ofs + 4) (if big_endian then Val.loword v else Val.hiword v) = Some m'. +Proof. + intros. + exploit store_valid_access_3; eauto. intros [A B]. simpl in *. + exploit store_storebytes. eexact H. intros SB. + rewrite encode_val_int64 in SB. + exploit storebytes_split. eexact SB. intros [m1 [SB1 SB2]]. + rewrite encode_val_length in SB2. simpl in SB2. + exists m1; split. + apply storebytes_store. exact SB1. + simpl. apply Zdivides_trans with 8; auto. exists 2; auto. + apply storebytes_store. exact SB2. + simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. +Qed. + +Theorem storev_int64_split: + forall m a v m', + storev Mint64 m a v = Some m' -> + exists m1, + storev Mint32 m a (if big_endian then Val.hiword v else Val.loword v) = Some m1 + /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if big_endian then Val.loword v else Val.hiword v) = Some m'. +Proof. + intros. destruct a; simpl in H; try discriminate. + exploit store_int64_split; eauto. intros [m1 [A B]]. + exists m1; split. + exact A. + unfold storev, Val.add. rewrite Int.add_unsigned. rewrite Int.unsigned_repr. exact B. + exploit store_valid_access_3. eexact H. intros [P Q]. simpl in Q. + exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8). + omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. + change (Int.unsigned (Int.repr 4)) with 4. unfold Int.max_unsigned. omega. +Qed. + (** ** Properties related to [alloc]. *) Section ALLOC. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 7f2ed3f..c18b09d 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -16,7 +16,7 @@ open Printf open Camlcoq open AST -let name_of_type = function Tint -> "int" | Tfloat -> "float" +let name_of_type = function Tint -> "int" | Tfloat -> "float" | Tlong -> "long" let name_of_chunk = function | Mint8signed -> "int8signed" @@ -24,6 +24,7 @@ let name_of_chunk = function | Mint16signed -> "int16signed" | Mint16unsigned -> "int16unsigned" | Mint32 -> "int32" + | Mint64 -> "int64" | Mfloat32 -> "float32" | Mfloat64 -> "float64" | Mfloat64al32 -> "float64al32" diff --git a/common/Values.v b/common/Values.v index f629628..f917e0b 100644 --- a/common/Values.v +++ b/common/Values.v @@ -36,6 +36,7 @@ Definition eq_block := zeq. Inductive val: Type := | Vundef: val | Vint: int -> val + | Vlong: int64 -> val | Vfloat: float -> val | Vptr: block -> int -> val. @@ -58,6 +59,7 @@ Definition has_type (v: val) (t: typ) : Prop := match v, t with | Vundef, _ => True | Vint _, Tint => True + | Vlong _, Tlong => True | Vfloat _, Tfloat => True | Vptr _ _, Tint => True | _, _ => False @@ -70,6 +72,12 @@ Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop := | _, _ => False end. +Definition has_opttype (v: val) (ot: option typ) : Prop := + match ot with + | None => v = Vundef + | Some t => has_type v t + end. + (** Truth values. Pointers and non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. [Vundef] and floats are neither true nor false. *) @@ -127,12 +135,6 @@ Definition floatofintu (v: val) : option val := | _ => None end. -Definition floatofwords (v1 v2: val) : val := - match v1, v2 with - | Vint n1, Vint n2 => Vfloat (Float.from_words n1 n2) - | _, _ => Vundef - end. - Definition negint (v: val) : val := match v with | Vint n => Vint (Int.neg n) @@ -344,6 +346,183 @@ Definition divf (v1 v2: val): val := | _, _ => Vundef end. +Definition floatofwords (v1 v2: val) : val := + match v1, v2 with + | Vint n1, Vint n2 => Vfloat (Float.from_words n1 n2) + | _, _ => Vundef + end. + +(** Operations on 64-bit integers *) + +Definition longofwords (v1 v2: val) : val := + match v1, v2 with + | Vint n1, Vint n2 => Vlong (Int64.ofwords n1 n2) + | _, _ => Vundef + end. + +Definition loword (v: val) : val := + match v with + | Vlong n => Vint (Int64.loword n) + | _ => Vundef + end. + +Definition hiword (v: val) : val := + match v with + | Vlong n => Vint (Int64.hiword n) + | _ => Vundef + end. + +Definition negl (v: val) : val := + match v with + | Vlong n => Vlong (Int64.neg n) + | _ => Vundef + end. + +Definition notl (v: val) : val := + match v with + | Vlong n => Vlong (Int64.not n) + | _ => Vundef + end. + +Definition longofint (v: val) : val := + match v with + | Vint n => Vlong (Int64.repr (Int.signed n)) + | _ => Vundef + end. + +Definition longofintu (v: val) : val := + match v with + | Vint n => Vlong (Int64.repr (Int.unsigned n)) + | _ => Vundef + end. + +Definition longoffloat (v: val) : option val := + match v with + | Vfloat f => option_map Vlong (Float.longoffloat f) + | _ => None + end. + +Definition longuoffloat (v: val) : option val := + match v with + | Vfloat f => option_map Vlong (Float.longuoffloat f) + | _ => None + end. + +Definition floatoflong (v: val) : option val := + match v with + | Vlong n => Some (Vfloat (Float.floatoflong n)) + | _ => None + end. + +Definition floatoflongu (v: val) : option val := + match v with + | Vlong n => Some (Vfloat (Float.floatoflongu n)) + | _ => None + end. + +Definition addl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vlong n2 => Vlong(Int64.add n1 n2) + | _, _ => Vundef + end. + +Definition subl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vlong n2 => Vlong(Int64.sub n1 n2) + | _, _ => Vundef + end. + +Definition mull (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vlong n2 => Vlong(Int64.mul n1 n2) + | _, _ => Vundef + end. + +Definition mull' (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vlong(Int64.mul' n1 n2) + | _, _ => Vundef + end. + +Definition divls (v1 v2: val): option val := + match v1, v2 with + | Vlong n1, Vlong n2 => + if Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone + then None + else Some(Vlong(Int64.divs n1 n2)) + | _, _ => None + end. + +Definition modls (v1 v2: val): option val := + match v1, v2 with + | Vlong n1, Vlong n2 => + if Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone + then None + else Some(Vlong(Int64.mods n1 n2)) + | _, _ => None + end. + +Definition divlu (v1 v2: val): option val := + match v1, v2 with + | Vlong n1, Vlong n2 => + if Int64.eq n2 Int64.zero then None else Some(Vlong(Int64.divu n1 n2)) + | _, _ => None + end. + +Definition modlu (v1 v2: val): option val := + match v1, v2 with + | Vlong n1, Vlong n2 => + if Int64.eq n2 Int64.zero then None else Some(Vlong(Int64.modu n1 n2)) + | _, _ => None + end. + +Definition andl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vlong n2 => Vlong(Int64.and n1 n2) + | _, _ => Vundef + end. + +Definition orl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vlong n2 => Vlong(Int64.or n1 n2) + | _, _ => Vundef + end. + +Definition xorl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vlong n2 => Vlong(Int64.xor n1 n2) + | _, _ => Vundef + end. + +Definition shll (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 Int64.iwordsize' + then Vlong(Int64.shl' n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition shrl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 Int64.iwordsize' + then Vlong(Int64.shr' n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition shrlu (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 Int64.iwordsize' + then Vlong(Int64.shru' n1 n2) + else Vundef + | _, _ => Vundef + end. + (** Comparisons *) Section COMPARISONS. @@ -392,6 +571,18 @@ Definition cmpf_bool (c: comparison) (v1 v2: val): option bool := | _, _ => 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) + | _, _ => None + end. + +Definition cmplu_bool (c: comparison) (v1 v2: val): option bool := + match v1, v2 with + | Vlong n1, Vlong n2 => Some (Int64.cmpu c n1 n2) + | _, _ => None + end. + Definition of_optbool (ob: option bool): val := match ob with Some true => Vtrue | Some false => Vfalse | None => Vundef end. @@ -404,6 +595,12 @@ Definition cmpu (c: comparison) (v1 v2: val): val := Definition cmpf (c: comparison) (v1 v2: val): val := of_optbool (cmpf_bool c v1 v2). +Definition cmpl (c: comparison) (v1 v2: val): val := + of_optbool (cmpl_bool c v1 v2). + +Definition cmplu (c: comparison) (v1 v2: val): val := + of_optbool (cmplu_bool c v1 v2). + End COMPARISONS. (** [load_result] is used in the memory model (library [Mem]) @@ -423,6 +620,7 @@ Definition load_result (chunk: memory_chunk) (v: val) := | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n) | Mint32, Vint n => Vint n | Mint32, Vptr b ofs => Vptr b ofs + | Mint64, Vlong n => Vlong n | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f) | (Mfloat64 | Mfloat64al32), Vfloat f => Vfloat f | _, _ => Vundef @@ -981,6 +1179,12 @@ Inductive lessdef: val -> val -> Prop := | lessdef_refl: forall v, lessdef v v | lessdef_undef: forall v, lessdef Vundef v. +Lemma lessdef_same: + forall v1 v2, v1 = v2 -> lessdef v1 v2. +Proof. + intros. subst v2. constructor. +Qed. + Lemma lessdef_trans: forall v1 v2 v3, lessdef v1 v2 -> lessdef v2 v3 -> lessdef v1 v3. Proof. @@ -1071,6 +1275,25 @@ Proof. intros. destruct ob; simpl; auto. rewrite (H b); auto. Qed. +Lemma longofwords_lessdef: + forall v1 v2 v1' v2', + lessdef v1 v1' -> lessdef v2 v2' -> lessdef (longofwords v1 v2) (longofwords v1' v2'). +Proof. + intros. unfold longofwords. inv H; auto. inv H0; auto. destruct v1'; auto. +Qed. + +Lemma loword_lessdef: + forall v v', lessdef v v' -> lessdef (loword v) (loword v'). +Proof. + intros. inv H; auto. +Qed. + +Lemma hiword_lessdef: + forall v v', lessdef v v' -> lessdef (hiword v) (hiword v'). +Proof. + intros. inv H; auto. +Qed. + End Val. (** * Values and memory injections *) @@ -1093,6 +1316,8 @@ Definition meminj : Type := block -> option (block * Z). Inductive val_inject (mi: meminj): val -> val -> Prop := | val_inject_int: forall i, val_inject mi (Vint i) (Vint i) + | val_inject_long: + forall i, val_inject mi (Vlong i) (Vlong i) | val_inject_float: forall f, val_inject mi (Vfloat f) (Vfloat f) | val_inject_ptr: @@ -1103,8 +1328,7 @@ Inductive val_inject (mi: meminj): val -> val -> Prop := | val_inject_undef: forall v, val_inject mi Vundef v. -Hint Resolve val_inject_int val_inject_float val_inject_ptr - val_inject_undef. +Hint Constructors val_inject. Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= | val_nil_inject : @@ -1225,6 +1449,25 @@ Proof. now erewrite !valid_ptr_inj by eauto. Qed. +Lemma val_longofwords_inject: + forall v1 v2 v1' v2', + val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.longofwords v1 v2) (Val.longofwords v1' v2'). +Proof. + intros. unfold Val.longofwords. inv H; auto. inv H0; auto. +Qed. + +Lemma val_loword_inject: + forall v v', val_inject f v v' -> val_inject f (Val.loword v) (Val.loword v'). +Proof. + intros. unfold Val.loword; inv H; auto. +Qed. + +Lemma val_hiword_inject: + forall v v', val_inject f v v' -> val_inject f (Val.hiword v) (Val.hiword v'). +Proof. + intros. unfold Val.hiword; inv H; auto. +Qed. + End VAL_INJ_OPS. (** Monotone evolution of a memory injection. *) @@ -1288,9 +1531,8 @@ Lemma val_inject_id: val_inject inject_id v1 v2 <-> Val.lessdef v1 v2. Proof. intros; split; intros. - inv H. constructor. constructor. + inv H; auto. unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor. - constructor. inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. constructor. Qed. -- cgit v1.2.3