-- |
-- 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 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           Data.Bits (bit, shiftL)
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 ( EvalError(..), Unsupported(..) )
import Cryptol.Backend.SBV

import Cryptol.Eval.Type (TValue(..))
import Cryptol.Eval.Generic
import Cryptol.Eval.Prims
import Cryptol.Eval.Value
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger)
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 :: SBV -> IO EvalOpts -> Map PrimIdent (Prim SBV)
primTable SBV
sym IO EvalOpts
getEOpts =
  Map PrimIdent (Prim SBV)
-> Map PrimIdent (Prim SBV) -> Map PrimIdent (Prim SBV)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (SBV -> IO EvalOpts -> Map PrimIdent (Prim SBV)
forall sym.
Backend sym =>
sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
genericPrimTable SBV
sym IO EvalOpts
getEOpts) (Map PrimIdent (Prim SBV) -> Map PrimIdent (Prim SBV))
-> Map PrimIdent (Prim SBV) -> Map PrimIdent (Prim SBV)
forall a b. (a -> b) -> a -> b
$
  [(PrimIdent, Prim SBV)] -> Map PrimIdent (Prim SBV)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PrimIdent, Prim SBV)] -> Map PrimIdent (Prim SBV))
-> [(PrimIdent, Prim SBV)] -> Map PrimIdent (Prim SBV)
forall a b. (a -> b) -> a -> b
$ ((String, Prim SBV) -> (PrimIdent, Prim SBV))
-> [(String, Prim SBV)] -> [(PrimIdent, Prim SBV)]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
n, Prim SBV
v) -> (Text -> PrimIdent
prelPrim (String -> Text
T.pack String
n), Prim SBV
v))

  [ (String
">>$"         , SBV -> Prim SBV
sshrV SBV
sym)

    -- Shifts and rotates
  , (String
"<<"          , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim SBV
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift SBV
sym String
"<<"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
shl SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
lshr SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex)

  , (String
">>"          , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim SBV
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift SBV
sym String
">>"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
lshr SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
shl SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex)

  , (String
"<<<"         , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim SBV
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift SBV
sym String
"<<<"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateLeft SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateRight SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex)

  , (String
">>>"         , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim SBV
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift SBV
sym String
">>>"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateRight SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateLeft SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex)

    -- Indexing and updates
  , (String
"@"           , SBV
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> SInteger SBV
    -> SEval SBV (GenValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> [SBit SBV]
    -> SEval SBV (GenValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> SWord SBV
    -> SEval SBV (GenValue SBV))
-> Prim SBV
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SInteger sym
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> [SBit sym]
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SWord sym
    -> SEval sym (GenValue sym))
-> Prim sym
indexPrim SBV
sym (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SVal
-> SEval SBV (GenValue SBV)
indexFront SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV (GenValue SBV)
indexFront_bits SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SVal
-> SEval SBV (GenValue SBV)
indexFront SBV
sym))
  , (String
"!"           , SBV
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> SInteger SBV
    -> SEval SBV (GenValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> [SBit SBV]
    -> SEval SBV (GenValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> SWord SBV
    -> SEval SBV (GenValue SBV))
-> Prim SBV
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SInteger sym
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> [SBit sym]
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SWord sym
    -> SEval sym (GenValue sym))
-> Prim sym
indexPrim SBV
sym (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SWord SBV
-> SEval SBV (GenValue SBV)
indexBack SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV (GenValue SBV)
indexBack_bits SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SWord SBV
-> SEval SBV (GenValue SBV)
indexBack SBV
sym))

  , (String
"update"      , SBV
-> (Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (WordValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV))
-> Prim SBV
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> WordValue sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (WordValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> Prim sym
updatePrim SBV
sym (SBV
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (WordValue SBV)
updateFrontSym_word SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym))
  , (String
"updateEnd"   , SBV
-> (Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (WordValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV))
-> Prim SBV
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> WordValue sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (WordValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> Prim sym
updatePrim SBV
sym (SBV
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (WordValue SBV)
updateBackSym_word SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (SeqMap SBV)
updateBackSym SBV
sym))

  ]

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

  | Nat Integer
n <- Nat'
mblen
  , TVSeq Integer
wlen TValue
TVBit <- TValue
a
  = do [WordValue SBV]
wvs <- (SBVEval (GenValue SBV) -> SBVEval (WordValue SBV))
-> [SBVEval (GenValue SBV)] -> SBVEval [WordValue SBV]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (String -> GenValue SBV -> SEval SBV (WordValue SBV)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
"indexFront" (GenValue SBV -> SBVEval (WordValue SBV))
-> SBVEval (GenValue SBV) -> SBVEval (WordValue SBV)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer -> SeqMap SBV -> [SEval SBV (GenValue SBV)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n SeqMap SBV
xs)
       case [WordValue SBV] -> Maybe [SWord SBV]
asWordList [WordValue SBV]
wvs of
         Just [SWord SBV]
ws ->
           do SVal
z <- SBV -> Integer -> Integer -> SEval SBV (SWord SBV)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit SBV
sym Integer
wlen Integer
0
              GenValue SBV -> SBVEval (GenValue SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBV -> SBVEval (GenValue SBV))
-> GenValue SBV -> SBVEval (GenValue SBV)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval SBV (WordValue SBV) -> GenValue SBV
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
wlen (SEval SBV (WordValue SBV) -> GenValue SBV)
-> SEval SBV (WordValue SBV) -> GenValue SBV
forall a b. (a -> b) -> a -> b
$ WordValue SBV -> SBVEval (WordValue SBV)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue SBV -> SBVEval (WordValue SBV))
-> WordValue SBV -> SBVEval (WordValue SBV)
forall a b. (a -> b) -> a -> b
$ SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SWord SBV -> WordValue SBV) -> SWord SBV -> WordValue SBV
forall a b. (a -> b) -> a -> b
$ [SVal] -> SVal -> SVal -> SVal
SBV.svSelect [SVal]
[SWord SBV]
ws SVal
z SVal
idx
         Maybe [SWord SBV]
Nothing -> SBVEval (GenValue SBV)
folded

  | Bool
otherwise
  = SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
folded

 where
    k :: Kind
k = SVal -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf SVal
idx
    def :: SEval SBV (GenValue SBV)
def = SBV -> TValue -> SEval SBV (GenValue SBV)
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV SBV
sym TValue
a
    f :: Integer -> SBVEval (GenValue SBV) -> SEval SBV (GenValue SBV)
f Integer
n SBVEval (GenValue SBV)
y = SBV
-> SBit SBV
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue SBV
sym (SVal -> SVal -> SVal
SBV.svEqual SVal
idx (Kind -> Integer -> SVal
SBV.svInteger Kind
k Integer
n)) (SeqMap SBV -> Integer -> SEval SBV (GenValue SBV)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
xs Integer
n) SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
y
    folded :: SBVEval (GenValue SBV)
folded =
      case Kind
k of
        KBounded Bool
_ Int
w ->
          case Nat'
mblen of
            Nat Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w -> (Integer -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV))
