From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id AE2A07F0A3 for ; Wed, 2 Sep 2015 21:14:52 +0200 (CEST) IronPort-PHdr: 9a23:eSEJVhAO9ap1+XE5KtgcUyQJP3N1i/DPJgcQr6AfoPdwSP7zpMbcNUDSrc9gkEXOFd2CrakU16yO6eu5AjNIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6bqodaKOFoArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5lH/Sl6m4HcGX2wN2iBPGBPP4Qv1FsPrtTDhvOdn1wGfJcyzVq8vHzO44PE4ZgXvjXI3PiA4/XufrsFqi7MT9CKouR1y2cjwbZuSJdJ/eLncdJUUXzwSDY5qSyVdD9bkPMM0BO0bMLMd9tGlqg== Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xavier.leroy@gmail.com; spf=Pass smtp.mailfrom=xavier.leroy@gmail.com; spf=None smtp.helo=postmaster@mail-lb0-f170.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of xavier.leroy@gmail.com) identity=pra; client-ip=209.85.217.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="xavier.leroy@gmail.com"; x-sender="xavier.leroy@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of xavier.leroy@gmail.com designates 209.85.217.170 as permitted sender) identity=mailfrom; client-ip=209.85.217.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="xavier.leroy@gmail.com"; x-sender="xavier.leroy@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-lb0-f170.google.com) identity=helo; client-ip=209.85.217.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="xavier.leroy@gmail.com"; x-sender="postmaster@mail-lb0-f170.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C2AABGSudVm6rZVdFdhFgGgx26KQEJiScHOBQBAQEBAQEBARABAQEBAQYLCwkhLoIdggcBAQMBEhEEGQESJgEDAQsBBQUEBzcCAiISAQUBHAYTIod3AwoIqFaBLz4xi0CEZYpeJw2FAQEBCAIaAQUOhFWCEIR7h3uBQwWVSYx2gUqVOYIgEiOBFxdJg0g8M4JNAQEB X-IPAS-Result: A0C2AABGSudVm6rZVdFdhFgGgx26KQEJiScHOBQBAQEBAQEBARABAQEBAQYLCwkhLoIdggcBAQMBEhEEGQESJgEDAQsBBQUEBzcCAiISAQUBHAYTIod3AwoIqFaBLz4xi0CEZYpeJw2FAQEBCAIaAQUOhFWCEIR7h3uBQwWVSYx2gUqVOYIgEiOBFxdJg0g8M4JNAQEB X-IronPort-AV: E=Sophos;i="5.17,455,1437429600"; d="scan'208";a="144546518" Received: from mail-lb0-f170.google.com ([209.85.217.170]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 02 Sep 2015 21:14:45 +0200 Received: by lbcao8 with SMTP id ao8so11991413lbc.3 for ; Wed, 02 Sep 2015 12:14:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc:content-type; bh=f0pDkBX+jlHTiZSp4vZcfFeBqwtM4vKxGzSVqxrkCPE=; b=Jy9bLwldTugNS0IMFsu7m3HKtxFWh0WChi/jLu4hKc50D/hIXIkklXmfQUlGnwn73/ HDcPipYextm2eMzeI/oSEsCaE0I5FJjLLL6Y+uRJRFDnvwUQWhnic22VCHlHBGzoKV+P 7CMjfu4QNEoWsOs/EWnXM5WMsGhZKwQEnBoMq1WGppxcR5jo7+vdvdA1Bs9zUZAC+owd yHkhmPwoxu643gS9hJD3vq0hM/PbcuyGApKJCqx0XNjUBfwPvpqlHU/nINIPz15hxhU5 pJv2neNhluT+EqK996ugRuk6Gba9N1/T9Z+RpX/wgg4O+mLnfRZ2g9ek8XGTlQWFz7dG q2rg== X-Received: by 10.152.228.135 with SMTP id si7mr13857567lac.77.1441221284728; Wed, 02 Sep 2015 12:14:44 -0700 (PDT) MIME-Version: 1.0 Sender: xavier.leroy@gmail.com Received: by 10.25.78.73 with HTTP; Wed, 2 Sep 2015 12:14:15 -0700 (PDT) In-Reply-To: <1D9E71FC-1C39-4655-9258-1F2CB85BAF3D@mpi-sws.org> References: <1D9E71FC-1C39-4655-9258-1F2CB85BAF3D@mpi-sws.org> From: Xavier Leroy Date: Wed, 2 Sep 2015 21:14:15 +0200 X-Google-Sender-Auth: gf_nMNZIY03RN6t62GTUTo98UvU Message-ID: To: Andreas Rossberg Cc: Ocaml Mailing List Content-Type: multipart/alternative; boundary=001a11342d52b81622051ec87a87 Subject: Re: [Caml-list] NaN reresentations --001a11342d52b81622051ec87a87 Content-Type: text/plain; charset=UTF-8 2015-09-02 10:56 GMT-07:00 Andreas Rossberg : > Does the Ocaml implementation make guarantees about the stable > representation of floats? In particular, if I use Int64.float_of_bits to > create a particular NaN representation, am I guaranteed that its bit > pattern is maintained no matter where the value is stored or passed? > It depends on the underlying hardware. For instance, with x86-32 bits, some FP moves go through the x87 FP stack, undergoing a double -> extended -> double conversion. These conversions turn signaling NaNs into quiet NaNs, and I'm not sure they preserve the other bits of the NaN payload. On other platforms, esp. x86-64 bits, I'm pretty confident that NaN bits are preserved by copying and parameter passing. > > We are currently in the process of implementing a reference interpreter > for a little low-level language, and that tries to be as accurate as > possible about float representations. > One possibility would be to represent your floats as int64 values (= their bit-level representation), and convert only when you operate over them, e.g. let fp_add x y = Int64.bits_of_float (Int64.float_of_bits x +. Int64.float_of_bits y) Best, - Xavier --001a11342d52b81622051ec87a87 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
2015-09-02 10:56 GMT-07:00 Andreas Rossberg <rossberg@= mpi-sws.org>:
Does the Ocaml implementation make= guarantees about the stable representation of floats? In particular, if I = use Int64.float_of_bits to create a particular NaN representation, am I gua= ranteed that its bit pattern is maintained no matter where the value is sto= red or passed?

It depends on the underl= ying hardware.=C2=A0 For instance, with x86-32 bits, some FP moves go throu= gh the x87 FP stack, undergoing a double -> extended -> double conver= sion.=C2=A0=C2=A0 These conversions turn signaling NaNs into quiet NaNs, an= d I'm not sure they preserve the other bits of the NaN payload.

=
On other platforms, esp. x86-64 bits, I'm pretty confident t= hat NaN bits are preserved by copying and parameter passing.
= =C2=A0

We are currently in the process of implementing a reference interpreter for= a little low-level language, and that tries to be as accurate as possible = about float representations.

One possib= ility would be to represent your floats as int64 values (=3D their bit-leve= l representation), and convert only when you operate over them, e.g.
let fp_add x y =3D Int64.bits_of_float (Int64.float_of_bits x += . Int64.float_of_bits y)

Best,

- Xavier=

--001a11342d52b81622051ec87a87--