`copilot-{bluespec,theorem}`: Special floating-point values are translated incorrectly

[RyanGlScott]

Description

The following functions use realToFrac in their implementations to translate Float values.

• copilot-bluespec:Copilot.Compile.Bluespec.constTy
• copilot-theorem:Copilot.Theorem.What4.valFromExpr

As noted in haskell/core-libraries-committee#338, the realToFrac function can miscompile special floating-point values, such as negative zero, infinity, and NaN. This can cause copilot-bluespec to generate unexpected Bluespec code, and it can cause copilot-theorem to produce incorrect counterexamples.

Type

• Bug: incorrect generated code and counterexamples.

Additional context

• Fix toRational and realToFrac for Float and Double haskell/core-libraries-committee#338 (the issue in which this problem was first observed)

Requester

• Ryan Scott (Galois)

Method to check presence of bug

The following search finds mentions of realToFrac in the implementation:

$ grep -nHre 'realToFrac' copilot**/src copilot**/tests
copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs:539:    Float     -> constFP ty . realToFrac
copilot-theorem/src/Copilot/Theorem/What4.hs:710:                       (realToFrac . fst . bfToDouble NearEven)

At a minimum, these should be removed.

Sometimes, it is also possible to test for the presence of incorrect results as a result of realToFrac, although the presence or absence of these effects can depend on GHC versions and optimization levels, so they may not be as reliable of a metric. The following test case has been observed to demonstrate incorrect generated code from copilot-bluespec:

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

import qualified Copilot.Compile.Bluespec as Bluespec
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
  Bluespec.compile "Test" spec'

Compare the results of the Copilot interpreter (which handles special Float values correctly):

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

To the generated Bluespec code, where NaN is mistranslated to 5.104235503814077e38, both positive and negative infinity are mistranslated to 3.402823669209385e38, and negative zero is mistranslated to zero:

      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);

In addition, copilot-theorem will generate an incorrect counterexample for the following program if you compile the Copilot libraries without optimizations:

-- 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

$ 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.

Expected result

The string returned by grep ... (as shown above) should be empty.

Desired result

The string returned by grep ... (as shown above) should be empty. At least one test for each of the copilot-bluespec and copilot-theorem packages should be added that exercise correct results involving Float values.

Proposed solution

Removing the function from the module Copilot.Theorem.Misc.SExpr.parseSExpr, as well as any auxiliary functions or imports exclusively needed by that function, if any.

Further notes

None.

[tkann-galois]

In addition to the realToFrac usage there is the added problem that infs, NaNs, and $\pm$ zeros are specially constructed in BS. This means that Doubles are also incorrectly parsed. This can be fixed by updating the translation on constants by adding a few extra guards that roll-out these functions.

In Expr.hs the following changes work locally for at least the bluespec generation, I haven't yet tackled the theorem proving section yet.

-- | Translate a Copilot floating-point literal into a Bluespec expression.
constFP :: Type ty -> Double -> BS.CExpr
constFP ty d
    -- Bluespec intentionally does not support negative literal syntax (e.g.,
    -- -42.5), so we must create negative floating-point literals using the
    -- `negate` function.
    | isInfinite d = BS.CApply 
                      (BS.CVar $ BS.mkId BS.NoPos "infinity") 
                      [if d < 0 then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse []]
    | isNaN d      = BS.CApply 
                      (BS.CVar $ BS.mkId BS.NoPos "qnan") []
    | d == 0       = BS.CApply 
                      (BS.CVar $ BS.mkId BS.NoPos "zero") 
                      [if isNegativeZero d then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse []]
    | d > 0        = withTypeAnnotation ty $ cLit $ BS.LReal d
    | otherwise    = withTypeAnnotation ty $
                     BS.CApply
                       (BS.CVar $ BS.idNegateAt BS.NoPos)
                       [cLit $ BS.LReal $ negate d]

These changes can be seen in a branch on the galois fork that also has an accompanying example matching the one previously posted. The following BS code is synthesized

      s0_0 :: Prelude.Reg Float <- mkReg (qnan);
      let { s0 :: Vector.Vector 1 (Prelude.Reg Float);
            s0 =  update newVector 0 s0_0; };
      s1_0 :: Prelude.Reg Float <- mkReg (infinity Prelude.False);
      s1_1 :: Prelude.Reg Float <- mkReg (infinity Prelude.True);
      let { s1 :: Vector.Vector 2 (Prelude.Reg Float);
            s1 =  update (update newVector 0 s1_0) 1 s1_1; };
      s2_0 :: Prelude.Reg Float <- mkReg (zero Prelude.False);
      s2_1 :: Prelude.Reg Float <- mkReg (zero Prelude.True);

and while the floating point print formatting doesn't seem to function correctly for these special cases, looking at the bit-representations (%b) they appear to be correct.

[RyanGlScott]

Good catch!

I don't think that copilot-theorem has a similar problem, as copilot-theorem doesn't scrutinize Float values in the same way that copilot-bluespec's constFP function does. All that copilot-theorem does is directly produce the Float value (in valFromExpr), which is then passed directly into a CounterExample (here). It is up to downstream users of the CounterExample to determine how they want to scrutinize any Float values that it contains, but any problems in code of this sort would be outside the copilot-theorem library itself.

Notably, the test case involving copilot-theorem above just calls show on the CounterExample's Float values, which correctly displays all of the special floating-point values that we care about:

-- In a GHCi session

λ> show @Float 0
"0.0"
λ> show @Float (-0)
"-0.0"
λ> import Numeric.IEEE -- from the ieee754 package
λ> show @Float infinity
"Infinity"
λ> show @Float (-infinity)
"-Infinity"
λ> show @Float nan
"NaN"

[ivanperez-keera]

It looks like this issue requires some discussion before it can be addressed. Do we need to turn it into a discussion?

[RyanGlScott]

Up to you, but I think there's a consensus on what the implementation should be. (@tkann-galois, please speak up if you feel differently.)

[tkann-galois]

Bluespec does expose both a quiet NaN and a signaling NaN. I assumed if someone put it in a stream it's intended and therefore should be a quiet nan (qnan). In reality I'm not sure how much this makes a difference. Otherwise, good to go!

[RyanGlScott]

This is a good observation, and it's a corner case that I've ran into separately in copilot-bluespec's test suite. As noted there, there really isn't a good way to express all the different NaN values in terms of Bluespec's API:

copilot/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs

Lines 1254 to 1267 in 21cb3b1

	-- We want to ensure that NaN values are correctly translated to Bluespec,
	-- bit by bit. We have two mechanisms to do so. On the Haskell side, we have
	-- `ieee754`'s `nanWithPayload` function, and on the Bluespec side, we have
	-- `FloatingPoint`'s `nanQuiet` function. Unfortunately, their arguments are
	-- of different types, and it isn't quite clear how to express one function
	-- in terms of the other.
	--
	-- To avoid this problem, we take a more indirect approach: we first cast
	-- the Haskell floating-point value to a word and then `unpack` the word to
	-- a floating-point value on the Bluespec side. It's somewhat verbose, but
	-- it gets the job done reliably.
	| isNaN float
	= "unpack (" ++ show (castFloatToWord float) ++
	" :: Bit " ++ show floatSizeInBits ++ ")"

For the sake of being bit-for-bit compatible, I opted for the approach of calling unpack on the raw, bit-level representation of the NaN value. The same approach should work just as well for your needs, I'd say. (We could conceivably do this for all floating-point values in constFP, but the output would be far less pretty, so best to limit this to just NaN values.)