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.

[ivanperez-keera]

I've converted this into an issue for now until we figure out what the problem really is. We can then open one or more issues as needed.

[RyanGlScott]

The use of realToFrac is 100% the source of the problem in copilot-bluespec. I've confirmed that applying the following patch fixes it:

diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
index c4978aef..56f5a543 100644
--- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
+++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
@@ -15,6 +15,7 @@ module Copilot.Compile.Bluespec.Expr
 -- External imports
 import Data.Foldable (foldl')
 import Data.String (IsString (..))
+import GHC.Float (float2Double)
 import qualified Language.Bluespec.Classic.AST as BS
 import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS

@@ -536,7 +537,7 @@ constTy ty =
     Word16    -> constInt ty . toInteger
     Word32    -> constInt ty . toInteger
     Word64    -> constInt ty . toInteger
-    Float     -> constFP ty . realToFrac
+    Float     -> constFP ty . float2Double
     Double    -> constFP ty

     -- Translating a Copilot array literal to a Bluespec Vector is somewhat

[RyanGlScott]

It's less clear if the use of realToFrac in copilot-theorem is actually a problem, but it's probably better to be safe than sorry and replace it with double2Float.

[RyanGlScott]

OK, here is a program that demonstrates the issue in copilot-theorem:

-- Test.hs
module Main (main) where

import qualified Prelude as P
import Control.Monad (void, forM_)
import qualified Data.Map as Map

import Language.Copilot
import Copilot.Theorem.What4

spec :: Spec
spec =
  let floats :: Stream Float
      floats = extern "floats" Nothing in
  void $ prop "refl" $ forAll (floats <= floats)

main :: IO ()
main = do
  spec' <- reify spec

  -- Use Z3 to prove the properties.
  results <- proveWithCounterExample Z3 spec'

  -- Print the results.
  forM_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      ValidCex -> putStrLn "valid"
      InvalidCex cex -> do
        putStrLn "invalid"
        putStrLn $ ppCounterExample cex
      UnknownCex -> putStrLn "unknown"

-- | Pretty-print a counterexample for user display.
ppCounterExample :: CounterExample -> String
ppCounterExample cex
    | any P.not (baseCases cex)
    = if Map.null baseCaseVals
        then
          "  All possible extern values during the base case(s) " P.++
          "constitute a counterexample."
        else
          unlines $
            "  The base cases failed with the following extern values:" :
            map
              (\((name, _), val) -> "    " P.++ name P.++ ": " P.++ show val)
              (Map.toList baseCaseVals)

    | P.not (inductionStep cex)
    = if Map.null inductionStepVals
        then
          "  All possible extern values during the induction step " P.++
          "constitute a counterexample."
        else
          unlines $
            "  The induction step failed with the following extern values:" :
            map
              (\((name, _), val) -> "    " P.++ name P.++ ": " P.++ show val)
              (Map.toList inductionStepVals)

    | otherwise
    = error $
        "ppCounterExample: " P.++
        "Counterexample without failing base cases or induction step"
  where
    allExternVals = concreteExternValues cex

    baseCaseVals =
      Map.filterWithKey
        (\(_, offset) _ ->
          case offset of
            AbsoluteOffset {} -> True
            RelativeOffset {} -> False
        )
        allExternVals

    inductionStepVals =
      Map.filterWithKey
        (\(_, offset) _ ->
          case offset of
            AbsoluteOffset {} -> False
            RelativeOffset {} -> True
        )
        allExternVals

The refl proposition is false, as NaN <= NaN does not hold. It's a bit tricky to get realToFrac @Double @Float NaN to miscompile, however, as you have to disable optimizations. I did so by compiling copilot without optimizations and then running this program, like so:

$ cabal build copilot copilot-bluespec --write-ghc-environment-file=always --disable-optimization
$ runghc Test.hs
refl: invalid
  The induction step failed with the following extern values:
    floats: Infinity

That last line should read floats: NaN, not reads: Infinity.

[RyanGlScott]

The following patch fixes the issue in copilot-theorem:

diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 818ac9b3..ad6b1e0b 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -82,7 +82,7 @@ import Data.Parameterized.NatRepr
 import Data.Parameterized.Nonce
 import Data.Parameterized.Some
 import qualified Data.Parameterized.Vector as V
-import GHC.Float (castWord32ToFloat, castWord64ToDouble)
+import GHC.Float (castWord32ToFloat, castWord64ToDouble, double2Float)
 import LibBF (BigFloat, bfToDouble, pattern NearEven)
 import qualified Panic as Panic

@@ -712,7 +712,7 @@ valFromExpr ge xe = case xe of
   XFloat e ->
     Some . CopilotValue CT.Float <$>
       iFloatGroundEval WFP.SingleFloatRepr e
-                       (realToFrac . fst . bfToDouble NearEven)
+                       (double2Float . fst . bfToDouble NearEven)
                        fromRational
                        (castWord32ToFloat . fromInteger . BV.asUnsigned)
   XDouble e ->