Special Float values are translated incorrectly

Description

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

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.

Documenting changes in Changelog for Copilot-Language#697

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

Merge branch 'develop-bluespec-special-constfp'. Close #696.

Documenting changes in Changelog for Copilot-Language#697

copilot-bluespec: Fix interpretation of special constant floating-poi…

copilot-theorem: remove the use of `realToFrac` when handling BigFloa…

Document changes in Changelog. Refs Copilot-Language#697.

copilot-bluespec: Fix interpretation of special constant floating-poi…

copilot-theorem: remove the use of `realToFrac` when handling BigFloa…

Document changes in Changelog. Refs Copilot-Language#697.

copilot-bluespec: Fix interpretation of special constant floating-poi…

copilot-theorem: remove the use of `realToFrac` when handling BigFloa…

Document changes in Changelog. Refs Copilot-Language#697.

copilot-bluespec: Fix interpretation of special constant floating-poi…

copilot-bluespec: Document changes in CHANGELOG. Refs Copilot-Languag…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

Implementor: Solution implemented, review requested.

copilot-bluespec: Fix translation of special Float values to Bluespec…

copilot-theorem: Handle special Float values correctly for counterexa…

copilot-bluespec: Document changes in CHANGELOG. Refs Copilot-Languag…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/277846515

The solution proposed produces the expected result. Details:
The following dockerfile first checks that realToFrac is not used anywhere in Copilot, and then installs both Copilot and Bluespec and confirms that printing some special floating point values (e.g., -0, -infinity) results in the same values being printed for Copilot's interpreter and for Copilot-generated Bluespec code being simulated, after which it prints the message "Success":

--- Dockerfile-verify-697
FROM ubuntu:jammy

WORKDIR /root
SHELL ["/bin/bash", "-c"]

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

RUN ghcup install ghc 9.8.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.8.4
RUN cabal update

RUN apt-get install --yes iverilog libtcl8.6

RUN curl -L https://github.com/B-Lang-org/bsc/releases/download/2025.01.1/bsc-2025.01.1-ubuntu-22.04.tar.gz -o $HOME/bsc.tar.gz
RUN tar -zxvpf bsc.tar.gz
ENV PATH=$PATH:/root/bsc-2025.01.1-ubuntu-22.04/bin/

ADD Top.bs /root/
ADD SpecialDoubles.hs /root/

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && ! grep -re 'realToFrac' $NAME/copilot**/src $NAME/copilot**/tests \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install \
       $NAME/copilot/ \
       $NAME/copilot-bluespec/ \
       $NAME/copilot-c99/ \
       $NAME/copilot-core/ \
       $NAME/copilot-prettyprinter/ \
       $NAME/copilot-interpreter/ \
       $NAME/copilot-language/ \
       $NAME/copilot-libraries/ \
       $NAME/copilot-theorem/ \
  && (cabal v1-exec -- runhaskell SpecialDoubles.hs > interpreter_output.txt) \
  && bsc -sim -g mkTop -u Top.bs \
  && bsc -sim -e mkTop -o mkTop.exe bs_fp.c \
  && (./mkTop.exe -m 1 > bluesim_output.txt) \
  && diff -q interpreter_output.txt bluesim_output.txt \
  && echo "Success"

--- Top.bs
package Top where

import SpecialDoubles

mkTop :: Module Empty
mkTop =
  module
    specialDoublesMod <- mkSpecialDoubles

    addRules $
      mkSpecialDoublesRules specialDoublesMod $
        interface SpecialDoublesRulesIfc
          value0_action x = $display (fshow (pack x))
          value1_action x = $display (fshow (pack x))
          value2_action x = $display (fshow (pack x))
          value3_action x = $display (fshow (pack x))
          value4_action x = $display (fshow (pack x))
          value5_action x = $display (fshow (pack x))
          value6_action x = $display (fshow (pack x))

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

import           Control.Monad (zipWithM_)
import           GHC.Float     (castFloatToWord32)
import           Numeric       (showHex)
import           Numeric.IEEE  (infinity)
import qualified Prelude       as P
import           Text.Printf   (printf)

import qualified Copilot.Compile.Bluespec as Bluespec
import           Copilot.Interpret.Eval
import           Language.Copilot

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

   -- Take the Copilot interpreter's output and display the resulting Floats'
   -- bit-level representations.
   let outputs = interpTriggers $ eval C 1 spec'
   mapM_
     (\(_, [Just [output]]) ->
       printf "'h%08x\n" $ castFloatToWord32 $ read output)
     outputs

   -- Also translate the Copilot spec to Bluespec.
   Bluespec.compile "SpecialDoubles" spec'

spec :: Spec
spec =
  zipWithM_
    (\i value -> trigger ("value" P.++ show i) true [arg (constF value)])
    [0..]
    values

word32ToHex :: Word32 -> String
word32ToHex w = takeLast 8 $ showHex w ""
   where
     -- On old versions of GHC, the implementation of `showHex` adds leading
     -- `f` digits, which we remove.
     takeLast n = reverse . P.take n . reverse

values :: [Float]
values =
  [ -- Infinity
    infinity
  , -infinity
  -- Zero
  , 0
  , -0
  -- Others
  , 1.0
  , 2.0
  , 3.0
  ]

Command (substitute variables based on new path after merge):

$ docker run -e "REPO=https://github.com/GaloisInc/copilot-1" -e "NAME=copilot-1" -e "COMMIT=6e2fed247bbf8b1a878306b8c0227c3629266ffb" -it copilot-verify-697

Implementation is documented. Details:
The new code is documented.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed; the changes do not affect existing examples.
Required version bumps are evaluated. Details:
Bump not needed; the change does not alter the public API but fixes an existing bug.

Change Manager: Implementation ready to be merged.

Merge branch 'fix-697-bluespec-special-floats'. Close Copilot-Languag…

Navigation Menu

Repository navigation

Special `Float` values are translated incorrectly #697

32 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Special Float values are translated incorrectly #697

Description

Activity

tkann-galois commented on Dec 19, 2025

32 remaining items

RyanGlScott commented on Mar 31, 2026

ivanperez-keera commented on May 7, 2026

ivanperez-keera commented on May 7, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Special `Float` values are translated incorrectly #697