Support for fcmpzd instruction (float compare with +0.0)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1858 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8 files changed, 74 insertions, 6 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 5e16f05..58b2634 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -158,6 +158,7 @@ Inductive instruction : Type :=
   | Pfsubd: freg -> freg -> freg -> instruction     (**r float subtraction *)
   | Pflid: freg -> float -> instruction             (**r load float constant *)
   | Pfcmpd: freg -> freg -> instruction             (**r float comparison *)
+  | Pfcmpzd: freg -> instruction             (**r float comparison with 0.0 *)
   | Pfsitod: freg -> ireg -> instruction            (**r signed int to float *)
   | Pfuitod: freg -> ireg -> instruction            (**r unsigned int to float *)
   | Pftosizd: ireg -> freg -> instruction           (**r float to signed int *)
@@ -501,6 +502,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#r1 <- (Vfloat f))) m
   | Pfcmpd r1 r2 =>              
       OK (nextinstr (compare_float rs rs#r1 rs#r2)) m
+  | Pfcmpzd r1 =>              
+      OK (nextinstr (compare_float rs rs#r1 (Vfloat Float.zero))) m
   | Pfsitod r1 r2 =>
       OK (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofint rs#r2)))) m
   | Pfuitod r1 r2 =>
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index c727db9..7cf25f5 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -155,6 +155,10 @@ Definition transl_cond
       Pfcmpd (freg_of a1) (freg_of a2) :: k
   | Cnotcompf cmp, a1 :: a2 :: nil =>
       Pfcmpd (freg_of a1) (freg_of a2) :: k
+  | Ccompfzero cmp, a1 :: nil =>
+      Pfcmpzd (freg_of a1) :: k
+  | Cnotcompfzero cmp, a1 :: nil =>
+      Pfcmpzd (freg_of a1) :: k
   | _, _ =>
      k (**r never happens for well-typed code *)
   end.
@@ -209,6 +213,8 @@ Definition crbit_for_cond (cond: condition) :=
   | Ccompuimm cmp n => crbit_for_unsigned_cmp cmp
   | Ccompf cmp => crbit_for_float_cmp cmp
   | Cnotcompf cmp => crbit_for_float_not_cmp cmp
+  | Ccompfzero cmp => crbit_for_float_cmp cmp
+  | Cnotcompfzero cmp => crbit_for_float_not_cmp cmp
   end.
 
 (** Translation of the arithmetic operation [r <- op(args)].
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 629a615..29197e9 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1082,6 +1082,21 @@ Proof.
   split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A.  
   destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
   auto.
+  (* Ccompfzero *)
+  generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. case c; apply MATCH; assumption.
+  auto.
+  (* Cnotcompf *)
+  generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)).
+  intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]].
+  econstructor.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A.  
+  destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
+  auto.
 Qed.
 
 (** Translation of arithmetic operations. *)
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 031ec32..0c77305 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -67,6 +67,8 @@ Nondetfunction eval_static_condition (cond: condition) (vl: list approx) :=
   | Ccompuimm c n, I n1 :: nil => Some(Int.cmpu c n1 n)
   | Ccompf c, F n1 :: F n2 :: nil => Some(Float.cmp c n1 n2)
   | Cnotcompf c, F n1 :: F n2 :: nil => Some(negb(Float.cmp c n1 n2))
+  | Ccompfzero c, F n1 :: nil => Some(Float.cmp c n1 Float.zero)
+  | Cnotcompfzero c, F n1 :: nil => Some(negb(Float.cmp c n1 Float.zero))
   | _, _ => None
   end.
 
@@ -166,6 +168,22 @@ Nondetfunction cond_strength_reduction
       (Ccompimm c (eval_static_shift s n2), r1 :: nil)
   | Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (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)
+      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)
   | _, _, _ => 
       (cond, args)
   end.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 711bb33..bf3b216 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -192,6 +192,15 @@ Proof.
   rewrite H. rewrite eval_static_shift_correct. auto.
   rewrite H. rewrite eval_static_shift_correct. auto.
   auto.
+  destruct (Float.eq_dec n1 Float.zero); simpl; auto.
+  rewrite H0; subst n1. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
+  destruct (Float.eq_dec n2 Float.zero); simpl; auto.
+  congruence.
+  destruct (Float.eq_dec n1 Float.zero); simpl; auto.
+  rewrite H0; subst n1. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
+  destruct (Float.eq_dec n2 Float.zero); simpl; auto.
+  congruence.
+  auto.
 Qed.
 
 Lemma make_addimm_correct:
diff --git a/arm/Op.v b/arm/Op.v
index 99ba924..a5502c0 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -58,7 +58,10 @@ Inductive condition : Type :=
   | 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 *)
