`copilot-bluespec`: Special floating-point values are translated to syntactically invalid Bluespec code

[RyanGlScott]

Description

copilot-bluespec currently generates syntactically invalid Bluespec code for special floating-point values, such as negative zero, infinity, and NaN values. For instance, it compiles infinity values to Infinity, which is not a valid Bluespec floating-point value.

Type

• Bug: incorrect generated code.

Additional context

None.

Requester

• Ryan Scott (Galois)

Method to check presence of bug

Take the following Copilot specification, which defines a stream containing an infinity value:

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

import Language.Copilot
import Copilot.Compile.Bluespec (compile)

inf :: Stream Double
inf = constant (1/0)

spec :: Spec
spec = trigger "trig" true [arg inf]

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

Compile this to Bluespec code:

$ runghc NegativeZero.hs

Then attempt to compile the generated Bluespec code. This will fail with a syntax error:

$ bsc -sim -g mkInfinity -u Infinity.bs
<snip>
compiling Infinity.bs
Error: "Infinity.bs", line 27, column 26: (T0003)
  Unbound constructor `Infinity'

Expected result

The generated Bluespec program should compile.

Desired result

The generated Bluespec program should compile.

Proposed solution

Add special cases to copilot-bluespec's constFP, to handle floating-point values ensuring that they are correctly translated to Bluespec code.

Add test cases to copilot-bluespec demonstrating correct translation for various special floating-point values.

Further notes

• copilot-bluespec already has special cases to handle specific floating point values (here).

• The new test cases will only work end-to-end for Doubles for now, as end-to-end test cases for Float would not work until copilot-{bluespec,theorem}: Special Float values are translated incorrectly #697 is resolved.

[ivanperez-keera]

Change Manager: Modified description to clarify proposed solution.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.