-> SBVEval (GenValue SBV) -> [Integer] -> SBVEval (GenValue SBV)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer -> SBVEval (GenValue SBV) -> SEval SBV (GenValue SBV)
Integer -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV)
f SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
def [Integer
0 .. Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1]
            Nat'
_ -> (Integer -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV))
-> SBVEval (GenValue SBV) -> [Integer] -> SBVEval (GenValue SBV)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer -> SBVEval (GenValue SBV) -> SEval SBV (GenValue SBV)
Integer -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV)
f SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
def [Integer
0 .. Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1]
        Kind
_ ->
          case Nat'
mblen of
            Nat Integer
n -> (Integer -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV))
-> SBVEval (GenValue SBV) -> [Integer] -> SBVEval (GenValue SBV)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer -> SBVEval (GenValue SBV) -> SEval SBV (GenValue SBV)
Integer -> SBVEval (GenValue SBV) -> SBVEval (GenValue SBV)
f SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
def [Integer
0 .. Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1]
            Nat'
Inf -> IO (GenValue SBV) -> SBVEval (GenValue SBV)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Unsupported -> IO (GenValue SBV)
forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
"unbounded integer indexing"))

indexBack ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  TValue ->
  SWord SBV ->
  SEval SBV Value
indexBack :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SWord SBV
-> SEval SBV (GenValue SBV)
indexBack SBV
sym (Nat Integer
n) TValue
a SeqMap SBV
xs TValue
ix SWord SBV
idx = SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SVal
-> SEval SBV (GenValue SBV)
indexFront SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
a (Integer -> SeqMap SBV -> SeqMap SBV
forall sym. Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
n SeqMap SBV
xs) TValue
ix SVal
SWord SBV
idx
indexBack SBV
_ Nat'
Inf TValue
_ SeqMap SBV
_ TValue
_ SWord SBV
_ = String -> [String] -> SBVEval (GenValue SBV)
forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"indexBack"]

