1-- |
2-- Module      :  Cryptol.Backend.Concrete
3-- Copyright   :  (c) 2013-2020 Galois, Inc.
4-- License     :  BSD3
5-- Maintainer  :  cryptol@galois.com
6-- Stability   :  provisional
7-- Portability :  portable
8
9{-# LANGUAGE BangPatterns #-}
10{-# LANGUAGE BlockArguments #-}
11{-# LANGUAGE LambdaCase #-}
12{-# LANGUAGE NamedFieldPuns #-}
13{-# LANGUAGE PatternGuards #-}
14{-# LANGUAGE Rank2Types #-}
15{-# LANGUAGE RecordWildCards #-}
16{-# LANGUAGE ScopedTypeVariables #-}
17{-# LANGUAGE TupleSections #-}
18{-# LANGUAGE TypeFamilies #-}
19{-# LANGUAGE ViewPatterns #-}
20module Cryptol.Backend.Concrete
21  ( BV(..)
22  , binBV
23  , unaryBV
24  , bvVal
25  , ppBV
26  , mkBv
27  , mask
28  , signedBV
29  , signedValue
30  , integerToChar
31  , lg2
32  , Concrete(..)
33  , liftBinIntMod
34  , fpBinArith
35  , fpRoundMode
36  ) where
37
38import qualified Control.Exception as X
39import Data.Bits
40import Data.Ratio
41import Numeric (showIntAtBase)
42import qualified LibBF as FP
43import qualified GHC.Integer.GMP.Internals as Integer
44
45import qualified Cryptol.Backend.Arch as Arch
46import qualified Cryptol.Backend.FloatHelpers as FP
47import Cryptol.Backend
48import Cryptol.Backend.Monad
49import Cryptol.TypeCheck.Solver.InfNat (genLog)
50import Cryptol.Utils.Panic (panic)
51import Cryptol.Utils.PP
52
53data Concrete = Concrete deriving Show
54
55-- | Concrete bitvector values: width, value
56-- Invariant: The value must be within the range 0 .. 2^width-1
57data BV = BV !Integer !Integer
58
59instance Show BV where
60  show = show . bvVal
61
62-- | Apply an integer function to the values of bitvectors.
63--   This function assumes both bitvectors are the same width.
64binBV :: Applicative m => (Integer -> Integer -> Integer) -> BV -> BV -> m BV
65binBV f (BV w x) (BV _ y) = pure $! mkBv w (f x y)
66{-# INLINE binBV #-}
67
68-- | Apply an integer function to the values of a bitvector.
69--   This function assumes the function will not require masking.
70unaryBV :: (Integer -> Integer) -> BV -> BV
71unaryBV f (BV w x) = mkBv w $! f x
72{-# INLINE unaryBV #-}
73
74bvVal :: BV -> Integer
75bvVal (BV _w x) = x
76{-# INLINE bvVal #-}
77
78-- | Smart constructor for 'BV's that checks for the width limit
79mkBv :: Integer -> Integer -> BV
80mkBv w i = BV w (mask w i)
81
82signedBV :: BV -> Integer
83signedBV (BV i x) = signedValue i x
84
85signedValue :: Integer -> Integer -> Integer
86signedValue i x = if testBit x (fromInteger (i-1)) then x - (bit (fromInteger i)) else x
87
88integerToChar :: Integer -> Char
89integerToChar = toEnum . fromInteger
90
91lg2 :: Integer -> Integer
92lg2 i = case genLog i 2 of
93  Just (i',isExact) | isExact   -> i'
94                    | otherwise -> i' + 1
95  Nothing                       -> 0
96
97
98ppBV :: PPOpts -> BV -> Doc
99ppBV opts (BV width i)
100  | base > 36 = integer i -- not sure how to rule this out
101  | asciiMode opts width = text (show (toEnum (fromInteger i) :: Char))
102  | otherwise = prefix <.> text value
103  where
104  base = useBase opts
105
106  padding bitsPerDigit = text (replicate padLen '0')
107    where
108    padLen | m > 0     = d + 1
109           | otherwise = d
110
111    (d,m) = (fromInteger width - (length value * bitsPerDigit))
112                   `divMod` bitsPerDigit
113
114  prefix = case base of
115    2  -> text "0b" <.> padding 1
116    8  -> text "0o" <.> padding 3
117    10 -> empty
118    16 -> text "0x" <.> padding 4
119    _  -> text "0"  <.> char '<' <.> int base <.> char '>'
120
121  value  = showIntAtBase (toInteger base) (digits !!) i ""
122  digits = "0123456789abcdefghijklmnopqrstuvwxyz"
123
124-- Concrete Big-endian Words ------------------------------------------------------------
125
126mask ::
127  Integer  {- ^ Bit-width -} ->
128  Integer  {- ^ Value -} ->
129  Integer  {- ^ Masked result -}
130mask w i | w >= Arch.maxBigIntWidth = wordTooWide w
131         | otherwise                = i .&. (bit (fromInteger w) - 1)
132
133instance Backend Concrete where
134  type SBit Concrete = Bool
135  type SWord Concrete = BV
136  type SInteger Concrete = Integer
137  type SFloat Concrete = FP.BF
138  type SEval Concrete = Eval
139
140  raiseError _ err =
141    do stk <- getCallStack
142       io (X.throwIO (EvalErrorEx stk err))
143
144  assertSideCondition _ True _ = return ()
145  assertSideCondition sym False err = raiseError sym err
146
147  wordLen _ (BV w _) = w
148  wordAsChar _ (BV _ x) = Just $! integerToChar x
149
150  wordBit _ (BV w x) idx = pure $! testBit x (fromInteger (w - 1 - idx))
151
152  wordUpdate _ (BV w x) idx True  = pure $! BV w (setBit   x (fromInteger (w - 1 - idx)))
153  wordUpdate _ (BV w x) idx False = pure $! BV w (clearBit x (fromInteger (w - 1 - idx)))
154
155  isReady _ (Ready _) = True
156  isReady _ _ = False
157
158  mergeEval _sym f c mx my =
159    do x <- mx
160       y <- my
161       f c x y
162
163  sDeclareHole _ = blackhole
164  sDelayFill _ = delayFill
165  sSpark _ = evalSpark
166  sModifyCallStack _ f m = modifyCallStack f m
167  sGetCallStack _ = getCallStack
168
169  bitLit _ b = b
170  bitAsLit _ b = Just b
171
172  bitEq _  x y = pure $! x == y
173  bitOr _  x y = pure $! x .|. y
174  bitAnd _ x y = pure $! x .&. y
175  bitXor _ x y = pure $! x `xor` y
176  bitComplement _ x = pure $! complement x
177
178  iteBit _ b x y  = pure $! if b then x else y
179  iteWord _ b x y = pure $! if b then x else y
180  iteInteger _ b x y = pure $! if b then x else y
181  iteFloat _ b x y   = pure $! if b then x else y
182
183  wordLit _ w i = pure $! mkBv w i
184  wordAsLit _ (BV w i) = Just (w,i)
185  integerLit _ i = pure i
186  integerAsLit _ = Just
187
188  wordToInt _ (BV _ x) = pure x
189  wordFromInt _ w x = pure $! mkBv w x
190
191  packWord _ bits = pure $! BV (toInteger w) a
192    where
193      w = case length bits of
194            len | toInteger len >= Arch.maxBigIntWidth -> wordTooWide (toInteger len)
195                | otherwise                  -> len
196      a = foldl setb 0 (zip [w - 1, w - 2 .. 0] bits)
197      setb acc (n,b) | b         = setBit acc n
198                     | otherwise = acc
199
200  unpackWord _ (BV w a) = pure [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ]
201    where
202      w' = fromInteger w
203
204  joinWord _ (BV i x) (BV j y) =
205    pure $! BV (i + j) (shiftL x (fromInteger j) + y)
206
207  splitWord _ leftW rightW (BV _ x) =
208    pure ( BV leftW (x `shiftR` (fromInteger rightW)), mkBv rightW x )
209
210  extractWord _ n i (BV _ x) = pure $! mkBv n (x `shiftR` (fromInteger i))
211
212  wordEq _ (BV i x) (BV j y)
213    | i == j = pure $! x == y
214    | otherwise = panic "Attempt to compare words of different sizes: wordEq" [show i, show j]
215
216  wordSignedLessThan _ (BV i x) (BV j y)
217    | i == j = pure $! signedValue i x < signedValue i y
218    | otherwise = panic "Attempt to compare words of different sizes: wordSignedLessThan" [show i, show j]
219
220  wordLessThan _ (BV i x) (BV j y)
221    | i == j = pure $! x < y
222    | otherwise = panic "Attempt to compare words of different sizes: wordLessThan" [show i, show j]
223
224  wordGreaterThan _ (BV i x) (BV j y)
225    | i == j = pure $! x > y
226    | otherwise = panic "Attempt to compare words of different sizes: wordGreaterThan" [show i, show j]
227
228  wordAnd _ (BV i x) (BV j y)
229    | i == j = pure $! mkBv i (x .&. y)
230    | otherwise = panic "Attempt to AND words of different sizes: wordPlus" [show i, show j]
231
232  wordOr _ (BV i x) (BV j y)
233    | i == j = pure $! mkBv i (x .|. y)
234    | otherwise = panic "Attempt to OR words of different sizes: wordPlus" [show i, show j]
235
236  wordXor _ (BV i x) (BV j y)
237    | i == j = pure $! mkBv i (x `xor` y)
238    | otherwise = panic "Attempt to XOR words of different sizes: wordPlus" [show i, show j]
239
240  wordComplement _ (BV i x) = pure $! mkBv i (complement x)
241
242  wordPlus _ (BV i x) (BV j y)
243    | i == j = pure $! mkBv i (x+y)
244    | otherwise = panic "Attempt to add words of different sizes: wordPlus" [show i, show j]
245
246  wordNegate _ (BV i x) = pure $! mkBv i (negate x)
247
248  wordMinus _ (BV i x) (BV j y)
249    | i == j = pure $! mkBv i (x-y)
250    | otherwise = panic "Attempt to subtract words of different sizes: wordMinus" [show i, show j]
251
252  wordMult _ (BV i x) (BV j y)
253    | i == j = pure $! mkBv i (x*y)
254    | otherwise = panic "Attempt to multiply words of different sizes: wordMult" [show i, show j]
255
256  wordDiv sym (BV i x) (BV j y)
257    | i == 0 && j == 0 = pure $! mkBv 0 0
258    | i == j =
259        do assertSideCondition sym (y /= 0) DivideByZero
260           pure $! mkBv i (x `div` y)
261    | otherwise = panic "Attempt to divide words of different sizes: wordDiv" [show i, show j]
262
263  wordMod sym (BV i x) (BV j y)
264    | i == 0 && j == 0 = pure $! mkBv 0 0
265    | i == j =
266        do assertSideCondition sym (y /= 0) DivideByZero
267           pure $! mkBv i (x `mod` y)
268    | otherwise = panic "Attempt to mod words of different sizes: wordMod" [show i, show j]
269
270  wordSignedDiv sym (BV i x) (BV j y)
271    | i == 0 && j == 0 = pure $! mkBv 0 0
272    | i == j =
273        do assertSideCondition sym (y /= 0) DivideByZero
274           let sx = signedValue i x
275               sy = signedValue i y
276           pure $! mkBv i (sx `quot` sy)
277    | otherwise = panic "Attempt to divide words of different sizes: wordSignedDiv" [show i, show j]
278
279  wordSignedMod sym (BV i x) (BV j y)
280    | i == 0 && j == 0 = pure $! mkBv 0 0
281    | i == j =
282        do assertSideCondition sym (y /= 0) DivideByZero
283           let sx = signedValue i x
284               sy = signedValue i y
285           pure $! mkBv i (sx `rem` sy)
286    | otherwise = panic "Attempt to mod words of different sizes: wordSignedMod" [show i, show j]
287
288  wordLg2 _ (BV i x) = pure $! mkBv i (lg2 x)
289
290  intEq _ x y = pure $! x == y
291  intLessThan _ x y = pure $! x < y
292  intGreaterThan _ x y = pure $! x > y
293
294  intPlus  _ x y = pure $! x + y
295  intMinus _ x y = pure $! x - y
296  intNegate _ x  = pure $! negate x
297  intMult  _ x y = pure $! x * y
298  intDiv sym x y =
299    do assertSideCondition sym (y /= 0) DivideByZero
300       pure $! x `div` y
301  intMod sym x y =
302    do assertSideCondition sym (y /= 0) DivideByZero
303       pure $! x `mod` y
304
305  intToZn _ 0 _ = evalPanic "intToZn" ["0 modulus not allowed"]
306  intToZn _ m x = pure $! x `mod` m
307
308  -- NB: requires we maintain the invariant that
309  --     Z_n is in reduced form
310  znToInt _ _m x = pure x
311  znEq _ _m x y = pure $! x == y
312
313  -- NB: under the precondition that `m` is prime,
314  -- the only values for which no inverse exists are
315  -- congruent to 0 modulo m.
316  znRecip sym m x
317    | r == 0    = raiseError sym DivideByZero
318    | otherwise = pure r
319   where
320     r = Integer.recipModInteger x m
321
322  znPlus  _ = liftBinIntMod (+)
323  znMinus _ = liftBinIntMod (-)
324  znMult  _ = liftBinIntMod (*)
325  znNegate _ 0 _ = evalPanic "znNegate" ["0 modulus not allowed"]
326  znNegate _ m x = pure $! (negate x) `mod` m
327
328  ------------------------------------------------------------------------
329  -- Floating Point
330  fpLit _sym e p rat     = pure (FP.fpLit e p rat)
331
332  fpNaN _sym e p         = pure (FP.BF e p FP.bfNaN)
333  fpPosInf _sym e p      = pure (FP.BF e p FP.bfPosInf)
334
335  fpAsLit _ f            = Just f
336  fpExactLit _sym bf     = pure bf
337  fpEq _sym x y          = pure (FP.bfValue x == FP.bfValue y)
338  fpLogicalEq _sym x y   = pure (FP.bfCompare (FP.bfValue x) (FP.bfValue y) == EQ)
339  fpLessThan _sym x y    = pure (FP.bfValue x <  FP.bfValue y)
340  fpGreaterThan _sym x y = pure (FP.bfValue x >  FP.bfValue y)
341  fpPlus  = fpBinArith FP.bfAdd
342  fpMinus = fpBinArith FP.bfSub
343  fpMult  = fpBinArith FP.bfMul
344  fpDiv   = fpBinArith FP.bfDiv
345  fpNeg _ x = pure $! x { FP.bfValue = FP.bfNeg (FP.bfValue x) }
346
347  fpAbs _ x = pure $! x { FP.bfValue = FP.bfAbs (FP.bfValue x) }
348  fpSqrt sym r x =
349    do r' <- fpRoundMode sym r
350       let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) r'
351       pure $! x{ FP.bfValue = FP.fpCheckStatus (FP.bfSqrt opts (FP.bfValue x)) }
352
353  fpFMA sym r x y z =
354    do r' <- fpRoundMode sym r
355       let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) r'
356       pure $! x { FP.bfValue = FP.fpCheckStatus (FP.bfFMA opts (FP.bfValue x) (FP.bfValue y) (FP.bfValue z)) }
357
358  fpIsZero _ x = pure (FP.bfIsZero (FP.bfValue x))
359  fpIsNeg _ x  = pure (FP.bfIsNeg (FP.bfValue x))
360  fpIsNaN _ x  = pure (FP.bfIsNaN (FP.bfValue x))
361  fpIsInf _ x  = pure (FP.bfIsInf (FP.bfValue x))
362  fpIsNorm _ x =
363    let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) FP.NearEven
364     in pure (FP.bfIsNormal opts (FP.bfValue x))
365  fpIsSubnorm _ x =
366    let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) FP.NearEven
367     in pure (FP.bfIsSubnormal opts (FP.bfValue x))
368
369  fpFromBits _sym e p bv = pure (FP.floatFromBits e p (bvVal bv))
370  fpToBits _sym (FP.BF e p v) = pure (mkBv (e+p) (FP.floatToBits e p v))
371
372  fpFromInteger sym e p r x =
373    do r' <- fpRoundMode sym r
374       pure FP.BF { FP.bfExpWidth = e
375                  , FP.bfPrecWidth = p
376                  , FP.bfValue = FP.fpCheckStatus $
377                                 FP.bfRoundInt r' (FP.bfFromInteger x)
378                  }
379  fpToInteger = fpCvtToInteger
380
381  fpFromRational sym e p r x =
382    do mode <- fpRoundMode sym r
383       pure (FP.floatFromRational e p mode (sNum x % sDenom x))
384
385  fpToRational sym fp =
386      case FP.floatToRational "fpToRational" fp of
387        Left err -> raiseError sym err
388        Right r  -> pure $ SRational { sNum = numerator r, sDenom = denominator r }
389
390{-# INLINE liftBinIntMod #-}
391liftBinIntMod :: Monad m =>
392  (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer
393liftBinIntMod op m x y
394  | m == 0    = evalPanic "znArithmetic" ["0 modulus not allowed"]
395  | otherwise = pure $ (op x y) `mod` m
396
397
398
399{-# INLINE fpBinArith #-}
400fpBinArith ::
401  (FP.BFOpts -> FP.BigFloat -> FP.BigFloat -> (FP.BigFloat, FP.Status)) ->
402  Concrete ->
403  SWord Concrete  {- ^ Rouding mode -} ->
404  SFloat Concrete ->
405  SFloat Concrete ->
406  SEval Concrete (SFloat Concrete)
407fpBinArith fun = \sym r x y ->
408  do opts <- FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x)
409                                                  <$> fpRoundMode sym r
410     pure $! x { FP.bfValue = FP.fpCheckStatus
411                                (fun opts (FP.bfValue x) (FP.bfValue y)) }
412
413fpCvtToInteger ::
414  Concrete ->
415  String ->
416  SWord Concrete {- ^ Rounding mode -} ->
417  SFloat Concrete ->
418  SEval Concrete (SInteger Concrete)
419fpCvtToInteger sym fun rnd flt =
420  do mode <- fpRoundMode sym rnd
421     case FP.floatToInteger fun mode flt of
422       Right i -> pure i
423       Left err -> raiseError sym err
424
425fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete FP.RoundMode
426fpRoundMode sym w =
427  case FP.fpRound (bvVal w) of
428    Left err -> raiseError sym err
429    Right a  -> pure a
430