`copilot-bluespec` miscompiles negative zero, infinite, and NaN `Float` values

[RyanGlScott]

Prompted by haskell/core-libraries-committee#338, I recently checked to see if Copilot has any problematic uses of the realToFrac function. There is one such use in copilot-bluespec to convert Floats to Doubles:

copilot/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs

Line 539 in 894f0aa

Float -> constFP ty . realToFrac

As noted in haskell/core-libraries-committee#338, realToFrac currently mishandles certain special floating-point values. To see this in action, consider this Copilot specification:

-- Test.hs
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import qualified Copilot.Compile.Bluespec as Bluespec
import qualified Copilot.Compile.C99 as C99
import Language.Copilot

nans :: Stream Float
nans = [read "NaN"] ++ nans

infinities :: Stream Float
infinities = [inf, -inf] ++ infinities
  where
    inf :: Float
    inf = read "Infinity"

zeroes :: Stream Float
zeroes = [0, -0] ++ zeroes

spec :: Spec
spec =
  trigger "rtf" true [arg nans, arg infinities, arg zeroes]

main :: IO ()
main = do
  interpret 2 spec
  spec' <- reify spec
  C99.compile "test" spec'
  Bluespec.compile "Test" spec'

This defines a spec with a single trigger rtf, whose arguments sample from Float streams containing several special values. We can see that the Copilot interpreter handles these special values correctly:

$ runghc Test.hs
rtf:
(NaN,Infinity,0.0)
(NaN,-Infinity,-0.0)

Moreover, these special values are correctly translated to C99, as seen in this excerpt from the generated test.c file:

static float s0[(1)] = {((float)(NAN))};
static float s1[(2)] = {((float)(INFINITY)), ((float)(-INFINITY))};
static float s2[(2)] = {((float)(0.0f)), ((float)(-0.0f))};

The translation to Bluespec, on the other hand, produces malformed values, as seen in this excerpt from the generated Test.bs file:

      s0_0 :: Prelude.Reg Float <- mkReg (5.104235503814077e38::Float);
      let { s0 :: Vector.Vector 1 (Prelude.Reg Float);
            s0 =  update newVector 0 s0_0; };
      s1_0 :: Prelude.Reg Float <- mkReg (3.402823669209385e38::Float);
      s1_1 :: Prelude.Reg Float <- mkReg
                                     ((Prelude.negate 3.402823669209385e38)::Float);
      let { s1 :: Vector.Vector 2 (Prelude.Reg Float);
            s1 =  update (update newVector 0 s1_0) 1 s1_1; };
      s2_0 :: Prelude.Reg Float <- mkReg (0.0::Float);
      s2_1 :: Prelude.Reg Float <- mkReg (0.0::Float);

Note that NaN is mistranslated to 5.104235503814077e38, both positive and negative infinity are mistranslated to 3.402823669209385e38, and negative zero is mistranslated to zero.

There is an in-flight patch being proposed to fix haskell/core-libraries-committee#338 in the base library, but we should consider fixing this bug independently so that copilot-bluespec can correctly translate special Float values on all versions of base that Copilot currently supports. My suspicion is that we could fix this bug by replacing the use of realToFrac above with GHC.Float.float2Double.

[RyanGlScott]

There is another suspicious use of realToFrac in copilot-theorem, this time for converting a Double to a Float:

copilot/copilot-theorem/src/Copilot/Theorem/What4.hs

Line 715 in 894f0aa

(realToFrac . fst . bfToDouble NearEven)

I haven't figured out a way to get this use of realToFrac to misbehave, but it seems like this should be replaced with GHC.Float.double2Float.