indexFront_bits ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  TValue ->
  [SBit SBV] ->
  SEval SBV Value
indexFront_bits :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV (GenValue SBV)
indexFront_bits SBV
sym Nat'
mblen TValue
_a SeqMap SBV
xs TValue
_ix [SBit SBV]
bits0 = Integer -> Int -> [SBit SBV] -> SEval SBV (GenValue SBV)
go Integer
0 ([SVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SVal]
[SBit SBV]
bits0) [SBit SBV]
bits0
 where
  go :: Integer -> Int -> [SBit SBV] -> SEval SBV Value
  go :: Integer -> Int -> [SBit SBV] -> SEval SBV (GenValue SBV)
go Integer
i Int
_k []
    -- For indices out of range, fail
    | Nat Integer
n <- Nat'
mblen
    , Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
    = SBV -> EvalError -> SEval SBV (GenValue SBV)
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError SBV
sym (Maybe Integer -> EvalError
InvalidIndex (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i))

    | Bool
otherwise
    = SeqMap SBV -> Integer -> SEval SBV (GenValue SBV)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
xs Integer
i

  go Integer
i Int
k (SBit SBV
b:[SBit SBV]
bs)
    -- Fail early when all possible indices we could compute from here
    -- are out of bounds
    | Nat Integer
