E4M3: Handle encoding of out-of-bounds and ieee values

Golds/encodeE4M3_in1.gold

@@ -0,0 +1,15 @@
+Arguments: -fe4m3 -- -448.0001
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = NaN :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 0 1111 111
+      Hex layout: 7F
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Positive
+        Exponent: 8 (Stored: 15, Bias: 7)
+  Classification: FP_NAN (Quiet)
+           Value: NaN
+            Note: The input value -448.0001 is out of bounds, and hence becomes NaN
+                  The representable range is [-448, 448]

Golds/encodeE4M3_in2.gold

@@ -0,0 +1,15 @@
+Arguments: -fe4m3 --  448.0001
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = NaN :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 0 1111 111
+      Hex layout: 7F
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Positive
+        Exponent: 8 (Stored: 15, Bias: 7)
+  Classification: FP_NAN (Quiet)
+           Value: NaN
+            Note: The input value 448.0001 is out of bounds, and hence becomes NaN
+                  The representable range is [-448, 448]

Golds/encodeE4M3_in3.gold

@@ -0,0 +1,16 @@
+Arguments: -fe4m3 -- -239.9999
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = -240 :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 1 1110 111
+      Hex layout: F7
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Negative
+        Exponent: 7 (Stored: 14, Bias: 7)
+  Classification: FP_NORMAL
+          Binary: -0b1.111p7
+           Octal: -0o3.6p6
+         Decimal: -240
+             Hex: -0xfp4

Golds/encodeE4M3_in4.gold

@@ -0,0 +1,16 @@
+Arguments: -fe4m3 --  239.9999
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = 240 :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 0 1110 111
+      Hex layout: 77
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Positive
+        Exponent: 7 (Stored: 14, Bias: 7)
+  Classification: FP_NORMAL
+          Binary: 0b1.111p7
+           Octal: 0o3.6p6
+         Decimal: 240
+             Hex: 0xfp4

Golds/encodeE4M3_in5.gold

@@ -0,0 +1,16 @@
+Arguments: -fe4m3 --  0
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = 0.0 :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 0 0000 000
+      Hex layout: 00
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Positive
+        Exponent: -7 (Stored: 0, Bias: 7)
+  Classification: FP_ZERO
+          Binary: 0b0.0
+           Octal: 0o0.0
+         Decimal: 0.0
+             Hex: 0x0

Golds/encodeE4M3_in6.gold

@@ -0,0 +1,16 @@
+Arguments: -fe4m3 --  -0
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = -0.0 :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 1 0000 000
+      Hex layout: 80
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Negative
+        Exponent: -7 (Stored: 0, Bias: 7)
+  Classification: FP_ZERO
+          Binary: -0b0.0
+           Octal: -0o0.0
+         Decimal: -0.0
+             Hex: -0o0

src/CrackNum/Main.hs

@@ -615,19 +615,35 @@ encodeE4M3 debug inp = case reads (fixup True inp) of
        fixNaN s | "Representation for NaN's is not unique" `isInfixOf` s = []
                 | True                                                   = [s]
 
+       -- bounds representable in E4M3 are -448 to 448
+       isOutOfBounds :: Double -> Bool
+       isOutOfBounds v = abs v > 448
+
+       -- For values in this bound, we can treat it as FP 4 4
+       isIEEESemantics :: Double -> Bool
+       isIEEESemantics v = abs v <= 240
+
+       getNaN = satWith config{crackNumSurfaceVals = [("ENCODED", 0x7F)]} $
+                              do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED"
+                                 constrain $ fpIsNaN x
+
        analyze :: Double -> IO ()
        analyze v
          -- NaN has two representations, with surface value S.1111.111; we use 0x7F for simplicity
          | isNaN v
-         = do res <- satWith config{crackNumSurfaceVals = [("ENCODED", 0x7F)]}
-                             (do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED"
-                                 constrain $ fpIsNaN x)
-              putStrLn $ onEach fixNaN $ fixEncoded res
+         = getNaN >>= putStrLn . onEach fixNaN . fixEncoded
          | isInfinite v
-         = do res <- satWith config{crackNumSurfaceVals = [("ENCODED", 0x7F)]}
-                             (do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED"
-                                 constrain $ fpIsNaN x)
-              putStrLn $ onEach fixNaN $ fixEncoded res
+         = do getNaN >>= putStrLn . onEach fixNaN . fixEncoded
               putStrLn "            Note: The input value was infinite, which is not representable in E4M3."
+         | isOutOfBounds v -- becomes NaN
+         = do getNaN >>= putStrLn . onEach fixNaN . fixEncoded
+              putStrLn $ "            Note: The input value " ++ show v ++ " is out of bounds, and hence becomes NaN"
+              putStrLn $ "                  The representable range is [-448, 448]"
+         | isIEEESemantics v -- can just decode as usual
+         = do res <- satWith config $ do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED"
+                                         constrain $ x .== fromSDouble sRNE (literal v)
+              putStrLn $ fixEncoded res
          | True
-         = error "not supported yet"
+         -- We're in the tricky range between (-448, -240) OR (240, 448)
+         -- Need to find the matching value
+         = error $ "not supported yet" ++ show v

src/CrackNum/TestSuite.hs

@@ -73,6 +73,12 @@ tests = testGroup "CrackNum" [
                gold "encodeE4M3_nan"  "-fe4m3    nan"
             ,  gold "encodeE4M3_+inf" "-fe4m3    inf"
             ,  gold "encodeE4M3_-inf" "-fe4m3 -- -inf"
+            ,  gold "encodeE4M3_in1"  "-fe4m3 -- -448.0001"
+            ,  gold "encodeE4M3_in2"  "-fe4m3 --  448.0001"
+            ,  gold "encodeE4M3_in3"  "-fe4m3 -- -239.9999"
+            ,  gold "encodeE4M3_in4"  "-fe4m3 --  239.9999"
+            ,  gold "encodeE4M3_in5"  "-fe4m3 --  0"
+            ,  gold "encodeE4M3_in6"  "-fe4m3 --  -0"
             ]
           , testGroup "Decode" [
                gold "decode0" "-i4       0b0110"