diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/Events.v | 42 | ||||
-rw-r--r-- | common/Memdata.v | 20 | ||||
-rw-r--r-- | common/Memory.v | 26 | ||||
-rw-r--r-- | common/Memtype.v | 20 | ||||
-rw-r--r-- | common/Values.v | 116 |
5 files changed, 113 insertions, 111 deletions
diff --git a/common/Events.v b/common/Events.v index 3bec15db..78162fff 100644 --- a/common/Events.v +++ b/common/Events.v @@ -453,7 +453,7 @@ Hypothesis symb_inj: symbols_inject. Lemma eventval_match_inject: forall ev ty v1 v2, - eventval_match ge1 ev ty v1 -> val_inject f v1 v2 -> eventval_match ge2 ev ty v2. + eventval_match ge1 ev ty v1 -> Val.inject f v1 v2 -> eventval_match ge2 ev ty v2. Proof. intros. inv H; inv H0; try constructor; auto. destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ. @@ -463,7 +463,7 @@ Qed. Lemma eventval_match_inject_2: forall ev ty v1, eventval_match ge1 ev ty v1 -> - exists v2, eventval_match ge2 ev ty v2 /\ val_inject f v1 v2. + exists v2, eventval_match ge2 ev ty v2 /\ Val.inject f v1 v2. Proof. intros. inv H; try (econstructor; split; eauto; constructor; fail). destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]]. @@ -473,7 +473,7 @@ Qed. Lemma eventval_list_match_inject: forall evl tyl vl1, eventval_list_match ge1 evl tyl vl1 -> - forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2. + forall vl2, Val.inject_list f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2. Proof. induction 1; intros. inv H; constructor. inv H1. constructor. eapply eventval_match_inject; eauto. eauto. @@ -669,10 +669,10 @@ Record extcall_properties (sem: extcall_sem) exists b2, f b1 = Some(b2, 0) /\ Senv.find_symbol ge2 id = Some b2) -> sem ge1 vargs m1 t vres m2 -> Mem.inject f m1 m1' -> - val_list_inject f vargs vargs' -> + Val.inject_list f vargs vargs' -> exists f', exists vres', exists m2', sem ge2 vargs' m1' t vres' m2' - /\ val_inject f' vres vres' + /\ Val.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' @@ -735,9 +735,9 @@ Lemma volatile_load_inject: forall ge1 ge2 f chunk m b ofs t v b' ofs' m', symbols_inject f ge1 ge2 -> volatile_load ge1 chunk m b ofs t v -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> Mem.inject f m m' -> - exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ val_inject f v v'. + exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ Val.inject f v v'. Proof. intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D). inv VL. @@ -747,7 +747,7 @@ Proof. rewrite Int.add_zero. exists (Val.load_result chunk v2); split. constructor; auto. erewrite D; eauto. - apply val_load_result_inject. auto. + apply Val.load_result_inject. auto. - (* normal load *) exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y). exists v2; split; auto. @@ -852,7 +852,7 @@ Proof. (* inject *) inv H1. inv H3. exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). + assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. econstructor; eauto. @@ -934,8 +934,8 @@ Lemma volatile_store_inject: forall ge1 ge2 f chunk m1 b ofs v t m2 m1' b' ofs' v', symbols_inject f ge1 ge2 -> volatile_store ge1 chunk m1 b ofs v t m2 -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> - val_inject f v v' -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f v v' -> Mem.inject f m1 m1' -> exists m2', volatile_store ge2 chunk m1' b' ofs' v' t m2' @@ -950,7 +950,7 @@ Proof. inv AI. exploit Q; eauto. intros [A B]. subst delta. rewrite Int.add_zero. exists m1'; split. constructor; auto. erewrite S; eauto. - eapply eventval_match_inject; eauto. apply val_load_result_inject. auto. + eapply eventval_match_inject; eauto. apply Val.load_result_inject. auto. intuition auto with mem. - (* normal store *) inversion AI; subst. @@ -1058,7 +1058,7 @@ Proof. (* mem inject *) rewrite volatile_store_global_charact in H1. destruct H1 as [b [P Q]]. exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. + assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. exploit ec_mem_inject. eapply volatile_store_ok. eauto. intuition. eexact Q. eauto. constructor. eauto. eauto. intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]]. exists f'; exists vres'; exists m2'; intuition. @@ -1552,10 +1552,10 @@ Lemma external_call_mem_inject: 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' -> + Val.inject_list f vargs vargs' -> exists f', exists vres', exists m2', external_call ef ge vargs' m1' t vres' m2' - /\ val_inject f' vres vres' + /\ Val.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' @@ -1644,11 +1644,11 @@ Proof. 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). + forall f tyl vl1 vl2, Val.inject_list f vl1 vl2 -> Val.inject_list 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. + destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. Qed. Lemma encode_long_lessdef: @@ -1659,10 +1659,10 @@ Proof. 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). + forall f oty v1 v2, Val.inject f v1 v2 -> Val.inject_list 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. + constructor. apply Val.hiword_inject; auto. constructor. apply Val.loword_inject; auto. auto. Qed. Lemma encode_long_has_type: @@ -1736,10 +1736,10 @@ Lemma external_call_mem_inject': 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' -> + Val.inject_list f vargs vargs' -> exists f' vres' m2', external_call' ef ge vargs' m1' t vres' m2' - /\ val_list_inject f' vres vres' + /\ Val.inject_list 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' diff --git a/common/Memdata.v b/common/Memdata.v index 96278a29..9c64563b 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -726,7 +726,7 @@ Inductive memval_inject (f: meminj): memval -> memval -> Prop := forall n, memval_inject f (Byte n) (Byte n) | memval_inject_frag: forall v1 v2 q n, - val_inject f v1 v2 -> + 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. @@ -738,7 +738,7 @@ Proof. Qed. (** [decode_val], applied to lists of memory values that are pairwise - related by [memval_inject], returns values that are related by [val_inject]. *) + related by [memval_inject], returns values that are related by [Val.inject]. *) Lemma proj_bytes_inject: forall f vl vl', @@ -759,7 +759,7 @@ Lemma check_value_inject: list_forall2 (memval_inject f) vl vl' -> forall v v' q n, check_value n v q vl = true -> - val_inject f v v' -> v <> Vundef -> + Val.inject f v v' -> v <> Vundef -> check_value n v' q vl' = true. Proof. induction 1; intros; destruct n; simpl in *; auto. @@ -774,7 +774,7 @@ Qed. Lemma proj_value_inject: forall f q vl1 vl2, list_forall2 (memval_inject f) vl1 vl2 -> - val_inject f (proj_value q vl1) (proj_value q vl2). + Val.inject f (proj_value q vl1) (proj_value q vl2). Proof. intros. unfold proj_value. inversion H; subst. auto. inversion H0; subst; auto. @@ -819,26 +819,26 @@ Qed. Theorem decode_val_inject: forall f vl1 vl2 chunk, list_forall2 (memval_inject f) vl1 vl2 -> - val_inject f (decode_val chunk vl1) (decode_val chunk vl2). + Val.inject f (decode_val chunk vl1) (decode_val chunk vl2). Proof. intros. unfold decode_val. 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)) + 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. + apply Val.load_result_inject. apply proj_value_inject; auto. } destruct chunk; auto. Qed. -(** Symmetrically, [encode_val], applied to values related by [val_inject], +(** Symmetrically, [encode_val], applied to values related by [Val.inject], returns lists of memory values that are pairwise related by [memval_inject]. *) @@ -870,7 +870,7 @@ Proof. 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). + 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. @@ -880,7 +880,7 @@ Qed. Theorem encode_val_inject: forall f v1 v2 chunk, - val_inject f v1 v2 -> + Val.inject f v1 v2 -> list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2). Proof. intros. inversion H; subst; simpl; destruct chunk; diff --git a/common/Memory.v b/common/Memory.v index 45c2497b..3d781cac 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -2303,7 +2303,7 @@ Lemma load_inj: mem_inj f m1 m2 -> load chunk m1 b1 ofs = Some v1 -> f b1 = Some (b2, delta) -> - exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2. Proof. intros. exists (decode_val chunk (getN (size_chunk_nat chunk) (ofs + delta) (m2.(mem_contents)#b2))). @@ -2367,7 +2367,7 @@ Lemma store_mapped_inj: store chunk m1 b1 ofs v1 = Some n1 -> meminj_no_overlap f m1 -> f b1 = Some (b2, delta) -> - val_inject f v1 v2 -> + Val.inject f v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 /\ mem_inj f n1 n2. @@ -3250,7 +3250,7 @@ Theorem valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> valid_pointer m2 b' (Int.unsigned ofs') = true. Proof. intros. inv H1. @@ -3263,7 +3263,7 @@ Theorem weak_valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> weak_valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> weak_valid_pointer m2 b' (Int.unsigned ofs') = true. Proof. intros. inv H1. @@ -3376,7 +3376,7 @@ Theorem load_inject: inject f m1 m2 -> load chunk m1 b1 ofs = Some v1 -> f b1 = Some (b2, delta) -> - exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2. Proof. intros. inv H. eapply load_inj; eauto. Qed. @@ -3385,8 +3385,8 @@ Theorem loadv_inject: forall f m1 m2 chunk a1 a2 v1, inject f m1 m2 -> loadv chunk m1 a1 = Some v1 -> - val_inject f a1 a2 -> - exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2. + Val.inject f a1 a2 -> + exists v2, loadv chunk m2 a2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. inv H1; simpl in H0; try discriminate. exploit load_inject; eauto. intros [v2 [LOAD INJ]]. @@ -3414,7 +3414,7 @@ Theorem store_mapped_inject: inject f m1 m2 -> store chunk m1 b1 ofs v1 = Some n1 -> f b1 = Some (b2, delta) -> - val_inject f v1 v2 -> + Val.inject f v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 /\ inject f n1 n2. @@ -3484,8 +3484,8 @@ Theorem storev_mapped_inject: forall f chunk m1 a1 v1 n1 m2 a2 v2, inject f m1 m2 -> storev chunk m1 a1 v1 = Some n1 -> - val_inject f a1 a2 -> - val_inject f v1 v2 -> + Val.inject f a1 a2 -> + Val.inject f v1 v2 -> exists n2, storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2. Proof. @@ -3977,14 +3977,14 @@ Qed. Lemma val_lessdef_inject_compose: forall f v1 v2 v3, - Val.lessdef v1 v2 -> val_inject f v2 v3 -> val_inject f v1 v3. + Val.lessdef v1 v2 -> Val.inject f v2 v3 -> Val.inject f v1 v3. Proof. intros. inv H. auto. auto. Qed. Lemma val_inject_lessdef_compose: forall f v1 v2 v3, - val_inject f v1 v2 -> Val.lessdef v2 v3 -> val_inject f v1 v3. + Val.inject f v1 v2 -> Val.lessdef v2 v3 -> Val.inject f v1 v3. Proof. intros. inv H0. auto. inv H. auto. Qed. @@ -4113,7 +4113,7 @@ Theorem store_inject_neutral: store chunk m b ofs v = Some m' -> inject_neutral thr m -> Plt b thr -> - val_inject (flat_inj thr) v v -> + Val.inject (flat_inj thr) v v -> inject_neutral thr m'. Proof. intros; red. diff --git a/common/Memtype.v b/common/Memtype.v index d94c895f..43fc708f 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -927,7 +927,7 @@ Axiom weak_valid_pointer_extends: - if [f b = Some(b', ofs)], the block [b] of [m2] corresponds to a sub-block at offset [ofs] of the block [b'] in [m2]. -A memory injection [f] defines a relation [val_inject] between values +A memory injection [f] defines a relation [Val.inject] between values that is the identity for integer and float values, and relocates pointer values as prescribed by [f]. (See module [Values].) @@ -1000,14 +1000,14 @@ Axiom valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> valid_pointer m2 b' (Int.unsigned ofs') = true. Axiom weak_valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> weak_valid_pointer m1 b (Int.unsigned ofs) = true -> - val_inject f (Vptr b ofs) (Vptr b' ofs') -> + Val.inject f (Vptr b ofs) (Vptr b' ofs') -> weak_valid_pointer m2 b' (Int.unsigned ofs') = true. Axiom inject_no_overlap: @@ -1037,14 +1037,14 @@ Axiom load_inject: inject f m1 m2 -> load chunk m1 b1 ofs = Some v1 -> f b1 = Some (b2, delta) -> - exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. + exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2. Axiom loadv_inject: forall f m1 m2 chunk a1 a2 v1, inject f m1 m2 -> loadv chunk m1 a1 = Some v1 -> - val_inject f a1 a2 -> - exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2. + Val.inject f a1 a2 -> + exists v2, loadv chunk m2 a2 = Some v2 /\ Val.inject f v1 v2. Axiom loadbytes_inject: forall f m1 m2 b1 ofs len b2 delta bytes1, @@ -1059,7 +1059,7 @@ Axiom store_mapped_inject: inject f m1 m2 -> store chunk m1 b1 ofs v1 = Some n1 -> f b1 = Some (b2, delta) -> - val_inject f v1 v2 -> + Val.inject f v1 v2 -> exists n2, store chunk m2 b2 (ofs + delta) v2 = Some n2 /\ inject f n1 n2. @@ -1085,8 +1085,8 @@ Axiom storev_mapped_inject: forall f chunk m1 a1 v1 n1 m2 a2 v2, inject f m1 m2 -> storev chunk m1 a1 v1 = Some n1 -> - val_inject f a1 a2 -> - val_inject f v1 v2 -> + Val.inject f a1 a2 -> + Val.inject f v1 v2 -> exists n2, storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2. @@ -1221,7 +1221,7 @@ Axiom store_inject_neutral: store chunk m b ofs v = Some m' -> inject_neutral thr m -> Plt b thr -> - val_inject (flat_inj thr) v v -> + Val.inject (flat_inj thr) v v -> inject_neutral thr m'. Axiom drop_inject_neutral: diff --git a/common/Values.v b/common/Values.v index 12b380b7..a4ead481 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1477,8 +1477,6 @@ Proof. intros. inv H; auto. Qed. -End Val. - (** * Values and memory injections *) (** A memory injection [f] is a function from addresses to either [None] @@ -1496,62 +1494,62 @@ Definition meminj : Type := block -> option (block * Z). as prescribed by the memory injection. Moreover, [Vundef] values inject into any other value. *) -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_single: - forall f, val_inject mi (Vsingle f) (Vsingle f) - | val_inject_ptr: +Inductive inject (mi: meminj): val -> val -> Prop := + | inject_int: + forall i, inject mi (Vint i) (Vint i) + | inject_long: + forall i, inject mi (Vlong i) (Vlong i) + | inject_float: + forall f, inject mi (Vfloat f) (Vfloat f) + | inject_single: + forall f, inject mi (Vsingle f) (Vsingle f) + | inject_ptr: forall b1 ofs1 b2 ofs2 delta, mi b1 = Some (b2, delta) -> ofs2 = Int.add ofs1 (Int.repr delta) -> - val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) + inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) | val_inject_undef: forall v, - val_inject mi Vundef v. + inject mi Vundef v. -Hint Constructors val_inject. +Hint Constructors inject. -Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= - | val_nil_inject : - val_list_inject mi nil nil - | val_cons_inject : forall v v' vl vl' , - val_inject mi v v' -> val_list_inject mi vl vl'-> - val_list_inject mi (v :: vl) (v' :: vl'). +Inductive inject_list (mi: meminj): list val -> list val-> Prop:= + | inject_list_nil : + inject_list mi nil nil + | inject_list_cons : forall v v' vl vl' , + inject mi v v' -> inject_list mi vl vl'-> + inject_list mi (v :: vl) (v' :: vl'). -Hint Resolve val_nil_inject val_cons_inject. +Hint Resolve inject_list_nil inject_list_cons. Section VAL_INJ_OPS. Variable f: meminj. -Lemma val_load_result_inject: +Lemma load_result_inject: forall chunk v1 v2, - val_inject f v1 v2 -> - val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2). + inject f v1 v2 -> + inject f (Val.load_result chunk v1) (Val.load_result chunk v2). Proof. intros. inv H; destruct chunk; simpl; econstructor; eauto. Qed. -Remark val_add_inject: +Remark add_inject: forall v1 v1' v2 v2', - val_inject f v1 v1' -> - val_inject f v2 v2' -> - val_inject f (Val.add v1 v2) (Val.add v1' v2'). + inject f v1 v1' -> + inject f v2 v2' -> + inject f (Val.add v1 v2) (Val.add v1' v2'). Proof. intros. inv H; inv H0; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. Qed. -Remark val_sub_inject: +Remark sun_inject: forall v1 v1' v2 v2', - val_inject f v1 v1' -> - val_inject f v2 v2' -> - val_inject f (Val.sub v1 v2) (Val.sub v1' v2'). + inject f v1 v1' -> + inject f v2 v2' -> + inject f (Val.sub v1 v2) (Val.sub v1' v2'). Proof. intros. inv H; inv H0; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. @@ -1559,10 +1557,10 @@ Proof. rewrite Int.sub_shifted. auto. Qed. -Lemma val_cmp_bool_inject: +Lemma cmp_bool_inject: forall c v1 v2 v1' v2' b, - val_inject f v1 v1' -> - val_inject f v2 v2' -> + inject f v1 v1' -> + inject f v2 v2' -> Val.cmp_bool c v1 v2 = Some b -> Val.cmp_bool c v1' v2' = Some b. Proof. @@ -1602,10 +1600,10 @@ Hypothesis valid_different_ptrs_inj: b1' <> b2' \/ Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). -Lemma val_cmpu_bool_inject: +Lemma cmpu_bool_inject: forall c v1 v2 v1' v2' b, - val_inject f v1 v1' -> - val_inject f v2 v2' -> + inject f v1 v1' -> + inject f v2 v2' -> Val.cmpu_bool valid_ptr1 c v1 v2 = Some b -> Val.cmpu_bool valid_ptr2 c v1' v2' = Some b. Proof. @@ -1644,27 +1642,31 @@ Proof. now erewrite !valid_ptr_inj by eauto. Qed. -Lemma val_longofwords_inject: +Lemma 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'). + inject f v1 v1' -> inject f v2 v2' -> 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'). +Lemma loword_inject: + forall v v', inject f v v' -> 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'). +Lemma hiword_inject: + forall v v', inject f v v' -> inject f (Val.hiword v) (Val.hiword v'). Proof. intros. unfold Val.hiword; inv H; auto. Qed. End VAL_INJ_OPS. +End Val. + +Notation meminj := Val.meminj. + (** Monotone evolution of a memory injection. *) Definition inject_incr (f1 f2: meminj) : Prop := @@ -1684,33 +1686,33 @@ Qed. Lemma val_inject_incr: forall f1 f2 v v', inject_incr f1 f2 -> - val_inject f1 v v' -> - val_inject f2 v v'. + Val.inject f1 v v' -> + Val.inject f2 v v'. Proof. intros. inv H0; eauto. Qed. -Lemma val_list_inject_incr: +Lemma val_inject_list_incr: forall f1 f2 vl vl' , - inject_incr f1 f2 -> val_list_inject f1 vl vl' -> - val_list_inject f2 vl vl'. + inject_incr f1 f2 -> Val.inject_list f1 vl vl' -> + Val.inject_list f2 vl vl'. Proof. induction vl; intros; inv H0. auto. constructor. eapply val_inject_incr; eauto. auto. Qed. -Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr. +Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr. Lemma val_inject_lessdef: - forall v1 v2, Val.lessdef v1 v2 <-> val_inject (fun b => Some(b, 0)) v1 v2. + forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2. Proof. intros; split; intros. inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. inv H; auto. inv H0. rewrite Int.add_zero; auto. Qed. -Lemma val_list_inject_lessdef: - forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> val_list_inject (fun b => Some(b, 0)) vl1 vl2. +Lemma val_inject_list_lessdef: + forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> Val.inject_list (fun b => Some(b, 0)) vl1 vl2. Proof. intros; split. induction 1; constructor; auto. apply val_inject_lessdef; auto. @@ -1723,7 +1725,7 @@ Definition inject_id : meminj := fun b => Some(b, 0). Lemma val_inject_id: forall v1 v2, - val_inject inject_id v1 v2 <-> Val.lessdef v1 v2. + Val.inject inject_id v1 v2 <-> Val.lessdef v1 v2. Proof. intros; split; intros. inv H; auto. @@ -1747,8 +1749,8 @@ Definition compose_meminj (f f': meminj) : meminj := Lemma val_inject_compose: forall f f' v1 v2 v3, - val_inject f v1 v2 -> val_inject f' v2 v3 -> - val_inject (compose_meminj f f') v1 v3. + Val.inject f v1 v2 -> Val.inject f' v2 v3 -> + Val.inject (compose_meminj f f') v1 v3. Proof. intros. inv H; auto; inv H0; auto. econstructor. unfold compose_meminj; rewrite H1; rewrite H3; eauto. |