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

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