From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- backend/Asmgenproof0.v | 12 ++++++------ backend/CSEdomain.v | 4 ++-- backend/CminorSel.v | 4 ++-- backend/Cminortyping.v | 12 ++++++------ backend/Deadcodeproof.v | 2 +- backend/NeedDomain.v | 10 +++++----- backend/RTLgenproof.v | 4 ++-- backend/RTLgenspec.v | 48 ++++++++++++++++++++++++------------------------ backend/ValueAnalysis.v | 4 ++-- backend/ValueDomain.v | 20 ++++++++++---------- 10 files changed, 60 insertions(+), 60 deletions(-) (limited to 'backend') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 5e8acd6f..85cee14f 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -31,7 +31,7 @@ Require Import Conventions. (** * Processor registers and register states *) -Hint Extern 2 (_ <> _) => congruence: asmgen. +Global Hint Extern 2 (_ <> _) => congruence: asmgen. Lemma ireg_of_eq: forall r r', ireg_of r = OK r' -> preg_of r = IR r'. @@ -56,7 +56,7 @@ Lemma preg_of_data: Proof. intros. destruct r; reflexivity. Qed. -Hint Resolve preg_of_data: asmgen. +Global Hint Resolve preg_of_data: asmgen. Lemma data_diff: forall r r', @@ -64,7 +64,7 @@ Lemma data_diff: Proof. congruence. Qed. -Hint Resolve data_diff: asmgen. +Global Hint Resolve data_diff: asmgen. Lemma preg_of_not_SP: forall r, preg_of r <> SP. @@ -78,7 +78,7 @@ Proof. intros. apply data_diff; auto with asmgen. Qed. -Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. +Global Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. Lemma nextinstr_pc: forall rs, (nextinstr rs)#PC = Val.offset_ptr rs#PC Ptrofs.one. @@ -746,7 +746,7 @@ Qed. Definition nolabel (i: instruction) := match i with Plabel _ => False | _ => True end. -Hint Extern 1 (nolabel _) => exact I : labels. +Global Hint Extern 1 (nolabel _) => exact I : labels. Lemma tail_nolabel_cons: forall i c k, @@ -757,7 +757,7 @@ Proof. intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction. Qed. -Hint Resolve tail_nolabel_refl: labels. +Global Hint Resolve tail_nolabel_refl: labels. Ltac TailNoLabel := eauto with labels; diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v index 9b1243c8..e96c4cd4 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -92,7 +92,7 @@ Record wf_numbering (n: numbering) : Prop := { In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v }. -Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse. +Global Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse. (** Satisfiability of numberings. A numbering holds in a concrete execution state if there exists a valuation assigning values to @@ -130,7 +130,7 @@ Record numbering_holds (valu: valuation) (ge: genv) (sp: val) n.(num_reg)!r = Some v -> rs#r = valu v }. -Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse. +Global Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse. Lemma empty_numbering_holds: forall valu ge sp rs m, diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 5cbdc249..f6f6e34d 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -464,7 +464,7 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). -Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. +Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. (** * Lifting of let-bound variables *) @@ -580,4 +580,4 @@ Proof. eexact H. apply insert_lenv_0. Qed. -Hint Resolve eval_lift: evalexpr. +Global Hint Resolve eval_lift: evalexpr. diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index 92ec45f2..9f35fe35 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -290,7 +290,7 @@ Lemma expect_incr: forall te e t1 t2 e', Proof. unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto. Qed. -Hint Resolve expect_incr: ty. +Global Hint Resolve expect_incr: ty. Lemma expect_sound: forall e t1 t2 e', expect e t1 t2 = OK e' -> t1 = t2. @@ -305,7 +305,7 @@ Proof. - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty. - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty. Qed. -Hint Resolve type_expr_incr: ty. +Global Hint Resolve type_expr_incr: ty. Lemma type_expr_sound: forall te a t e e', type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t. @@ -325,7 +325,7 @@ Lemma type_exprlist_incr: forall te al tl e e', Proof. induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T; eauto with ty. Qed. -Hint Resolve type_exprlist_incr: ty. +Global Hint Resolve type_exprlist_incr: ty. Lemma type_exprlist_sound: forall te al tl e e', type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl. @@ -342,7 +342,7 @@ Proof. - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty. - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty. Qed. -Hint Resolve type_assign_incr: ty. +Global Hint Resolve type_assign_incr: ty. Lemma type_assign_sound: forall te id a e e', type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id). @@ -362,7 +362,7 @@ Lemma opt_set_incr: forall te optid optty e e', Proof. unfold opt_set; intros. destruct optid, optty; try (monadInv H); eauto with ty. Qed. -Hint Resolve opt_set_incr: ty. +Global Hint Resolve opt_set_incr: ty. Lemma opt_set_sound: forall te optid sg e e', opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' -> @@ -379,7 +379,7 @@ Proof. induction s; simpl; intros e1 e2 T SAT; try (monadInv T); eauto with ty. - destruct tret, o; try (monadInv T); eauto with ty. Qed. -Hint Resolve type_stmt_incr: ty. +Global Hint Resolve type_stmt_incr: ty. Lemma type_stmt_sound: forall te tret s e e', type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 7aa6ff88..7be12c69 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -358,7 +358,7 @@ Proof. intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto. Qed. -Hint Resolve add_need_all_eagree add_need_all_lessdef +Global Hint Resolve add_need_all_eagree add_need_all_lessdef add_need_eagree add_need_vagree add_needs_all_eagree add_needs_all_lessdef add_needs_eagree add_needs_vagree diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index d3c6ed75..fc1ae16d 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -74,7 +74,7 @@ Proof. intros. simpl in H. auto. Qed. -Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na. +Global Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na. Inductive vagree_list: list val -> list val -> list nval -> Prop := | vagree_list_nil: forall nvl, @@ -100,7 +100,7 @@ Proof. destruct nvl; constructor; auto with na. Qed. -Hint Resolve lessdef_vagree_list vagree_lessdef_list: na. +Global Hint Resolve lessdef_vagree_list vagree_lessdef_list: na. (** ** Ordering and least upper bound between value needs *) @@ -116,8 +116,8 @@ Proof. destruct x; constructor; auto. Qed. -Hint Constructors nge: na. -Hint Resolve nge_refl: na. +Global Hint Constructors nge: na. +Global Hint Resolve nge_refl: na. Lemma nge_trans: forall x y, nge x y -> forall z, nge y z -> nge x z. Proof. @@ -1084,7 +1084,7 @@ Proof. intros. apply H. Qed. -Hint Resolve nreg_agree: na. +Global Hint Resolve nreg_agree: na. Lemma eagree_ge: forall e1 e2 ne ne', diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 88f7fe53..1602823f 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -165,7 +165,7 @@ Proof. subst r0; contradiction. apply Regmap.gso; auto. Qed. -Hint Resolve match_env_update_temp: rtlg. +Global Hint Resolve match_env_update_temp: rtlg. (** Matching between environments is preserved by simultaneous assignment to a Cminor local variable (in the Cminor environments) @@ -205,7 +205,7 @@ Proof. eapply match_env_update_temp; eauto. eapply match_env_update_var; eauto. Qed. -Hint Resolve match_env_update_dest: rtlg. +Global Hint Resolve match_env_update_dest: rtlg. (** A variant of [match_env_update_var] corresponding to the assignment of the result of a builtin. *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 72693f63..25f9954c 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -128,7 +128,7 @@ Ltac monadInv H := (** * Monotonicity properties of the state *) -Hint Resolve state_incr_refl: rtlg. +Global Hint Resolve state_incr_refl: rtlg. Lemma instr_at_incr: forall s1 s2 n i, @@ -137,7 +137,7 @@ Proof. intros. inv H. destruct (H3 n); congruence. Qed. -Hint Resolve instr_at_incr: rtlg. +Global Hint Resolve instr_at_incr: rtlg. (** The following tactic saturates the hypotheses with [state_incr] properties that follow by transitivity from @@ -174,14 +174,14 @@ Lemma valid_fresh_absurd: Proof. intros r s. unfold reg_valid, reg_fresh; case r; tauto. Qed. -Hint Resolve valid_fresh_absurd: rtlg. +Global Hint Resolve valid_fresh_absurd: rtlg. Lemma valid_fresh_different: forall r1 r2 s, reg_valid r1 s -> reg_fresh r2 s -> r1 <> r2. Proof. unfold not; intros. subst r2. eauto with rtlg. Qed. -Hint Resolve valid_fresh_different: rtlg. +Global Hint Resolve valid_fresh_different: rtlg. Lemma reg_valid_incr: forall r s1 s2, state_incr s1 s2 -> reg_valid r s1 -> reg_valid r s2. @@ -190,7 +190,7 @@ Proof. inversion INCR. unfold reg_valid. intros; apply Plt_Ple_trans with (st_nextreg s1); auto. Qed. -Hint Resolve reg_valid_incr: rtlg. +Global Hint Resolve reg_valid_incr: rtlg. Lemma reg_fresh_decr: forall r s1 s2, state_incr s1 s2 -> reg_fresh r s2 -> reg_fresh r s1. @@ -199,7 +199,7 @@ Proof. unfold reg_fresh; unfold not; intros. apply H4. apply Plt_Ple_trans with (st_nextreg s1); auto. Qed. -Hint Resolve reg_fresh_decr: rtlg. +Global Hint Resolve reg_fresh_decr: rtlg. (** Validity of a list of registers. *) @@ -211,7 +211,7 @@ Lemma regs_valid_nil: Proof. intros; red; intros. elim H. Qed. -Hint Resolve regs_valid_nil: rtlg. +Global Hint Resolve regs_valid_nil: rtlg. Lemma regs_valid_cons: forall r1 rl s, @@ -232,7 +232,7 @@ Lemma regs_valid_incr: Proof. unfold regs_valid; intros; eauto with rtlg. Qed. -Hint Resolve regs_valid_incr: rtlg. +Global Hint Resolve regs_valid_incr: rtlg. (** A register is ``in'' a mapping if it is associated with a Cminor local or let-bound variable. *) @@ -253,7 +253,7 @@ Lemma map_valid_incr: Proof. unfold map_valid; intros; eauto with rtlg. Qed. -Hint Resolve map_valid_incr: rtlg. +Global Hint Resolve map_valid_incr: rtlg. (** * Properties of basic operations over the state *) @@ -265,7 +265,7 @@ Lemma add_instr_at: Proof. intros. monadInv H. simpl. apply PTree.gss. Qed. -Hint Resolve add_instr_at: rtlg. +Global Hint Resolve add_instr_at: rtlg. (** Properties of [update_instr]. *) @@ -278,7 +278,7 @@ Proof. destruct (check_empty_node s1 n); try discriminate. inv H. simpl. apply PTree.gss. Qed. -Hint Resolve update_instr_at: rtlg. +Global Hint Resolve update_instr_at: rtlg. (** Properties of [new_reg]. *) @@ -289,7 +289,7 @@ Proof. intros. monadInv H. unfold reg_valid; simpl. apply Plt_succ. Qed. -Hint Resolve new_reg_valid: rtlg. +Global Hint Resolve new_reg_valid: rtlg. Lemma new_reg_fresh: forall s1 s2 r i, @@ -299,7 +299,7 @@ Proof. unfold reg_fresh; simpl. exact (Plt_strict _). Qed. -Hint Resolve new_reg_fresh: rtlg. +Global Hint Resolve new_reg_fresh: rtlg. Lemma new_reg_not_in_map: forall s1 s2 m r i, @@ -307,7 +307,7 @@ Lemma new_reg_not_in_map: Proof. unfold not; intros; eauto with rtlg. Qed. -Hint Resolve new_reg_not_in_map: rtlg. +Global Hint Resolve new_reg_not_in_map: rtlg. (** * Properties of operations over compilation environments *) @@ -330,7 +330,7 @@ Proof. intros. inv H0. left; exists name; auto. intros. inv H0. Qed. -Hint Resolve find_var_in_map: rtlg. +Global Hint Resolve find_var_in_map: rtlg. Lemma find_var_valid: forall s1 s2 map name r i, @@ -338,7 +338,7 @@ Lemma find_var_valid: Proof. eauto with rtlg. Qed. -Hint Resolve find_var_valid: rtlg. +Global Hint Resolve find_var_valid: rtlg. (** Properties of [find_letvar]. *) @@ -350,7 +350,7 @@ Proof. caseEq (nth_error (map_letvars map) idx); intros; monadInv H0. right; apply nth_error_in with idx; auto. Qed. -Hint Resolve find_letvar_in_map: rtlg. +Global Hint Resolve find_letvar_in_map: rtlg. Lemma find_letvar_valid: forall s1 s2 map idx r i, @@ -358,7 +358,7 @@ Lemma find_letvar_valid: Proof. eauto with rtlg. Qed. -Hint Resolve find_letvar_valid: rtlg. +Global Hint Resolve find_letvar_valid: rtlg. (** Properties of [add_var]. *) @@ -445,7 +445,7 @@ Proof. intros until r. unfold alloc_reg. case a; eauto with rtlg. Qed. -Hint Resolve alloc_reg_valid: rtlg. +Global Hint Resolve alloc_reg_valid: rtlg. Lemma alloc_reg_fresh_or_in_map: forall map a s r s' i, @@ -469,7 +469,7 @@ Proof. apply regs_valid_nil. apply regs_valid_cons. eauto with rtlg. eauto with rtlg. Qed. -Hint Resolve alloc_regs_valid: rtlg. +Global Hint Resolve alloc_regs_valid: rtlg. Lemma alloc_regs_fresh_or_in_map: forall map al s rl s' i, @@ -494,7 +494,7 @@ Proof. intros until r. unfold alloc_reg. case dest; eauto with rtlg. Qed. -Hint Resolve alloc_optreg_valid: rtlg. +Global Hint Resolve alloc_optreg_valid: rtlg. Lemma alloc_optreg_fresh_or_in_map: forall map dest s r s' i, @@ -609,7 +609,7 @@ Proof. apply regs_valid_cons; eauto with rtlg. Qed. -Hint Resolve new_reg_target_ok alloc_reg_target_ok +Global Hint Resolve new_reg_target_ok alloc_reg_target_ok alloc_regs_target_ok: rtlg. (** The following predicate is a variant of [target_reg_ok] used @@ -631,7 +631,7 @@ Lemma return_reg_ok_incr: Proof. induction 1; intros; econstructor; eauto with rtlg. Qed. -Hint Resolve return_reg_ok_incr: rtlg. +Global Hint Resolve return_reg_ok_incr: rtlg. Lemma new_reg_return_ok: forall s1 r s2 map sig i, @@ -676,7 +676,7 @@ Inductive reg_map_ok: mapping -> reg -> option ident -> Prop := map.(map_vars)!id = Some rd -> reg_map_ok map rd (Some id). -Hint Resolve reg_map_ok_novar: rtlg. +Global Hint Resolve reg_map_ok_novar: rtlg. (** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index f7e4f0ed..ebf2c5ea 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -342,7 +342,7 @@ Proof. induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto. Qed. -Hint Resolve areg_sound aregs_sound: va. +Global Hint Resolve areg_sound aregs_sound: va. Lemma abuiltin_arg_sound: forall bc ge rs sp m ae rm am, @@ -1912,7 +1912,7 @@ Proof. - exact NOSTACK. Qed. -Hint Resolve areg_sound aregs_sound: va. +Global Hint Resolve areg_sound aregs_sound: va. (** * Interface with other optimizations *) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 45894bfc..01f080ff 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -43,12 +43,12 @@ Proof. elim H. apply H0; auto. Qed. -Hint Extern 2 (_ = _) => congruence : va. -Hint Extern 2 (_ <> _) => congruence : va. -Hint Extern 2 (_ < _) => extlia : va. -Hint Extern 2 (_ <= _) => extlia : va. -Hint Extern 2 (_ > _) => extlia : va. -Hint Extern 2 (_ >= _) => extlia : va. +Global Hint Extern 2 (_ = _) => congruence : va. +Global Hint Extern 2 (_ <> _) => congruence : va. +Global Hint Extern 2 (_ < _) => extlia : va. +Global Hint Extern 2 (_ <= _) => extlia : va. +Global Hint Extern 2 (_ > _) => extlia : va. +Global Hint Extern 2 (_ >= _) => extlia : va. Section MATCH. @@ -4711,10 +4711,10 @@ Module VA <: SEMILATTICE. End VA. -Hint Constructors cmatch : va. -Hint Constructors pmatch: va. -Hint Constructors vmatch: va. -Hint Resolve cnot_sound symbol_address_sound +Global Hint Constructors cmatch : va. +Global Hint Constructors pmatch: va. +Global Hint Constructors vmatch: va. +Global Hint Resolve cnot_sound symbol_address_sound shl_sound shru_sound shr_sound and_sound or_sound xor_sound notint_sound ror_sound rolm_sound -- cgit