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