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 --- backend/CMlexer.mll | 1 + backend/CMparser.mly | 31 +++++++++++++------------- backend/CMtypecheck.ml | 6 ++--- backend/CSEproof.v | 58 ++++++++++++++++++++++++------------------------ backend/Coloringaux.ml | 6 ++--- backend/Constpropproof.v | 20 ++++++++--------- backend/Inliningproof.v | 10 ++++----- backend/Inliningspec.v | 6 ++--- backend/Linearizeaux.ml | 21 ++++-------------- backend/PrintCminor.ml | 9 ++++---- backend/PrintLTLin.ml | 8 +++---- backend/PrintMach.ml | 8 +++---- backend/PrintRTL.ml | 12 +++++----- backend/RREproof.v | 8 +++---- backend/RREtyping.v | 4 ++-- backend/Reloadtyping.v | 2 +- backend/Renumberproof.v | 4 ++-- backend/Selectionproof.v | 6 ++--- backend/Stackingproof.v | 4 ++-- 19 files changed, 104 insertions(+), 120 deletions(-) (limited to 'backend') diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index eac48e0..4083c95 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -14,6 +14,7 @@ (* *********************************************************************) { +open BinNums open Camlcoq open CMparser exception Error of string diff --git a/backend/CMparser.mly b/backend/CMparser.mly index ff77c03..eb3b9ab 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -19,8 +19,7 @@ %{ open Datatypes open Camlcoq -open BinPos -open BinInt +open BinNums open Integers open AST open Cminor @@ -45,16 +44,16 @@ let mkef sg toks = EF_vstore c | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c; EFT_tok "global"; EFT_string s; EFT_int n] -> - EF_vload_global(c, intern_string s, z_of_camlint n) + EF_vload_global(c, intern_string s, coqint_of_camlint n) | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c; EFT_tok "global"; EFT_string s; EFT_int n] -> - EF_vstore_global(c, intern_string s, z_of_camlint n) + EF_vstore_global(c, intern_string s, coqint_of_camlint n) | [EFT_tok "malloc"] -> EF_malloc | [EFT_tok "free"] -> EF_free | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> - EF_memcpy(z_of_camlint sz, z_of_camlint al) + EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al) | [EFT_tok "annot"; EFT_string txt] -> EF_annot(intern_string txt, sg.sig_args) | [EFT_tok "annot_val"; EFT_string txt] -> @@ -183,7 +182,7 @@ let mkwhile expr body = let intconst n = Rconst(Ointconst(coqint_of_camlint n)) -let exitnum n = nat_of_camlint n +let exitnum n = Nat.of_int32 n let mkswitch expr (cases, dfl) = convert_accu := []; @@ -211,25 +210,25 @@ let mkswitch expr (cases, dfl) = ***) let mkmatch_aux expr cases = - let ncases = Int32.of_int (List.length cases) in + let ncases = List.length cases in let rec mktable n = function | [] -> assert false | [key, action] -> [] | (key, action) :: rem -> - (coqint_of_camlint key, nat_of_camlint n) - :: mktable (Int32.succ n) rem in + (coqint_of_camlint key, Nat.of_int n) + :: mktable (n + 1) rem in let sw = - Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in + Sswitch(expr, mktable 0 cases, Nat.of_int (ncases - 1)) in let rec mkblocks body n = function | [] -> assert false | [key, action] -> Sblock(Sseq(body, action)) | (key, action) :: rem -> mkblocks - (Sblock(Sseq(body, Sseq(action, Sexit (nat_of_camlint n))))) - (Int32.pred n) + (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n))))) + (n - 1) rem in - mkblocks (Sblock sw) (Int32.pred ncases) cases + mkblocks (Sblock sw) (ncases - 1) cases let mkmatch expr cases = convert_accu := []; @@ -377,7 +376,7 @@ global_declaration: { $1 } | VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */ { (intern_string $2, - Gvar{gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)]; + Gvar{gvar_info = (); gvar_init = [Init_space(Z.of_sint32 $4)]; gvar_readonly = false; gvar_volatile = false}) } | VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE { (intern_string $2, @@ -413,7 +412,7 @@ init_data: | FLOAT64 FLOATLIT { Init_float64 (coqfloat_of_camlfloat $2) } | FLOAT FLOATLIT { Init_float64 (coqfloat_of_camlfloat $2) } | FLOATLIT { Init_float64 (coqfloat_of_camlfloat $1) } - | LBRACKET INTLIT RBRACKET { Init_space (z_of_camlint $2) } + | LBRACKET INTLIT RBRACKET { Init_space (Z.of_sint32 $2) } | INTLIT LPAREN STRINGLIT RPAREN { Init_addrof (intern_string $3, coqint_of_camlint $1) } ; @@ -462,7 +461,7 @@ parameter_list: stack_declaration: /* empty */ { Z0 } - | STACK INTLIT SEMICOLON { z_of_camlint $2 } + | STACK INTLIT SEMICOLON { Z.of_sint32 $2 } ; var_declarations: diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 408e9ec..39e8c51 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -64,7 +64,7 @@ let type_var env id = raise (Error (sprintf "Unbound variable %s\n" (extern_atom id))) let type_letvar env n = - let n = camlint_of_nat n in + let n = Nat.to_int n in try List.nth env n with Not_found -> @@ -303,8 +303,8 @@ let rec type_stmt env blk ret s = | Sblock s1 -> type_stmt env (blk + 1) ret s1 | Sexit n -> - if camlint_of_nat n >= blk then - raise (Error (sprintf "Bad exit(%d)\n" (camlint_of_nat n))) + if Nat.to_int n >= blk then + raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n))) | Sswitch(e, cases, deflt) -> unify (type_expr env [] e) tint | Sreturn None -> diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 5569123..44d23c8 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -94,7 +94,7 @@ Lemma wf_valnum_reg: wf_numbering n' /\ Plt v n'.(num_next) /\ Ple n.(num_next) n'.(num_next). Proof. intros until v. unfold valnum_reg. intros WF VREG. inversion WF. - destruct ((num_reg n)!r) as [v'|]_eqn. + destruct ((num_reg n)!r) as [v'|] eqn:?. (* found *) inv VREG. split. auto. split. eauto. apply Ple_refl. (* not found *) @@ -174,7 +174,7 @@ Lemma wf_forget_reg: In r (PMap.get v (forget_reg n rd)) -> r <> rd /\ PTree.get r n.(num_reg) = Some v. Proof. unfold forget_reg; intros. inversion H. - destruct ((num_reg n)!rd) as [vd|]_eqn. + destruct ((num_reg n)!rd) as [vd|] eqn:?. rewrite PMap.gsspec in H0. destruct (peq v vd). subst vd. rewrite in_remove in H0. destruct H0. split. auto. eauto. split; eauto. exploit VAL; eauto. congruence. @@ -201,7 +201,7 @@ Lemma wf_add_rhs: wf_numbering (add_rhs n rd rh). Proof. intros. inversion H. unfold add_rhs. - destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|]_eqn. + destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|] eqn:?. (* found *) exploit find_valnum_rhs_correct; eauto. intros IN. split; simpl; intros. @@ -226,16 +226,16 @@ Lemma wf_add_op: wf_numbering n -> wf_numbering (add_op n rd op rs). Proof. - intros. unfold add_op. destruct (is_move_operation op rs) as [r|]_eqn. + intros. unfold add_op. destruct (is_move_operation op rs) as [r|] eqn:?. (* move *) - destruct (valnum_reg n r) as [n' v]_eqn. + destruct (valnum_reg n r) as [n' v] eqn:?. exploit wf_valnum_reg; eauto. intros [A [B C]]. inversion A. constructor; simpl; intros. eauto. rewrite PTree.gsspec in H0. destruct (peq r0 rd). inv H0. auto. eauto. eapply wf_update_reg; eauto. (* not a move *) - destruct (valnum_regs n rs) as [n' vs]_eqn. + destruct (valnum_regs n rs) as [n' vs] eqn:?. exploit wf_valnum_regs; eauto. intros [A [B C]]. eapply wf_add_rhs; eauto. Qed. @@ -270,7 +270,7 @@ Remark kill_eqs_in: Proof. induction eqs; simpl; intros. tauto. - destruct (pred (snd a)) as []_eqn. + destruct (pred (snd a)) eqn:?. exploit IHeqs; eauto. tauto. simpl in H; destruct H. subst a. auto. exploit IHeqs; eauto. tauto. Qed. @@ -289,7 +289,7 @@ Lemma wf_add_store: wf_numbering n -> wf_numbering (add_store n chunk addr rargs rsrc). Proof. intros. unfold add_store. - destruct (valnum_regs n rargs) as [n1 vargs]_eqn. + destruct (valnum_regs n rargs) as [n1 vargs] eqn:?. exploit wf_valnum_regs; eauto. intros [A [B C]]. assert (wf_numbering (kill_equations (filter_after_store chunk addr vargs) n1)). apply wf_kill_equations. auto. @@ -664,7 +664,7 @@ Lemma add_store_satisfiable: numbering_satisfiable ge sp rs m' (add_store n chunk addr args src). Proof. intros. unfold add_store. destruct H0 as [valu A]. - destruct (valnum_regs n args) as [n1 vargs]_eqn. + destruct (valnum_regs n args) as [n1 vargs] eqn:?. exploit valnum_regs_holds; eauto. intros [valu' [B [C D]]]. exploit wf_valnum_regs; eauto. intros [U [V W]]. set (n2 := kill_equations (filter_after_store chunk addr vargs) n1). @@ -704,7 +704,7 @@ Lemma reg_valnum_correct: forall n v r, wf_numbering n -> reg_valnum n v = Some r -> n.(num_reg)!r = Some v. Proof. unfold reg_valnum; intros. inv H. - destruct ((num_val n)#v) as [| r1 rl]_eqn; inv H0. + destruct ((num_val n)#v) as [| r1 rl] eqn:?; inv H0. eapply VAL. rewrite Heql. auto with coqlib. Qed. @@ -755,8 +755,8 @@ Lemma regs_valnums_correct: Proof. induction vl; simpl; intros. inv H. auto. - destruct (reg_valnum n a) as [r1|]_eqn; try discriminate. - destruct (regs_valnums n vl) as [rx|]_eqn; try discriminate. + destruct (reg_valnum n a) as [r1|] eqn:?; try discriminate. + destruct (regs_valnums n vl) as [rx|] eqn:?; try discriminate. inv H. simpl; decEq; auto. eapply (proj2 n_holds); eauto. eapply reg_valnum_correct; eauto. Qed. @@ -770,13 +770,13 @@ Proof. induction niter; simpl; intros. discriminate. destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args) - as [[op1 args1] | ]_eqn. + as [[op1 args1] | ] eqn:?. assert (sem op1 (map valu args1) = Some res). rewrite <- H0. eapply f_sound; eauto. simpl; intros. apply (proj1 n_holds). eapply find_valnum_num_correct; eauto. - destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ]_eqn. + destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ] eqn:?. inv H. eapply IHniter; eauto. - destruct (regs_valnums n args1) as [rl|]_eqn. + destruct (regs_valnums n args1) as [rl|] eqn:?. inv H. erewrite regs_valnums_correct; eauto. discriminate. discriminate. @@ -790,7 +790,7 @@ Lemma reduce_sound: sem op' rs##rl' = Some res. Proof. unfold reduce; intros. - destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ]_eqn; inv H. + destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ] eqn:?; inv H. eapply reduce_rec_sound; eauto. congruence. auto. Qed. @@ -973,21 +973,21 @@ Proof. (* Iop *) exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split. - destruct (is_trivial_op op) as []_eqn. + destruct (is_trivial_op op) eqn:?. eapply exec_Iop'; eauto. rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. - destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. destruct SAT as [valu1 NH1]. exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. assert (wf_numbering n1). eapply wf_valnum_regs; eauto. - destruct (find_rhs n1 (Op op vl)) as [r|]_eqn. + destruct (find_rhs n1 (Op op vl)) as [r|] eqn:?. (* replaced by move *) assert (EV: rhs_evals_to ge sp valu2 (Op op vl) m rs#r). eapply find_rhs_correct; eauto. assert (RES: rs#r = v). red in EV. congruence. eapply exec_Iop'; eauto. simpl. congruence. (* possibly simplified *) - destruct (reduce operation combine_op n1 op args vl) as [op' args']_eqn. + destruct (reduce operation combine_op n1 op args vl) as [op' args'] eqn:?. assert (RES: eval_operation ge sp op' rs##args' m = Some v). eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. intros; eapply combine_op_sound; eauto. @@ -1007,18 +1007,18 @@ Proof. (* Iload *) exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split. - destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. destruct SAT as [valu1 NH1]. exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. assert (wf_numbering n1). eapply wf_valnum_regs; eauto. - destruct (find_rhs n1 (Load chunk addr vl)) as [r|]_eqn. + destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. (* replaced by move *) assert (EV: rhs_evals_to ge sp valu2 (Load chunk addr vl) m rs#r). eapply find_rhs_correct; eauto. assert (RES: rs#r = v). red in EV. destruct EV as [a' [EQ1 EQ2]]. congruence. eapply exec_Iop'; eauto. simpl. congruence. (* possibly simplified *) - destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn. + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. intros; eapply combine_addr_sound; eauto. @@ -1035,12 +1035,12 @@ Proof. (* Istore *) exists (State s' (transf_function' f approx) sp pc' rs m'); split. - destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. destruct SAT as [valu1 NH1]. exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. assert (wf_numbering n1). eapply wf_valnum_regs; eauto. - destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn. + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. intros; eapply combine_addr_sound; eauto. @@ -1093,12 +1093,12 @@ Proof. eapply kill_loads_satisfiable; eauto. (* Icond *) - destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. elim SAT; intros valu1 NH1. exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. assert (wf_numbering n1). eapply wf_valnum_regs; eauto. - destruct (reduce condition combine_cond n1 cond args vl) as [cond' args']_eqn. + destruct (reduce condition combine_cond n1 cond args vl) as [cond' args'] eqn:?. assert (RES: eval_condition cond' rs##args' m = Some b). eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. intros; eapply combine_cond_sound; eauto. @@ -1124,8 +1124,8 @@ Proof. (* internal function *) monadInv H7. unfold transf_function in EQ. - destruct (type_function f) as [tyenv|]_eqn; try discriminate. - destruct (analyze f) as [approx|]_eqn; inv EQ. + destruct (type_function f) as [tyenv|] eqn:?; try discriminate. + destruct (analyze f) as [approx|] eqn:?; inv EQ. assert (WTF: wt_function f tyenv). apply type_function_correct; auto. econstructor; split. eapply exec_function_internal; eauto. diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index 2fce25e..ddd3094 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -12,8 +12,6 @@ open Camlcoq open Datatypes -open BinPos -open BinInt open AST open Maps open Registers @@ -766,8 +764,8 @@ let rec reuse_slot conflicts n mvlist = let find_slot conflicts typ = let rec find curr = let l = S(Local(curr, typ)) in - if Locset.mem l conflicts then find (coq_Zsucc curr) else l - in find Z0 + if Locset.mem l conflicts then find (Z.succ curr) else l + in find Z.zero let assign_color n = let conflicts = ref Locset.empty in diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 1b90666..cd757cd 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -199,9 +199,9 @@ Lemma eval_static_load_sound: val_match_approx ge sp (eval_static_load gapp chunk addr) v. Proof. intros. unfold eval_static_load. destruct addr; simpl; auto. - destruct (gapp!i) as [il|]_eqn; auto. + destruct (gapp!i) as [il|] eqn:?; auto. red in H1. subst vaddr. unfold symbol_address in H. - destruct (Genv.find_symbol ge i) as [b'|]_eqn; simpl in H; try discriminate. + destruct (Genv.find_symbol ge i) as [b'|] eqn:?; simpl in H; try discriminate. exploit H0; eauto. intros [A [B C]]. eapply eval_load_init_sound; eauto. red; auto. @@ -290,7 +290,7 @@ Proof. \/ id0 <> id /\ ga!id0 = Some il). destruct gd. rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. - destruct (gvar_readonly v && negb (gvar_volatile v)) as []_eqn. + destruct (gvar_readonly v && negb (gvar_volatile v)) eqn:?. rewrite PTree.gsspec in H0. destruct (peq id0 id). inv H0. left. split; auto. destruct v; simpl in *. @@ -455,10 +455,10 @@ Lemma match_successor_rec: Proof. induction n; simpl; intros. apply match_pc_base. - destruct (fn_code f)!pc as [i|]_eqn; try apply match_pc_base. + destruct (fn_code f)!pc as [i|] eqn:?; try apply match_pc_base. destruct i; try apply match_pc_base. eapply match_pc_nop; eauto. - destruct (eval_static_condition c (approx_regs app l)) as [b|]_eqn. + destruct (eval_static_condition c (approx_regs app l)) as [b|] eqn:?. eapply match_pc_cond; eauto. apply match_pc_base. Qed. @@ -607,7 +607,7 @@ Proof. assert (MATCH'': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v). eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto. unfold transfer; rewrite H. auto. - destruct (const_for_result a) as [cop|]_eqn; intros. + destruct (const_for_result a) as [cop|] eqn:?; intros. (* constant is propagated *) left; econstructor; econstructor; split. eapply exec_Iop; eauto. @@ -640,7 +640,7 @@ Proof. eapply approx_regs_val_list; eauto. assert (VM2: val_match_approx ge sp ap2 v). eapply eval_static_load_sound; eauto. - destruct (const_for_result ap2) as [cop|]_eqn; intros. + destruct (const_for_result ap2) as [cop|] eqn:?; intros. (* constant-propagated *) left; econstructor; econstructor; split. eapply exec_Iop; eauto. eapply const_for_result_correct; eauto. @@ -708,7 +708,7 @@ Proof. (* Ibuiltin *) rename pc'0 into pc. Opaque builtin_strength_reduction. - destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args']_eqn. + destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args'] eqn:?. generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs MATCH2 ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0). rewrite Heqp. intros P. @@ -732,7 +732,7 @@ Opaque builtin_strength_reduction. destruct (cond_strength_reduction cond args (approx_regs (analyze gapp f) # pc args)) as [cond' args']. intros EV1 TCODE. left; exists O; exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. - destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) as []_eqn. + destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) eqn:?. assert (eval_condition cond rs ## args m = Some b0). eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto. assert (b = b0) by congruence. subst b0. @@ -758,7 +758,7 @@ Opaque builtin_strength_reduction. rename pc'0 into pc. assert (A: (fn_code (transf_function gapp f))!pc = Some(Ijumptable arg tbl) \/ (fn_code (transf_function gapp f))!pc = Some(Inop pc')). - TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) as []_eqn; auto. + TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) eqn:?; auto. generalize (MATCH2 arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. simpl. intro EQ; inv EQ. rewrite H1. auto. assert (B: rs'#arg = Vint n). diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 8de8487..9536141 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -306,7 +306,7 @@ Lemma range_private_free_left: range_private F m1 m' sp base hi. Proof. intros; red; intros. - destruct (zlt ofs (base + Zmax sz 0)). + destruct (zlt ofs (base + Zmax sz 0)) as [z|z]. red; split. replace ofs with ((ofs - base) + base) by omega. eapply Mem.perm_inject; eauto. @@ -342,7 +342,7 @@ Proof. red; intros. exploit RP; eauto. intros [A B]. destruct UNCH as [U1 U2]. split. auto. - intros. red in SEP. destruct (F b) as [[sp1 delta1] |]_eqn. + intros. red in SEP. destruct (F b) as [[sp1 delta1] |] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. red; intros; eelim B; eauto. eapply PERM; eauto. red. destruct (zlt b (Mem.nextblock m1)); auto. @@ -710,7 +710,7 @@ Proof. induction 1; intros. apply match_stacks_nil with bound1; auto. inv MG. constructor; intros; eauto. - destruct (F1 b1) as [[b2' delta']|]_eqn. + destruct (F1 b1) as [[b2' delta']|] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto. exploit SEP; eauto. intros [A B]. elim B. red. omega. eapply match_stacks_cons; eauto. @@ -919,7 +919,7 @@ Proof. eapply agree_val_regs; eauto. (* inlined *) assert (fd = Internal f0). - simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate. + simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate. exploit (funenv_program_compat prog); eauto. intros. unfold ge in H0. congruence. subst fd. @@ -973,7 +973,7 @@ Proof. eapply Mem.free_left_inject; eauto. (* inlined *) assert (fd = Internal f0). - simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate. + simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate. exploit (funenv_program_compat prog); eauto. intros. unfold ge in H0. congruence. subst fd. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 014986d..06826c2 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -498,7 +498,7 @@ Proof. (* tailcall *) destruct (can_inline fe s1) as [|id f P Q]. (* not inlined *) - destruct (retinfo ctx) as [[rpc rreg] | ]_eqn. + destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. (* turned into a call *) eapply tr_tailcall_call; eauto. (* preserved *) @@ -526,7 +526,7 @@ Proof. red; simpl. subst s2; simpl in *; xomega. red; auto. (* return *) - destruct (retinfo ctx) as [[rpc rreg] | ]_eqn. + destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. (* inlined *) eapply tr_return_inlined; eauto. (* unchanged *) @@ -671,7 +671,7 @@ Lemma transf_function_spec: forall f f', transf_function fenv f = OK f' -> tr_function f f'. Proof. intros. unfold transf_function in H. - destruct (expand_function fenv f initstate) as [ctx s i]_eqn. + destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. destruct (zle (st_stksize s) Int.max_unsigned); inv H. monadInv Heqr. set (ctx := initcontext x x0 (max_def_function f) (fn_stacksize f)) in *. Opaque initstate. diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index ce7788f..ac47ae8 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -10,7 +10,6 @@ (* *) (* *********************************************************************) -open BinPos open Coqlib open Datatypes open LTL @@ -33,18 +32,6 @@ let enumerate_aux f reach = (* More clever enumeration that flattens basic blocks *) -let rec int_of_pos = function - | Coq_xI p -> (int_of_pos p lsl 1) + 1 - | Coq_xO p -> int_of_pos p lsl 1 - | Coq_xH -> 1 - -let rec pos_of_int n = - if n = 0 then assert false else - if n = 1 then Coq_xH else - if n land 1 = 0 - then Coq_xO (pos_of_int (n lsr 1)) - else Coq_xI (pos_of_int (n lsr 1)) - module IntSet = Set.Make(struct type t = int let compare = compare end) (* Determine join points: reachable nodes that have > 1 predecessor *) @@ -54,7 +41,7 @@ let join_points f = let reached = ref IntSet.empty in let reached_twice = ref IntSet.empty in let rec traverse pc = - let npc = int_of_pos pc in + let npc = P.to_int pc in if IntSet.mem npc !reached then begin if not (IntSet.mem npc !reached_twice) then reached_twice := IntSet.add npc !reached_twice @@ -74,14 +61,14 @@ let basic_blocks f joins = or a join point or the successor of a conditional test *) let rec start_block pc = - let npc = int_of_pos pc in + let npc = P.to_int pc in if not (IntSet.mem npc !visited) then begin visited := IntSet.add npc !visited; in_block [] max_int pc end (* in_block: add pc to block and check successors *) and in_block blk minpc pc = - let npc = int_of_pos pc in + let npc = P.to_int pc in let blk = pc :: blk in let minpc = min npc minpc in match PTree.get pc f.fn_code with @@ -103,7 +90,7 @@ let basic_blocks f joins = (* next_in_block: check if join point and either extend block or start block *) and next_in_block blk minpc pc = - let npc = int_of_pos pc in + let npc = P.to_int pc in if IntSet.mem npc joins then (end_block blk minpc; start_block pc) else in_block blk minpc pc diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 59178bd..ef6ba1d 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -18,7 +18,6 @@ open Format open Camlcoq open Datatypes -open BinPos open Integers open AST open PrintAST @@ -212,15 +211,15 @@ let rec print_stmt p s = fprintf p "@[{{ %a@;<0 -3>}}@]" print_stmt s | Sexit n -> - fprintf p "exit %d;" (camlint_of_nat n) + fprintf p "exit %d;" (Nat.to_int n) | Sswitch(e, cases, dfl) -> fprintf p "@[switch (%a) {" print_expr e; List.iter (fun (n, x) -> fprintf p "@ case %ld: exit %d;\n" - (camlint_of_coqint n) (camlint_of_nat x)) + (camlint_of_coqint n) (Nat.to_int x)) cases; - fprintf p "@ default: exit %d;\n" (camlint_of_nat dfl); + fprintf p "@ default: exit %d;\n" (Nat.to_int dfl); fprintf p "@;<0 -2>}@]" | Sreturn None -> fprintf p "return;" @@ -247,7 +246,7 @@ let print_function p id f = print_varlist (f.fn_params, true) print_sig f.fn_sig; fprintf p "@[{@ "; - let stksz = camlint_of_z f.fn_stackspace in + let stksz = Z.to_int32 f.fn_stackspace in if stksz <> 0l then fprintf p "stack %ld;@ " stksz; if f.fn_vars <> [] then diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml index 4dc311c..4e8efd1 100644 --- a/backend/PrintLTLin.ml +++ b/backend/PrintLTLin.ml @@ -71,18 +71,18 @@ let print_instruction pp i = fprintf pp "%a = builtin %s(%a)@ " reg res (name_of_external ef) regs args | Llabel lbl -> - fprintf pp "%ld:@ " (camlint_of_positive lbl) + fprintf pp "%ld:@ " (P.to_int32 lbl) | Lgoto lbl -> - fprintf pp "goto %ld@ " (camlint_of_positive lbl) + fprintf pp "goto %ld@ " (P.to_int32 lbl) | Lcond(cond, args, lbl) -> fprintf pp "if (%a) goto %ld@ " (PrintOp.print_condition reg) (cond, args) - (camlint_of_positive lbl) + (P.to_int32 lbl) | Ljumptable(arg, tbl) -> let tbl = Array.of_list tbl in fprintf pp "@[jumptable (%a)" reg arg; for i = 0 to Array.length tbl - 1 do - fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i)) + fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) done; fprintf pp "@]@ " | Lreturn None -> diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index dfbc66e..7e6c343 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -80,18 +80,18 @@ let print_instruction pp i = | Mannot(ef, args) -> fprintf pp "%s(%a)@ " (name_of_external ef) annot_params args | Mlabel lbl -> - fprintf pp "%ld:@ " (camlint_of_positive lbl) + fprintf pp "%ld:@ " (P.to_int32 lbl) | Mgoto lbl -> - fprintf pp "goto %ld@ " (camlint_of_positive lbl) + fprintf pp "goto %ld@ " (P.to_int32 lbl) | Mcond(cond, args, lbl) -> fprintf pp "if (%a) goto %ld@ " (PrintOp.print_condition reg) (cond, args) - (camlint_of_positive lbl) + (P.to_int32 lbl) | Mjumptable(arg, tbl) -> let tbl = Array.of_list tbl in fprintf pp "@[jumptable (%a)" reg arg; for i = 0 to Array.length tbl - 1 do - fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i)) + fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) done; fprintf pp "@]@ " | Mreturn -> diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 4cd3871..0bafcde 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -25,7 +25,7 @@ open PrintOp (* Printing of RTL code *) let reg pp r = - fprintf pp "x%ld" (camlint_of_positive r) + fprintf pp "x%ld" (P.to_int32 r) let rec regs pp = function | [] -> () @@ -37,14 +37,14 @@ let ros pp = function | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) let print_succ pp s dfl = - let s = camlint_of_positive s in + let s = P.to_int32 s in if s <> dfl then fprintf pp " goto %ld@ " s let print_instruction pp (pc, i) = fprintf pp "%5ld: " pc; match i with | Inop s -> - let s = camlint_of_positive s in + let s = P.to_int32 s in if s = Int32.pred pc then fprintf pp "nop@ " else fprintf pp "goto %ld@ " s @@ -77,12 +77,12 @@ let print_instruction pp (pc, i) = | Icond(cond, args, s1, s2) -> fprintf pp "if (%a) goto %ld else goto %ld@ " (PrintOp.print_condition reg) (cond, args) - (camlint_of_positive s1) (camlint_of_positive s2) + (P.to_int32 s1) (P.to_int32 s2) | Ijumptable(arg, tbl) -> let tbl = Array.of_list tbl in fprintf pp "@[jumptable (%a)" reg arg; for i = 0 to Array.length tbl - 1 do - fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i)) + fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) done; fprintf pp "@]@ " | Ireturn None -> @@ -96,7 +96,7 @@ let print_function pp id f = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) (List.map - (fun (pc, i) -> (camlint_of_positive pc, i)) + (fun (pc, i) -> (P.to_int32 pc, i)) (PTree.elements f.fn_code)) in print_succ pp f.fn_entrypoint (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l); diff --git a/backend/RREproof.v b/backend/RREproof.v index 8926fe4..40632f7 100644 --- a/backend/RREproof.v +++ b/backend/RREproof.v @@ -248,7 +248,7 @@ Proof. induction ll; intros; simpl. apply H. simpl. auto. apply IHll. intros. unfold Locmap.set. - destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) as []_eqn. auto. + destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) eqn:?. auto. apply H. simpl. split; auto. apply Loc.diff_sym. apply Loc.non_overlap_diff; auto. Qed. @@ -396,7 +396,7 @@ Opaque destroyed_at_move_regs. simpl in SAFE. assert (SAFE': sm = false \/ ~In r destroyed_at_move_regs /\ safe_move_insertion b = true). destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence. - destruct (is_incoming sl) as []_eqn. + destruct (is_incoming sl) eqn:?. (* incoming, stays as getstack *) assert (UGS: forall rs, undef_getstack sl rs = Locmap.set (R IT1) Vundef rs). destruct sl; simpl in Heqb0; discriminate || auto. @@ -419,11 +419,11 @@ Opaque destroyed_at_move_regs. rewrite <- EQ1; rewrite EQ; rewrite EQ2. rewrite locmap_set_reg_same. apply match_states_regular with sm; auto; tauto. (* found an equation *) - destruct (find_reg_containing sl eqs) as [r'|]_eqn. + destruct (find_reg_containing sl eqs) as [r'|] eqn:?. exploit EQH. eapply find_reg_containing_sound; eauto. simpl; intro EQ. (* turned into a move *) - destruct (safe_move_insertion b) as []_eqn. + destruct (safe_move_insertion b) eqn:?. left; econstructor; split. constructor. simpl; eauto. rewrite UGS. rewrite <- EQ. apply match_states_regular with true; auto. diff --git a/backend/RREtyping.v b/backend/RREtyping.v index 2501c7f..539fb20 100644 --- a/backend/RREtyping.v +++ b/backend/RREtyping.v @@ -91,9 +91,9 @@ Proof. assert (WC: wt_code f c) by (red; auto with coqlib). clear H. inv WI; auto 10 with linearty. - destruct (is_incoming s) as []_eqn. auto with linearty. + destruct (is_incoming s) eqn:?. auto with linearty. destruct (contains_equation s r eqs). auto with linearty. - destruct (find_reg_containing s eqs) as [r'|]_eqn; auto with linearty. + destruct (find_reg_containing s eqs) as [r'|] eqn:?; auto with linearty. assert (mreg_type r' = mreg_type r). exploit H0. eapply find_reg_containing_sound; eauto. simpl. congruence. destruct (safe_move_insertion c); auto 10 with linearty. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 99c89ab..9f5563c 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -289,7 +289,7 @@ Proof. destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. auto 10 with reloadty. - destruct (ef_reloads ef) as [] _eqn. + destruct (ef_reloads ef) as [] eqn:?. assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence. assert (map mreg_type (regs_for args) = map Loc.type args). apply wt_regs_for. apply arity_ok_enough. congruence. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index d086010..4488e49 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -91,7 +91,7 @@ Proof. (* induction *) rewrite PTree.gsspec in H2. unfold renum_node. destruct (peq x k). inv H2. rewrite H3. apply PTree.gss. - destruct f!k as [y'|]_eqn. + destruct f!k as [y'|] eqn:?. rewrite PTree.gso. eauto. red; intros; subst y'. elim n. eapply f_inj; eauto. eauto. Qed. @@ -111,7 +111,7 @@ Proof. intros. destruct (postorder_correct (successors f) f.(fn_entrypoint)) as [A B]. fold (pnum f) in *. - unfold renum_pc. destruct (pnum f)! pc as [pc'|]_eqn. + unfold renum_pc. destruct (pnum f)! pc as [pc'|] eqn:?. simpl. eapply renum_cfg_nodes; eauto. elim (B pc); auto. unfold successors. rewrite PTree.gmap1. rewrite H. simpl. congruence. Qed. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 09dc0ff..0269438 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -166,10 +166,10 @@ Lemma classify_call_correct: end. Proof. unfold classify_call; intros. - destruct (expr_is_addrof_ident a) as [id|]_eqn. + destruct (expr_is_addrof_ident a) as [id|] eqn:?. exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a. inv H. inv H2. - destruct (Genv.find_symbol ge id) as [b|]_eqn. + destruct (Genv.find_symbol ge id) as [b|] eqn:?. rewrite Genv.find_funct_find_funct_ptr in H0. rewrite H0. destruct fd. exists b; auto. @@ -567,7 +567,7 @@ Proof. apply call_cont_commut; eauto. rewrite H. destruct (find_label lbl (sel_stmt ge (Cminor.fn_body f)) (call_cont k'0)) - as [[s'' k'']|]_eqn; intros; try contradiction. + as [[s'' k'']|] eqn:?; intros; try contradiction. destruct H0. left; econstructor; split. econstructor; eauto. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 6c4e43f..b731487 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -2171,7 +2171,7 @@ Proof. exists b; exists tf; split; auto. simpl. generalize (AG m0). rewrite EQ. intro INJ. inv INJ. inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. - destruct (Genv.find_symbol ge i) as [b|]_eqn; try discriminate. + destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. rewrite symbols_preserved. auto. @@ -2398,7 +2398,7 @@ Proof. econstructor; split. apply plus_one. eapply exec_Mgetparam; eauto. rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs. - eapply index_contains_load_stack with (idx := FI_link). eauto. eapply agree_link; eauto. + eapply index_contains_load_stack with (idx := FI_link). eapply TRANSL. eapply agree_link; eauto. simpl parent_sp. change (offset_of_index (make_env (function_bounds f)) (FI_arg z t)) with (offset_of_index (make_env (function_bounds f0)) (FI_arg z t)). -- cgit v1.2.3