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. --- powerpc/SelectOpproof.v | 304 ++++++++++++++++++++++++------------------------ 1 file changed, 152 insertions(+), 152 deletions(-) (limited to 'powerpc/SelectOpproof.v') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 147132dd..b40ad21b 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -32,7 +32,7 @@ Open Local Scope cminorsel_scope. (** The following are trivial lemmas and custom tactics that help perform backward (inversion) and forward reasoning over the evaluation - of operator applications. *) + of operator applications. *) Ltac EvalOp := eapply eval_Eop; eauto with evalexpr. @@ -117,8 +117,8 @@ Theorem eval_addrsymbol: forall le id ofs, exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v. Proof. - intros. unfold addrsymbol. econstructor; split. - EvalOp. simpl; eauto. + intros. unfold addrsymbol. econstructor; split. + EvalOp. simpl; eauto. auto. Qed. @@ -127,7 +127,7 @@ Theorem eval_addrstack: exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v. Proof. intros. unfold addrstack. econstructor; split. - EvalOp. simpl; eauto. + EvalOp. simpl; eauto. auto. Qed. @@ -138,20 +138,20 @@ Proof. unfold notint; red; intros until x; case (notint_match a); intros; InvEval. TrivialExists. subst. exists v1; split; auto. - subst. TrivialExists. + subst. TrivialExists. subst. TrivialExists. subst. TrivialExists. subst. exists (Val.and v1 v0); split; auto. EvalOp. subst. exists (Val.or v1 v0); split; auto. EvalOp. subst. exists (Val.xor v1 v0); split; auto. EvalOp. - subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp. + subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp. destruct v0; destruct v1; simpl; auto. rewrite Int.not_and_or_not. rewrite Int.not_involutive. rewrite Int.or_commut. auto. - subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. + subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive. rewrite Int.and_commut. auto. subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. auto. - TrivialExists. + TrivialExists. Qed. Theorem eval_addimm: @@ -159,7 +159,7 @@ Theorem eval_addimm: Proof. red; unfold addimm; intros until x. predSpec Int.eq Int.eq_spec n Int.zero. - subst n. intros. exists x; split; auto. + subst n. intros. exists x; split; auto. destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto. case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl. rewrite Int.add_commut. auto. @@ -167,15 +167,15 @@ Proof. rewrite Val.add_assoc. rewrite Int.add_commut. auto. subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto. subst. rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut. -Qed. +Qed. Theorem eval_addsymbol: forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (Genv.symbol_address ge s ofs)). Proof. red; unfold addsymbol; intros until x. case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl. - rewrite Genv.shift_symbol_address. auto. - rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. + rewrite Genv.shift_symbol_address. auto. + rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. apply Val.add_commut. Qed. @@ -187,36 +187,36 @@ Proof. - apply eval_addimm; auto. - apply eval_addsymbol; auto. - rewrite Val.add_commut. apply eval_addsymbol; auto. -- subst. +- subst. replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2))) with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. decEq. apply Val.add_permut. -- subst. +- subst. replace (Val.add (Val.add v1 (Vint n1)) y) with (Val.add (Val.add v1 y) (Vint n1)). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. decEq. apply Val.add_commut. -- subst. TrivialExists. +- subst. TrivialExists. econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. simpl. repeat rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_commut. rewrite Val.add_permut. auto. - replace (Val.add x y) with (Val.add (Genv.symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)). - apply eval_addsymbol; auto. EvalOp. - subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. + apply eval_addsymbol; auto. EvalOp. + subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. rewrite Val.add_permut. f_equal. apply Val.add_commut. -- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. +- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. - subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. -- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp. -- TrivialExists. +- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp. +- TrivialExists. Qed. Theorem eval_subimm: forall n, unary_constructor_sound (subimm n) (fun v => Val.sub (Vint n) v). Proof. intros; red; intros until x. unfold subimm. destruct (subimm_match a); intros. - InvEval. TrivialExists. + InvEval. TrivialExists. InvEval. subst x. TrivialExists. unfold eval_operation. destruct v1; simpl; auto. rewrite ! Int.sub_add_opp. rewrite Int.add_assoc. f_equal. f_equal. f_equal. rewrite Int.neg_add_distr. apply Int.add_commut. @@ -229,7 +229,7 @@ Proof. unfold sub; case (sub_match a b); intros; InvEval. rewrite Val.sub_add_opp. apply eval_addimm; auto. apply eval_subimm; auto. - subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. + subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp. apply eval_addimm; EvalOp. subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. @@ -239,7 +239,7 @@ Qed. Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v). Proof. - red; intros. unfold negint. apply eval_subimm; auto. + red; intros. unfold negint. apply eval_subimm; auto. Qed. Lemma eval_rolm: @@ -248,7 +248,7 @@ Lemma eval_rolm: (fun x => Val.rolm x amount mask). Proof. red; intros until x. unfold rolm; case (rolm_match a); intros; InvEval. - TrivialExists. + TrivialExists. subst. rewrite Val.rolm_rolm. TrivialExists. subst. rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm. rewrite (Int.add_commut Int.zero). rewrite Int.add_zero. TrivialExists. @@ -262,8 +262,8 @@ Proof. red; intros. unfold shlimm. predSpec Int.eq Int.eq_spec n Int.zero. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto. - destruct (Int.ltu n Int.iwordsize) eqn:?. - rewrite Val.shl_rolm; auto. apply eval_rolm; auto. + destruct (Int.ltu n Int.iwordsize) eqn:?. + rewrite Val.shl_rolm; auto. apply eval_rolm; auto. TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto. Qed. @@ -274,8 +274,8 @@ Proof. red; intros. unfold shruimm. predSpec Int.eq Int.eq_spec n Int.zero. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto. - destruct (Int.ltu n Int.iwordsize) eqn:?. - rewrite Val.shru_rolm; auto. apply eval_rolm; auto. + destruct (Int.ltu n Int.iwordsize) eqn:?. + rewrite Val.shru_rolm; auto. apply eval_rolm; auto. TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto. Qed. @@ -283,18 +283,18 @@ Theorem eval_shrimm: forall n, unary_constructor_sound (fun a => shrimm a n) (fun x => Val.shr x (Vint n)). Proof. - red; intros until x. unfold shrimm. + red; intros until x. unfold shrimm. predSpec Int.eq Int.eq_spec n Int.zero. intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto. destruct (Int.ltu n Int.iwordsize) eqn:WS. case (shrimm_match a); intros. InvEval. exists (Vint (Int.shr n1 n)); split. EvalOp. simpl; rewrite WS; auto. - simpl; destruct (Int.lt mask1 Int.zero) eqn:?. + simpl; destruct (Int.lt mask1 Int.zero) eqn:?. TrivialExists. - replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). + replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). apply eval_shruimm; auto. destruct x; simpl; auto. rewrite WS. - decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. + decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. apply Int.shr_and_is_shru_and; auto. simpl. TrivialExists. intros. simpl. TrivialExists. @@ -304,13 +304,13 @@ Qed. Lemma eval_mulimm_base: forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)). Proof. - intros; red; intros; unfold mulimm_base. - generalize (Int.one_bits_decomp n). + intros; red; intros; unfold mulimm_base. + generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). destruct (Int.one_bits n). - intros. TrivialExists. + intros. TrivialExists. destruct l. - intros. rewrite H1. simpl. + intros. rewrite H1. simpl. rewrite Int.add_zero. replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul. apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib. @@ -325,27 +325,27 @@ Proof. replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one i0))) with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint i0))). rewrite Val.mul_add_distr_r. - repeat rewrite Val.shl_mul. apply Val.add_lessdef; auto. - simpl. repeat rewrite H0; auto with coqlib. - intros. TrivialExists. + repeat rewrite Val.shl_mul. apply Val.add_lessdef; auto. + simpl. repeat rewrite H0; auto with coqlib. + intros. TrivialExists. Qed. Theorem eval_mulimm: forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Vint n)). Proof. intros; red; intros until x; unfold mulimm. - predSpec Int.eq Int.eq_spec n Int.zero. - intros. exists (Vint Int.zero); split. EvalOp. + predSpec Int.eq Int.eq_spec n Int.zero. + intros. exists (Vint Int.zero); split. EvalOp. destruct x; simpl; auto. subst n. rewrite Int.mul_zero. auto. predSpec Int.eq Int.eq_spec n Int.one. intros. exists x; split; auto. destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto. case (mulimm_match a); intros; InvEval. TrivialExists. simpl. rewrite Int.mul_commut; auto. - subst. rewrite Val.mul_add_distr_l. + subst. rewrite Val.mul_add_distr_l. exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]]. exploit (eval_addimm (Int.mul n n2) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]]. - exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto. + exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto. rewrite Val.mul_commut; auto. apply eval_mulimm_base; auto. Qed. @@ -354,7 +354,7 @@ Theorem eval_mul: binary_constructor_sound mul Val.mul. Proof. red; intros until y. unfold mul; case (mul_match a b); intros; InvEval. - rewrite Val.mul_commut. apply eval_mulimm. auto. + rewrite Val.mul_commut. apply eval_mulimm. auto. apply eval_mulimm. auto. TrivialExists. Qed. @@ -362,9 +362,9 @@ Qed. Theorem eval_andimm: forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)). Proof. - intros; red; intros until x. unfold andimm. + intros; red; intros until x. unfold andimm. predSpec Int.eq Int.eq_spec n Int.zero. - intros. subst. exists (Vint Int.zero); split. EvalOp. + intros. subst. exists (Vint Int.zero); split. EvalOp. destruct x; simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone. intros. subst. exists x; split. auto. @@ -372,10 +372,10 @@ Proof. clear H H0. case (andimm_match a); intros. InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto. - set (n' := Int.and n n2). + set (n' := Int.and n n2). destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' && Int.ltu amount Int.iwordsize) eqn:?. - InvEval. destruct (andb_prop _ _ Heqb). + InvEval. destruct (andb_prop _ _ Heqb). generalize (Int.eq_spec (Int.shru (Int.shl n' amount) amount) n'). rewrite H1; intros. replace (Val.and x (Vint n)) with (Val.rolm v0 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n')). @@ -383,26 +383,26 @@ Proof. subst. destruct v0; simpl; auto. rewrite H3. simpl. decEq. rewrite Int.and_assoc. rewrite (Int.and_commut n2 n). transitivity (Int.and (Int.shru i amount) (Int.and n n2)). - rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. + rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. symmetry. apply Int.shr_and_shru_and. auto. set (e2 := Eop (Oshrimm amount) (t2 ::: Enil)) in *. - InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. - InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. - InvEval. subst. TrivialExists. simpl. - destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc. + InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. + InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. + InvEval. subst. TrivialExists. simpl. + destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc. decEq. decEq. decEq. apply Int.and_commut. destruct (Int.eq (Int.shru (Int.shl n amount) amount) n && Int.ltu amount Int.iwordsize) eqn:?. - InvEval. destruct (andb_prop _ _ Heqb). + InvEval. destruct (andb_prop _ _ Heqb). generalize (Int.eq_spec (Int.shru (Int.shl n amount) amount) n). rewrite H0; intros. replace (Val.and x (Vint n)) with (Val.rolm v1 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n)). apply eval_rolm; auto. - subst x. destruct v1; simpl; auto. rewrite H1; simpl. decEq. + subst x. destruct v1; simpl; auto. rewrite H1; simpl. decEq. transitivity (Int.and (Int.shru i amount) n). - rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. + rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. symmetry. apply Int.shr_and_shru_and. auto. - TrivialExists. + TrivialExists. TrivialExists. Qed. @@ -426,7 +426,7 @@ Proof. intros. subst. exists (Vint Int.mone); split. EvalOp. destruct x; simpl; auto. rewrite Int.or_mone; auto. clear H H0. destruct (orimm_match a); intros; InvEval. TrivialExists. simpl. rewrite Int.or_commut; auto. - subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. + subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. TrivialExists. Qed. @@ -438,10 +438,10 @@ Remark eval_same_expr: a1 = a2 /\ v1 = v2. Proof. intros until v2. - destruct a1; simpl; try (intros; discriminate). + destruct a1; simpl; try (intros; discriminate). destruct a2; simpl; try (intros; discriminate). case (ident_eq i i0); intros. - subst i0. inversion H0. inversion H1. split. auto. congruence. + subst i0. inversion H0. inversion H1. split. auto. congruence. discriminate. Qed. @@ -452,29 +452,29 @@ Proof. destruct (Int.eq amount1 amount2 && same_expr_pure t1 t2) eqn:?. destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec amount1 amount2). rewrite H1. intro. subst amount2. - InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. + InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. rewrite Val.or_rolm. TrivialExists. TrivialExists. (* andimm - rolm *) destruct (Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2) eqn:?. - destruct (andb_prop _ _ Heqb0). + destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec mask1 (Int.not mask2)); rewrite H1; intros. - InvEval. subst. TrivialExists. + InvEval. subst. TrivialExists. TrivialExists. (* rolm - andimm *) destruct (Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1) eqn:?. - destruct (andb_prop _ _ Heqb0). + destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec mask2 (Int.not mask1)); rewrite H1; intros. InvEval. subst. rewrite Val.or_commut. TrivialExists. TrivialExists. (* intconst *) - InvEval. rewrite Val.or_commut. apply eval_orimm; auto. + InvEval. rewrite Val.or_commut. apply eval_orimm; auto. InvEval. apply eval_orimm; auto. (* orc *) InvEval. subst. rewrite Val.or_commut. TrivialExists. InvEval. subst. TrivialExists. (* default *) - TrivialExists. + TrivialExists. Qed. Theorem eval_xorimm: @@ -484,11 +484,11 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero. intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.xor_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone. - intros. subst. rewrite <- Val.not_xor. apply eval_notint; auto. + intros. subst. rewrite <- Val.not_xor. apply eval_notint; auto. clear H H0. destruct (xorimm_match a); intros; InvEval. TrivialExists. simpl. rewrite Int.xor_commut; auto. subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. - subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. + subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut; auto. TrivialExists. Qed. @@ -498,7 +498,7 @@ Proof. red; intros until y; unfold xor; case (xor_match a b); intros; InvEval. rewrite Val.xor_commut. apply eval_xorimm; auto. apply eval_xorimm; auto. - subst. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. + subst. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. rewrite Val.xor_commut. TrivialExists. subst. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. TrivialExists. TrivialExists. @@ -524,19 +524,19 @@ Lemma eval_mod_aux: eval_expr ge sp e m le (mod_aux divop a b) (Val.sub x (Val.mul z y)). Proof. intros; unfold mod_aux. - eapply eval_Elet. eexact H0. eapply eval_Elet. + eapply eval_Elet. eexact H0. eapply eval_Elet. apply eval_lift. eexact H1. - eapply eval_Eop. eapply eval_Econs. + eapply eval_Eop. eapply eval_Econs. eapply eval_Eletvar. simpl; reflexivity. - eapply eval_Econs. eapply eval_Eop. + eapply eval_Econs. eapply eval_Eop. eapply eval_Econs. eapply eval_Eop. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. + apply eval_Enil. rewrite H. eauto. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. - simpl; reflexivity. apply eval_Enil. + apply eval_Enil. + simpl; reflexivity. apply eval_Enil. reflexivity. Qed. @@ -547,7 +547,7 @@ Theorem eval_mods_base: Val.mods x y = Some z -> exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v. Proof. - intros; unfold mods_base. + intros; unfold mods_base. exploit Val.mods_divs; eauto. intros [v [A B]]. subst. econstructor; split; eauto. apply eval_mod_aux with (semdivop := Val.divs); auto. @@ -570,7 +570,7 @@ Theorem eval_modu_base: Val.modu x y = Some z -> exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v. Proof. - intros; unfold modu_base. + intros; unfold modu_base. exploit Val.modu_divu; eauto. intros [v [A B]]. subst. econstructor; split; eauto. apply eval_mod_aux with (semdivop := Val.divu); auto. @@ -582,13 +582,13 @@ Theorem eval_shrximm: Val.shrx x (Vint n) = Some z -> exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v. Proof. - intros. unfold shrximm. + intros. unfold shrximm. predSpec Int.eq Int.eq_spec n Int.zero. - subst n. exists x; split; auto. + subst n. exists x; split; auto. destruct x; simpl in H0; try discriminate. destruct (Int.ltu Int.zero (Int.repr 31)); inv H0. - replace (Int.shrx i Int.zero) with i. auto. - unfold Int.shrx, Int.divs. rewrite Int.shl_zero. + replace (Int.shrx i Int.zero) with i. auto. + unfold Int.shrx, Int.divs. rewrite Int.shl_zero. change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. econstructor; split. EvalOp. auto. Qed. @@ -597,38 +597,38 @@ Theorem eval_shl: binary_constructor_sound shl Val.shl. Proof. red; intros until y; unfold shl; case (shl_match b); intros. InvEval. apply eval_shlimm; auto. - TrivialExists. + TrivialExists. Qed. Theorem eval_shr: binary_constructor_sound shr Val.shr. Proof. red; intros until y; unfold shr; case (shr_match b); intros. InvEval. apply eval_shrimm; auto. - TrivialExists. + TrivialExists. Qed. Theorem eval_shru: binary_constructor_sound shru Val.shru. Proof. red; intros until y; unfold shru; case (shru_match b); intros. InvEval. apply eval_shruimm; auto. - TrivialExists. + TrivialExists. Qed. Theorem eval_negf: unary_constructor_sound negf Val.negf. Proof. - red; intros. TrivialExists. + red; intros. TrivialExists. Qed. Theorem eval_absf: unary_constructor_sound absf Val.absf. Proof. - red; intros. TrivialExists. + red; intros. TrivialExists. Qed. Theorem eval_addf: binary_constructor_sound addf Val.addf. Proof. red; intros; TrivialExists. Qed. - + Theorem eval_subf: binary_constructor_sound subf Val.subf. Proof. red; intros; TrivialExists. @@ -641,19 +641,19 @@ Qed. Theorem eval_negfs: unary_constructor_sound negfs Val.negfs. Proof. - red; intros. TrivialExists. + red; intros. TrivialExists. Qed. Theorem eval_absfs: unary_constructor_sound absfs Val.absfs. Proof. - red; intros. TrivialExists. + red; intros. TrivialExists. Qed. Theorem eval_addfs: binary_constructor_sound addfs Val.addfs. Proof. red; intros; TrivialExists. Qed. - + Theorem eval_subfs: binary_constructor_sound subfs Val.subfs. Proof. red; intros; TrivialExists. @@ -687,8 +687,8 @@ Proof. (* constant *) InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto. (* eq cmp *) - InvEval. inv H. simpl in H5. inv H5. - destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. + InvEval. inv H. simpl in H5. inv H5. + destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto. @@ -697,13 +697,13 @@ Proof. simpl. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto. rewrite sem_undef; auto. - exists (Vint Int.zero); split. EvalOp. + exists (Vint Int.zero); split. EvalOp. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto. rewrite sem_undef; auto. (* ne cmp *) - InvEval. inv H. simpl in H5. inv H5. - destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. + InvEval. inv H. simpl in H5. inv H5. + destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. simpl. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto. rewrite sem_undef; auto. @@ -711,21 +711,21 @@ Proof. simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto. rewrite sem_undef; auto. - exists (Vint Int.one); split. EvalOp. + exists (Vint Int.one); split. EvalOp. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto. rewrite sem_undef; auto. (* eq andimm *) destruct (Int.eq_dec n2 Int.zero). InvEval; subst. - econstructor; split. EvalOp. simpl; eauto. - destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq. - destruct (Int.eq (Int.and i n1) Int.zero); auto. + econstructor; split. EvalOp. simpl; eauto. + destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq. + destruct (Int.eq (Int.and i n1) Int.zero); auto. TrivialExists. simpl. rewrite sem_default. auto. (* ne andimm *) destruct (Int.eq_dec n2 Int.zero). InvEval; subst. - econstructor; split. EvalOp. simpl; eauto. - destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne. - destruct (Int.eq (Int.and i n1) Int.zero); auto. + econstructor; split. EvalOp. simpl; eauto. + destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne. + destruct (Int.eq (Int.and i n1) Int.zero); auto. TrivialExists. simpl. rewrite sem_default. auto. (* default *) TrivialExists. simpl. rewrite sem_default. auto. @@ -740,7 +740,7 @@ Lemma eval_compimm_swap: exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v /\ Val.lessdef (sem c (Vint n2) x) v. Proof. - intros. rewrite <- sem_swap. eapply eval_compimm; eauto. + intros. rewrite <- sem_swap. eapply eval_compimm; eauto. Qed. End COMP_IMM. @@ -749,9 +749,9 @@ Theorem eval_comp: forall c, binary_constructor_sound (comp c) (Val.cmp c). Proof. intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval. - eapply eval_compimm_swap; eauto. + eapply eval_compimm_swap; eauto. intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto. - eapply eval_compimm; eauto. + eapply eval_compimm; eauto. TrivialExists. Qed. @@ -759,9 +759,9 @@ Theorem eval_compu: forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c). Proof. intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval. - eapply eval_compimm_swap; eauto. + eapply eval_compimm_swap; eauto. intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto. - eapply eval_compimm; eauto. + eapply eval_compimm; eauto. TrivialExists. Qed. @@ -777,11 +777,11 @@ Proof. intros; red; intros. unfold compfs. replace (Val.cmpfs c x y) with (Val.cmpf c (Val.floatofsingle x) (Val.floatofsingle y)). - TrivialExists. constructor. EvalOp. simpl; reflexivity. + TrivialExists. constructor. EvalOp. simpl; reflexivity. constructor. EvalOp. simpl; reflexivity. constructor. - auto. - destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl. - rewrite Float32.cmp_double. auto. + auto. + destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl. + rewrite Float32.cmp_double. auto. Qed. Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). @@ -826,7 +826,7 @@ Theorem eval_intoffloat: Val.intoffloat x = Some y -> exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v. Proof. - intros; unfold intoffloat. TrivialExists. + intros; unfold intoffloat. TrivialExists. Qed. Theorem eval_intuoffloat: @@ -845,24 +845,24 @@ Proof. assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)). constructor. auto. econstructor. eauto. - econstructor. instantiate (1 := Vfloat fm). EvalOp. + econstructor. instantiate (1 := Vfloat fm). EvalOp. eapply eval_Econdition with (va := Float.cmp Clt f fm). eauto with evalexpr. destruct (Float.cmp Clt f fm) eqn:?. exploit Float.to_intu_to_int_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. - exploit Float.to_intu_to_int_2; eauto. + exploit Float.to_intu_to_int_2; eauto. change Float.ox8000_0000 with im. fold fm. intro EQ. set (t2 := subf (Eletvar (S O)) (Eletvar O)). set (t3 := intoffloat t2). exploit (eval_subf (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f) (Eletvar O)); eauto. - fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2. + fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2. exploit (eval_addimm Float.ox8000_0000 (Vfloat fm :: Vfloat f :: le) t3). - unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto. - intros [v4 [A4 B4]]. simpl in B4. inv B4. - rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4. - rewrite (Int.add_commut (Int.neg im)) in A4. - rewrite Int.add_neg_zero in A4. + unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto. + intros [v4 [A4 B4]]. simpl in B4. inv B4. + rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4. + rewrite (Int.add_commut (Int.neg im)) in A4. + rewrite Int.add_neg_zero in A4. rewrite Int.add_zero in A4. auto. Qed. @@ -874,18 +874,18 @@ Theorem eval_floatofint: exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v. Proof. intros until y. unfold floatofint. destruct (floatofint_match a); intros. - InvEval. TrivialExists. + InvEval. TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_int i)); split; auto. set (t1 := addimm Float.ox8000_0000 a). set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil). - exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1. + exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1. intros [v1 [A1 B1]]. simpl in B1. inv B1. - exploit (eval_subf le t2). - unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. - unfold eval_operation. eauto. - instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto. + exploit (eval_subf le t2). + unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. + unfold eval_operation. eauto. + instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto. intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_int_from_words. auto. Qed. @@ -902,9 +902,9 @@ Proof. unfold floatofintu. set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil). - exploit (eval_subf le t2). - unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. - unfold eval_operation. eauto. + exploit (eval_subf le t2). + unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. + unfold eval_operation. eauto. instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto. intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_intu_from_words. auto. Qed. @@ -915,14 +915,14 @@ Theorem eval_intofsingle: Val.intofsingle x = Some y -> exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v. Proof. - intros; unfold intofsingle. + intros; unfold intofsingle. assert (Val.intoffloat (Val.floatofsingle x) = Some y). { destruct x; simpl in H0; try discriminate. - destruct (Float32.to_int f) eqn:F; inv H0. - apply Float32.to_int_double in F. - simpl. unfold Float32.to_double in F; rewrite F; auto. + destruct (Float32.to_int f) eqn:F; inv H0. + apply Float32.to_int_double in F. + simpl. unfold Float32.to_double in F; rewrite F; auto. } - apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp. + apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp. Qed. Theorem eval_singleofint: @@ -935,11 +935,11 @@ Proof. assert (exists z, Val.floatofint x = Some z /\ y = Val.singleoffloat z). { destruct x; inv H0. simpl. exists (Vfloat (Float.of_int i)); simpl; split; auto. - f_equal. apply Float32.of_int_double. + f_equal. apply Float32.of_int_double. } - destruct H1 as (z & A & B). subst y. - exploit eval_floatofint; eauto. intros (v & C & D). - exists (Val.singleoffloat v); split. EvalOp. inv D; auto. + destruct H1 as (z & A & B). subst y. + exploit eval_floatofint; eauto. intros (v & C & D). + exists (Val.singleoffloat v); split. EvalOp. inv D; auto. Qed. Theorem eval_intuofsingle: @@ -948,14 +948,14 @@ Theorem eval_intuofsingle: Val.intuofsingle x = Some y -> exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v. Proof. - intros; unfold intuofsingle. + intros; unfold intuofsingle. assert (Val.intuoffloat (Val.floatofsingle x) = Some y). { destruct x; simpl in H0; try discriminate. - destruct (Float32.to_intu f) eqn:F; inv H0. - apply Float32.to_intu_double in F. - simpl. unfold Float32.to_double in F; rewrite F; auto. + destruct (Float32.to_intu f) eqn:F; inv H0. + apply Float32.to_intu_double in F. + simpl. unfold Float32.to_double in F; rewrite F; auto. } - apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp. + apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp. Qed. Theorem eval_singleofintu: @@ -968,11 +968,11 @@ Proof. assert (exists z, Val.floatofintu x = Some z /\ y = Val.singleoffloat z). { destruct x; inv H0. simpl. exists (Vfloat (Float.of_intu i)); simpl; split; auto. - f_equal. apply Float32.of_intu_double. + f_equal. apply Float32.of_intu_double. } - destruct H1 as (z & A & B). subst y. - exploit eval_floatofintu; eauto. intros (v & C & D). - exists (Val.singleoffloat v); split. EvalOp. inv D; auto. + destruct H1 as (z & A & B). subst y. + exploit eval_floatofintu; eauto. intros (v & C & D). + exists (Val.singleoffloat v); split. EvalOp. inv D; auto. Qed. Theorem eval_addressing: @@ -981,7 +981,7 @@ Theorem eval_addressing: v = Vptr b ofs -> match addressing chunk a with (mode, args) => exists vl, - eval_exprlist ge sp e m le args vl /\ + eval_exprlist ge sp e m le args vl /\ eval_addressing ge sp mode vl = Some v end. Proof. @@ -990,12 +990,12 @@ Proof. exists (@nil val). split. eauto with evalexpr. simpl. auto. exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence. exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence. - destruct (can_use_Aindexed2 chunk). + destruct (can_use_Aindexed2 chunk). exists (v1 :: v0 :: nil). split. eauto with evalexpr. simpl. congruence. exists (Vptr b ofs :: nil). split. - constructor. EvalOp. simpl; congruence. constructor. + constructor. EvalOp. simpl; congruence. constructor. simpl. rewrite Int.add_zero. auto. - exists (v :: nil). split. eauto with evalexpr. subst v. simpl. + exists (v :: nil). split. eauto with evalexpr. subst v. simpl. rewrite Int.add_zero. auto. Qed. @@ -1007,7 +1007,7 @@ Proof. intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval. - constructor. - constructor. -- constructor. +- constructor. - simpl in H5. inv H5. constructor. - subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. -- cgit