SBV.hs

-- |
-- Module      :  Cryptol.Eval.SBV
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Eval.SBV
  ( primTable
  ) where

import qualified Control.Exception as X
import           Control.Monad.IO.Class (MonadIO(..))
import qualified Data.Map as Map
import qualified Data.Text as T

import Data.SBV.Dynamic as SBV

import Cryptol.Backend
import Cryptol.Backend.Monad (Unsupported(..), EvalError(..) )
import Cryptol.Backend.SBV
import Cryptol.Backend.SeqMap
import Cryptol.Backend.WordValue

import Cryptol.Eval.Type (TValue(..))
import Cryptol.Eval.Generic
import Cryptol.Eval.Prims
import Cryptol.Eval.Value
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))
import Cryptol.Utils.Ident

-- Values ----------------------------------------------------------------------

type Value = GenValue SBV

-- Primitives ------------------------------------------------------------------

-- See also Cryptol.Eval.Concrete.primTable
primTable :: SBV -> IO EvalOpts -> Map.Map PrimIdent (Prim SBV)
primTable sym getEOpts =
  Map.union (genericPrimTable sym getEOpts) $
  Map.fromList $ map (\(n, v) -> (prelPrim (T.pack n), v))

  [ -- Indexing and updates
    ("@"           , indexPrim sym IndexForward  (indexFront sym) (indexFront_segs sym))
  , ("!"           , indexPrim sym IndexBackward (indexFront sym) (indexFront_segs sym))

  , ("update"      , updatePrim sym (updateFrontSym_word sym) (updateFrontSym sym))
  , ("updateEnd"   , updatePrim sym (updateBackSym_word sym) (updateBackSym sym))

  ]

indexFront ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV (GenValue SBV) ->
  TValue ->
  SVal ->
  SEval SBV Value
indexFront sym mblen a xs _ix idx
  | Just i <- SBV.svAsInteger idx
  = lookupSeqMap xs i

  | Nat n <- mblen
  , TVSeq wlen TVBit <- a
  = do wvs <- traverse (fromWordVal "indexFront" <$>) (enumerateSeqMap n xs)
       asWordList sym wvs >>= \case
         Just ws ->
           do z <- wordLit sym wlen 0
              return $ VWord $ wordVal $ SBV.svSelect ws z idx
         Nothing -> folded'

  | otherwise = folded'


 where
    k = SBV.kindOf idx

    f n (Just y) = Just $ iteValue sym (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y
    f n Nothing  = Just $ lookupSeqMap xs n

    folded' =
      case folded of
        Nothing -> raiseError sym (InvalidIndex Nothing)
        Just m  -> m

    folded =
      case k of
        KBounded _ w ->
          case mblen of
            Nat n | n < 2^w -> foldr f Nothing [0 .. n-1]
            _ -> foldr f Nothing [0 .. 2^w - 1]
        _ ->
          case mblen of
            Nat n -> foldr f Nothing [0 .. n-1]
            Inf -> Just (liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing")))

indexFront_segs ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV (GenValue SBV) ->
  TValue ->
  Integer ->
  [IndexSegment SBV] ->
  SEval SBV Value
indexFront_segs sym mblen a xs ix _idx_bits [WordIndexSegment w] =
  indexFront sym mblen a xs ix w

indexFront_segs sym mblen _a xs _ix idx_bits segs =
  do xs' <- barrelShifter sym (mergeValue sym) shiftOp mblen xs idx_bits segs
     lookupSeqMap xs' 0
  where
    shiftOp vs amt = pure (indexSeqMap (\i -> lookupSeqMap vs $! amt+i))


updateFrontSym ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV (GenValue SBV) ->
  Either (SInteger SBV) (WordValue SBV) ->
  SEval SBV (GenValue SBV) ->
  SEval SBV (SeqMap SBV (GenValue SBV))
updateFrontSym sym _len _eltTy vs (Left idx) val =
  case SBV.svAsInteger idx of
    Just i -> return $ updateSeqMap vs i val
    Nothing -> return $ indexSeqMap $ \i ->
      do b <- intEq sym idx =<< integerLit sym i
         iteValue sym b val (lookupSeqMap vs i)

updateFrontSym sym _len _eltTy vs (Right wv) val =
  wordValAsLit sym wv >>= \case
   Just j -> return $ updateSeqMap vs j val
   Nothing ->
      return $ indexSeqMap $ \i ->
      do b <- wordValueEqualsInteger sym wv i
         iteValue sym b val (lookupSeqMap vs i)

updateFrontSym_word ::
  SBV ->
  Nat' ->
  TValue ->
  WordValue SBV ->
  Either (SInteger SBV) (WordValue SBV) ->
  SEval SBV (GenValue SBV) ->
  SEval SBV (WordValue SBV)
updateFrontSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateFrontSym_bits"]

updateFrontSym_word sym (Nat n) _eltTy w (Left idx) val =
  do idx' <- wordFromInt sym n idx
     updateWordByWord sym IndexForward w (wordVal idx') (fromVBit <$> val)
updateFrontSym_word sym (Nat _n) _eltTy w (Right idx) val =
  updateWordByWord sym IndexForward w idx (fromVBit <$> val)


updateBackSym ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV (GenValue SBV) ->
  Either (SInteger SBV) (WordValue SBV) ->
  SEval SBV (GenValue SBV) ->
  SEval SBV (SeqMap SBV (GenValue SBV))
updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]

updateBackSym sym (Nat n) _eltTy vs (Left idx) val =
  case SBV.svAsInteger idx of
    Just i -> return $ updateSeqMap vs (n - 1 - i) val
    Nothing -> return $ indexSeqMap $ \i ->
      do b <- intEq sym idx =<< integerLit sym (n - 1 - i)
         iteValue sym b val (lookupSeqMap vs i)

updateBackSym sym (Nat n) _eltTy vs (Right wv) val =
  wordValAsLit sym wv >>= \case
    Just j -> return $ updateSeqMap vs (n - 1 - j) val
    Nothing ->
      return $ indexSeqMap $ \i ->
      do b <- wordValueEqualsInteger sym wv (n - 1 - i)
         iteValue sym b val (lookupSeqMap vs i)

updateBackSym_word ::
  SBV ->
  Nat' ->
  TValue ->
  WordValue SBV ->
  Either (SInteger SBV) (WordValue SBV) ->
  SEval SBV (GenValue SBV) ->
  SEval SBV (WordValue SBV)
updateBackSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym_bits"]

updateBackSym_word sym (Nat n) _eltTy w (Left idx) val =
  do idx' <- wordFromInt sym n idx
     updateWordByWord sym IndexBackward w (wordVal idx') (fromVBit <$> val)
updateBackSym_word sym (Nat _n) _eltTy w (Right idx) val =
  updateWordByWord sym IndexBackward w idx (fromVBit <$> val)