diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-13 13:07:24 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-13 13:07:24 +0100 |
commit | 41c895850f75e3084fc8efdb7c9b1f7c8ec4fa5d (patch) | |
tree | 3126fa4af7ba97dbc4f4f841a81820c95a2e35a3 | |
parent | 8f972659841ad38f6f548161b5ca3cfcbdd135cb (diff) | |
parent | 72ba1c282e2a8bfd0e826352a251fa71bfb71e05 (diff) | |
download | compcert-kvx-41c895850f75e3084fc8efdb7c9b1f7c8ec4fa5d.tar.gz compcert-kvx-41c895850f75e3084fc8efdb7c9b1f7c8ec4fa5d.zip |
Merge branch 'master' into mppa_postpass
Conflicts:
.gitignore
runtime/include/stdbool.h
-rw-r--r-- | .gitignore | 2 | ||||
-rw-r--r-- | Changelog | 35 | ||||
-rw-r--r-- | Makefile | 7 | ||||
-rw-r--r-- | VERSION | 2 | ||||
-rw-r--r-- | backend/SelectDivproof.v | 14 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 5 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 56 | ||||
-rw-r--r-- | common/Linking.v | 94 | ||||
-rwxr-xr-x | configure | 11 | ||||
-rw-r--r-- | cparser/Checks.ml | 9 | ||||
-rw-r--r-- | cparser/Cutil.ml | 38 | ||||
-rw-r--r-- | cparser/Cutil.mli | 9 | ||||
-rw-r--r-- | cparser/Elab.ml | 51 | ||||
-rw-r--r-- | cparser/PackedStructs.ml | 8 | ||||
-rw-r--r-- | doc/index.html | 12 | ||||
-rw-r--r-- | lib/Floats.v | 29 | ||||
-rw-r--r-- | lib/Integers.v | 16 | ||||
-rw-r--r-- | powerpc/Asm.v | 4 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 52 | ||||
-rw-r--r-- | powerpc/Asmgenproof1.v | 11 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 9 | ||||
-rw-r--r-- | runtime/include/stdbool.h | 1 | ||||
-rw-r--r-- | runtime/include/stddef.h | 2 | ||||
-rw-r--r-- | test/regression/Makefile | 2 | ||||
-rw-r--r-- | test/regression/Results/aligned | 12 | ||||
-rw-r--r-- | test/regression/aligned.c | 115 | ||||
-rw-r--r-- | test/regression/varargs3.c | 52 | ||||
-rw-r--r-- | x86/Asm.v | 12 | ||||
-rw-r--r-- | x86/Asmgenproof1.v | 184 |
29 files changed, 564 insertions, 290 deletions
@@ -78,3 +78,5 @@ runtime/mppa_k1c/i64_udivmod.s runtime/mppa_k1c/i64_umod.s # Test generated data /test/clightgen/*.v +# Coq cache +.lia.cache @@ -1,3 +1,38 @@ +Release 3.5, 2019-02-27 +======================= + +Bug fixing: +- Modeling error in PowerPC ISA: how register 0 is interpreted when + used as base register for indexed load/stores. The code generated + by CompCert was correct, but was proved correct against the wrong + specification. +- Modeling error in x86 ISA: how flag ZF is set by floating-point + comparisons. Here as well, the code generated by CompCert was + correct, but was proved correct against the wrong specification. +- Revised handling of attributes so that they behave more like in + GCC and Clang. CompCert now distinguishes between attributes that + attach to names (variables, fields, typedefs, structs and unions) + and attributes that attach to objects (variables). In particular, + the `aligned(N)` attribute now attaches to names, while the `_Alignas(N)` + modifier still attaches to objects. This fixes issue 256. +- Issue with NULL as argument to a variadic function on 64-bit platforms + (issue 265) +- Macro __bool_true_false_are_defined was missing from <stdbool.h> (issue 266) + +Coq development: +- Can now be entirely rechecked using coqchk + (contributed by Vincent Laporte) +- Support Coq version 8.9.0 +- Avoid using "refine mode" when defining Instance + (contributed by Maxime Dénès) +- Do not support Menhir versions more recent than 20181113, because + they will introduce an incompatibility with this CompCert release. + +New feature: +- PowerPC port: add __builtin_isel (conditional move) at types int64, uint64, + and _Bool. + + Release 3.4, 2018-09-17 ======================= @@ -272,6 +272,7 @@ clean: rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o rm -f $(GENERATED) .depend + rm -f .lia.cache $(MAKE) -f Makefile.extr clean $(MAKE) -C runtime clean $(MAKE) -C test clean @@ -283,12 +284,8 @@ distclean: check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." -# Problems with coqchk (coq 8.6): -# Integers.Int.Z_mod_modulus_range takes forever to check -# compcert.backend.SelectDivproof.divs_mul_shift_2 takes forever to check - check-proof: $(FILES) - $(COQCHK) -admit compcert.lib.Integers -admit compcert.backend.SelectDivproof compcert.driver.Complements + $(COQCHK) compcert.driver.Complements print-includes: @echo $(COQINCLUDES) @@ -1,3 +1,3 @@ -version=3.4 +version=3.5 buildnr= tag= diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index b10deb5c..3fd50b76 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -283,14 +283,15 @@ Proof. intros (A & B & C). split. auto. rewrite C. f_equal. f_equal. rewrite Int.add_signed. unfold Int.mulhs. set (n := Int.signed x). transitivity (Int.repr (n * (m - Int.modulus) / Int.modulus + n)). - f_equal. + apply f_equal. replace (n * (m - Int.modulus)) with (n * m + (-n) * Int.modulus) by ring. rewrite Z_div_plus. ring. apply Int.modulus_pos. apply Int.eqm_samerepr. apply Int.eqm_add; auto with ints. apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned. - apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. f_equal. f_equal. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. + apply (f_equal (fun x => n * x / Int.modulus)). rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption. - apply zlt_false. omega. + apply zlt_false. assumption. Qed. Theorem divu_mul_shift: @@ -436,14 +437,15 @@ Proof. intros (A & B & C). split. auto. rewrite C. f_equal. f_equal. rewrite Int64.add_signed. unfold Int64.mulhs. set (n := Int64.signed x). transitivity (Int64.repr (n * (m - Int64.modulus) / Int64.modulus + n)). - f_equal. + apply f_equal. replace (n * (m - Int64.modulus)) with (n * m + (-n) * Int64.modulus) by ring. rewrite Z_div_plus. ring. apply Int64.modulus_pos. apply Int64.eqm_samerepr. apply Int64.eqm_add; auto with ints. apply Int64.eqm_sym. eapply Int64.eqm_trans. apply Int64.eqm_signed_unsigned. - apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2. f_equal. f_equal. + apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2. + apply (f_equal (fun x => n * x / Int64.modulus)). rewrite Int64.signed_repr_eq. rewrite Zmod_small by assumption. - apply zlt_false. omega. + apply zlt_false. assumption. Qed. Remark int64_shru'_div_two_p: diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d6bf76f3..d70c4dad 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -315,8 +315,9 @@ let attributes = [ ("noinline",Cutil.Attr_function); (* name-related *) ("aligned", Cutil.Attr_name); - ("section", Cutil.Attr_name); - ("unused", Cutil.Attr_name) + (* object-related *) + ("section", Cutil.Attr_object); + ("unused", Cutil.Attr_object) ] diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 036b768b..bfc5daa9 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -1173,14 +1173,12 @@ Unset Implicit Arguments. (** ** Linking types *) -Instance Linker_types : Linker type := { +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 }. -Proof. - auto. - intros; congruence. - intros. destruct (type_eq x y); inv H. auto. +Next Obligation. + destruct (type_eq x y); inv H. auto. Defined. Global Opaque Linker_types. @@ -1224,14 +1222,18 @@ Proof. assert (x = y) by eauto. subst y. auto. Qed. -Instance Linker_composite_defs : Linker (list composite_definition) := { +Program Instance Linker_composite_defs : Linker (list composite_definition) := { link := link_composite_defs; linkorder := @List.incl composite_definition }. -Proof. -- intros; apply incl_refl. -- intros; red; intros; eauto. -- intros. apply link_composite_def_inv in H; destruct H as (A & B & C). +Next Obligation. + apply incl_refl. +Defined. +Next Obligation. + red; intros; eauto. +Defined. +Next Obligation. + apply link_composite_def_inv in H; destruct H as (A & B & C). split; red; intros; apply C; auto. Defined. @@ -1406,18 +1408,22 @@ 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). -Instance Linker_fundef (F: Type): Linker (fundef F) := { +Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. -Proof. -- intros; constructor. -- intros. inv H; inv H0; constructor. -- intros x y z EQ. destruct x, y; simpl in EQ. +Next Obligation. + constructor. +Defined. +Next Obligation. + inv H; inv H0; constructor. +Defined. +Next Obligation. + destruct x, y; simpl in H. + discriminate. -+ destruct e; inv EQ. split; constructor. -+ destruct e; inv EQ. split; constructor. -+ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv EQ. ++ destruct e; inv H. split; constructor. ++ destruct e; inv H. split; constructor. ++ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv H. InvBooleans. subst. split; constructor. Defined. @@ -1465,15 +1471,19 @@ 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). -Instance Linker_program (F: Type): Linker (program F) := { +Program Instance Linker_program (F: Type): Linker (program F) := { link := link_program; linkorder := linkorder_program }. -Proof. -- intros; split. apply linkorder_refl. auto. -- intros. destruct H, H0. split. eapply linkorder_trans; eauto. +Next Obligation. + split. apply linkorder_refl. auto. +Defined. +Next Obligation. + destruct H, H0. split. eapply linkorder_trans; eauto. intros; auto. -- intros until z. unfold link_program. +Defined. +Next Obligation. + revert H. unfold link_program. destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate. destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate. destruct (link_build_composite_env (prog_types x) (prog_types y) typs diff --git a/common/Linking.v b/common/Linking.v index eaa95462..ec828ea4 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -59,18 +59,22 @@ 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). -Instance Linker_fundef (F: Type): Linker (fundef F) := { +Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. -Proof. -- intros; constructor. -- intros. inv H; inv H0; constructor. -- intros x y z EQ. destruct x, y; simpl in EQ. +Next Obligation. + constructor. +Defined. +Next Obligation. + inv H; inv H0; constructor. +Defined. +Next Obligation. + destruct x, y; simpl in H. + discriminate. -+ destruct e; inv EQ. split; constructor. -+ destruct e; inv EQ. split; constructor. -+ destruct (external_function_eq e e0); inv EQ. split; constructor. ++ destruct e; inv H. split; constructor. ++ destruct e; inv H. split; constructor. ++ destruct (external_function_eq e e0); inv H. split; constructor. Defined. Global Opaque Linker_fundef. @@ -109,16 +113,20 @@ 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. -Instance Linker_varinit : Linker (list init_data) := { +Program Instance Linker_varinit : Linker (list init_data) := { link := link_varinit; linkorder := linkorder_varinit }. -Proof. -- intros. constructor. -- intros. inv H; inv H0; constructor; auto. +Next Obligation. + constructor. +Defined. +Next Obligation. + inv H; inv H0; constructor; auto. congruence. simpl. generalize (init_data_list_size_pos z). xomega. -- unfold link_varinit; intros until z. +Defined. +Next Obligation. + revert H; unfold link_varinit. destruct (classify_init x) eqn:Cx, (classify_init y) eqn:Cy; intros E; inv E; try (split; constructor; fail). + destruct (zeq sz (Z.max sz0 0 + 0)); inv H0. split; constructor. congruence. auto. @@ -154,14 +162,18 @@ 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). -Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { +Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { link := link_vardef; linkorder := linkorder_vardef }. -Proof. -- intros. destruct x; constructor; apply linkorder_refl. -- intros. inv H; inv H0. constructor; eapply linkorder_trans; eauto. -- unfold link_vardef; intros until z. +Next Obligation. + destruct x; constructor; apply linkorder_refl. +Defined. +Next Obligation. + inv H; inv H0. constructor; eapply linkorder_trans; eauto. +Defined. +Next Obligation. + revert H; unfold link_vardef. destruct x as [f1 i1 r1 v1], y as [f2 i2 r2 v2]; simpl. destruct (link f1 f2) as [f|] eqn:LF; try discriminate. destruct (link i1 i2) as [i|] eqn:LI; try discriminate. @@ -176,15 +188,10 @@ Global Opaque Linker_vardef. (** A trivial linker for the trivial var info [unit]. *) -Instance Linker_unit: Linker unit := { +Program Instance Linker_unit: Linker unit := { link := fun x y => Some tt; linkorder := fun x y => True }. -Proof. -- auto. -- auto. -- auto. -Defined. Global Opaque Linker_unit. @@ -207,18 +214,22 @@ Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V - linkorder v1 v2 -> linkorder_def (Gvar v1) (Gvar v2). -Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { +Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { link := link_def; linkorder := linkorder_def }. -Proof. -- intros. destruct x; constructor; apply linkorder_refl. -- intros. inv H; inv H0; constructor; eapply linkorder_trans; eauto. -- unfold link_def; intros. +Next Obligation. + destruct x; constructor; apply linkorder_refl. +Defined. +Next Obligation. + inv H; inv H0; constructor; eapply linkorder_trans; eauto. +Defined. +Next Obligation. + unfold link_def; intros. destruct x as [f1|v1], y as [f2|v2]; try discriminate. -+ destruct (link f1 f2) as [f|] eqn:L; inv H. apply link_linkorder in L. - split; constructor; tauto. -+ destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L. ++ simpl in H. destruct (link f1 f2) as [f|] eqn:L. inv H. apply link_linkorder in L. + split; constructor; tauto. discriminate. ++ simpl in H; destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L. split; constructor; tauto. Defined. @@ -320,7 +331,7 @@ Qed. End LINKER_PROG. -Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { +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) @@ -332,18 +343,19 @@ Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program /\ linkorder gd1 gd2 /\ (~In id p2.(prog_public) -> gd2 = gd1) }. -Proof. -- intros; split; auto. split. apply incl_refl. intros. +Next Obligation. + split; auto. split. apply incl_refl. intros. exists gd1; split; auto. split; auto. apply linkorder_refl. - -- intros x y z (A1 & B1 & C1) (A2 & B2 & C2). +Defined. +Next Obligation. split. congruence. split. red; eauto. - intros. exploit C1; eauto. intros (gd2 & P & Q & R). - exploit C2; eauto. intros (gd3 & U & X & Y). + intros. exploit H4; eauto. intros (gd2 & P & Q & R). + exploit H2; eauto. intros (gd3 & U & X & Y). exists gd3. split; auto. split. eapply linkorder_trans; eauto. intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto. - -- intros. apply link_prog_inv in H. destruct H as (L1 & L2 & L3). +Defined. +Next Obligation. + apply link_prog_inv in H. destruct H as (L1 & L2 & L3). subst z; simpl. intuition auto. + red; intros; apply in_app_iff; auto. + rewrite prog_defmap_elements, PTree.gcombine, H by auto. @@ -528,19 +528,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.6.1|8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2) + 8.6.1|8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.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 one of the following Coq versions: 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0, 8.6.1" + echo "Error: CompCert requires one of the following Coq versions: 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0, 8.6.1" missingtools=true fi;; "") echo "NOT FOUND" - echo "Error: make sure Coq version 8.8.1 is installed." + echo "Error: make sure Coq version 8.9.0 is installed." missingtools=true;; esac @@ -580,12 +580,13 @@ fi MENHIR_REQUIRED=20161201 MENHIR_NEW_API=20180530 +MENHIR_MAX=20181113 menhir_flags='' echo "Testing Menhir... " | tr -d '\n' menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) - if test "$menhir_ver" -ge $MENHIR_REQUIRED; then + if test "$menhir_ver" -ge $MENHIR_REQUIRED -a "$menhir_ver" -le $MENHIR_MAX; then echo "version $menhir_ver -- good!" menhir_includes="-I `menhir --suggest-menhirLib`" if test "$menhir_ver" -ge $MENHIR_NEW_API; then @@ -593,7 +594,7 @@ case "$menhir_ver" in fi else echo "version $menhir_ver -- UNSUPPORTED" - echo "Error: CompCert requires Menhir version $MENHIR_REQUIRED or later." + echo "Error: CompCert requires a version of Menhir between $MENHIR_REQUIRED and $MENHIR_MAX, included." missingtools=true fi;; *) diff --git a/cparser/Checks.ml b/cparser/Checks.ml index 62d85c1b..a30cde7d 100644 --- a/cparser/Checks.ml +++ b/cparser/Checks.ml @@ -18,19 +18,12 @@ open Diagnostics open Cutil open Env -let attribute_string = function - | AConst -> "const" - | AVolatile -> "volatile" - | ARestrict -> "restrict" - | AAlignas n -> "_Alignas" - | Attr(name, _) -> name - let unknown_attrs loc attrs = let unknown attr = let attr_class = class_of_attribute attr in if attr_class = Attr_unknown then warning loc Unknown_attribute - "unknown attribute '%s' ignored" (attribute_string attr) in + "unknown attribute '%s' ignored" (name_of_attribute attr) in List.iter unknown attrs let unknown_attrs_typ env loc ty = diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index ea9713d5..cf67015a 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -95,7 +95,10 @@ let rec remove_custom_attributes (names: string list) (al: attributes) = (* Classification of attributes *) type attribute_class = - | Attr_name (* Attribute applies to the names being declared *) + | Attr_object (* Attribute applies to the object being declared + (function, global variable, local variable) *) + | Attr_name (* Attribute applies to the name being declared + (object, struct/union member, struct/union/enum tag *) | Attr_type (* Attribute applies to types *) | Attr_struct (* Attribute applies to struct, union and enum *) | Attr_function (* Attribute applies to function types and decls *) @@ -111,11 +114,20 @@ let declare_attributes l = let class_of_attribute = function | AConst | AVolatile | ARestrict -> Attr_type - | AAlignas _ -> Attr_name + | AAlignas _ -> Attr_object | Attr(name, args) -> try Hashtbl.find attr_class (normalize_attrname name) with Not_found -> Attr_unknown +(* Name for printing an attribute *) + +let name_of_attribute = function + | AConst -> "const" + | AVolatile -> "volatile" + | ARestrict -> "restrict" + | AAlignas n -> "_Alignas" + | Attr(name, _) -> name + (* Is an attribute a ISO C standard attribute? *) let attr_is_standard = function @@ -163,7 +175,10 @@ let rec unroll env t = unroll env (add_attributes_type attr ty) | _ -> t -(* Extracting the attributes of a type *) +(* Extracting the attributes of a type, including the attributes + attached to typedefs, structs and unions. In other words, + typedefs are unrolled and composite definitions expanded + before extracting the attributes. *) let rec attributes_of_type env t = match t with @@ -190,6 +205,23 @@ let rec attributes_of_type env t = | exception Env.Error(Env.Unbound_tag _) -> a end +(* Extracting the attributes of a type, excluding the attributes + attached to typedefs, structs and unions. In other words, + typedefs are not unrolled and composite definitions are not expanded. *) + +let rec attributes_of_type_no_expand t = + match t with + | TVoid a -> a + | TInt(ik, a) -> a + | TFloat(fk, a) -> a + | TPtr(ty, a) -> a + | TArray(ty, sz, a) -> add_attributes a (attributes_of_type_no_expand ty) + | TFun(ty, params, vararg, a) -> a + | TNamed(s, a) -> a + | TStruct(s, a) -> a + | TUnion(s, a) -> a + | TEnum(s, a) -> a + (* Changing the attributes of a type (at top-level) *) (* Same hack as above for array types. *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index dc9dc0cc..5a1e9af3 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -50,6 +50,8 @@ val remove_custom_attributes : string list -> attributes -> attributes in the given list of names. *) val attributes_of_type : Env.t -> typ -> attributes (* Return the attributes of the given type, expanding typedefs if needed. *) +val attributes_of_type_no_expand : typ -> attributes + (* Return the attributes of the given type, without expanding typedefs. *) val add_attributes_type : attributes -> typ -> typ (* Add the given set of attributes to those of the given type. *) val remove_attributes_type : Env.t -> attributes -> typ -> typ @@ -62,7 +64,10 @@ val has_std_alignas : Env.t -> typ -> bool (* Do the attributes of the type contain the C11 _Alignas attribute *) type attribute_class = - | Attr_name (* Attribute applies to the names being declared *) + | Attr_object (* Attribute applies to the object being declared + (function, global variable, local variable) *) + | Attr_name (* Attribute applies to the name being declared + (object, struct/union member, struct/union/enum tag *) | Attr_type (* Attribute applies to types *) | Attr_struct (* Attribute applies to struct, union and enum *) | Attr_function (* Attribute applies to function types and decls *) @@ -76,6 +81,8 @@ val class_of_attribute: attribute -> attribute_class have class [Attr_type]. Custom attributes have the class that was given to them using [declare_attribute], or [Attr_unknown] if not declared. *) +val name_of_attribute: attribute -> string + (* Name for printing an attribute *) val attr_inherited_by_members: attribute -> bool (* Is an attribute of a composite inherited by members of the composite? *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 718261b4..7a0b05de 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -535,8 +535,11 @@ let elab_attribute env = function (List.flatten (List.map (elab_gcc_attr loc env) l))) | PACKED_ATTR (args, loc) -> - enter_gcc_attr loc + begin try + enter_gcc_attr loc (Attr("__packed__", List.map (elab_attr_arg loc env) args)) + with Wrong_attr_arg -> error loc "ill-formed 'packed' attribute"; [] + end | ALIGNAS_ATTR ([a], loc) -> warning loc Celeven_extension "'_Alignas' is a C11 extension"; begin match elab_attr_arg loc env a with @@ -595,7 +598,7 @@ let get_nontype_attrs env ty = | Attr_type -> false | Attr_function -> not (is_function_type env ty) | _ -> true in - let nta = List.filter to_be_removed (attributes_of_type env ty) in + let nta = List.filter to_be_removed (attributes_of_type_no_expand ty) in (remove_attributes_type env nta ty, nta) (* Elaboration of a type specifier. Returns 6-tuple: @@ -653,15 +656,31 @@ let rec elab_specifier ?(only = false) loc env specifier = restrict_check ty; (!sto, !inline, !noreturn ,!typedef, add_attributes_type !attr ty, env) in - (* As done in CIL, partition !attr into struct-related attributes, + (* Partition !attr into name- and struct-related attributes, which are returned, and other attributes, which are left in !attr. - The returned struct-related attributes are applied to the + The returned name-or-struct-related attributes are applied to the struct/union/enum being defined. - The leftover non-struct-related attributes will be applied - to the variable being defined. *) - let get_struct_attrs () = + The leftover attributes (e.g. object attributes) will be applied + to the variable being defined. + If [optmembers] is [None], name-related attributes are not returned + but left in !attr. This corresponds to two use cases: + - A use of an already-defined struct/union/enum. In this case + the name-related attributes should go to the name being declared. + Sending them to the struct/union/enum would cause them to be ignored, + with a warning. The struct-related attributes go to the + struct/union/enum, are ignored, and cause a warning. + - An incomplete declaration of a struct/union. In this case + the name- and struct-related attributes are just ignored, + like GCC does. + *) + let get_definition_attrs optmembers = let (ta, nta) = - List.partition (fun a -> class_of_attribute a = Attr_struct) !attr in + List.partition + (fun a -> match class_of_attribute a with + | Attr_struct -> true + | Attr_name -> optmembers <> None + | _ -> false) + !attr in attr := nta; ta in @@ -720,7 +739,8 @@ let rec elab_specifier ?(only = false) loc env specifier = | [Cabs.Tstruct_union(STRUCT, id, optmembers, a)] -> let a' = - add_attributes (get_struct_attrs()) (elab_attributes env a) in + add_attributes (get_definition_attrs optmembers) + (elab_attributes env a) in let (id', env') = elab_struct_or_union only Struct loc id optmembers a' env in let ty = TStruct(id', !attr) in @@ -729,7 +749,8 @@ let rec elab_specifier ?(only = false) loc env specifier = | [Cabs.Tstruct_union(UNION, id, optmembers, a)] -> let a' = - add_attributes (get_struct_attrs()) (elab_attributes env a) in + add_attributes (get_definition_attrs optmembers) + (elab_attributes env a) in let (id', env') = elab_struct_or_union only Union loc id optmembers a' env in let ty = TUnion(id', !attr) in @@ -738,7 +759,8 @@ let rec elab_specifier ?(only = false) loc env specifier = | [Cabs.Tenum(id, optmembers, a)] -> let a' = - add_attributes (get_struct_attrs()) (elab_attributes env a) in + add_attributes (get_definition_attrs optmembers) + (elab_attributes env a) in let (id', env') = elab_enum only loc id optmembers a' env in let ty = TEnum (id', !attr) in @@ -2359,6 +2381,13 @@ let enter_typedefs loc env sto dl = error loc "initializer in typedef"; if has_std_alignas env ty then error loc "alignment specified for typedef '%s'" s; + List.iter + (fun a -> match class_of_attribute a with + | Attr_object | Attr_struct -> + error loc "attribute '%s' not allowed in 'typedef'" + (name_of_attribute a) + | _ -> ()) + (attributes_of_type_no_expand ty); match previous_def Env.lookup_typedef env s with | Some (s',ty') when Env.in_current_scope env s' -> if equal_types env ty ty' then begin diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index a2c91c0a..3c27f3a9 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -36,7 +36,7 @@ let byteswapped_fields : (ident * string, unit) Hashtbl.t let rec can_byte_swap env ty = match unroll env ty with - | TInt(ik, _) -> (sizeof_ikind ik <= !config.sizeof_ptr (*FIXME*), sizeof_ikind ik > 1) + | TInt(ik, _) -> (sizeof_ikind ik <= !config.sizeof_intreg, sizeof_ikind ik > 1) | TEnum(_, _) -> (true, sizeof_ikind enum_ikind > 1) | TPtr(_, _) -> (true, true) (* tolerance? *) | TArray(ty_elt, _, _) -> can_byte_swap env ty_elt @@ -66,7 +66,7 @@ let transf_field_decl mfa swapped loc env struct_id f = if swapped then begin let (can_swap, must_swap) = can_byte_swap env f.fld_typ in if not can_swap then - error loc "cannot byte-swap field of type '%a'" + fatal_error loc "cannot byte-swap field of type '%a'" Cprint.typ f.fld_typ; if must_swap then Hashtbl.add byteswapped_fields (struct_id, f.fld_name) () @@ -141,7 +141,7 @@ let use_reversed = ref false let bswap_read loc env lval = let ty = lval.etyp in let (bsize, aty) = accessor_type loc env ty in - assert (bsize = 16 || bsize = 32 || (bsize = 64 && !config.sizeof_ptr = 8)); + assert (bsize = 16 || bsize = 32 || (bsize = 64 && !config.sizeof_intreg = 8)); try if !use_reversed then begin let (id, fty) = @@ -168,7 +168,7 @@ let bswap_write loc env lhs rhs = let ty = lhs.etyp in let (bsize, aty) = accessor_type loc env ty in - assert (bsize = 16 || bsize = 32 || (bsize = 64 && !config.sizeof_ptr = 8)); + assert (bsize = 16 || bsize = 32 || (bsize = 64 && !config.sizeof_intreg = 8)); try if !use_reversed then begin let (id, fty) = diff --git a/doc/index.html b/doc/index.html index 72875e1a..edb3accd 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; } <H1 align="center">The CompCert verified compiler</H1> <H2 align="center">Commented Coq development</H2> -<H3 align="center">Version 3.4, 2018-09-17</H3> +<H3 align="center">Version 3.5, 2019-02-27</H3> <H2>Introduction</H2> @@ -183,7 +183,7 @@ code. <TD>Recognition of operators<br>and addressing modes</TD> <TD>Cminor to CminorSel</TD> <TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br> - <A HREF="html/Selectcompcert.powerpc.Op.html"><I>SelectOp</I></A><br> + <A HREF="html/compcert.powerpc.SelectOp.html"><I>SelectOp</I></A><br> <A HREF="html/compcert.powerpc.SelectLong.html"><I>SelectLong</I></A><br> <A HREF="html/compcert.backend.SelectDiv.html">SelectDiv</A><br> <A HREF="html/compcert.backend.SplitLong.html">SplitLong</A></TD> @@ -228,7 +228,7 @@ code. <TD>Constant propagation</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br> - <A HREF="html/compcert.powerpc.Constpropcompcert.powerpc.Op.html"><I>ConstpropOp</I></A></TD> + <A HREF="html/compcert.powerpc.ConstpropOp.html"><I>ConstpropOp</I></A></TD> <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br> <A HREF="html/compcert.powerpc.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD> </TR> @@ -237,7 +237,7 @@ code. <TD>Common subexpression elimination</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR> - <A HREF="html/compcert.powerpc.Combinecompcert.powerpc.Op.html"><I>CombineOp</I></A></TD> + <A HREF="html/compcert.powerpc.CombineOp.html"><I>CombineOp</I></A></TD> <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR> <A HREF="html/compcert.powerpc.CombineOpproof.html"><I>CombineOpproof</I></A></TD> </TR> @@ -328,10 +328,10 @@ CSE, and dead code elimination. <LI> <A HREF="html/compcert.backend.Liveness.html">Liveness</A>: liveness analysis</A>. <LI> <A HREF="html/compcert.backend.ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR> See also: <A HREF="html/compcert.backend.ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR> -See also: <A HREF="html/ValueAcompcert.powerpc.Op.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis. +See also: <A HREF="html/compcert.powerpc.ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis. <LI> <A HREF="html/compcert.backend.Deadcode.html">Deadcode</A>: neededness analysis</A> <BR> See also: <A HREF="html/compcert.backend.NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR> -See also: <A HREF="html/compcert.powerpc.Needcompcert.powerpc.Op.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis. +See also: <A HREF="html/compcert.powerpc.NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis. </UL> <H3>Type systems</H3> diff --git a/lib/Floats.v b/lib/Floats.v index 0c8ff5a4..ba225be1 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -48,6 +48,9 @@ Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : match x with Some(Gt|Eq) => true | _ => false end end. +Definition ordered_of_comparison (x: option Datatypes.comparison) : bool := + match x with None => false | Some _ => true end. + Lemma cmp_of_comparison_swap: forall c x, cmp_of_comparison (swap_comparison c) x = @@ -217,8 +220,12 @@ Definition mul: float -> float -> float := Bmult 53 1024 __ __ binop_pl mode_NE. (**r multiplication *) Definition div: float -> float -> float := Bdiv 53 1024 __ __ binop_pl mode_NE. (**r division *) -Definition cmp (c:comparison) (f1 f2: float) : bool := (**r comparison *) - cmp_of_comparison c (Bcompare _ _ f1 f2). +Definition compare (f1 f2: float) : option Datatypes.comparison := (**r general comparison *) + Bcompare 53 1024 f1 f2. +Definition cmp (c:comparison) (f1 f2: float) : bool := (**r Boolean comparison *) + cmp_of_comparison c (compare f1 f2). +Definition ordered (f1 f2: float) : bool := + ordered_of_comparison (compare f1 f2). (** Conversions *) @@ -322,7 +329,7 @@ Qed. Theorem cmp_swap: forall c x y, cmp (swap_comparison c) x y = cmp c y x. Proof. - unfold cmp; intros. rewrite (Bcompare_swap _ _ x y). + unfold cmp, compare; intros. rewrite (Bcompare_swap _ _ x y). apply cmp_of_comparison_swap. Qed. @@ -440,7 +447,7 @@ Proof. subst p; smart_omega. destruct (ZofB_range_pos 53 1024 __ __ x p C) as [P Q]. omega. assert (CMP: Bcompare _ _ x y = Some Lt). - { unfold cmp, cmp_of_comparison in H. destruct (Bcompare _ _ x y) as [[]|]; auto; discriminate. } + { unfold cmp, cmp_of_comparison, compare in H. destruct (Bcompare _ _ x y) as [[]|]; auto; discriminate. } rewrite Bcompare_correct in CMP by auto. inv CMP. apply Rcompare_Lt_inv in H1. rewrite EQy in H1. assert (p < Int.unsigned ox8000_0000). @@ -465,7 +472,7 @@ Proof. assert (FINx: is_finite _ _ x = true). { rewrite ZofB_correct in C. destruct (is_finite _ _ x) eqn:FINx; congruence. } assert (GE: (B2R _ _ x >= Z2R (Int.unsigned ox8000_0000))%R). - { rewrite <- EQy. unfold cmp, cmp_of_comparison in H. + { rewrite <- EQy. unfold cmp, cmp_of_comparison, compare in H. rewrite Bcompare_correct in H by auto. destruct (Rcompare (B2R 53 1024 x) (B2R 53 1024 y)) eqn:CMP. apply Req_ge; apply Rcompare_Eq_inv; auto. @@ -949,8 +956,12 @@ Definition mul: float32 -> float32 -> float32 := Bmult 24 128 __ __ binop_pl mode_NE. (**r multiplication *) Definition div: float32 -> float32 -> float32 := Bdiv 24 128 __ __ binop_pl mode_NE. (**r division *) +Definition compare (f1 f2: float32) : option Datatypes.comparison := (**r general comparison *) + Bcompare 24 128 f1 f2. Definition cmp (c:comparison) (f1 f2: float32) : bool := (**r comparison *) - cmp_of_comparison c (Bcompare _ _ f1 f2). + cmp_of_comparison c (compare f1 f2). +Definition ordered (f1 f2: float32) : bool := + ordered_of_comparison (compare f1 f2). (** Conversions *) @@ -1034,7 +1045,7 @@ Qed. Theorem cmp_swap: forall c x y, cmp (swap_comparison c) x y = cmp c y x. Proof. - unfold cmp; intros. rewrite (Bcompare_swap _ _ x y). + unfold cmp, compare; intros. rewrite (Bcompare_swap _ _ x y). apply cmp_of_comparison_swap. Qed. @@ -1338,12 +1349,12 @@ Global Opaque Float.zero Float.eq_dec Float.neg Float.abs Float.of_single Float.to_single Float.of_int Float.of_intu Float.of_long Float.of_longu Float.to_int Float.to_intu Float.to_long Float.to_longu - Float.add Float.sub Float.mul Float.div Float.cmp + Float.add Float.sub Float.mul Float.div Float.cmp Float.ordered Float.to_bits Float.of_bits Float.from_words. Global Opaque Float32.zero Float32.eq_dec Float32.neg Float32.abs Float32.of_int Float32.of_intu Float32.of_long Float32.of_longu Float32.to_int Float32.to_intu Float32.to_long Float32.to_longu - Float32.add Float32.sub Float32.mul Float32.div Float32.cmp + Float32.add Float32.sub Float32.mul Float32.div Float32.cmp Float32.ordered Float32.to_bits Float32.of_bits. diff --git a/lib/Integers.v b/lib/Integers.v index a905a7d1..0e506208 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -150,19 +150,19 @@ Lemma Z_mod_modulus_range: Proof. intros; unfold Z_mod_modulus. destruct x. - - generalize modulus_pos; omega. + - generalize modulus_pos; intuition. - apply P_mod_two_p_range. - set (r := P_mod_two_p p wordsize). assert (0 <= r < modulus) by apply P_mod_two_p_range. destruct (zeq r 0). - + generalize modulus_pos; omega. - + omega. + + generalize modulus_pos; intuition. + + Psatz.lia. Qed. Lemma Z_mod_modulus_range': forall x, -1 < Z_mod_modulus x < modulus. Proof. - intros. generalize (Z_mod_modulus_range x); omega. + intros. generalize (Z_mod_modulus_range x); intuition. Qed. Lemma Z_mod_modulus_eq: @@ -178,10 +178,10 @@ Proof. set (r := P_mod_two_p p wordsize) in *. rewrite <- B in C. change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0). - + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. ring. - generalize modulus_pos; omega. - + symmetry. apply Zmod_unique with (-q - 1). rewrite C. ring. - omega. + + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. Psatz.lia. + intuition. + + symmetry. apply Zmod_unique with (-q - 1). rewrite C. Psatz.lia. + intuition. Qed. (** The [unsigned] and [signed] functions return the Coq integer corresponding diff --git a/powerpc/Asm.v b/powerpc/Asm.v index aa15547b..ad24f563 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -606,7 +606,7 @@ Definition load1 (chunk: memory_chunk) (rd: preg) Definition load2 (chunk: memory_chunk) (rd: preg) (r1 r2: ireg) (rs: regset) (m: mem) := - match Mem.loadv chunk m (Val.add rs#r1 rs#r2) with + match Mem.loadv chunk m (Val.add (gpr_or_zero rs r1) rs#r2) with | None => Stuck | Some v => Next (nextinstr (rs#rd <- v)) m end. @@ -620,7 +620,7 @@ Definition store1 (chunk: memory_chunk) (r: preg) Definition store2 (chunk: memory_chunk) (r: preg) (r1 r2: ireg) (rs: regset) (m: mem) := - match Mem.storev chunk m (Val.add rs#r1 rs#r2) (rs#r) with + match Mem.storev chunk m (Val.add (gpr_or_zero rs r1) rs#r2) (rs#r) with | None => Stuck | Some m' => Next (nextinstr rs) m' end. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 5a2df8d3..49a0d237 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -348,7 +348,7 @@ let expand_builtin_vstore_1 chunk addr src = expand_store_int64 hi lo temp (Cint _0) (Cint _4)) (fun r1 r2 -> emit (Padd(temp, r1, r2)); - expand_load_int64 hi lo temp (Cint _0) (Cint _4)) + expand_store_int64 hi lo temp (Cint _0) (Cint _4)) addr temp | _, _ -> assert false @@ -410,6 +410,30 @@ let expand_builtin_va_start r = let expand_int64_arith conflict rl fn = if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl +(* Expansion of integer conditional moves (__builtin_*sel) *) +(* The generated code works equally well with 32-bit integer registers + and with 64-bit integer registers. *) + +let expand_integer_cond_move a1 a2 a3 res = + if a2 = a3 then + emit (Pmr (res, a2)) + else if eref then begin + emit (Pcmpwi (a1,Cint (Int.zero))); + emit (Pisel (res,a3,a2,CRbit_2)) + end else begin + (* a1 has type _Bool, hence it is 0 or 1 *) + emit (Psubfic (GPR0, a1, Cint _0)); + (* r0 = -1 (all ones) if a1 is true, r0 = 0 if a1 is false *) + if res <> a3 then begin + emit (Pand_ (res, a2, GPR0)); + emit (Pandc (GPR0, a3, GPR0)) + end else begin + emit (Pandc (res, a3, GPR0)); + emit (Pand_ (GPR0, a2, GPR0)) + end; + emit (Por (res, res, GPR0)) + end + (* Convert integer constant into GPR with corresponding number *) let int_to_int_reg = function | 0 -> Some GPR0 | 1 -> Some GPR1 | 2 -> Some GPR2 | 3 -> Some GPR3 @@ -669,25 +693,13 @@ let expand_builtin_inline name args res = | "__builtin_return_address",_,BR (IR res) -> emit (Plwz (res, Cint! retaddr_offset,GPR1)) (* Integer selection *) - | ("__builtin_isel" | "__builtin_uisel"), [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> - if eref then begin - emit (Pcmpwi (a1,Cint (Int.zero))); - emit (Pisel (res,a3,a2,CRbit_2)) - end else if a2 = a3 then - emit (Pmr (res, a2)) - else begin - (* a1 has type _Bool, hence it is 0 or 1 *) - emit (Psubfic (GPR0, a1, Cint _0)); - (* r0 = 0xFFFF_FFFF if a1 is true, r0 = 0 if a1 is false *) - if res <> a3 then begin - emit (Pand_ (res, a2, GPR0)); - emit (Pandc (GPR0, a3, GPR0)) - end else begin - emit (Pandc (res, a3, GPR0)); - emit (Pand_ (GPR0, a2, GPR0)) - end; - emit (Por (res, res, GPR0)) - end + | ("__builtin_bsel" | "__builtin_isel" | "__builtin_uisel"), [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> + expand_integer_cond_move a1 a2 a3 res + | ("__builtin_isel64" | "__builtin_uisel64"), [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> + if Archi.ppc64 then + expand_integer_cond_move a1 a2 a3 res + else + raise (Error (name ^" is only supported for PPC64 targets")) (* no operation *) | "__builtin_nop", [], _ -> emit (Pori (GPR0, GPR0, Cint _0)) diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 460fa670..c18757b2 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -735,7 +735,9 @@ Proof. intros. repeat Simplif. - exploit (loadimm_correct GPR0 ofs'); eauto. intros [rs' [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. - apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen. + apply exec_straight_one. rewrite H0. unfold load2. + rewrite gpr_or_zero_not_zero by auto. simpl. + rewrite Q, R by auto with asmgen. rewrite LD. reflexivity. unfold nextinstr. repeat Simplif. split. repeat Simplif. intros. repeat Simplif. @@ -789,6 +791,7 @@ Proof. - exploit (loadimm_correct GPR0 ofs'); eauto. intros [rs' [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. rewrite H0. unfold store2. + rewrite gpr_or_zero_not_zero by auto. rewrite Q. rewrite R by auto with asmgen. rewrite R by auto. rewrite ST. reflexivity. unfold nextinstr. repeat Simplif. intros. repeat Simplif. @@ -1409,7 +1412,7 @@ Lemma transl_memory_access_correct: exists rs', exec_straight ge fn (mk1 cst r1 :: k) rs1 m k rs' m' /\ P rs') -> (forall (r1 r2: ireg) (rs1: regset) k, - Val.lessdef a (Val.add rs1#r1 rs1#r2) -> + Val.lessdef a (Val.add (gpr_or_zero rs1 r1) rs1#r2) -> (forall r, r <> PC -> r <> temp -> r <> GPR0 -> rs1 r = rs r) -> exists rs', exec_straight ge fn (mk2 r1 r2 :: k) rs1 m k rs' m' /\ P rs') -> @@ -1435,7 +1438,7 @@ Transparent Val.add. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. auto. auto. (* Aindexed2 *) - apply MK2; auto. + apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. (* Aglobal *) destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. (* Aglobal from small data *) @@ -1469,6 +1472,7 @@ Transparent Val.add. (* Abased from small data *) set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). exploit (MK2 x GPR0 rs1 k). + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. unfold rs1; Simpl. rewrite Val.add_commut. auto. intros. unfold rs1; Simpl. intros [rs' [EX' AG']]. @@ -1483,6 +1487,7 @@ Transparent Val.add. set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))). set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))). exploit (MK2 temp GPR0 rs3). + rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. intros. unfold rs3, rs2, rs1; Simpl. intros [rs' [EX' AG']]. diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index c76b69ba..11b7aef9 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -142,6 +142,15 @@ let builtins = { (* uisel *) "__builtin_uisel", (TInt (IUInt, []),[TInt(IBool, []);TInt(IUInt, []);TInt(IUInt, [])],false); + (* isel64 *) + "__builtin_isel64", + (TInt (ILongLong, []),[TInt(IBool, []);TInt(ILongLong, []);TInt(ILongLong, [])],false); + (* uisel *) + "__builtin_uisel64", + (TInt (IULongLong, []),[TInt(IBool, []);TInt(IULongLong, []);TInt(IULongLong, [])],false); + (* bsel *) + "__builtin_bsel", + (TInt (IBool, []),[TInt(IBool, []);TInt(IBool, []);TInt(IBool, [])],false); (* no operation *) "__builtin_nop", (TVoid [], [], false); diff --git a/runtime/include/stdbool.h b/runtime/include/stdbool.h index 07a25eb0..c549da08 100644 --- a/runtime/include/stdbool.h +++ b/runtime/include/stdbool.h @@ -36,4 +36,5 @@ #define true 1 #define false 0 #define __bool_true_false_are_defined 1 + #endif diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h index 6056db62..5a66215a 100644 --- a/runtime/include/stddef.h +++ b/runtime/include/stddef.h @@ -108,7 +108,7 @@ typedef signed int wchar_t; #if defined(_STDDEF_H) || defined(__need_NULL) #ifndef NULL -#define NULL 0 +#define NULL ((void *) 0) #endif #undef __need_NULL #endif diff --git a/test/regression/Makefile b/test/regression/Makefile index 191a2285..760ee570 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -23,7 +23,7 @@ TESTS=int32 int64 floats floats-basics \ TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ bitfields5 bitfields6 bitfields7 bitfields8 \ builtins-$(ARCH) packedstruct1 packedstruct2 alignas \ - varargs1 varargs2 sections alias + varargs1 varargs2 varargs3 sections alias aligned # Can run, both in compiled mode and in interpreter mode, # but produce processor-dependent results, so no reference output in Results diff --git a/test/regression/Results/aligned b/test/regression/Results/aligned new file mode 100644 index 00000000..c42a5c40 --- /dev/null +++ b/test/regression/Results/aligned @@ -0,0 +1,12 @@ +a: size 1, offset mod 16 = 0 +b: size 3, offset mod 16 = 0 +c: size is that of a pointer, offset mod 16 is good +d: size 1, offset mod 16 = 0 +f: size is that of a pointer, offset mod 16 is good +g: size 32, offset mod 16 = 0 +h: size 16, offset mod 16 = 0 +i: size 16, offset mod 16 = 0 +j: size 16, offset mod 16 = 0 +T2: size 112, alignment 16 +T4: size is that of a pointer, alignment is that of a pointer +t2: size 9, alignment 1 diff --git a/test/regression/aligned.c b/test/regression/aligned.c new file mode 100644 index 00000000..bd16d513 --- /dev/null +++ b/test/regression/aligned.c @@ -0,0 +1,115 @@ +/* The "aligned" attribute */ + +#include <stdio.h> + +#define ALIGNED __attribute((aligned(16))) +#define ALIGNED1 __attribute((aligned(1))) + +typedef ALIGNED char c16; + +struct s { + char y; + char ALIGNED x; +}; + +typedef struct { char y; } ALIGNED u; + +struct { + char filler1; + + /* Base type */ + char ALIGNED a; + /* Array */ + /* Expected: array of 3 naturally-aligned chars -> size = 3 */ + ALIGNED char b[3]; + /* Pointer */ + /* Expected: 16-aligned pointer to naturally-aligned char */ + ALIGNED char * c; + +/* Typedef */ + + c16 d; + /* Expected: like char ALIGNED d */ + // c16 e[3] = {2, 3, 4}; + /* Expected: unclear. This one is rejected by gcc. + clang says size = 16, alignment = 16, but initializes first 3 bytes only. + compcert says size = 3, alignment = 16. */ + char filler2; + c16 * f; + /* Expected: naturally-aligned pointer to 16-aligned char */ + +/* Struct */ + + struct s g; + /* Expected: alignment 16, size 17 + (1 byte, padding to mod 16, 1 bytes) */ + + char filler3; + + struct t { + char y; + } ALIGNED h; + /* Expected: type struct t and variable h have alignment 16 and size 1 */ + + char filler4; + + struct t i; + /* Expected: alignment 16 and size 1. This checks that the ALIGNED + attribute is attached to "struct t". */ + + char filler5; + + u j; + /* Expected: type u and variable j have alignment 16 and size 1. */ +} x; + +typedef char T1[100]; + +typedef struct { T1 mess[1]; } ALIGNED T2; +/* Expected: alignment 16, size 112 = 100 aligned to 16 */ + +typedef T2 T3[]; + +typedef struct { T3 *area; } T4; +/* Expected: size of a pointer, alignment of a pointer */ + +struct t1 { double d; }; +struct t2 { char c; ALIGNED1 struct t1 d; }; +/* Expected: size = 1 + 8, alignment 1 */ + +void check(const char * msg, void * addr, size_t sz) +{ + printf("%s: size %zu, offset mod 16 = %lu\n", + msg, sz, (unsigned long) ((char *) addr - (char *) &x) % 16); +} + +void checkptr(const char * msg, void * addr, size_t sz, size_t al) +{ + printf("%s: size %s that of a pointer, offset mod 16 %s\n", + msg, + sz == sizeof(void *) ? "is" : "IS NOT", + (((char *) addr - (char *) &x) % 16) == al ? + "is good" : "IS BAD"); +} + +int main() +{ + check("a", &(x.a), sizeof(x.a)); + check("b", &(x.b), sizeof(x.b)); + checkptr("c", &(x.c), sizeof(x.c), 0); + check("d", &(x.d), sizeof(x.d)); + checkptr("f", &(x.f), sizeof(x.f), _Alignof(void *)); + check("g", &(x.g), sizeof(x.g)); + check("h", &(x.h), sizeof(x.h)); + check("i", &(x.i), sizeof(x.i)); + check("j", &(x.j), sizeof(x.j)); + + printf("T2: size %zu, alignment %zu\n", sizeof(T2), _Alignof(T2)); + printf("T4: size %s that of a pointer, alignment %s that of a pointer\n", + sizeof(T4) == sizeof(void *) ? "is" : "IS NOT", + _Alignof(T4) == _Alignof(void *) ? "is" : "IS NOT"); + + printf("t2: size %zu, alignment %zu\n", + sizeof(struct t2), _Alignof(struct t2)); + return 0; +} diff --git a/test/regression/varargs3.c b/test/regression/varargs3.c new file mode 100644 index 00000000..a46d81e3 --- /dev/null +++ b/test/regression/varargs3.c @@ -0,0 +1,52 @@ +#include <stdarg.h> +#include <stdio.h> + +void initialize(int first, ...) +{ + va_list ap; + va_start(ap, first); + while (1) { + int * p = va_arg(ap, int *); + if (p == NULL) break; + *p = first; + first++; + } +} + +void test(void) +{ + int a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q; + initialize(42, &a, &b, &c, &d, &e, &f, &g, &h, &i, &j, + &k, &l, &m, &n, &o, &p, &q, NULL); + printf("a = %d\n", a); + printf("b = %d\n", b); + printf("c = %d\n", c); + printf("d = %d\n", d); + printf("e = %d\n", e); + printf("f = %d\n", f); + printf("g = %d\n", g); + printf("h = %d\n", h); + printf("i = %d\n", i); + printf("j = %d\n", j); + printf("k = %d\n", k); + printf("l = %d\n", l); + printf("m = %d\n", m); + printf("n = %d\n", n); + printf("o = %d\n", o); + printf("p = %d\n", p); + printf("q = %d\n", q); +} + +void wipestack(void) +{ + unsigned int b[100]; + int i; + for (i = 0; i < 100; i++) ((volatile unsigned int *)b)[i] = 0xDEADBEEFU; +} + +int main() +{ + wipestack(); + test(); + return 0; +} @@ -442,8 +442,8 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := #PF <- Vundef. (** Floating-point comparison between x and y: -- ZF = 1 if x=y or unordered, 0 if x<>y -- CF = 1 if x<y or unordered, 0 if x>=y +- ZF = 1 if x=y or unordered, 0 if x<>y and ordered +- CF = 1 if x<y or unordered, 0 if x>=y. - PF = 1 if unordered, 0 if ordered. - SF and 0F are undefined *) @@ -451,9 +451,9 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := Definition compare_floats (vx vy: val) (rs: regset) : regset := match vx, vy with | Vfloat x, Vfloat y => - rs #ZF <- (Val.of_bool (negb (Float.cmp Cne x y))) + rs #ZF <- (Val.of_bool (Float.cmp Ceq x y || negb (Float.ordered x y))) #CF <- (Val.of_bool (negb (Float.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float.cmp Ceq x y || Float.cmp Clt x y || Float.cmp Cgt x y))) + #PF <- (Val.of_bool (negb (Float.ordered x y))) #SF <- Vundef #OF <- Vundef | _, _ => @@ -463,9 +463,9 @@ Definition compare_floats (vx vy: val) (rs: regset) : regset := Definition compare_floats32 (vx vy: val) (rs: regset) : regset := match vx, vy with | Vsingle x, Vsingle y => - rs #ZF <- (Val.of_bool (negb (Float32.cmp Cne x y))) + rs #ZF <- (Val.of_bool (Float32.cmp Ceq x y || negb (Float32.ordered x y))) #CF <- (Val.of_bool (negb (Float32.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float32.cmp Ceq x y || Float32.cmp Clt x y || Float32.cmp Cgt x y))) + #PF <- (Val.of_bool (negb (Float32.ordered x y))) #SF <- Vundef #OF <- Vundef | _, _ => diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index c5b03426..904debdc 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -700,9 +700,9 @@ Qed. Lemma compare_floats_spec: forall rs n1 n2, let rs' := nextinstr (compare_floats (Vfloat n1) (Vfloat n2) rs) in - rs'#ZF = Val.of_bool (negb (Float.cmp Cne n1 n2)) + rs'#ZF = Val.of_bool (Float.cmp Ceq n1 n2 || negb (Float.ordered n1 n2)) /\ rs'#CF = Val.of_bool (negb (Float.cmp Cge n1 n2)) - /\ rs'#PF = Val.of_bool (negb (Float.cmp Ceq n1 n2 || Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2)) + /\ rs'#PF = Val.of_bool (negb (Float.ordered n1 n2)) /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. intros. unfold rs'; unfold compare_floats. @@ -715,9 +715,9 @@ Qed. Lemma compare_floats32_spec: forall rs n1 n2, let rs' := nextinstr (compare_floats32 (Vsingle n1) (Vsingle n2) rs) in - rs'#ZF = Val.of_bool (negb (Float32.cmp Cne n1 n2)) + rs'#ZF = Val.of_bool (Float32.cmp Ceq n1 n2 || negb (Float32.ordered n1 n2)) /\ rs'#CF = Val.of_bool (negb (Float32.cmp Cge n1 n2)) - /\ rs'#PF = Val.of_bool (negb (Float32.cmp Ceq n1 n2 || Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2)) + /\ rs'#PF = Val.of_bool (negb (Float32.ordered n1 n2)) /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. intros. unfold rs'; unfold compare_floats32. @@ -763,38 +763,22 @@ Proof. intros [A [B [C D]]]. unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. -(* eq *) - rewrite Float.cmp_ne_eq. - caseEq (Float.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto. -(* ne *) - rewrite Float.cmp_ne_eq. - caseEq (Float.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto. -(* lt *) - rewrite <- (Float.cmp_swap Cge n1 n2). - rewrite <- (Float.cmp_swap Cne n1 n2). - simpl. - rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq. - caseEq (Float.cmp Clt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float.cmp_lt_eq_false; eauto. - auto. - destruct (Float.cmp Ceq n1 n2); auto. -(* le *) +- (* eq *) +Transparent Float.cmp Float.ordered. + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. +- (* ne *) + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. +- (* lt *) + rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. + destruct (Float.compare n2 n1) as [[]|]; reflexivity. +- (* le *) rewrite <- (Float.cmp_swap Cge n1 n2). simpl. - destruct (Float.cmp Cle n1 n2); auto. -(* gt *) - rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. - caseEq (Float.cmp Cgt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float.cmp_gt_eq_false; eauto. - auto. - destruct (Float.cmp Ceq n1 n2); auto. -(* ge *) + destruct (Float.compare n1 n2) as [[]|]; auto. +- (* gt *) + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. +- (* ge *) destruct (Float.cmp Cge n1 n2); auto. +Opaque Float.cmp Float.ordered. Qed. Lemma testcond_for_neg_float_comparison_correct: @@ -811,38 +795,22 @@ Proof. intros [A [B [C D]]]. unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. -(* eq *) - rewrite Float.cmp_ne_eq. - caseEq (Float.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto. -(* ne *) - rewrite Float.cmp_ne_eq. - caseEq (Float.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto. -(* lt *) - rewrite <- (Float.cmp_swap Cge n1 n2). - rewrite <- (Float.cmp_swap Cne n1 n2). - simpl. - rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq. - caseEq (Float.cmp Clt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float.cmp_lt_eq_false; eauto. - auto. - destruct (Float.cmp Ceq n1 n2); auto. -(* le *) +- (* eq *) +Transparent Float.cmp Float.ordered. + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. +- (* ne *) + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. +- (* lt *) + rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. + destruct (Float.compare n2 n1) as [[]|]; reflexivity. +- (* le *) rewrite <- (Float.cmp_swap Cge n1 n2). simpl. - destruct (Float.cmp Cle n1 n2); auto. -(* gt *) - rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. - caseEq (Float.cmp Cgt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float.cmp_gt_eq_false; eauto. - auto. - destruct (Float.cmp Ceq n1 n2); auto. -(* ge *) + destruct (Float.compare n1 n2) as [[]|]; auto. +- (* gt *) + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. +- (* ge *) destruct (Float.cmp Cge n1 n2); auto. +Opaque Float.cmp Float.ordered. Qed. Lemma testcond_for_float32_comparison_correct: @@ -859,38 +827,22 @@ Proof. intros [A [B [C D]]]. unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. -(* eq *) - rewrite Float32.cmp_ne_eq. - caseEq (Float32.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto. -(* ne *) - rewrite Float32.cmp_ne_eq. - caseEq (Float32.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto. -(* lt *) - rewrite <- (Float32.cmp_swap Cge n1 n2). - rewrite <- (Float32.cmp_swap Cne n1 n2). - simpl. - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq. - caseEq (Float32.cmp Clt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float32.cmp_lt_eq_false; eauto. - auto. - destruct (Float32.cmp Ceq n1 n2); auto. -(* le *) +- (* eq *) +Transparent Float32.cmp Float32.ordered. + unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. +- (* ne *) + unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. +- (* lt *) + rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. + destruct (Float32.compare n2 n1) as [[]|]; reflexivity. +- (* le *) rewrite <- (Float32.cmp_swap Cge n1 n2). simpl. - destruct (Float32.cmp Cle n1 n2); auto. -(* gt *) - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. - caseEq (Float32.cmp Cgt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float32.cmp_gt_eq_false; eauto. - auto. - destruct (Float32.cmp Ceq n1 n2); auto. -(* ge *) + destruct (Float32.compare n1 n2) as [[]|]; auto. +- (* gt *) + unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. +- (* ge *) destruct (Float32.cmp Cge n1 n2); auto. +Opaque Float32.cmp Float32.ordered. Qed. Lemma testcond_for_neg_float32_comparison_correct: @@ -907,38 +859,22 @@ Proof. intros [A [B [C D]]]. unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. -(* eq *) - rewrite Float32.cmp_ne_eq. - caseEq (Float32.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto. -(* ne *) - rewrite Float32.cmp_ne_eq. - caseEq (Float32.cmp Ceq n1 n2); intros. - auto. - simpl. destruct (Float32.cmp Clt n1 n2 || Float32.cmp Cgt n1 n2); auto. -(* lt *) - rewrite <- (Float32.cmp_swap Cge n1 n2). - rewrite <- (Float32.cmp_swap Cne n1 n2). - simpl. - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq. - caseEq (Float32.cmp Clt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float32.cmp_lt_eq_false; eauto. - auto. - destruct (Float32.cmp Ceq n1 n2); auto. -(* le *) +- (* eq *) +Transparent Float32.cmp Float32.ordered. + unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. +- (* ne *) + unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. +- (* lt *) + rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. + destruct (Float32.compare n2 n1) as [[]|]; reflexivity. +- (* le *) rewrite <- (Float32.cmp_swap Cge n1 n2). simpl. - destruct (Float32.cmp Cle n1 n2); auto. -(* gt *) - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. - caseEq (Float32.cmp Cgt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float32.cmp_gt_eq_false; eauto. - auto. - destruct (Float32.cmp Ceq n1 n2); auto. -(* ge *) + destruct (Float32.compare n1 n2) as [[]|]; auto. +- (* gt *) + unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. +- (* ge *) destruct (Float32.cmp Cge n1 n2); auto. +Opaque Float32.cmp Float32.ordered. Qed. Remark swap_floats_commut: |