diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-11-12 19:23:49 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2019-03-26 16:08:10 +0100 |
| commit | 8252140c54d9be6f8c62a068f96795eac1e6c078 (patch) | |
| tree | 33a8ab2fd1a18c094f16888ab88acc6d940bf294 | |
| parent | 1df887f5a275e4c31096018ff1a8fdfc39bca591 (diff) | |
| download | compcert-8252140c54d9be6f8c62a068f96795eac1e6c078.tar.gz compcert-8252140c54d9be6f8c62a068f96795eac1e6c078.zip | |
Introduce and use the type fp_comparison for floating-point comparisons
With FP arithmetic, the negation of "x < y" is not "x >= y". For this reason, the back-end intermediate languages of CompCert used to have both "Ccompf c" and "Cnotcompf c" comparison operators, where "c" is of type Integers.comparison and "Cnotcompf c" denotes the negation of FP comparison c.
There are some problems with this approach:
- Beyond Cnotcompf we also need Cnotcompfs (for single precision FP) and, in case of ARM, special forms for not-comparison against 0.0. This duplication of comparison constructors inevitably causes some code and proof duplication.
- Cnotcompf Ceq is really Ccompf Cne, and likewise Cnotcompf Cne is really Ccompf Ceq, hence the representation of FP comparisons is not canonical, adding to the code and proof duplication mentioned above.
- Cnotcompf is introduced in CminorSel, but in Cminor we don't have it, making it impossible to express some transformations over comparisons at the machine-independent Cminor level.
This commit develops an alternate approach, whereas FP comparisons have their own type, defined as Floats.fp_comparison, and which includes constructors for "not <", "not <=", "not >" and "not >=". Hence this type is closed under boolean negation, so to speak, and there is no longer a need for "Cnotcompf", given that "Ccompf" takes a fp_comparison and can therefore express all FP comparisons of interest.
46 files changed, 556 insertions, 761 deletions
@@ -474,10 +474,10 @@ unord N=0 Z=0 C=1 V=1 Definition compare_float (rs: regset) (v1 v2: val) := match v1, v2 with | Vfloat f1, Vfloat f2 => - rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2)) - #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2)) - #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2))) - #CV <- (Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2))) + rs#CN <- (Val.of_bool (Float.cmp FClt f1 f2)) + #CZ <- (Val.of_bool (Float.cmp FCeq f1 f2)) + #CC <- (Val.of_bool (negb (Float.cmp FClt f1 f2))) + #CV <- (Val.of_bool (negb (Float.cmp FCeq f1 f2 || Float.cmp FClt f1 f2 || Float.cmp FCgt f1 f2))) | _, _ => rs#CN <- Vundef #CZ <- Vundef @@ -488,10 +488,10 @@ Definition compare_float (rs: regset) (v1 v2: val) := Definition compare_float32 (rs: regset) (v1 v2: val) := match v1, v2 with | Vsingle f1, Vsingle f2 => - rs#CN <- (Val.of_bool (Float32.cmp Clt f1 f2)) - #CZ <- (Val.of_bool (Float32.cmp Ceq f1 f2)) - #CC <- (Val.of_bool (negb (Float32.cmp Clt f1 f2))) - #CV <- (Val.of_bool (negb (Float32.cmp Ceq f1 f2 || Float32.cmp Clt f1 f2 || Float32.cmp Cgt f1 f2))) + rs#CN <- (Val.of_bool (Float32.cmp FClt f1 f2)) + #CZ <- (Val.of_bool (Float32.cmp FCeq f1 f2)) + #CC <- (Val.of_bool (negb (Float32.cmp FClt f1 f2))) + #CV <- (Val.of_bool (negb (Float32.cmp FCeq f1 f2 || Float32.cmp FClt f1 f2 || Float32.cmp FCgt f1 f2))) | _, _ => rs#CN <- Vundef #CZ <- Vundef diff --git a/arm/Asmgen.v b/arm/Asmgen.v index f12ea870..4ed100d3 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -258,27 +258,15 @@ Definition transl_cond | Ccompf cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (Pfcmpd r1 r2 :: k) - | Cnotcompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmpd r1 r2 :: k) | Ccompfzero cmp, a1 :: nil => do r1 <- freg_of a1; OK (Pfcmpzd r1 :: k) - | Cnotcompfzero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmpzd r1 :: k) | Ccompfs cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (Pfcmps r1 r2 :: k) - | Cnotcompfs cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmps r1 r2 :: k) | Ccompfszero cmp, a1 :: nil => do r1 <- freg_of a1; OK (Pfcmpzs r1 :: k) - | Cnotcompfszero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmpzs r1 :: k) | _, _ => Error(msg "Asmgen.transl_cond") end. @@ -303,24 +291,18 @@ Definition cond_for_unsigned_cmp (cmp: comparison) := | Cge => TChs end. -Definition cond_for_float_cmp (cmp: comparison) := - match cmp with - | Ceq => TCeq - | Cne => TCne - | Clt => TCmi - | Cle => TCls - | Cgt => TCgt - | Cge => TCge - end. - -Definition cond_for_float_not_cmp (cmp: comparison) := +Definition cond_for_float_cmp (cmp: fp_comparison) := match cmp with - | Ceq => TCne - | Cne => TCeq - | Clt => TCpl - | Cle => TChi - | Cgt => TCle - | Cge => TClt + | FCeq => TCeq + | FCne => TCne + | FClt => TCmi + | FCle => TCls + | FCgt => TCgt + | FCge => TCge + | FCnotlt => TCpl + | FCnotle => TChi + | FCnotgt => TCle + | FCnotge => TClt end. Definition cond_for_cond (cond: condition) := @@ -332,13 +314,9 @@ Definition cond_for_cond (cond: condition) := | Ccompimm cmp n => cond_for_signed_cmp cmp | Ccompuimm cmp n => cond_for_unsigned_cmp cmp | Ccompf cmp => cond_for_float_cmp cmp - | Cnotcompf cmp => cond_for_float_not_cmp cmp | Ccompfzero cmp => cond_for_float_cmp cmp - | Cnotcompfzero cmp => cond_for_float_not_cmp cmp | Ccompfs cmp => cond_for_float_cmp cmp - | Cnotcompfs cmp => cond_for_float_not_cmp cmp | Ccompfszero cmp => cond_for_float_cmp cmp - | Cnotcompfszero cmp => cond_for_float_not_cmp cmp end. (** Translation of the arithmetic operation [r <- op(args)]. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 2c001f45..e2a837f7 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -781,19 +781,19 @@ Opaque loadind. left; eapply exec_straight_steps_goto; eauto. intros. simpl in TR. destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. - rewrite EC in B. destruct B as [Bpos Bneg]. + rewrite EC in B. econstructor; econstructor; econstructor; split. eexact A. split. eapply agree_undef_regs; eauto with asmgen. - simpl. rewrite Bpos. reflexivity. + simpl. rewrite B. reflexivity. - (* Mcond false *) exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps; eauto. intros. simpl in TR. destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. - rewrite EC in B. destruct B as [Bpos Bneg]. + rewrite EC in B. econstructor; split. eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite Bpos. reflexivity. auto. + apply exec_straight_one. simpl. rewrite B. reflexivity. auto. split. eapply agree_undef_regs; eauto with asmgen. intros; Simpl. simpl. congruence. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 98cd5eea..6a02b77f 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -799,10 +799,10 @@ Qed. Lemma compare_float_spec: forall rs f1 f2, let rs1 := nextinstr (compare_float rs (Vfloat f1) (Vfloat f2)) in - rs1#CN = Val.of_bool (Float.cmp Clt f1 f2) - /\ rs1#CZ = Val.of_bool (Float.cmp Ceq f1 f2) - /\ rs1#CC = Val.of_bool (negb (Float.cmp Clt f1 f2)) - /\ rs1#CV = Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)). + rs1#CN = Val.of_bool (Float.cmp FClt f1 f2) + /\ rs1#CZ = Val.of_bool (Float.cmp FCeq f1 f2) + /\ rs1#CC = Val.of_bool (negb (Float.cmp FClt f1 f2)) + /\ rs1#CV = Val.of_bool (negb (Float.cmp FCeq f1 f2 || Float.cmp FClt f1 f2 || Float.cmp FCgt f1 f2)). Proof. intros. intuition. Qed. @@ -838,65 +838,48 @@ Proof. intros [A [B [C D]]]. unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. destruct c; simpl. -(* eq *) - destruct (Float.cmp Ceq n1 n2); auto. -(* ne *) - rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto. -(* lt *) - destruct (Float.cmp Clt n1 n2); auto. -(* le *) +- (* eq *) + destruct (Float.cmp FCeq n1 n2); auto. +- (* ne *) + rewrite Float.cmp_ne_eq. destruct (Float.cmp FCeq n1 n2); auto. +- (* lt *) + destruct (Float.cmp FClt n1 n2); auto. +- (* le *) rewrite Float.cmp_le_lt_eq. - destruct (Float.cmp Clt n1 n2); destruct (Float.cmp Ceq n1 n2); auto. -(* gt *) - destruct (Float.cmp Ceq n1 n2) eqn:EQ; - destruct (Float.cmp Clt n1 n2) eqn:LT; - destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + destruct (Float.cmp FClt n1 n2); destruct (Float.cmp FCeq n1 n2); auto. +- (* gt *) + destruct (Float.cmp FCeq n1 n2) eqn:EQ; + destruct (Float.cmp FClt n1 n2) eqn:LT; + destruct (Float.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float.cmp_lt_gt_false; eauto. exfalso; eapply Float.cmp_gt_eq_false; eauto. exfalso; eapply Float.cmp_lt_gt_false; eauto. -(* ge *) +- (* ge *) rewrite Float.cmp_ge_gt_eq. - destruct (Float.cmp Ceq n1 n2) eqn:EQ; - destruct (Float.cmp Clt n1 n2) eqn:LT; - destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + destruct (Float.cmp FCeq n1 n2) eqn:EQ; + destruct (Float.cmp FClt n1 n2) eqn:LT; + destruct (Float.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float.cmp_lt_eq_false; eauto. exfalso; eapply Float.cmp_lt_eq_false; eauto. exfalso; eapply Float.cmp_lt_gt_false; eauto. -Qed. - -Lemma cond_for_float_not_cmp_correct: - forall c n1 n2 rs, - eval_testcond (cond_for_float_not_cmp c) - (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2)))= - Some(negb(Float.cmp c n1 n2)). -Proof. - intros. - generalize (compare_float_spec rs n1 n2). - set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))). - intros [A [B [C D]]]. - unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. - destruct c; simpl. -(* eq *) - destruct (Float.cmp Ceq n1 n2); auto. -(* ne *) - rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto. -(* lt *) - destruct (Float.cmp Clt n1 n2); auto. -(* le *) - rewrite Float.cmp_le_lt_eq. - destruct (Float.cmp Clt n1 n2) eqn:LT; destruct (Float.cmp Ceq n1 n2) eqn:EQ; auto. -(* gt *) - destruct (Float.cmp Ceq n1 n2) eqn:EQ; - destruct (Float.cmp Clt n1 n2) eqn:LT; - destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. +- (* lt *) + rewrite (Float.cmp_negate FClt). destruct (Float.cmp FClt n1 n2); auto. +- (* le *) + rewrite (Float.cmp_negate FCle), Float.cmp_le_lt_eq. + destruct (Float.cmp FClt n1 n2) eqn:LT; destruct (Float.cmp FCeq n1 n2) eqn:EQ; auto. +- (* gt *) + rewrite (Float.cmp_negate FCgt). + destruct (Float.cmp FCeq n1 n2) eqn:EQ; + destruct (Float.cmp FClt n1 n2) eqn:LT; + destruct (Float.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float.cmp_lt_gt_false; eauto. exfalso; eapply Float.cmp_gt_eq_false; eauto. exfalso; eapply Float.cmp_lt_gt_false; eauto. -(* ge *) - rewrite Float.cmp_ge_gt_eq. - destruct (Float.cmp Ceq n1 n2) eqn:EQ; - destruct (Float.cmp Clt n1 n2) eqn:LT; - destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. +- (* ge *) + rewrite (Float.cmp_negate FCge), Float.cmp_ge_gt_eq. + destruct (Float.cmp FCeq n1 n2) eqn:EQ; + destruct (Float.cmp FClt n1 n2) eqn:LT; + destruct (Float.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float.cmp_lt_eq_false; eauto. exfalso; eapply Float.cmp_lt_eq_false; eauto. exfalso; eapply Float.cmp_lt_gt_false; eauto. @@ -905,10 +888,10 @@ Qed. Lemma compare_float32_spec: forall rs f1 f2, let rs1 := nextinstr (compare_float32 rs (Vsingle f1) (Vsingle f2)) in - rs1#CN = Val.of_bool (Float32.cmp Clt f1 f2) - /\ rs1#CZ = Val.of_bool (Float32.cmp Ceq f1 f2) - /\ rs1#CC = Val.of_bool (negb (Float32.cmp Clt f1 f2)) - /\ rs1#CV = Val.of_bool (negb (Float32.cmp Ceq f1 f2 || Float32.cmp Clt f1 f2 || Float32.cmp Cgt f1 f2)). + rs1#CN = Val.of_bool (Float32.cmp FClt f1 f2) + /\ rs1#CZ = Val.of_bool (Float32.cmp FCeq f1 f2) + /\ rs1#CC = Val.of_bool (negb (Float32.cmp FClt f1 f2)) + /\ rs1#CV = Val.of_bool (negb (Float32.cmp FCeq f1 f2 || Float32.cmp FClt f1 f2 || Float32.cmp FCgt f1 f2)). Proof. intros. intuition. Qed. @@ -944,65 +927,48 @@ Proof. intros [A [B [C D]]]. unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. destruct c; simpl. -(* eq *) - destruct (Float32.cmp Ceq n1 n2); auto. -(* ne *) - rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq n1 n2); auto. -(* lt *) - destruct (Float32.cmp Clt n1 n2); auto. -(* le *) +- (* eq *) + destruct (Float32.cmp FCeq n1 n2); auto. +- (* ne *) + rewrite Float32.cmp_ne_eq. destruct (Float32.cmp FCeq n1 n2); auto. +- (* lt *) + destruct (Float32.cmp FClt n1 n2); auto. +- (* le *) rewrite Float32.cmp_le_lt_eq. - destruct (Float32.cmp Clt n1 n2); destruct (Float32.cmp Ceq n1 n2); auto. -(* gt *) - destruct (Float32.cmp Ceq n1 n2) eqn:EQ; - destruct (Float32.cmp Clt n1 n2) eqn:LT; - destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. + destruct (Float32.cmp FClt n1 n2); destruct (Float32.cmp FCeq n1 n2); auto. +- (* gt *) + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; + destruct (Float32.cmp FClt n1 n2) eqn:LT; + destruct (Float32.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. exfalso; eapply Float32.cmp_gt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. -(* ge *) +- (* ge *) rewrite Float32.cmp_ge_gt_eq. - destruct (Float32.cmp Ceq n1 n2) eqn:EQ; - destruct (Float32.cmp Clt n1 n2) eqn:LT; - destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; + destruct (Float32.cmp FClt n1 n2) eqn:LT; + destruct (Float32.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float32.cmp_lt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. -Qed. - -Lemma cond_for_float32_not_cmp_correct: - forall c n1 n2 rs, - eval_testcond (cond_for_float_not_cmp c) - (nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2)))= - Some(negb(Float32.cmp c n1 n2)). -Proof. - intros. - generalize (compare_float32_spec rs n1 n2). - set (rs' := nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2))). - intros [A [B [C D]]]. - unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. - destruct c; simpl. -(* eq *) - destruct (Float32.cmp Ceq n1 n2); auto. -(* ne *) - rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq n1 n2); auto. -(* lt *) - destruct (Float32.cmp Clt n1 n2); auto. -(* le *) - rewrite Float32.cmp_le_lt_eq. - destruct (Float32.cmp Clt n1 n2) eqn:LT; destruct (Float32.cmp Ceq n1 n2) eqn:EQ; auto. -(* gt *) - destruct (Float32.cmp Ceq n1 n2) eqn:EQ; - destruct (Float32.cmp Clt n1 n2) eqn:LT; - destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. +- (* lt *) + rewrite (Float32.cmp_negate FClt). destruct (Float32.cmp FClt n1 n2); auto. +- (* le *) + rewrite (Float32.cmp_negate FCle), Float32.cmp_le_lt_eq. + destruct (Float32.cmp FClt n1 n2) eqn:LT; destruct (Float32.cmp FCeq n1 n2) eqn:EQ; auto. +- (* gt *) + rewrite (Float32.cmp_negate FCgt). + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; + destruct (Float32.cmp FClt n1 n2) eqn:LT; + destruct (Float32.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. exfalso; eapply Float32.cmp_gt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. -(* ge *) - rewrite Float32.cmp_ge_gt_eq. - destruct (Float32.cmp Ceq n1 n2) eqn:EQ; - destruct (Float32.cmp Clt n1 n2) eqn:LT; - destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. +- (* ge *) + rewrite (Float32.cmp_negate FCge), Float32.cmp_ge_gt_eq. + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; + destruct (Float32.cmp FClt n1 n2) eqn:LT; + destruct (Float32.cmp FCgt n1 n2) eqn:GT; auto. exfalso; eapply Float32.cmp_lt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. @@ -1029,8 +995,7 @@ Lemma transl_cond_correct: exec_straight ge fn c rs m k rs' m /\ match eval_condition cond (map rs (map preg_of args)) m with | Some b => eval_testcond (cond_for_cond cond) rs' = Some b - /\ eval_testcond (cond_for_cond (negate_condition cond)) rs' = Some (negb b) - | None => True + | None => True end /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. @@ -1040,34 +1005,34 @@ Proof. econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:CMP; auto. - split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. + apply cond_for_signed_cmp_correct; auto. apply compare_int_inv. - (* Ccompu *) econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:CMP; auto. - split; apply cond_for_unsigned_cmp_correct; auto. rewrite Val.negate_cmpu_bool, CMP; auto. + apply cond_for_unsigned_cmp_correct; auto. apply compare_int_inv. - (* Ccompshift *) econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. rewrite transl_shift_correct. destruct (Val.cmp_bool c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. - split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. + apply cond_for_signed_cmp_correct; auto. apply compare_int_inv. - (* Ccompushift *) econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. rewrite transl_shift_correct. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. - split; apply cond_for_unsigned_cmp_correct; auto. rewrite Val.negate_cmpu_bool, CMP; auto. + apply cond_for_unsigned_cmp_correct; auto. apply compare_int_inv. - (* Ccompimm *) destruct (is_immed_arith i). econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. - split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. + apply cond_for_signed_cmp_correct; auto. apply compare_int_inv. destruct (is_immed_arith (Int.neg i)). econstructor. @@ -1082,14 +1047,14 @@ Proof. rewrite Q. rewrite R; eauto with asmgen. auto. split. rewrite <- R by (eauto with asmgen). destruct (Val.cmp_bool c0 (rs' x) (Vint i)) eqn:CMP; auto. - split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. + apply cond_for_signed_cmp_correct; auto. intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompuimm *) destruct (is_immed_arith i). econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:CMP; auto. - split; apply cond_for_unsigned_cmp_correct; auto. rewrite Val.negate_cmpu_bool, CMP; auto. + apply cond_for_unsigned_cmp_correct; auto. apply compare_int_inv. destruct (is_immed_arith (Int.neg i)). econstructor. @@ -1104,76 +1069,39 @@ Proof. rewrite Q. rewrite R; eauto with asmgen. auto. split. rewrite <- R by (eauto with asmgen). destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs' x) (Vint i)) eqn:CMP; auto. - split; apply cond_for_unsigned_cmp_correct; auto. rewrite Val.negate_cmpu_bool, CMP; auto. + apply cond_for_unsigned_cmp_correct; auto. intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompf *) econstructor. split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. - split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto. - destruct (rs x); try discriminate. destruct (rs x0); try discriminate. - simpl in CMP. inv CMP. - split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. - apply compare_float_inv. -- (* Cnotcompf *) - econstructor. - split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. - split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + split. destruct (Val.cmpf_bool f (rs x) (rs x0)) eqn:CMP; auto. destruct (rs x); try discriminate. destruct (rs x0); try discriminate. simpl in CMP. inv CMP. -Local Opaque compare_float. simpl. - split. apply cond_for_float_not_cmp_correct. rewrite negb_involutive. apply cond_for_float_cmp_correct. - exact I. + apply cond_for_float_cmp_correct. apply compare_float_inv. - (* Ccompfzero *) econstructor. split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. - split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto. + split. destruct (Val.cmpf_bool f (rs x) (Vfloat Float.zero)) eqn:CMP; auto. destruct (rs x); try discriminate. simpl in CMP. inv CMP. - split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. - apply compare_float_inv. -- (* Cnotcompfzero *) - econstructor. - split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. - split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto. - destruct (rs x); try discriminate. simpl in CMP. inv CMP. -Local Opaque compare_float. simpl. - split. apply cond_for_float_not_cmp_correct. rewrite negb_involutive. apply cond_for_float_cmp_correct. - exact I. + apply cond_for_float_cmp_correct. apply compare_float_inv. - (* Ccompfs *) econstructor. split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. - split. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) eqn:CMP; auto. - destruct (rs x); try discriminate. destruct (rs x0); try discriminate. - simpl in CMP. inv CMP. - split. apply cond_for_float32_cmp_correct. apply cond_for_float32_not_cmp_correct. - apply compare_float32_inv. -- (* Cnotcompfs *) - econstructor. - split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. - split. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + split. destruct (Val.cmpfs_bool f (rs x) (rs x0)) eqn:CMP; auto. destruct (rs x); try discriminate. destruct (rs x0); try discriminate. simpl in CMP. inv CMP. -Local Opaque compare_float32. simpl. - split. apply cond_for_float32_not_cmp_correct. rewrite negb_involutive. apply cond_for_float32_cmp_correct. - exact I. + apply cond_for_float32_cmp_correct. apply compare_float32_inv. - (* Ccompfszero *) econstructor. split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. - split. destruct (Val.cmpfs_bool c0 (rs x) (Vsingle Float32.zero)) eqn:CMP; auto. + split. destruct (Val.cmpfs_bool f (rs x) (Vsingle Float32.zero)) eqn:CMP; auto. destruct (rs x); try discriminate. simpl in CMP. inv CMP. - split. apply cond_for_float32_cmp_correct. apply cond_for_float32_not_cmp_correct. - apply compare_float32_inv. -- (* Cnotcompfzero *) - econstructor. - split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. - split. destruct (Val.cmpfs_bool c0 (rs x) (Vsingle Float32.zero)) eqn:CMP; auto. - destruct (rs x); try discriminate. simpl in CMP. inv CMP. - simpl. split. apply cond_for_float32_not_cmp_correct. rewrite negb_involutive. apply cond_for_float32_cmp_correct. - exact I. + apply cond_for_float32_cmp_correct. apply compare_float32_inv. Qed. @@ -1367,7 +1295,7 @@ Proof. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. - destruct B as [B1 B2]; rewrite B1. destruct b; auto. + rewrite B; destruct b; auto. Qed. (** Translation of loads and stores. *) diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index d62240ef..5bd173a7 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -68,36 +68,20 @@ Nondetfunction cond_strength_reduction (Ccompuimm c (eval_static_shift s n2), r1 :: nil) | Ccompf c, r1 :: r2 :: nil, F n1 :: v2 :: nil => if Float.eq_dec n1 Float.zero - then (Ccompfzero (swap_comparison c), r2 :: nil) + then (Ccompfzero (swap_fp_comparison c), r2 :: nil) else (cond, args) | Ccompf c, r1 :: r2 :: nil, v1 :: F n2 :: nil => if Float.eq_dec n2 Float.zero then (Ccompfzero c, r1 :: nil) else (cond, args) - | Cnotcompf c, r1 :: r2 :: nil, F n1 :: v2 :: nil => - if Float.eq_dec n1 Float.zero - then (Cnotcompfzero (swap_comparison c), r2 :: nil) - else (cond, args) - | Cnotcompf c, r1 :: r2 :: nil, v1 :: F n2 :: nil => - if Float.eq_dec n2 Float.zero - then (Cnotcompfzero c, r1 :: nil) - else (cond, args) | Ccompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil => if Float32.eq_dec n1 Float32.zero - then (Ccompfszero (swap_comparison c), r2 :: nil) + then (Ccompfszero (swap_fp_comparison c), r2 :: nil) else (cond, args) | Ccompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil => if Float32.eq_dec n2 Float32.zero then (Ccompfszero c, r1 :: nil) else (cond, args) - | Cnotcompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil => - if Float32.eq_dec n1 Float32.zero - then (Cnotcompfszero (swap_comparison c), r2 :: nil) - else (cond, args) - | Cnotcompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil => - if Float32.eq_dec n2 Float32.zero - then (Cnotcompfszero c, r1 :: nil) - else (cond, args) | _, _, _ => (cond, args) end. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 079ba2be..5fc908db 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -145,24 +145,12 @@ Proof. - destruct (Float.eq_dec n2 Float.zero). subst n2. simpl. auto. simpl. rewrite H1; auto. -- destruct (Float.eq_dec n1 Float.zero). - subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto. - simpl. rewrite H1; auto. -- destruct (Float.eq_dec n2 Float.zero); simpl; auto. - subst n2; auto. - rewrite H1; auto. - destruct (Float32.eq_dec n1 Float32.zero). subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float32.cmp_swap. auto. simpl. rewrite H1; auto. - destruct (Float32.eq_dec n2 Float32.zero). subst n2. simpl. auto. simpl. rewrite H1; auto. -- destruct (Float32.eq_dec n1 Float32.zero). - subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float32.cmp_swap. auto. - simpl. rewrite H1; auto. -- destruct (Float32.eq_dec n2 Float32.zero); simpl; auto. - subst n2; auto. - rewrite H1; auto. - auto. Qed. @@ -58,14 +58,10 @@ Inductive condition : Type := | Ccompushift: comparison -> shift -> condition (**r unsigned integer comparison *) | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *) | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *) - | Ccompf: comparison -> condition (**r 64-bit floating-point comparison *) - | Cnotcompf: comparison -> condition (**r negation of a floating-point comparison *) - | Ccompfzero: comparison -> condition (**r floating-point comparison with 0.0 *) - | Cnotcompfzero: comparison -> condition (**r negation of a floating-point comparison with 0.0 *) - | Ccompfs: comparison -> condition (**r 32-bit floating-point comparison *) - | Cnotcompfs: comparison -> condition (**r negation of a floating-point comparison *) - | Ccompfszero: comparison -> condition (**r floating-point comparison with 0.0 *) - | Cnotcompfszero: comparison -> condition. (**r negation of a floating-point comparison with 0.0 *) + | Ccompf: fp_comparison -> condition (**r 64-bit floating-point comparison *) + | Ccompfzero: fp_comparison -> condition (**r floating-point comparison with 0.0 *) + | Ccompfs: fp_comparison -> condition (**r 32-bit floating-point comparison *) + | Ccompfszero: fp_comparison -> condition. (**r floating-point comparison with 0.0 *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -167,7 +163,8 @@ Defined. Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. generalize Int.eq_dec; intro. - assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + assert (forall (x y: comparison), {x=y}+{x<>y}) by decide equality. + assert (forall (x y: fp_comparison), {x=y}+{x<>y}) by decide equality. generalize eq_shift; intro. decide equality. Defined. @@ -215,13 +212,9 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): | Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n) | Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n) | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfzero c, v1 :: nil => Val.cmpf_bool c v1 (Vfloat Float.zero) - | Cnotcompfzero c, v1 :: nil => option_map negb (Val.cmpf_bool c v1 (Vfloat Float.zero)) | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) | Ccompfszero c, v1 :: nil => Val.cmpfs_bool c v1 (Vsingle Float32.zero) - | Cnotcompfszero c, v1 :: nil => option_map negb (Val.cmpfs_bool c v1 (Vsingle Float32.zero)) | _, _ => None end. @@ -343,13 +336,9 @@ Definition type_of_condition (c: condition) : list typ := | Ccompimm _ _ => Tint :: nil | Ccompuimm _ _ => Tint :: nil | Ccompf _ => Tfloat :: Tfloat :: nil - | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfzero _ => Tfloat :: nil - | Cnotcompfzero _ => Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil - | Cnotcompfs _ => Tsingle :: Tsingle :: nil | Ccompfszero _ => Tsingle :: nil - | Cnotcompfszero _ => Tsingle :: nil end. Definition type_of_operation (op: operation) : list typ * typ := @@ -568,14 +557,10 @@ Definition negate_condition (cond: condition): condition := | Ccompushift c s => Ccompushift (negate_comparison c) s | Ccompimm c n => Ccompimm (negate_comparison c) n | Ccompuimm c n => Ccompuimm (negate_comparison c) n - | Ccompf c => Cnotcompf c - | Cnotcompf c => Ccompf c - | Ccompfzero c => Cnotcompfzero c - | Cnotcompfzero c => Ccompfzero c - | Ccompfs c => Cnotcompfs c - | Cnotcompfs c => Ccompfs c - | Ccompfszero c => Cnotcompfszero c - | Cnotcompfszero c => Ccompfszero c + | Ccompf c => Ccompf (negate_fp_comparison c) + | Ccompfzero c => Ccompfzero (negate_fp_comparison c) + | Ccompfs c => Ccompfs (negate_fp_comparison c) + | Ccompfszero c => Ccompfszero (negate_fp_comparison c) end. Lemma eval_negate_condition: @@ -589,14 +574,10 @@ Proof. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. repeat (destruct vl; auto). apply Val.negate_cmp_bool. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpf_bool c v (Vfloat Float.zero)); auto. destruct b; auto. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0); auto. destruct b; auto. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v (Vsingle Float32.zero)); auto. destruct b; auto. + repeat (destruct vl; auto). apply Val.negate_cmpf_bool. + repeat (destruct vl; auto). apply Val.negate_cmpf_bool. + repeat (destruct vl; auto). apply Val.negate_cmpfs_bool. + repeat (destruct vl; auto). apply Val.negate_cmpfs_bool. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) @@ -820,12 +801,8 @@ Proof. eauto 4 using Val.cmp_bool_inject. eauto 4 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; simpl in H0; inv H0; auto. inv H3; simpl in H0; inv H0; auto. inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; simpl in H0; inv H0; auto. inv H3; simpl in H0; inv H0; auto. Qed. diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 642fff80..eeaf3723 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -14,17 +14,9 @@ open Printf open Camlcoq -open Integers +open PrintAST open Op -let comparison_name = function - | Ceq -> "==" - | Cne -> "!=" - | Clt -> "<" - | Cle -> "<=" - | Cgt -> ">" - | Cge -> ">=" - let shift pp = function | Slsl a -> fprintf pp "<< %ld" (camlint_of_coqint a) | Slsr a -> fprintf pp ">>u %ld" (camlint_of_coqint a) @@ -45,21 +37,13 @@ let print_condition reg pp = function | (Ccompuimm(c, n), [r1]) -> fprintf pp "%a %su %ld" reg r1 (comparison_name c) (camlint_of_coqint n) | (Ccompf c, [r1;r2]) -> - fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompf c, [r1;r2]) -> - fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sf %a" reg r1 (fp_comparison_name c) reg r2 | (Ccompfzero c, [r1]) -> - fprintf pp "%a %sf 0.0" reg r1 (comparison_name c) - | (Cnotcompfzero c, [r1]) -> - fprintf pp "%a not(%sf) 0.0" reg r1 (comparison_name c) + fprintf pp "%a %sf 0.0" reg r1 (fp_comparison_name c) | (Ccompfs c, [r1;r2]) -> - fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompfs c, [r1;r2]) -> - fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sfs %a" reg r1 (fp_comparison_name c) reg r2 | (Ccompfszero c, [r1]) -> - fprintf pp "%a %sfs 0.0" reg r1 (comparison_name c) - | (Cnotcompfszero c, [r1]) -> - fprintf pp "%a not(%sfs) 0.0" reg r1 (comparison_name c) + fprintf pp "%a %sfs 0.0" reg r1 (fp_comparison_name c) | _ -> fprintf pp "<bad condition>" diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index c361df65..89a54edd 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -376,10 +376,10 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) end. -Definition compf (c: comparison) (e1: expr) (e2: expr) := +Definition compf (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -Definition compfs (c: comparison) (e1: expr) (e2: expr) := +Definition compfs (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). (** ** Integer conversions *) diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index e19ddd6d..42c7cca9 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -41,13 +41,9 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n) | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n) | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfzero c, v1 :: nil => cmpf_bool c v1 (F Float.zero) - | Cnotcompfzero c, v1 :: nil => cnot (cmpf_bool c v1 (F Float.zero)) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) | Ccompfszero c, v1 :: nil => cmpfs_bool c v1 (FS Float32.zero) - | Cnotcompfszero c, v1 :: nil => cnot (cmpfs_bool c v1 (FS Float32.zero)) | _, _ => Bnone end. diff --git a/backend/Cminor.v b/backend/Cminor.v index 11941da3..02df60e9 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -113,8 +113,8 @@ Inductive binary_operation : Type := | Oshrlu: binary_operation (**r long right unsigned shift *) | Ocmp: comparison -> binary_operation (**r integer signed comparison *) | Ocmpu: comparison -> binary_operation (**r integer unsigned comparison *) - | Ocmpf: comparison -> binary_operation (**r float64 comparison *) - | Ocmpfs: comparison -> binary_operation (**r float32 comparison *) + | Ocmpf: fp_comparison -> binary_operation (**r float64 comparison *) + | Ocmpfs: fp_comparison -> binary_operation (**r float32 comparison *) | Ocmpl: comparison -> binary_operation (**r long signed comparison *) | Ocmplu: comparison -> binary_operation. (**r long unsigned comparison *) diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index f68c1267..b1172924 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -17,7 +17,6 @@ open Format open Camlcoq -open Integers open AST open PrintAST open Cminor @@ -80,14 +79,6 @@ let name_of_unop = function | Osingleoflong -> "singleoflong" | Osingleoflongu -> "singleoflongu" -let comparison_name = function - | Ceq -> "==" - | Cne -> "!=" - | Clt -> "<" - | Cle -> "<=" - | Cgt -> ">" - | Cge -> ">=" - let name_of_binop = function | Oadd -> "+" | Osub -> "-" @@ -125,8 +116,8 @@ let name_of_binop = function | Oshrlu -> ">>lu" | Ocmp c -> comparison_name c | Ocmpu c -> comparison_name c ^ "u" - | Ocmpf c -> comparison_name c ^ "f" - | Ocmpfs c -> comparison_name c ^ "s" + | Ocmpf c -> fp_comparison_name c ^ "f" + | Ocmpfs c -> fp_comparison_name c ^ "s" | Ocmpl c -> comparison_name c ^ "l" | Ocmplu c -> comparison_name c ^ "lu" diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index e7e44e29..518cbc6e 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2744,7 +2744,7 @@ Proof. - constructor. Qed. -Definition cmpf_bool (c: comparison) (v w: aval) : abool := +Definition cmpf_bool (c: fp_comparison) (v w: aval) : abool := match v, w with | F f1, F f2 => Just (Float.cmp c f1 f2) | _, _ => Btop @@ -2756,7 +2756,7 @@ Proof. intros. inv H; try constructor; inv H0; constructor. Qed. -Definition cmpfs_bool (c: comparison) (v w: aval) : abool := +Definition cmpfs_bool (c: fp_comparison) (v w: aval) : abool := match v, w with | FS f1, FS f2 => Just (Float32.cmp c f1 f2) | _, _ => Btop diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index c395a2cb..cd9d5f02 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -304,13 +304,13 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := | cast_case_f2bool => match v with | Vfloat f => - Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one)) + Some(Vint(if Float.cmp FCeq f Float.zero then Int.zero else Int.one)) | _ => None end | cast_case_s2bool => match v with | Vsingle f => - Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one)) + Some(Vint(if Float32.cmp FCeq f Float32.zero then Int.zero else Int.one)) | _ => None end | cast_case_l2l => @@ -421,12 +421,12 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool := end | bool_case_f => match v with - | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero)) + | Vfloat f => Some (negb (Float.cmp FCeq f Float.zero)) | _ => None end | bool_case_s => match v with - | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero)) + | Vsingle f => Some (negb (Float32.cmp FCeq f Float32.zero)) | _ => None end | bool_default => None @@ -937,7 +937,7 @@ Definition cmp_ptr (m: mem) (c: comparison) (v1 v2: val): option val := then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2). -Definition sem_cmp (c:comparison) +Definition sem_cmp (c:comparison) (fc: fp_comparison) (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val := match classify_cmp t1 t2 with @@ -990,9 +990,9 @@ Definition sem_cmp (c:comparison) (fun sg n1 n2 => Some(Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end))) (fun n1 n2 => - Some(Val.of_bool(Float.cmp c n1 n2))) + Some(Val.of_bool(Float.cmp fc n1 n2))) (fun n1 n2 => - Some(Val.of_bool(Float32.cmp c n1 n2))) + Some(Val.of_bool(Float32.cmp fc n1 n2))) v1 t1 v2 t2 m end. @@ -1060,12 +1060,12 @@ Definition sem_binary_operation | Oxor => sem_xor v1 t1 v2 t2 m | Oshl => sem_shl v1 t1 v2 t2 | Oshr => sem_shr v1 t1 v2 t2 - | Oeq => sem_cmp Ceq v1 t1 v2 t2 m - | One => sem_cmp Cne v1 t1 v2 t2 m - | Olt => sem_cmp Clt v1 t1 v2 t2 m - | Ogt => sem_cmp Cgt v1 t1 v2 t2 m - | Ole => sem_cmp Cle v1 t1 v2 t2 m - | Oge => sem_cmp Cge v1 t1 v2 t2 m + | Oeq => sem_cmp Ceq FCeq v1 t1 v2 t2 m + | One => sem_cmp Cne FCne v1 t1 v2 t2 m + | Olt => sem_cmp Clt FClt v1 t1 v2 t2 m + | Ogt => sem_cmp Cgt FCgt v1 t1 v2 t2 m + | Ole => sem_cmp Cle FCle v1 t1 v2 t2 m + | Oge => sem_cmp Cge FCge v1 t1 v2 t2 m end. Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) (m: mem) := @@ -1257,11 +1257,11 @@ Proof. Qed. Remark sem_cmp_inj: - forall cmp v1 tv1 ty1 v2 tv2 ty2 v, - sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> + forall cmp fcmp v1 tv1 ty1 v2 tv2 ty2 v, + sem_cmp cmp fcmp v1 ty1 v2 ty2 m = Some v -> Val.inject f v1 tv1 -> Val.inject f v2 tv2 -> - exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. + exists tv, sem_cmp cmp fcmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. intros. unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). @@ -1447,9 +1447,9 @@ Lemma cast_bool_bool_val: destruct f; auto. destruct f; auto. destruct f; auto. - destruct (Float.cmp Ceq f0 Float.zero); auto. + destruct (Float.cmp FCeq f0 Float.zero); auto. destruct f; auto. - destruct (Float32.cmp Ceq f0 Float32.zero); auto. + destruct (Float32.cmp FCeq f0 Float32.zero); auto. destruct f; auto. destruct ptr64; auto. destruct (Int.eq i Int.zero); auto. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 792a73f9..aee7f0ff 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -165,8 +165,8 @@ Definition make_cast (from to: type) (e: expr) := | cast_case_f2l si2 => OK (make_longoffloat e si2) | cast_case_s2l si2 => OK (make_longofsingle e si2) | cast_case_i2bool => OK (make_cmpu_ne_zero e) - | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)) - | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)) + | cast_case_f2bool => OK (Ebinop (Ocmpf FCne) e (make_floatconst Float.zero)) + | cast_case_s2bool => OK (Ebinop (Ocmpfs FCne) e (make_singleconst Float32.zero)) | cast_case_l2bool => OK (Ebinop (Ocmplu Cne) e (make_longconst Int64.zero)) | cast_case_struct id1 id2 => OK e | cast_case_union id1 id2 => OK e @@ -180,8 +180,8 @@ Definition make_cast (from to: type) (e: expr) := Definition make_boolean (e: expr) (ty: type) := match classify_bool ty with | bool_case_i => make_cmpu_ne_zero e - | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero) - | bool_case_s => Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero) + | bool_case_f => Ebinop (Ocmpf FCne) e (make_floatconst Float.zero) + | bool_case_s => Ebinop (Ocmpfs FCne) e (make_singleconst Float32.zero) | bool_case_l => Ebinop (Ocmplu Cne) e (make_longconst Int64.zero) | bool_default => e (**r should not happen *) end. @@ -191,8 +191,8 @@ Definition make_boolean (e: expr) (ty: type) := Definition make_notbool (e: expr) (ty: type) := match classify_bool ty with | bool_case_i => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero)) - | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero)) - | bool_case_s => OK (Ebinop (Ocmpfs Ceq) e (make_singleconst Float32.zero)) + | bool_case_f => OK (Ebinop (Ocmpf FCeq) e (make_floatconst Float.zero)) + | bool_case_s => OK (Ebinop (Ocmpfs FCeq) e (make_singleconst Float32.zero)) | bool_case_l => OK (Ebinop (Ocmplu Ceq) e (make_longconst Int64.zero)) | bool_default => Error (msg "Cshmgen.make_notbool") end. @@ -354,7 +354,8 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) := Definition make_cmp_ptr (c: comparison) (e1 e2: expr) := Ebinop (if Archi.ptr64 then Ocmplu c else Ocmpu c) e1 e2. -Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := +Definition make_cmp (c: comparison) (fc: fp_comparison) + (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_cmp ty1 ty2 with | cmp_case_pp => OK (make_cmp_ptr c e1 e2) | cmp_case_pi si => @@ -367,7 +368,7 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type OK (make_cmp_ptr c (if Archi.ptr64 then e1 else Eunop Ointoflong e1) e2) | cmp_default => make_binarith - (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpfs c) (Ocmpl c) (Ocmplu c) + (Ocmp c) (Ocmpu c) (Ocmpf fc) (Ocmpfs fc) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2 end. @@ -430,12 +431,12 @@ Definition transl_binop (ce: composite_env) | Cop.Oxor => make_xor a ta b tb | Cop.Oshl => make_shl a ta b tb | Cop.Oshr => make_shr a ta b tb - | Cop.Oeq => make_cmp Ceq a ta b tb - | Cop.One => make_cmp Cne a ta b tb - | Cop.Olt => make_cmp Clt a ta b tb - | Cop.Ogt => make_cmp Cgt a ta b tb - | Cop.Ole => make_cmp Cle a ta b tb - | Cop.Oge => make_cmp Cge a ta b tb + | Cop.Oeq => make_cmp Ceq FCeq a ta b tb + | Cop.One => make_cmp Cne FCne a ta b tb + | Cop.Olt => make_cmp Clt FClt a ta b tb + | Cop.Ogt => make_cmp Cgt FCgt a ta b tb + | Cop.Ole => make_cmp Cle FCle a ta b tb + | Cop.Oge => make_cmp Cge FCge a ta b tb end. (** ** Translation of field accesses *) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 09e31cb2..71fd952f 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -423,11 +423,11 @@ Proof. - (* float -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. - destruct (Float.cmp Ceq f Float.zero); auto. + destruct (Float.cmp FCeq f Float.zero); auto. - (* single -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq. - destruct (Float32.cmp Ceq f Float32.zero); auto. + destruct (Float32.cmp FCeq f Float32.zero); auto. - (* struct *) destruct (ident_eq id1 id2); inv H1; auto. - (* union *) @@ -460,11 +460,11 @@ Proof. - (* float *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. - destruct (Float.cmp Cne f Float.zero); constructor. + destruct (Float.cmp FCne f Float.zero); constructor. - (* single *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. - destruct (Float32.cmp Cne f Float32.zero); constructor. + destruct (Float32.cmp FCne f Float32.zero); constructor. Qed. Lemma make_neg_correct: @@ -514,9 +514,9 @@ Proof. econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto. - econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. - destruct (Float.cmp Ceq f Float.zero); auto. + destruct (Float.cmp FCeq f Float.zero); auto. - econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. - destruct (Float32.cmp Ceq f Float32.zero); auto. + destruct (Float32.cmp FCeq f Float32.zero); auto. Qed. Lemma make_notint_correct: @@ -887,7 +887,8 @@ Proof. apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr. Qed. -Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp). +Lemma make_cmp_correct: forall cmp fcmp, + binary_constructor_correct (make_cmp cmp fcmp) (sem_cmp cmp fcmp). Proof. red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_cmp tya tyb). diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index ba1d34fb..87d299ca 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1461,9 +1461,9 @@ Proof. Qed. Lemma pres_sem_cmp: - forall ty1 ty2 msg ty c v1 v2 m v, + forall ty1 ty2 msg ty c fc v1 v2 m v, comparison_type ty1 ty2 msg = OK ty -> - sem_cmp c v1 ty1 v2 ty2 m = Some v -> + sem_cmp c fc v1 ty1 v2 ty2 m = Some v -> wt_val v ty. Proof with (try discriminate). unfold comparison_type, sem_cmp; intros. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e477957a..6e115a14 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -18,6 +18,8 @@ open Printf open Camlcoq open AST +open Integers +open Floats let name_of_type = function | Tint -> "int" @@ -90,3 +92,22 @@ let rec print_builtin_res px oc = function fprintf oc "splitlong(%a, %a)" (print_builtin_res px) hi (print_builtin_res px) lo +let comparison_name = function + | Ceq -> "==" + | Cne -> "!=" + | Clt -> "<" + | Cle -> "<=" + | Cgt -> ">" + | Cge -> ">=" + +let fp_comparison_name = function + | FCeq -> "==" + | FCne -> "!=" + | FClt -> "<" + | FCle -> "<=" + | FCgt -> ">" + | FCge -> ">=" + | FCnotlt -> "!<" + | FCnotle -> "!<=" + | FCnotgt -> "!>" + | FCnotge -> "!>=" diff --git a/common/Values.v b/common/Values.v index a20dd567..6a1ffd26 100644 --- a/common/Values.v +++ b/common/Values.v @@ -815,13 +815,13 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := | _, _ => None end. -Definition cmpf_bool (c: comparison) (v1 v2: val): option bool := +Definition cmpf_bool (c: fp_comparison) (v1 v2: val): option bool := match v1, v2 with | Vfloat f1, Vfloat f2 => Some (Float.cmp c f1 f2) | _, _ => None end. -Definition cmpfs_bool (c: comparison) (v1 v2: val): option bool := +Definition cmpfs_bool (c: fp_comparison) (v1 v2: val): option bool := match v1, v2 with | Vsingle f1, Vsingle f2 => Some (Float32.cmp c f1 f2) | _, _ => None @@ -870,10 +870,10 @@ Definition cmp (c: comparison) (v1 v2: val): val := Definition cmpu (c: comparison) (v1 v2: val): val := of_optbool (cmpu_bool c v1 v2). -Definition cmpf (c: comparison) (v1 v2: val): val := +Definition cmpf (c: fp_comparison) (v1 v2: val): val := of_optbool (cmpf_bool c v1 v2). -Definition cmpfs (c: comparison) (v1 v2: val): val := +Definition cmpfs (c: fp_comparison) (v1 v2: val): val := of_optbool (cmpfs_bool c v1 v2). Definition cmpl (c: comparison) (v1 v2: val): option val := @@ -1672,6 +1672,20 @@ Proof. - rewrite Int64.negate_cmpu. auto. Qed. +Theorem negate_cmpf_bool: + forall c v1 v2, cmpf_bool (negate_fp_comparison c) v1 v2 = option_map negb (cmpf_bool c v1 v2). +Proof. + intros; unfold cmpf; destruct v1; auto; destruct v2; auto. + simpl. rewrite Float.cmp_negate. auto. +Qed. + +Theorem negate_cmpfs_bool: + forall c v1 v2, cmpfs_bool (negate_fp_comparison c) v1 v2 = option_map negb (cmpfs_bool c v1 v2). +Proof. + intros; unfold cmpf; destruct v1; auto; destruct v2; auto. + simpl. rewrite Float32.cmp_negate. auto. +Qed. + Lemma not_of_optbool: forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob). Proof. @@ -1693,6 +1707,18 @@ Proof. intros. unfold cmpu. rewrite negate_cmpu_bool. apply not_of_optbool. Qed. +Theorem negate_cmpf: + forall c v1 v2, cmpf (negate_fp_comparison c) v1 v2 = notbool (cmpf c v1 v2). +Proof. + intros; unfold cmpf. rewrite negate_cmpf_bool. apply not_of_optbool. +Qed. + +Theorem negate_cmpfs: + forall c v1 v2, cmpfs (negate_fp_comparison c) v1 v2 = notbool (cmpfs c v1 v2). +Proof. + intros; unfold cmpfs. rewrite negate_cmpfs_bool. apply not_of_optbool. +Qed. + Theorem swap_cmp_bool: forall c x y, cmp_bool (swap_comparison c) x y = cmp_bool c y x. @@ -1749,33 +1775,31 @@ Proof. Qed. Theorem negate_cmpf_eq: - forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2. + forall v1 v2, notbool (cmpf FCne v1 v2) = cmpf FCeq v1 v2. Proof. - destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. - rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto. + intros; symmetry; apply (negate_cmpf FCne). Qed. Theorem negate_cmpf_ne: - forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2. + forall v1 v2, notbool (cmpf FCeq v1 v2) = cmpf FCne v1 v2. Proof. - destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. - rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto. + intros; symmetry; apply (negate_cmpf FCeq). Qed. Theorem cmpf_le: - forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2). + forall v1 v2, cmpf FCle v1 v2 = or (cmpf FClt v1 v2) (cmpf FCeq v1 v2). Proof. destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. rewrite Float.cmp_le_lt_eq. - destruct (Float.cmp Clt f f0); destruct (Float.cmp Ceq f f0); auto. + destruct (Float.cmp FClt f f0); destruct (Float.cmp FCeq f f0); auto. Qed. Theorem cmpf_ge: - forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2). + forall v1 v2, cmpf FCge v1 v2 = or (cmpf FCgt v1 v2) (cmpf FCeq v1 v2). Proof. destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. rewrite Float.cmp_ge_gt_eq. - destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto. + destruct (Float.cmp FCgt f f0); destruct (Float.cmp FCeq f f0); auto. Qed. Theorem cmp_ne_0_optbool: diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v index c9e7bad5..ba01193d 100644 --- a/lib/BoolEqual.v +++ b/lib/BoolEqual.v @@ -161,7 +161,7 @@ Ltac boolean_equality := BE.bool_eq. (** Given a function [beq] of type [t -> t -> bool] produced by [boolean_equality], the [decidable_equality_from beq] produces a decidable equality with type - [forall (x y: t], {x=y}+{x<>y}. *) + [forall (x y: t), {x=y}+{x<>y}. *) Ltac decidable_equality_from beq := apply (BE.dec_eq_from_bool_eq _ beq); [abstract BE.bool_eq_refl|abstract BE.bool_eq_sound]. diff --git a/lib/Floats.v b/lib/Floats.v index ba225be1..6a84c3be 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -32,20 +32,68 @@ Definition float32 := binary32. (**r the type of IEE754 single-precision FP numb (** Boolean-valued comparisons *) -Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : bool := +Inductive fp_comparison : Type := + | FCeq (**r same *) + | FCne (**r different *) + | FClt (**r less than *) + | FCle (**r less than or equal *) + | FCgt (**r greater than *) + | FCge (**r greater than or equal *) + | FCnotlt (**r no less than *) + | FCnotle (**r no less than or equal *) + | FCnotgt (**r no greater than *) + | FCnotge. (**r no greater than or equal *) + +Definition negate_fp_comparison (c: fp_comparison): fp_comparison := match c with - | Ceq => + | FCeq => FCne + | FCne => FCeq + | FClt => FCnotlt + | FCle => FCnotle + | FCgt => FCnotgt + | FCge => FCnotge + | FCnotlt => FClt + | FCnotle => FCle + | FCnotgt => FCgt + | FCnotge => FCge + end. + +Definition swap_fp_comparison (c: fp_comparison): fp_comparison := + match c with + | FCeq => FCeq + | FCne => FCne + | FClt => FCgt + | FCle => FCge + | FCgt => FClt + | FCge => FCle + | FCnotlt => FCnotgt + | FCnotle => FCnotge + | FCnotgt => FCnotlt + | FCnotge => FCnotle + end. + +Definition cmp_of_comparison (c: fp_comparison) (x: option Datatypes.comparison) : bool := + match c with + | FCeq => match x with Some Eq => true | _ => false end - | Cne => + | FCne => match x with Some Eq => false | _ => true end - | Clt => + | FClt => match x with Some Lt => true | _ => false end - | Cle => + | FCle => match x with Some(Lt|Eq) => true | _ => false end - | Cgt => + | FCgt => match x with Some Gt => true | _ => false end - | Cge => + | FCge => match x with Some(Gt|Eq) => true | _ => false end + | FCnotlt => + match x with Some Lt => false | _ => true end + | FCnotle => + match x with Some(Lt|Eq) => false | _ => true end + | FCnotgt => + match x with Some Gt => false | _ => true end + | FCnotge => + match x with Some(Gt|Eq) => false | _ => true end end. Definition ordered_of_comparison (x: option Datatypes.comparison) : bool := @@ -53,44 +101,45 @@ Definition ordered_of_comparison (x: option Datatypes.comparison) : bool := Lemma cmp_of_comparison_swap: forall c x, - cmp_of_comparison (swap_comparison c) x = + cmp_of_comparison (swap_fp_comparison c) x = cmp_of_comparison c (match x with None => None | Some x => Some (CompOpp x) end). Proof. intros. destruct c; destruct x as [[]|]; reflexivity. Qed. -Lemma cmp_of_comparison_ne_eq: - forall x, cmp_of_comparison Cne x = negb (cmp_of_comparison Ceq x). +Lemma cmp_of_comparison_negate: + forall c x, + cmp_of_comparison (negate_fp_comparison c) x = negb (cmp_of_comparison c x). Proof. - intros. destruct x as [[]|]; reflexivity. + intros. destruct c; destruct x as [[]|]; reflexivity. Qed. Lemma cmp_of_comparison_lt_eq_false: - forall x, cmp_of_comparison Clt x = true -> cmp_of_comparison Ceq x = true -> False. + forall x, cmp_of_comparison FClt x = true -> cmp_of_comparison FCeq x = true -> False. Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. Lemma cmp_of_comparison_le_lt_eq: - forall x, cmp_of_comparison Cle x = cmp_of_comparison Clt x || cmp_of_comparison Ceq x. + forall x, cmp_of_comparison FCle x = cmp_of_comparison FClt x || cmp_of_comparison FCeq x. Proof. destruct x as [[]|]; reflexivity. Qed. Lemma cmp_of_comparison_gt_eq_false: - forall x, cmp_of_comparison Cgt x = true -> cmp_of_comparison Ceq x = true -> False. + forall x, cmp_of_comparison FCgt x = true -> cmp_of_comparison FCeq x = true -> False. Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. Lemma cmp_of_comparison_ge_gt_eq: - forall x, cmp_of_comparison Cge x = cmp_of_comparison Cgt x || cmp_of_comparison Ceq x. + forall x, cmp_of_comparison FCge x = cmp_of_comparison FCgt x || cmp_of_comparison FCeq x. Proof. destruct x as [[]|]; reflexivity. Qed. Lemma cmp_of_comparison_lt_gt_false: - forall x, cmp_of_comparison Clt x = true -> cmp_of_comparison Cgt x = true -> False. + forall x, cmp_of_comparison FClt x = true -> cmp_of_comparison FCgt x = true -> False. Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. @@ -222,7 +271,7 @@ Definition div: float -> float -> float := Bdiv 53 1024 __ __ binop_pl mode_NE. (**r division *) 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 *) +Definition cmp (c: fp_comparison) (f1 f2: float) : bool := (**r comparison *) cmp_of_comparison c (compare f1 f2). Definition ordered (f1 f2: float) : bool := ordered_of_comparison (compare f1 f2). @@ -327,44 +376,50 @@ Qed. (** Properties of comparisons. *) Theorem cmp_swap: - forall c x y, cmp (swap_comparison c) x y = cmp c y x. + forall c x y, cmp (swap_fp_comparison c) x y = cmp c y x. Proof. unfold cmp, compare; intros. rewrite (Bcompare_swap _ _ x y). apply cmp_of_comparison_swap. Qed. +Theorem cmp_negate: + forall c x y, cmp (negate_fp_comparison c) x y = negb (cmp c x y). +Proof. + unfold cmp; intros. apply cmp_of_comparison_negate. +Qed. + Theorem cmp_ne_eq: - forall f1 f2, cmp Cne f1 f2 = negb (cmp Ceq f1 f2). + forall f1 f2, cmp FCne f1 f2 = negb (cmp FCeq f1 f2). Proof. - intros; apply cmp_of_comparison_ne_eq. + intros; apply (cmp_of_comparison_negate FCeq). Qed. Theorem cmp_lt_eq_false: - forall f1 f2, cmp Clt f1 f2 = true -> cmp Ceq f1 f2 = true -> False. + forall f1 f2, cmp FClt f1 f2 = true -> cmp FCeq f1 f2 = true -> False. Proof. intros f1 f2; apply cmp_of_comparison_lt_eq_false. Qed. Theorem cmp_le_lt_eq: - forall f1 f2, cmp Cle f1 f2 = cmp Clt f1 f2 || cmp Ceq f1 f2. + forall f1 f2, cmp FCle f1 f2 = cmp FClt f1 f2 || cmp FCeq f1 f2. Proof. intros f1 f2; apply cmp_of_comparison_le_lt_eq. Qed. Theorem cmp_gt_eq_false: - forall x y, cmp Cgt x y = true -> cmp Ceq x y = true -> False. + forall x y, cmp FCgt x y = true -> cmp FCeq x y = true -> False. Proof. intros f1 f2; apply cmp_of_comparison_gt_eq_false. Qed. Theorem cmp_ge_gt_eq: - forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2. + forall f1 f2, cmp FCge f1 f2 = cmp FCgt f1 f2 || cmp FCeq f1 f2. Proof. intros f1 f2; apply cmp_of_comparison_ge_gt_eq. Qed. Theorem cmp_lt_gt_false: - forall f1 f2, cmp Clt f1 f2 = true -> cmp Cgt f1 f2 = true -> False. + forall f1 f2, cmp FClt f1 f2 = true -> cmp FCgt f1 f2 = true -> False. Proof. intros f1 f2; apply cmp_of_comparison_lt_gt_false. Qed. @@ -427,7 +482,7 @@ Qed. Theorem to_intu_to_int_1: forall x n, - cmp Clt x (of_intu ox8000_0000) = true -> + cmp FClt x (of_intu ox8000_0000) = true -> to_intu x = Some n -> to_int x = Some n. Proof. @@ -457,7 +512,7 @@ Qed. Theorem to_intu_to_int_2: forall x n, - cmp Clt x (of_intu ox8000_0000) = false -> + cmp FClt x (of_intu ox8000_0000) = false -> to_intu x = Some n -> to_int (sub x (of_intu ox8000_0000)) = Some (Int.sub n ox8000_0000). Proof. @@ -958,7 +1013,7 @@ 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 *) +Definition cmp (c: fp_comparison) (f1 f2: float32) : bool := (**r comparison *) cmp_of_comparison c (compare f1 f2). Definition ordered (f1 f2: float32) : bool := ordered_of_comparison (compare f1 f2). @@ -1043,44 +1098,50 @@ Qed. (** Properties of comparisons. *) Theorem cmp_swap: - forall c x y, cmp (swap_comparison c) x y = cmp c y x. + forall c x y, cmp (swap_fp_comparison c) x y = cmp c y x. Proof. unfold cmp, compare; intros. rewrite (Bcompare_swap _ _ x y). apply cmp_of_comparison_swap. Qed. +Theorem cmp_negate: + forall c x y, cmp (negate_fp_comparison c) x y = negb (cmp c x y). +Proof. + unfold cmp; intros. apply cmp_of_comparison_negate. +Qed. + Theorem cmp_ne_eq: - forall f1 f2, cmp Cne f1 f2 = negb (cmp Ceq f1 f2). + forall f1 f2, cmp FCne f1 f2 = negb (cmp FCeq f1 f2). Proof. - intros; apply cmp_of_comparison_ne_eq. + intros; apply (cmp_of_comparison_negate FCeq). Qed. Theorem cmp_lt_eq_false: - forall f1 f2, cmp Clt f1 f2 = true -> cmp Ceq f1 f2 = true -> False. + forall f1 f2, cmp FClt f1 f2 = true -> cmp FCeq f1 f2 = true -> False. Proof. intros f1 f2; apply cmp_of_comparison_lt_eq_false. Qed. Theorem cmp_le_lt_eq: - forall f1 f2, cmp Cle f1 f2 = cmp Clt f1 f2 || cmp Ceq f1 f2. + forall f1 f2, cmp FCle f1 f2 = cmp FClt f1 f2 || cmp FCeq f1 f2. Proof. intros f1 f2; apply cmp_of_comparison_le_lt_eq. Qed. Theorem cmp_gt_eq_false: - forall x y, cmp Cgt x y = true -> cmp Ceq x y = true -> False. + forall x y, cmp FCgt x y = true -> cmp FCeq x y = true -> False. Proof. intros f1 f2; apply cmp_of_comparison_gt_eq_false. Qed. Theorem cmp_ge_gt_eq: - forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2. + forall f1 f2, cmp FCge f1 f2 = cmp FCgt f1 f2 || cmp FCeq f1 f2. Proof. intros f1 f2; apply cmp_of_comparison_ge_gt_eq. Qed. Theorem cmp_lt_gt_false: - forall f1 f2, cmp Clt f1 f2 = true -> cmp Cgt f1 f2 = true -> False. + forall f1 f2, cmp FClt f1 f2 = true -> cmp FCgt f1 f2 = true -> False. Proof. intros f1 f2; apply cmp_of_comparison_lt_gt_false. Qed. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index ad24f563..cbcb261a 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -661,9 +661,9 @@ Definition compare_ulong (rs: regset) (m: mem) (v1 v2: val) := #CR0_3 <- Vundef. Definition compare_float (rs: regset) (v1 v2: val) := - rs#CR0_0 <- (Val.cmpf Clt v1 v2) - #CR0_1 <- (Val.cmpf Cgt v1 v2) - #CR0_2 <- (Val.cmpf Ceq v1 v2) + rs#CR0_0 <- (Val.cmpf FClt v1 v2) + #CR0_1 <- (Val.cmpf FCgt v1 v2) + #CR0_2 <- (Val.cmpf FCeq v1 v2) #CR0_3 <- Vundef. (** Execution of a single instruction [i] in initial state diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 8c296f0a..37bef464 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -213,11 +213,11 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : synthesized by a [cror] instruction that computes the logical ``or'' of the corresponding two conditions. *) -Definition floatcomp (cmp: comparison) (r1 r2: freg) (k: code) := +Definition floatcomp (cmp: fp_comparison) (r1 r2: freg) (k: code) := Pfcmpu r1 r2 :: match cmp with - | Cle => Pcror CRbit_3 CRbit_2 CRbit_0 :: k - | Cge => Pcror CRbit_3 CRbit_2 CRbit_1 :: k + | FCle | FCnotle => Pcror CRbit_3 CRbit_2 CRbit_0 :: k + | FCge | FCnotge => Pcror CRbit_3 CRbit_2 CRbit_1 :: k | _ => k end. @@ -247,8 +247,6 @@ Definition transl_cond OK (loadimm GPR0 n (Pcmplw r1 GPR0 :: k)) | Ccompf cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k) - | Cnotcompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 k) | Cmaskzero n, a1 :: nil => do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k) | Cmasknotzero n, a1 :: nil => @@ -292,14 +290,18 @@ Definition crbit_for_icmp (cmp: comparison) := | Cge => (CRbit_0, false) end. -Definition crbit_for_fcmp (cmp: comparison) := +Definition crbit_for_fcmp (cmp: fp_comparison) := match cmp with - | Ceq => (CRbit_2, true) - | Cne => (CRbit_2, false) - | Clt => (CRbit_0, true) - | Cle => (CRbit_3, true) - | Cgt => (CRbit_1, true) - | Cge => (CRbit_3, true) + | FCeq => (CRbit_2, true) + | FCne => (CRbit_2, false) + | FClt => (CRbit_0, true) + | FCle => (CRbit_3, true) + | FCgt => (CRbit_1, true) + | FCge => (CRbit_3, true) + | FCnotlt => (CRbit_0, false) + | FCnotle => (CRbit_3, false) + | FCnotgt => (CRbit_1, false) + | FCnotge => (CRbit_3, false) end. Definition crbit_for_cond (cond: condition) := @@ -309,7 +311,6 @@ Definition crbit_for_cond (cond: condition) := | Ccompimm cmp n => crbit_for_icmp cmp | Ccompuimm cmp n => crbit_for_icmp cmp | Ccompf cmp => crbit_for_fcmp cmp - | Cnotcompf cmp => let p := crbit_for_fcmp cmp in (fst p, negb (snd p)) | Cmaskzero n => (CRbit_2, true) | Cmasknotzero n => (CRbit_2, false) | Ccompl cmp => crbit_for_icmp cmp diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index c18757b2..153b6f17 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -250,9 +250,9 @@ Variable fn: function. Lemma compare_float_spec: forall rs v1 v2, let rs1 := nextinstr (compare_float rs v1 v2) in - rs1#CR0_0 = Val.cmpf Clt v1 v2 - /\ rs1#CR0_1 = Val.cmpf Cgt v1 v2 - /\ rs1#CR0_2 = Val.cmpf Ceq v1 v2 + rs1#CR0_0 = Val.cmpf FClt v1 v2 + /\ rs1#CR0_1 = Val.cmpf FCgt v1 v2 + /\ rs1#CR0_2 = Val.cmpf FCeq v1 v2 /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. Proof. intros. unfold rs1. @@ -836,32 +836,30 @@ Proof. generalize (compare_float_spec rs rs#r1 rs#r2). intros [A [B [C D]]]. set (rs1 := nextinstr (compare_float rs rs#r1 rs#r2)) in *. - assert ((cmp = Ceq \/ cmp = Cne \/ cmp = Clt \/ cmp = Cgt) - \/ (cmp = Cle \/ cmp = Cge)). - case cmp; tauto. - unfold floatcomp. elim H; intro; clear H. + assert (E: (cmp = FCeq \/ cmp = FCne \/ cmp = FClt \/ cmp = FCgt \/ cmp = FCnotlt \/ cmp = FCnotgt) + \/ (cmp = FCle \/ cmp = FCge \/ cmp = FCnotle \/ cmp = FCnotge)) + by (destruct cmp; tauto). + unfold floatcomp. destruct E as [E|E]. +- (* one instr *) exists rs1. - split. destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; - apply exec_straight_one; reflexivity. - split. - destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. - rewrite Val.negate_cmpf_eq. auto. + split. decompose [or] E; subst cmp; apply exec_straight_one; reflexivity. + split. decompose [or] E; subst cmp; simpl; auto; rewrite <- Val.negate_cmpf; auto. auto. - (* two instrs *) - exists (nextinstr (rs1#CR0_3 <- (Val.cmpf cmp rs#r1 rs#r2))). - split. elim H0; intro; subst cmp. - apply exec_straight_two with rs1 m. - reflexivity. simpl. - rewrite C; rewrite A. rewrite Val.or_commut. rewrite <- Val.cmpf_le. - reflexivity. reflexivity. reflexivity. - apply exec_straight_two with rs1 m. - reflexivity. simpl. - rewrite C; rewrite B. rewrite Val.or_commut. rewrite <- Val.cmpf_ge. - reflexivity. reflexivity. reflexivity. - split. elim H0; intro; subst cmp; simpl. - reflexivity. - reflexivity. - intros. Simpl. +- (* two instrs *) + exists (nextinstr (rs1#CR0_3 <- (if snd (crbit_for_fcmp cmp) + then Val.cmpf cmp rs#r1 rs#r2 + else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)))). + split. ++ apply exec_straight_step with rs1 m. reflexivity. reflexivity. + decompose [or] E; subst cmp; apply exec_straight_one; auto; simpl; rewrite ?A, ?B, ?C. +* rewrite Val.or_commut, <- Val.cmpf_le. auto. +* rewrite Val.or_commut, <- Val.cmpf_ge. auto. +* rewrite Val.or_commut, <- Val.cmpf_le, <- Val.negate_cmpf. auto. +* rewrite Val.or_commut, <- Val.cmpf_ge, <- Val.negate_cmpf. auto. ++ split. +* replace (reg_of_crbit (fst (crbit_for_fcmp cmp))) with CR0_3. reflexivity. + decompose [or] E; subst cmp; reflexivity. +* intros; Simpl. Qed. (** Translation of conditions. *) @@ -894,7 +892,7 @@ Proof. intros. Opaque Int.eq. unfold transl_cond in H; destruct cond; ArgsInv; simpl. - (* Ccomp *) +- (* Ccomp *) fold (Val.cmp c0 (rs x) (rs x0)). destruct (compare_sint_spec rs (rs x) (rs x0)) as [A [B [C D]]]. econstructor; split. @@ -902,7 +900,7 @@ Opaque Int.eq. split. case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. auto with asmgen. - (* Ccompu *) +- (* Ccompu *) fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (rs x0)). destruct (compare_uint_spec rs m (rs x) (rs x0)) as [A [B [C D]]]. econstructor; split. @@ -910,7 +908,7 @@ Opaque Int.eq. split. case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. auto with asmgen. - (* Ccompimm *) +- (* Ccompimm *) fold (Val.cmp c0 (rs x) (Vint i)). destruct (Int.eq (high_s i) Int.zero); inv EQ0. destruct (compare_sint_spec rs (rs x) (Vint i)) as [A [B [C D]]]. @@ -929,7 +927,7 @@ Opaque Int.eq. split. rewrite SAME. case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. intros. rewrite SAME; rewrite D; auto with asmgen. - (* Ccompuimm *) +- (* Ccompuimm *) fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (Vint i)). destruct (Int.eq (high_u i) Int.zero); inv EQ0. destruct (compare_uint_spec rs m (rs x) (Vint i)) as [A [B [C D]]]. @@ -948,26 +946,19 @@ Opaque Int.eq. split. rewrite SAME. case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. intros. rewrite SAME; rewrite D; auto with asmgen. - (* Ccompf *) - fold (Val.cmpf c0 (rs x) (rs x0)). - destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. +- (* Ccompf *) + fold (Val.cmpf f (rs x) (rs x0)). + destruct (floatcomp_correct f x x0 k rs m) as [rs' [EX [RES OTH]]]. exists rs'. split. auto. split. apply RES. auto with asmgen. - (* Cnotcompf *) - rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. - fold (Val.cmpf c0 (rs x) (rs x0)). - destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto. - auto with asmgen. - (* Cmaskzero *) +- (* Cmaskzero *) destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. eauto with asmgen. exists rs'. split. assumption. split. rewrite C. destruct (rs x); auto. auto with asmgen. - (* Cmasknotzero *) +- (* Cmasknotzero *) destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. eauto with asmgen. exists rs'. split. assumption. diff --git a/powerpc/Op.v b/powerpc/Op.v index e6f942c1..214f5d23 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -43,8 +43,7 @@ Inductive condition : Type := | Ccompu: comparison -> condition (**r unsigned integer comparison *) | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *) | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *) - | Ccompf: comparison -> condition (**r floating-point comparison *) - | Cnotcompf: comparison -> condition (**r negation of a floating-point comparison *) + | Ccompf: fp_comparison -> condition (**r floating-point comparison *) | Cmaskzero: int -> condition (**r test [(arg & constant) == 0] *) | Cmasknotzero: int -> condition (**r test [(arg & constant) != 0] *) (*c PPC64 specific conditions: *) @@ -168,7 +167,8 @@ Inductive addressing: Type := Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. generalize Int.eq_dec Int64.eq_dec; intro. - assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + assert (forall (x y: comparison), {x=y}+{x<>y}) by decide equality. + assert (forall (x y: fp_comparison), {x=y}+{x<>y}) by decide equality. decide equality. Defined. @@ -203,7 +203,6 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n) | Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n) | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n | Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n) | Ccompl c, v1 :: v2 :: nil => Val.cmpl_bool c v1 v2 @@ -356,7 +355,6 @@ Definition type_of_condition (c: condition) : list typ := | Ccompimm _ _ => Tint :: nil | Ccompuimm _ _ => Tint :: nil | Ccompf _ => Tfloat :: Tfloat :: nil - | Cnotcompf _ => Tfloat :: Tfloat :: nil | Cmaskzero _ => Tint :: nil | Cmasknotzero _ => Tint :: nil | Ccompl _ => Tlong :: Tlong :: nil @@ -611,8 +609,7 @@ Definition negate_condition (cond: condition): condition := | Ccompu c => Ccompu(negate_comparison c) | Ccompimm c n => Ccompimm (negate_comparison c) n | Ccompuimm c n => Ccompuimm (negate_comparison c) n - | Ccompf c => Cnotcompf c - | Cnotcompf c => Ccompf c + | Ccompf c => Ccompf (negate_fp_comparison c) | Cmaskzero n => Cmasknotzero n | Cmasknotzero n => Cmaskzero n | Ccompl c => Ccompl(negate_comparison c) @@ -630,9 +627,8 @@ Proof. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. repeat (destruct vl; auto). apply Val.negate_cmp_bool. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. - repeat (destruct vl; auto). + repeat (destruct vl; auto). apply Val.negate_cmpf_bool. + repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.maskzero_bool v i) as [[]|]; auto. repeat (destruct vl; auto). apply Val.negate_cmpl_bool. repeat (destruct vl; auto). apply Val.negate_cmplu_bool. @@ -867,7 +863,6 @@ Proof. inv H3; simpl in H0; inv H0; auto. eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; try discriminate; auto. inv H3; try discriminate; auto. inv H3; inv H2; simpl in H0; inv H0; auto. diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index cffaafdb..db6b9657 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -14,17 +14,9 @@ open Printf open Camlcoq -open Integers +open PrintAST open Op -let comparison_name = function - | Ceq -> "==" - | Cne -> "!=" - | Clt -> "<" - | Cle -> "<=" - | Cgt -> ">" - | Cge -> ">=" - let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2 @@ -35,9 +27,7 @@ let print_condition reg pp = function | (Ccompuimm(c, n), [r1]) -> fprintf pp "%a %su %ld" reg r1 (comparison_name c) (camlint_of_coqint n) | (Ccompf c, [r1;r2]) -> - fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompf c, [r1;r2]) -> - fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sf %a" reg r1 (fp_comparison_name c) reg r2 | (Cmaskzero n, [r1]) -> fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n) | (Cmasknotzero n, [r1]) -> diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index d2ca408a..39a300db 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -439,10 +439,10 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) end. -Definition compf (c: comparison) (e1: expr) (e2: expr) := +Definition compf (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -Definition compfs (c: comparison) (e1: expr) (e2: expr) := +Definition compfs (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (Eop Ofloatofsingle (e1 ::: Enil) ::: Eop Ofloatofsingle (e2 ::: Enil) ::: Enil). @@ -474,7 +474,7 @@ Definition intuoffloat (e: expr) := else Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf FClt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 5f87d9b9..24b6e42e 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -867,9 +867,9 @@ Proof. constructor. auto. econstructor. eauto. econstructor. instantiate (1 := Vfloat fm). EvalOp. - eapply eval_Econdition with (va := Float.cmp Clt f fm). + eapply eval_Econdition with (va := Float.cmp FClt f fm). eauto with evalexpr. - destruct (Float.cmp Clt f fm) eqn:?. + destruct (Float.cmp FClt f fm) eqn:?. exploit Float.to_intu_to_int_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. exploit Float.to_intu_to_int_2; eauto. diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index f7f65e9e..5993fee9 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -31,7 +31,6 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n) | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n) | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Cmaskzero n, v1 :: nil => maskzero v1 n | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n) | Ccompl c, v1 :: v2 :: nil => cmpl_bool c v1 v2 diff --git a/riscV/Asm.v b/riscV/Asm.v index 1d8fda11..6674b8be 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -842,11 +842,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfdivs d s1 s2 => Next (nextinstr (rs#d <- (Val.divfs rs#s1 rs#s2))) m | Pfeqs d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpfs Ceq rs#s1 rs#s2))) m + Next (nextinstr (rs#d <- (Val.cmpfs FCeq rs#s1 rs#s2))) m | Pflts d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpfs Clt rs#s1 rs#s2))) m + Next (nextinstr (rs#d <- (Val.cmpfs FClt rs#s1 rs#s2))) m | Pfles d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpfs Cle rs#s1 rs#s2))) m + Next (nextinstr (rs#d <- (Val.cmpfs FCle rs#s1 rs#s2))) m | Pfcvtws d s => Next (nextinstr (rs#d <- (Val.maketotal (Val.intofsingle rs#s)))) m @@ -890,11 +890,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfdivd d s1 s2 => Next (nextinstr (rs#d <- (Val.divf rs#s1 rs#s2))) m | Pfeqd d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpf Ceq rs#s1 rs#s2))) m + Next (nextinstr (rs#d <- (Val.cmpf FCeq rs#s1 rs#s2))) m | Pfltd d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpf Clt rs#s1 rs#s2))) m + Next (nextinstr (rs#d <- (Val.cmpf FClt rs#s1 rs#s2))) m | Pfled d s1 s2 => - Next (nextinstr (rs#d <- (Val.cmpf Cle rs#s1 rs#s2))) m + Next (nextinstr (rs#d <- (Val.cmpf FCle rs#s1 rs#s2))) m | Pfcvtwd d s => Next (nextinstr (rs#d <- (Val.maketotal (Val.intoffloat rs#s)))) m diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..be34cc21 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -183,24 +183,32 @@ Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) : | Cge => Pbgeul r1 r2 lbl end. -Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := +Definition transl_cond_float (cmp: fp_comparison) (rd: ireg) (fs1 fs2: freg) := match cmp with - | Ceq => (Pfeqd rd fs1 fs2, true) - | Cne => (Pfeqd rd fs1 fs2, false) - | Clt => (Pfltd rd fs1 fs2, true) - | Cle => (Pfled rd fs1 fs2, true) - | Cgt => (Pfltd rd fs2 fs1, true) - | Cge => (Pfled rd fs2 fs1, true) + | FCeq => (Pfeqd rd fs1 fs2, true) + | FCne => (Pfeqd rd fs1 fs2, false) + | FClt => (Pfltd rd fs1 fs2, true) + | FCle => (Pfled rd fs1 fs2, true) + | FCgt => (Pfltd rd fs2 fs1, true) + | FCge => (Pfled rd fs2 fs1, true) + | FCnotlt => (Pfltd rd fs1 fs2, false) + | FCnotle => (Pfled rd fs1 fs2, false) + | FCnotgt => (Pfltd rd fs2 fs1, false) + | FCnotge => (Pfled rd fs2 fs1, false) end. -Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := +Definition transl_cond_single (cmp: fp_comparison) (rd: ireg) (fs1 fs2: freg) := match cmp with - | Ceq => (Pfeqs rd fs1 fs2, true) - | Cne => (Pfeqs rd fs1 fs2, false) - | Clt => (Pflts rd fs1 fs2, true) - | Cle => (Pfles rd fs1 fs2, true) - | Cgt => (Pflts rd fs2 fs1, true) - | Cge => (Pfles rd fs2 fs1, true) + | FCeq => (Pfeqs rd fs1 fs2, true) + | FCne => (Pfeqs rd fs1 fs2, false) + | FClt => (Pflts rd fs1 fs2, true) + | FCle => (Pfles rd fs1 fs2, true) + | FCgt => (Pflts rd fs2 fs1, true) + | FCge => (Pfles rd fs2 fs1, true) + | FCnotlt => (Pflts rd fs1 fs2, false) + | FCnotle => (Pfles rd fs1 fs2, false) + | FCnotgt => (Pflts rd fs2 fs1, false) + | FCnotge => (Pfles rd fs2 fs1, false) end. Definition transl_cbranch @@ -246,18 +254,10 @@ Definition transl_cbranch do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_float c X31 r1 r2 in OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) | Ccompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_single c X31 r1 r2 in OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) | _, _ => Error(msg "Asmgen.transl_cond_branch") end. @@ -373,18 +373,10 @@ Definition transl_cond_op do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_float c rd r1 r2 in OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) | Ccompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_single c rd r1 r2 in OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) | _, _ => Error(msg "Asmgen.transl_cond_op") end. diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 5ec57886..675efb25 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -203,12 +203,6 @@ Proof. - destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. destruct normal; TailNoLabel. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. - destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. destruct normal; TailNoLabel. @@ -258,12 +252,6 @@ Proof. - destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. destruct normal; TailNoLabel. -- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. - destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. destruct normal; TailNoLabel. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 7f070c12..4b413393 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -360,6 +360,12 @@ Proof. rewrite <- Float.cmp_swap. auto. - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. rewrite <- Float.cmp_swap. auto. +- rewrite <- Val.negate_cmpf. auto. +- rewrite <- Val.negate_cmpf. auto. +- rewrite <- Val.negate_cmpf. simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. + rewrite <- Float.cmp_swap. auto. +- rewrite <- Val.negate_cmpf. simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. + rewrite <- Float.cmp_swap. auto. Qed. Lemma transl_cond_single_correct: @@ -369,12 +375,17 @@ Lemma transl_cond_single_correct: exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. Proof. intros. destruct cmp; simpl in H; inv H; auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto. +- rewrite <- Val.negate_cmpfs. auto. - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. rewrite <- Float32.cmp_swap. auto. - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. rewrite <- Float32.cmp_swap. auto. +- rewrite <- Val.negate_cmpfs. auto. +- rewrite <- Val.negate_cmpfs. auto. +- rewrite <- Val.negate_cmpfs. simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. + rewrite <- Float32.cmp_swap. auto. +- rewrite <- Val.negate_cmpfs. simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. + rewrite <- Float32.cmp_swap. auto. Qed. Remark branch_on_X31: @@ -481,16 +492,6 @@ Proof. split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. intros; Simpl. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. - destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). assert (V: v = Val.of_bool (eqb normal b)). @@ -499,16 +500,6 @@ Proof. split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. Qed. Lemma transl_cbranch_correct_true: @@ -897,20 +888,6 @@ Proof. simpl; reflexivity. auto. auto. split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. + (* cmpfs *) destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. fold (Val.cmpfs c0 (rs x) (rs x0)). @@ -925,20 +902,6 @@ Proof. simpl; reflexivity. auto. auto. split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. Qed. (** Some arithmetic properties. *) @@ -46,10 +46,8 @@ Inductive condition : Type := | Ccomplu (c: comparison) (**r unsigned 64-bit integer comparison *) | Ccomplimm (c: comparison) (n: int64) (**r signed 64-bit integer comparison with a constant *) | Ccompluimm (c: comparison) (n: int64) (**r unsigned 64-bit integer comparison with a constant *) - | Ccompf (c: comparison) (**r 64-bit floating-point comparison *) - | Cnotcompf (c: comparison) (**r negation of a floating-point comparison *) - | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) - | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) + | Ccompf (c: fp_comparison) (**r 64-bit floating-point comparison *) + | Ccompfs (c: fp_comparison). (**r 32-bit floating-point comparison *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -167,7 +165,8 @@ Inductive addressing: Type := Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. generalize Int.eq_dec Int64.eq_dec; intro. - assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + assert (forall (x y: comparison), {x=y}+{x<>y}) by decide equality. + assert (forall (x y: fp_comparison), {x=y}+{x<>y}) by decide equality. decide equality. Defined. @@ -215,9 +214,7 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n) | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n) | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) | _, _ => None end. @@ -374,9 +371,7 @@ Definition type_of_condition (c: condition) : list typ := | Ccomplimm _ _ => Tlong :: nil | Ccompluimm _ _ => Tlong :: nil | Ccompf _ => Tfloat :: Tfloat :: nil - | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil - | Cnotcompfs _ => Tsingle :: Tsingle :: nil end. Definition type_of_operation (op: operation) : list typ * typ := @@ -704,10 +699,8 @@ Definition negate_condition (cond: condition): condition := | Ccomplu c => Ccomplu(negate_comparison c) | Ccomplimm c n => Ccomplimm (negate_comparison c) n | Ccompluimm c n => Ccompluimm (negate_comparison c) n - | Ccompf c => Cnotcompf c - | Cnotcompf c => Ccompf c - | Ccompfs c => Cnotcompfs c - | Cnotcompfs c => Ccompfs c + | Ccompf c => Ccompf (negate_fp_comparison c) + | Ccompfs c => Ccompfs (negate_fp_comparison c) end. Lemma eval_negate_condition: @@ -723,10 +716,8 @@ Proof. repeat (destruct vl; auto). apply Val.negate_cmplu_bool. repeat (destruct vl; auto). apply Val.negate_cmpl_bool. repeat (destruct vl; auto). apply Val.negate_cmplu_bool. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. + repeat (destruct vl; auto). apply Val.negate_cmpf_bool. + repeat (destruct vl; auto). apply Val.negate_cmpfs_bool. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) @@ -957,8 +948,6 @@ Proof. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. Qed. Ltac TrivialExists := diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 9ec474b3..fd1cf0ba 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -19,17 +19,9 @@ open Printf open Camlcoq -open Integers +open PrintAST open Op -let comparison_name = function - | Ceq -> "==" - | Cne -> "!=" - | Clt -> "<" - | Cle -> "<=" - | Cgt -> ">" - | Cge -> ">=" - let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2 @@ -39,8 +31,6 @@ let print_condition reg pp = function fprintf pp "%a %ss %ld" reg r1 (comparison_name c) (camlint_of_coqint n) | (Ccompuimm(c, n), [r1]) -> fprintf pp "%a %su %ld" reg r1 (comparison_name c) (camlint_of_coqint n) - | (Ccompf c, [r1;r2]) -> - fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 | (Ccompl c, [r1;r2]) -> fprintf pp "%a %sls %a" reg r1 (comparison_name c) reg r2 | (Ccomplu c, [r1;r2]) -> @@ -49,12 +39,10 @@ let print_condition reg pp = function fprintf pp "%a %sls %Ld" reg r1 (comparison_name c) (camlint64_of_coqint n) | (Ccompluimm(c, n), [r1]) -> fprintf pp "%a %slu %Lu" reg r1 (comparison_name c) (camlint64_of_coqint n) - | (Cnotcompf c, [r1;r2]) -> - fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + | (Ccompf c, [r1;r2]) -> + fprintf pp "%a %sf %a" reg r1 (fp_comparison_name c) reg r2 | (Ccompfs c, [r1;r2]) -> - fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompfs c, [r1;r2]) -> - fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sfs %a" reg r1 (fp_comparison_name c) reg r2 | _ -> fprintf pp "<bad condition>" diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index bb8af2ed..f49a6101 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -370,10 +370,10 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) end. -Definition compf (c: comparison) (e1: expr) (e2: expr) := +Definition compf (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -Definition compfs (c: comparison) (e1: expr) (e2: expr) := +Definition compfs (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). (** ** Integer conversions *) diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 5670b5fe..51cd1228 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -27,9 +27,7 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n) | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n) | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) | _, _ => Bnone end. @@ -451,8 +451,8 @@ 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 (Float.cmp Ceq x y || negb (Float.ordered x y))) - #CF <- (Val.of_bool (negb (Float.cmp Cge x y))) + rs #ZF <- (Val.of_bool (Float.cmp FCeq x y || negb (Float.ordered x y))) + #CF <- (Val.of_bool (negb (Float.cmp FCge x y))) #PF <- (Val.of_bool (negb (Float.ordered x y))) #SF <- Vundef #OF <- Vundef @@ -463,8 +463,8 @@ 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 (Float32.cmp Ceq x y || negb (Float32.ordered x y))) - #CF <- (Val.of_bool (negb (Float32.cmp Cge x y))) + rs #ZF <- (Val.of_bool (Float32.cmp FCeq x y || negb (Float32.ordered x y))) + #CF <- (Val.of_bool (negb (Float32.cmp FCge x y))) #PF <- (Val.of_bool (negb (Float32.ordered x y))) #SF <- Vundef #OF <- Vundef diff --git a/x86/Asmgen.v b/x86/Asmgen.v index dedbfbe6..700bbe2c 100644 --- a/x86/Asmgen.v +++ b/x86/Asmgen.v @@ -165,16 +165,16 @@ Definition normalize_addrmode_64 (a: addrmode) := (** Floating-point comparison. We swap the operands in some cases to simplify the handling of the unordered case. *) -Definition floatcomp (cmp: comparison) (r1 r2: freg) : instruction := +Definition floatcomp (cmp: fp_comparison) (r1 r2: freg) : instruction := match cmp with - | Clt | Cle => Pcomisd_ff r2 r1 - | Ceq | Cne | Cgt | Cge => Pcomisd_ff r1 r2 + | FClt | FCle | FCnotlt | FCnotle => Pcomisd_ff r2 r1 + | FCeq | FCne | FCgt | FCge | FCnotgt | FCnotge => Pcomisd_ff r1 r2 end. -Definition floatcomp32 (cmp: comparison) (r1 r2: freg) : instruction := +Definition floatcomp32 (cmp: fp_comparison) (r1 r2: freg) : instruction := match cmp with - | Clt | Cle => Pcomiss_ff r2 r1 - | Ceq | Cne | Cgt | Cge => Pcomiss_ff r1 r2 + | FClt | FCle | FCnotlt | FCnotle => Pcomiss_ff r2 r1 + | FCeq | FCne | FCgt | FCge | FCnotgt | FCnotge => Pcomiss_ff r1 r2 end. (** Translation of a condition. Prepends to [k] the instructions @@ -204,12 +204,8 @@ Definition transl_cond do r1 <- ireg_of a1; OK (Pcmpq_ri r1 n :: k) | Ccompf cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) - | Cnotcompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) | Ccompfs cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp32 cmp r1 r2 :: k) - | Cnotcompfs cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp32 cmp r1 r2 :: k) | Cmaskzero n, a1 :: nil => do r1 <- ireg_of a1; OK (Ptestl_ri r1 n :: k) | Cmasknotzero n, a1 :: nil => @@ -257,21 +253,16 @@ Definition testcond_for_condition (cond: condition) : extcond := | Ccompluimm c n => Cond_base(testcond_for_unsigned_comparison c) | Ccompf c | Ccompfs c => match c with - | Ceq => Cond_and Cond_np Cond_e - | Cne => Cond_or Cond_p Cond_ne - | Clt => Cond_base Cond_a - | Cle => Cond_base Cond_ae - | Cgt => Cond_base Cond_a - | Cge => Cond_base Cond_ae - end - | Cnotcompf c | Cnotcompfs c => - match c with - | Ceq => Cond_or Cond_p Cond_ne - | Cne => Cond_and Cond_np Cond_e - | Clt => Cond_base Cond_be - | Cle => Cond_base Cond_b - | Cgt => Cond_base Cond_be - | Cge => Cond_base Cond_b + | FCeq => Cond_and Cond_np Cond_e + | FCne => Cond_or Cond_p Cond_ne + | FClt => Cond_base Cond_a + | FCle => Cond_base Cond_ae + | FCgt => Cond_base Cond_a + | FCge => Cond_base Cond_ae + | FCnotlt => Cond_base Cond_be + | FCnotle => Cond_base Cond_b + | FCnotgt => Cond_base Cond_be + | FCnotge => Cond_base Cond_b end | Cmaskzero n => Cond_base Cond_e | Cmasknotzero n => Cond_base Cond_ne diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index 3aa87a4c..ab177167 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -205,8 +205,6 @@ Proof. destruct (Int64.eq_dec n Int64.zero); TailNoLabel. destruct c0; simpl; TailNoLabel. destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. Qed. Remark transl_op_label: diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index 904debdc..c638cdcf 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -700,8 +700,8 @@ 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 (Float.cmp Ceq n1 n2 || negb (Float.ordered n1 n2)) - /\ rs'#CF = Val.of_bool (negb (Float.cmp Cge n1 n2)) + rs'#ZF = Val.of_bool (Float.cmp FCeq n1 n2 || negb (Float.ordered n1 n2)) + /\ rs'#CF = Val.of_bool (negb (Float.cmp FCge n1 n2)) /\ rs'#PF = Val.of_bool (negb (Float.ordered n1 n2)) /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. @@ -715,8 +715,8 @@ 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 (Float32.cmp Ceq n1 n2 || negb (Float32.ordered n1 n2)) - /\ rs'#CF = Val.of_bool (negb (Float32.cmp Cge n1 n2)) + rs'#ZF = Val.of_bool (Float32.cmp FCeq n1 n2 || negb (Float32.ordered n1 n2)) + /\ rs'#CF = Val.of_bool (negb (Float32.cmp FCge n1 n2)) /\ rs'#PF = Val.of_bool (negb (Float32.ordered n1 n2)) /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. @@ -743,10 +743,10 @@ Definition eval_extcond (xc: extcond) (rs: regset) : option bool := end end. -Definition swap_floats {A: Type} (c: comparison) (n1 n2: A) : A := +Definition swap_floats {A: Type} (c: fp_comparison) (n1 n2: A) : A := match c with - | Clt | Cle => n2 - | Ceq | Cne | Cgt | Cge => n1 + | FClt | FCle | FCnotlt | FCnotle => n2 + | FCeq | FCne | FCgt | FCge | FCnotgt | FCnotge => n1 end. Lemma testcond_for_float_comparison_correct: @@ -778,38 +778,32 @@ Transparent Float.cmp Float.ordered. 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: - forall c n1 n2 rs, - eval_extcond (testcond_for_condition (Cnotcompf c)) - (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) - (Vfloat (swap_floats c n2 n1)) rs)) = - Some(negb(Float.cmp c n1 n2)). -Proof. - intros. - generalize (compare_floats_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)). - set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) - (Vfloat (swap_floats c n2 n1)) rs)). - intros [A [B [C D]]]. - unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. - destruct c; simpl. -- (* 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.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. +- (* notlt *) + replace (Float.cmp FCnotlt n1 n2) with (negb (Float.cmp FClt n1 n2)) by (symmetry; apply (Float.cmp_negate FClt)). + rewrite <- (Float.cmp_swap FCge n1 n2). + rewrite <- (Float.cmp_swap FCne n1 n2). + simpl. + rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq. + destruct (Float.cmp FClt n1 n2) eqn:LT; simpl. + destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float.cmp_lt_eq_false; eauto. + auto. + destruct (Float.cmp FCeq n1 n2); auto. +- (* notle *) + replace (Float.cmp FCnotle n1 n2) with (negb (Float.cmp FCle n1 n2)) by (symmetry; apply (Float.cmp_negate FCle)). + rewrite <- (Float.cmp_swap FCge n1 n2). simpl. + destruct (Float.cmp FCle n1 n2); auto. +- (* notgt *) + replace (Float.cmp FCnotgt n1 n2) with (negb (Float.cmp FCgt n1 n2)) by (symmetry; apply (Float.cmp_negate FCgt)). + rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. + destruct (Float.cmp FCgt n1 n2) eqn:GT; simpl. + destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float.cmp_gt_eq_false; eauto. + auto. + destruct (Float.cmp FCeq n1 n2); auto. +- (* notge *) + replace (Float.cmp FCnotge n1 n2) with (negb (Float.cmp FCge n1 n2)) by (symmetry; apply (Float.cmp_negate FCge)). + destruct (Float.cmp FCge n1 n2); auto. Opaque Float.cmp Float.ordered. Qed. @@ -823,7 +817,7 @@ Proof. intros. generalize (compare_floats32_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)). set (rs' := nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2)) - (Vsingle (swap_floats c n2 n1)) rs)). + (Vsingle (swap_floats c n2 n1)) rs)). intros [A [B [C D]]]. unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. @@ -874,9 +868,36 @@ Transparent Float32.cmp Float32.ordered. unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. - (* ge *) destruct (Float32.cmp Cge n1 n2); auto. +- (* notlt *) + replace (Float32.cmp FCnotlt n1 n2) with (negb (Float32.cmp FClt n1 n2)) by (symmetry; apply (Float32.cmp_negate FClt)). + rewrite <- (Float32.cmp_swap FCge n1 n2). + rewrite <- (Float32.cmp_swap FCne n1 n2). + simpl. + rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq. + destruct (Float32.cmp FClt n1 n2) eqn:LT; simpl. + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float32.cmp_lt_eq_false; eauto. + auto. + destruct (Float32.cmp FCeq n1 n2); auto. +- (* notle *) + replace (Float32.cmp FCnotle n1 n2) with (negb (Float32.cmp FCle n1 n2)) by (symmetry; apply (Float32.cmp_negate FCle)). + rewrite <- (Float32.cmp_swap FCge n1 n2). simpl. + destruct (Float32.cmp FCle n1 n2); auto. +- (* notgt *) + replace (Float32.cmp FCnotgt n1 n2) with (negb (Float32.cmp FCgt n1 n2)) by (symmetry; apply (Float32.cmp_negate FCgt)). + rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. + destruct (Float32.cmp FCgt n1 n2) eqn:GT; simpl. + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float32.cmp_gt_eq_false; eauto. + auto. + destruct (Float32.cmp FCeq n1 n2); auto. +- (* notge *) + replace (Float32.cmp FCnotge n1 n2) with (negb (Float32.cmp FCge n1 n2)) by (symmetry; apply (Float32.cmp_negate FCge)). + destruct (Float32.cmp FCge n1 n2); auto. Opaque Float32.cmp Float32.ordered. Qed. + Remark swap_floats_commut: forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y). Proof. @@ -983,15 +1004,6 @@ Proof. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct. intros. Simplifs. apply compare_floats_inv; auto with asmgen. -- (* notcompf *) - simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). - exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. - destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. - split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_neg_float_comparison_correct. - intros. Simplifs. apply compare_floats_inv; auto with asmgen. - (* compfs *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). @@ -1001,15 +1013,6 @@ Proof. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_float32_comparison_correct. intros. Simplifs. apply compare_floats32_inv; auto with asmgen. -- (* notcompfs *) - simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). - exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. - destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. - split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_neg_float32_comparison_correct. - intros. Simplifs. apply compare_floats32_inv; auto with asmgen. - (* maskzero *) simpl. rewrite (ireg_of_eq _ _ EQ). econstructor. split. apply exec_straight_one. simpl; eauto. auto. @@ -46,10 +46,8 @@ Inductive condition : Type := | Ccomplu (c: comparison) (**r unsigned 64-bit integer comparison *) | Ccomplimm (c: comparison) (n: int64) (**r signed 64-bit integer comparison with a constant *) | Ccompluimm (c: comparison) (n: int64) (**r unsigned 64-bit integer comparison with a constant *) - | Ccompf (c: comparison) (**r 64-bit floating-point comparison *) - | Cnotcompf (c: comparison) (**r negation of a floating-point comparison *) - | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) - | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) + | Ccompf (c: fp_comparison) (**r 64-bit floating-point comparison *) + | Ccompfs (c: fp_comparison) (**r 32-bit floating-point comparison *) | Cmaskzero (n: int) (**r test [(arg & constant) == 0] *) | Cmasknotzero (n: int). (**r test [(arg & constant) != 0] *) @@ -174,7 +172,8 @@ Inductive operation : Type := Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. generalize Int.eq_dec Int64.eq_dec; intro. - assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + assert (forall (x y: comparison), {x=y}+{x<>y}) by decide equality. + assert (forall (x y: fp_comparison), {x=y}+{x<>y}) by decide equality. decide equality. Defined. @@ -253,9 +252,7 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n) | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n) | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) | Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n | Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n) | _, _ => None @@ -461,9 +458,7 @@ Definition type_of_condition (c: condition) : list typ := | Ccomplimm _ _ => Tlong :: nil | Ccompluimm _ _ => Tlong :: nil | Ccompf _ => Tfloat :: Tfloat :: nil - | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil - | Cnotcompfs _ => Tsingle :: Tsingle :: nil | Cmaskzero _ => Tint :: nil | Cmasknotzero _ => Tint :: nil end. @@ -775,10 +770,8 @@ Definition negate_condition (cond: condition): condition := | Ccomplu c => Ccomplu(negate_comparison c) | Ccomplimm c n => Ccomplimm (negate_comparison c) n | Ccompluimm c n => Ccompluimm (negate_comparison c) n - | Ccompf c => Cnotcompf c - | Cnotcompf c => Ccompf c - | Ccompfs c => Cnotcompfs c - | Cnotcompfs c => Ccompfs c + | Ccompf c => Ccompf (negate_fp_comparison c) + | Ccompfs c => Ccompfs (negate_fp_comparison c) | Cmaskzero n => Cmasknotzero n | Cmasknotzero n => Cmaskzero n end. @@ -796,10 +789,8 @@ Proof. repeat (destruct vl; auto). apply Val.negate_cmplu_bool. repeat (destruct vl; auto). apply Val.negate_cmpl_bool. repeat (destruct vl; auto). apply Val.negate_cmplu_bool. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. + repeat (destruct vl; auto). apply Val.negate_cmpf_bool. + repeat (destruct vl; auto). apply Val.negate_cmpfs_bool. destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v n) as [[]|]; auto. Qed. @@ -1119,8 +1110,6 @@ Proof. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; try discriminate; auto. - inv H3; try discriminate; auto. Qed. diff --git a/x86/PrintOp.ml b/x86/PrintOp.ml index faa5bb5f..356b2027 100644 --- a/x86/PrintOp.ml +++ b/x86/PrintOp.ml @@ -14,17 +14,9 @@ open Printf open Camlcoq -open Integers +open PrintAST open Op -let comparison_name = function - | Ceq -> "==" - | Cne -> "!=" - | Clt -> "<" - | Cle -> "<=" - | Cgt -> ">" - | Cge -> ">=" - let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2 @@ -43,13 +35,9 @@ let print_condition reg pp = function | (Ccompluimm(c, n), [r1]) -> fprintf pp "%a %slu %Lu" reg r1 (comparison_name c) (camlint64_of_coqint n) | (Ccompf c, [r1;r2]) -> - fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompf c, [r1;r2]) -> - fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sf %a" reg r1 (fp_comparison_name c) reg r2 | (Ccompfs c, [r1;r2]) -> - fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompfs c, [r1;r2]) -> - fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sfs %a" reg r1 (fp_comparison_name c) reg r2 | (Cmaskzero n, [r1]) -> fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n) | (Cmasknotzero n, [r1]) -> diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index a1583600..a9985528 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -412,10 +412,10 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) end. -Definition compf (c: comparison) (e1: expr) (e2: expr) := +Definition compf (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -Definition compfs (c: comparison) (e1: expr) (e2: expr) := +Definition compfs (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). (** ** Integer conversions *) @@ -472,7 +472,7 @@ Nondetfunction floatofint (e: expr) := Definition intuoffloat (e: expr) := Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf FClt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index fdbadaa8..bfd5364c 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -816,9 +816,9 @@ Proof. constructor. auto. econstructor. eauto. econstructor. instantiate (1 := Vfloat fm). EvalOp. - eapply eval_Econdition with (va := Float.cmp Clt f fm). + eapply eval_Econdition with (va := Float.cmp FClt f fm). eauto with evalexpr. - destruct (Float.cmp Clt f fm) eqn:?. + destruct (Float.cmp FClt f fm) eqn:?. exploit Float.to_intu_to_int_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. exploit Float.to_intu_to_int_2; eauto. diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v index 1021a9c8..12a13499 100644 --- a/x86/ValueAOp.v +++ b/x86/ValueAOp.v @@ -27,9 +27,7 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n) | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n) | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) | Cmaskzero n, v1 :: nil => maskzero v1 n | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n) | _, _ => Bnone |