From 822a6a12316aa043eea7f6aed4d730bc10a73d7b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 10 Jul 2019 15:43:03 +0200 Subject: x86_64: branchless implementation of floatofintu and intuoffloat MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The implementation uses float <-> signed 64-bit integer conversion instructions, and is both efficient and branchless. Based on a suggestion by Rémi Hutin. --- x86/SelectOpproof.v | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'x86/SelectOpproof.v') diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index 821a54e8..a1bb0703 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -828,7 +828,8 @@ Proof. intros. destruct x; simpl in H0; try discriminate. destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. - set (im := Int.repr Int.half_modulus). + destruct Archi.splitlong. +- set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). constructor. auto. @@ -855,6 +856,11 @@ Proof. rewrite Int.add_neg_zero in A4. rewrite Int.add_zero in A4. auto. +- apply Float.to_intu_to_long in Heqo. repeat econstructor. eauto. + simpl. rewrite Heqo; reflexivity. + simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned; auto. + assert (Int.modulus < Int64.max_unsigned) by reflexivity. + generalize (Int.unsigned_range n); omega. Qed. Theorem eval_floatofintu: @@ -864,10 +870,11 @@ Theorem eval_floatofintu: exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v. Proof. intros until y; unfold floatofintu. case (floatofintu_match a); intros. - InvEval. TrivialExists. - destruct x; simpl in H0; try discriminate. inv H0. +- InvEval. TrivialExists. +- destruct x; simpl in H0; try discriminate. inv H0. exists (Vfloat (Float.of_intu i)); split; auto. - econstructor. eauto. + destruct Archi.splitlong. ++ econstructor. eauto. set (fm := Float.of_intu Float.ox8000_0000). assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)). constructor. auto. @@ -883,6 +890,7 @@ Proof. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. fold fm. rewrite Float.of_intu_of_int_2; auto. rewrite Int.sub_add_opp. auto. ++ rewrite Float.of_intu_of_long. repeat econstructor. eauto. reflexivity. Qed. Theorem eval_intofsingle: -- cgit