content: -- |
  -- Module      :  Cryptol.Backend.SBV
  -- Copyright   :  (c) 2013-2016 Galois, Inc.
  -- License     :  BSD3
  -- Maintainer  :  cryptol@galois.com
  -- Stability   :  provisional
  -- Portability :  portable
  
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE MultiWayIf #-}
  {-# LANGUAGE PatternGuards #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeSynonymInstances #-}
  {-# LANGUAGE ViewPatterns #-}
  module Cryptol.Backend.SBV
    ( SBV(..), SBVEval(..), SBVResult(..)
    , literalSWord
    , freshSBool_
    , freshBV_
    , freshSInteger_
    , addDefEqn
    , ashr
    , lshr
    , shl
    , evalPanic
    , svFromInteger
    , svToInteger
    ) where
  
  import qualified Control.Exception as X
  import           Control.Concurrent.MVar
  import           Control.Monad.IO.Class (MonadIO(..))
  import           Data.Bits (bit, complement)
  import           Data.List (foldl')
  
  import qualified GHC.Num.Compat as Integer
  
  import Data.SBV.Dynamic as SBV
  import qualified Data.SBV.Internals as SBV
  
  import Cryptol.Backend
  import Cryptol.Backend.Concrete ( integerToChar )
  import Cryptol.Backend.Monad
    ( Eval(..), blackhole, delayFill, evalSpark
    , EvalError(..), EvalErrorEx(..), Unsupported(..)
    , modifyCallStack, getCallStack, maybeReady
    )
  
  import Cryptol.Utils.Panic (panic)
  
  data SBV =
    SBV
    { sbvStateVar     :: MVar (SBV.State)
    , sbvDefRelations :: MVar SVal
    }
  
  -- Utility operations -------------------------------------------------------------
  
  fromBitsLE :: [SBit SBV] -> SWord SBV
  fromBitsLE bs = foldl' f (literalSWord 0 0) bs
    where f w b = svJoin (svToWord1 b) w
  
  packSBV :: [SBit SBV] -> SWord SBV
  packSBV bs = fromBitsLE (reverse bs)
  
  unpackSBV :: SWord SBV -> [SBit SBV]
  unpackSBV x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ]
  
  literalSWord :: Int -> Integer -> SWord SBV
  literalSWord w i = svInteger (KBounded False w) i
  
  svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> SBV.State -> IO SVal
  #if MIN_VERSION_sbv(8,8,0)
  svMkSymVar_ = svMkSymVar . SBV.NonQueryVar
  #else
  svMkSymVar_ = svMkSymVar
  #endif
  
  freshBV_ :: SBV -> Int -> IO (SWord SBV)
  freshBV_ (SBV stateVar _) w =
    withMVar stateVar (svMkSymVar_ Nothing (KBounded False w) Nothing)
  
  freshSBool_ :: SBV -> IO (SBit SBV)
  freshSBool_ (SBV stateVar _) =
    withMVar stateVar (svMkSymVar_ Nothing KBool Nothing)
  
  freshSInteger_ :: SBV -> IO (SInteger SBV)
  freshSInteger_ (SBV stateVar _) =
    withMVar stateVar (svMkSymVar_ Nothing KUnbounded Nothing)
  
  
  -- SBV Evaluation monad -------------------------------------------------------
  
  data SBVResult a
    = SBVError !EvalErrorEx
    | SBVResult !SVal !a -- safety predicate and result
  
  instance Functor SBVResult where
    fmap _ (SBVError err) = SBVError err
    fmap f (SBVResult p x) = SBVResult p (f x)
  
  instance Applicative SBVResult where
    pure = SBVResult svTrue
    SBVError err <*> _ = SBVError err
    _ <*> SBVError err = SBVError err
    SBVResult p1 f <*> SBVResult p2 x = SBVResult (svAnd p1 p2) (f x)
  
  instance Monad SBVResult where
    return = pure
    SBVError err >>= _ = SBVError err
    SBVResult px x >>= m =
      case m x of
        SBVError err   -> SBVError err
        SBVResult pm z -> SBVResult (svAnd px pm) z
  
  newtype SBVEval a = SBVEval{ sbvEval :: Eval (SBVResult a) }
    deriving (Functor)
  
  instance Applicative SBVEval where
    pure = SBVEval . pure . pure
    f <*> x = SBVEval $
      do f' <- sbvEval f
         x' <- sbvEval x
         pure (f' <*> x')
  
  instance Monad SBVEval where
    return = pure
    x >>= f = SBVEval $
      sbvEval x >>= \case
        SBVError err -> pure (SBVError err)
        SBVResult px x' ->
          sbvEval (f x') >>= \case
            SBVError err -> pure (SBVError err)
            SBVResult pz z -> pure (SBVResult (svAnd px pz) z)
  
  instance MonadIO SBVEval where
    liftIO m = SBVEval $ fmap pure (liftIO m)
  
  
  addDefEqn :: SBV -> SVal -> IO ()
  addDefEqn (SBV _ relsVar) b = modifyMVar_ relsVar (pure . svAnd b)
  
  -- Symbolic Big-endian Words -------------------------------------------------------
  
  instance Backend SBV where
    type SBit SBV = SVal
    type SWord SBV = SVal
    type SInteger SBV = SVal
    type SFloat SBV = ()        -- XXX: not implemented
    type SEval SBV = SBVEval
  
    raiseError _ err = SBVEval $
      do stk <- getCallStack
         pure (SBVError (EvalErrorEx stk err))
  
    assertSideCondition sym cond err
      | Just False <- svAsBool cond = raiseError sym err
      | otherwise = SBVEval (pure (SBVResult cond ()))
  
    isReady _ (SBVEval m) = SBVEval $
      maybeReady m >>= \case
        Just x  -> pure (Just <$> x)
        Nothing -> pure (pure Nothing)
  
    sDelayFill _ m retry msg = SBVEval $
      do m' <- delayFill (sbvEval m) (sbvEval <$> retry) msg
         pure (pure (SBVEval m'))
  
    sSpark _ m = SBVEval $
      do m' <- evalSpark (sbvEval m)
         pure (pure (SBVEval m'))
  
    sDeclareHole _ msg = SBVEval $
      do (hole, fill) <- blackhole msg
         pure (pure (SBVEval hole, \m -> SBVEval (fmap pure $ fill (sbvEval m))))
  
    sModifyCallStack _ f (SBVEval m) = SBVEval $
      modifyCallStack f m
  
    sGetCallStack _ = SBVEval (pure <$> getCallStack)
  
    mergeEval _sym f c mx my = SBVEval $
      do rx <- sbvEval mx
         ry <- sbvEval my
         case (rx, ry) of
           (SBVError err, SBVError _) ->
             pure $ SBVError err -- arbitrarily choose left error to report
           (SBVError _, SBVResult p y) ->
             pure $ SBVResult (svAnd (svNot c) p) y
           (SBVResult p x, SBVError _) ->
             pure $ SBVResult (svAnd c p) x
           (SBVResult px x, SBVResult py y) ->
             do zr <- sbvEval (f c x y)
                case zr of
                  SBVError err -> pure $ SBVError err
                  SBVResult pz z ->
                    pure $ SBVResult (svAnd (svIte c px py) pz) z
  
    wordLen' _ v = toInteger (intSizeOf v)
    {-# INLINE wordLen' #-}
    wordAsChar _ v = integerToChar <$> svAsInteger v
  
    iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y
    iteWord _ b x y = pure $! svSymbolicMerge (kindOf x) True b x y
    iteInteger _ b x y = pure $! svSymbolicMerge KUnbounded True b x y
  
    bitAsLit _ b = svAsBool b
    wordAsLit _ w =
      case svAsInteger w of
        Just x -> Just (toInteger (intSizeOf w), x)
        Nothing -> Nothing
    integerAsLit _ v = svAsInteger v
  
    bitLit _ b     = svBool b
    wordLit _ n x  = pure $! literalSWord (fromInteger n) x
    integerLit _ x = pure $! svInteger KUnbounded x
  
    bitEq  _ x y = pure $! svEqual x y
    bitOr  _ x y = pure $! svOr x y
    bitAnd _ x y = pure $! svAnd x y
    bitXor _ x y = pure $! svXOr x y
    bitComplement _ x = pure $! svNot x
  
    wordBit _ x idx = pure $! svTestBit x (intSizeOf x - 1 - fromInteger idx)
  
    wordUpdate _ x idx b = pure $! svSymbolicMerge (kindOf x) False b wtrue wfalse
      where
       i' = intSizeOf x - 1 - fromInteger idx
       wtrue  = x `svOr`  svInteger (kindOf x) (bit i' :: Integer)
       wfalse = x `svAnd` svInteger (kindOf x) (complement (bit i' :: Integer))
  
    packWord _ bs  = pure $! packSBV bs
    unpackWord _ x = pure $! unpackSBV x
  
    wordEq _ x y = pure $! svEqual x y
    wordLessThan _ x y = pure $! svLessThan x y
    wordGreaterThan _ x y = pure $! svGreaterThan x y
  
    wordSignedLessThan _ x y = pure $! svLessThan sx sy
      where sx = svSign x
            sy = svSign y
  
    joinWord _ x y = pure $! svJoin x y
  
    splitWord _ _leftW rightW w = pure
      ( svExtract (intSizeOf w - 1) (fromInteger rightW) w
      , svExtract (fromInteger rightW - 1) 0 w
      )
  
    extractWord _ len start w =
      pure $! svExtract (fromInteger start + fromInteger len - 1) (fromInteger start) w
  
    wordAnd _ a b = pure $! svAnd a b
    wordOr  _ a b = pure $! svOr a b
    wordXor _ a b = pure $! svXOr a b
    wordComplement _ a = pure $! svNot a
  
    wordPlus  _ a b = pure $! svPlus a b
    wordMinus _ a b = pure $! svMinus a b
    wordMult  _ a b = pure $! svTimes a b
    wordNegate _ a  = pure $! svUNeg a
  
    wordShiftLeft _ a b   = pure $! shl a b
    wordShiftRight _ a b  = pure $! lshr a b
    wordRotateLeft _ a b  = pure $! SBV.svRotateLeft a b
    wordRotateRight _ a b = pure $! SBV.svRotateRight a b
    wordSignedShiftRight _ a b = pure $! ashr a b
  
    wordDiv sym a b =
      do let z = literalSWord (intSizeOf b) 0
         assertSideCondition sym (svNot (svEqual b z)) DivideByZero
         pure $! svQuot a b
  
    wordMod sym a b =
      do let z = literalSWord (intSizeOf b) 0
         assertSideCondition sym (svNot (svEqual b z)) DivideByZero
         pure $! svRem a b
  
    wordSignedDiv sym a b =
      do let z = literalSWord (intSizeOf b) 0
         assertSideCondition sym (svNot (svEqual b z)) DivideByZero
         pure $! signedQuot a b
  
    wordSignedMod sym a b =
      do let z = literalSWord (intSizeOf b) 0
         assertSideCondition sym (svNot (svEqual b z)) DivideByZero
         pure $! signedRem a b
  
    wordLg2 _ a = sLg2 a
  
    wordToInt _ x = pure $! svToInteger x
    wordToSignedInt _ x = pure $! svToInteger (svSign x)
    wordFromInt _ w i = pure $! svFromInteger w i
  
    intEq _ a b = pure $! svEqual a b
    intLessThan _ a b = pure $! svLessThan a b
    intGreaterThan _ a b = pure $! svGreaterThan a b
  
    intPlus  _ a b = pure $! svPlus a b
    intMinus _ a b = pure $! svMinus a b
    intMult  _ a b = pure $! svTimes a b
    intNegate _ a  = pure $! SBV.svUNeg a
  
    intDiv sym a b =
      do let z = svInteger KUnbounded 0
         assertSideCondition sym (svNot (svEqual b z)) DivideByZero
         let p = svLessThan z b
         pure $! svSymbolicMerge KUnbounded True p (svQuot a b) (svQuot (svUNeg a) (svUNeg b))
    intMod sym a b =
      do let z = svInteger KUnbounded 0
         assertSideCondition sym (svNot (svEqual b z)) DivideByZero
         let p = svLessThan z b
         pure $! svSymbolicMerge KUnbounded True p (svRem a b) (svUNeg (svRem (svUNeg a) (svUNeg b)))
  
    -- NB, we don't do reduction here
    intToZn _ _m a = pure a
  
    znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"]
    znToInt _ m a =
      do let m' = svInteger KUnbounded m
         pure $! svRem a m'
  
    znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"]
    znEq sym m a b = svDivisible sym m (SBV.svMinus a b)
  
    znPlus  sym m a b = sModAdd sym m a b
    znMinus sym m a b = sModSub sym m a b
    znMult  sym m a b = sModMult sym m a b
    znNegate sym m a  = sModNegate sym m a
    znRecip = sModRecip
  
    fpAsLit _ _               = Nothing
    iteFloat _ _ _ _          = unsupported "iteFloat"
    fpNaN _ _ _               = unsupported "fpNaN"
    fpPosInf _ _ _            = unsupported "fpPosInf"
    fpExactLit _ _            = unsupported "fpExactLit"
    fpLit _ _ _ _             = unsupported "fpLit"
    fpLogicalEq _ _ _         = unsupported "fpLogicalEq"
    fpEq _ _ _                = unsupported "fpEq"
    fpLessThan _ _ _          = unsupported "fpLessThan"
    fpGreaterThan _ _ _       = unsupported "fpGreaterThan"
    fpPlus _ _ _ _            = unsupported "fpPlus"
    fpMinus _ _ _ _           = unsupported "fpMinus"
    fpMult _ _ _ _            = unsupported "fpMult"
    fpDiv _ _ _ _             = unsupported "fpDiv"
    fpAbs _ _                 = unsupported "fpAbs"
    fpSqrt _ _ _              = unsupported "fpSqrt"
    fpFMA _ _ _ _ _           = unsupported "fpFMA"
    fpNeg _ _                 = unsupported "fpNeg"
    fpFromInteger _ _ _ _ _   = unsupported "fpFromInteger"
    fpToInteger _ _ _ _       = unsupported "fpToInteger"
    fpIsZero _ _              = unsupported "fpIsZero"
    fpIsInf _ _               = unsupported "fpIsInf"
    fpIsNeg _ _               = unsupported "fpIsNeg"
    fpIsNaN _ _               = unsupported "fpIsNaN"
    fpIsNorm _ _              = unsupported "fpIsNorm"
    fpIsSubnorm _ _           = unsupported "fpIsSubnorm"
    fpToBits _ _              = unsupported "fpToBits"
    fpFromBits _ _ _ _        = unsupported "fpFromBits"
    fpToRational _ _          = unsupported "fpToRational"
    fpFromRational _ _ _ _ _  = unsupported "fpFromRational"
  
  
  unsupported :: String -> SEval SBV a
  unsupported x = liftIO (X.throw (UnsupportedSymbolicOp x))
  
  
  svToInteger :: SWord SBV -> SInteger SBV
  svToInteger w =
    case svAsInteger w of
      Nothing -> svFromIntegral KUnbounded w
      Just x  -> svInteger KUnbounded x
  
  svFromInteger :: Integer -> SInteger SBV -> SWord SBV
  svFromInteger 0 _ = literalSWord 0 0
  svFromInteger n i =
    case svAsInteger i of
      Nothing -> svFromIntegral (KBounded False (fromInteger n)) i
      Just x  -> literalSWord (fromInteger n) x
  
  -- Errors ----------------------------------------------------------------------
  
  evalPanic :: String -> [String] -> a
  evalPanic cxt = panic ("[SBV] " ++ cxt)
  
  
  sModAdd :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
  sModAdd _ 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"]
  sModAdd sym modulus x y =
    case (SBV.svAsInteger x, SBV.svAsInteger y) of
      (Just i, Just j) -> integerLit sym ((i + j) `mod` modulus)
      _                -> pure $ SBV.svPlus x y
  
  sModSub :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
  sModSub _ 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"]
  sModSub sym modulus x y =
    case (SBV.svAsInteger x, SBV.svAsInteger y) of
      (Just i, Just j) -> integerLit sym ((i - j) `mod` modulus)
      _                -> pure $ SBV.svMinus x y
  
  sModNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
  sModNegate _ 0 _ = evalPanic "sModNegate" ["0 modulus not allowed"]
  sModNegate sym modulus x =
    case SBV.svAsInteger x of
      Just i -> integerLit sym ((negate i) `mod` modulus)
      _      -> pure $ SBV.svUNeg x
  
  sModMult :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
  sModMult _ 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"]
  sModMult sym modulus x y =
    case (SBV.svAsInteger x, SBV.svAsInteger y) of
      (Just i, Just j) -> integerLit sym ((i * j) `mod` modulus)
      _                -> pure $ SBV.svTimes x y
  
  -- Create a fresh constant and assert that it is the
  -- multiplicitive inverse of x; return the constant.
  -- Such an inverse must exist under the precondition
  -- that the modulus is prime and the input is nonzero.
  sModRecip ::
    SBV ->
    Integer {- ^ modulus: must be prime -} ->
    SInteger SBV ->
    SEval SBV (SInteger SBV)
  sModRecip _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"]
  sModRecip sym m x
    -- If the input is concrete, evaluate the answer
    | Just xi <- svAsInteger x
    = case Integer.integerRecipMod xi m of
        Just r  -> integerLit sym r
        Nothing -> raiseError sym DivideByZero
  
    -- If the input is symbolic, create a new symbolic constant
    -- and assert that it is the desired multiplicitive inverse.
    -- Such an inverse will exist under the precondition that
    -- the modulus is prime, and as long as the input is nonzero.
    | otherwise
    = do divZero <- svDivisible sym m x
         assertSideCondition sym (svNot divZero) DivideByZero
  
         z <- liftIO (freshSInteger_ sym)
         let xz = svTimes x z
         rel <- znEq sym m xz (svInteger KUnbounded 1)
         let range = svAnd (svLessThan (svInteger KUnbounded 0) z)
                           (svLessThan z (svInteger KUnbounded m))
         liftIO (addDefEqn sym (svAnd range (svOr divZero rel)))
  
         return z
  
  -- | Ceiling (log_2 x)
  sLg2 :: SWord SBV -> SEval SBV (SWord SBV)
  sLg2 x = pure $ go 0
    where
      lit n = literalSWord (SBV.intSizeOf x) n
      go i | i < SBV.intSizeOf x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
           | otherwise           = lit (toInteger i)
  
  svDivisible :: SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
  svDivisible sym m x =
    do m' <- integerLit sym m
       z  <- integerLit sym 0
       pure $ SBV.svEqual (SBV.svRem x m') z
  
  signedQuot :: SWord SBV -> SWord SBV -> SWord SBV
  signedQuot x y = SBV.svUnsign (SBV.svQuot (SBV.svSign x) (SBV.svSign y))
  
  signedRem :: SWord SBV -> SWord SBV -> SWord SBV
  signedRem x y = SBV.svUnsign (SBV.svRem (SBV.svSign x) (SBV.svSign y))
  
  ashr :: SVal -> SVal -> SVal
  ashr x idx =
    case SBV.svAsInteger idx of
      Just i  -> SBV.svUnsign (SBV.svShr (SBV.svSign x) (fromInteger i))
      Nothing -> SBV.svUnsign (SBV.svShiftRight (SBV.svSign x) idx)
  
  lshr :: SVal -> SVal -> SVal
  lshr x idx =
    case SBV.svAsInteger idx of
      Just i -> SBV.svShr x (fromInteger i)
      Nothing -> SBV.svShiftRight x idx
  
  shl :: SVal -> SVal -> SVal
  shl x idx =
    case SBV.svAsInteger idx of
      Just i  -> SBV.svShl x (fromInteger i)
      Nothing -> SBV.svShiftLeft x idx
  