n <- Nat'
mblen
    , (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
    = SBV -> EvalError -> SEval SBV (GenValue SBV)
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError SBV
sym (Maybe Integer -> EvalError
InvalidIndex Maybe Integer
forall a. Maybe a
Nothing)

    | Bool
otherwise
    = SBV
-> SBit SBV
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue SBV
sym SBit SBV
b
         (Integer -> Int -> [SBit SBV] -> SEval SBV (GenValue SBV)
go ((Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SBit SBV]
bs)
         (Integer -> Int -> [SBit SBV] -> SEval SBV (GenValue SBV)
go  (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
1)      (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SBit SBV]
bs)


indexBack_bits ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  TValue ->
  [SBit SBV] ->
  SEval SBV Value
indexBack_bits :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV (GenValue SBV)
indexBack_bits SBV
sym (Nat Integer
n) TValue
a SeqMap SBV
xs TValue
ix [SBit SBV]
idx = SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV (GenValue SBV)
indexFront_bits SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
a (Integer -> SeqMap SBV -> SeqMap SBV
forall sym. Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
n SeqMap SBV
xs) TValue
ix [SBit SBV]
idx
indexBack_bits SBV
_ Nat'
Inf TValue
_ SeqMap SBV
_ TValue
_ [SBit SBV]
_ = String -> [String] -> SBVEval (GenValue SBV)
forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"indexBack_bits"]


-- | Compare a symbolic word value with a concrete integer.
wordValueEqualsInteger :: SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
wordValueEqualsInteger :: SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
wordValueEqualsInteger SBV
sym WordValue SBV
wv Integer
i
  | SBV -> WordValue SBV -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize SBV
sym WordValue SBV
wv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Integer
widthInteger Integer
i = SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return SVal
SBV.svFalse
  | Bool
otherwise =
    case WordValue SBV
wv of
      WordVal SWord SBV
w -> SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
SBV.svEqual SVal
SWord SBV
w (Int -> Integer -> SWord SBV
literalSWord (SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
w) Integer
i)
      WordValue SBV
_ -> Integer -> [SBit SBV] -> SBit SBV
bitsAre Integer
i ([SVal] -> SVal) -> SBVEval [SVal] -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> WordValue SBV -> SEval SBV [SBit SBV]
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev SBV
sym WordValue SBV
wv -- little-endian
  where
    bitsAre :: Integer -> [SBit SBV] -> SBit SBV
    bitsAre :: Integer -> [SBit SBV] -> SBit SBV
bitsAre Integer
n [] = Bool -> SVal
SBV.svBool (Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
    bitsAre Integer
n (SBit SBV
b : [SBit SBV]
bs) = SVal -> SVal -> SVal
SBV.svAnd (Bool -> SBit SBV -> SBit SBV
bitIs (Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
n) SBit SBV
b) (Integer -> [SBit SBV] -> SBit SBV
bitsAre (Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2) [SBit SBV]
bs)

    bitIs :: Bool -> SBit SBV -> SBit SBV
    bitIs :: Bool -> SBit SBV -> SBit SBV
bitIs Bool
b SBit SBV
x = if Bool
b then SBit SBV
x else SVal -> SVal
SBV.svNot SVal
SBit SBV
x


updateFrontSym ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  Either (SInteger SBV) (WordValue SBV) ->
  SEval SBV (GenValue SBV) ->
  SEval SBV (SeqMap SBV)
updateFrontSym :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym Nat'
_len TValue
_eltTy SeqMap SBV
vs (Left SInteger SBV
idx) SEval SBV (GenValue SBV)
val =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
idx of
    Just Integer
i -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap SBV
vs Integer
i SEval SBV (GenValue SBV)
val
    Maybe Integer
Nothing -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV)
-> (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SVal
b <- SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq SBV
sym SInteger SBV
idx (SVal -> SBVEval SVal) -> SBVEval SVal -> SBVEval SVal
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym Integer
i
         SBV
-> SBit SBV
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue SBV
sym SVal
SBit SBV
b SEval SBV (GenValue SBV)
val (SeqMap SBV -> Integer -> SEval SBV (GenValue SBV)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
vs Integer
i)

updateFrontSym SBV
sym Nat'
_len TValue
_eltTy SeqMap SBV
vs (Right WordValue SBV
wv) SEval SBV (GenValue SBV)
val =
  case WordValue SBV
wv of
    WordVal SWord SBV
w | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
w ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap SBV
vs Integer
j SEval SBV (GenValue SBV)
val
    WordValue SBV
_ ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV)
-> (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SVal
b <- SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
wordValueEqualsInteger SBV
sym WordValue SBV
wv Integer
i
         SBV
-> SBit SBV
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue SBV
sym SVal
SBit SBV
b SEval SBV (GenValue SBV)
val (SeqMap SBV -> Integer -> SEval SBV (GenValue SBV)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
vs Integer
i)

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

updateFrontSym_word SBV
sym (Nat Integer
_) TValue
eltTy (LargeBitsVal Integer
n SeqMap SBV
bv) Either (SInteger SBV) (WordValue SBV)
idx SEval SBV (GenValue SBV)
val =
  Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy SeqMap SBV
bv Either (SInteger SBV) (WordValue SBV)
idx SEval SBV (GenValue SBV)
val

updateFrontSym_word SBV
sym (Nat Integer
n) TValue
eltTy (WordVal SWord SBV
bv) (Left SInteger SBV
idx) SEval SBV (GenValue SBV)
val =
  do SVal
idx' <- SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt SBV
sym Integer
n SInteger SBV
idx
     SBV
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (WordValue SBV)
updateFrontSym_word SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SWord SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SVal
SWord SBV
idx')) SEval SBV (GenValue SBV)
val

updateFrontSym_word SBV
sym (Nat Integer
n) TValue
eltTy WordValue SBV
bv (Right WordValue SBV
wv) SEval SBV (GenValue SBV)
val =
  case WordValue SBV
wv of
    WordVal SWord SBV
idx
      | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
idx ->
          SBV
-> WordValue SBV
-> Integer
-> SEval SBV (SBit SBV)
-> SEval SBV (WordValue SBV)
forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue SBV
sym WordValue SBV
bv Integer
j (GenValue SBV -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
val)

      | WordVal SWord SBV
bw <- WordValue SBV
bv ->
        SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> WordValue SBV) -> SBVEval SVal -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          do SVal
b <- GenValue SBV -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
val
             let sz :: Int
sz   = SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
bw
             let z :: SWord SBV
z    = Int -> Integer -> SWord SBV
literalSWord Int
sz Integer
0
             let znot :: SVal
znot = SVal -> SVal
SBV.svNot SVal
SWord SBV
z
             let q :: SVal
q    = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
SBV.svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf SVal
SWord SBV
bw) Bool
True SVal
b SVal
znot SVal
SWord SBV
z
             let msk :: SVal
