diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /backend/ValueDomain.v | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'backend/ValueDomain.v')
| -rw-r--r-- | backend/ValueDomain.v | 778 |
1 files changed, 389 insertions, 389 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 3d95bdd1..048ab816 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -47,7 +47,7 @@ Definition bc_below (bc: block_classification) (bound: block) : Prop := Lemma bc_below_invalid: forall b bc bound, ~Plt b bound -> bc_below bc bound -> bc b = BCinvalid. Proof. - intros. destruct (block_class_eq (bc b) BCinvalid); auto. + intros. destruct (block_class_eq (bc b) BCinvalid); auto. elim H. apply H0; auto. Qed. @@ -96,7 +96,7 @@ Lemma cmatch_lub_l: Proof. intros. unfold club; inv H; destruct y; try constructor; destruct (eqb b b0) eqn:EQ; try constructor. - replace b0 with b by (apply eqb_prop; auto). constructor. + replace b0 with b by (apply eqb_prop; auto). constructor. Qed. Lemma cmatch_lub_r: @@ -136,7 +136,7 @@ Inductive aptr : Type := Definition eq_aptr: forall (p1 p2: aptr), {p1=p2} + {p1<>p2}. Proof. - intros. generalize ident_eq, Int.eq_dec; intros. decide equality. + intros. generalize ident_eq, Int.eq_dec; intros. decide equality. Defined. Inductive pmatch (b: block) (ofs: int): aptr -> Prop := @@ -192,7 +192,7 @@ Qed. Lemma pmatch_top': forall b ofs p, pmatch b ofs p -> pmatch b ofs Ptop. Proof. - intros. apply pmatch_ge with p; auto with va. + intros. apply pmatch_ge with p; auto with va. Qed. Definition plub (p q: aptr) : aptr := @@ -215,7 +215,7 @@ Definition plub (p q: aptr) : aptr := Nonstack | Stk ofs1, Stk ofs2 => if Int.eq_dec ofs1 ofs2 then p else Stack - | (Stk _ | Stack), Stack => + | (Stk _ | Stack), Stack => Stack | Stack, Stk _ => Stack @@ -226,22 +226,22 @@ Lemma plub_comm: forall p q, plub p q = plub q p. Proof. intros; unfold plub; destruct p; destruct q; auto. - destruct (ident_eq id id0). subst id0. - rewrite dec_eq_true. + destruct (ident_eq id id0). subst id0. + rewrite dec_eq_true. destruct (Int.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true. auto. - rewrite dec_eq_false by auto. auto. - rewrite dec_eq_false by auto. auto. - destruct (ident_eq id id0). subst id0. + rewrite dec_eq_false by auto. auto. + rewrite dec_eq_false by auto. auto. + destruct (ident_eq id id0). subst id0. rewrite dec_eq_true; auto. rewrite dec_eq_false; auto. - destruct (ident_eq id id0). subst id0. + destruct (ident_eq id id0). subst id0. rewrite dec_eq_true; auto. rewrite dec_eq_false; auto. - destruct (ident_eq id id0). subst id0. + destruct (ident_eq id id0). subst id0. rewrite dec_eq_true; auto. rewrite dec_eq_false; auto. destruct (Int.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true; auto. - rewrite dec_eq_false; auto. + rewrite dec_eq_false; auto. Qed. Lemma pge_lub_l: @@ -283,7 +283,7 @@ Proof. - unfold plub; destruct q; repeat rewrite dec_eq_true; constructor. - rewrite dec_eq_true; constructor. - rewrite dec_eq_true; constructor. -- rewrite dec_eq_true. destruct (Int.eq_dec ofs ofs0); constructor. +- rewrite dec_eq_true. destruct (Int.eq_dec ofs ofs0); constructor. - destruct (ident_eq id id0). destruct (Int.eq_dec ofs ofs0); constructor. constructor. - destruct (ident_eq id id0); constructor. - destruct (ident_eq id id0); constructor. @@ -328,7 +328,7 @@ Lemma pincl_sound: forall b ofs p q, pincl p q = true -> pmatch b ofs p -> pmatch b ofs q. Proof. - intros. eapply pmatch_ge; eauto. apply pincl_ge; auto. + intros. eapply pmatch_ge; eauto. apply pincl_ge; auto. Qed. Definition padd (p: aptr) (n: int) : aptr := @@ -343,7 +343,7 @@ Lemma padd_sound: pmatch b ofs p -> pmatch b (Int.add ofs delta) (padd p delta). Proof. - intros. inv H; simpl padd; eauto with va. + intros. inv H; simpl padd; eauto with va. Qed. Definition psub (p: aptr) (n: int) : aptr := @@ -358,7 +358,7 @@ Lemma psub_sound: pmatch b ofs p -> pmatch b (Int.sub ofs delta) (psub p delta). Proof. - intros. inv H; simpl psub; eauto with va. + intros. inv H; simpl psub; eauto with va. Qed. Definition poffset (p: aptr) : aptr := @@ -373,7 +373,7 @@ Lemma poffset_sound: pmatch b ofs1 p -> pmatch b ofs2 (poffset p). Proof. - intros. inv H; simpl poffset; eauto with va. + intros. inv H; simpl poffset; eauto with va. Qed. Definition psub2 (p q: aptr) : option int := @@ -442,7 +442,7 @@ Lemma pcmp_sound: cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) (pcmp c p1 p2). Proof. intros. - assert (DIFF: b1 <> b2 -> + assert (DIFF: b1 <> b2 -> cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) (cmp_different_blocks c)). { @@ -455,19 +455,19 @@ Proof. cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) (Maybe (Int.cmpu c ofs1 ofs2))). { - intros. subst b2. simpl. rewrite dec_eq_true. + intros. subst b2. simpl. rewrite dec_eq_true. destruct ((valid b1 (Int.unsigned ofs1) || valid b1 (Int.unsigned ofs1 - 1)) && (valid b1 (Int.unsigned ofs2) || valid b1 (Int.unsigned ofs2 - 1))); simpl. - constructor. + constructor. constructor. } unfold pcmp; inv H; inv H0; (apply cmatch_top || (apply DIFF; congruence) || idtac). - - destruct (peq id id0). subst id0. apply SAME. eapply bc_glob; eauto. + - destruct (peq id id0). subst id0. apply SAME. eapply bc_glob; eauto. auto with va. - destruct (peq id id0); auto with va. - destruct (peq id id0); auto with va. - destruct (peq id id0); auto with va. - - apply SAME. eapply bc_stack; eauto. + - apply SAME. eapply bc_stack; eauto. Qed. Lemma pcmp_none: @@ -539,7 +539,7 @@ Definition Vtop := Ifptr Ptop. Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}. Proof. intros. generalize zeq Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec eq_aptr; intros. - decide equality. + decide equality. Defined. Definition is_uns (n: Z) (i: int) : Prop := @@ -570,7 +570,7 @@ Lemma vmatch_ifptr: (forall b ofs, v = Vptr b ofs -> pmatch b ofs p) -> vmatch v (Ifptr p). Proof. - intros. destruct v; constructor; auto. + intros. destruct v; constructor; auto. Qed. Lemma vmatch_top: forall v x, vmatch v x -> vmatch v Vtop. @@ -604,8 +604,8 @@ Definition ssize (i: int) := Int.size (if Int.lt i Int.zero then Int.not i else Lemma is_uns_usize: forall i, is_uns (usize i) i. Proof. - unfold usize; intros; red; intros. - apply Int.bits_size_2. omega. + unfold usize; intros; red; intros. + apply Int.bits_size_2. omega. Qed. Lemma is_sgn_ssize: @@ -627,7 +627,7 @@ Qed. Lemma is_uns_zero_ext: forall n i, is_uns n i <-> Int.zero_ext n i = i. Proof. - intros; split; intros. + intros; split; intros. Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. omega. rewrite <- H. red; intros. rewrite Int.bits_zero_ext by omega. rewrite zlt_false by omega. auto. Qed. @@ -635,12 +635,12 @@ Qed. Lemma is_sgn_sign_ext: forall n i, 0 < n -> (is_sgn n i <-> Int.sign_ext n i = i). Proof. - intros; split; intros. + intros; split; intros. Int.bit_solve. destruct (zlt i0 n); auto. transitivity (Int.testbit i (Int.zwordsize - 1)). - apply H0; omega. symmetry; apply H0; omega. + apply H0; omega. symmetry; apply H0; omega. rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by omega. - f_equal. transitivity (n-1). destruct (zlt m n); omega. + f_equal. transitivity (n-1). destruct (zlt m n); omega. destruct (zlt (Int.zwordsize - 1) n); omega. Qed. @@ -649,7 +649,7 @@ Lemma is_zero_ext_uns: is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i). Proof. intros. red; intros. rewrite Int.bits_zero_ext by omega. - destruct (zlt m0 n); auto. destruct H. apply H; omega. omegaContradiction. + destruct (zlt m0 n); auto. destruct H. apply H; omega. omegaContradiction. Qed. Lemma is_zero_ext_sgn: @@ -657,7 +657,7 @@ Lemma is_zero_ext_sgn: n < m -> is_sgn m (Int.zero_ext n i). Proof. - intros. red; intros. rewrite ! Int.bits_zero_ext by omega. + intros. red; intros. rewrite ! Int.bits_zero_ext by omega. transitivity false. apply zlt_false; omega. symmetry; apply zlt_false; omega. Qed. @@ -668,18 +668,18 @@ Lemma is_sign_ext_uns: is_uns m i -> is_uns m (Int.sign_ext n i). Proof. - intros; red; intros. rewrite Int.bits_sign_ext by omega. + intros; red; intros. rewrite Int.bits_sign_ext by omega. apply H0. destruct (zlt m0 n); omega. destruct (zlt m0 n); omega. Qed. - + Lemma is_sign_ext_sgn: forall i n m, 0 < n -> 0 < m -> is_sgn m i \/ n <= m -> is_sgn m (Int.sign_ext n i). Proof. intros. apply is_sgn_sign_ext; auto. - destruct (zlt m n). destruct H1. apply is_sgn_sign_ext in H1; auto. - rewrite <- H1. rewrite (Int.sign_ext_widen i) by omega. apply Int.sign_ext_idem; auto. + destruct (zlt m n). destruct H1. apply is_sgn_sign_ext in H1; auto. + rewrite <- H1. rewrite (Int.sign_ext_widen i) by omega. apply Int.sign_ext_idem; auto. omegaContradiction. apply Int.sign_ext_widen; omega. Qed. @@ -690,7 +690,7 @@ Lemma is_uns_1: forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one. Proof. intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros. - rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. + rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega. Qed. @@ -744,8 +744,8 @@ Lemma vmatch_uns': Proof. intros. assert (A: forall n', n' >= 0 -> n' >= n -> is_uns n' i) by (eauto with va). - unfold uns. - destruct (zle n 1). auto with va. + unfold uns. + destruct (zle n 1). auto with va. destruct (zle n 7). auto with va. destruct (zle n 8). auto with va. destruct (zle n 15). auto with va. @@ -761,8 +761,8 @@ Qed. Lemma vmatch_uns_undef: forall p n, vmatch Vundef (uns p n). Proof. - intros. unfold uns. - destruct (zle n 1). auto with va. + intros. unfold uns. + destruct (zle n 1). auto with va. destruct (zle n 7). auto with va. destruct (zle n 8). auto with va. destruct (zle n 15). auto with va. @@ -774,7 +774,7 @@ Lemma vmatch_sgn': Proof. intros. assert (A: forall n', n' >= 1 -> n' >= n -> is_sgn n' i) by (eauto with va). - unfold sgn. + unfold sgn. destruct (zle n 8). auto with va. destruct (zle n 16); auto with va. Qed. @@ -893,8 +893,8 @@ Proof. intros. unfold vlub; destruct v; destruct w; auto. - rewrite Int.eq_sym. predSpec Int.eq Int.eq_spec n0 n. congruence. - rewrite orb_comm. - destruct (Int.lt n0 Int.zero || Int.lt n Int.zero); f_equal; apply Z.max_comm. + rewrite orb_comm. + destruct (Int.lt n0 Int.zero || Int.lt n Int.zero); f_equal; apply Z.max_comm. - f_equal. apply plub_comm. apply Z.max_comm. - f_equal. apply plub_comm. apply Z.max_comm. - f_equal; apply plub_comm. @@ -918,7 +918,7 @@ Qed. Lemma vge_uns_uns': forall p n, vge (uns p n) (Uns p n). Proof. - unfold uns; intros. + unfold uns; intros. destruct (zle n 1). auto with va. destruct (zle n 7). auto with va. destruct (zle n 8). auto with va. @@ -928,19 +928,19 @@ Qed. Lemma vge_uns_i': forall p n i, 0 <= n -> is_uns n i -> vge (uns p n) (I i). Proof. - intros. apply vge_trans with (Uns p n). apply vge_uns_uns'. auto with va. + intros. apply vge_trans with (Uns p n). apply vge_uns_uns'. auto with va. Qed. Lemma vge_sgn_sgn': forall p n, vge (sgn p n) (Sgn p n). Proof. - unfold sgn; intros. + unfold sgn; intros. destruct (zle n 8). auto with va. destruct (zle n 16); auto with va. Qed. Lemma vge_sgn_i': forall p n i, 0 < n -> is_sgn n i -> vge (sgn p n) (I i). Proof. - intros. apply vge_trans with (Sgn p n). apply vge_sgn_sgn'. auto with va. + intros. apply vge_trans with (Sgn p n). apply vge_sgn_sgn'. auto with va. Qed. Hint Resolve vge_uns_uns' vge_uns_i' vge_sgn_sgn' vge_sgn_i' : va. @@ -952,7 +952,7 @@ Qed. Lemma ssize_pos: forall n, 0 < ssize n. Proof. - unfold ssize; intros. + unfold ssize; intros. generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); omega. Qed. @@ -964,16 +964,16 @@ Proof. unfold vlub; destruct x, y; eauto using pge_lub_l with va. - predSpec Int.eq Int.eq_spec n n0. auto with va. destruct (Int.lt n Int.zero || Int.lt n0 Int.zero). - apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. + apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. + apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. - destruct (Int.lt n Int.zero). - apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. -- apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. + apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. + apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. +- apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - destruct (Int.lt n0 Int.zero). eapply vge_trans. apply vge_sgn_sgn'. apply vge_trans with (Sgn p (n + 1)); eauto with va. - eapply vge_trans. apply vge_uns_uns'. eauto with va. + eapply vge_trans. apply vge_uns_uns'. eauto with va. - eapply vge_trans. apply vge_sgn_sgn'. apply vge_trans with (Sgn p (n + 1)); eauto using pge_lub_l with va. - eapply vge_trans. apply vge_sgn_sgn'. eauto with va. @@ -987,7 +987,7 @@ Qed. Lemma vge_lub_r: forall x y, vge (vlub x y) y. Proof. - intros. rewrite vlub_comm. apply vge_lub_l. + intros. rewrite vlub_comm. apply vge_lub_l. Qed. Lemma vmatch_lub_l: @@ -1036,13 +1036,13 @@ Definition vplub (v: aval) (p: aptr) : aptr := Lemma vmatch_vplub_l: forall v x p, vmatch v x -> vmatch v (Ifptr (vplub x p)). Proof. - intros. unfold vplub; inv H; auto with va; constructor; eapply pmatch_lub_l; eauto. + intros. unfold vplub; inv H; auto with va; constructor; eapply pmatch_lub_l; eauto. Qed. Lemma pmatch_vplub: forall b ofs x p, pmatch b ofs p -> pmatch b ofs (vplub x p). Proof. - intros. + intros. assert (DFL: pmatch b ofs (if va_strict tt then p else Ptop)). { destruct (va_strict tt); auto. eapply pmatch_top'; eauto. } unfold vplub; destruct x; auto; apply pmatch_lub_r; auto. @@ -1051,7 +1051,7 @@ Qed. Lemma vmatch_vplub_r: forall v x p, vmatch v (Ifptr p) -> vmatch v (Ifptr (vplub x p)). Proof. - intros. apply vmatch_ifptr; intros; subst v. inv H. apply pmatch_vplub; auto. + intros. apply vmatch_ifptr; intros; subst v. inv H. apply pmatch_vplub; auto. Qed. (** Inclusion *) @@ -1065,13 +1065,13 @@ Definition vpincl (v: aval) (p: aptr) : bool := Lemma vpincl_ge: forall x p, vpincl x p = true -> vge (Ifptr p) x. Proof. - unfold vpincl; intros. destruct x; constructor; apply pincl_ge; auto. + unfold vpincl; intros. destruct x; constructor; apply pincl_ge; auto. Qed. Lemma vpincl_sound: forall v x p, vpincl x p = true -> vmatch v x -> vmatch v (Ifptr p). Proof. - intros. apply vmatch_ge with x; auto. apply vpincl_ge; auto. + intros. apply vmatch_ge with x; auto. apply vpincl_ge; auto. Qed. Definition vincl (v w: aval) : bool := @@ -1111,8 +1111,8 @@ Lemma symbol_address_sound: genv_match ge -> vmatch (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)). Proof. - intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. - constructor. constructor. apply H; auto. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + constructor. constructor. apply H; auto. constructor. Qed. @@ -1122,8 +1122,8 @@ Lemma vmatch_ptr_gl: vmatch v (Ptr (Gl id ofs)) -> Val.lessdef v (Genv.symbol_address ge id ofs). Proof. - intros. unfold Genv.symbol_address. inv H0. -- inv H3. replace (Genv.find_symbol ge id) with (Some b). constructor. + intros. unfold Genv.symbol_address. inv H0. +- inv H3. replace (Genv.find_symbol ge id) with (Some b). constructor. symmetry. apply H; auto. - constructor. Qed. @@ -1134,7 +1134,7 @@ Lemma vmatch_ptr_stk: bc sp = BCstack -> Val.lessdef v (Vptr sp ofs). Proof. - intros. inv H. + intros. inv H. - inv H3. replace b with sp by (eapply bc_stack; eauto). constructor. - constructor. Qed. @@ -1223,19 +1223,19 @@ Definition shl (v w: aval) := | _ => ntop1 v end. -Lemma shl_sound: +Lemma shl_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shl v w) (shl x y). Proof. intros. - assert (DEFAULT: vmatch (Val.shl v w) (ntop1 x)). + assert (DEFAULT: vmatch (Val.shl v w) (ntop1 x)). { - destruct v; destruct w; simpl; try constructor. + destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. } destruct y; auto. simpl. inv H0. unfold Val.shl. destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto. exploit Int.ltu_inv; eauto. intros RANGE. - inv H; auto with va. + inv H; auto with va. - apply vmatch_uns'. red; intros. rewrite Int.bits_shl by omega. destruct (zlt m (Int.unsigned n)). auto. apply H1; xomega. - apply vmatch_sgn'. red; intros. zify. @@ -1258,13 +1258,13 @@ Definition shru (v w: aval) := | _ => ntop1 v end. -Lemma shru_sound: +Lemma shru_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shru v w) (shru x y). Proof. intros. - assert (DEFAULT: vmatch (Val.shru v w) (ntop1 x)). + assert (DEFAULT: vmatch (Val.shru v w) (ntop1 x)). { - destruct v; destruct w; simpl; try constructor. + destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. } destruct y; auto. inv H0. unfold shru, Val.shru. @@ -1272,14 +1272,14 @@ Proof. exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE. assert (DEFAULT2: forall i, vmatch (Vint (Int.shru i n)) (uns (provenance x) (Int.zwordsize - Int.unsigned n))). { - intros. apply vmatch_uns. red; intros. - rewrite Int.bits_shru by omega. apply zlt_false. omega. + intros. apply vmatch_uns. red; intros. + rewrite Int.bits_shru by omega. apply zlt_false. omega. } inv H; auto with va. - apply vmatch_uns'. red; intros. zify. rewrite Int.bits_shru by omega. destruct (zlt (m + Int.unsigned n) Int.zwordsize); auto. - apply H1; omega. + apply H1; omega. - destruct v; constructor. Qed. @@ -1297,13 +1297,13 @@ Definition shr (v w: aval) := | _ => ntop1 v end. -Lemma shr_sound: +Lemma shr_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shr v w) (shr x y). Proof. intros. - assert (DEFAULT: vmatch (Val.shr v w) (ntop1 x)). + assert (DEFAULT: vmatch (Val.shr v w) (ntop1 x)). { - destruct v; destruct w; simpl; try constructor. + destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. } destruct y; auto. inv H0. unfold shr, Val.shr. @@ -1311,7 +1311,7 @@ Proof. exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE. assert (DEFAULT2: forall i, vmatch (Vint (Int.shr i n)) (sgn (provenance x) (Int.zwordsize - Int.unsigned n))). { - intros. apply vmatch_sgn. red; intros. + intros. apply vmatch_sgn. red; intros. rewrite ! Int.bits_shr by omega. f_equal. destruct (zlt (m + Int.unsigned n) Int.zwordsize); destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize); @@ -1346,12 +1346,12 @@ Definition and (v w: aval) := | _, _ => ntop2 v w end. -Lemma and_sound: +Lemma and_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.and v w) (and x y). Proof. assert (UNS_l: forall i j n, is_uns n i -> is_uns n (Int.and i j)). { - intros; red; intros. rewrite Int.bits_and by auto. rewrite (H m) by auto. + intros; red; intros. rewrite Int.bits_and by auto. rewrite (H m) by auto. apply andb_false_l. } assert (UNS_r: forall i j n, is_uns n i -> is_uns n (Int.and j i)). @@ -1360,7 +1360,7 @@ Proof. } assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.min n m) (Int.and i j)). { - intros. apply Z.min_case; auto. + intros. apply Z.min_case; auto. } assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.and i j)). { @@ -1379,12 +1379,12 @@ Definition or (v w: aval) := | _, _ => ntop2 v w end. -Lemma or_sound: +Lemma or_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.or v w) (or x y). Proof. assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.or i j)). { - intros; red; intros. rewrite Int.bits_or by auto. + intros; red; intros. rewrite Int.bits_or by auto. rewrite H by xomega. rewrite H0 by xomega. auto. } assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.or i j)). @@ -1404,12 +1404,12 @@ Definition xor (v w: aval) := | _, _ => ntop2 v w end. -Lemma xor_sound: +Lemma xor_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.xor v w) (xor x y). Proof. assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.xor i j)). { - intros; red; intros. rewrite Int.bits_xor by auto. + intros; red; intros. rewrite Int.bits_xor by auto. rewrite H by xomega. rewrite H0 by xomega. auto. } assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.xor i j)). @@ -1433,7 +1433,7 @@ Lemma notint_sound: Proof. assert (SGN: forall n i, is_sgn n i -> is_sgn n (Int.not i)). { - intros; red; intros. rewrite ! Int.bits_not by omega. + intros; red; intros. rewrite ! Int.bits_not by omega. f_equal. apply H; auto. } intros. unfold Val.notint, notint; inv H; eauto with va. @@ -1445,13 +1445,13 @@ Definition ror (x y: aval) := | _, _ => ntop1 x end. -Lemma ror_sound: +Lemma ror_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.ror v w) (ror x y). Proof. - intros. - assert (DEFAULT: forall p, vmatch (Val.ror v w) (Ifptr p)). + intros. + assert (DEFAULT: forall p, vmatch (Val.ror v w) (Ifptr p)). { - destruct v; destruct w; simpl; try constructor. + destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. } unfold ror; destruct y; try apply DEFAULT; auto. inv H0. unfold Val.ror. @@ -1473,7 +1473,7 @@ Proof. intros. assert (UNS_r: forall i j n, is_uns n j -> is_uns n (Int.and i j)). { - intros; red; intros. rewrite Int.bits_and by auto. rewrite (H0 m) by auto. + intros; red; intros. rewrite Int.bits_and by auto. rewrite (H0 m) by auto. apply andb_false_r. } assert (UNS: forall i, vmatch (Vint (Int.rolm i amount mask)) @@ -1486,7 +1486,7 @@ Qed. Definition neg := unop_int Int.neg. -Lemma neg_sound: +Lemma neg_sound: forall v x, vmatch v x -> vmatch (Val.neg v) (neg x). Proof (unop_int_sound Int.neg). @@ -1506,8 +1506,8 @@ Lemma add_sound: Proof. intros. unfold Val.add, add; inv H; inv H0; constructor; ((apply padd_sound; assumption) || (eapply poffset_sound; eassumption) || idtac). - apply pmatch_lub_r. eapply poffset_sound; eauto. - apply pmatch_lub_l. eapply poffset_sound; eauto. + apply pmatch_lub_r. eapply poffset_sound; eauto. + apply pmatch_lub_l. eapply poffset_sound; eauto. Qed. Definition sub (v w: aval) := @@ -1524,7 +1524,7 @@ Definition sub (v w: aval) := | _, _ => ntop2 v w end. -Lemma sub_sound: +Lemma sub_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.sub v w) (sub x y). Proof. intros. inv H; subst; inv H0; subst; simpl; @@ -1534,19 +1534,19 @@ Qed. Definition mul := binop_int Int.mul. -Lemma mul_sound: +Lemma mul_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mul v w) (mul x y). Proof (binop_int_sound Int.mul). Definition mulhs := binop_int Int.mulhs. -Lemma mulhs_sound: +Lemma mulhs_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulhs v w) (mulhs x y). Proof (binop_int_sound Int.mulhs). Definition mulhu := binop_int Int.mulhu. -Lemma mulhu_sound: +Lemma mulhu_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulhu v w) (mulhu x y). Proof (binop_int_sound Int.mulhu). @@ -1563,7 +1563,7 @@ Definition divs (v w: aval) := Lemma divs_sound: forall v w u x y, vmatch v x -> vmatch w y -> Val.divs v w = Some u -> vmatch u (divs x y). Proof. - intros. destruct v; destruct w; try discriminate; simpl in H1. + intros. destruct v; destruct w; try discriminate; simpl in H1. destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:E; inv H1. inv H; inv H0; auto with va. simpl. rewrite E. constructor. @@ -1581,7 +1581,7 @@ Definition divu (v w: aval) := Lemma divu_sound: forall v w u x y, vmatch v x -> vmatch w y -> Val.divu v w = Some u -> vmatch u (divu x y). Proof. - intros. destruct v; destruct w; try discriminate; simpl in H1. + intros. destruct v; destruct w; try discriminate; simpl in H1. destruct (Int.eq i0 Int.zero) eqn:E; inv H1. inv H; inv H0; auto with va. simpl. rewrite E. constructor. Qed. @@ -1599,7 +1599,7 @@ Definition mods (v w: aval) := Lemma mods_sound: forall v w u x y, vmatch v x -> vmatch w y -> Val.mods v w = Some u -> vmatch u (mods x y). Proof. - intros. destruct v; destruct w; try discriminate; simpl in H1. + intros. destruct v; destruct w; try discriminate; simpl in H1. destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:E; inv H1. inv H; inv H0; auto with va. simpl. rewrite E. constructor. @@ -1623,14 +1623,14 @@ Proof. intros. apply is_uns_mon with (usize (Int.modu i j)); auto with va. unfold usize, Int.size. apply Int.Zsize_monotone. generalize (Int.unsigned_range_2 j); intros RANGE. - assert (Int.unsigned j <> 0). + assert (Int.unsigned j <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. - unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. } intros. destruct v; destruct w; try discriminate; simpl in H1. destruct (Int.eq i0 Int.zero) eqn:Z; inv H1. - assert (i0 <> Int.zero) by (generalize (Int.eq_spec i0 Int.zero); rewrite Z; auto). + assert (i0 <> Int.zero) by (generalize (Int.eq_spec i0 Int.zero); rewrite Z; auto). unfold modu. inv H; inv H0; auto with va. rewrite Z. constructor. Qed. @@ -1640,13 +1640,13 @@ Definition shrx (v w: aval) := | _, _ => ntop1 v end. -Lemma shrx_sound: +Lemma shrx_sound: forall v w u x y, vmatch v x -> vmatch w y -> Val.shrx v w = Some u -> vmatch u (shrx x y). Proof. intros. - destruct v; destruct w; try discriminate; simpl in H1. + destruct v; destruct w; try discriminate; simpl in H1. destruct (Int.ltu i0 (Int.repr 31)) eqn:LTU; inv H1. - unfold shrx; inv H; auto with va; inv H0; auto with va. + unfold shrx; inv H; auto with va; inv H0; auto with va. rewrite LTU; auto with va. Qed. @@ -1654,73 +1654,73 @@ Qed. Definition negf := unop_float Float.neg. -Lemma negf_sound: +Lemma negf_sound: forall v x, vmatch v x -> vmatch (Val.negf v) (negf x). Proof (unop_float_sound Float.neg). Definition absf := unop_float Float.abs. -Lemma absf_sound: +Lemma absf_sound: forall v x, vmatch v x -> vmatch (Val.absf v) (absf x). Proof (unop_float_sound Float.abs). Definition addf := binop_float Float.add. -Lemma addf_sound: +Lemma addf_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addf v w) (addf x y). Proof (binop_float_sound Float.add). Definition subf := binop_float Float.sub. -Lemma subf_sound: +Lemma subf_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.subf v w) (subf x y). Proof (binop_float_sound Float.sub). Definition mulf := binop_float Float.mul. -Lemma mulf_sound: +Lemma mulf_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulf v w) (mulf x y). Proof (binop_float_sound Float.mul). Definition divf := binop_float Float.div. -Lemma divf_sound: +Lemma divf_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divf v w) (divf x y). Proof (binop_float_sound Float.div). Definition negfs := unop_single Float32.neg. -Lemma negfs_sound: +Lemma negfs_sound: forall v x, vmatch v x -> vmatch (Val.negfs v) (negfs x). Proof (unop_single_sound Float32.neg). Definition absfs := unop_single Float32.abs. -Lemma absfs_sound: +Lemma absfs_sound: forall v x, vmatch v x -> vmatch (Val.absfs v) (absfs x). Proof (unop_single_sound Float32.abs). Definition addfs := binop_single Float32.add. -Lemma addfs_sound: +Lemma addfs_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addfs v w) (addfs x y). Proof (binop_single_sound Float32.add). Definition subfs := binop_single Float32.sub. -Lemma subfs_sound: +Lemma subfs_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.subfs v w) (subfs x y). Proof (binop_single_sound Float32.sub). Definition mulfs := binop_single Float32.mul. -Lemma mulfs_sound: +Lemma mulfs_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulfs v w) (mulfs x y). Proof (binop_single_sound Float32.mul). Definition divfs := binop_single Float32.div. -Lemma divfs_sound: +Lemma divfs_sound: forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divfs v w) (divfs x y). Proof (binop_single_sound Float32.div). @@ -1738,12 +1738,12 @@ Lemma zero_ext_sound: Proof. assert (DFL: forall nbits i, is_uns nbits (Int.zero_ext nbits i)). { - intros; red; intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; auto. + intros; red; intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; auto. } intros. inv H; simpl; auto with va. apply vmatch_uns. red; intros. zify. rewrite Int.bits_zero_ext by omega. - destruct (zlt m nbits); auto. apply H1; omega. + destruct (zlt m nbits); auto. apply H1; omega. Qed. Definition sign_ext (nbits: Z) (v: aval) := @@ -1761,9 +1761,9 @@ Proof. { intros. apply vmatch_sgn. apply is_sign_ext_sgn; auto with va. } - intros. inv H0; simpl; auto with va. + intros. inv H0; simpl; auto with va. - destruct (zlt n nbits); eauto with va. - constructor; auto. eapply is_sign_ext_uns; eauto with va. + constructor; auto. eapply is_sign_ext_uns; eauto with va. - destruct (zlt n nbits); auto with va. - apply vmatch_sgn. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. @@ -1778,10 +1778,10 @@ Definition singleoffloat (v: aval) := Lemma singleoffloat_sound: forall v x, vmatch v x -> vmatch (Val.singleoffloat v) (singleoffloat x). Proof. - intros. + intros. assert (DEFAULT: vmatch (Val.singleoffloat v) (ntop1 x)). { destruct v; constructor. } - destruct x; auto. inv H. constructor. + destruct x; auto. inv H. constructor. Qed. Definition floatofsingle (v: aval) := @@ -1793,10 +1793,10 @@ Definition floatofsingle (v: aval) := Lemma floatofsingle_sound: forall v x, vmatch v x -> vmatch (Val.floatofsingle v) (floatofsingle x). Proof. - intros. + intros. assert (DEFAULT: vmatch (Val.floatofsingle v) (ntop1 x)). { destruct v; constructor. } - destruct x; auto. inv H. constructor. + destruct x; auto. inv H. constructor. Qed. Definition intoffloat (x: aval) := @@ -1812,9 +1812,9 @@ Definition intoffloat (x: aval) := Lemma intoffloat_sound: forall v x w, vmatch v x -> Val.intoffloat v = Some w -> vmatch w (intoffloat x). Proof. - unfold Val.intoffloat; intros. destruct v; try discriminate. + unfold Val.intoffloat; intros. destruct v; try discriminate. destruct (Float.to_int f) as [i|] eqn:E; simpl in H0; inv H0. - inv H; simpl; auto with va. rewrite E; constructor. + inv H; simpl; auto with va. rewrite E; constructor. Qed. Definition intuoffloat (x: aval) := @@ -1830,9 +1830,9 @@ Definition intuoffloat (x: aval) := Lemma intuoffloat_sound: forall v x w, vmatch v x -> Val.intuoffloat v = Some w -> vmatch w (intuoffloat x). Proof. - unfold Val.intuoffloat; intros. destruct v; try discriminate. + unfold Val.intuoffloat; intros. destruct v; try discriminate. destruct (Float.to_intu f) as [i|] eqn:E; simpl in H0; inv H0. - inv H; simpl; auto with va. rewrite E; constructor. + inv H; simpl; auto with va. rewrite E; constructor. Qed. Definition floatofint (x: aval) := @@ -1874,9 +1874,9 @@ Definition intofsingle (x: aval) := Lemma intofsingle_sound: forall v x w, vmatch v x -> Val.intofsingle v = Some w -> vmatch w (intofsingle x). Proof. - unfold Val.intofsingle; intros. destruct v; try discriminate. + unfold Val.intofsingle; intros. destruct v; try discriminate. destruct (Float32.to_int f) as [i|] eqn:E; simpl in H0; inv H0. - inv H; simpl; auto with va. rewrite E; constructor. + inv H; simpl; auto with va. rewrite E; constructor. Qed. Definition intuofsingle (x: aval) := @@ -1892,9 +1892,9 @@ Definition intuofsingle (x: aval) := Lemma intuofsingle_sound: forall v x w, vmatch v x -> Val.intuofsingle v = Some w -> vmatch w (intuofsingle x). Proof. - unfold Val.intuofsingle; intros. destruct v; try discriminate. + unfold Val.intuofsingle; intros. destruct v; try discriminate. destruct (Float32.to_intu f) as [i|] eqn:E; simpl in H0; inv H0. - inv H; simpl; auto with va. rewrite E; constructor. + inv H; simpl; auto with va. rewrite E; constructor. Qed. Definition singleofint (x: aval) := @@ -2000,7 +2000,7 @@ Proof. intros c [lo hi] x n; simpl; intros R. destruct c; unfold zcmp, proj_sumbool. - (* eq *) - destruct (zlt n lo). rewrite zeq_false by omega. constructor. + destruct (zlt n lo). rewrite zeq_false by omega. constructor. destruct (zlt hi n). rewrite zeq_false by omega. constructor. constructor. - (* ne *) @@ -2055,7 +2055,7 @@ Proof. intros. inv H; simpl; try (apply Int.unsigned_range_2). - omega. - destruct (zlt n0 Int.zwordsize); simpl. -+ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by omega. ++ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by omega. exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. omega. + apply Int.unsigned_range_2. Qed. @@ -2077,7 +2077,7 @@ Lemma cmpu_intv_sound_2: vmatch (Vint n1) v1 -> cmatch (Val.cmpu_bool valid c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (uintv v1) (Int.unsigned n2)). Proof. - intros. rewrite <- Val.swap_cmpu_bool. apply cmpu_intv_sound; auto. + intros. rewrite <- Val.swap_cmpu_bool. apply cmpu_intv_sound; auto. Qed. Definition sintv (v: aval) : Z * Z := @@ -2098,20 +2098,20 @@ Proof. intros. inv H; simpl; try (apply Int.signed_range). - omega. - destruct (zlt n0 Int.zwordsize); simpl. -+ rewrite is_uns_zero_ext in H2. rewrite <- H2. ++ rewrite is_uns_zero_ext in H2. rewrite <- H2. assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; omega). exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. intros. replace (Int.signed (Int.zero_ext n0 n)) with (Int.unsigned (Int.zero_ext n0 n)). - rewrite H. omega. - unfold Int.signed. rewrite zlt_true. auto. - assert (two_p n0 <= Int.half_modulus). - { change Int.half_modulus with (two_p (Int.zwordsize - 1)). + rewrite H. omega. + unfold Int.signed. rewrite zlt_true. auto. + assert (two_p n0 <= Int.half_modulus). + { change Int.half_modulus with (two_p (Int.zwordsize - 1)). apply two_p_monotone. omega. } - omega. + omega. + apply Int.signed_range. - destruct (zlt n0 (Int.zwordsize)); simpl. -+ rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2. - exploit (Int.sign_ext_range n0 n). omega. omega. ++ rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2. + exploit (Int.sign_ext_range n0 n). omega. omega. + apply Int.signed_range. Qed. @@ -2132,8 +2132,8 @@ Lemma cmp_intv_sound_2: vmatch (Vint n1) v1 -> cmatch (Val.cmp_bool c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (sintv v1) (Int.signed n2)). Proof. - intros. rewrite <- Val.swap_cmp_bool. apply cmp_intv_sound; auto. -Qed. + intros. rewrite <- Val.swap_cmp_bool. apply cmp_intv_sound; auto. +Qed. (** Comparisons *) @@ -2184,7 +2184,7 @@ Definition cmp_bool (c: comparison) (v w: aval) : abool := Lemma cmp_bool_sound: forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmp_bool c v w) (cmp_bool c x y). Proof. - intros. + intros. unfold cmp_bool; inversion H; subst; inversion H0; subst; auto using cmatch_top, cmp_intv_sound, cmp_intv_sound_2, cmp_intv_None. - constructor. @@ -2199,7 +2199,7 @@ Definition cmpf_bool (c: comparison) (v w: aval) : abool := Lemma cmpf_bool_sound: forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpf_bool c v w) (cmpf_bool c x y). Proof. - intros. inv H; try constructor; inv H0; constructor. + intros. inv H; try constructor; inv H0; constructor. Qed. Definition cmpfs_bool (c: comparison) (v w: aval) : abool := @@ -2211,7 +2211,7 @@ Definition cmpfs_bool (c: comparison) (v w: aval) : abool := Lemma cmpfs_bool_sound: forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpfs_bool c v w) (cmpfs_bool c x y). Proof. - intros. inv H; try constructor; inv H0; constructor. + intros. inv H; try constructor; inv H0; constructor. Qed. Definition maskzero (x: aval) (mask: int) : abool := @@ -2226,12 +2226,12 @@ Lemma maskzero_sound: vmatch v x -> cmatch (Val.maskzero_bool v mask) (maskzero x mask). Proof. - intros. inv H; simpl; auto with va. + intros. inv H; simpl; auto with va. predSpec Int.eq Int.eq_spec (Int.zero_ext n mask) Int.zero; auto with va. replace (Int.and i mask) with Int.zero. rewrite Int.eq_true. constructor. rewrite is_uns_zero_ext in H1. rewrite Int.zero_ext_and in * by auto. - rewrite <- H1. rewrite Int.and_assoc. rewrite Int.and_commut in H. rewrite H. + rewrite <- H1. rewrite Int.and_assoc. rewrite Int.and_commut in H. rewrite H. rewrite Int.and_zero; auto. destruct (Int.eq (Int.zero_ext n mask) Int.zero); constructor. Qed. @@ -2249,7 +2249,7 @@ Proof. assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns Pbot 1)). { destruct ob; simpl; auto with va. - destruct b; constructor; try omega. + destruct b; constructor; try omega. change 1 with (usize Int.one). apply is_uns_usize. red; intros. apply Int.bits_zero. } @@ -2329,16 +2329,16 @@ Lemma vnormalize_cast: vmatch v (Ifptr p) -> vmatch v (vnormalize chunk (Ifptr p)). Proof. - intros. exploit Mem.load_cast; eauto. exploit Mem.load_type; eauto. + intros. exploit Mem.load_cast; eauto. exploit Mem.load_type; eauto. destruct chunk; simpl; intros. - (* int8signed *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. + rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. - (* int8unsigned *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. + rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. - (* int16signed *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. + rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. - (* int16unsigned *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. + rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. - (* int32 *) auto. - (* int64 *) @@ -2391,7 +2391,7 @@ Proof with (auto using provenance_monotone with va). - constructor... apply is_zero_ext_uns... - unfold provenance; destruct (va_strict tt)... - destruct (va_strict tt)... -- destruct (zlt n2 8); constructor... +- destruct (zlt n2 8); constructor... - destruct (zlt n2 16); constructor... - destruct (va_strict tt)... - destruct (va_strict tt)... @@ -2423,7 +2423,7 @@ Inductive acontent : Type := Definition eq_acontent : forall (c1 c2: acontent), {c1=c2} + {c1<>c2}. Proof. - intros. generalize chunk_eq eq_aval. decide equality. + intros. generalize chunk_eq eq_aval. decide equality. Defined. Record ablock : Type := ABlock { @@ -2494,7 +2494,7 @@ Qed. Remark fst_inval_before: forall hi lo c, fst (inval_before hi lo c) = fst c. Proof. intros. functional induction (inval_before hi lo c); auto. - rewrite IHt. unfold inval_if. destruct c##lo; auto. + rewrite IHt. unfold inval_if. destruct c##lo; auto. destruct (zle (lo + size_chunk chunk) hi); auto. Qed. @@ -2507,7 +2507,7 @@ Program Definition ablock_store (chunk: memory_chunk) (ab: ablock) (i: Z) (av: a vplub av ab.(ab_summary); ab_default := _ |}. Next Obligation. - rewrite fst_inval_before, fst_inval_after. apply ab_default. + rewrite fst_inval_before, fst_inval_after. apply ab_default. Qed. Definition ablock_store_anywhere (chunk: memory_chunk) (ab: ablock) (av: aval) : ablock := @@ -2539,7 +2539,7 @@ Remark loadbytes_load_ext: forall chunk ofs v, Mem.load chunk m' b ofs = Some v -> Mem.load chunk m b ofs = Some v. Proof. intros. exploit Mem.load_loadbytes; eauto. intros [bytes [A B]]. - exploit Mem.load_valid_access; eauto. intros [C D]. + exploit Mem.load_valid_access; eauto. intros [C D]. subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); omega. Qed. @@ -2567,7 +2567,7 @@ Qed. Lemma smatch_ge: forall m b p q, smatch m b p -> pge q p -> smatch m b q. Proof. - intros. destruct H as [A B]. split; intros. + intros. destruct H as [A B]. split; intros. apply vmatch_ge with (Ifptr p); eauto with va. apply pmatch_ge with p; eauto with va. Qed. @@ -2578,26 +2578,26 @@ Lemma In_loadbytes: In byte bytes -> exists ofs', ofs <= ofs' < ofs + n /\ Mem.loadbytes m b ofs' 1 = Some(byte :: nil). Proof. - intros until n. pattern n. + intros until n. pattern n. apply well_founded_ind with (R := Zwf 0). - apply Zwf_well_founded. - intros sz REC ofs bytes LOAD IN. - destruct (zle sz 0). + destruct (zle sz 0). + rewrite (Mem.loadbytes_empty m b ofs sz) in LOAD by auto. inv LOAD. contradiction. + exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes). replace (1 + (sz - 1)) with sz by omega. auto. omega. omega. - intros (bytes1 & bytes2 & LOAD1 & LOAD2 & CONCAT). - subst bytes. + intros (bytes1 & bytes2 & LOAD1 & LOAD2 & CONCAT). + subst bytes. exploit Mem.loadbytes_length. eexact LOAD1. change (nat_of_Z 1) with 1%nat. intros LENGTH1. rewrite in_app_iff in IN. destruct IN. - * destruct bytes1; try discriminate. destruct bytes1; try discriminate. + * destruct bytes1; try discriminate. destruct bytes1; try discriminate. simpl in H. destruct H; try contradiction. subst m0. exists ofs; split. omega. auto. * exploit (REC (sz - 1)). red; omega. eexact LOAD2. auto. - intros (ofs' & A & B). + intros (ofs' & A & B). exists ofs'; split. omega. auto. Qed. @@ -2609,7 +2609,7 @@ Lemma smatch_loadbytes: pmatch b' ofs' p. Proof. intros. exploit In_loadbytes; eauto. intros (ofs1 & A & B). - eapply H0; eauto. + eapply H0; eauto. Qed. Lemma loadbytes_provenance: @@ -2619,7 +2619,7 @@ Lemma loadbytes_provenance: ofs <= ofs' < ofs + n -> In byte bytes. Proof. - intros until n. pattern n. + intros until n. pattern n. apply well_founded_ind with (R := Zwf 0). - apply Zwf_well_founded. - intros sz REC ofs bytes LOAD LOAD1 IN. @@ -2640,15 +2640,15 @@ Lemma storebytes_provenance: In (Fragment (Vptr b'' ofs'') q i) bytes \/ Mem.loadbytes m b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil). Proof. - intros. + intros. assert (EITHER: (b' <> b \/ ofs' + 1 <= ofs \/ ofs + Z.of_nat (length bytes) <= ofs') \/ (b' = b /\ ofs <= ofs' < ofs + Z.of_nat (length bytes))). { destruct (eq_block b' b); auto. - destruct (zle (ofs' + 1) ofs); auto. - destruct (zle (ofs + Z.of_nat (length bytes)) ofs'); auto. - right. split. auto. omega. + destruct (zle (ofs' + 1) ofs); auto. + destruct (zle (ofs + Z.of_nat (length bytes)) ofs'); auto. + right. split. auto. omega. } destruct EITHER as [A | (A & B)]. - right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. omega. @@ -2664,15 +2664,15 @@ Lemma store_provenance: v = Vptr b'' ofs'' /\ (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) \/ Mem.loadbytes m b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil). Proof. - intros. exploit storebytes_provenance; eauto. eapply Mem.store_storebytes; eauto. + intros. exploit storebytes_provenance; eauto. eapply Mem.store_storebytes; eauto. intros [A|A]; auto. left. generalize (encode_val_shape chunk v). intros ENC; inv ENC. - split; auto. rewrite <- H1 in A; destruct A. + congruence. + exploit H5; eauto. intros (j & P & Q); congruence. -- rewrite <- H1 in A; destruct A. +- rewrite <- H1 in A; destruct A. + congruence. - + exploit H3; eauto. intros [byte P]; congruence. + + exploit H3; eauto. intros [byte P]; congruence. - rewrite <- H1 in A; destruct A. + congruence. + exploit H2; eauto. congruence. @@ -2687,18 +2687,18 @@ Lemma smatch_store: Proof. intros. destruct H0 as [A B]. split. - intros chunk' ofs' v' LOAD. destruct v'; auto with va. - exploit Mem.load_pointer_store; eauto. - intros [(P & Q & R & S) | DISJ]. + exploit Mem.load_pointer_store; eauto. + intros [(P & Q & R & S) | DISJ]. + subst. apply vmatch_vplub_l. auto. + apply vmatch_vplub_r. apply A with (chunk := chunk') (ofs := ofs'). rewrite <- LOAD. symmetry. eapply Mem.load_store_other; eauto. -- intros. exploit store_provenance; eauto. intros [[P Q] | P]. -+ subst. +- intros. exploit store_provenance; eauto. intros [[P Q] | P]. ++ subst. assert (V: vmatch (Vptr b'0 ofs') (Ifptr (vplub av p))). { - apply vmatch_vplub_l. auto. + apply vmatch_vplub_l. auto. } - inv V; auto. + inv V; auto. + apply pmatch_vplub. eapply B; eauto. Qed. @@ -2710,22 +2710,22 @@ Lemma smatch_storebytes: smatch m' b' (plub p' p). Proof. intros. destruct H0 as [A B]. split. -- intros. apply vmatch_ifptr. intros bx ofsx EQ; subst v. +- intros. apply vmatch_ifptr. intros bx ofsx EQ; subst v. exploit Mem.load_loadbytes; eauto. intros (bytes' & P & Q). - destruct bytes' as [ | byte1' bytes']. + destruct bytes' as [ | byte1' bytes']. exploit Mem.loadbytes_length; eauto. intros. destruct chunk; discriminate. - generalize (decode_val_shape chunk byte1' bytes'). rewrite <- Q. + generalize (decode_val_shape chunk byte1' bytes'). rewrite <- Q. intros DEC; inv DEC; try contradiction. assert (v = Vptr bx ofsx). { destruct H5 as [E|[E|E]]; rewrite E in H4; destruct v; simpl in H4; congruence. } - exploit In_loadbytes; eauto. eauto with coqlib. - intros (ofs' & X & Y). subst v. + exploit In_loadbytes; eauto. eauto with coqlib. + intros (ofs' & X & Y). subst v. exploit storebytes_provenance; eauto. intros [Z | Z]. - apply pmatch_lub_l. eauto. - apply pmatch_lub_r. eauto. + apply pmatch_lub_l. eauto. + apply pmatch_lub_r. eauto. - intros. exploit storebytes_provenance; eauto. intros [Z | Z]. - apply pmatch_lub_l. eauto. - apply pmatch_lub_r. eauto. + apply pmatch_lub_l. eauto. + apply pmatch_lub_r. eauto. Qed. Definition bmatch (m: mem) (b: block) (ab: ablock) : Prop := @@ -2740,7 +2740,7 @@ Lemma bmatch_ext: Proof. intros. destruct H as [A B]. split; intros. apply smatch_ext with m; auto. - eapply B; eauto. eapply loadbytes_load_ext; eauto. + eapply B; eauto. eapply loadbytes_load_ext; eauto. Qed. Lemma bmatch_inv: @@ -2759,7 +2759,7 @@ Lemma ablock_load_sound: bmatch m b ab -> vmatch v (ablock_load chunk ab ofs). Proof. - intros. destruct H0. eauto. + intros. destruct H0. eauto. Qed. Lemma ablock_load_anywhere_sound: @@ -2768,16 +2768,16 @@ Lemma ablock_load_anywhere_sound: bmatch m b ab -> vmatch v (ablock_load_anywhere chunk ab). Proof. - intros. destruct H0. destruct H0. unfold ablock_load_anywhere. - eapply vnormalize_cast; eauto. + intros. destruct H0. destruct H0. unfold ablock_load_anywhere. + eapply vnormalize_cast; eauto. Qed. Lemma ablock_init_sound: forall m b p, smatch m b p -> bmatch m b (ablock_init p). Proof. - intros; split; auto; intros. + intros; split; auto; intros. unfold ablock_load, ablock_init; simpl. rewrite ZMap.gi. - eapply vnormalize_cast; eauto. eapply H; eauto. + eapply vnormalize_cast; eauto. eapply H; eauto. Qed. Lemma ablock_store_anywhere_sound: @@ -2788,14 +2788,14 @@ Lemma ablock_store_anywhere_sound: bmatch m' b' (ablock_store_anywhere chunk ab av). Proof. intros. destruct H0 as [A B]. unfold ablock_store_anywhere. - apply ablock_init_sound. eapply smatch_store; eauto. + apply ablock_init_sound. eapply smatch_store; eauto. Qed. Remark inval_after_outside: forall i lo hi c, i < lo \/ i > hi -> (inval_after lo hi c)##i = c##i. Proof. intros until c. functional induction (inval_after lo hi c); intros. - rewrite IHt by omega. apply ZMap.gso. unfold ZIndexed.t; omega. + rewrite IHt by omega. apply ZMap.gso. unfold ZIndexed.t; omega. auto. Qed. @@ -2805,7 +2805,7 @@ Remark inval_after_contents: c##i = ACval chunk av /\ (i < lo \/ i > hi). Proof. intros until c. functional induction (inval_after lo hi c); intros. - destruct (zeq i hi). + destruct (zeq i hi). subst i. rewrite inval_after_outside in H by omega. rewrite ZMap.gss in H. discriminate. exploit IHt; eauto. intros [A B]. rewrite ZMap.gso in A by auto. split. auto. omega. split. auto. omega. @@ -2815,9 +2815,9 @@ Remark inval_before_outside: forall i hi lo c, i < lo \/ i >= hi -> (inval_before hi lo c)##i = c##i. Proof. intros until c. functional induction (inval_before hi lo c); intros. - rewrite IHt by omega. unfold inval_if. destruct (c##lo); auto. + rewrite IHt by omega. unfold inval_if. destruct (c##lo); auto. destruct (zle (lo + size_chunk chunk) hi); auto. - apply ZMap.gso. unfold ZIndexed.t; omega. + apply ZMap.gso. unfold ZIndexed.t; omega. auto. Qed. @@ -2828,15 +2828,15 @@ Remark inval_before_contents_1: Proof. intros until c. functional induction (inval_before hi lo c); intros. - destruct (zeq lo i). -+ subst i. rewrite inval_before_outside in H0 by omega. - unfold inval_if in H0. destruct (c##lo) eqn:C. congruence. ++ subst i. rewrite inval_before_outside in H0 by omega. + unfold inval_if in H0. destruct (c##lo) eqn:C. congruence. destruct (zle (lo + size_chunk chunk0) hi). - rewrite C in H0; inv H0. auto. + rewrite C in H0; inv H0. auto. rewrite ZMap.gss in H0. congruence. -+ exploit IHt. omega. auto. intros [A B]; split; auto. ++ exploit IHt. omega. auto. intros [A B]; split; auto. unfold inval_if in A. destruct (c##lo) eqn:C. auto. destruct (zle (lo + size_chunk chunk0) hi); auto. - rewrite ZMap.gso in A; auto. + rewrite ZMap.gso in A; auto. - omegaContradiction. Qed. @@ -2850,12 +2850,12 @@ Remark inval_before_contents: (inval_before i (i - 7) c)##j = ACval chunk' av' -> c##j = ACval chunk' av' /\ (j + size_chunk chunk' <= i \/ i <= j). Proof. - intros. destruct (zlt j (i - 7)). - rewrite inval_before_outside in H by omega. + intros. destruct (zlt j (i - 7)). + rewrite inval_before_outside in H by omega. split. auto. left. generalize (max_size_chunk chunk'); omega. - destruct (zlt j i). + destruct (zlt j i). exploit inval_before_contents_1; eauto. omega. tauto. - rewrite inval_before_outside in H by omega. + rewrite inval_before_outside in H by omega. split. auto. omega. Qed. @@ -2863,12 +2863,12 @@ Lemma ablock_store_contents: forall chunk ab i av j chunk' av', (ablock_store chunk ab i av).(ab_contents)##j = ACval chunk' av' -> (i = j /\ chunk' = chunk /\ av' = av) - \/ (ab.(ab_contents)##j = ACval chunk' av' + \/ (ab.(ab_contents)##j = ACval chunk' av' /\ (j + size_chunk chunk' <= i \/ i + size_chunk chunk <= j)). Proof. unfold ablock_store; simpl; intros. - destruct (zeq i j). - subst j. rewrite ZMap.gss in H. inv H; auto. + destruct (zeq i j). + subst j. rewrite ZMap.gss in H. inv H; auto. right. rewrite ZMap.gso in H by auto. exploit inval_before_contents; eauto. intros [A B]. exploit inval_after_contents; eauto. intros [C D]. @@ -2891,20 +2891,20 @@ Lemma ablock_store_sound: bmatch m' b (ablock_store chunk ab ofs av). Proof. intros until av; intros STORE BIN VIN. destruct BIN as [BIN1 BIN2]. split. - eapply smatch_store; eauto. + eapply smatch_store; eauto. intros chunk' ofs' v' LOAD. assert (SUMMARY: vmatch v' (vnormalize chunk' (Ifptr (vplub av ab.(ab_summary))))). { exploit smatch_store; eauto. intros [A B]. eapply vnormalize_cast; eauto. } - unfold ablock_load. + unfold ablock_load. destruct ((ab_contents (ablock_store chunk ab ofs av)) ## ofs') as [ | chunk1 av1] eqn:C. apply SUMMARY. destruct (chunk_compat chunk' chunk1) eqn:COMPAT; auto. exploit chunk_compat_true; eauto. intros (U & V & W). exploit ablock_store_contents; eauto. intros [(P & Q & R) | (P & Q)]. - (* same offset and compatible chunks *) - subst. - assert (v' = Val.load_result chunk' v). - { exploit Mem.load_store_similar_2; eauto. congruence. } + subst. + assert (v' = Val.load_result chunk' v). + { exploit Mem.load_store_similar_2; eauto. congruence. } subst v'. apply vnormalize_sound; auto. - (* disjoint load/store *) assert (Mem.load chunk' m b ofs' = Some v'). @@ -2920,7 +2920,7 @@ Lemma ablock_loadbytes_sound: In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' (ablock_loadbytes ab). Proof. - intros. destruct H0. eapply smatch_loadbytes; eauto. + intros. destruct H0. eapply smatch_loadbytes; eauto. Qed. Lemma ablock_storebytes_anywhere_sound: @@ -2937,7 +2937,7 @@ Qed. Lemma ablock_storebytes_contents: forall ab p i sz j chunk' av', (ablock_storebytes ab p i sz).(ab_contents)##j = ACval chunk' av' -> - ab.(ab_contents)##j = ACval chunk' av' + ab.(ab_contents)##j = ACval chunk' av' /\ (j + size_chunk chunk' <= i \/ i + Zmax sz 0 <= j). Proof. unfold ablock_storebytes; simpl; intros. @@ -2954,15 +2954,15 @@ Lemma ablock_storebytes_sound: bmatch m b ab -> bmatch m' b (ablock_storebytes ab p ofs sz). Proof. - intros until sz; intros STORE LENGTH CONTENTS BM. destruct BM as [BM1 BM2]. split. - eapply smatch_storebytes; eauto. + intros until sz; intros STORE LENGTH CONTENTS BM. destruct BM as [BM1 BM2]. split. + eapply smatch_storebytes; eauto. intros chunk' ofs' v' LOAD'. assert (SUMMARY: vmatch v' (vnormalize chunk' (Ifptr (plub p ab.(ab_summary))))). { exploit smatch_storebytes; eauto. intros [A B]. eapply vnormalize_cast; eauto. } - unfold ablock_load. + unfold ablock_load. destruct (ab_contents (ablock_storebytes ab p ofs sz))##ofs' eqn:C. exact SUMMARY. - destruct (chunk_compat chunk' chunk) eqn:COMPAT; auto. + destruct (chunk_compat chunk' chunk) eqn:COMPAT; auto. exploit chunk_compat_true; eauto. intros (U & V & W). exploit ablock_storebytes_contents; eauto. intros [A B]. assert (Mem.load chunk' m b ofs' = Some v'). @@ -2975,7 +2975,7 @@ Qed. Definition bbeq (ab1 ab2: ablock) : bool := eq_aptr ab1.(ab_summary) ab2.(ab_summary) && - PTree.beq (fun c1 c2 => proj_sumbool (eq_acontent c1 c2)) + PTree.beq (fun c1 c2 => proj_sumbool (eq_acontent c1 c2)) (snd ab1.(ab_contents)) (snd ab2.(ab_contents)). Lemma bbeq_load: @@ -2989,7 +2989,7 @@ Proof. - rewrite PTree.beq_correct in H1. assert (A: forall i, ZMap.get i (ab_contents ab1) = ZMap.get i (ab_contents ab2)). { - intros. unfold ZMap.get, PMap.get. set (j := ZIndexed.index i). + intros. unfold ZMap.get, PMap.get. set (j := ZIndexed.index i). specialize (H1 j). destruct (snd (ab_contents ab1))!j; destruct (snd (ab_contents ab2))!j; try contradiction. InvBooleans; auto. @@ -3004,9 +3004,9 @@ Lemma bbeq_sound: bbeq ab1 ab2 = true -> forall m b, bmatch m b ab1 <-> bmatch m b ab2. Proof. - intros. exploit bbeq_load; eauto. intros [A B]. - unfold bmatch. rewrite A. intuition. rewrite <- B; eauto. rewrite B; eauto. -Qed. + intros. exploit bbeq_load; eauto. intros [A B]. + unfold bmatch. rewrite A. intuition. rewrite <- B; eauto. rewrite B; eauto. +Qed. (** Least upper bound *) @@ -3039,11 +3039,11 @@ Lemma get_combine_contentmaps: ZMap.get i (combine_contentmaps m1 m2) = combine_acontents (ZMap.get i m1) (ZMap.get i m2). Proof. intros. destruct m1 as [dfl1 pt1]. destruct m2 as [dfl2 pt2]; simpl in *. - subst dfl1 dfl2. unfold combine_contentmaps, ZMap.get, PMap.get, fst, snd. - set (j := ZIndexed.index i). + subst dfl1 dfl2. unfold combine_contentmaps, ZMap.get, PMap.get, fst, snd. + set (j := ZIndexed.index i). rewrite PTree.gcombine by auto. destruct (pt1!j) as [[]|]; destruct (pt2!j) as [[]|]; simpl; auto. - destruct (chunk_eq chunk chunk0); auto. + destruct (chunk_eq chunk chunk0); auto. Qed. Lemma smatch_lub_l: @@ -3051,7 +3051,7 @@ Lemma smatch_lub_l: Proof. intros. destruct H as [A B]. split; intros. change (vmatch v (vlub (Ifptr p) (Ifptr q))). apply vmatch_lub_l. eapply A; eauto. - apply pmatch_lub_l. eapply B; eauto. + apply pmatch_lub_l. eapply B; eauto. Qed. Lemma smatch_lub_r: @@ -3059,14 +3059,14 @@ Lemma smatch_lub_r: Proof. intros. destruct H as [A B]. split; intros. change (vmatch v (vlub (Ifptr p) (Ifptr q))). apply vmatch_lub_r. eapply A; eauto. - apply pmatch_lub_r. eapply B; eauto. + apply pmatch_lub_r. eapply B; eauto. Qed. Lemma bmatch_lub_l: forall m b x y, bmatch m b x -> bmatch m b (blub x y). Proof. intros. destruct H as [BM1 BM2]. split; unfold blub; simpl. -- apply smatch_lub_l; auto. +- apply smatch_lub_l; auto. - intros. assert (SUMMARY: vmatch v (vnormalize chunk (Ifptr (plub (ab_summary x) (ab_summary y)))) ). @@ -3077,14 +3077,14 @@ Proof. unfold combine_acontents; destruct (ab_contents x)##ofs, (ab_contents y)##ofs; auto. destruct (chunk_eq chunk0 chunk1); auto. subst chunk0. destruct (chunk_compat chunk chunk1); auto. - intros. eapply vmatch_ge; eauto. apply vnormalize_monotone. apply vge_lub_l. + intros. eapply vmatch_ge; eauto. apply vnormalize_monotone. apply vge_lub_l. Qed. Lemma bmatch_lub_r: forall m b x y, bmatch m b y -> bmatch m b (blub x y). Proof. intros. destruct H as [BM1 BM2]. split; unfold blub; simpl. -- apply smatch_lub_r; auto. +- apply smatch_lub_r; auto. - intros. assert (SUMMARY: vmatch v (vnormalize chunk (Ifptr (plub (ab_summary x) (ab_summary y)))) ). @@ -3095,7 +3095,7 @@ Proof. unfold combine_acontents; destruct (ab_contents x)##ofs, (ab_contents y)##ofs; auto. destruct (chunk_eq chunk0 chunk1); auto. subst chunk0. destruct (chunk_compat chunk chunk1); auto. - intros. eapply vmatch_ge; eauto. apply vnormalize_monotone. apply vge_lub_r. + intros. eapply vmatch_ge; eauto. apply vnormalize_monotone. apply vge_lub_r. Qed. (** * Abstracting read-only global variables *) @@ -3119,7 +3119,7 @@ Proof. intros; red; intros. exploit H0; eauto. intros (A & B & C). split; auto. split. - exploit Mem.store_valid_access_3; eauto. intros [P _]. apply bmatch_inv with m; auto. -+ intros. eapply Mem.loadbytes_store_other; eauto. ++ intros. eapply Mem.loadbytes_store_other; eauto. left. red; intros; subst b0. elim (C ofs). apply Mem.perm_cur_max. apply P. generalize (size_chunk_pos chunk); omega. - intros; red; intros; elim (C ofs0). eauto with mem. @@ -3133,7 +3133,7 @@ Lemma romatch_storebytes: Proof. intros; red; intros. exploit H0; eauto. intros (A & B & C). split; auto. split. - apply bmatch_inv with m; auto. - intros. eapply Mem.loadbytes_storebytes_disjoint; eauto. + intros. eapply Mem.loadbytes_storebytes_disjoint; eauto. destruct (eq_block b0 b); auto. subst b0. right; red; unfold Intv.In; simpl; red; intros. elim (C x). apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto. - intros; red; intros; elim (C ofs0). eauto with mem. @@ -3149,7 +3149,7 @@ Proof. intros; red; intros. exploit H; eauto. intros (A & B & C). split. auto. split. apply bmatch_ext with m; auto. intros. eapply H0; eauto. - intros; red; intros. elim (C ofs). eapply H1; eauto. + intros; red; intros. elim (C ofs). eapply H1; eauto. Qed. Lemma romatch_free: @@ -3158,8 +3158,8 @@ Lemma romatch_free: romatch m rm -> romatch m' rm. Proof. - intros. apply romatch_ext with m; auto. - intros. eapply Mem.loadbytes_free_2; eauto. + intros. apply romatch_ext with m; auto. + intros. eapply Mem.loadbytes_free_2; eauto. intros. eauto with mem. Qed. @@ -3170,7 +3170,7 @@ Lemma romatch_alloc: romatch m rm -> romatch m' rm. Proof. - intros. apply romatch_ext with m; auto. + intros. apply romatch_ext with m; auto. intros. rewrite <- H3; symmetry. eapply Mem.loadbytes_alloc_unchanged; eauto. apply H0. congruence. intros. eapply Mem.perm_alloc_4; eauto. apply Mem.valid_not_valid_diff with m; eauto with mem. @@ -3191,7 +3191,7 @@ Record mmatch (m: mem) (am: amem) : Prop := mk_mem_match { bc b = BCstack -> bmatch m b am.(am_stack); mmatch_glob: forall id ab b, - bc b = BCglob id -> + bc b = BCglob id -> am.(am_glob)!id = Some ab -> bmatch m b ab; mmatch_nonstack: forall b, @@ -3323,18 +3323,18 @@ Theorem load_sound: pmatch b ofs p -> vmatch v (load chunk rm am p). Proof. - intros. unfold load. inv H2. + intros. unfold load. inv H2. - (* Gl id ofs *) - destruct (rm!id) as [ab|] eqn:RM. - eapply ablock_load_sound; eauto. eapply H0; eauto. + destruct (rm!id) as [ab|] eqn:RM. + eapply ablock_load_sound; eauto. eapply H0; eauto. destruct (am_glob am)!id as [ab|] eqn:AM. - eapply ablock_load_sound; eauto. eapply mmatch_glob; eauto. + eapply ablock_load_sound; eauto. eapply mmatch_glob; eauto. eapply vnormalize_cast; eauto. eapply mmatch_nonstack; eauto; congruence. - (* Glo id *) - destruct (rm!id) as [ab|] eqn:RM. - eapply ablock_load_anywhere_sound; eauto. eapply H0; eauto. + destruct (rm!id) as [ab|] eqn:RM. + eapply ablock_load_anywhere_sound; eauto. eapply H0; eauto. destruct (am_glob am)!id as [ab|] eqn:AM. - eapply ablock_load_anywhere_sound; eauto. eapply mmatch_glob; eauto. + eapply ablock_load_anywhere_sound; eauto. eapply mmatch_glob; eauto. eapply vnormalize_cast; eauto. eapply mmatch_nonstack; eauto; congruence. - (* Glob *) eapply vnormalize_cast; eauto. eapply mmatch_nonstack; eauto. congruence. congruence. @@ -3343,7 +3343,7 @@ Proof. - (* Stack *) eapply ablock_load_anywhere_sound; eauto. eapply mmatch_stack; eauto. - (* Nonstack *) - eapply vnormalize_cast; eauto. eapply mmatch_nonstack; eauto. + eapply vnormalize_cast; eauto. eapply mmatch_nonstack; eauto. - (* Top *) eapply vnormalize_cast; eauto. eapply mmatch_top; eauto. Qed. @@ -3357,7 +3357,7 @@ Theorem loadv_sound: vmatch v (loadv chunk rm am aaddr). Proof. intros. destruct addr; simpl in H; try discriminate. - eapply load_sound; eauto. apply match_aptr_of_aval; auto. + eapply load_sound; eauto. apply match_aptr_of_aval; auto. Qed. Theorem store_sound: @@ -3372,27 +3372,27 @@ Proof. unfold store; constructor; simpl; intros. - (* Stack *) assert (DFL: bc b <> BCstack -> bmatch m' b0 (am_stack am)). - { intros. apply bmatch_inv with m. eapply mmatch_stack; eauto. + { intros. apply bmatch_inv with m. eapply mmatch_stack; eauto. intros. eapply Mem.loadbytes_store_other; eauto. left; congruence. } inv PM; try (apply DFL; congruence). - + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. - eapply ablock_store_sound; eauto. eapply mmatch_stack; eauto. - + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. - eapply ablock_store_anywhere_sound; eauto. eapply mmatch_stack; eauto. + + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. + eapply ablock_store_sound; eauto. eapply mmatch_stack; eauto. + + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. + eapply ablock_store_anywhere_sound; eauto. eapply mmatch_stack; eauto. + eapply ablock_store_anywhere_sound; eauto. eapply mmatch_stack; eauto. - (* Globals *) rename b0 into b'. - assert (DFL: bc b <> BCglob id -> (am_glob am)!id = Some ab -> + assert (DFL: bc b <> BCglob id -> (am_glob am)!id = Some ab -> bmatch m' b' ab). { intros. apply bmatch_inv with m. eapply mmatch_glob; eauto. intros. eapply Mem.loadbytes_store_other; eauto. left; congruence. } - inv PM. + inv PM. + rewrite PTree.gsspec in H0. destruct (peq id id0). subst id0; inv H0. assert (b' = b) by (eapply bc_glob; eauto). subst b'. eapply ablock_store_sound; eauto. - destruct (am_glob am)!id as [ab0|] eqn:GL. + destruct (am_glob am)!id as [ab0|] eqn:GL. eapply mmatch_glob; eauto. apply ablock_init_sound. eapply mmatch_nonstack; eauto; congruence. eapply DFL; eauto. congruence. @@ -3400,13 +3400,13 @@ Proof. subst id0; inv H0. assert (b' = b) by (eapply bc_glob; eauto). subst b'. eapply ablock_store_anywhere_sound; eauto. - destruct (am_glob am)!id as [ab0|] eqn:GL. + destruct (am_glob am)!id as [ab0|] eqn:GL. eapply mmatch_glob; eauto. apply ablock_init_sound. eapply mmatch_nonstack; eauto; congruence. eapply DFL; eauto. congruence. + rewrite PTree.gempty in H0; congruence. + eapply DFL; eauto. congruence. - + eapply DFL; eauto. congruence. + + eapply DFL; eauto. congruence. + rewrite PTree.gempty in H0; congruence. + rewrite PTree.gempty in H0; congruence. @@ -3434,7 +3434,7 @@ Theorem storev_sound: vmatch v av -> mmatch m' (storev chunk am aaddr av). Proof. - intros. destruct addr; simpl in H; try discriminate. + intros. destruct addr; simpl in H; try discriminate. eapply store_sound; eauto. apply match_aptr_of_aval; auto. Qed. @@ -3451,21 +3451,21 @@ Proof. destruct (rm!id) as [ab|] eqn:RM. exploit H0; eauto. intros (A & B & C). eapply ablock_loadbytes_sound; eauto. destruct (am_glob am)!id as [ab|] eqn:GL. - eapply ablock_loadbytes_sound; eauto. eapply mmatch_glob; eauto. + eapply ablock_loadbytes_sound; eauto. eapply mmatch_glob; eauto. eapply smatch_loadbytes; eauto. eapply mmatch_nonstack; eauto with va. - (* Glo id *) destruct (rm!id) as [ab|] eqn:RM. exploit H0; eauto. intros (A & B & C). eapply ablock_loadbytes_sound; eauto. destruct (am_glob am)!id as [ab|] eqn:GL. - eapply ablock_loadbytes_sound; eauto. eapply mmatch_glob; eauto. + eapply ablock_loadbytes_sound; eauto. eapply mmatch_glob; eauto. eapply smatch_loadbytes; eauto. eapply mmatch_nonstack; eauto with va. - (* Glob *) eapply smatch_loadbytes; eauto. eapply mmatch_nonstack; eauto with va. - (* Stk ofs *) - eapply ablock_loadbytes_sound; eauto. eapply mmatch_stack; eauto. + eapply ablock_loadbytes_sound; eauto. eapply mmatch_stack; eauto. - (* Stack *) eapply ablock_loadbytes_sound; eauto. eapply mmatch_stack; eauto. -- (* Nonstack *) +- (* Nonstack *) eapply smatch_loadbytes; eauto. eapply mmatch_nonstack; eauto with va. - (* Top *) eapply smatch_loadbytes; eauto. eapply mmatch_top; eauto with va. @@ -3484,27 +3484,27 @@ Proof. unfold storebytes; constructor; simpl; intros. - (* Stack *) assert (DFL: bc b <> BCstack -> bmatch m' b0 (am_stack am)). - { intros. apply bmatch_inv with m. eapply mmatch_stack; eauto. + { intros. apply bmatch_inv with m. eapply mmatch_stack; eauto. intros. eapply Mem.loadbytes_storebytes_other; eauto. left; congruence. } inv PM; try (apply DFL; congruence). - + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. - eapply ablock_storebytes_sound; eauto. eapply mmatch_stack; eauto. - + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. - eapply ablock_storebytes_anywhere_sound; eauto. eapply mmatch_stack; eauto. + + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. + eapply ablock_storebytes_sound; eauto. eapply mmatch_stack; eauto. + + assert (b0 = b) by (eapply bc_stack; eauto). subst b0. + eapply ablock_storebytes_anywhere_sound; eauto. eapply mmatch_stack; eauto. + eapply ablock_storebytes_anywhere_sound; eauto. eapply mmatch_stack; eauto. - (* Globals *) rename b0 into b'. - assert (DFL: bc b <> BCglob id -> (am_glob am)!id = Some ab -> + assert (DFL: bc b <> BCglob id -> (am_glob am)!id = Some ab -> bmatch m' b' ab). { intros. apply bmatch_inv with m. eapply mmatch_glob; eauto. intros. eapply Mem.loadbytes_storebytes_other; eauto. left; congruence. } - inv PM. + inv PM. + rewrite PTree.gsspec in H0. destruct (peq id id0). subst id0; inv H0. assert (b' = b) by (eapply bc_glob; eauto). subst b'. eapply ablock_storebytes_sound; eauto. - destruct (am_glob am)!id as [ab0|] eqn:GL. + destruct (am_glob am)!id as [ab0|] eqn:GL. eapply mmatch_glob; eauto. apply ablock_init_sound. eapply mmatch_nonstack; eauto; congruence. eapply DFL; eauto. congruence. @@ -3512,13 +3512,13 @@ Proof. subst id0; inv H0. assert (b' = b) by (eapply bc_glob; eauto). subst b'. eapply ablock_storebytes_anywhere_sound; eauto. - destruct (am_glob am)!id as [ab0|] eqn:GL. + destruct (am_glob am)!id as [ab0|] eqn:GL. eapply mmatch_glob; eauto. apply ablock_init_sound. eapply mmatch_nonstack; eauto; congruence. eapply DFL; eauto. congruence. + rewrite PTree.gempty in H0; congruence. + eapply DFL; eauto. congruence. - + eapply DFL; eauto. congruence. + + eapply DFL; eauto. congruence. + rewrite PTree.gempty in H0; congruence. + rewrite PTree.gempty in H0; congruence. @@ -3550,7 +3550,7 @@ Proof. - apply bmatch_ext with m; eauto with va. - apply smatch_ext with m; auto with va. - apply smatch_ext with m; auto with va. -- red; intros. exploit mmatch_below0; eauto. xomega. +- red; intros. exploit mmatch_below0; eauto. xomega. Qed. Lemma mmatch_free: @@ -3559,16 +3559,16 @@ Lemma mmatch_free: mmatch m am -> mmatch m' am. Proof. - intros. apply mmatch_ext with m; auto. - intros. eapply Mem.loadbytes_free_2; eauto. - erewrite <- Mem.nextblock_free by eauto. xomega. + intros. apply mmatch_ext with m; auto. + intros. eapply Mem.loadbytes_free_2; eauto. + erewrite <- Mem.nextblock_free by eauto. xomega. Qed. Lemma mmatch_top': forall m am, mmatch m am -> mmatch m mtop. Proof. intros. constructor; simpl; intros. -- apply ablock_init_sound. apply smatch_ge with (ab_summary (am_stack am)). +- apply ablock_init_sound. apply smatch_ge with (ab_summary (am_stack am)). eapply mmatch_stack; eauto. constructor. - rewrite PTree.gempty in H1; discriminate. - eapply smatch_ge. eapply mmatch_nonstack; eauto. constructor. @@ -3589,16 +3589,16 @@ Lemma mbeq_sound: Proof. unfold mbeq; intros. InvBooleans. rewrite PTree.beq_correct in H1. split; intros M; inv M; constructor; intros. -- erewrite <- bbeq_sound; eauto. -- specialize (H1 id). rewrite H4 in H1. destruct (am_glob m1)!id eqn:G; try contradiction. - erewrite <- bbeq_sound; eauto. -- rewrite <- H; eauto. +- erewrite <- bbeq_sound; eauto. +- specialize (H1 id). rewrite H4 in H1. destruct (am_glob m1)!id eqn:G; try contradiction. + erewrite <- bbeq_sound; eauto. +- rewrite <- H; eauto. - rewrite <- H0; eauto. - auto. -- erewrite bbeq_sound; eauto. -- specialize (H1 id). rewrite H4 in H1. destruct (am_glob m2)!id eqn:G; try contradiction. - erewrite bbeq_sound; eauto. -- rewrite H; eauto. +- erewrite bbeq_sound; eauto. +- specialize (H1 id). rewrite H4 in H1. destruct (am_glob m2)!id eqn:G; try contradiction. + erewrite bbeq_sound; eauto. +- rewrite H; eauto. - rewrite H0; eauto. - auto. Qed. @@ -3620,14 +3620,14 @@ Definition mlub (m1 m2: amem) : amem := Lemma mmatch_lub_l: forall m x y, mmatch m x -> mmatch m (mlub x y). Proof. - intros. inv H. constructor; simpl; intros. -- apply bmatch_lub_l; auto. -- rewrite PTree.gcombine in H0 by auto. unfold combine_ablock in H0. + intros. inv H. constructor; simpl; intros. +- apply bmatch_lub_l; auto. +- rewrite PTree.gcombine in H0 by auto. unfold combine_ablock in H0. destruct (am_glob x)!id as [b1|] eqn:G1; destruct (am_glob y)!id as [b2|] eqn:G2; inv H0. - apply bmatch_lub_l; eauto. -- apply smatch_lub_l; auto. + apply bmatch_lub_l; eauto. +- apply smatch_lub_l; auto. - apply smatch_lub_l; auto. - auto. Qed. @@ -3635,14 +3635,14 @@ Qed. Lemma mmatch_lub_r: forall m x y, mmatch m y -> mmatch m (mlub x y). Proof. - intros. inv H. constructor; simpl; intros. -- apply bmatch_lub_r; auto. -- rewrite PTree.gcombine in H0 by auto. unfold combine_ablock in H0. + intros. inv H. constructor; simpl; intros. +- apply bmatch_lub_r; auto. +- rewrite PTree.gcombine in H0 by auto. unfold combine_ablock in H0. destruct (am_glob x)!id as [b1|] eqn:G1; destruct (am_glob y)!id as [b2|] eqn:G2; inv H0. - apply bmatch_lub_r; eauto. -- apply smatch_lub_r; auto. + apply bmatch_lub_r; eauto. +- apply smatch_lub_r; auto. - apply smatch_lub_r; auto. - auto. Qed. @@ -3658,9 +3658,9 @@ Lemma genv_match_exten: (forall b, bc1 b = BCother -> bc2 b = BCother) -> genv_match bc2 ge. Proof. - intros. destruct H as [A B]. split; intros. -- rewrite <- H0. eauto. -- exploit B; eauto. destruct (bc1 b) eqn:BC1. + intros. destruct H as [A B]. split; intros. +- rewrite <- H0. eauto. +- exploit B; eauto. destruct (bc1 b) eqn:BC1. + intuition congruence. + rewrite H0 in BC1. intuition congruence. + intuition congruence. @@ -3678,19 +3678,19 @@ Proof. assert (PM: forall b ofs p, pmatch bc1 b ofs p -> pmatch bc1 b ofs (ab_summary ab) -> pmatch bc2 b ofs p). { intros. - assert (pmatch bc1 b0 ofs Glob) by (eapply pmatch_ge; eauto). + assert (pmatch bc1 b0 ofs Glob) by (eapply pmatch_ge; eauto). inv H5. - assert (bc2 b0 = BCglob id0) by (rewrite H0; auto). + assert (bc2 b0 = BCglob id0) by (rewrite H0; auto). inv H3; econstructor; eauto with va. } assert (VM: forall v x, vmatch bc1 v x -> vmatch bc1 v (Ifptr (ab_summary ab)) -> vmatch bc2 v x). { - intros. inv H3; constructor; auto; inv H4; eapply PM; eauto. + intros. inv H3; constructor; auto; inv H4; eapply PM; eauto. } destruct B as [[B1 B2] B3]. split. split. -- intros. apply VM; eauto. -- intros. apply PM; eauto. -- intros. apply VM; eauto. +- intros. apply VM; eauto. +- intros. apply PM; eauto. +- intros. apply VM; eauto. Qed. Definition bc_incr (bc1 bc2: block_classification) : Prop := @@ -3703,28 +3703,28 @@ Hypothesis INCR: bc_incr bc1 bc2. Lemma pmatch_incr: forall b ofs p, pmatch bc1 b ofs p -> pmatch bc2 b ofs p. Proof. - induction 1; + induction 1; assert (bc2 b = bc1 b) by (apply INCR; congruence); - econstructor; eauto with va. rewrite H0; eauto. + econstructor; eauto with va. rewrite H0; eauto. Qed. Lemma vmatch_incr: forall v x, vmatch bc1 v x -> vmatch bc2 v x. Proof. - induction 1; constructor; auto; apply pmatch_incr; auto. + induction 1; constructor; auto; apply pmatch_incr; auto. Qed. Lemma smatch_incr: forall m b p, smatch bc1 m b p -> smatch bc2 m b p. Proof. - intros. destruct H as [A B]. split; intros. - apply vmatch_incr; eauto. + intros. destruct H as [A B]. split; intros. + apply vmatch_incr; eauto. apply pmatch_incr; eauto. Qed. Lemma bmatch_incr: forall m b ab, bmatch bc1 m b ab -> bmatch bc2 m b ab. Proof. - intros. destruct H as [B1 B2]. split. - apply smatch_incr; auto. - intros. apply vmatch_incr; eauto. + intros. destruct H as [B1 B2]. split. + apply smatch_incr; auto. + intros. apply vmatch_incr; eauto. Qed. End MATCH_INCR. @@ -3737,7 +3737,7 @@ Definition inj_of_bc (bc: block_classification) : meminj := Lemma inj_of_bc_valid: forall (bc: block_classification) b, bc b <> BCinvalid -> inj_of_bc bc b = Some(b, 0). Proof. - intros. unfold inj_of_bc. destruct (bc b); congruence. + intros. unfold inj_of_bc. destruct (bc b); congruence. Qed. Lemma inj_of_bc_inv: @@ -3750,44 +3750,44 @@ Qed. Lemma pmatch_inj: forall bc b ofs p, pmatch bc b ofs p -> inj_of_bc bc b = Some(b, 0). Proof. - intros. apply inj_of_bc_valid. inv H; congruence. + intros. apply inj_of_bc_valid. inv H; congruence. Qed. Lemma vmatch_inj: forall bc v x, vmatch bc v x -> Val.inject (inj_of_bc bc) v v. Proof. - induction 1; econstructor. - eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. - eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. + induction 1; econstructor. + eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. + eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. Qed. Lemma vmatch_list_inj: forall bc vl xl, list_forall2 (vmatch bc) vl xl -> Val.inject_list (inj_of_bc bc) vl vl. Proof. - induction 1; constructor. eapply vmatch_inj; eauto. auto. -Qed. + induction 1; constructor. eapply vmatch_inj; eauto. auto. +Qed. Lemma mmatch_inj: forall bc m am, mmatch bc m am -> bc_below bc (Mem.nextblock m) -> Mem.inject (inj_of_bc bc) m m. Proof. intros. constructor. constructor. - (* perms *) - intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. auto. + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + rewrite Zplus_0_r. auto. - (* alignment *) - intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - apply Zdivide_0. + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + apply Zdivide_0. - (* contents *) - intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + rewrite Zplus_0_r. set (mv := ZMap.get ofs (Mem.mem_contents m)#b1). assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)). { Local Transparent Mem.loadbytes. - unfold Mem.loadbytes. rewrite pred_dec_true. reflexivity. + unfold Mem.loadbytes. rewrite pred_dec_true. reflexivity. red; intros. replace ofs0 with ofs by omega. auto. } - destruct mv; econstructor. destruct v; econstructor. + destruct mv; econstructor. destruct v; econstructor. apply inj_of_bc_valid. assert (PM: pmatch bc b i Ptop). { exploit mmatch_top; eauto. intros [P Q]. @@ -3795,17 +3795,17 @@ Proof. inv PM; auto. rewrite Int.add_zero; auto. - (* free blocks *) - intros. unfold inj_of_bc. erewrite bc_below_invalid; eauto. + intros. unfold inj_of_bc. erewrite bc_below_invalid; eauto. - (* mapped blocks *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. apply H0; auto. - (* overlap *) - red; intros. + red; intros. exploit inj_of_bc_inv. eexact H2. intros (A1 & B & C); subst. exploit inj_of_bc_inv. eexact H3. intros (A2 & B & C); subst. auto. - (* overflow *) - intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r. split. omega. apply Int.unsigned_range_2. Qed. @@ -3814,8 +3814,8 @@ Lemma inj_of_bc_preserves_globals: Proof. intros. destruct H as [A B]. split. intros. apply inj_of_bc_valid. rewrite A in H. congruence. - split. intros. apply inj_of_bc_valid. apply B. eapply Genv.genv_vars_range; eauto. - intros. exploit inj_of_bc_inv; eauto. intros (P & Q & R). auto. + split. intros. apply inj_of_bc_valid. apply B. eapply Genv.genv_vars_range; eauto. + intros. exploit inj_of_bc_inv; eauto. intros (P & Q & R). auto. Qed. Lemma pmatch_inj_top: @@ -3827,27 +3827,27 @@ Qed. Lemma vmatch_inj_top: forall bc v v', Val.inject (inj_of_bc bc) v v' -> vmatch bc v Vtop. Proof. - intros. inv H; constructor. eapply pmatch_inj_top; eauto. + intros. inv H; constructor. eapply pmatch_inj_top; eauto. Qed. Lemma mmatch_inj_top: forall bc m m', Mem.inject (inj_of_bc bc) m m' -> mmatch bc m mtop. Proof. - intros. + intros. assert (SM: forall b, bc b <> BCinvalid -> smatch bc m b Ptop). { - intros; split; intros. - - exploit Mem.load_inject. eauto. eauto. apply inj_of_bc_valid; auto. - intros (v' & A & B). eapply vmatch_inj_top; eauto. - - exploit Mem.loadbytes_inject. eauto. eauto. apply inj_of_bc_valid; auto. - intros (bytes' & A & B). inv B. inv H4. inv H8. eapply pmatch_inj_top; eauto. + intros; split; intros. + - exploit Mem.load_inject. eauto. eauto. apply inj_of_bc_valid; auto. + intros (v' & A & B). eapply vmatch_inj_top; eauto. + - exploit Mem.loadbytes_inject. eauto. eauto. apply inj_of_bc_valid; auto. + intros (bytes' & A & B). inv B. inv H4. inv H8. eapply pmatch_inj_top; eauto. } - constructor; simpl; intros. + constructor; simpl; intros. - apply ablock_init_sound. apply SM. congruence. - rewrite PTree.gempty in H1; discriminate. - apply SM; auto. - apply SM; auto. - - red; intros. eapply Mem.valid_block_inject_1. eapply inj_of_bc_valid; eauto. eauto. + - red; intros. eapply Mem.valid_block_inject_1. eapply inj_of_bc_valid; eauto. eauto. Qed. (** * Abstracting RTL register environments *) @@ -3882,30 +3882,30 @@ End AVal. Module AE := LPMap(AVal). -Definition aenv := AE.t. +Definition aenv := AE.t. Section MATCHENV. Variable bc: block_classification. Definition ematch (e: regset) (ae: aenv) : Prop := - forall r, vmatch bc e#r (AE.get r ae). + forall r, vmatch bc e#r (AE.get r ae). Lemma ematch_ge: forall e ae1 ae2, ematch e ae1 -> AE.ge ae2 ae1 -> ematch e ae2. Proof. - intros; red; intros. apply vmatch_ge with (AE.get r ae1); auto. apply H0. + intros; red; intros. apply vmatch_ge with (AE.get r ae1); auto. apply H0. Qed. Lemma ematch_update: forall e ae v av r, ematch e ae -> vmatch bc v av -> ematch (e#r <- v) (AE.set r av ae). Proof. - intros; red; intros. rewrite AE.gsspec. rewrite PMap.gsspec. - destruct (peq r0 r); auto. - red; intros. specialize (H xH). subst ae. simpl in H. inv H. - unfold AVal.eq; red; intros. subst av. inv H0. + intros; red; intros. rewrite AE.gsspec. rewrite PMap.gsspec. + destruct (peq r0 r); auto. + red; intros. specialize (H xH). subst ae. simpl in H. inv H. + unfold AVal.eq; red; intros. subst av. inv H0. Qed. Fixpoint einit_regs (rl: list reg) : aenv := @@ -3919,23 +3919,23 @@ Lemma ematch_init: (forall v, In v vl -> vmatch bc v (Ifptr Nonstack)) -> ematch (init_regs vl rl) (einit_regs rl). Proof. - induction rl; simpl; intros. -- red; intros. rewrite Regmap.gi. simpl AE.get. rewrite PTree.gempty. - constructor. -- destruct vl as [ | v1 vs ]. + induction rl; simpl; intros. +- red; intros. rewrite Regmap.gi. simpl AE.get. rewrite PTree.gempty. + constructor. +- destruct vl as [ | v1 vs ]. + assert (ematch (init_regs nil rl) (einit_regs rl)). { apply IHrl. simpl; tauto. } - replace (init_regs nil rl) with (Regmap.init Vundef) in H0 by (destruct rl; auto). - red; intros. rewrite AE.gsspec. destruct (peq r a). - rewrite Regmap.gi. constructor. - apply H0. + replace (init_regs nil rl) with (Regmap.init Vundef) in H0 by (destruct rl; auto). + red; intros. rewrite AE.gsspec. destruct (peq r a). + rewrite Regmap.gi. constructor. + apply H0. red; intros EQ; rewrite EQ in H0. specialize (H0 xH). simpl in H0. inv H0. unfold AVal.eq, AVal.bot. congruence. + assert (ematch (init_regs vs rl) (einit_regs rl)). { apply IHrl. eauto with coqlib. } - red; intros. rewrite Regmap.gsspec. rewrite AE.gsspec. destruct (peq r a). + red; intros. rewrite Regmap.gsspec. rewrite AE.gsspec. destruct (peq r a). auto with coqlib. - apply H0. + apply H0. red; intros EQ; rewrite EQ in H0. specialize (H0 xH). simpl in H0. inv H0. unfold AVal.eq, AVal.bot. congruence. Qed. @@ -3954,14 +3954,14 @@ Proof. destruct ae. unfold AE.get at 2. apply AVal.ge_bot. eapply AVal.ge_trans. apply IHrl. rewrite AE.gsspec. destruct (peq p a). apply AVal.ge_top. apply AVal.ge_refl. apply AVal.eq_refl. - congruence. + congruence. unfold AVal.eq, Vtop, AVal.bot. congruence. Qed. Lemma ematch_forget: forall e rl ae, ematch e ae -> ematch e (eforget rl ae). Proof. - intros. eapply ematch_ge; eauto. apply eforget_ge. + intros. eapply ematch_ge; eauto. apply eforget_ge. Qed. End MATCHENV. @@ -3969,7 +3969,7 @@ End MATCHENV. Lemma ematch_incr: forall bc bc' e ae, ematch bc e ae -> bc_incr bc bc' -> ematch bc' e ae. Proof. - intros; red; intros. apply vmatch_incr with bc; auto. + intros; red; intros. apply vmatch_incr with bc; auto. Qed. (** * Lattice for dataflow analysis *) @@ -3989,12 +3989,12 @@ Module VA <: SEMILATTICE. Lemma eq_refl: forall x, eq x x. Proof. - destruct x; simpl. auto. split. apply AE.eq_refl. tauto. + destruct x; simpl. auto. split. apply AE.eq_refl. tauto. Qed. Lemma eq_sym: forall x y, eq x y -> eq y x. Proof. - destruct x, y; simpl; auto. intros [A B]. - split. apply AE.eq_sym; auto. intros. rewrite B. tauto. + destruct x, y; simpl; auto. intros [A B]. + split. apply AE.eq_sym; auto. intros. rewrite B. tauto. Qed. Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. Proof. @@ -4009,16 +4009,16 @@ Module VA <: SEMILATTICE. | State ae1 am1, State ae2 am2 => AE.beq ae1 ae2 && mbeq am1 am2 | _, _ => false end. - + Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. - destruct x, y; simpl; intros. + destruct x, y; simpl; intros. auto. congruence. congruence. InvBooleans; split. apply AE.beq_correct; auto. - intros. apply mbeq_sound; auto. + intros. apply mbeq_sound; auto. Qed. Definition ge (x y: t) : Prop := @@ -4030,21 +4030,21 @@ Module VA <: SEMILATTICE. Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - destruct x, y; simpl; try tauto. intros [A B]; split. + destruct x, y; simpl; try tauto. intros [A B]; split. apply AE.ge_refl; auto. - intros. rewrite B; auto. + intros. rewrite B; auto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. destruct x, y, z; simpl; try tauto. intros [A B] [C D]; split. - eapply AE.ge_trans; eauto. - eauto. + eapply AE.ge_trans; eauto. + eauto. Qed. Definition bot : t := Bot. Lemma ge_bot: forall x, ge x bot. Proof. - destruct x; simpl; auto. + destruct x; simpl; auto. Qed. Definition lub (x y: t) : t := @@ -4078,7 +4078,7 @@ Hint Constructors pmatch: va. Hint Constructors vmatch: va. Hint Resolve cnot_sound symbol_address_sound shl_sound shru_sound shr_sound - and_sound or_sound xor_sound notint_sound + and_sound or_sound xor_sound notint_sound ror_sound rolm_sound neg_sound add_sound sub_sound mul_sound mulhs_sound mulhu_sound @@ -4090,6 +4090,6 @@ Hint Resolve cnot_sound symbol_address_sound zero_ext_sound sign_ext_sound singleoffloat_sound floatofsingle_sound intoffloat_sound intuoffloat_sound floatofint_sound floatofintu_sound intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound - longofwords_sound loword_sound hiword_sound + longofwords_sound loword_sound hiword_sound cmpu_bool_sound cmp_bool_sound cmpf_bool_sound cmpfs_bool_sound maskzero_sound : va. |