aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--Changelog35
-rw-r--r--Makefile7
-rw-r--r--VERSION2
-rw-r--r--backend/SelectDivproof.v14
-rw-r--r--cfrontend/C2C.ml5
-rw-r--r--cfrontend/Ctypes.v56
-rw-r--r--common/Linking.v94
-rwxr-xr-xconfigure11
-rw-r--r--cparser/Checks.ml9
-rw-r--r--cparser/Cutil.ml38
-rw-r--r--cparser/Cutil.mli9
-rw-r--r--cparser/Elab.ml51
-rw-r--r--cparser/PackedStructs.ml8
-rw-r--r--doc/index.html12
-rw-r--r--lib/Floats.v29
-rw-r--r--lib/Integers.v16
-rw-r--r--powerpc/Asm.v4
-rw-r--r--powerpc/Asmexpand.ml52
-rw-r--r--powerpc/Asmgenproof1.v11
-rw-r--r--powerpc/CBuiltins.ml9
-rw-r--r--runtime/include/stdbool.h1
-rw-r--r--runtime/include/stddef.h2
-rw-r--r--test/regression/Makefile2
-rw-r--r--test/regression/Results/aligned12
-rw-r--r--test/regression/aligned.c115
-rw-r--r--test/regression/varargs3.c52
-rw-r--r--x86/Asm.v12
-rw-r--r--x86/Asmgenproof1.v184
29 files changed, 564 insertions, 290 deletions
diff --git a/.gitignore b/.gitignore
index 42bf23b3..f5911e69 100644
--- a/.gitignore
+++ b/.gitignore
@@ -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
diff --git a/Changelog b/Changelog
index fda9417e..e5e701d0 100644
--- a/Changelog
+++ b/Changelog
@@ -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
=======================
diff --git a/Makefile b/Makefile
index f2a18d3f..ed9059db 100644
--- a/Makefile
+++ b/Makefile
@@ -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)
diff --git a/VERSION b/VERSION
index 895933ab..d4563a62 100644
--- a/VERSION
+++ b/VERSION
@@ -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.
diff --git a/configure b/configure
index 2d18531d..a3a2ea8c 100755
--- a/configure
+++ b/configure
@@ -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;
+}
diff --git a/x86/Asm.v b/x86/Asm.v
index dfa2a88a..32235c2d 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -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:
generated by cgit (git 2.34.1) at 2024-05-20 07:53:53 +0000