msk  = SVal -> SVal -> SVal
SBV.svShiftRight (Int -> Integer -> SWord SBV
literalSWord Int
sz (Int -> Integer
forall a. Bits a => Int -> a
bit (Int
szInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))) SVal
SWord SBV
idx
             let bw' :: SVal
bw'  = SVal -> SVal -> SVal
SBV.svAnd SVal
SWord SBV
bw (SVal -> SVal
SBV.svNot SVal
msk)
             SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
SBV.svXOr SVal
bw' (SVal -> SVal -> SVal
SBV.svAnd SVal
q SVal
msk)

    WordValue SBV
_ -> Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SBV -> WordValue SBV -> SeqMap SBV
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap SBV
sym WordValue SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right WordValue SBV
wv) SEval SBV (GenValue SBV)
val


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

updateBackSym SBV
sym (Nat Integer
n) TValue
_eltTy SeqMap SBV
vs (Left SInteger SBV
idx) SEval SBV (GenValue SBV)
val =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
idx of
    Just Integer
i -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap SBV
vs (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i) SEval SBV (GenValue SBV)
val
    Maybe Integer
Nothing -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV)
-> (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SVal
b <- SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq SBV
sym SInteger SBV
idx (SVal -> SBVEval SVal) -> SBVEval SVal -> SBVEval SVal
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
         SBV
-> SBit SBV
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue SBV
sym SVal
SBit SBV
b SEval SBV (GenValue SBV)
val (SeqMap SBV -> Integer -> SEval SBV (GenValue SBV)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
vs Integer
i)

updateBackSym SBV
sym (Nat Integer
n) TValue
_eltTy SeqMap SBV
vs (Right WordValue SBV
wv) SEval SBV (GenValue SBV)
val =
  case WordValue SBV
wv of
    WordVal SWord SBV
w | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
w ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap SBV
vs (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) SEval SBV (GenValue SBV)
val
    WordValue SBV
_ ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV)
-> (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SVal
b <- SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
wordValueEqualsInteger SBV
sym WordValue SBV
wv (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
         SBV
-> SBit SBV
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (GenValue SBV)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue SBV
sym SVal
SBit SBV
b SEval SBV (GenValue SBV)
val (SeqMap SBV -> Integer -> SEval SBV (GenValue SBV)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
vs Integer
i)

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

updateBackSym_word SBV
sym (Nat Integer
_) TValue
eltTy (LargeBitsVal Integer
n SeqMap SBV
bv) Either (SInteger SBV) (WordValue SBV)
idx SEval SBV (GenValue SBV)
val =
  Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (SeqMap SBV)
updateBackSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy SeqMap SBV
bv Either (SInteger SBV) (WordValue SBV)
idx SEval SBV (GenValue SBV)
val

updateBackSym_word SBV
sym (Nat Integer
n) TValue
eltTy (WordVal SWord SBV
bv) (Left SInteger SBV
idx) SEval SBV (GenValue SBV)
val =
  do SVal
idx' <- SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt SBV
sym Integer
n SInteger SBV
idx
     SBV
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (WordValue SBV)
updateBackSym_word SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SWord SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SVal
SWord SBV
idx')) SEval SBV (GenValue SBV)
val

updateBackSym_word SBV
sym (Nat Integer
n) TValue
eltTy WordValue SBV
bv (Right WordValue SBV
wv) SEval SBV (GenValue SBV)
val = do
  case WordValue SBV
wv of
    WordVal SWord SBV
idx
      | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
idx ->
          SBV
-> WordValue SBV
-> Integer
-> SEval SBV (SBit SBV)
-> SEval SBV (WordValue SBV)
forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue SBV
sym WordValue SBV
bv (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) (GenValue SBV -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
val)

      | WordVal SWord SBV
bw <- WordValue SBV
bv ->
        SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> WordValue SBV) -> SBVEval SVal -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          do SVal
b <- GenValue SBV -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV (GenValue SBV)
SBVEval (GenValue SBV)
val
             let sz :: Int
sz   = SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
bw
             let z :: SWord SBV
z    = Int -> Integer -> SWord SBV
literalSWord Int
sz Integer
0
             let znot :: SVal
znot = SVal -> SVal
SBV.svNot SVal
SWord SBV
z
             let q :: SVal
q    = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
SBV.svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf SVal
SWord SBV
bw) Bool
True SVal
b SVal
znot SVal
SWord SBV
z
             let msk :: SVal
