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 --- arm/Asmgenproof.v | 6 ++++-- arm/Asmgenproof1.v | 14 +++++++++----- arm/ConstpropOpproof.v | 16 ++++++++-------- arm/Op.v | 12 ++++++------ arm/PrintAsm.ml | 2 +- arm/SelectOpproof.v | 30 +++++++++++++++--------------- 6 files changed, 43 insertions(+), 37 deletions(-) (limited to 'arm') diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 8ee9c2e..b0598e9 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -1087,7 +1087,8 @@ Proof. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros A. exploit transl_cond_correct. eauto. eauto. - instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. + instantiate (1 := rs). instantiate (1 := m'). + rewrite A || (unfold PregEq.t; rewrite A). intros [rs2 [EX [RES OTH]]]. inv AT. simpl in H5. generalize (functions_transl _ _ H4); intro FN. @@ -1123,7 +1124,8 @@ Proof. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros A. exploit transl_cond_correct. eauto. - instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. + instantiate (1 := rs). instantiate (1 := m'). + rewrite A || (unfold PregEq.t; rewrite A). intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. exists m'; split; auto. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index e7d2509..19edcd9 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -539,7 +539,7 @@ Proof. auto. rewrite IHl. rewrite DISTR. decEq. decEq. auto. intros. unfold decompose_int. - destruct (decompose_int_rec 12 n Int.zero) as []_eqn. + destruct (decompose_int_rec 12 n Int.zero) eqn:?. simpl. exploit decompose_int_rec_nil; eauto. congruence. simpl. rewrite B. decEq. generalize (DECOMP 12%nat n Int.zero Int.zero). @@ -617,7 +617,7 @@ Lemma iterate_op_correct: Proof. intros until k; intros SEM2 SEM1. unfold iterate_op. - destruct (decompose_int n) as [ | i tl] _eqn. + destruct (decompose_int n) as [ | i tl] eqn:?. unfold decompose_int in Heql. destruct (decompose_int_rec 12%nat n Int.zero); congruence. revert k. pattern tl. apply List.rev_ind. (* base case *) @@ -1256,7 +1256,7 @@ Proof. eapply exec_straight_trans. eauto. apply exec_straight_two with rs2 m; auto. simpl. unfold rs3, v. - destruct (rs2 (crbit_for_cond c)) as []_eqn; auto. + destruct (rs2 (crbit_for_cond c)) eqn:?; auto. destruct (Int.eq i Int.zero); auto. decEq. decEq. apply extensionality; intros. unfold Pregmap.set. destruct (PregEq.eq x (ireg_of res)); auto. subst. @@ -1380,6 +1380,7 @@ Lemma transl_load_int_correct: Proof. intros. unfold transl_load_store_int. 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. @@ -1421,6 +1422,7 @@ Lemma transl_load_float_correct: Proof. intros. unfold transl_load_store_int. 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. @@ -1455,7 +1457,8 @@ Lemma transl_store_int_correct: /\ agree (undef_temps ms) sp rs'. Proof. intros. unfold transl_load_store_int. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + unfold PregEq.t. intros [a' [A B]]. exploit preg_val; eauto. instantiate (1 := rd). intros C. exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. @@ -1498,7 +1501,8 @@ Lemma transl_store_float_correct: /\ agree (undef_temps ms) sp rs'. Proof. intros. unfold transl_load_store_float. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + unfold PregEq.t. intros [a' [A B]]. exploit preg_val; eauto. instantiate (1 := rd). intros C. exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 4c38d5e..e7e6a41 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -149,7 +149,7 @@ Proof. destruct (propagate_float_constants tt); simpl; auto. 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. @@ -247,7 +247,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. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -261,7 +261,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; intros. + destruct (Int.ltu n Int.iwordsize) eqn:?; intros. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -275,7 +275,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. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -291,7 +291,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. exploit Int.is_power2_range; eauto. intros R. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). auto. @@ -306,8 +306,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. @@ -321,7 +321,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:?. replace v with (Val.shru rs#r1 (Vint i)). econstructor; split. simpl. rewrite mk_shift_amount_eq. eauto. eapply Int.is_power2_range; eauto. auto. diff --git a/arm/Op.v b/arm/Op.v index cfe8b83..f26bccc 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -775,8 +775,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. @@ -796,8 +796,8 @@ Opaque Int.add. eapply CMPU; eauto. eapply CMP. eauto. eapply eval_shift_inj. eauto. auto. eapply CMPU. eauto. eapply eval_shift_inj. eauto. auto. - eapply CMP; eauto. - eapply CMPU; eauto. + eapply CMP; try eassumption; eauto. + eapply CMPU; try eassumption; eauto. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; simpl in H0; inv H0; auto. @@ -871,7 +871,7 @@ Proof. inv H4; simpl in *; inv H1. TrivialExists. inv H4; simpl in *; inv H1. TrivialExists. - 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. @@ -1005,7 +1005,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/arm/PrintAsm.ml b/arm/PrintAsm.ml index 6415248..9d09fc1 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -719,7 +719,7 @@ let print_init oc = function fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.bits_of_double n)) 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 " .word %a\n" print_symb_ofs (symb, ofs) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index e25fb0c..ecc758f 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -204,10 +204,10 @@ Opaque mk_shift_amount. red; intros until x. unfold shlimm. predSpec Int.eq Int.eq_spec n Int.zero. intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl. + destruct (Int.ltu n Int.iwordsize) eqn:?; simpl. destruct (shlimm_match a); intros. InvEval. simpl; rewrite Heqb. TrivialExists. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. InvEval. subst x. exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp. simpl. rewrite mk_shift_amount_eq; auto. destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0. @@ -224,10 +224,10 @@ Proof. 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) as []_eqn; simpl. + destruct (Int.ltu n Int.iwordsize) eqn:?; simpl. destruct (shrimm_match a); intros. InvEval. simpl; rewrite Heqb. TrivialExists. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. InvEval. subst x. exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp. simpl. rewrite mk_shift_amount_eq; auto. destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0. @@ -244,13 +244,13 @@ Proof. red; intros until x. unfold shruimm. predSpec Int.eq Int.eq_spec n Int.zero. intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl. + destruct (Int.ltu n Int.iwordsize) eqn:?; simpl. destruct (shruimm_match a); intros. InvEval. simpl; rewrite Heqb. TrivialExists. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. InvEval. subst x. exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp. simpl. rewrite mk_shift_amount_eq; auto. - destruct v1; simpl; auto. destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto. + destruct v1; simpl; auto. destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto. rewrite Heqb; rewrite Heqb0. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto. TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. @@ -379,27 +379,27 @@ Proof. rewrite Val.or_commut. apply eval_orimm; auto. apply eval_orimm; auto. (* shl - shru *) - destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn. + destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?. destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. exists (Val.ror v0 (Vint n2)); split. EvalOp. destruct v0; simpl; auto. - destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto. - destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto. + destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto. + destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. simpl. rewrite <- Int.or_ror; auto. subst. TrivialExists. econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor. simpl. auto. (* shru - shr *) - destruct (Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2) as []_eqn. + destruct (Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2) eqn:?. destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec (Int.add n2 n1) Int.iwordsize); rewrite H1; intros. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. exists (Val.ror v0 (Vint n1)); split. EvalOp. destruct v0; simpl; auto. - destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto. - destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto. + destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto. + destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto. subst. TrivialExists. econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor. @@ -490,7 +490,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. @@ -516,7 +516,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))). TrivialExists. eapply Val.modu_pow2; eauto. exploit Val.modu_divu; eauto. intros [v [A B]]. -- cgit v1.2.3