+  | 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 *)
+
 
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
@@ -186,6 +189,8 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem):
   | 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))
   | _, _ => None
   end.
 
@@ -276,6 +281,8 @@ Definition type_of_condition (c: condition) : list typ :=
   | Ccompuimm _ _ => Tint :: nil
   | Ccompf _ => Tfloat :: Tfloat :: nil
   | Cnotcompf _ => Tfloat :: Tfloat :: nil
+  | Ccompfzero _ => Tfloat :: nil
+  | Cnotcompfzero _ => Tfloat :: nil
   end.
 
 Definition type_of_operation (op: operation) : list typ * typ :=
@@ -480,6 +487,8 @@ Definition negate_condition (cond: condition): condition :=
   | Ccompuimm c n => Ccompuimm (negate_comparison c) n
   | Ccompf c => Cnotcompf c
   | Cnotcompf c => Ccompf c
+  | Ccompfzero c => Cnotcompfzero c
+  | Cnotcompfzero c => Ccompfzero c
   end.
 
 Lemma eval_negate_condition:
@@ -497,6 +506,8 @@ Proof.
   rewrite Val.negate_cmpu_bool; rewrite H; auto.
   rewrite H; auto.
   destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. 
+  rewrite H; auto.
+  destruct (Val.cmpf_bool c v (Vfloat Float.zero)); simpl in H; inv H. rewrite negb_elim; auto. 
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
@@ -801,6 +812,8 @@ Opaque Int.add.
   eapply CMPU; eauto.
   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.
 
 Ltac TrivialExists :=
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 634faae..48943e9 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -562,16 +562,16 @@ let print_instruction oc = function
   | Pfsubd(r1, r2, r3) ->
       fprintf oc "	fsubd	%a, %a, %a\n" freg r1 freg r2 freg r3; 1
   | Pflid(r1, f) ->
-(*
-      if Int64.bits_of_float f = 0L (* +0.0 *) then begin
-        fprintf oc "	mvfd	%a, #0.0\n" freg r1; 1
-      end else begin
-*)
+      (* We could make good use of the fconstd instruction, but it's available
+         in VFD v3 and up, not in v1 nor v2 *)
       let lbl = label_float f in
       fprintf oc "	fldd	%a, .L%d @ %.12g\n" freg r1 lbl f; 1
   | Pfcmpd(r1, r2) ->
       fprintf oc "	fcmpd	%a, %a\n" freg r1 freg r2;
       fprintf oc "	fmstat\n"; 2
+  | Pfcmpzd(r1) ->
+      fprintf oc "	fcmpzd	%a\n" freg r1;
+      fprintf oc "	fmstat\n"; 2
   | Pfsitod(r1, r2) ->
       fprintf oc "	fmsr	%a, %a\n" freg_single r1 ireg r2;
       fprintf oc "	fsitod	%a, %a\n" freg r1 freg_single r1; 2
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index 9ebce97..8f21cd4 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -48,6 +48,10 @@ let print_condition reg pp = function
       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
+  | (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 "<bad condition>"