From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: Ported to Coq 8.4pl1. Merge of branches/coq-8.4. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof1.v | 2 ++ powerpc/ConstpropOpproof.v | 20 ++++++++++---------- powerpc/Op.v | 16 ++++++++-------- powerpc/PrintAsm.ml | 2 +- powerpc/SelectOpproof.v | 24 ++++++++++++------------ 5 files changed, 33 insertions(+), 31 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 2af4f700..f1c206e8 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1516,6 +1516,7 @@ Lemma transl_load_correct: Proof. intros. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + unfold PregEq.t. intros [a' [A B]]. exploit Mem.loadv_extends; eauto. intros [v' [C D]]. apply transl_load_store_correct with ms; auto. @@ -1570,6 +1571,7 @@ Lemma transl_store_correct: Proof. intros. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + unfold PregEq.t. intros [a' [A B]]. assert (Z: Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m1' [C D]]. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index eef39448..7d557c6d 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -155,7 +155,7 @@ Proof. destruct (propagate_float_constants tt); simpl; auto. unfold eval_static_condition_val, Val.of_optbool. - destruct (eval_static_condition c vl0) as []_eqn. + destruct (eval_static_condition c vl0) eqn:?. rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). destruct b; simpl; auto. simpl; auto. @@ -240,7 +240,7 @@ Proof. intros; unfold make_shlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; intros. + destruct (Int.ltu n Int.iwordsize) eqn:?; intros. rewrite Val.shl_rolm; auto. econstructor; split; eauto. auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -254,7 +254,7 @@ Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shr_zero. auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn. + destruct (Int.ltu n Int.iwordsize) eqn:?. econstructor; split; eauto. simpl. auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -268,7 +268,7 @@ Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; intros. + destruct (Int.ltu n Int.iwordsize) eqn:?; intros. rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -284,7 +284,7 @@ Proof. exists (Vint Int.zero); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_zero; auto. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto. - destruct (Int.is_power2 n) as []_eqn; intros. + destruct (Int.is_power2 n) eqn:?; intros. rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). rewrite Val.shl_rolm. econstructor; split; eauto. auto. eapply Int.is_power2_range; eauto. @@ -299,8 +299,8 @@ Lemma make_divimm_correct: exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. - destruct (Int.is_power2 n) as []_eqn. - destruct (Int.ltu i (Int.repr 31)) as []_eqn. + destruct (Int.is_power2 n) eqn:?. + destruct (Int.ltu i (Int.repr 31)) eqn:?. exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. exists v; auto. exists v; auto. @@ -314,7 +314,7 @@ Lemma make_divuimm_correct: exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. - destruct (Int.is_power2 n) as []_eqn. + destruct (Int.is_power2 n) eqn:?. econstructor; split. simpl; eauto. exploit Int.is_power2_range; eauto. intros RANGE. rewrite <- Val.shru_rolm; auto. rewrite H0 in H. @@ -439,10 +439,10 @@ Lemma builtin_strength_reduction_correct: Proof. intros until m'. unfold builtin_strength_reduction. destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA. - unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H in H0. + unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0. rewrite volatile_load_global_charact. exists b; auto. inv H0. - unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H1 in H0. + unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0. rewrite volatile_store_global_charact. exists b; auto. inv H0. auto. diff --git a/powerpc/Op.v b/powerpc/Op.v index e59e15f1..58bcb2ca 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -576,8 +576,8 @@ Proof. right. apply Int.no_overlap_sound; auto. (* Aglobal *) unfold symbol_address in *. - destruct (Genv.find_symbol ge i1) as []_eqn; inv H2. - destruct (Genv.find_symbol ge i) as []_eqn; inv H1. + destruct (Genv.find_symbol ge i1) eqn:?; inv H2. + destruct (Genv.find_symbol ge i) eqn:?; inv H1. destruct (ident_eq i i1). subst. replace (Int.unsigned n1) with (Int.unsigned (Int.add Int.zero n1)). replace (Int.unsigned n2) with (Int.unsigned (Int.add Int.zero n2)). @@ -587,9 +587,9 @@ Proof. left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto. (* Abased *) unfold symbol_address in *. - destruct (Genv.find_symbol ge i1) as []_eqn; simpl in *; try discriminate. + destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate. destruct v; inv H2. - destruct (Genv.find_symbol ge i) as []_eqn; inv H1. + destruct (Genv.find_symbol ge i) eqn:?; inv H1. destruct (ident_eq i i1). subst. rewrite (Int.add_commut i0 i3). rewrite (Int.add_commut i2 i3). right. apply Int.no_overlap_sound; auto. @@ -706,8 +706,8 @@ Opaque Int.add. Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b -> Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b). intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. - destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) as []_eqn; try discriminate. - destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) as []_eqn; try discriminate. + destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate. + destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. rewrite (valid_pointer_inj _ H2 Heqb4). rewrite (valid_pointer_inj _ H Heqb0). simpl. destruct (zeq b1 b0); simpl in H1. @@ -792,7 +792,7 @@ Proof. inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2. exists (Vint i); auto. inv H4; inv H2; simpl; auto. - subst v1. destruct (eval_condition c vl1 m1) as []_eqn. + subst v1. destruct (eval_condition c vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. @@ -923,7 +923,7 @@ Hypothesis sp_inj: f sp1 = Some(sp2, delta). Remark symbol_address_inject: forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs). Proof. - intros. unfold symbol_address. destruct (Genv.find_symbol genv id) as []_eqn; auto. + intros. unfold symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. econstructor; eauto. rewrite Int.add_zero; auto. Qed. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index a20448c3..f56c3f22 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -924,7 +924,7 @@ let print_init oc = function (Int64.logand b 0xFFFFFFFFL) comment (camlfloat_of_coqfloat n) | Init_space n -> - let n = camlint_of_z n in + let n = Z.to_int32 n in if n > 0l then fprintf oc " .space %ld\n" n | Init_addrof(symb, ofs) -> fprintf oc " .long %a\n" diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 5e493662..7be88580 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -232,7 +232,7 @@ 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) as []_eqn. + 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. @@ -244,7 +244,7 @@ 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) as []_eqn. + 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. @@ -257,7 +257,7 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero. intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto. case (shrimm_match a); intros. - destruct (Int.lt mask1 Int.zero) as []_eqn. + destruct (Int.lt mask1 Int.zero) eqn:?. TrivialExists. replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). apply eval_shruimm; auto. @@ -331,7 +331,7 @@ Proof. InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto. set (n' := Int.and n n2). destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' && - Int.ltu amount Int.iwordsize) as []_eqn. + Int.ltu amount Int.iwordsize) eqn:?. 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)) @@ -349,7 +349,7 @@ Proof. 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) as []_eqn. + Int.ltu amount Int.iwordsize) eqn:?. 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)) @@ -402,20 +402,20 @@ Theorem eval_or: binary_constructor_sound or Val.or. Proof. red; intros until y; unfold or; case (or_match a b); intros. (* rolm - rolm *) - destruct (Int.eq amount1 amount2 && same_expr_pure t1 t2) as []_eqn. + 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. rewrite Val.or_rolm. TrivialExists. TrivialExists. (* andimm - rolm *) - destruct (Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2) as []_eqn. + destruct (Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2) eqn:?. destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec mask1 (Int.not mask2)); rewrite H1; intros. InvEval. subst. TrivialExists. TrivialExists. (* rolm - andimm *) - destruct (Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1) as []_eqn. + destruct (Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1) eqn:?. destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec mask2 (Int.not mask1)); rewrite H1; intros. InvEval. subst. rewrite Val.or_commut. TrivialExists. @@ -507,7 +507,7 @@ Theorem eval_divuimm: exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v. Proof. intros; unfold divuimm. - destruct (Int.is_power2 n) as []_eqn. + destruct (Int.is_power2 n) eqn:?. replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto. eapply Val.divu_pow2; eauto. TrivialExists. @@ -533,7 +533,7 @@ Theorem eval_moduimm: exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v. Proof. intros; unfold moduimm. - destruct (Int.is_power2 n) as []_eqn. + destruct (Int.is_power2 n) eqn:?. replace z with (Val.and x (Vint (Int.sub n Int.one))). apply eval_andimm; auto. eapply Val.modu_pow2; eauto. exploit Val.modu_divu; eauto. intros [v [A B]]. @@ -758,7 +758,7 @@ Theorem eval_intuoffloat: exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. intros. destruct x; simpl in H0; try discriminate. - destruct (Float.intuoffloat f) as [n|]_eqn; simpl in H0; inv H0. + destruct (Float.intuoffloat f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. set (im := Int.repr Int.half_modulus). set (fm := Float.floatofintu im). @@ -770,7 +770,7 @@ Proof. econstructor. instantiate (1 := Vfloat fm). EvalOp. eapply eval_Econdition with (vb := Float.cmp Clt f fm). eauto with evalexpr. auto. - destruct (Float.cmp Clt f fm) as []_eqn. + destruct (Float.cmp Clt f fm) eqn:?. exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. exploit Float.intuoffloat_intoffloat_2; eauto. -- cgit