msk  = SVal -> SVal -> SVal
SBV.svShiftLeft (Int -> Integer -> SWord SBV
literalSWord Int
sz Integer
1) SVal
SWord SBV
idx
             let bw' :: SVal
bw'  = SVal -> SVal -> SVal
SBV.svAnd SVal
SWord SBV
bw (SVal -> SVal
SBV.svNot SVal
msk)
             SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
SBV.svXOr SVal
bw' (SVal -> SVal -> SVal
SBV.svAnd SVal
q SVal
msk)

    WordValue SBV
_ -> Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV (GenValue SBV)
-> SEval SBV (SeqMap SBV)
updateBackSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SBV -> WordValue SBV -> SeqMap SBV
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap SBV
sym WordValue SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right WordValue SBV
wv) SEval SBV (GenValue SBV)
val


asWordList :: [WordValue SBV] -> Maybe [SWord SBV]
asWordList :: [WordValue SBV] -> Maybe [SWord SBV]
asWordList = ([SWord SBV] -> [SWord SBV])
-> [WordValue SBV] -> Maybe [SWord SBV]
go [SWord SBV] -> [SWord SBV]
forall a. a -> a
id
 where go :: ([SWord SBV] -> [SWord SBV]) -> [WordValue SBV] -> Maybe [SWord SBV]
       go :: ([SWord SBV] -> [SWord SBV])
-> [WordValue SBV] -> Maybe [SWord SBV]
go [SWord SBV] -> [SWord SBV]
f [] = [SVal] -> Maybe [SVal]
forall a. a -> Maybe a
Just ([SWord SBV] -> [SWord SBV]
f [])
       go [SWord SBV] -> [SWord SBV]
f (WordVal SWord SBV
x :[WordValue SBV]
vs) = ([SWord SBV] -> [SWord SBV])
-> [WordValue SBV] -> Maybe [SWord SBV]
go ([SVal] -> [SVal]
[SWord SBV] -> [SWord SBV]
f ([SVal] -> [SVal]) -> ([SVal] -> [SVal]) -> [SVal] -> [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal
SWord SBV
xSVal -> [SVal] -> [SVal]
forall a. a -> [a] -> [a]
:)) [WordValue SBV]
vs
       go [SWord SBV] -> [SWord SBV]
_f (LargeBitsVal Integer
_ SeqMap SBV
_ : [WordValue SBV]
_) = Maybe [SWord SBV]
forall a. Maybe a
Nothing

