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 --- common/AST.v | 12 ++++----- common/Globalenvs.v | 72 ++++++++++++++++++++++++++--------------------------- common/Memory.v | 36 +++++++++++++-------------- common/PrintAST.ml | 2 +- common/Values.v | 10 ++++---- 5 files changed, 66 insertions(+), 66 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 40da732..d2065d6 100644 --- a/common/AST.v +++ b/common/AST.v @@ -225,10 +225,10 @@ Proof. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. - destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. exists f; auto. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. - destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. Qed. @@ -245,10 +245,10 @@ Proof. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. - destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. - destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto. exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. @@ -394,11 +394,11 @@ Proof. monadInv EQ. constructor. destruct a as [id [f|v]]. (* function *) - destruct (transf_fun f) as [tf|?]_eqn; monadInv EQ. + destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. constructor; auto. constructor; auto. (* variable *) unfold transf_globvar in EQ. - destruct (transf_var (gvar_info v)) as [tinfo|?]_eqn; simpl in EQ; monadInv EQ. + destruct (transf_var (gvar_info v)) as [tinfo|?] eqn:?; simpl in EQ; monadInv EQ. constructor; auto. destruct v; simpl in *. constructor; auto. Qed. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 100cab8..d426440 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -607,14 +607,14 @@ Proof. unfold alloc_global. intros. destruct g as [id [f|v]]. (* function *) - destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. - destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. - destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. - destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate. + destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?. + destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate. + destruct (store_init_data_list m2 b 0 init) as [m3|] eqn:?; try discriminate. erewrite Mem.nextblock_drop; eauto. erewrite store_init_data_list_nextblock; eauto. erewrite store_zeros_nextblock; eauto. @@ -629,7 +629,7 @@ Proof. induction gl. simpl; intros. inv H; unfold block; omega. simpl length; rewrite inj_S; simpl; intros. - destruct (alloc_global m a) as [m1|]_eqn; try discriminate. + destruct (alloc_global m a) as [m1|] eqn:?; try discriminate. erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega. Qed. @@ -672,7 +672,7 @@ Remark alloc_global_perm: Proof. intros. destruct idg as [id [f|v]]; simpl in H. (* function *) - destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. split; intros. eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto. @@ -680,9 +680,9 @@ Proof. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. - destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. - destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. - destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate. + destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?. + destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate. + destruct (store_init_data_list m2 b 0 init) as [m3|] eqn:?; try discriminate. assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. split; intros. eapply Mem.perm_drop_3; eauto. @@ -703,7 +703,7 @@ Remark alloc_globals_perm: Proof. induction gl. simpl; intros. inv H. tauto. - simpl; intros. destruct (alloc_global m a) as [m1|]_eqn; try discriminate. + simpl; intros. destruct (alloc_global m a) as [m1|] eqn:?; try discriminate. erewrite alloc_global_perm; eauto. eapply IHgl; eauto. unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. Qed. @@ -734,7 +734,7 @@ Remark store_init_data_list_outside: Proof. induction il; simpl. intros; congruence. - intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence. + intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. transitivity (Mem.load chunk m1 b' q). eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega. destruct a; simpl in Heqo; @@ -784,7 +784,7 @@ Proof. induction il; simpl. auto. - intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence. + intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. exploit IHil; eauto. intro D. destruct a; simpl in Heqo; intuition. eapply (A Mint8unsigned (Vint i)); eauto. @@ -804,7 +804,7 @@ Remark load_alloc_global: Proof. intros. destruct g as [f|v]; simpl in H. (* function *) - destruct (Mem.alloc m 0 1) as [m1 b']_eqn. + destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. transitivity (Mem.load chunk m1 b p). eapply Mem.load_drop; eauto. @@ -812,9 +812,9 @@ Proof. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. - destruct (Mem.alloc m 0 sz) as [m1 b']_eqn. - destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate. - destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate. + destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?. + destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate. + destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate. assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. transitivity (Mem.load chunk m3 b p). eapply Mem.load_drop; eauto. @@ -833,7 +833,7 @@ Remark load_alloc_globals: Proof. induction gl; simpl; intros. congruence. - destruct (alloc_global m a) as [m''|]_eqn; try discriminate. + destruct (alloc_global m a) as [m''|] eqn:?; try discriminate. transitivity (Mem.load chunk m'' b p). apply IHgl; auto. unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. @@ -895,9 +895,9 @@ Proof. inv H3. simpl in H0. set (init := gvar_init gv) in *. set (sz := init_data_list_size init) in *. - destruct (Mem.alloc m 0 sz) as [m1 b']_eqn. - destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate. - destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate. + destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?. + destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate. + destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate. exploit Mem.alloc_result; eauto. intro RES. replace (genv_next ge0) with b' by congruence. split. red; intros. eapply Mem.perm_drop_1; eauto. @@ -928,7 +928,7 @@ Proof. destruct (ZIndexed.eq b (genv_next ge0)). (* same *) inv H3. simpl in H0. - destruct (Mem.alloc m 0 1) as [m1 b']_eqn. + destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. exploit Mem.alloc_result; eauto. intro RES. replace (genv_next ge0) with b' by congruence. split. eapply Mem.perm_drop_1; eauto. omega. @@ -964,7 +964,7 @@ Lemma alloc_globals_initialized: Proof. induction gl; simpl; intros. inv H0; auto. - destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|]_eqn; try discriminate. + destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|] eqn:?; try discriminate. exploit alloc_global_initialized; eauto. intros [P [Q R]]. eapply IHgl; eauto. Qed. @@ -1099,16 +1099,16 @@ Lemma alloc_global_neutral: Proof. intros. destruct idg as [id [f|v]]; simpl in H. (* function *) - destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_inject_neutral; eauto. eapply Mem.alloc_inject_neutral; eauto. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. - destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. - destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. - destruct (store_init_data_list ge m2 b 0 init) as [m3|]_eqn; try discriminate. + destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?. + destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate. + destruct (store_init_data_list ge m2 b 0 init) as [m3|] eqn:?; try discriminate. assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_inject_neutral; eauto. eapply store_init_data_list_neutral with (m := m2) (b := b); eauto. @@ -1210,7 +1210,7 @@ Lemma alloc_global_augment: Proof. intros. destruct idg as [id [f|v]]; simpl in H. (* function *) - destruct (Mem.alloc m2 0 1) as [m3 b]_eqn. + destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?. assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_outside_inject. 2: eauto. eapply Mem.alloc_right_inject; eauto. @@ -1219,9 +1219,9 @@ Proof. (* variable *) set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. - destruct (Mem.alloc m2 0 sz) as [m3 b]_eqn. - destruct (store_zeros m3 b 0 sz) as [m4|]_eqn; try discriminate. - destruct (store_init_data_list ge m4 b 0 init) as [m5|]_eqn; try discriminate. + destruct (Mem.alloc m2 0 sz) as [m3 b] eqn:?. + destruct (store_zeros m3 b 0 sz) as [m4|] eqn:?; try discriminate. + destruct (store_init_data_list ge m4 b 0 init) as [m5|] eqn:?; try discriminate. assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_outside_inject. 2: eauto. eapply store_init_data_list_augment. 3: eauto. 2: eauto. @@ -1497,7 +1497,7 @@ Proof. assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' -> store_init_data (globalenv p') m b ofs a = Some m'). destruct a; simpl; auto. rewrite find_symbol_match. auto. - simpl in H. destruct (find_symbol (globalenv p) i) as [b'|]_eqn; try discriminate. + simpl in H. destruct (find_symbol (globalenv p) i) as [b'|] eqn:?; try discriminate. apply new_ids_fresh. congruence. case_eq (store_init_data (globalenv p) m b ofs a); intros. rewrite H1 in H. @@ -1513,14 +1513,14 @@ Lemma alloc_globals_match: Proof. induction 1; simpl; intros. auto. - destruct (alloc_global (globalenv p) m a1) as [m1|]_eqn; try discriminate. + destruct (alloc_global (globalenv p) m a1) as [m1|] eqn:?; try discriminate. assert (alloc_global (globalenv p') m b1 = Some m1). inv H; simpl in *. auto. set (sz := init_data_list_size init) in *. - destruct (Mem.alloc m 0 sz) as [m2 b]_eqn. - destruct (store_zeros m2 b 0 sz) as [m3|]_eqn; try discriminate. - destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|]_eqn; try discriminate. + destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?. + destruct (store_zeros m2 b 0 sz) as [m3|] eqn:?; try discriminate. + destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|] eqn:?; try discriminate. erewrite store_init_data_list_match; eauto. rewrite H2. eauto. Qed. @@ -1718,7 +1718,7 @@ Hypothesis transf_OK: Remark transf_augment_OK: transform_partial_augment_program transf_fun transf_var nil p.(prog_main) p = OK p'. Proof. - rewrite <- transf_OK. apply symmetry. apply transform_partial_program2_augment. + rewrite <- transf_OK. symmetry. apply transform_partial_program2_augment. Qed. Theorem find_funct_ptr_transf_partial2: diff --git a/common/Memory.v b/common/Memory.v index 37f21d7..514e1e0 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1023,7 +1023,7 @@ Proof. decEq. rewrite store_mem_contents; simpl. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. destruct H. congruence. - destruct (zle n 0). + destruct (zle n 0) as [z | n0]. rewrite (nat_of_Z_neg _ z). auto. destruct H. omegaContradiction. apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv. @@ -1108,7 +1108,7 @@ Proof. assert (length mvl = sz). generalize (encode_val_length chunk v). rewrite <- H1. rewrite SZ. simpl; congruence. - rewrite H4. rewrite size_chunk_conv in z0. omega. + rewrite H4. rewrite size_chunk_conv in *. omega. contradiction. (* 3. ofs > ofs': @@ -1126,8 +1126,8 @@ Proof. rewrite setN_outside. rewrite ZMap.gss. auto. omega. assert (~memval_valid_first (c'#ofs)). rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. - apply H4. apply getN_in. rewrite size_chunk_conv in z. - rewrite SZ' in z. rewrite inj_S in z. omega. + apply H4. apply getN_in. rewrite size_chunk_conv in *. + rewrite SZ' in *. rewrite inj_S in *. omega. contradiction. Qed. @@ -3632,18 +3632,18 @@ Lemma mem_inj_compose: Proof. intros. unfold compose_meminj. inv H; inv H0; constructor; intros. (* perm *) - destruct (f b1) as [[b' delta'] |]_eqn; try discriminate. - destruct (f' b') as [[b'' delta''] |]_eqn; inv H. + destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. + destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega. eauto. (* valid access *) - destruct (f b1) as [[b' delta'] |]_eqn; try discriminate. - destruct (f' b') as [[b'' delta''] |]_eqn; inv H. + destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. + destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega. eauto. (* memval *) - destruct (f b1) as [[b' delta'] |]_eqn; try discriminate. - destruct (f' b') as [[b'' delta''] |]_eqn; inv H. + destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. + destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega. eapply memval_inject_compose; eauto. Qed. @@ -3661,15 +3661,15 @@ Proof. intros. erewrite mi_freeblocks0; eauto. (* mapped *) intros. - destruct (f b) as [[b1 delta1] |]_eqn; try discriminate. - destruct (f' b1) as [[b2 delta2] |]_eqn; inv H. + destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. + destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. eauto. (* no overlap *) red; intros. - destruct (f b1) as [[b1x delta1x] |]_eqn; try discriminate. - destruct (f' b1x) as [[b1y delta1y] |]_eqn; inv H0. - destruct (f b2) as [[b2x delta2x] |]_eqn; try discriminate. - destruct (f' b2x) as [[b2y delta2y] |]_eqn; inv H1. + destruct (f b1) as [[b1x delta1x] |] eqn:?; try discriminate. + destruct (f' b1x) as [[b1y delta1y] |] eqn:?; inv H0. + destruct (f b2) as [[b2x delta2x] |] eqn:?; try discriminate. + destruct (f' b2x) as [[b2y delta2y] |] eqn:?; inv H1. exploit mi_no_overlap0; eauto. intros A. destruct (eq_block b1x b2x). subst b1x. destruct A. congruence. @@ -3680,8 +3680,8 @@ Proof. unfold block; omega. (* representable *) intros. - destruct (f b) as [[b1 delta1] |]_eqn; try discriminate. - destruct (f' b1) as [[b2 delta2] |]_eqn; inv H. + destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. + destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. exploit mi_representable0; eauto. intros [A B]. set (ofs' := Int.repr (Int.unsigned ofs + delta1)). assert (Int.unsigned ofs' = Int.unsigned ofs + delta1). diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 53741d5..7f2ed3f 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -42,7 +42,7 @@ let name_of_external = function | EF_malloc -> "malloc" | EF_free -> "free" | EF_memcpy(sz, al) -> - sprintf "memcpy size %ld align %ld " (camlint_of_z sz) (camlint_of_z al) + sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al) | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text) diff --git a/common/Values.v b/common/Values.v index 1c03789..177cd93 100644 --- a/common/Values.v +++ b/common/Values.v @@ -620,7 +620,7 @@ Theorem modu_divu: modu x y = Some z -> exists v, divu x y = Some v /\ z = sub x (mul v y). Proof. intros. destruct x; destruct y; simpl in *; try discriminate. - destruct (Int.eq i0 Int.zero) as []_eqn; inv H. + destruct (Int.eq i0 Int.zero) eqn:?; inv H. exists (Vint (Int.divu i i0)); split; auto. simpl. rewrite Int.modu_divu. auto. generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto. @@ -731,7 +731,7 @@ Theorem shrx_carry: add (shr x y) (shr_carry x y) = z. Proof. intros. destruct x; destruct y; simpl in H; inv H. - destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1. + destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. @@ -746,7 +746,7 @@ Theorem shrx_shr: z = shr (if Int.lt p Int.zero then add x (Vint (Int.sub (Int.shl Int.one q) Int.one)) else x) (Vint q). Proof. intros. destruct x; destruct y; simpl in H; inv H. - destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1. + destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. @@ -1030,8 +1030,8 @@ Proof. destruct v1; simpl in H2; try discriminate; destruct v2; simpl in H2; try discriminate; inv H0; inv H1; simpl; auto. - destruct (valid_ptr b0 (Int.unsigned i)) as []_eqn; try discriminate. - destruct (valid_ptr b1 (Int.unsigned i0)) as []_eqn; try discriminate. + destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate. + destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate. rewrite (H _ _ Heqb2). rewrite (H _ _ Heqb0). auto. Qed. -- cgit v1.2.3