Fix handling of special Float values. Refs #697.

[RyanGlScott]

Both copilot-bluespec and copilot-theorem up-cast Float values to Double values using the realToFrac function. realToFrac incorrectly handles special floating-point values such as negative zero, infinity, and NaN values, causing copilot-bluespec to generate the wrong Bluespec Float values and causing copilot-theorem to generate incorrect counterexamples.

This commit removes the use of realToFrac in favor of an alternative approach based on GHC.Float.{float2Double,double2Float}, which correctly handles most special floating-point values. A notable exception is NaN values, as {float2Double,double2Float} does not reliably preserve the payload of a NaN value. As such, we include a special case for NaN values that takes care to preserve payloads.

Fixes#697.

[ivanperez-keera]

Change Manager: See notes above about changes requested.

[RyanGlScott]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

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.