From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- powerpc/Asmgenproof1.v | 292 ++++++++++++++++++++++++------------------------- 1 file changed, 146 insertions(+), 146 deletions(-) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 25e8bf07..aa2645f3 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -35,8 +35,8 @@ Lemma low_high_u: forall n, Int.or (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n. Proof. intros. unfold high_u, low_u. - rewrite Int.shl_rolm. rewrite Int.shru_rolm. - rewrite Int.rolm_rolm. + rewrite Int.shl_rolm. rewrite Int.shru_rolm. + rewrite Int.rolm_rolm. change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) (Int.repr (Z_of_nat Int.wordsize))) @@ -50,8 +50,8 @@ Lemma low_high_u_xor: forall n, Int.xor (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n. Proof. intros. unfold high_u, low_u. - rewrite Int.shl_rolm. rewrite Int.shru_rolm. - rewrite Int.rolm_rolm. + rewrite Int.shl_rolm. rewrite Int.shru_rolm. + rewrite Int.rolm_rolm. change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) (Int.repr (Z_of_nat Int.wordsize))) @@ -65,8 +65,8 @@ Lemma low_high_s: forall n, Int.add (Int.shl (high_s n) (Int.repr 16)) (low_s n) = n. Proof. intros. - rewrite Int.shl_mul_two_p. - unfold high_s. + rewrite Int.shl_mul_two_p. + unfold high_s. rewrite <- (Int.divu_pow2 (Int.sub n (low_s n)) (Int.repr 65536) (Int.repr 16)). 2: reflexivity. change (two_p (Int.unsigned (Int.repr 16))) with 65536. @@ -78,17 +78,17 @@ Proof. unfold Int.modu, Int.zero. decEq. change 0 with (0 mod 65536). change (Int.unsigned (Int.repr 65536)) with 65536. - apply Int.eqmod_mod_eq. omega. + apply Int.eqmod_mod_eq. omega. unfold x, low_s. eapply Int.eqmod_trans. apply Int.eqmod_divides with Int.modulus. unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. exists 65536. compute; auto. replace 0 with (Int.unsigned n - Int.unsigned n) by omega. - apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'. + apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'. compute; auto. rewrite H0 in H. rewrite Int.add_zero in H. rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp. + rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp. rewrite Int.sub_idem. apply Int.add_zero. Qed. @@ -96,7 +96,7 @@ Lemma add_zero_symbol_address: forall (ge: genv) id ofs, Val.add Vzero (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs. Proof. - unfold Genv.symbol_address; intros. destruct (Genv.find_symbol ge id); auto. + unfold Genv.symbol_address; intros. destruct (Genv.find_symbol ge id); auto. simpl. rewrite Int.add_zero; auto. Qed. @@ -213,15 +213,15 @@ Proof. intros. unfold loadimm. case (Int.eq (high_s n) Int.zero). (* addi *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. rewrite Int.add_zero_l. intuition Simpl. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - rewrite <- H. rewrite Int.add_commut. rewrite low_high_s. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + rewrite <- H. rewrite Int.add_commut. rewrite low_high_s. intuition Simpl. (* addis + ori *) - econstructor; split. eapply exec_straight_two. + econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. split. Simpl. rewrite Int.add_zero_l. unfold Val.or. rewrite low_high_u. auto. intros; Simpl. @@ -241,25 +241,25 @@ Proof. intros. unfold addimm. (* addi *) case (Int.eq (high_s n) Int.zero). - econstructor; split. apply exec_straight_one. + econstructor; split. apply exec_straight_one. simpl. rewrite gpr_or_zero_not_zero; eauto. reflexivity. intuition Simpl. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. econstructor; split. apply exec_straight_one. - simpl. rewrite gpr_or_zero_not_zero; auto. auto. - split. Simpl. - generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. congruence. + simpl. rewrite gpr_or_zero_not_zero; auto. auto. + split. Simpl. + generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. congruence. intros; Simpl. (* addis + addi *) econstructor; split. eapply exec_straight_two. - simpl. rewrite gpr_or_zero_not_zero; eauto. simpl. rewrite gpr_or_zero_not_zero; eauto. - auto. auto. + simpl. rewrite gpr_or_zero_not_zero; eauto. + auto. auto. split. Simpl. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. intros; Simpl. -Qed. +Qed. (** And integer immediate. *) @@ -290,7 +290,7 @@ Proof. generalize (compare_sint_spec (rs#r1 <- v) v Vzero). intros [A [B [C D]]]. split. apply exec_straight_one. simpl. - generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. + generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. intro. rewrite H1. reflexivity. reflexivity. split. rewrite D; auto with asmgen. Simpl. split. auto. @@ -301,10 +301,10 @@ Proof. exists (nextinstr (compare_sint (rs1#r1 <- v) v Vzero)). generalize (compare_sint_spec (rs1#r1 <- v) v Vzero). intros [A [B [C D]]]. - split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. rewrite RES1. + split. eapply exec_straight_trans. eexact EX1. + apply exec_straight_one. simpl. rewrite RES1. rewrite (OTHER1 r2). reflexivity. congruence. congruence. - reflexivity. + reflexivity. split. rewrite D; auto with asmgen. Simpl. split. auto. intros. rewrite D; auto with asmgen. Simpl. @@ -321,7 +321,7 @@ Proof. intros. unfold andimm. destruct (is_rlw_mask n). (* turned into rlw *) econstructor; split. eapply exec_straight_one. - simpl. rewrite Val.rolm_zero. eauto. auto. + simpl. rewrite Val.rolm_zero. eauto. auto. intuition Simpl. (* andimm_base *) destruct (andimm_base_correct r1 r2 n k rs m) as [rs' [A [B [C D]]]]; auto. @@ -349,13 +349,13 @@ Proof. case (Int.eq (low_u n) Int.zero); intro. exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. simpl. - generalize (low_high_u n). rewrite H. rewrite Int.or_zero. + generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. intuition Simpl. (* oris + ori *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - intuition Simpl. - rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. + intuition Simpl. + rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. Qed. (** Xor integer immediate. *) @@ -379,13 +379,13 @@ Proof. case (Int.eq (low_u n) Int.zero); intro. exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. simpl. - generalize (low_high_u n). rewrite H. rewrite Int.or_zero. + generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. intuition Simpl. (* xoris + xori *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - intuition Simpl. - rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. + intuition Simpl. + rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. Qed. (** Rotate and mask. *) @@ -406,12 +406,12 @@ Proof. set (rs1 := nextinstr (rs#r1 <- (Val.rolm rs#r2 amount Int.mone))). destruct (andimm_base_correct r1 r1 mask k rs1 m) as [rs' [A [B [C D]]]]; auto. exists rs'. - split. eapply exec_straight_step; eauto. auto. auto. - split. rewrite B. unfold rs1. rewrite nextinstr_inv; auto with asmgen. - rewrite Pregmap.gss. destruct (rs r2); simpl; auto. - unfold Int.rolm. rewrite Int.and_assoc. + split. eapply exec_straight_step; eauto. auto. auto. + split. rewrite B. unfold rs1. rewrite nextinstr_inv; auto with asmgen. + rewrite Pregmap.gss. destruct (rs r2); simpl; auto. + unfold Int.rolm. rewrite Int.and_assoc. decEq; decEq; decEq. rewrite Int.and_commut. apply Int.and_mone. - intros. rewrite D; auto. unfold rs1; Simpl. + intros. rewrite D; auto. unfold rs1; Simpl. Qed. (** Indexed memory loads. *) @@ -433,14 +433,14 @@ Lemma accessind_load_correct: /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r. Proof. intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero). -- econstructor; split. apply exec_straight_one. +- econstructor; split. apply exec_straight_one. rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl. rewrite H1. eauto. unfold nextinstr. repeat Simplif. - split. unfold nextinstr. repeat Simplif. - intros. repeat Simplif. + split. unfold nextinstr. repeat Simplif. + intros. repeat Simplif. - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. - apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen. + apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen. rewrite H1. reflexivity. unfold nextinstr. repeat Simplif. split. repeat Simplif. intros. repeat Simplif. @@ -482,14 +482,14 @@ Lemma accessind_store_correct: /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r. Proof. intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero). -- econstructor; split. apply exec_straight_one. +- econstructor; split. apply exec_straight_one. rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl. rewrite H1. eauto. unfold nextinstr. repeat Simplif. - intros. repeat Simplif. + intros. repeat Simplif. - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. rewrite H0. unfold store2. - rewrite Q. rewrite R by auto with asmgen. rewrite R by auto. + rewrite Q. rewrite R by auto with asmgen. rewrite R by auto. rewrite H1. reflexivity. unfold nextinstr. repeat Simplif. intros. repeat Simplif. Qed. @@ -519,15 +519,15 @@ Lemma floatcomp_correct: forall cmp (r1 r2: freg) k rs m, exists rs', exec_straight ge fn (floatcomp cmp r1 r2 k) rs m k rs' m - /\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) = + /\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) = (if snd (crbit_for_fcmp cmp) then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) - /\ forall r', + /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> rs'#r' = rs#r'. Proof. - intros. + intros. generalize (compare_float_spec rs rs#r1 rs#r2). intros [A [B [C D]]]. set (rs1 := nextinstr (compare_float rs rs#r1 rs#r2)) in *. @@ -538,25 +538,25 @@ Proof. exists rs1. split. destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; apply exec_straight_one; reflexivity. - split. - destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. + split. + destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. rewrite Val.negate_cmpf_eq. auto. auto. (* two instrs *) exists (nextinstr (rs1#CR0_3 <- (Val.cmpf cmp rs#r1 rs#r2))). split. elim H0; intro; subst cmp. apply exec_straight_two with rs1 m. - reflexivity. simpl. + reflexivity. simpl. rewrite C; rewrite A. rewrite Val.or_commut. rewrite <- Val.cmpf_le. reflexivity. reflexivity. reflexivity. apply exec_straight_two with rs1 m. - reflexivity. simpl. + reflexivity. simpl. rewrite C; rewrite B. rewrite Val.or_commut. rewrite <- Val.cmpf_ge. reflexivity. reflexivity. reflexivity. split. elim H0; intro; subst cmp; simpl. reflexivity. reflexivity. - intros. Simpl. + intros. Simpl. Qed. (** Translation of conditions. *) @@ -580,7 +580,7 @@ Lemma transl_cond_correct_1: transl_cond cond args k = OK c -> exists rs', exec_straight ge fn c rs m k rs' m - /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = + /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m))) @@ -594,7 +594,7 @@ Opaque Int.eq. destruct (compare_sint_spec rs (rs x) (rs x0)) as [A [B [C D]]]. econstructor; split. apply exec_straight_one. simpl; reflexivity. reflexivity. - split. + split. case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. auto with asmgen. (* Ccompu *) @@ -602,7 +602,7 @@ Opaque Int.eq. destruct (compare_uint_spec rs m (rs x) (rs x0)) as [A [B [C D]]]. econstructor; split. apply exec_straight_one. simpl; reflexivity. reflexivity. - split. + split. case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. auto with asmgen. (* Ccompimm *) @@ -611,7 +611,7 @@ Opaque Int.eq. destruct (compare_sint_spec rs (rs x) (Vint i)) as [A [B [C D]]]. econstructor; split. apply exec_straight_one. simpl; reflexivity. reflexivity. - split. + split. case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. auto with asmgen. destruct (loadimm_correct GPR0 i (Pcmpw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. @@ -620,8 +620,8 @@ Opaque Int.eq. exists (nextinstr (compare_sint rs1 (rs1 x) (Vint i))). split. eapply exec_straight_trans. eexact EX1. apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto. - reflexivity. - split. rewrite SAME. + reflexivity. + split. rewrite SAME. case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. intros. rewrite SAME; rewrite D; auto with asmgen. (* Ccompuimm *) @@ -630,7 +630,7 @@ Opaque Int.eq. destruct (compare_uint_spec rs m (rs x) (Vint i)) as [A [B [C D]]]. econstructor; split. apply exec_straight_one. simpl; reflexivity. reflexivity. - split. + split. case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. auto with asmgen. destruct (loadimm_correct GPR0 i (Pcmplw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. @@ -639,36 +639,36 @@ Opaque Int.eq. exists (nextinstr (compare_uint rs1 m (rs1 x) (Vint i))). split. eapply exec_straight_trans. eexact EX1. apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto. - reflexivity. - split. rewrite SAME. + reflexivity. + split. rewrite SAME. case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. intros. rewrite SAME; rewrite D; auto with asmgen. (* Ccompf *) fold (Val.cmpf c0 (rs x) (rs x0)). destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - split. apply RES. + exists rs'. split. auto. + split. apply RES. auto with asmgen. (* Cnotcompf *) rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. fold (Val.cmpf c0 (rs x) (rs x0)). destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto. + exists rs'. split. auto. + split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto. auto with asmgen. (* Cmaskzero *) destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. eauto with asmgen. - exists rs'. split. assumption. - split. rewrite C. destruct (rs x); auto. + exists rs'. split. assumption. + split. rewrite C. destruct (rs x); auto. auto with asmgen. (* Cmasknotzero *) destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. eauto with asmgen. - exists rs'. split. assumption. + exists rs'. split. assumption. split. rewrite C. destruct (rs x); auto. fold (option_map negb (Some (Int.eq (Int.and i0 i) Int.zero))). - rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto. + rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto. auto with asmgen. Qed. @@ -678,7 +678,7 @@ Lemma transl_cond_correct_2: eval_condition cond (map rs (map preg_of args)) m = Some b -> exists rs', exec_straight ge fn c rs m k rs' m - /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = + /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_bool b else Val.notbool (Val.of_bool b)) @@ -687,7 +687,7 @@ Proof. intros. replace (Val.of_bool b) with (Val.of_optbool (eval_condition cond rs ## (preg_of ## args) m)). - eapply transl_cond_correct_1; eauto. + eapply transl_cond_correct_1; eauto. rewrite H0; auto. Qed. @@ -699,14 +699,14 @@ Lemma transl_cond_correct_3: Mem.extends m m' -> exists rs', exec_straight ge fn c rs m' k rs' m' - /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = + /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_bool b else Val.notbool (Val.of_bool b)) /\ agree ms sp rs'. Proof. intros. - exploit transl_cond_correct_2. eauto. + exploit transl_cond_correct_2. eauto. eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [rs' [A [B C]]]. exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto. @@ -722,21 +722,21 @@ Remark add_carry_eq0: Proof. intros. rewrite <- Int.sub_add_l. rewrite Int.add_zero_l. rewrite Int.sub_idem. rewrite Int.add_zero_l. fold (Int.not i). - predSpec Int.eq Int.eq_spec i Int.zero. + predSpec Int.eq Int.eq_spec i Int.zero. subst i. reflexivity. - unfold Val.of_bool, Vfalse. decEq. + unfold Val.of_bool, Vfalse. decEq. unfold Int.add_carry. rewrite Int.unsigned_zero. rewrite Int.unsigned_one. apply zlt_true. - generalize (Int.unsigned_range (Int.not i)); intro. + generalize (Int.unsigned_range (Int.not i)); intro. assert (Int.unsigned (Int.not i) <> Int.modulus - 1). red; intros. assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone). Local Transparent Int.repr. - rewrite H1. apply Int.mkint_eq. reflexivity. - rewrite Int.repr_unsigned in H2. + rewrite H1. apply Int.mkint_eq. reflexivity. + rewrite Int.repr_unsigned in H2. assert (Int.not (Int.not i) = Int.zero). rewrite H2. apply Int.mkint_eq; reflexivity. - rewrite Int.not_involutive in H3. + rewrite Int.not_involutive in H3. congruence. omega. Qed. @@ -749,10 +749,10 @@ Remark add_carry_ne0: Proof. intros. fold (Int.not (Int.add i Int.mone)). rewrite Int.not_neg. rewrite (Int.add_commut (Int.neg (Int.add i Int.mone))). - rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem. + rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem. rewrite Int.add_zero_l. rewrite Int.add_neg_zero. rewrite Int.add_zero_l. Transparent Int.eq. - unfold Int.add_carry, Int.eq. + unfold Int.add_carry, Int.eq. rewrite Int.unsigned_zero. rewrite Int.unsigned_mone. unfold negb, Val.of_bool, Vtrue, Vfalse. destruct (zeq (Int.unsigned i) 0); decEq. @@ -774,25 +774,25 @@ Proof. (* eq 0 *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. destruct (rs x0); simpl; auto. + split. Simpl. destruct (rs x0); simpl; auto. apply add_carry_eq0. intros; Simpl. (* ne 0 *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. rewrite gpr_or_zero_not_zero; eauto with asmgen. - split. Simpl. destruct (rs x0); simpl; auto. + split. Simpl. destruct (rs x0); simpl; auto. apply add_carry_ne0. intros; Simpl. (* ge 0 *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. rewrite Val.rolm_ge_zero. auto. + split. Simpl. rewrite Val.rolm_ge_zero. auto. intros; Simpl. (* lt 0 *) econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. Simpl. rewrite Val.rolm_lt_zero. auto. + split. Simpl. rewrite Val.rolm_lt_zero. auto. intros; Simpl. (* default *) set (bit := fst (crbit_for_cond c)) in *. @@ -803,15 +803,15 @@ Proof. then k else Pxori x x (Cint Int.one) :: k)). generalize (transl_cond_correct_1 c rl k1 rs m c0 EQ0). - fold bit; fold isset. + fold bit; fold isset. intros [rs1 [EX1 [RES1 AG1]]]. destruct isset. (* bit set *) - econstructor; split. eapply exec_straight_trans. eexact EX1. + econstructor; split. eapply exec_straight_trans. eexact EX1. unfold k1. apply exec_straight_one; simpl; reflexivity. intuition Simpl. (* bit clear *) - econstructor; split. eapply exec_straight_trans. eexact EX1. + econstructor; split. eapply exec_straight_trans. eexact EX1. unfold k1. eapply exec_straight_two; simpl; reflexivity. intuition Simpl. rewrite RES1. destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto. @@ -840,8 +840,8 @@ Opaque Int.eq. TranslOpSimpl. TranslOpSimpl. (* Ointconst *) - destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. - exists rs'. auto with asmgen. + destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. + exists rs'. auto with asmgen. (* Oaddrsymbol *) set (v' := Genv.symbol_address ge i i0). destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. @@ -853,13 +853,13 @@ Opaque Val.add. (* relative data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. Simpl. - apply low_high_half_zero. + apply low_high_half_zero. intros; Simpl. (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. apply low_high_half_zero. - intros; Simpl. + intros; Simpl. (* Oaddrstack *) destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. exists rs'; auto with asmgen. @@ -869,21 +869,21 @@ Opaque Val.add. (* Oaddsymbol *) destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. (* small data *) - econstructor; split. eapply exec_straight_two; simpl; reflexivity. + econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite (Val.add_commut (rs x)). f_equal. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. (* relative data *) - econstructor; split. eapply exec_straight_trans. + econstructor; split. eapply exec_straight_trans. eapply exec_straight_two; simpl; reflexivity. eapply exec_straight_two; simpl; reflexivity. split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen). Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl. rewrite low_high_half_zero. auto. - intros; Simpl. + intros; Simpl. (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl. + split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl. rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). rewrite low_high_half. auto. intros; Simpl. (* Osubimm *) @@ -892,7 +892,7 @@ Opaque Val.add. destruct (loadimm_correct GPR0 i (Psubfc x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. - split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. + split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. intros; Simpl. (* Omulimm *) case (Int.eq (high_s i) Int.zero). @@ -900,15 +900,15 @@ Opaque Val.add. destruct (loadimm_correct GPR0 i (Pmullw x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. - split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. + split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. intros; Simpl. (* Odivs *) replace v with (Val.maketotal (Val.divs (rs x) (rs x0))). - TranslOpSimpl. + TranslOpSimpl. rewrite H1; auto. (* Odivu *) replace v with (Val.maketotal (Val.divu (rs x) (rs x0))). - TranslOpSimpl. + TranslOpSimpl. rewrite H1; auto. (* Oand *) set (v' := Val.and (rs x) (rs x0)) in *. @@ -932,8 +932,8 @@ Opaque Val.add. destruct (rs x); simpl; auto. rewrite Int.or_idem. auto. (* Oshrximm *) econstructor; split. - eapply exec_straight_two; simpl; reflexivity. - split. Simpl. apply Val.shrx_carry. auto. + eapply exec_straight_two; simpl; reflexivity. + split. Simpl. apply Val.shrx_carry. auto. intros; Simpl. (* Orolm *) destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]; eauto with asmgen. @@ -969,9 +969,9 @@ Lemma transl_op_correct: /\ agree (Regmap.set res v (Mach.undef_regs (destroyed_by_op op) ms)) sp rs' /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. - intros. - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. - intros [v' [A B]]. rewrite (sp_val _ _ _ H0) in A. + intros. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. + intros [v' [A B]]. rewrite (sp_val _ _ _ H0) in A. exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]]. rewrite <- Q in B. exists rs'; split. eexact P. @@ -999,7 +999,7 @@ Lemma transl_memory_access_correct: exists rs', exec_straight ge fn c rs m k rs' m' /\ P rs'. Proof. - intros until m'; intros TR ADDR TEMP MK1 MK2. + intros until m'; intros TR ADDR TEMP MK1 MK2. unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR. (* Aindexed *) case (Int.eq (high_s i) Int.zero). @@ -1015,37 +1015,37 @@ Transparent Val.add. intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. auto. auto. (* Aindexed2 *) apply MK2; auto. (* Aglobal *) destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. (* Aglobal from small data *) - apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. + apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. auto. (* Aglobal from relative data *) set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))). exploit (MK1 (Cint Int.zero) temp rs2). - simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. unfold rs2. Simpl. rewrite Val.add_commut. apply add_zero_symbol_address. - intros; unfold rs2, rs1; Simpl. + intros; unfold rs2, rs1; Simpl. intros [rs' [EX' AG']]. - exists rs'; split. apply exec_straight_step with rs1 m; auto. - apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. + exists rs'; split. apply exec_straight_step with rs1 m; auto. + apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal. unfold rs1; Simpl. apply low_high_half_zero. eexact EX'. auto. (* Aglobal from absolute data *) set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). exploit (MK1 (Csymbol_low i i0) temp rs1). - simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. - unfold rs1. Simpl. apply low_high_half_zero. - intros; unfold rs1; Simpl. + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. + unfold rs1. Simpl. apply low_high_half_zero. + intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. - exists rs'; split. apply exec_straight_step with rs1 m; auto. + exists rs'; split. apply exec_straight_step with rs1 m; auto. eexact EX'. auto. (* Abased *) destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]. @@ -1055,8 +1055,8 @@ Transparent Val.add. unfold rs1; Simpl. apply Val.add_commut. intros. unfold rs1; Simpl. intros [rs' [EX' AG']]. - exists rs'; split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. + exists rs'; split. apply exec_straight_step with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. unfold const_low. rewrite small_data_area_addressing; auto. apply add_zero_symbol_address. reflexivity. @@ -1066,20 +1066,20 @@ Transparent Val.add. set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))). set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))). exploit (MK2 temp GPR0 rs3). - f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. + f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. intros. unfold rs3, rs2, rs1; Simpl. intros [rs' [EX' AG']]. - exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). - apply exec_straight_three with rs1 m rs2 m; auto. - simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. - unfold rs2; Simpl. apply low_high_half_zero. - eexact EX'. auto. + exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). + apply exec_straight_three with rs1 m rs2 m; auto. + simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. + unfold rs2; Simpl. apply low_high_half_zero. + eexact EX'. auto. (* Abased absolute *) set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))). exploit (MK1 (Csymbol_low i i0) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. - unfold rs1. Simpl. - rewrite Val.add_assoc. rewrite low_high_half. apply Val.add_commut. + unfold rs1. Simpl. + rewrite Val.add_assoc. rewrite low_high_half. apply Val.add_commut. intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. @@ -1087,10 +1087,10 @@ Transparent Val.add. assumption. assumption. (* Ainstack *) destruct (Int.eq (high_s i) Int.zero); inv TR. - apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s i) (Int.repr 16)))))). exploit (MK1 (Cint (low_s i)) temp rs1 k). - simpl. rewrite gpr_or_zero_not_zero; auto. + simpl. rewrite gpr_or_zero_not_zero; auto. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. congruence. @@ -1129,12 +1129,12 @@ Proof. /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r). { intros. eapply transl_memory_access_correct; eauto. congruence. - intros. econstructor; split. apply exec_straight_one. - rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto. + intros. econstructor; split. apply exec_straight_one. + rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. intuition Simpl. - intros. econstructor; split. apply exec_straight_one. - rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto. + intros. econstructor; split. apply exec_straight_one. + rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. intuition Simpl. } @@ -1142,17 +1142,17 @@ Proof. - (* Mint8signed *) assert (exists v1, Mem.loadv Mint8unsigned m a = Some v1 /\ v = Val.sign_ext 8 v1). { - destruct a; simpl in *; try discriminate. - rewrite Mem.load_int8_signed_unsigned in H1. + destruct a; simpl in *; try discriminate. + rewrite Mem.load_int8_signed_unsigned in H1. destruct (Mem.load Mint8unsigned m b (Int.unsigned i)); simpl in H1; inv H1. exists v0; auto. } - destruct H as [v1 [LD SG]]. clear H1. + destruct H as [v1 [LD SG]]. clear H1. exploit BASE; eauto; erewrite ireg_of_eq by eauto; auto. intros [rs1 [A [B C]]]. - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. - split. Simpl. congruence. intros. Simpl. + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split. Simpl. congruence. intros. Simpl. - (* Mint8unsigned *) eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. - (* Mint816signed *) @@ -1185,9 +1185,9 @@ Local Transparent destroyed_by_store. assert (TEMP1: int_temp_for src <> GPR0). destruct TEMP0; congruence. assert (TEMP2: IR (int_temp_for src) <> preg_of src). - unfold int_temp_for. destruct (mreg_eq src R12). + unfold int_temp_for. destruct (mreg_eq src R12). subst src; simpl; congruence. - change (IR GPR12) with (preg_of R12). red; intros; elim n. + change (IR GPR12) with (preg_of R12). red; intros; elim n. eapply preg_of_injective; eauto. assert (BASE: forall mk1 mk2 chunk', transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c -> @@ -1203,12 +1203,12 @@ Local Transparent destroyed_by_store. /\ forall r, r <> PC -> r <> GPR0 -> r <> GPR11 /\ r <> GPR12 -> rs' r = rs r). { intros. eapply transl_memory_access_correct; eauto. - intros. econstructor; split. apply exec_straight_one. - rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. - intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. - intros. econstructor; split. apply exec_straight_one. - rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. - intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. + intros. econstructor; split. apply exec_straight_one. + rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. + intros. econstructor; split. apply exec_straight_one. + rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. } destruct chunk; monadInv H. - (* Mint8signed *) -- cgit