copilot-theorem: Correctly display special Float values in counterexamples. Refs #697.

`copilot-theorem`'s counterexample-reporting machinery up-casts `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-theorem` to generate incorrect counterexamples when
these special values are involved.

This commit removes the use of `realToFrac` in favor of an alternative approach
based on `GHC.Float.double2Float`, which correctly handles most special
floating-point values. A notable exception is NaN values, as `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.

Co-authored-by: Ryan Scott <rscott@galois.com>

Author: tkann-galois

copilot-theorem/copilot-theorem.cabal

@@ -51,6 +51,7 @@ library
                           , containers            >= 0.4 && < 0.9
                           , data-default          >= 0.7 && < 0.9
                           , directory             >= 1.3 && < 1.4
+                          , fp-ieee               >= 0.1 && < 0.2
                           , libBF                 >= 0.6.2 && < 0.7
                           , mtl                   >= 2.0 && < 2.4
                           , panic                 >= 0.4.0 && < 0.5

copilot-theorem/src/Copilot/Theorem/What4.hs

@@ -77,8 +77,9 @@ import Data.Parameterized.NatRepr
 import Data.Parameterized.Nonce
 import Data.Parameterized.Some
 import qualified Data.Parameterized.Vector as V
-import GHC.Float (castWord32ToFloat, castWord64ToDouble)
+import GHC.Float (castWord32ToFloat, castWord64ToDouble, double2Float)
 import LibBF (BigFloat, bfToDouble, pattern NearEven)
+import Numeric.Floating.IEEE.NaN (getPayload, isSignaling, setPayload, setPayloadSignaling)
 import qualified Panic as Panic
 
 import Copilot.Theorem.What4.Translate
@@ -707,7 +708,7 @@ valFromExpr ge xe = case xe of
   XFloat e ->
     Some . CopilotValue CT.Float <$>
       iFloatGroundEval WFP.SingleFloatRepr e
-                       (realToFrac . fst . bfToDouble NearEven)
+                       (nanSafeDoubleToFloat . fst . bfToDouble NearEven)
                        fromRational
                        (castWord32ToFloat . fromInteger . BV.asUnsigned)
   XDouble e ->
@@ -757,3 +758,22 @@ valFromExpr ge xe = case xe of
         WB.FloatIEEERepr          -> ieeeK <$> WG.groundEval ge e
         WB.FloatRealRepr          -> realK <$> WG.groundEval ge e
         WB.FloatUninterpretedRepr -> uninterpK <$> WG.groundEval ge e
+
+    -- Convert a Double to a Float. This function takes care to preserve
+    -- special floating-point values, such as negative zero, infinity, and NaN
+    -- values.
+    nanSafeDoubleToFloat :: Double -> Float
+    nanSafeDoubleToFloat x
+      | isNaN x   = convertDoubleNaNToFloatNan x
+      | otherwise = double2Float x
+      where
+        payload :: Float
+        payload = double2Float $ getPayload x
+
+        -- double2Float does not preserve the payloads of NaN values, so we
+        -- include a special case for translating NaNs.
+        convertDoubleNaNToFloatNan :: Double -> Float
+        convertDoubleNaNToFloatNan nan =
+          if isSignaling nan
+            then setPayloadSignaling payload
+            else setPayload payload