Special `Float` 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 , the realToFrac function can mis-translate 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.

Additional context

• Fix toRational and realToFrac for Float and Double haskell/core-libraries-committee#338: describes the issue with realToFrac.

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.

It is sometimes possible to test for the presence of incorrect results produced by realToFrac, depending on GHC versions and optimization levels. 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 (i.e., infinity) 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 generates an incorrect counterexample for the following program when Copilot is compiled 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

copilot-bluespec and copilot-theorem should not use realToFrac to translate floating point values, and should instead use a function that translates NaN and special values correctly.

Desired result

copilot-bluespec and copilot-theorem should not use realToFrac to translate floating point values, and should instead use a function that translates NaN and special values correctly.

Proposed solution

Replace uses of realToFrac in copilot-bluespec and copilot-theorem with calls to a function that converts floats correctly including special cases such as NaN and negative zero.

Further notes

• An end-to-end test case for copilot-bluespec would also require fixing copilot-bluespec: Special floating-point values are translated to syntactically invalid Bluespec code #696 first.

• The function GHC.Float.double2Float is a possible alternative, and translates special values correctly.

[tkann-galois]

The commits are all ready for this but I can wait until #696 is accepted to keep the history clean