diff options
-rw-r--r-- | Makefile | 12 | ||||
-rw-r--r-- | aarch64/Machregs.v | 4 | ||||
-rw-r--r-- | arm/Machregs.v | 4 | ||||
-rw-r--r-- | backend/Selectionproof.v | 2 | ||||
-rw-r--r-- | backend/Unusedglobproof.v | 2 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 2 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 8 | ||||
-rw-r--r-- | cfrontend/SimplExprproof.v | 2 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 2 | ||||
-rw-r--r-- | common/Linking.v | 20 | ||||
-rwxr-xr-x | configure | 14 | ||||
-rw-r--r-- | driver/Compiler.vexpand | 2 | ||||
-rw-r--r-- | flocq/IEEE754/Bits.v | 2 | ||||
-rw-r--r-- | lib/Decidableplus.v | 42 | ||||
-rw-r--r-- | lib/Maps.v | 4 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 4 | ||||
-rw-r--r-- | powerpc/Asmgenproof.v | 6 | ||||
-rw-r--r-- | powerpc/Asmgenproof1.v | 2 | ||||
-rw-r--r-- | powerpc/Machregs.v | 4 | ||||
-rw-r--r-- | powerpc/Op.v | 39 | ||||
-rw-r--r-- | riscV/Machregs.v | 4 | ||||
-rw-r--r-- | x86/Machregs.v | 4 |
22 files changed, 103 insertions, 82 deletions
@@ -61,11 +61,21 @@ endif # deprecated-ident-entry: # warning introduced in 8.13 # suggested change (use `name` instead of `ident`) supported since 8.13 +# deprecated-hint-rewrite-without-locality: +# warning introduced in 8.14 +# suggested change (add Global or Local or [#export] modifier) +# is not supported in 8.13 nor in 8.11, but was supported in 8.9 (go figure) +# deprecated-instance-without-locality: +# warning introduced in 8.14 +# triggered by Menhir-generated files, to be solved upstream in Menhir COQCOPTS ?= \ -w -undeclared-scope \ -w -unused-pattern-matching-variable \ - -w -deprecated-ident-entry + -w -deprecated-ident-entry \ + -w -deprecated-hint-rewrite-without-locality + +cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index bfe23e83..454a7cbe 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -54,9 +54,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/arm/Machregs.v b/arm/Machregs.v index 1ec8f0a1..9fe8548b 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -57,9 +57,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index e737ba4b..fe286627 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1467,7 +1467,7 @@ End PRESERVATION. (** ** Commutation with linking *) -Instance TransfSelectionLink : TransfLink match_prog. +Global Instance TransfSelectionLink : TransfLink match_prog. Proof. red; intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. eapply link_match_program; eauto. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index aaacf9d1..476208b0 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1465,4 +1465,4 @@ Proof. * intros. apply PTree.elements_keys_norepet. Qed. -Instance TransfSelectionLink : TransfLink match_prog := link_match_program. +Global Instance TransfSelectionLink : TransfLink match_prog := link_match_program. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index e373d4e5..d8653544 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1974,7 +1974,7 @@ End CORRECTNESS. (** ** Commutation with linking *) -Instance TransfCshmgenLink : TransfLink match_prog. +Global Instance TransfCshmgenLink : TransfLink match_prog. Proof. red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2). generalize H. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index e3356510..504e8be1 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -1530,7 +1530,7 @@ Unset Implicit Arguments. (** ** Linking types *) -Program Instance Linker_types : Linker type := { +Global Program Instance Linker_types : Linker type := { link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None; linkorder := fun t1 t2 => t1 = t2 }. @@ -1579,7 +1579,7 @@ Proof. assert (x = y) by eauto. subst y. auto. Qed. -Program Instance Linker_composite_defs : Linker (list composite_definition) := { +Global Program Instance Linker_composite_defs : Linker (list composite_definition) := { link := link_composite_defs; linkorder := @List.incl composite_definition }. @@ -1765,7 +1765,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := | linkorder_fundef_ext_int: forall f id sg targs tres cc, linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f). -Program Instance Linker_fundef (F: Type): Linker (fundef F) := { +Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. @@ -1828,7 +1828,7 @@ Definition linkorder_program {F: Type} (p1 p2: program F) : Prop := linkorder (program_of_program p1) (program_of_program p2) /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co). -Program Instance Linker_program (F: Type): Linker (program F) := { +Global Program Instance Linker_program (F: Type): Linker (program F) := { link := link_program; linkorder := linkorder_program }. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 67bf0e51..507e2128 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -2444,7 +2444,7 @@ End PRESERVATION. (** ** Commutation with linking *) -Instance TransfSimplExprLink : TransfLink match_prog. +Global Instance TransfSimplExprLink : TransfLink match_prog. Proof. red; intros. eapply Ctypes.link_match_program_gen; eauto. - intros. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index e4b759c4..c133d8ea 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -2320,7 +2320,7 @@ End PRESERVATION. (** ** Commutation with linking *) -Instance TransfSimplLocalsLink : TransfLink match_prog. +Global Instance TransfSimplLocalsLink : TransfLink match_prog. Proof. red; intros. eapply Ctypes.link_match_program; eauto. - intros. diff --git a/common/Linking.v b/common/Linking.v index d23b1028..4ef83d42 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -60,7 +60,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := | linkorder_fundef_refl: forall fd, linkorder_fundef fd fd | linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f). -Program Instance Linker_fundef (F: Type): Linker (fundef F) := { +Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. @@ -114,7 +114,7 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop := il <> nil -> init_data_list_size il = sz -> linkorder_varinit (Init_space sz :: nil) il. -Program Instance Linker_varinit : Linker (list init_data) := { +Global Program Instance Linker_varinit : Linker (list init_data) := { link := link_varinit; linkorder := linkorder_varinit }. @@ -163,7 +163,7 @@ Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> P linkorder i1 i2 -> linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo). -Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { +Global Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { link := link_vardef; linkorder := linkorder_vardef }. @@ -189,7 +189,7 @@ Global Opaque Linker_vardef. (** A trivial linker for the trivial var info [unit]. *) -Program Instance Linker_unit: Linker unit := { +Global Program Instance Linker_unit: Linker unit := { link := fun x y => Some tt; linkorder := fun x y => True }. @@ -215,7 +215,7 @@ Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V - linkorder v1 v2 -> linkorder_def (Gvar v1) (Gvar v2). -Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { +Global Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { link := link_def; linkorder := linkorder_def }. @@ -332,7 +332,7 @@ Qed. End LINKER_PROG. -Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { +Global Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { link := link_prog; linkorder := fun p1 p2 => p1.(prog_main) = p2.(prog_main) @@ -699,7 +699,7 @@ Local Transparent Linker_fundef. - destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto. Qed. -Instance TransfPartialContextualLink +Global Instance TransfPartialContextualLink {A B C V: Type} {LV: Linker V} (tr_fun: C -> A -> res B) (ctx_for: program (fundef A) V -> C): @@ -714,7 +714,7 @@ Proof. - intros; subst. exists v; auto. Qed. -Instance TransfPartialLink +Global Instance TransfPartialLink {A B V: Type} {LV: Linker V} (tr_fun: A -> res B): TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => @@ -728,7 +728,7 @@ Proof. - intros; subst. exists v; auto. Qed. -Instance TransfTotallContextualLink +Global Instance TransfTotallContextualLink {A B C V: Type} {LV: Linker V} (tr_fun: C -> A -> B) (ctx_for: program (fundef A) V -> C): @@ -747,7 +747,7 @@ Proof. - intros; subst. exists v; auto. Qed. -Instance TransfTotalLink +Global Instance TransfTotalLink {A B V: Type} {LV: Linker V} (tr_fun: A -> B): TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => @@ -352,7 +352,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then cc_options="-m64" casm_options="-m64 -c" clinker_options="-m64" - cprepro_options="-std=c99 -m64 -U__GNUC__ -E" + cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E" system="bsd" ;; linux) @@ -360,7 +360,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then cc_options="-m64" casm_options="-m64 -c" clinker_options="-m64" - cprepro_options="-std=c99 -m64 -U__GNUC__ -E" + cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E" system="linux" ;; macos|macosx) @@ -369,7 +369,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then casm_options="-arch x86_64 -c" clinker_options="-arch x86_64" clinker_needs_no_pie=false - cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E" + cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__SIZEOF_INT128__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E" libmath="" system="macos" ;; @@ -378,7 +378,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then cc_options="-m64" casm_options="-m64 -c" clinker_options="-m64" - cprepro_options="-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E" + cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ '-D__attribute__(x)=' -E" system="cygwin" ;; *) @@ -541,19 +541,19 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2) + 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.2" + echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.0" missingtools=true fi;; "") echo "NOT FOUND" - echo "Error: make sure Coq version 8.12.2 is installed." + echo "Error: make sure Coq version 8.13.2 is installed." missingtools=true;; esac diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 9673267d..7503d3ed 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -163,7 +163,7 @@ Proof. intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence. Qed. -Instance TransfIfLink {A: Type} {LA: Linker A} +Global Instance TransfIfLink {A: Type} {LA: Linker A} (flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf) : TransfLink (match_if flag transf). Proof. diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v index 3c19e31b..b38d4900 100644 --- a/flocq/IEEE754/Bits.v +++ b/flocq/IEEE754/Bits.v @@ -181,7 +181,7 @@ cut (x / (2^mw * 2^ew) < 2)%Z. clear ; lia. apply Zdiv_lt_upper_bound. now apply Zmult_lt_0_compat. rewrite <- Zpower_exp ; try ( apply Z.le_ge ; apply Zlt_le_weak ; assumption ). -change 2%Z at 1 with (Zpower 2 1). +change 2%Z with (Zpower 2 1) at 1. rewrite <- Zpower_exp. now rewrite Zplus_comm. discriminate. diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 69ba4723..224c9640 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -27,14 +27,14 @@ Ltac decide_goal := eapply Decidable_sound; reflexivity. (** Deciding logical connectives *) -Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := { +Global Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := { Decidable_witness := negb (@Decidable_witness P dP) }. Next Obligation. rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt. Qed. -Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := { +Global Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := { Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ) }. Next Obligation. @@ -46,21 +46,21 @@ Next Obligation. eapply Decidable_sound_alt; rewrite H; eapply Decidable_complete_alt; eauto. Qed. -Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := { +Global Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := { Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ }. Next Obligation. rewrite andb_true_iff. rewrite ! Decidable_spec. tauto. Qed. -Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := { +Global Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := { Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ }. Next Obligation. rewrite orb_true_iff. rewrite ! Decidable_spec. tauto. Qed. -Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := { +Global Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := { Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true }. Next Obligation. @@ -79,28 +79,28 @@ Next Obligation. split; intros. InvBooleans. auto. subst y. apply dec_eq_true. Qed. -Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { +Global Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { Decidable_witness := Bool.eqb x y }. Next Obligation. apply eqb_true_iff. Qed. -Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { +Global Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { Decidable_witness := Nat.eqb x y }. Next Obligation. apply Nat.eqb_eq. Qed. -Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := { +Global Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := { Decidable_witness := Pos.eqb x y }. Next Obligation. apply Pos.eqb_eq. Qed. -Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := { +Global Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := { Decidable_witness := Z.eqb x y }. Next Obligation. @@ -109,35 +109,35 @@ Qed. (** Deciding order on Z *) -Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := { +Global Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := { Decidable_witness := Z.leb x y }. Next Obligation. apply Z.leb_le. Qed. -Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := { +Global Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := { Decidable_witness := Z.ltb x y }. Next Obligation. apply Z.ltb_lt. Qed. -Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { +Global Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { Decidable_witness := Z.geb x y }. Next Obligation. rewrite Z.geb_le. intuition lia. Qed. -Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { +Global Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { Decidable_witness := Z.gtb x y }. Next Obligation. rewrite Z.gtb_lt. intuition lia. Qed. -Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { +Global Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { Decidable_witness := Z.eqb y ((y / x) * x)%Z }. Next Obligation. @@ -153,7 +153,7 @@ Qed. (** Deciding properties over lists *) -Program Instance Decidable_forall_in_list : +Global Program Instance Decidable_forall_in_list : forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)), Decidable (forall x:A, In x l -> P x) := { Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l @@ -164,7 +164,7 @@ Next Obligation. - eapply Decidable_complete; eauto. Qed. -Program Instance Decidable_exists_in_list : +Global Program Instance Decidable_exists_in_list : forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)), Decidable (exists x:A, In x l /\ P x) := { Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l @@ -184,7 +184,7 @@ Class Finite (T: Type) := { (** Deciding forall and exists quantification over finite types. *) -Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := { +Global Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := { Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT) }. Next Obligation. @@ -193,7 +193,7 @@ Next Obligation. - eapply Decidable_complete; eauto. Qed. -Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := { +Global Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := { Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT) }. Next Obligation. @@ -204,21 +204,21 @@ Qed. (** Some examples of finite types. *) -Program Instance Finite_bool : Finite bool := { +Global Program Instance Finite_bool : Finite bool := { Finite_elements := false :: true :: nil }. Next Obligation. destruct x; auto. Qed. -Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := { +Global Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := { Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB) }. Next Obligation. apply List.in_prod; eapply Finite_elements_spec. Qed. -Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := { +Global Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := { Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA) }. Next Obligation. @@ -1761,7 +1761,7 @@ Proof. intros. transitivity a0; auto. Qed. -Instance Equal_Equivalence : Equivalence Equal := { +Global Instance Equal_Equivalence : Equivalence Equal := { Equivalence_Reflexive := Equal_refl; Equivalence_Symmetric := Equal_sym; Equivalence_Transitive := Equal_trans @@ -1790,7 +1790,7 @@ Next Obligation. unfold equiv, complement in H0. congruence. Qed. -Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec. +Global Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec. End EXTENSIONAL_EQUALITY. diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 924773e7..eafb6d3c 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -183,7 +183,9 @@ Definition andimm64 (r1 r2: ireg) (n: int64) (k : code) := andimm64_base r1 r2 n k. Definition rolm64 (r1 r2: ireg) (amount: int) (mask: int64) (k: code) := - if is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount) then + if is_rldl_mask mask || is_rldr_mask mask + || (let mask' := Int64.shru' mask amount in + Int64.eq mask (Int64.shl' mask' amount) && is_rldl_mask mask') then Prldinm r1 r2 amount mask :: k else Prldinm r1 r2 amount Int64.mone :: andimm64_base r1 r1 mask k. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index e25ae583..b6b5c678 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -294,10 +294,10 @@ Opaque Int.eq. - unfold xorimm64, opimm64. destruct Int64.eq. TailNoLabel. destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. - unfold rolm64, andimm64_base, opimm64. - destruct (is_rldl_mask i0 || is_rldr_mask i0 || is_rldl_mask (Int64.shru' i0 i)). TailNoLabel. - apply tail_nolabel_cons; unfold nolabel; auto. + destruct orb. + TailNoLabel. destruct Int64.eq. TailNoLabel. - destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. + destruct ireg_eq; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. - eapply transl_cond_op_label; eauto. - destruct (preg_of r); monadInv H. eapply transl_select_op_label; eauto. eapply transl_fselect_op_label; eauto. Qed. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index cc9fc1a7..c0651bf9 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -788,7 +788,7 @@ Lemma rolm64_correct: /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> important_preg r' = true -> rs'#r' = rs#r'. Proof. intros. unfold rolm64. - destruct (is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount)). + destruct orb. - econstructor; split. eapply exec_straight_one. simpl; reflexivity. reflexivity. intuition Simpl. - edestruct (andimm64_base_correct r1 r1 mask k) as (rs2 & A & B & C); auto. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 9967bbae..eeca880a 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -75,9 +75,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/powerpc/Op.v b/powerpc/Op.v index 505b7545..0b379883 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -1367,53 +1367,62 @@ Definition is_rlw_mask (x: int) : bool := is_mask_rec rlw_transition rlw_accepting Int.wordsize RLW_S0 (Int.unsigned x). (** For the 64-bit [rldicl] and [rldicr] instructions, the acceptable - masks are [1111100000] and [0000011111], that is, some ones in the - high bits and some zeroes in the low bits, or conversely. All ones - is OK, but not all zeroes. The corresponding automata are: -<< - 0 1 - / \ / \ - \ / \ / (accepting: [1]) - [0] --1--> [1] + masks are (in big endian): +- for [rldicl]: masks that clear the leftmost bits (most significant bits), + that is, [00000011111], that is, ones in the low bits followed by zeros + in the high bits; +- for [rldicr]: masks that clear the rightmost bits (least significant bits), + that is, [11110000000], that is, zeros in the low bits followed by ones + in the high bits. + All ones is OK, but not all zeroes. + The corresponding automata for [rldicl] is +<< 1 0 / \ / \ \ / \ / (accepting: [1], [2]) [0] --1--> [1] --0--> [2] >> + The automata for [rldicr] is +<< + 0 1 + / \ / \ + \ / \ / (accepting: [1]) + [0] --1--> [1] +>> *) -Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_Sbad. +Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_S2 | RLL_Sbad. Definition rll_transition (s: rll_state) (b: bool) : rll_state := match s, b with - | RLL_S0, false => RLL_S0 | RLL_S0, true => RLL_S1 + | RLL_S1, false => RLL_S2 | RLL_S1, true => RLL_S1 + | RLL_S2, false => RLL_S2 | _, _ => RLL_Sbad end. Definition rll_accepting (s: rll_state) : bool := match s with - | RLL_S1 => true + | RLL_S1 | RLL_S2 => true | _ => false end. -Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_S2 | RLR_Sbad. +Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_Sbad. Definition rlr_transition (s: rlr_state) (b: bool) : rlr_state := match s, b with + | RLR_S0, false => RLR_S0 | RLR_S0, true => RLR_S1 - | RLR_S1, false => RLR_S2 | RLR_S1, true => RLR_S1 - | RLR_S2, false => RLR_S2 | _, _ => RLR_Sbad end. Definition rlr_accepting (s: rlr_state) : bool := match s with - | RLR_S1 | RLR_S2 => true + | RLR_S1 => true | _ => false end. diff --git a/riscV/Machregs.v b/riscV/Machregs.v index d469e594..89fa37b0 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -78,9 +78,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/x86/Machregs.v b/x86/Machregs.v index 6f3064b8..a440bffc 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -57,9 +57,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. |