Incorrect signum translation

[RyanGlScott]

copilot-bluespec incorrectly translates the Copilot signum function to Bluespec.

signum @Int8

In Copilot, signum @Int8 0 should return 0. In Bluespec, however, it returns 1:

package Top where

mkTop :: Module Empty
mkTop =
  module
    rules
      "step": when True ==> do
        let x :: Int 8
            x = 0
        $display "%d\n" (signum x)
        $finish

$ bsc -sim -g mkTop -u Top.bs
checking package dependencies
compiling Top.bs
code generation for mkTop starts
Elaborated module file created: mkTop.ba
All packages are up to date.

$ bsc -sim -e mkTop -o mkTop
Bluesim object created: mkTop.{h,o}
Bluesim object created: model_mkTop.{h,o}
Simulation shared library created: mkTop.so
Simulation executable created: mkTop

$ ./mkTop
   1

signum @Double

In Copilot, signum @Double x returns x whenever x is 0.0, -0.0, or NaN. In Bluespec, however, it will return 1.0 if the sign bit is clear and -1.0 if the sign bit is set. Here are some examples demonstrating this in action:

package Top where

import FloatingPoint

mkTop :: Module Empty
mkTop =
  module
    rules
      "step": when True ==> do
        let x1 :: Double
            x1 = 0.0
        $display "%x\n" (signum x1)
        let x2 :: Double
            x2 = negate 0.0
        $display "%x\n" (signum x2)
        let x3 :: Double
            x3 = qnan
        $display "%x\n" (signum x3)
        let x4 :: Double
            x4 = negate qnan
        $display "%x\n" (signum x4)
        $finish

$ bsc -sim -g mkTop -u Top.bs
checking package dependencies
compiling Top.bs
code generation for mkTop starts
Elaborated module file created: mkTop.ba
All packages are up to date.

$ bsc -sim -e mkTop -o mkTop
Bluesim object created: mkTop.{h,o}
Bluesim object created: model_mkTop.{h,o}
Simulation shared library created: mkTop.so
Simulation executable created: mkTop

$ ./mkTop
3ff0000000000000

bff0000000000000

3ff0000000000000

bff0000000000000

(Note that 0x3ff0000000000000 is the hexadecimal representation of 1.0 :: Double as bits, and 0xbff0000000000000 is the hexadecimal representation of -1.0 :: Double as bits.)

Proposed fix

In order to make these translations faithful to Copilot's semantics, I think we will need to translate signum e to something like if e > 0 then 1 else (if e < 0 then -1 else e) in Bluespec. This is similar to how copilot-c99 translates signum (see this code).

[RyanGlScott]

I attempted the if e > 0 then 1 else (if e < 0 then -1 else e) fix as above, but that led me to discover another strange Bluespec quirk: compiling e > 0 (where e is a Double) will cause a Bluespec evaluation-time error. This time, I'm wondering if Bluespec is at fault. I've opened B-Lang-org/bsc#711 to discuss this.

[RyanGlScott]

It turns out that the evaluation-time error is expected behavior—see B-Lang-org/bsc#711 (comment). As such, I will need to redefine <, <=, >, and >= such that instead of erroring when one of the arguments is a NaN, they instead return False (as is the case in Copilot). For example, I think we should translate the Copilot expression x < y to compareFP x y == LT in Bluespec (where compareFP is defined here).

[RyanGlScott]

I've opened #15 to track the (<) issue mentioned above, as it is really a separate problem.

[RyanGlScott]

Fixed in #17.