sshrV :: SBV -> Prim SBV
sshrV :: SBV -> Prim SBV
sshrV SBV
sym =
  (Nat' -> Prim SBV) -> Prim SBV
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
n ->
  (TValue -> Prim SBV) -> Prim SBV
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly  \TValue
ix ->
  (SWord SBV -> Prim SBV) -> Prim SBV
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord SBV
x ->
  (GenValue SBV -> Prim SBV) -> Prim SBV
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict  \GenValue SBV
y ->
  SEval SBV (GenValue SBV) -> Prim SBV
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (SEval SBV (GenValue SBV) -> Prim SBV)
-> SEval SBV (GenValue SBV) -> Prim SBV
forall a b. (a -> b) -> a -> b
$
   SBV
-> String
-> TValue
-> GenValue SBV
-> SEval SBV (Either (SInteger SBV) (WordValue SBV))
forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> SEval sym (Either (SInteger sym) (WordValue sym))
asIndex SBV
sym String
">>$" TValue
ix GenValue SBV
y SBVEval (Either SVal (WordValue SBV))
-> (Either SVal (WordValue SBV) -> SBVEval (GenValue SBV))
-> SBVEval (GenValue SBV)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     Left SVal
idx ->
       do let w :: Integer
w = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
x)
          let pneg :: SVal
pneg = SVal -> SVal -> SVal
svLessThan SVal
idx (Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
0)
          SVal
zneg <- SVal -> SVal -> SVal
shl SVal
SWord SBV
x  (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SInteger SBV -> SWord SBV
svFromInteger Integer
w (SVal -> SVal) -> SBVEval SVal -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink SBV
sym Nat'
n TValue
ix (SVal -> SVal
SBV.svUNeg SVal
idx)
          SVal
zpos <- SVal -> SVal -> SVal
ashr SVal
SWord SBV
x (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SInteger SBV -> SWord SBV
svFromInteger Integer
w (SVal -> SVal) -> SBVEval SVal -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink SBV
sym Nat'
n TValue
ix SVal
SInteger SBV
idx
          let z :: SVal
z = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
SWord SBV
x) Bool
True SVal
pneg SVal
zneg SVal
zpos
          GenValue SBV -> SBVEval (GenValue SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBV -> SBVEval (GenValue SBV))
-> (SVal -> GenValue SBV) -> SVal -> SBVEval (GenValue SBV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SEval SBV (WordValue SBV) -> GenValue SBV
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SBVEval (WordValue SBV) -> GenValue SBV)
-> (SVal -> SBVEval (WordValue SBV)) -> SVal -> GenValue SBV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBV -> SBVEval (WordValue SBV)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue SBV -> SBVEval (WordValue SBV))
-> (SVal -> WordValue SBV) -> SVal -> SBVEval (WordValue SBV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> SBVEval (GenValue SBV)) -> SVal -> SBVEval (GenValue SBV)
forall a b. (a -> b) -> a -> b
$ SVal
z

     Right WordValue SBV
wv ->
       do SVal
z <- SVal -> SVal -> SVal
ashr SVal
SWord SBV
x (SVal -> SVal) -> SBVEval SVal -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> WordValue SBV -> SEval SBV (SWord SBV)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal SBV
sym WordValue SBV
wv
          GenValue SBV -> SBVEval (GenValue SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBV -> SBVEval (GenValue SBV))
-> (SVal -> GenValue SBV) -> SVal -> SBVEval (GenValue SBV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SEval SBV (WordValue SBV) -> GenValue SBV
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
x)) (SBVEval (WordValue SBV) -> GenValue SBV)
-> (SVal -> SBVEval (WordValue SBV)) -> SVal -> GenValue SBV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBV -> SBVEval (WordValue SBV)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue SBV -> SBVEval (WordValue SBV))
-> (SVal -> WordValue SBV) -> SVal -> SBVEval (WordValue SBV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> SBVEval (GenValue SBV)) -> SVal -> SBVEval (GenValue SBV)
forall a b. (a -> b) -> a -> b
$ SVal
z