1-- | 2-- Module : Cryptol.Backend.What4 3-- Copyright : (c) 2020 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6 7{-# LANGUAGE BlockArguments #-} 8{-# LANGUAGE DeriveFunctor #-} 9{-# LANGUAGE ExistentialQuantification #-} 10{-# LANGUAGE LambdaCase #-} 11{-# LANGUAGE MultiWayIf #-} 12{-# LANGUAGE ScopedTypeVariables #-} 13{-# LANGUAGE TypeFamilies #-} 14{-# LANGUAGE ViewPatterns #-} 15module Cryptol.Backend.What4 where 16 17 18import qualified Control.Exception as X 19import Control.Concurrent.MVar 20import Control.Monad (foldM,ap,liftM) 21import Control.Monad.IO.Class 22import Data.Bits (bit) 23import qualified Data.BitVector.Sized as BV 24import Data.List 25import Data.Map (Map) 26import Data.Set (Set) 27import Data.Text (Text) 28import Data.Parameterized.NatRepr 29import Data.Parameterized.Some 30 31import qualified GHC.Integer.GMP.Internals as Integer 32 33import qualified What4.Interface as W4 34import qualified What4.SWord as SW 35import qualified What4.SFloat as FP 36 37import Cryptol.Backend 38import Cryptol.Backend.FloatHelpers 39import Cryptol.Backend.Monad 40 ( Eval(..), EvalError(..), EvalErrorEx(..) 41 , Unsupported(..), delayFill, blackhole, evalSpark 42 , modifyCallStack, getCallStack 43 ) 44import Cryptol.Utils.Panic 45 46 47data What4 sym = 48 What4 49 { w4 :: sym 50 , w4defs :: MVar (W4.Pred sym) 51 , w4funs :: MVar (What4FunCache sym) 52 , w4uninterpWarns :: MVar (Set Text) 53 } 54 55type What4FunCache sym = Map Text (SomeSymFn sym) 56 57data SomeSymFn sym = 58 forall args ret. SomeSymFn (W4.SymFn sym args ret) 59 60{- | This is the monad used for symbolic evaluation. It adds to 61aspects to 'Eval'---'WConn' keeps track of the backend and collects 62definitional predicates, and 'W4Eval` adds support for partially 63defined values -} 64newtype W4Eval sym a = W4Eval { evalPartial :: W4Conn sym (W4Result sym a) } 65 66{- | This layer has the symbolic back-end, and can keep track of definitional 67predicates used when working with uninterpreted constants defined 68via a property. -} 69newtype W4Conn sym a = W4Conn { evalConn :: sym -> Eval a } 70 71-- | The symbolic value we computed. 72data W4Result sym a 73 = W4Error !EvalErrorEx 74 -- ^ A malformed value 75 76 | W4Result !(W4.Pred sym) !a 77 -- ^ safety predicate and result: the result only makes sense when 78 -- the predicate holds. 79 80 81-------------------------------------------------------------------------------- 82-- Moving between the layers 83 84w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a) 85w4Eval (W4Eval (W4Conn m)) = m 86 87w4Thunk :: Eval (W4Result sym a) -> W4Eval sym a 88w4Thunk m = W4Eval (W4Conn \_ -> m) 89 90-- | A value with no context. 91doEval :: W4.IsSymExprBuilder sym => Eval a -> W4Conn sym a 92doEval m = W4Conn \_sym -> m 93 94-- | A total value. 95total :: W4.IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a 96total m = W4Eval 97 do sym <- getSym 98 W4Result (W4.backendPred sym True) <$> m 99 100-------------------------------------------------------------------------------- 101-- Operations in WConn 102 103instance W4.IsSymExprBuilder sym => Functor (W4Conn sym) where 104 fmap = liftM 105 106instance W4.IsSymExprBuilder sym => Applicative (W4Conn sym) where 107 pure = doEval . pure 108 (<*>) = ap 109 110instance W4.IsSymExprBuilder sym => Monad (W4Conn sym) where 111 m1 >>= f = W4Conn \sym -> 112 do res1 <- evalConn m1 sym 113 evalConn (f res1) sym 114 115instance W4.IsSymExprBuilder sym => MonadIO (W4Conn sym) where 116 liftIO = doEval . liftIO 117 118-- | Access the symbolic back-end 119getSym :: W4Conn sym sym 120getSym = W4Conn \sym -> pure sym 121 122-- | Record a definition. 123--addDef :: W4.Pred sym -> W4Conn sym () 124--addDef p = W4Conn \_ -> pure W4Defs { w4Defs = p, w4Result = () } 125 126-- | Compute conjunction. 127w4And :: W4.IsSymExprBuilder sym => 128 W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym) 129w4And p q = 130 do sym <- getSym 131 liftIO (W4.andPred sym p q) 132 133-- | Compute negation. 134w4Not :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Conn sym (W4.Pred sym) 135w4Not p = 136 do sym <- getSym 137 liftIO (W4.notPred sym p) 138 139-- | Compute if-then-else. 140w4ITE :: W4.IsSymExprBuilder sym => 141 W4.Pred sym -> W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym) 142w4ITE ifP ifThen ifElse = 143 do sym <- getSym 144 liftIO (W4.itePred sym ifP ifThen ifElse) 145 146 147 148-------------------------------------------------------------------------------- 149-- Operations in W4Eval 150 151instance W4.IsSymExprBuilder sym => Functor (W4Eval sym) where 152 fmap = liftM 153 154instance W4.IsSymExprBuilder sym => Applicative (W4Eval sym) where 155 pure = total . pure 156 (<*>) = ap 157 158instance W4.IsSymExprBuilder sym => Monad (W4Eval sym) where 159 m1 >>= f = W4Eval 160 do res1 <- evalPartial m1 161 case res1 of 162 W4Error err -> pure (W4Error err) 163 W4Result px x' -> 164 do res2 <- evalPartial (f x') 165 case res2 of 166 W4Result py y -> 167 do pz <- w4And px py 168 pure (W4Result pz y) 169 W4Error _ -> pure res2 170 171instance W4.IsSymExprBuilder sym => MonadIO (W4Eval sym) where 172 liftIO = total . liftIO 173 174 175-- | Add a definitional equation. 176-- This will always be asserted when we make queries to the solver. 177addDefEqn :: W4.IsSymExprBuilder sym => What4 sym -> W4.Pred sym -> W4Eval sym () 178addDefEqn sym p = 179 liftIO (modifyMVar_ (w4defs sym) (W4.andPred (w4 sym) p)) 180 181-- | Add s safety condition. 182addSafety :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Eval sym () 183addSafety p = W4Eval (pure (W4Result p ())) 184 185-- | A fully undefined symbolic value 186evalError :: W4.IsSymExprBuilder sym => EvalError -> W4Eval sym a 187evalError err = W4Eval $ W4Conn $ \_sym -> 188 do stk <- getCallStack 189 pure (W4Error (EvalErrorEx stk err)) 190 191-------------------------------------------------------------------------------- 192 193 194assertBVDivisor :: W4.IsSymExprBuilder sym => What4 sym -> SW.SWord sym -> W4Eval sym () 195assertBVDivisor sym x = 196 do p <- liftIO (SW.bvIsNonzero (w4 sym) x) 197 assertSideCondition sym p DivideByZero 198 199assertIntDivisor :: 200 W4.IsSymExprBuilder sym => What4 sym -> W4.SymInteger sym -> W4Eval sym () 201assertIntDivisor sym x = 202 do p <- liftIO (W4.notPred (w4 sym) =<< W4.intEq (w4 sym) x =<< W4.intLit (w4 sym) 0) 203 assertSideCondition sym p DivideByZero 204 205instance W4.IsSymExprBuilder sym => Backend (What4 sym) where 206 type SBit (What4 sym) = W4.Pred sym 207 type SWord (What4 sym) = SW.SWord sym 208 type SInteger (What4 sym) = W4.SymInteger sym 209 type SFloat (What4 sym) = FP.SFloat sym 210 type SEval (What4 sym) = W4Eval sym 211 212 raiseError _ = evalError 213 214 assertSideCondition _ cond err 215 | Just False <- W4.asConstantPred cond = evalError err 216 | otherwise = addSafety cond 217 218 isReady sym m = 219 case w4Eval m (w4 sym) of 220 Ready _ -> True 221 _ -> False 222 223 sDelayFill _ m retry msg = 224 total 225 do sym <- getSym 226 doEval (w4Thunk <$> delayFill (w4Eval m sym) (w4Eval <$> retry <*> pure sym) msg) 227 228 sSpark _ m = 229 total 230 do sym <- getSym 231 doEval (w4Thunk <$> evalSpark (w4Eval m sym)) 232 233 sModifyCallStack _ f (W4Eval (W4Conn m)) = 234 W4Eval (W4Conn \sym -> modifyCallStack f (m sym)) 235 236 sGetCallStack _ = total (doEval getCallStack) 237 238 sDeclareHole _ msg = 239 total 240 do (hole, fill) <- doEval (blackhole msg) 241 pure ( w4Thunk hole 242 , \m -> total 243 do sym <- getSym 244 doEval (fill (w4Eval m sym)) 245 ) 246 247 mergeEval _sym f c mx my = W4Eval 248 do rx <- evalPartial mx 249 ry <- evalPartial my 250 case (rx, ry) of 251 252 (W4Error err, W4Error _) -> 253 pure (W4Error err) -- arbitrarily choose left error to report 254 255 (W4Error _, W4Result p y) -> 256 do p' <- w4And p =<< w4Not c 257 pure (W4Result p' y) 258 259 (W4Result p x, W4Error _) -> 260 do p' <- w4And p c 261 pure (W4Result p' x) 262 263 (W4Result px x, W4Result py y) -> 264 do zr <- evalPartial (f c x y) 265 case zr of 266 W4Error err -> pure $ W4Error err 267 W4Result pz z -> 268 do p' <- w4And pz =<< w4ITE c px py 269 pure (W4Result p' z) 270 271 wordAsChar _ bv 272 | SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv 273 | otherwise = Nothing 274 275 wordLen _ bv = SW.bvWidth bv 276 277 bitLit sym b = W4.backendPred (w4 sym) b 278 bitAsLit _ v = W4.asConstantPred v 279 280 wordLit sym intw i 281 | Just (Some w) <- someNat intw 282 = case isPosNat w of 283 Nothing -> pure $ SW.ZBV 284 Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit (w4 sym) w (BV.mkBV w i)) 285 | otherwise = panic "what4: wordLit" ["invalid bit width:", show intw ] 286 287 wordAsLit _ v 288 | Just x <- SW.bvAsUnsignedInteger v = Just (SW.bvWidth v, x) 289 | otherwise = Nothing 290 291 integerLit sym i = liftIO (W4.intLit (w4 sym) i) 292 293 integerAsLit _ v = W4.asInteger v 294 295 iteBit sym c x y = liftIO (W4.itePred (w4 sym) c x y) 296 iteWord sym c x y = liftIO (SW.bvIte (w4 sym) c x y) 297 iteInteger sym c x y = liftIO (W4.intIte (w4 sym) c x y) 298 iteFloat sym p x y = liftIO (FP.fpIte (w4 sym) p x y) 299 300 bitEq sym x y = liftIO (W4.eqPred (w4 sym) x y) 301 bitAnd sym x y = liftIO (W4.andPred (w4 sym) x y) 302 bitOr sym x y = liftIO (W4.orPred (w4 sym) x y) 303 bitXor sym x y = liftIO (W4.xorPred (w4 sym) x y) 304 bitComplement sym x = liftIO (W4.notPred (w4 sym) x) 305 306 wordBit sym bv idx = liftIO (SW.bvAtBE (w4 sym) bv idx) 307 wordUpdate sym bv idx b = liftIO (SW.bvSetBE (w4 sym) bv idx b) 308 309 packWord sym bs = 310 do z <- wordLit sym (genericLength bs) 0 311 let f w (idx,b) = wordUpdate sym w idx b 312 foldM f z (zip [0..] bs) 313 314 unpackWord sym bv = liftIO $ 315 mapM (SW.bvAtBE (w4 sym) bv) [0 .. SW.bvWidth bv-1] 316 317 joinWord sym x y = liftIO $ SW.bvJoin (w4 sym) x y 318 319 splitWord _sym 0 _ bv = pure (SW.ZBV, bv) 320 splitWord _sym _ 0 bv = pure (bv, SW.ZBV) 321 splitWord sym lw rw bv = liftIO $ 322 do l <- SW.bvSliceBE (w4 sym) 0 lw bv 323 r <- SW.bvSliceBE (w4 sym) lw rw bv 324 return (l, r) 325 326 extractWord sym bits idx bv = 327 liftIO $ SW.bvSliceLE (w4 sym) idx bits bv 328 329 wordEq sym x y = liftIO (SW.bvEq (w4 sym) x y) 330 wordLessThan sym x y = liftIO (SW.bvult (w4 sym) x y) 331 wordGreaterThan sym x y = liftIO (SW.bvugt (w4 sym) x y) 332 wordSignedLessThan sym x y = liftIO (SW.bvslt (w4 sym) x y) 333 334 wordOr sym x y = liftIO (SW.bvOr (w4 sym) x y) 335 wordAnd sym x y = liftIO (SW.bvAnd (w4 sym) x y) 336 wordXor sym x y = liftIO (SW.bvXor (w4 sym) x y) 337 wordComplement sym x = liftIO (SW.bvNot (w4 sym) x) 338 339 wordPlus sym x y = liftIO (SW.bvAdd (w4 sym) x y) 340 wordMinus sym x y = liftIO (SW.bvSub (w4 sym) x y) 341 wordMult sym x y = liftIO (SW.bvMul (w4 sym) x y) 342 wordNegate sym x = liftIO (SW.bvNeg (w4 sym) x) 343 wordLg2 sym x = sLg2 (w4 sym) x 344 345 wordDiv sym x y = 346 do assertBVDivisor sym y 347 liftIO (SW.bvUDiv (w4 sym) x y) 348 wordMod sym x y = 349 do assertBVDivisor sym y 350 liftIO (SW.bvURem (w4 sym) x y) 351 wordSignedDiv sym x y = 352 do assertBVDivisor sym y 353 liftIO (SW.bvSDiv (w4 sym) x y) 354 wordSignedMod sym x y = 355 do assertBVDivisor sym y 356 liftIO (SW.bvSRem (w4 sym) x y) 357 358 wordToInt sym x = liftIO (SW.bvToInteger (w4 sym) x) 359 wordFromInt sym width i = liftIO (SW.integerToBV (w4 sym) i width) 360 361 intPlus sym x y = liftIO $ W4.intAdd (w4 sym) x y 362 intMinus sym x y = liftIO $ W4.intSub (w4 sym) x y 363 intMult sym x y = liftIO $ W4.intMul (w4 sym) x y 364 intNegate sym x = liftIO $ W4.intNeg (w4 sym) x 365 366 -- NB: What4's division operation provides SMTLib's euclidean division, 367 -- which doesn't match the round-to-neg-infinity semantics of Cryptol, 368 -- so we have to do some work to get the desired semantics. 369 intDiv sym x y = 370 do assertIntDivisor sym y 371 liftIO $ do 372 neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0) 373 case W4.asConstantPred neg of 374 Just False -> W4.intDiv (w4 sym) x y 375 Just True -> 376 do xneg <- W4.intNeg (w4 sym) x 377 yneg <- W4.intNeg (w4 sym) y 378 W4.intDiv (w4 sym) xneg yneg 379 Nothing -> 380 do xneg <- W4.intNeg (w4 sym) x 381 yneg <- W4.intNeg (w4 sym) y 382 zneg <- W4.intDiv (w4 sym) xneg yneg 383 z <- W4.intDiv (w4 sym) x y 384 W4.intIte (w4 sym) neg zneg z 385 386 -- NB: What4's division operation provides SMTLib's euclidean division, 387 -- which doesn't match the round-to-neg-infinity semantics of Cryptol, 388 -- so we have to do some work to get the desired semantics. 389 intMod sym x y = 390 do assertIntDivisor sym y 391 liftIO $ do 392 neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0) 393 case W4.asConstantPred neg of 394 Just False -> W4.intMod (w4 sym) x y 395 Just True -> 396 do xneg <- W4.intNeg (w4 sym) x 397 yneg <- W4.intNeg (w4 sym) y 398 W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg 399 Nothing -> 400 do xneg <- W4.intNeg (w4 sym) x 401 yneg <- W4.intNeg (w4 sym) y 402 z <- W4.intMod (w4 sym) x y 403 zneg <- W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg 404 W4.intIte (w4 sym) neg zneg z 405 406 intEq sym x y = liftIO $ W4.intEq (w4 sym) x y 407 intLessThan sym x y = liftIO $ W4.intLt (w4 sym) x y 408 intGreaterThan sym x y = liftIO $ W4.intLt (w4 sym) y x 409 410 -- NB, we don't do reduction here on symbolic values 411 intToZn sym m x 412 | Just xi <- W4.asInteger x 413 = liftIO $ W4.intLit (w4 sym) (xi `mod` m) 414 415 | otherwise 416 = pure x 417 418 znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"] 419 znToInt sym m x = liftIO (W4.intMod (w4 sym) x =<< W4.intLit (w4 sym) m) 420 421 znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"] 422 znEq sym m x y = liftIO $ 423 do diff <- W4.intSub (w4 sym) x y 424 W4.intDivisible (w4 sym) diff (fromInteger m) 425 426 znPlus sym m x y = liftIO $ sModAdd (w4 sym) m x y 427 znMinus sym m x y = liftIO $ sModSub (w4 sym) m x y 428 znMult sym m x y = liftIO $ sModMult (w4 sym) m x y 429 znNegate sym m x = liftIO $ sModNegate (w4 sym) m x 430 znRecip = sModRecip 431 432 -------------------------------------------------------------- 433 434 fpLit sym e p r = liftIO $ FP.fpFromRationalLit (w4 sym) e p r 435 fpAsLit _ f = BF e p <$> FP.fpAsLit f 436 where (e,p) = FP.fpSize f 437 438 fpExactLit sym BF{ bfExpWidth = e, bfPrecWidth = p, bfValue = bf } = 439 liftIO (FP.fpFromBinary (w4 sym) e p =<< SW.bvLit (w4 sym) (e+p) (floatToBits e p bf)) 440 441 fpNaN sym e p = liftIO (FP.fpNaN (w4 sym) e p) 442 fpPosInf sym e p = liftIO (FP.fpPosInf (w4 sym) e p) 443 444 fpToBits sym f = liftIO (FP.fpToBinary (w4 sym) f) 445 fpFromBits sym e p w = liftIO (FP.fpFromBinary (w4 sym) e p w) 446 447 fpEq sym x y = liftIO $ FP.fpEqIEEE (w4 sym) x y 448 fpLessThan sym x y = liftIO $ FP.fpLtIEEE (w4 sym) x y 449 fpGreaterThan sym x y = liftIO $ FP.fpGtIEEE (w4 sym) x y 450 fpLogicalEq sym x y = liftIO $ FP.fpEq (w4 sym) x y 451 452 fpPlus = fpBinArith FP.fpAdd 453 fpMinus = fpBinArith FP.fpSub 454 fpMult = fpBinArith FP.fpMul 455 fpDiv = fpBinArith FP.fpDiv 456 457 fpNeg sym x = liftIO $ FP.fpNeg (w4 sym) x 458 fpAbs sym x = liftIO $ FP.fpAbs (w4 sym) x 459 fpSqrt sym r x = 460 do rm <- fpRoundingMode sym r 461 liftIO $ FP.fpSqrt (w4 sym) rm x 462 463 fpFMA sym r x y z = 464 do rm <- fpRoundingMode sym r 465 liftIO $ FP.fpFMA (w4 sym) rm x y z 466 467 fpIsZero sym x = liftIO $ FP.fpIsZero (w4 sym) x 468 fpIsNeg sym x = liftIO $ FP.fpIsNeg (w4 sym) x 469 fpIsNaN sym x = liftIO $ FP.fpIsNaN (w4 sym) x 470 fpIsInf sym x = liftIO $ FP.fpIsInf (w4 sym) x 471 fpIsNorm sym x = liftIO $ FP.fpIsNorm (w4 sym) x 472 fpIsSubnorm sym x = liftIO $ FP.fpIsSubnorm (w4 sym) x 473 474 fpFromInteger sym e p r x = 475 do rm <- fpRoundingMode sym r 476 liftIO $ FP.fpFromInteger (w4 sym) e p rm x 477 478 fpToInteger = fpCvtToInteger 479 480 fpFromRational = fpCvtFromRational 481 fpToRational = fpCvtToRational 482 483sModAdd :: W4.IsSymExprBuilder sym => 484 sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym) 485sModAdd _sym 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"] 486sModAdd sym m x y 487 | Just xi <- W4.asInteger x 488 , Just yi <- W4.asInteger y 489 = W4.intLit sym ((xi+yi) `mod` m) 490 491 | otherwise 492 = W4.intAdd sym x y 493 494sModSub :: W4.IsSymExprBuilder sym => 495 sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym) 496sModSub _sym 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"] 497sModSub sym m x y 498 | Just xi <- W4.asInteger x 499 , Just yi <- W4.asInteger y 500 = W4.intLit sym ((xi-yi) `mod` m) 501 502 | otherwise 503 = W4.intSub sym x y 504 505 506sModMult :: W4.IsSymExprBuilder sym => 507 sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym) 508sModMult _sym 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"] 509sModMult sym m x y 510 | Just xi <- W4.asInteger x 511 , Just yi <- W4.asInteger y 512 = W4.intLit sym ((xi*yi) `mod` m) 513 514 | otherwise 515 = W4.intMul sym x y 516 517sModNegate :: W4.IsSymExprBuilder sym => 518 sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym) 519sModNegate _sym 0 _ = evalPanic "sModMult" ["0 modulus not allowed"] 520sModNegate sym m x 521 | Just xi <- W4.asInteger x 522 = W4.intLit sym ((negate xi) `mod` m) 523 524 | otherwise 525 = W4.intNeg sym x 526 527 528-- | Try successive powers of 2 to find the first that dominates the input. 529-- We could perhaps reduce to using CLZ instead... 530sLg2 :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SEval (What4 sym) (SW.SWord sym) 531sLg2 sym x = liftIO $ go 0 532 where 533 w = SW.bvWidth x 534 lit n = SW.bvLit sym w (toInteger n) 535 536 go i | toInteger i < w = 537 do p <- SW.bvule sym x =<< lit (bit i) 538 lazyIte (SW.bvIte sym) p (lit i) (go (i+1)) 539 540 -- base case, should only happen when i = w 541 go i = lit i 542 543 544 545-- Errors ---------------------------------------------------------------------- 546 547evalPanic :: String -> [String] -> a 548evalPanic cxt = panic ("[What4] " ++ cxt) 549 550lazyIte :: 551 (W4.IsExpr p, Monad m) => 552 (p W4.BaseBoolType -> a -> a -> m a) -> 553 p W4.BaseBoolType -> 554 m a -> 555 m a -> 556 m a 557lazyIte f c mx my 558 | Just b <- W4.asConstantPred c = if b then mx else my 559 | otherwise = 560 do x <- mx 561 y <- my 562 f c x y 563 564w4bvShl :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym) 565w4bvShl sym x y = liftIO $ SW.bvShl sym x y 566 567w4bvLshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym) 568w4bvLshr sym x y = liftIO $ SW.bvLshr sym x y 569 570w4bvAshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym) 571w4bvAshr sym x y = liftIO $ SW.bvAshr sym x y 572 573w4bvRol :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym) 574w4bvRol sym x y = liftIO $ SW.bvRol sym x y 575 576w4bvRor :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym) 577w4bvRor sym x y = liftIO $ SW.bvRor sym x y 578 579 580 581fpRoundingMode :: 582 W4.IsSymExprBuilder sym => 583 What4 sym -> SWord (What4 sym) -> SEval (What4 sym) W4.RoundingMode 584fpRoundingMode sym v = 585 case wordAsLit sym v of 586 Just (_w,i) -> 587 case i of 588 0 -> pure W4.RNE 589 1 -> pure W4.RNA 590 2 -> pure W4.RTP 591 3 -> pure W4.RTN 592 4 -> pure W4.RTZ 593 x -> raiseError sym (BadRoundingMode x) 594 _ -> liftIO $ X.throwIO $ UnsupportedSymbolicOp "rounding mode" 595 596fpBinArith :: 597 W4.IsSymExprBuilder sym => 598 FP.SFloatBinArith sym -> 599 What4 sym -> 600 SWord (What4 sym) -> 601 SFloat (What4 sym) -> 602 SFloat (What4 sym) -> 603 SEval (What4 sym) (SFloat (What4 sym)) 604fpBinArith fun = \sym r x y -> 605 do m <- fpRoundingMode sym r 606 liftIO (fun (w4 sym) m x y) 607 608 609fpCvtToInteger :: 610 (W4.IsSymExprBuilder sy, sym ~ What4 sy) => 611 sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym) 612fpCvtToInteger sym fun r x = 613 do grd <- liftIO 614 do bad1 <- FP.fpIsInf (w4 sym) x 615 bad2 <- FP.fpIsNaN (w4 sym) x 616 W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2 617 assertSideCondition sym grd (BadValue fun) 618 rnd <- fpRoundingMode sym r 619 liftIO 620 do y <- FP.fpToReal (w4 sym) x 621 case rnd of 622 W4.RNE -> W4.realRoundEven (w4 sym) y 623 W4.RNA -> W4.realRound (w4 sym) y 624 W4.RTP -> W4.realCeil (w4 sym) y 625 W4.RTN -> W4.realFloor (w4 sym) y 626 W4.RTZ -> W4.realTrunc (w4 sym) y 627 628 629fpCvtToRational :: 630 (W4.IsSymExprBuilder sy, sym ~ What4 sy) => 631 sym -> SFloat sym -> SEval sym (SRational sym) 632fpCvtToRational sym fp = 633 do grd <- liftIO 634 do bad1 <- FP.fpIsInf (w4 sym) fp 635 bad2 <- FP.fpIsNaN (w4 sym) fp 636 W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2 637 assertSideCondition sym grd (BadValue "fpToRational") 638 (rel,x,y) <- liftIO (FP.fpToRational (w4 sym) fp) 639 addDefEqn sym =<< liftIO (W4.impliesPred (w4 sym) grd rel) 640 ratio sym x y 641 642fpCvtFromRational :: 643 (W4.IsSymExprBuilder sy, sym ~ What4 sy) => 644 sym -> Integer -> Integer -> SWord sym -> 645 SRational sym -> SEval sym (SFloat sym) 646fpCvtFromRational sym e p r rat = 647 do rnd <- fpRoundingMode sym r 648 liftIO (FP.fpFromRational (w4 sym) e p rnd (sNum rat) (sDenom rat)) 649 650-- Create a fresh constant and assert that it is the 651-- multiplicitive inverse of x; return the constant. 652-- Such an inverse must exist under the precondition 653-- that the modulus is prime and the input is nonzero. 654sModRecip :: 655 W4.IsSymExprBuilder sym => 656 What4 sym -> 657 Integer -> 658 W4.SymInteger sym -> 659 W4Eval sym (W4.SymInteger sym) 660sModRecip _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"] 661sModRecip sym m x 662 -- If the input is concrete, evaluate the answer 663 | Just xi <- W4.asInteger x 664 = let r = Integer.recipModInteger xi m 665 in if r == 0 then raiseError sym DivideByZero else integerLit sym r 666 667 -- If the input is symbolic, create a new symbolic constant 668 -- and assert that it is the desired multiplicitive inverse. 669 -- Such an inverse will exist under the precondition that 670 -- the modulus is prime, and as long as the input is nonzero. 671 | otherwise 672 = do divZero <- liftIO (W4.intDivisible (w4 sym) x (fromInteger m)) 673 ok <- liftIO (W4.notPred (w4 sym) divZero) 674 assertSideCondition sym ok DivideByZero 675 676 z <- liftIO (W4.freshBoundedInt (w4 sym) W4.emptySymbol (Just 1) (Just (m-1))) 677 xz <- liftIO (W4.intMul (w4 sym) x z) 678 rel <- znEq sym m xz =<< liftIO (W4.intLit (w4 sym) 1) 679 addDefEqn sym =<< liftIO (W4.orPred (w4 sym) divZero rel) 680 681 return z 682