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