copilot-bluespec: Fix translation of constant floating-point values. Refs #696.

[tkann-galois]

Fixes#696

The previous usage of constFp in Copilot-Bluespec did not correctly translate special double-width floating point values. This PR implements a fix and a proof-of-concept example.
The example does not compile before the fix but does compile after the patch, giving the expected bit-representations of the floating point values.

Interestingly this issue was not caught before during testing because the test suite uses a different method for deriving the Bluespec versions of floating point values that was not used in the public-facing reification. For that reason I provide the example directory that demonstrates the error (because a test would not work).

[ivanperez-keera]

Change Manager: Please rebase on top of latest master.

[tkann-galois]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Can you please make the following changes:

• Remove the commit with the example.
• Make the commit messages follow the same structure and pattern we use for other commits in the project.
• Alphabetize imports where they already are alphabetized.
• Keep code to 80 columns max.
• Align where to 2 spaces, and indent other lines by two spaces.
• Remove unnecessary parentheses.
• Move auxiliary functions below the functions that use them, or even to a where clause.
• Why is Apply being used with a literal string starting with "unpack" with no arguments. Should "unpack" be the Id to which arguments are passed? Should the numeric values be passed as strings part of an ID, rather than literals with a type in Bluespec (using a higher level representation).
• If this code deals with floats (not just doubles), the commit messages should say so (even if it cannot be tested yet).

[ivanperez-keera]

Change Manager: Deviation from Process: I decide to continue reviewing this PR after implementor has updated it, based on discussion with implementor as well as (deleted) notification left at #696 (comment).

[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/277188372

  • The solution proposed produces the expected result. Details:
    The following dockerfile and associated files check that a spec that uses negative zero, infinite and other special Double floating point values generates code that compiles, and runs producing valid values (evaluated by visual inspection), after which it prints the message "Success":

    --- Dockerfile-verify-696
    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 .. \
    && 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 \
    && bsc -sim -g mkTop -u Top.bs \
    && bsc -sim -e mkTop -o mkTop.exe bs_fp.c \
    && ./mkTop.exe -m 4 \
    && echo "Success"
    --- Top.bs
    package Top where
    import SpecialDoubles
    import SpecialDoublesTypes
    mkTop :: Module Empty
    mkTop =
    module
    doublesMod <- mkSpecialDoubles
    rules
    "first": when doublesMod.nan_0_guard ==> do
    let nan_bits = pack doublesMod.nan_0_arg0
    inf_bits = pack doublesMod.inf_1_arg0
    zero_bits = pack doublesMod.zeros_2_arg0
    othr_bits = pack doublesMod.others_3_arg0
    $display "NaN value --- sign: %b exponent: %b silent: %b payload: %b" nan_bits[63:63] nan_bits[62:52] nan_bits[51:51] nan_bits[50:0]
    $display "inf value --- sign: %b exponent: %b mantissa: %b" inf_bits[63:63] inf_bits[62:52] inf_bits[51:0]
    $display "zero value -- sign: %b exponent: %b mantissa: %b" zero_bits[63:63] zero_bits[62:52] zero_bits[51:0]
    $display "other value - sign: %b exponent: %b mantissa: %b" othr_bits[63:63] othr_bits[62:52] othr_bits[51:0]
    $display ""
    --- SpecialDoubles.hs
    {-# LANGUAGE NoImplicitPrelude #-}
    module Main (main) where
    import qualified Copilot.Compile.Bluespec as Bluespec
    import Language.Copilot
    import Numeric.Floating.IEEE.NaN
    main :: IO ()
    main = do
    spec' <- reify spec
    Bluespec.compile "SpecialDoubles" spec'
    spec :: Spec
    spec = do
    trigger "nan" true [arg nans]
    trigger "inf" true [arg infinities]
    trigger "zeros" true [arg zeroes]
    trigger "others" true [arg others]
    nans :: Stream Double
    nans = [setPayload 0, setPayloadSignaling 2] ++ nans
    infinities :: Stream Double
    infinities = [inf, -inf] ++ infinities
    where
    inf :: Double
    inf = read "Infinity"
    zeroes :: Stream Double
    zeroes = [0, -0] ++ zeroes
    others :: Stream Double
    others = [1.0, 2.0, 3.0] ++ others
    

    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=f69f8db70774f78580985797ae6dd67cb864e414 copilot-verify-696
    

• Implementation is documented. Details:
  New auxiliary functions and code include comments.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  Updates not needed; change fixes existing bug.
• Required version bumps are evaluated. Details:
  Bump not needed; change does not affect existing API.