From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/NeedDomain.v | 320 +++++++++++++++++++++++++-------------------------- 1 file changed, 160 insertions(+), 160 deletions(-) (limited to 'backend/NeedDomain.v') diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 770648b1..e40c1322 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -53,7 +53,7 @@ Fixpoint vagree (v w: val) (x: nval) {struct x}: Prop := match v, w with | Vint p, Vint q => iagree p q m | Vint p, _ => False - | _, _ => True + | _, _ => True end | All => Val.lessdef v w end. @@ -143,7 +143,7 @@ Lemma nge_lub_l: forall x y, nge (nlub x y) x. Proof. unfold nlub; destruct x, y; auto with na. - constructor. intros. autorewrite with ints; auto. rewrite H0; auto. + constructor. intros. autorewrite with ints; auto. rewrite H0; auto. Qed. Lemma nge_lub_r: @@ -171,13 +171,13 @@ Lemma iagree_and_eq: forall x y mask, iagree x y mask <-> Int.and x mask = Int.and y mask. Proof. - intros; split; intros. -- Int.bit_solve. specialize (H i H0). - destruct (Int.testbit mask i). - rewrite ! andb_true_r; auto. + intros; split; intros. +- Int.bit_solve. specialize (H i H0). + destruct (Int.testbit mask i). + rewrite ! andb_true_r; auto. rewrite ! andb_false_r; auto. - red; intros. exploit (eq_same_bits i); eauto; autorewrite with ints; auto. - rewrite H1. rewrite ! andb_true_r; auto. + rewrite H1. rewrite ! andb_true_r; auto. Qed. Lemma iagree_mone: @@ -203,7 +203,7 @@ Qed. Lemma iagree_not: forall x y m, iagree x y m -> iagree (Int.not x) (Int.not y) m. Proof. - intros; red; intros; autorewrite with ints; auto. f_equal; auto. + intros; red; intros; autorewrite with ints; auto. f_equal; auto. Qed. Lemma iagree_not': @@ -217,7 +217,7 @@ Lemma iagree_or: forall x y n m, iagree x y (Int.and m (Int.not n)) -> iagree (Int.or x n) (Int.or y n) m. Proof. - intros. apply iagree_not'. rewrite ! Int.not_or_and_not. apply iagree_and. + intros. apply iagree_not'. rewrite ! Int.not_or_and_not. apply iagree_and. apply iagree_not; auto. Qed. @@ -228,19 +228,19 @@ Lemma iagree_bitwise_binop: forall x1 x2 y1 y2 m, iagree x1 y1 m -> iagree x2 y2 m -> iagree (f x1 x2) (f y1 y2) m. Proof. - intros; red; intros. rewrite ! H by auto. f_equal; auto. + intros; red; intros. rewrite ! H by auto. f_equal; auto. Qed. Lemma iagree_shl: forall x y m n, iagree x y (Int.shru m n) -> iagree (Int.shl x n) (Int.shl y n) m. Proof. - intros; red; intros. autorewrite with ints; auto. + intros; red; intros. autorewrite with ints; auto. destruct (zlt i (Int.unsigned n)). - auto. -- generalize (Int.unsigned_range n); intros. - apply H. omega. rewrite Int.bits_shru by omega. - replace (i - Int.unsigned n + Int.unsigned n) with i by omega. +- generalize (Int.unsigned_range n); intros. + apply H. omega. rewrite Int.bits_shru by omega. + replace (i - Int.unsigned n + Int.unsigned n) with i by omega. rewrite zlt_true by omega. auto. Qed. @@ -248,11 +248,11 @@ Lemma iagree_shru: forall x y m n, iagree x y (Int.shl m n) -> iagree (Int.shru x n) (Int.shru y n) m. Proof. - intros; red; intros. autorewrite with ints; auto. + intros; red; intros. autorewrite with ints; auto. destruct (zlt (i + Int.unsigned n) Int.zwordsize). -- generalize (Int.unsigned_range n); intros. - apply H. omega. rewrite Int.bits_shl by omega. - replace (i + Int.unsigned n - Int.unsigned n) with i by omega. +- generalize (Int.unsigned_range n); intros. + apply H. omega. rewrite Int.bits_shl by omega. + replace (i + Int.unsigned n - Int.unsigned n) with i by omega. rewrite zlt_false by omega. auto. - auto. Qed. @@ -262,8 +262,8 @@ Lemma iagree_shr_1: Int.shru (Int.shl m n) n = m -> iagree x y (Int.shl m n) -> iagree (Int.shr x n) (Int.shr y n) m. Proof. - intros; red; intros. rewrite <- H in H2. rewrite Int.bits_shru in H2 by auto. - rewrite ! Int.bits_shr by auto. + intros; red; intros. rewrite <- H in H2. rewrite Int.bits_shru in H2 by auto. + rewrite ! Int.bits_shr by auto. destruct (zlt (i + Int.unsigned n) Int.zwordsize). - apply H0; auto. generalize (Int.unsigned_range n); omega. - discriminate. @@ -274,17 +274,17 @@ Lemma iagree_shr: iagree x y (Int.or (Int.shl m n) (Int.repr Int.min_signed)) -> iagree (Int.shr x n) (Int.shr y n) m. Proof. - intros; red; intros. rewrite ! Int.bits_shr by auto. - generalize (Int.unsigned_range n); intros. + intros; red; intros. rewrite ! Int.bits_shr by auto. + generalize (Int.unsigned_range n); intros. set (j := if zlt (i + Int.unsigned n) Int.zwordsize then i + Int.unsigned n else Int.zwordsize - 1). assert (0 <= j < Int.zwordsize). { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); omega. } - apply H; auto. autorewrite with ints; auto. apply orb_true_intro. + apply H; auto. autorewrite with ints; auto. apply orb_true_intro. unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize). -- left. rewrite zlt_false by omega. - replace (i + Int.unsigned n - Int.unsigned n) with i by omega. +- left. rewrite zlt_false by omega. + replace (i + Int.unsigned n - Int.unsigned n) with i by omega. auto. - right. reflexivity. Qed. @@ -302,14 +302,14 @@ Proof. mod Int.zwordsize) with i. auto. apply Int.eqmod_small_eq with Int.zwordsize; auto. apply Int.eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount). - apply Int.eqmod_refl2; omega. + apply Int.eqmod_refl2; omega. eapply Int.eqmod_trans. 2: apply Int.eqmod_mod; auto. - apply Int.eqmod_add. - apply Int.eqmod_mod; auto. - apply Int.eqmod_refl. - apply Z_mod_lt; auto. + apply Int.eqmod_add. + apply Int.eqmod_mod; auto. + apply Int.eqmod_refl. apply Z_mod_lt; auto. -Qed. + apply Z_mod_lt; auto. +Qed. Lemma iagree_ror: forall p q m amount, @@ -317,9 +317,9 @@ Lemma iagree_ror: iagree (Int.ror p amount) (Int.ror q amount) m. Proof. intros. rewrite ! Int.ror_rol_neg by apply int_wordsize_divides_modulus. - apply iagree_rol. + apply iagree_rol. rewrite Int.ror_rol_neg by apply int_wordsize_divides_modulus. - rewrite Int.neg_involutive; auto. + rewrite Int.neg_involutive; auto. Qed. Lemma eqmod_iagree: @@ -327,14 +327,14 @@ Lemma eqmod_iagree: Int.eqmod (two_p (Int.size m)) x y -> iagree (Int.repr x) (Int.repr y) m. Proof. - intros. set (p := nat_of_Z (Int.size m)). + intros. set (p := nat_of_Z (Int.size m)). generalize (Int.size_range m); intros RANGE. assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. } rewrite EQ in H; rewrite <- two_power_nat_two_p in H. red; intros. rewrite ! Int.testbit_repr by auto. - destruct (zlt i (Int.size m)). + destruct (zlt i (Int.size m)). eapply Int.same_bits_eqmod; eauto. omega. - assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega). + assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega). congruence. Qed. @@ -345,12 +345,12 @@ Lemma iagree_eqmod: iagree x y (complete_mask m) -> Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y). Proof. - intros. set (p := nat_of_Z (Int.size m)). + intros. set (p := nat_of_Z (Int.size m)). generalize (Int.size_range m); intros RANGE. assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. } - rewrite EQ; rewrite <- two_power_nat_two_p. - apply Int.eqmod_same_bits. intros. apply H. omega. - unfold complete_mask. rewrite Int.bits_zero_ext by omega. + rewrite EQ; rewrite <- two_power_nat_two_p. + apply Int.eqmod_same_bits. intros. apply H. omega. + unfold complete_mask. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto. Qed. @@ -361,13 +361,13 @@ Proof. + subst m; reflexivity. + assert (Int.unsigned m <> 0). { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. } - assert (0 < Int.size m). + assert (0 < Int.size m). { apply Int.Zsize_pos'. generalize (Int.unsigned_range m); omega. } generalize (Int.size_range m); intros. - f_equal. apply Int.bits_size_4. tauto. + f_equal. apply Int.bits_size_4. tauto. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega. apply Int.bits_mone; omega. - intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; omega. + intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; omega. Qed. (** ** Abstract operations over value needs. *) @@ -416,7 +416,7 @@ Proof. unfold orimm; intros; destruct x; simpl in *. - auto. - unfold Val.or; InvAgree. apply iagree_or; auto. -- InvAgree. simpl. apply Val.lessdef_same. f_equal. apply iagree_mone. +- InvAgree. simpl. apply Val.lessdef_same. f_equal. apply iagree_mone. apply iagree_or. rewrite Int.and_commut. rewrite Int.and_mone. auto. Qed. @@ -438,8 +438,8 @@ Lemma vagree_bitwise_binop: x. Proof. unfold bitwise; intros. destruct x; simpl in *. -- auto. -- InvAgree. +- auto. +- InvAgree. - inv H0; auto. inv H1; auto. destruct w1; auto. Qed. @@ -482,8 +482,8 @@ Lemma shlimm_sound: vagree v w (shlimm x n) -> vagree (Val.shl v (Vint n)) (Val.shl w (Vint n)) x. Proof. - unfold shlimm; intros. unfold Val.shl. - destruct (Int.ltu n Int.iwordsize). + unfold shlimm; intros. unfold Val.shl. + destruct (Int.ltu n Int.iwordsize). destruct x; simpl in *. - auto. - InvAgree. apply iagree_shl; auto. @@ -504,7 +504,7 @@ Lemma shruimm_sound: vagree (Val.shru v (Vint n)) (Val.shru w (Vint n)) x. Proof. unfold shruimm; intros. unfold Val.shru. - destruct (Int.ltu n Int.iwordsize). + destruct (Int.ltu n Int.iwordsize). destruct x; simpl in *. - auto. - InvAgree. apply iagree_shru; auto. @@ -528,10 +528,10 @@ Lemma shrimm_sound: vagree (Val.shr v (Vint n)) (Val.shr w (Vint n)) x. Proof. unfold shrimm; intros. unfold Val.shr. - destruct (Int.ltu n Int.iwordsize). + destruct (Int.ltu n Int.iwordsize). destruct x; simpl in *. - auto. -- InvAgree. +- InvAgree. destruct (Int.eq_dec (Int.shru (Int.shl m n) n) m). apply iagree_shr_1; auto. apply iagree_shr; auto. @@ -553,10 +553,10 @@ Lemma rolm_sound: Proof. unfold rolm; intros; destruct x; simpl in *. - auto. -- unfold Val.rolm; InvAgree. unfold Int.rolm. - apply iagree_and. apply iagree_rol. auto. -- unfold Val.rolm; InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone. - unfold Int.rolm. apply iagree_and. apply iagree_rol. rewrite Int.and_commut. +- unfold Val.rolm; InvAgree. unfold Int.rolm. + apply iagree_and. apply iagree_rol. auto. +- unfold Val.rolm; InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone. + unfold Int.rolm. apply iagree_and. apply iagree_rol. rewrite Int.and_commut. rewrite Int.and_mone. auto. Qed. @@ -573,15 +573,15 @@ Lemma ror_sound: vagree (Val.ror v (Vint n)) (Val.ror w (Vint n)) x. Proof. unfold ror; intros. unfold Val.ror. - destruct (Int.ltu n Int.iwordsize). + destruct (Int.ltu n Int.iwordsize). destruct x; simpl in *. - auto. -- InvAgree. apply iagree_ror; auto. +- InvAgree. apply iagree_ror; auto. - inv H; auto. - destruct v; auto with na. Qed. -(** Modular arithmetic operations: add, mul, opposite. +(** Modular arithmetic operations: add, mul, opposite. (But not subtraction because of the pointer - pointer case. *) Definition modarith (x: nval) := @@ -596,10 +596,10 @@ Lemma add_sound: vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) -> vagree (Val.add v1 v2) (Val.add w1 w2) x. Proof. - unfold modarith; intros. destruct x; simpl in *. + unfold modarith; intros. destruct x; simpl in *. - auto. -- unfold Val.add; InvAgree. apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto. -- inv H; auto. inv H0; auto. destruct w1; auto. +- unfold Val.add; InvAgree. apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto. +- inv H; auto. inv H0; auto. destruct w1; auto. Qed. Remark modarith_idem: forall nv, modarith (modarith nv) = modarith nv. @@ -612,10 +612,10 @@ Lemma mul_sound: vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) -> vagree (Val.mul v1 v2) (Val.mul w1 w2) x. Proof. - unfold mul, add; intros. destruct x; simpl in *. + unfold mul, add; intros. destruct x; simpl in *. - auto. -- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto. -- inv H; auto. inv H0; auto. destruct w1; auto. +- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto. +- inv H; auto. inv H0; auto. destruct w1; auto. Qed. Lemma neg_sound: @@ -625,8 +625,8 @@ Lemma neg_sound: Proof. intros; destruct x; simpl in *. - auto. -- unfold Val.neg; InvAgree. - apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto. +- unfold Val.neg; InvAgree. + apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto. - inv H; simpl; auto. Qed. @@ -648,12 +648,12 @@ Proof. unfold zero_ext; intros. destruct x; simpl in *. - auto. -- unfold Val.zero_ext; InvAgree. - red; intros. autorewrite with ints; try omega. +- unfold Val.zero_ext; InvAgree. + red; intros. autorewrite with ints; try omega. destruct (zlt i1 n); auto. apply H; auto. autorewrite with ints; try omega. rewrite zlt_true; auto. -- unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. - Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto. +- unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. + Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto. autorewrite with ints; try omega. apply zlt_true; auto. Qed. @@ -672,25 +672,25 @@ Lemma sign_ext_sound: Proof. unfold sign_ext; intros. destruct x; simpl in *. - auto. -- unfold Val.sign_ext; InvAgree. +- unfold Val.sign_ext; InvAgree. red; intros. autorewrite with ints; try omega. set (j := if zlt i1 n then i1 else n - 1). - assert (0 <= j < Int.zwordsize). + assert (0 <= j < Int.zwordsize). { unfold j; destruct (zlt i1 n); omega. } - apply H; auto. - autorewrite with ints; try omega. apply orb_true_intro. - unfold j; destruct (zlt i1 n). - left. rewrite zlt_true; auto. - right. rewrite Int.unsigned_repr. rewrite zlt_false by omega. - replace (n - 1 - (n - 1)) with 0 by omega. reflexivity. + apply H; auto. + autorewrite with ints; try omega. apply orb_true_intro. + unfold j; destruct (zlt i1 n). + left. rewrite zlt_true; auto. + right. rewrite Int.unsigned_repr. rewrite zlt_false by omega. + replace (n - 1 - (n - 1)) with 0 by omega. reflexivity. generalize Int.wordsize_max_unsigned; omega. -- unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. +- unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. Int.bit_solve; try omega. set (j := if zlt i1 n then i1 else n - 1). - assert (0 <= j < Int.zwordsize). + assert (0 <= j < Int.zwordsize). { unfold j; destruct (zlt i1 n); omega. } - apply H; auto. rewrite Int.bits_zero_ext; try omega. - rewrite zlt_true. apply Int.bits_mone; auto. + apply H; auto. rewrite Int.bits_zero_ext; try omega. + rewrite zlt_true. apply Int.bits_mone; auto. unfold j. destruct (zlt i1 n); omega. Qed. @@ -713,25 +713,25 @@ Proof. (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk w)). { - rewrite <- (encode_val_length chunk w). + rewrite <- (encode_val_length chunk w). apply repeat_Undef_inject_any. } assert (SAME: forall vl1 vl2, vl1 = vl2 -> list_forall2 memval_lessdef vl1 vl2). { - intros. subst vl2. revert vl1. induction vl1; constructor; auto. - apply memval_lessdef_refl. + intros. subst vl2. revert vl1. induction vl1; constructor; auto. + apply memval_lessdef_refl. } intros. unfold store_argument in H; destruct chunk. -- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod. +- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod. change 8 with (Int.size (Int.repr 255)). apply iagree_eqmod; auto. -- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod. +- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod. change 8 with (Int.size (Int.repr 255)). apply iagree_eqmod; auto. -- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod. +- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod. change 16 with (Int.size (Int.repr 65535)). apply iagree_eqmod; auto. -- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod. +- InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod. change 16 with (Int.size (Int.repr 65535)). apply iagree_eqmod; auto. - apply encode_val_inject. rewrite val_inject_id; auto. - apply encode_val_inject. rewrite val_inject_id; auto. @@ -768,7 +768,7 @@ Lemma maskzero_sound: Val.maskzero_bool v n = Some b -> Val.maskzero_bool w n = Some b. Proof. - unfold maskzero; intros. + unfold maskzero; intros. unfold Val.maskzero_bool; InvAgree; try discriminate. inv H0. rewrite iagree_and_eq in H. rewrite H. auto. Qed. @@ -795,9 +795,9 @@ Let valid_pointer_inj: Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. Proof. - unfold inject_id; intros. inv H. rewrite Int.add_zero. + unfold inject_id; intros. inv H. rewrite Int.add_zero. rewrite Mem.valid_pointer_nonempty_perm in *. eauto. -Qed. +Qed. Let weak_valid_pointer_inj: forall b1 ofs b2 delta, @@ -805,7 +805,7 @@ Let weak_valid_pointer_inj: Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. Proof. - unfold inject_id; intros. inv H. rewrite Int.add_zero. + unfold inject_id; intros. inv H. rewrite Int.add_zero. rewrite Mem.weak_valid_pointer_spec in *. rewrite ! Mem.valid_pointer_nonempty_perm in *. destruct H0; [left|right]; eauto. @@ -830,7 +830,7 @@ Let valid_different_pointers_inj: b1' <> b2' \/ Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). Proof. - unfold inject_id; intros. left; congruence. + unfold inject_id; intros. left; congruence. Qed. Lemma default_needs_of_condition_sound: @@ -846,7 +846,7 @@ Qed. Lemma default_needs_of_operation_sound: forall op args1 v1 args2 nv, eval_operation ge (Vptr sp Int.zero) op args1 m1 = Some v1 -> - vagree_list args1 args2 nil + vagree_list args1 args2 nil \/ vagree_list args1 args2 (default nv :: nil) \/ vagree_list args1 args2 (default nv :: default nv :: nil) -> nv <> Nothing -> @@ -854,12 +854,12 @@ Lemma default_needs_of_operation_sound: eval_operation ge (Vptr sp Int.zero) op args2 m2 = Some v2 /\ vagree v1 v2 nv. Proof. - intros. assert (default nv = All) by (destruct nv; simpl; congruence). + intros. assert (default nv = All) by (destruct nv; simpl; congruence). rewrite H2 in H0. assert (Val.lessdef_list args1 args2). { - destruct H0. auto with na. - destruct H0. inv H0; constructor; auto with na. + destruct H0. auto with na. + destruct H0. inv H0; constructor; auto with na. inv H0; constructor; auto with na. inv H8; constructor; auto with na. } exploit (@eval_operation_inj _ _ _ _ ge ge inject_id). @@ -869,7 +869,7 @@ Proof. apply val_inject_list_lessdef; eauto. eauto. intros (v2 & A & B). exists v2; split; auto. - apply vagree_lessdef. apply val_inject_lessdef. auto. + apply vagree_lessdef. apply val_inject_lessdef. auto. Qed. End DEFAULT. @@ -890,12 +890,12 @@ Lemma andimm_redundant_sound: vagree (Val.and v (Vint n)) w x. Proof. unfold andimm_redundant; intros. destruct x; try discriminate. -- simpl; auto. +- simpl; auto. - InvBooleans. simpl in *; unfold Val.and; InvAgree. - red; intros. exploit (eq_same_bits i1); eauto. - autorewrite with ints; auto. rewrite H2; simpl; intros. - destruct (Int.testbit n i1) eqn:N; try discriminate. - rewrite andb_true_r. apply H0; auto. autorewrite with ints; auto. + red; intros. exploit (eq_same_bits i1); eauto. + autorewrite with ints; auto. rewrite H2; simpl; intros. + destruct (Int.testbit n i1) eqn:N; try discriminate. + rewrite andb_true_r. apply H0; auto. autorewrite with ints; auto. rewrite H2, N; auto. Qed. @@ -915,7 +915,7 @@ Proof. unfold orimm_redundant; intros. destruct x; try discriminate. - auto. - InvBooleans. simpl in *; unfold Val.or; InvAgree. - apply iagree_not'. rewrite Int.not_or_and_not. + apply iagree_not'. rewrite Int.not_or_and_not. apply (andimm_redundant_sound (Vint (Int.not i)) (Vint (Int.not i0)) (I m) (Int.not n)). simpl. rewrite Int.not_involutive. apply proj_sumbool_is_true. auto. simpl. apply iagree_not; auto. @@ -933,9 +933,9 @@ Proof. unfold rolm_redundant; intros; InvBooleans. subst amount. rewrite Val.rolm_zero. apply andimm_redundant_sound; auto. assert (forall n, Int.ror n Int.zero = n). - { intros. rewrite Int.ror_rol_neg by apply int_wordsize_divides_modulus. + { intros. rewrite Int.ror_rol_neg by apply int_wordsize_divides_modulus. rewrite Int.neg_zero. apply Int.rol_zero. } - unfold rolm, andimm in *. destruct x; auto. + unfold rolm, andimm in *. destruct x; auto. rewrite H in H0. auto. rewrite H in H0. auto. Qed. @@ -956,8 +956,8 @@ Lemma zero_ext_redundant_sound: Proof. unfold zero_ext_redundant; intros. destruct x; try discriminate. - auto. -- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. - red; intros; autorewrite with ints; try omega. +- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. + red; intros; autorewrite with ints; try omega. destruct (zlt i1 n). apply H0; auto. rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate. Qed. @@ -978,10 +978,10 @@ Lemma sign_ext_redundant_sound: Proof. unfold sign_ext_redundant; intros. destruct x; try discriminate. - auto. -- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. - red; intros; autorewrite with ints; try omega. +- simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. + red; intros; autorewrite with ints; try omega. destruct (zlt i1 n). apply H0; auto. - rewrite Int.bits_or; auto. rewrite H3; auto. + rewrite Int.bits_or; auto. rewrite H3; auto. rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate. Qed. @@ -1014,7 +1014,7 @@ End NVal. Module NE := LPMap1(NVal). -Definition nenv := NE.t. +Definition nenv := NE.t. Definition nreg (ne: nenv) (r: reg) := NE.get r ne. @@ -1024,7 +1024,7 @@ Definition eagree (e1 e2: regset) (ne: nenv) : Prop := Lemma nreg_agree: forall rs1 rs2 ne r, eagree rs1 rs2 ne -> vagree rs1#r rs2#r (nreg ne r). Proof. - intros. apply H. + intros. apply H. Qed. Hint Resolve nreg_agree: na. @@ -1033,7 +1033,7 @@ Lemma eagree_ge: forall e1 e2 ne ne', eagree e1 e2 ne -> NE.ge ne ne' -> eagree e1 e2 ne'. Proof. - intros; red; intros. apply nge_agree with (NE.get r ne); auto. apply H0. + intros; red; intros. apply nge_agree with (NE.get r ne); auto. apply H0. Qed. Lemma eagree_bot: @@ -1045,15 +1045,15 @@ Qed. Lemma eagree_same: forall e ne, eagree e e ne. Proof. - intros; red; intros. apply vagree_same. + intros; red; intros. apply vagree_same. Qed. Lemma eagree_update_1: forall e1 e2 ne v1 v2 nv r, eagree e1 e2 ne -> vagree v1 v2 nv -> eagree (e1#r <- v1) (e2#r <- v2) (NE.set r nv ne). Proof. - intros; red; intros. rewrite NE.gsspec. rewrite ! PMap.gsspec. - destruct (peq r0 r); auto. + intros; red; intros. rewrite NE.gsspec. rewrite ! PMap.gsspec. + destruct (peq r0 r); auto. Qed. Lemma eagree_update: @@ -1062,7 +1062,7 @@ Lemma eagree_update: eagree e1 e2 (NE.set r Nothing ne) -> eagree (e1#r <- v1) (e2#r <- v2) ne. Proof. - intros; red; intros. specialize (H0 r0). rewrite NE.gsspec in H0. + intros; red; intros. specialize (H0 r0). rewrite NE.gsspec in H0. rewrite ! PMap.gsspec. destruct (peq r0 r). subst r0. auto. auto. @@ -1073,8 +1073,8 @@ Lemma eagree_update_dead: nreg ne r = Nothing -> eagree e1 e2 ne -> eagree (e1#r <- v1) e2 ne. Proof. - intros; red; intros. rewrite PMap.gsspec. - destruct (peq r0 r); auto. subst. unfold nreg in H. rewrite H. red; auto. + intros; red; intros. rewrite PMap.gsspec. + destruct (peq r0 r); auto. subst. unfold nreg in H. rewrite H. red; auto. Qed. (** * Neededness for memory locations *) @@ -1146,12 +1146,12 @@ Lemma nlive_add: Int.unsigned ofs <= i < Int.unsigned ofs + sz -> nlive (nmem_add nm p sz) b i. Proof. - intros. unfold nmem_add. destruct nm. apply nlive_all. - inv H1; try (apply nlive_all). + intros. unfold nmem_add. destruct nm. apply nlive_all. + inv H1; try (apply nlive_all). - (* Gl id ofs *) - assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). + assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). destruct gl!id as [iv|] eqn:NG. - + constructor; simpl; intros. + + constructor; simpl; intros. congruence. assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. rewrite PTree.gss in H5. inv H5. rewrite ISet.In_remove. @@ -1161,13 +1161,13 @@ Proof. assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. congruence. - (* Glo id *) - assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). + assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). constructor; simpl; intros. congruence. - assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. + assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. rewrite PTree.grs in H5. congruence. - (* Stk ofs *) - constructor; simpl; intros. + constructor; simpl; intros. rewrite ISet.In_remove. intros [A B]. elim A; auto. assert (bc b = BCglob id) by (eapply H; eauto). congruence. - (* Stack *) @@ -1183,19 +1183,19 @@ Proof. intros. inversion H; subst. unfold nmem_add; destruct p; try (apply nlive_all). - (* Gl id ofs *) destruct gl!id as [iv|] eqn:NG. - + split; simpl; intros. auto. - rewrite PTree.gsspec in H1. destruct (peq id0 id); eauto. inv H1. + + split; simpl; intros. auto. + rewrite PTree.gsspec in H1. destruct (peq id0 id); eauto. inv H1. rewrite ISet.In_remove. intros [P Q]. eelim GL; eauto. - + auto. + + auto. - (* Glo id *) - split; simpl; intros. auto. + split; simpl; intros. auto. rewrite PTree.grspec in H1. destruct (PTree.elt_eq id0 id). congruence. eauto. - (* Stk ofs *) - split; simpl; intros. + split; simpl; intros. rewrite ISet.In_remove. intros [P Q]. eelim STK; eauto. eauto. - (* Stack *) - split; simpl; intros. + split; simpl; intros. apply ISet.In_empty. eauto. Qed. @@ -1243,13 +1243,13 @@ Proof. split; simpl; auto; intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). + inv H6. destruct H3. congruence. destruct gl!id as [iv0|] eqn:NG. - rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto. - rewrite ISet.In_interval. omega. -+ eauto. + rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto. + rewrite ISet.In_interval. omega. ++ eauto. - (* Stk ofs *) - split; simpl; auto; intros. destruct H3. - elim H3. subst b'. eapply bc_stack; eauto. - rewrite ISet.In_add. intros [P|P]. omega. eapply STK; eauto. + split; simpl; auto; intros. destruct H3. + elim H3. subst b'. eapply bc_stack; eauto. + rewrite ISet.In_add. intros [P|P]. omega. eapply STK; eauto. Qed. (** Test (conservatively) whether some locations in the range delimited @@ -1284,12 +1284,12 @@ Proof. inv H1; try discriminate. - (* Gl id ofs *) assert (Genv.find_symbol ge id = Some b) by (eapply H; eauto). - destruct gl!id as [iv|] eqn:HG; inv H2. + destruct gl!id as [iv|] eqn:HG; inv H2. destruct (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) iv) eqn:IC; try discriminate. rewrite ISet.contains_spec in IC. eelim GL; eauto. -- (* Stk ofs *) +- (* Stk ofs *) destruct (ISet.contains (Int.unsigned ofs) (Int.unsigned ofs + sz) stk) eqn:IC; try discriminate. - rewrite ISet.contains_spec in IC. eelim STK; eauto. eapply bc_stack; eauto. + rewrite ISet.contains_spec in IC. eelim STK; eauto. eapply bc_stack; eauto. Qed. (** Kill all stack locations between 0 and [sz], and mark everything else @@ -1303,7 +1303,7 @@ Lemma nlive_dead_stack: forall sz b' i, b' <> sp \/ ~(0 <= i < sz) -> nlive (nmem_dead_stack sz) b' i. Proof. intros; constructor; simpl; intros. -- rewrite ISet.In_interval. intuition. +- rewrite ISet.In_interval. intuition. - rewrite PTree.gempty in H1; discriminate. Qed. @@ -1330,10 +1330,10 @@ Proof. intros. inversion H; subst. destruct nm2; simpl. auto. constructor; simpl; intros. - rewrite ISet.In_inter. intros [P Q]. eelim STK; eauto. -- rewrite PTree.gcombine in H1 by auto. +- rewrite PTree.gcombine in H1 by auto. destruct gl!id as [iv1|] eqn:NG1; try discriminate; destruct gl0!id as [iv2|] eqn:NG2; inv H1. - rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto. + rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto. Qed. Lemma nlive_lub_r: @@ -1342,10 +1342,10 @@ Proof. intros. inversion H; subst. destruct nm1; simpl. auto. constructor; simpl; intros. - rewrite ISet.In_inter. intros [P Q]. eelim STK; eauto. -- rewrite PTree.gcombine in H1 by auto. +- rewrite PTree.gcombine in H1 by auto. destruct gl0!id as [iv1|] eqn:NG1; try discriminate; destruct gl!id as [iv2|] eqn:NG2; inv H1. - rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto. + rewrite ISet.In_inter. intros [P Q]. eelim GL; eauto. Qed. (** Boolean-valued equality test *) @@ -1362,18 +1362,18 @@ Lemma nmem_beq_sound: nmem_beq nm1 nm2 = true -> (nlive nm1 b ofs <-> nlive nm2 b ofs). Proof. - unfold nmem_beq; intros. + unfold nmem_beq; intros. destruct nm1 as [ | stk1 gl1]; destruct nm2 as [ | stk2 gl2]; try discriminate. - split; intros L; inv L. - InvBooleans. rewrite ISet.beq_spec in H0. rewrite PTree.beq_correct in H1. split; intros L; inv L; constructor; intros. -+ rewrite <- H0. eauto. ++ rewrite <- H0. eauto. + specialize (H1 id). rewrite H2 in H1. destruct gl1!id as [iv1|] eqn: NG; try contradiction. - rewrite ISet.beq_spec in H1. rewrite <- H1. eauto. -+ rewrite H0. eauto. + rewrite ISet.beq_spec in H1. rewrite <- H1. eauto. ++ rewrite H0. eauto. + specialize (H1 id). rewrite H2 in H1. destruct gl2!id as [iv2|] eqn: NG; try contradiction. rewrite ISet.beq_spec in H1. rewrite H1. eauto. -Qed. +Qed. End LOCATIONS. @@ -1390,11 +1390,11 @@ Module NA <: SEMILATTICE. Lemma eq_refl: forall x, eq x x. Proof. - unfold eq; destruct x; simpl; split. apply NE.eq_refl. tauto. + unfold eq; destruct x; simpl; split. apply NE.eq_refl. tauto. Qed. Lemma eq_sym: forall x y, eq x y -> eq y x. Proof. - unfold eq; destruct x, y; simpl. intros [A B]. + unfold eq; destruct x, y; simpl. intros [A B]. split. apply NE.eq_sym; auto. intros. rewrite B. tauto. Qed. @@ -1407,10 +1407,10 @@ Module NA <: SEMILATTICE. Definition beq (x y: t) : bool := NE.beq (fst x) (fst y) && nmem_beq (snd x) (snd y). - + Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. - unfold beq, eq; destruct x, y; simpl; intros. InvBooleans. split. + unfold beq, eq; destruct x, y; simpl; intros. InvBooleans. split. apply NE.beq_correct; auto. intros. apply nmem_beq_sound; auto. Qed. @@ -1438,7 +1438,7 @@ Module NA <: SEMILATTICE. Proof. unfold ge, bot; destruct x; simpl. split. apply NE.ge_bot. - intros. inv H. + intros. inv H. Qed. Definition lub (x y: t) : t := @@ -1446,13 +1446,13 @@ Module NA <: SEMILATTICE. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. - unfold ge; destruct x, y; simpl; split. + unfold ge; destruct x, y; simpl; split. apply NE.ge_lub_left. intros; apply nlive_lub_l; auto. Qed. Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. - unfold ge; destruct x, y; simpl; split. + unfold ge; destruct x, y; simpl; split. apply NE.ge_lub_right. intros; apply nlive_lub_r; auto. Qed. -- cgit