From 448cc3ff32cc60f4b9e78911404106797e109d90 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 29 Mar 2012 11:57:33 +0000 Subject: 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 --- arm/Asm.v | 3 +++ arm/Asmgen.v | 6 ++++++ arm/Asmgenproof1.v | 15 +++++++++++++++ arm/ConstpropOp.vp | 18 ++++++++++++++++++ arm/ConstpropOpproof.v | 9 +++++++++ arm/Op.v | 15 ++++++++++++++- arm/PrintAsm.ml | 10 +++++----- arm/PrintOp.ml | 4 ++++ 8 files changed, 74 insertions(+), 6 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index 5e16f059..58b26343 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 c727db9b..7cf25f5f 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 629a6151..29197e90 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 031ec32c..0c77305d 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 711bb33b..bf3b216c 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 99ba9246..a5502c01 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 634faae1..48943e98 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 9ebce979..8f21cd41 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 "" -- cgit