1{-# Language DataKinds #-}
2{-# Language FlexibleContexts #-}
3{-# Language GADTs #-}
4{-# Language RankNTypes #-}
5{-# Language TypeApplications #-}
6{-# Language TypeOperators #-}
7
8-- | Working with floats of dynamic sizes.
9module What4.SFloat
10  ( -- * Interface
11    SFloat(..)
12  , fpReprOf
13  , fpSize
14  , fpRepr
15  , fpAsLit
16  , fpIte
17
18    -- * Constants
19  , fpFresh
20  , fpNaN
21  , fpPosInf
22  , fpNegInf
23  , fpFromLit
24  , fpFromRationalLit
25
26    -- * Interchange formats
27  , fpFromBinary
28  , fpToBinary
29
30    -- * Relations
31  , SFloatRel
32  , fpEq
33  , fpEqIEEE
34  , fpLtIEEE
35  , fpGtIEEE
36
37    -- * Arithmetic
38  , SFloatBinArith
39  , fpNeg
40  , fpAbs
41  , fpSqrt
42  , fpAdd
43  , fpSub
44  , fpMul
45  , fpDiv
46  , fpMin
47  , fpMax
48  , fpFMA
49
50    -- * Conversions
51  , fpRound
52  , fpToReal
53  , fpFromReal
54  , fpFromRational
55  , fpToRational
56  , fpFromInteger
57
58    -- * Queries
59  , fpIsInf
60  , fpIsNaN
61  , fpIsZero
62  , fpIsNeg
63  , fpIsSubnorm
64  , fpIsNorm
65
66  -- * Exceptions
67  , UnsupportedFloat(..)
68  , FPTypeError(..)
69  ) where
70
71import Control.Exception
72import LibBF (BigFloat)
73
74import Data.Parameterized.Some
75import Data.Parameterized.NatRepr
76
77import What4.BaseTypes
78import What4.Panic(panic)
79import What4.SWord
80import What4.Interface
81
82-- | Symbolic floating point numbers.
83data SFloat sym where
84  SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym
85
86
87
88--------------------------------------------------------------------------------
89
90-- | This exception is thrown if the operations try to create a
91-- floating point value we do not support
92data UnsupportedFloat =
93  UnsupportedFloat { fpWho :: String, exponentBits, precisionBits :: Integer }
94  deriving Show
95
96
97-- | Throw 'UnsupportedFloat' exception
98unsupported ::
99  String  {- ^ Label -} ->
100  Integer {- ^ Exponent width -} ->
101  Integer {- ^ Precision width -} ->
102  IO a
103unsupported l e p =
104  throwIO UnsupportedFloat { fpWho         = l
105                           , exponentBits  = e
106                           , precisionBits = p }
107
108instance Exception UnsupportedFloat
109
110-- | This exceptoin is throws if the types don't match.
111data FPTypeError =
112  FPTypeError { fpExpected :: Some BaseTypeRepr
113              , fpActual   :: Some BaseTypeRepr
114              }
115    deriving Show
116
117instance Exception FPTypeError
118
119fpTypeMismatch :: BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
120fpTypeMismatch expect actual =
121  throwIO FPTypeError { fpExpected = Some expect
122                      , fpActual   = Some actual
123                      }
124fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
125fpTypeError t1 t2 =
126  fpTypeMismatch (BaseFloatRepr t1) (BaseFloatRepr t2)
127
128
129--------------------------------------------------------------------------------
130-- | Construct the 'FloatPrecisionRepr' with the given parameters.
131fpRepr ::
132  Integer {- ^ Exponent width -} ->
133  Integer {- ^ Precision width -} ->
134  Maybe (Some FloatPrecisionRepr)
135fpRepr iE iP =
136  do Some e    <- someNat iE
137     LeqProof  <- testLeq (knownNat @2) e
138     Some p    <- someNat iP
139     LeqProof  <- testLeq (knownNat @2) p
140     pure (Some (FloatingPointPrecisionRepr e p))
141
142fpReprOf ::
143  IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
144fpReprOf _ e =
145  case exprType e of
146    BaseFloatRepr r -> r
147
148fpSize :: SFloat sym -> (Integer,Integer)
149fpSize (SFloat f) =
150  case exprType f of
151    BaseFloatRepr (FloatingPointPrecisionRepr e p) -> (intValue e, intValue p)
152
153fpAsLit :: SFloat sym -> Maybe BigFloat
154fpAsLit (SFloat f) = asFloat f
155
156--------------------------------------------------------------------------------
157-- Constants
158
159-- | A fresh variable of the given type.
160fpFresh ::
161  IsSymExprBuilder sym =>
162  sym ->
163  Integer ->
164  Integer ->
165  IO (SFloat sym)
166fpFresh sym e p
167  | Just (Some fpp) <- fpRepr e p =
168    SFloat <$> freshConstant sym emptySymbol (BaseFloatRepr fpp)
169  | otherwise = unsupported "fpFresh" e p
170
171-- | Not a number
172fpNaN ::
173  IsExprBuilder sym =>
174  sym ->
175  Integer {- ^ Exponent width -} ->
176  Integer {- ^ Precision width -} ->
177  IO (SFloat sym)
178fpNaN sym e p
179  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatNaN sym fpp
180  | otherwise = unsupported "fpNaN" e p
181
182
183-- | Positive infinity
184fpPosInf ::
185  IsExprBuilder sym =>
186  sym ->
187  Integer {- ^ Exponent width -} ->
188  Integer {- ^ Precision width -} ->
189  IO (SFloat sym)
190fpPosInf sym e p
191  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatPInf sym fpp
192  | otherwise = unsupported "fpPosInf" e p
193
194-- | Negative infinity
195fpNegInf ::
196  IsExprBuilder sym =>
197  sym ->
198  Integer {- ^ Exponent width -} ->
199  Integer {- ^ Precision width -} ->
200  IO (SFloat sym)
201fpNegInf sym e p
202  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatNInf sym fpp
203  | otherwise = unsupported "fpNegInf" e p
204
205
206-- | A floating point number corresponding to the given BigFloat.
207fpFromLit ::
208  IsExprBuilder sym =>
209  sym ->
210  Integer {- ^ Exponent width -} ->
211  Integer {- ^ Precision width -} ->
212  BigFloat ->
213  IO (SFloat sym)
214fpFromLit sym e p f
215  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatLit sym fpp f
216  | otherwise = unsupported "fpFromLit" e p
217
218-- | A floating point number corresponding to the given rational.
219fpFromRationalLit ::
220  IsExprBuilder sym =>
221  sym ->
222  Integer {- ^ Exponent width -} ->
223  Integer {- ^ Precision width -} ->
224  Rational ->
225  IO (SFloat sym)
226fpFromRationalLit sym e p r
227  | Just (Some fpp) <- fpRepr e p = SFloat <$> floatLitRational sym fpp r
228  | otherwise = unsupported "fpFromRationalLit" e p
229
230
231-- | Make a floating point number with the given bit representation.
232fpFromBinary ::
233  IsExprBuilder sym =>
234  sym ->
235  Integer {- ^ Exponent width -} ->
236  Integer {- ^ Precision width -} ->
237  SWord sym ->
238  IO (SFloat sym)
239fpFromBinary sym e p swe
240  | DBV sw <- swe
241  , Just (Some fpp) <- fpRepr e p
242  , FloatingPointPrecisionRepr ew pw <- fpp
243  , let expectW = addNat ew pw
244  , actual@(BaseBVRepr actualW)  <- exprType sw =
245    case testEquality expectW actualW of
246      Just Refl -> SFloat <$> floatFromBinary sym fpp sw
247      Nothing -- we want to report type correct type errors! :-)
248        | Just LeqProof <- testLeq (knownNat @1) expectW ->
249                fpTypeMismatch (BaseBVRepr expectW) actual
250        | otherwise -> panic "fpFromBits" [ "1 >= 2" ]
251  | otherwise = unsupported "fpFromBits" e p
252
253fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
254fpToBinary sym (SFloat f)
255  | FloatingPointPrecisionRepr e p <- fpReprOf sym f
256  , Just LeqProof <- testLeq (knownNat @1) (addNat e p)
257    = DBV <$> floatToBinary sym f
258  | otherwise = panic "fpToBinary" [ "we messed up the types" ]
259
260
261--------------------------------------------------------------------------------
262-- Arithmetic
263
264fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
265fpNeg sym (SFloat fl) = SFloat <$> floatNeg sym fl
266
267fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
268fpAbs sym (SFloat fl) = SFloat <$> floatAbs sym fl
269
270fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
271fpSqrt sym r (SFloat fl) = SFloat <$> floatSqrt sym r fl
272
273fpBinArith ::
274  IsExprBuilder sym =>
275  (forall t.
276      sym ->
277      RoundingMode ->
278      SymFloat sym t ->
279      SymFloat sym t ->
280      IO (SymFloat sym t)
281  ) ->
282  sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
283fpBinArith fun sym r (SFloat x) (SFloat y) =
284  let t1 = sym `fpReprOf` x
285      t2 = sym `fpReprOf` y
286  in
287  case testEquality t1 t2 of
288    Just Refl -> SFloat <$> fun sym r x y
289    _         -> fpTypeError t1 t2
290
291type SFloatBinArith sym =
292  sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
293
294fpAdd :: IsExprBuilder sym => SFloatBinArith sym
295fpAdd = fpBinArith floatAdd
296
297fpSub :: IsExprBuilder sym => SFloatBinArith sym
298fpSub = fpBinArith floatSub
299
300fpMul :: IsExprBuilder sym => SFloatBinArith sym
301fpMul = fpBinArith floatMul
302
303fpDiv :: IsExprBuilder sym => SFloatBinArith sym
304fpDiv = fpBinArith floatDiv
305
306fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
307fpMin sym (SFloat x) (SFloat y) =
308  let t1 = sym `fpReprOf` x
309      t2 = sym `fpReprOf` y
310  in
311  case testEquality t1 t2 of
312    Just Refl -> SFloat <$> floatMin sym x y
313    _         -> fpTypeError t1 t2
314
315fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
316fpMax sym (SFloat x) (SFloat y) =
317  let t1 = sym `fpReprOf` x
318      t2 = sym `fpReprOf` y
319  in
320  case testEquality t1 t2 of
321    Just Refl -> SFloat <$> floatMax sym x y
322    _         -> fpTypeError t1 t2
323
324fpFMA :: IsExprBuilder sym =>
325  sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
326fpFMA sym r (SFloat x) (SFloat y) (SFloat z) =
327  let t1 = sym `fpReprOf` x
328      t2 = sym `fpReprOf` y
329      t3 = sym `fpReprOf` z
330   in
331   case (testEquality t1 t2, testEquality t2 t3) of
332     (Just Refl, Just Refl) -> SFloat <$> floatFMA sym r x y z
333     (Nothing, _) -> fpTypeError t1 t2
334     (_, Nothing) -> fpTypeError t2 t3
335
336fpIte :: IsExprBuilder sym =>
337  sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
338fpIte sym p (SFloat x) (SFloat y) =
339  let t1 = sym `fpReprOf` x
340      t2 = sym `fpReprOf` y
341  in
342  case testEquality t1 t2 of
343    Just Refl -> SFloat <$> floatIte sym p x y
344    _         -> fpTypeError t1 t2
345
346--------------------------------------------------------------------------------
347
348fpRel ::
349  IsExprBuilder sym =>
350  (forall t.
351    sym ->
352    SymFloat sym t ->
353    SymFloat sym t ->
354    IO (Pred sym)
355  ) ->
356  sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
357fpRel fun sym (SFloat x) (SFloat y) =
358  let t1 = sym `fpReprOf` x
359      t2 = sym `fpReprOf` y
360  in
361  case testEquality t1 t2 of
362    Just Refl -> fun sym x y
363    _         -> fpTypeError t1 t2
364
365
366
367
368type SFloatRel sym =
369  sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
370
371fpEq :: IsExprBuilder sym => SFloatRel sym
372fpEq = fpRel floatEq
373
374fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
375fpEqIEEE = fpRel floatFpEq
376
377fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
378fpLtIEEE = fpRel floatLt
379
380fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
381fpGtIEEE = fpRel floatGt
382
383
384--------------------------------------------------------------------------------
385fpRound ::
386  IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
387fpRound sym r (SFloat x) = SFloat <$> floatRound sym r x
388
389-- | This is undefined on "special" values (NaN,infinity)
390fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)
391fpToReal sym (SFloat x) = floatToReal sym x
392
393fpFromReal ::
394  IsExprBuilder sym =>
395  sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)
396fpFromReal sym e p r x
397  | Just (Some repr) <- fpRepr e p = SFloat <$> realToFloat sym repr r x
398  | otherwise = unsupported "fpFromReal" e p
399
400
401fpFromInteger ::
402  IsExprBuilder sym =>
403  sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)
404fpFromInteger sym e p r x = fpFromReal sym e p r =<< integerToReal sym x
405
406
407fpFromRational ::
408  IsExprBuilder sym =>
409  sym -> Integer -> Integer -> RoundingMode ->
410  SymInteger sym -> SymInteger sym -> IO (SFloat sym)
411fpFromRational sym e p r x y =
412  do num <- integerToReal sym x
413     den <- integerToReal sym y
414     res <- realDiv sym num den
415     fpFromReal sym e p r res
416
417{- | Returns a predicate and two integers, @x@ and @y@.
418If the the predicate holds, then @x / y@ is a rational representing
419the floating point number. Assumes the FP number is not one of the
420special ones that has no real representation. -}
421fpToRational ::
422  IsSymExprBuilder sym =>
423  sym ->
424  SFloat sym ->
425  IO (Pred sym, SymInteger sym, SymInteger sym)
426fpToRational sym fp =
427  do r    <- fpToReal sym fp
428     x    <- freshConstant sym emptySymbol BaseIntegerRepr
429     y    <- freshConstant sym emptySymbol BaseIntegerRepr
430     num  <- integerToReal sym x
431     den  <- integerToReal sym y
432     res  <- realDiv sym num den
433     same <- realEq sym r res
434     pure (same, x, y)
435
436
437
438--------------------------------------------------------------------------------
439fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
440fpIsInf sym (SFloat x) = floatIsInf sym x
441
442fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
443fpIsNaN sym (SFloat x) = floatIsNaN sym x
444
445fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
446fpIsZero sym (SFloat x) = floatIsZero sym x
447
448fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
449fpIsNeg sym (SFloat x) = floatIsNeg sym x
450
451fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
452fpIsSubnorm sym (SFloat x) = floatIsSubnorm sym x
453
454fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
455fpIsNorm sym (SFloat x) = floatIsNorm sym x
456