{-# Language NamedFieldPuns #-}
{-# Language DataKinds #-}
{-# Language OverloadedStrings #-}
{-# Language TypeApplications #-}
{-# Language ScopedTypeVariables #-}

module EVM.Symbolic where

import Prelude hiding  (Word, LT, GT)
import qualified Data.ByteString as BS
import Data.ByteString (ByteString)
import Control.Lens hiding (op, (:<), (|>), (.>))
import Data.Maybe                   (fromMaybe, fromJust)

import EVM.Types
import qualified EVM.Concrete as Concrete
import qualified Data.ByteArray       as BA
import Data.SBV hiding (runSMT, newArray_, addAxiom, Word)
import Data.SBV.Tools.Overflow
import Crypto.Hash (Digest, SHA256)
import qualified Crypto.Hash as Crypto

litWord :: Word -> SymWord
litWord :: Word -> SymWord
litWord (C Whiff
whiff W256
a) = Whiff -> SWord 256 -> SymWord
S Whiff
whiff (WordN 256 -> SWord 256
forall a. SymVal a => a -> SBV a
literal (WordN 256 -> SWord 256) -> WordN 256 -> SWord 256
forall a b. (a -> b) -> a -> b
$ W256 -> ToSizzle W256
forall a. ToSizzleBV a => a -> ToSizzle a
toSizzle W256
a)

litAddr :: Addr -> SAddr
litAddr :: Addr -> SAddr
litAddr = SWord 160 -> SAddr
SAddr (SWord 160 -> SAddr) -> (Addr -> SWord 160) -> Addr -> SAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN 160 -> SWord 160
forall a. SymVal a => a -> SBV a
literal (WordN 160 -> SWord 160)
-> (Addr -> WordN 160) -> Addr -> SWord 160
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> WordN 160
forall a. ToSizzleBV a => a -> ToSizzle a
toSizzle

maybeLitAddr :: SAddr -> Maybe Addr
maybeLitAddr :: SAddr -> Maybe Addr
maybeLitAddr (SAddr SWord 160
a) = (WordN 160 -> Addr) -> Maybe (WordN 160) -> Maybe Addr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WordN 160 -> Addr
forall a. FromSizzleBV a => a -> FromSizzle a
fromSizzle (SWord 160 -> Maybe (WordN 160)
forall a. SymVal a => SBV a -> Maybe a
unliteral SWord 160
a)

maybeLitBytes :: [SWord 8] -> Maybe ByteString
maybeLitBytes :: [SWord 8] -> Maybe ByteString
maybeLitBytes [SWord 8]
xs = ([WordN 8] -> ByteString) -> Maybe [WordN 8] -> Maybe ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[WordN 8]
x -> [Word8] -> ByteString
BS.pack ((WordN 8 -> Word8) -> [WordN 8] -> [Word8]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WordN 8 -> Word8
forall a. FromSizedBV a => a -> FromSized a
fromSized [WordN 8]
x)) ((SWord 8 -> Maybe (WordN 8)) -> [SWord 8] -> Maybe [WordN 8]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SWord 8 -> Maybe (WordN 8)
forall a. SymVal a => SBV a -> Maybe a
unliteral [SWord 8]
xs)

-- | Note: the (force*) functions are crude and in general,
-- the continuation passing style `forceConcrete`
-- alternatives should be prefered for better error
-- handling when used during EVM execution
forceLit :: SymWord -> Word
forceLit :: SymWord -> Word
forceLit (S Whiff
whiff SWord 256
a) = case SWord 256 -> Maybe (WordN 256)
forall a. SymVal a => SBV a -> Maybe a
unliteral SWord 256
a of
  Just WordN 256
c -> Whiff -> W256 -> Word
C Whiff
whiff (WordN 256 -> FromSizzle (WordN 256)
forall a. FromSizzleBV a => a -> FromSizzle a
fromSizzle WordN 256
c)
  Maybe (WordN 256)
Nothing -> [Char] -> Word
forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected symbolic argument"

forceLitBytes :: [SWord 8] -> ByteString
forceLitBytes :: [SWord 8] -> ByteString
forceLitBytes = [Word8] -> ByteString
BS.pack ([Word8] -> ByteString)
-> ([SWord 8] -> [Word8]) -> [SWord 8] -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SWord 8 -> Word8) -> [SWord 8] -> [Word8]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (WordN 8 -> Word8
forall a. FromSizedBV a => a -> FromSized a
fromSized (WordN 8 -> Word8) -> (SWord 8 -> WordN 8) -> SWord 8 -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (WordN 8) -> WordN 8
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN 8) -> WordN 8)
-> (SWord 8 -> Maybe (WordN 8)) -> SWord 8 -> WordN 8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 8 -> Maybe (WordN 8)
forall a. SymVal a => SBV a -> Maybe a
unliteral)

forceBuffer :: Buffer -> ByteString
forceBuffer :: Buffer -> ByteString
forceBuffer (ConcreteBuffer ByteString
b) = ByteString
b
forceBuffer (SymbolicBuffer [SWord 8]
b) = [SWord 8] -> ByteString
forceLitBytes [SWord 8]
b

sdiv :: SymWord -> SymWord -> SymWord
sdiv :: SymWord -> SymWord -> SymWord
sdiv (S Whiff
a SWord 256
x) (S Whiff
b SWord 256
y) = let sx, sy :: SInt 256
                           sx :: SInt 256
sx = SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
x
                           sy :: SInt 256
sy = SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
y
                       in Whiff -> SWord 256 -> SymWord
S (Whiff -> Whiff -> Whiff
Div Whiff
a Whiff
b) (SInt 256 -> SWord 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (SInt 256
sx SInt 256 -> SInt 256 -> SInt 256
forall a. SDivisible a => a -> a -> a
`sQuot` SInt 256
sy))

smod :: SymWord -> SymWord -> SymWord
smod :: SymWord -> SymWord -> SymWord
smod (S Whiff
a SWord 256
x) (S Whiff
b SWord 256
y) = let sx, sy :: SInt 256
                           sx :: SInt 256
sx = SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
x
                           sy :: SInt 256
sy = SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
y
                       in Whiff -> SWord 256 -> SymWord
S (Whiff -> Whiff -> Whiff
Mod Whiff
a Whiff
b) (SWord 256 -> SymWord) -> SWord 256 -> SymWord
forall a b. (a -> b) -> a -> b
$ SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (SWord 256
y SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
0) SWord 256
0 (SInt 256 -> SWord 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (SInt 256
sx SInt 256 -> SInt 256 -> SInt 256
forall a. SDivisible a => a -> a -> a
`sRem` SInt 256
sy))

addmod :: SymWord -> SymWord -> SymWord -> SymWord
addmod :: SymWord -> SymWord -> SymWord -> SymWord
addmod (S Whiff
a SWord 256
x) (S Whiff
b SWord 256
y) (S Whiff
c SWord 256
z) = let to512 :: SWord 256 -> SWord 512
                                     to512 :: SWord 256 -> SWord 512
to512 = SWord 256 -> SWord 512
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral
                                 in  Whiff -> SWord 256 -> SymWord
S ([Char] -> [Whiff] -> Whiff
Todo [Char]
"addmod" [Whiff
a, Whiff
b, Whiff
c]) (SWord 256 -> SymWord) -> SWord 256 -> SymWord
forall a b. (a -> b) -> a -> b
$ SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (SWord 256
z SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
0) SWord 256
0 (SWord 256 -> SWord 256) -> SWord 256 -> SWord 256
forall a b. (a -> b) -> a -> b
$ SWord 512 -> SWord 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (SWord 512 -> SWord 256) -> SWord 512 -> SWord 256
forall a b. (a -> b) -> a -> b
$ ((SWord 256 -> SWord 512
to512 SWord 256
x) SWord 512 -> SWord 512 -> SWord 512
forall a. Num a => a -> a -> a
+ (SWord 256 -> SWord 512
to512 SWord 256
y)) SWord 512 -> SWord 512 -> SWord 512
forall a. SDivisible a => a -> a -> a
`sMod` (SWord 256 -> SWord 512
to512 SWord 256
z)

mulmod :: SymWord -> SymWord -> SymWord -> SymWord
mulmod :: SymWord -> SymWord -> SymWord -> SymWord
mulmod (S Whiff
a SWord 256
x) (S Whiff
b SWord 256
y) (S Whiff
c SWord 256
z) = let to512 :: SWord 256 -> SWord 512
                                     to512 :: SWord 256 -> SWord 512
to512 = SWord 256 -> SWord 512
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral
                                 in Whiff -> SWord 256 -> SymWord
S ([Char] -> [Whiff] -> Whiff
Todo [Char]
"mulmod" [Whiff
a, Whiff
b, Whiff
c]) (SWord 256 -> SymWord) -> SWord 256 -> SymWord
forall a b. (a -> b) -> a -> b
$ SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (SWord 256
z SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
0) SWord 256
0 (SWord 256 -> SWord 256) -> SWord 256 -> SWord 256
forall a b. (a -> b) -> a -> b
$ SWord 512 -> SWord 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral (SWord 512 -> SWord 256) -> SWord 512 -> SWord 256
forall a b. (a -> b) -> a -> b
$ ((SWord 256 -> SWord 512
to512 SWord 256
x) SWord 512 -> SWord 512 -> SWord 512
forall a. Num a => a -> a -> a
* (SWord 256 -> SWord 512
to512 SWord 256
y)) SWord 512 -> SWord 512 -> SWord 512
forall a. SDivisible a => a -> a -> a
`sMod` (SWord 256 -> SWord 512
to512 SWord 256
z)

-- | Signed less than
slt :: SymWord -> SymWord -> SymWord
slt :: SymWord -> SymWord -> SymWord
slt (S Whiff
xw SWord 256
x) (S Whiff
yw SWord 256
y) =
  Whiff -> SBool -> SWord 256 -> SWord 256 -> SymWord
iteWhiff (Whiff -> Whiff -> Whiff
SLT Whiff
xw Whiff
yw) (SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
x SInt 256 -> SInt 256 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< (SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
y :: (SInt 256))) SWord 256
1 SWord 256
0

-- | Signed greater than
sgt :: SymWord -> SymWord -> SymWord
sgt :: SymWord -> SymWord -> SymWord
sgt (S Whiff
xw SWord 256
x) (S Whiff
yw SWord 256
y) =
  Whiff -> SBool -> SWord 256 -> SWord 256 -> SymWord
iteWhiff (Whiff -> Whiff -> Whiff
SGT Whiff
xw Whiff
yw) (SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
x SInt 256 -> SInt 256 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> (SWord 256 -> SInt 256
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 256
y :: (SInt 256))) SWord 256
1 SWord 256
0

-- * Operations over symbolic memory (list of symbolic bytes)
swordAt :: Int -> [SWord 8] -> SymWord
swordAt :: Int -> [SWord 8] -> SymWord
swordAt Int
i [SWord 8]
bs = let bs' :: [SWord 8]
bs' = Int -> [SWord 8] -> [SWord 8]
truncpad Int
32 ([SWord 8] -> [SWord 8]) -> [SWord 8] -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
i [SWord 8]
bs
               in Whiff -> SWord 256 -> SymWord
S (Buffer -> Whiff
FromBytes ([SWord 8] -> Buffer
SymbolicBuffer [SWord 8]
bs')) ([SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes [SWord 8]
bs')

readByteOrZero' :: Int -> [SWord 8] -> SWord 8
readByteOrZero' :: Int -> [SWord 8] -> SWord 8
readByteOrZero' Int
i [SWord 8]
bs = SWord 8 -> Maybe (SWord 8) -> SWord 8
forall a. a -> Maybe a -> a
fromMaybe SWord 8
0 ([SWord 8]
bs [SWord 8]
-> Getting (First (SWord 8)) [SWord 8] (SWord 8) -> Maybe (SWord 8)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index [SWord 8] -> Traversal' [SWord 8] (IxValue [SWord 8])
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Int
Index [SWord 8]
i)

sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8]
sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8]
sliceWithZero' Int
o Int
s [SWord 8]
m = Int -> [SWord 8] -> [SWord 8]
truncpad Int
s ([SWord 8] -> [SWord 8]) -> [SWord 8] -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
o [SWord 8]
m

writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
writeMemory' [SWord 8]
bs1 (C Whiff
_ W256
n) (C Whiff
_ W256
src) (C Whiff
_ W256
dst) [SWord 8]
bs0 =
  let
    ([SWord 8]
a, [SWord 8]
b) = Int -> [SWord 8] -> ([SWord 8], [SWord 8])
forall a. Int -> [a] -> ([a], [a])
splitAt (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
dst) [SWord 8]
bs0
    a' :: [SWord 8]
a'     = Int -> SWord 8 -> [SWord 8]
forall a. Int -> a -> [a]
replicate (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
dst Int -> Int -> Int
forall a. Num a => a -> a -> a
- [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
a) SWord 8
0
    c :: [SWord 8]
c      = if W256
src W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> W256
forall a b. (Integral a, Num b) => a -> b
num ([SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
bs1)
             then Int -> SWord 8 -> [SWord 8]
forall a. Int -> a -> [a]
replicate (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
n) SWord 8
0
             else Int -> Int -> [SWord 8] -> [SWord 8]
sliceWithZero' (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
src) (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
n) [SWord 8]
bs1
    b' :: [SWord 8]
b'     = Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num (W256
n)) [SWord 8]
b
  in
    [SWord 8]
a [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. Semigroup a => a -> a -> a
<> [SWord 8]
a' [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. Semigroup a => a -> a -> a
<> [SWord 8]
c [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. Semigroup a => a -> a -> a
<> [SWord 8]
b'

readMemoryWord' :: Word -> [SWord 8] -> SymWord
readMemoryWord' :: Word -> [SWord 8] -> SymWord
readMemoryWord' (C Whiff
_ W256
i) [SWord 8]
m =
  let bs :: [SWord 8]
bs = Int -> [SWord 8] -> [SWord 8]
truncpad Int
32 (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
i) [SWord 8]
m)
  in Whiff -> SWord 256 -> SymWord
S (Buffer -> Whiff
FromBytes ([SWord 8] -> Buffer
SymbolicBuffer [SWord 8]
bs)) ([SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes [SWord 8]
bs)

readMemoryWord32' :: Word -> [SWord 8] -> SWord 32
readMemoryWord32' :: Word -> [SWord 8] -> SWord 32
readMemoryWord32' (C Whiff
_ W256
i) [SWord 8]
m = [SWord 8] -> SWord 32
forall a. ByteConverter a => [SWord 8] -> a
fromBytes ([SWord 8] -> SWord 32) -> [SWord 8] -> SWord 32
forall a b. (a -> b) -> a -> b
$ Int -> [SWord 8] -> [SWord 8]
truncpad Int
4 (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
i) [SWord 8]
m)

setMemoryWord' :: Word -> SymWord -> [SWord 8] -> [SWord 8]
setMemoryWord' :: Word -> SymWord -> [SWord 8] -> [SWord 8]
setMemoryWord' (C Whiff
_ W256
i) (S Whiff
_ SWord 256
x) =
  [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
writeMemory' (SWord 256 -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes SWord 256
x) Word
32 Word
0 (W256 -> Word
forall a b. (Integral a, Num b) => a -> b
num W256
i)

setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8]
setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8]
setMemoryByte' (C Whiff
_ W256
i) SWord 8
x =
  [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
writeMemory' [SWord 8
x] Word
1 Word
0 (W256 -> Word
forall a b. (Integral a, Num b) => a -> b
num W256
i)

readSWord' :: Word -> [SWord 8] -> SymWord
readSWord' :: Word -> [SWord 8] -> SymWord
readSWord' (C Whiff
_ W256
i) [SWord 8]
x =
  if W256
i W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> W256
forall a b. (Integral a, Num b) => a -> b
num ([SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
x)
  then SymWord
0
  else Int -> [SWord 8] -> SymWord
swordAt (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num W256
i) [SWord 8]
x


select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a
select' :: [a] -> a -> SBV b -> a
select' [a]
xs a
err SBV b
ind = [a] -> SBV b -> a -> a
forall a t.
(Num a, Mergeable t, EqSymbolic a) =>
[t] -> a -> t -> t
walk [a]
xs SBV b
ind a
err
    where walk :: [t] -> a -> t -> t
walk []     a
_ t
acc = t
acc
          walk (t
e:[t]
es) a
i t
acc = [t] -> a -> t -> t
walk [t]
es (a
ia -> a -> a
forall a. Num a => a -> a -> a
-a
1) (SBool -> t -> t -> t
forall a. Mergeable a => SBool -> a -> a -> a
ite (a
i a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
0) t
e t
acc)

-- | Read 32 bytes from index from a bounded list of bytes.
readSWordWithBound :: SymWord -> Buffer -> SymWord -> SymWord
readSWordWithBound :: SymWord -> Buffer -> SymWord -> SymWord
readSWordWithBound sind :: SymWord
sind@(S Whiff
_ SWord 256
ind) (SymbolicBuffer [SWord 8]
xs) (S Whiff
_ SWord 256
bound) = case (Word -> Int
forall a b. (Integral a, Num b) => a -> b
num (Word -> Int) -> Maybe Word -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymWord -> Maybe Word
maybeLitWord SymWord
sind, W256 -> Int
forall a b. (Integral a, Num b) => a -> b
num (W256 -> Int) -> (WordN 256 -> W256) -> WordN 256 -> Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WordN 256 -> W256
forall a. FromSizzleBV a => a -> FromSizzle a
fromSizzle (WordN 256 -> Int) -> Maybe (WordN 256) -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord 256 -> Maybe (WordN 256)
forall a. SymVal a => SBV a -> Maybe a
unliteral SWord 256
bound) of
  (Just Int
i, Just Int
b) ->
    let bs :: [SWord 8]
bs = Int -> [SWord 8] -> [SWord 8]
truncpad Int
32 ([SWord 8] -> [SWord 8]) -> [SWord 8] -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
drop Int
i (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
b [SWord 8]
xs)
    in Whiff -> SWord 256 -> SymWord
S (Buffer -> Whiff
FromBytes ([SWord 8] -> Buffer
SymbolicBuffer [SWord 8]
bs)) ([SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes [SWord 8]
bs)
  (Maybe Int, Maybe Int)
_ ->
    -- Generates a ridiculously large set of constraints (roughly 25k) when
    -- the index is symbolic, but it still seems (kind of) manageable
    -- for the solvers.

    -- The proper solution here is to use smt arrays instead.

    let boundedList :: [SWord 8]
boundedList = [SBool -> SWord 8 -> SWord 8 -> SWord 8
forall a. Mergeable a => SBool -> a -> a -> a
ite (SWord 256
i SWord 256 -> SWord 256 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SWord 256
bound) SWord 8
x' SWord 8
0 | (SWord 8
x', SWord 256
i) <- [SWord 8] -> [SWord 256] -> [(SWord 8, SWord 256)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SWord 8]
xs [SWord 256
1..]]
        res :: [SWord 8]
res = [[SWord 8] -> SWord 8 -> SWord 256 -> SWord 8
forall b a.
(Ord b, Num b, SymVal b, Mergeable a) =>
[a] -> a -> SBV b -> a
select' [SWord 8]
boundedList SWord 8
0 (SWord 256
ind SWord 256 -> SWord 256 -> SWord 256
forall a. Num a => a -> a -> a
+ SWord 256
j) | SWord 256
j <- [SWord 256
0..SWord 256
31]]
    in Whiff -> SWord 256 -> SymWord
S (Buffer -> Whiff
FromBytes (Buffer -> Whiff) -> Buffer -> Whiff
forall a b. (a -> b) -> a -> b
$ [SWord 8] -> Buffer
SymbolicBuffer [SWord 8]
res) (SWord 256 -> SymWord) -> SWord 256 -> SymWord
forall a b. (a -> b) -> a -> b
$ [SWord 8] -> SWord 256
forall a. ByteConverter a => [SWord 8] -> a
fromBytes [SWord 8]
res

readSWordWithBound SymWord
sind (ConcreteBuffer ByteString
xs) SymWord
bound =
  case SymWord -> Maybe Word
maybeLitWord SymWord
sind of
    Maybe Word
Nothing -> SymWord -> Buffer -> SymWord -> SymWord
readSWordWithBound SymWord
sind ([SWord 8] -> Buffer
SymbolicBuffer (ByteString -> [SWord 8]
litBytes ByteString
xs)) SymWord
bound
    Just Word
x' ->
       -- INVARIANT: bound should always be length xs for concrete bytes
       -- so we should be able to safely ignore it here
         Word -> SymWord
litWord (Word -> SymWord) -> Word -> SymWord
forall a b. (a -> b) -> a -> b
$ Word -> ByteString -> Word
Concrete.readMemoryWord Word
x' ByteString
xs

-- a whole foldable instance seems overkill, but length is always good to have!
len :: Buffer -> Int
len :: Buffer -> Int
len (SymbolicBuffer [SWord 8]
bs) = [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
bs
len (ConcreteBuffer ByteString
bs) = ByteString -> Int
BS.length ByteString
bs

readByteOrZero :: Int -> Buffer -> SWord 8
readByteOrZero :: Int -> Buffer -> SWord 8
readByteOrZero Int
i (SymbolicBuffer [SWord 8]
bs) = Int -> [SWord 8] -> SWord 8
readByteOrZero' Int
i [SWord 8]
bs
readByteOrZero Int
i (ConcreteBuffer ByteString
bs) = Word8 -> SWord 8
forall a b. (Integral a, Num b) => a -> b
num (Word8 -> SWord 8) -> Word8 -> SWord 8
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> Word8
Concrete.readByteOrZero Int
i ByteString
bs

sliceWithZero :: Int -> Int -> Buffer -> Buffer
sliceWithZero :: Int -> Int -> Buffer -> Buffer
sliceWithZero Int
o Int
s (SymbolicBuffer [SWord 8]
m) = [SWord 8] -> Buffer
SymbolicBuffer (Int -> Int -> [SWord 8] -> [SWord 8]
sliceWithZero' Int
o Int
s [SWord 8]
m)
sliceWithZero Int
o Int
s (ConcreteBuffer ByteString
m) = ByteString -> Buffer
ConcreteBuffer (Int -> Int -> ByteString -> ByteString
Concrete.byteStringSliceWithDefaultZeroes Int
o Int
s ByteString
m)

writeMemory :: Buffer -> Word -> Word -> Word -> Buffer -> Buffer
writeMemory :: Buffer -> Word -> Word -> Word -> Buffer -> Buffer
writeMemory (ConcreteBuffer ByteString
bs1) Word
n Word
src Word
dst (ConcreteBuffer ByteString
bs0) =
  ByteString -> Buffer
ConcreteBuffer (ByteString -> Word -> Word -> Word -> ByteString -> ByteString
Concrete.writeMemory ByteString
bs1 Word
n Word
src Word
dst ByteString
bs0)
writeMemory (ConcreteBuffer ByteString
bs1) Word
n Word
src Word
dst (SymbolicBuffer [SWord 8]
bs0) =
  [SWord 8] -> Buffer
SymbolicBuffer ([SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
writeMemory' (ByteString -> [SWord 8]
litBytes ByteString
bs1) Word
n Word
src Word
dst [SWord 8]
bs0)
writeMemory (SymbolicBuffer [SWord 8]
bs1) Word
n Word
src Word
dst (ConcreteBuffer ByteString
bs0) =
  [SWord 8] -> Buffer
SymbolicBuffer ([SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
writeMemory' [SWord 8]
bs1 Word
n Word
src Word
dst (ByteString -> [SWord 8]
litBytes ByteString
bs0))
writeMemory (SymbolicBuffer [SWord 8]
bs1) Word
n Word
src Word
dst (SymbolicBuffer [SWord 8]
bs0) =
  [SWord 8] -> Buffer
SymbolicBuffer ([SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
writeMemory' [SWord 8]
bs1 Word
n Word
src Word
dst [SWord 8]
bs0)

readMemoryWord :: Word -> Buffer -> SymWord
readMemoryWord :: Word -> Buffer -> SymWord
readMemoryWord Word
i (SymbolicBuffer [SWord 8]
m) = Word -> [SWord 8] -> SymWord
readMemoryWord' Word
i [SWord 8]
m
readMemoryWord Word
i (ConcreteBuffer ByteString
m) = Word -> SymWord
litWord (Word -> SymWord) -> Word -> SymWord
forall a b. (a -> b) -> a -> b
$ Word -> ByteString -> Word
Concrete.readMemoryWord Word
i ByteString
m

readMemoryWord32 :: Word -> Buffer -> SWord 32
readMemoryWord32 :: Word -> Buffer -> SWord 32
readMemoryWord32 Word
i (SymbolicBuffer [SWord 8]
m) = Word -> [SWord 8] -> SWord 32
readMemoryWord32' Word
i [SWord 8]
m
readMemoryWord32 Word
i (ConcreteBuffer ByteString
m) = Word -> SWord 32
forall a b. (Integral a, Num b) => a -> b
num (Word -> SWord 32) -> Word -> SWord 32
forall a b. (a -> b) -> a -> b
$ Word -> ByteString -> Word
Concrete.readMemoryWord32 Word
i ByteString
m

setMemoryWord :: Word -> SymWord -> Buffer -> Buffer
setMemoryWord :: Word -> SymWord -> Buffer -> Buffer
setMemoryWord Word
i SymWord
x (SymbolicBuffer [SWord 8]
z) = [SWord 8] -> Buffer
SymbolicBuffer ([SWord 8] -> Buffer) -> [SWord 8] -> Buffer
forall a b. (a -> b) -> a -> b
$ Word -> SymWord -> [SWord 8] -> [SWord 8]
setMemoryWord' Word
i SymWord
x [SWord 8]
z
setMemoryWord Word
i SymWord
x (ConcreteBuffer ByteString
z) = case SymWord -> Maybe Word
maybeLitWord SymWord
x of
  Just Word
x' -> ByteString -> Buffer
ConcreteBuffer (ByteString -> Buffer) -> ByteString -> Buffer
forall a b. (a -> b) -> a -> b
$ Word -> Word -> ByteString -> ByteString
Concrete.setMemoryWord Word
i Word
x' ByteString
z
  Maybe Word
Nothing -> [SWord 8] -> Buffer
SymbolicBuffer ([SWord 8] -> Buffer) -> [SWord 8] -> Buffer
forall a b. (a -> b) -> a -> b
$ Word -> SymWord -> [SWord 8] -> [SWord 8]
setMemoryWord' Word
i SymWord
x (ByteString -> [SWord 8]
litBytes ByteString
z)

setMemoryByte :: Word -> SWord 8 -> Buffer -> Buffer
setMemoryByte :: Word -> SWord 8 -> Buffer -> Buffer
setMemoryByte Word
i SWord 8
x (SymbolicBuffer [SWord 8]
m) = [SWord 8] -> Buffer
SymbolicBuffer ([SWord 8] -> Buffer) -> [SWord 8] -> Buffer
forall a b. (a -> b) -> a -> b
$ Word -> SWord 8 -> [SWord 8] -> [SWord 8]
setMemoryByte' Word
i SWord 8
x [SWord 8]
m
setMemoryByte Word
i SWord 8
x (ConcreteBuffer ByteString
m) = case WordN 8 -> Word8
forall a. FromSizedBV a => a -> FromSized a
fromSized (WordN 8 -> Word8) -> Maybe (WordN 8) -> Maybe Word8
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord 8 -> Maybe (WordN 8)
forall a. SymVal a => SBV a -> Maybe a
unliteral SWord 8
x of
  Maybe Word8
Nothing -> [SWord 8] -> Buffer
SymbolicBuffer ([SWord 8] -> Buffer) -> [SWord 8] -> Buffer
forall a b. (a -> b) -> a -> b
$ Word -> SWord 8 -> [SWord 8] -> [SWord 8]
setMemoryByte' Word
i SWord 8
x (ByteString -> [SWord 8]
litBytes ByteString
m)
  Just Word8
x' -> ByteString -> Buffer
ConcreteBuffer (ByteString -> Buffer) -> ByteString -> Buffer
forall a b. (a -> b) -> a -> b
$ Word -> Word8 -> ByteString -> ByteString
Concrete.setMemoryByte Word
i Word8
x' ByteString
m

readSWord :: Word -> Buffer -> SymWord
readSWord :: Word -> Buffer -> SymWord
readSWord Word
i (SymbolicBuffer [SWord 8]
x) = Word -> [SWord 8] -> SymWord
readSWord' Word
i [SWord 8]
x
readSWord Word
i (ConcreteBuffer ByteString
x) = Word -> SymWord
forall a b. (Integral a, Num b) => a -> b
num (Word -> SymWord) -> Word -> SymWord
forall a b. (a -> b) -> a -> b
$ Word -> ByteString -> Word
Concrete.readMemoryWord Word
i ByteString
x

index :: Int -> Buffer -> SWord8
index :: Int -> Buffer -> SWord8
index Int
x (ConcreteBuffer ByteString
b) = Word8 -> SWord8
forall a. SymVal a => a -> SBV a
literal (Word8 -> SWord8) -> Word8 -> SWord8
forall a b. (a -> b) -> a -> b
$ ByteString -> Int -> Word8
BS.index ByteString
b Int
x
index Int
x (SymbolicBuffer [SWord 8]
b) = SWord 8 -> FromSized (SWord 8)
forall a. FromSizedBV a => a -> FromSized a
fromSized (SWord 8 -> FromSized (SWord 8)) -> SWord 8 -> FromSized (SWord 8)
forall a b. (a -> b) -> a -> b
$ [SWord 8]
b [SWord 8] -> Int -> SWord 8
forall a. [a] -> Int -> a
!! Int
x

-- * Uninterpreted functions

symSHA256N :: SInteger -> SInteger -> SWord 256
symSHA256N :: SInteger -> SInteger -> SWord 256
symSHA256N = [Char] -> SInteger -> SInteger -> SWord 256
forall a. Uninterpreted a => [Char] -> a
uninterpret [Char]
"sha256"

symkeccakN :: SInteger -> SInteger -> SWord 256
symkeccakN :: SInteger -> SInteger -> SWord 256
symkeccakN = [Char] -> SInteger -> SInteger -> SWord 256
forall a. Uninterpreted a => [Char] -> a
uninterpret [Char]
"keccak"

toSInt :: [SWord 8] -> SInteger
toSInt :: [SWord 8] -> SInteger
toSInt [SWord 8]
bs = [SInteger] -> SInteger
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger) -> [SInteger] -> SInteger
forall a b. (a -> b) -> a -> b
$ (SWord 8 -> Integer -> SInteger)
-> [SWord 8] -> [Integer] -> [SInteger]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\SWord 8
a (Integer
i :: Integer) -> SWord 8 -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SWord 8
a SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
256 SInteger -> Integer -> SInteger
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
i) [SWord 8]
bs [Integer
0..]


-- | Although we'd like to define this directly as an uninterpreted function,
-- we cannot because [a] is not a symbolic type. We must convert the list into a suitable
-- symbolic type first. The only important property of this conversion is that it is injective.
-- We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution.
symkeccak' :: [SWord 8] -> SWord 256
symkeccak' :: [SWord 8] -> SWord 256
symkeccak' [SWord 8]
bytes = case [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
bytes of
  Int
0 -> WordN 256 -> SWord 256
forall a. SymVal a => a -> SBV a
literal (WordN 256 -> SWord 256) -> WordN 256 -> SWord 256
forall a b. (a -> b) -> a -> b
$ W256 -> ToSizzle W256
forall a. ToSizzleBV a => a -> ToSizzle a
toSizzle (W256 -> ToSizzle W256) -> W256 -> ToSizzle W256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
keccak ByteString
""
  Int
n -> SInteger -> SInteger -> SWord 256
symkeccakN (Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
num Int
n) ([SWord 8] -> SInteger
toSInt [SWord 8]
bytes)

symSHA256 :: [SWord 8] -> [SWord 8]
symSHA256 :: [SWord 8] -> [SWord 8]
symSHA256 [SWord 8]
bytes = case [SWord 8] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
bytes of
  Int
0 -> ByteString -> [SWord 8]
litBytes (ByteString -> [SWord 8]) -> ByteString -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> [Word8] -> ByteString
forall a b. (a -> b) -> a -> b
$ Digest SHA256 -> [Word8]
forall a. ByteArrayAccess a => a -> [Word8]
BA.unpack (Digest SHA256 -> [Word8]) -> Digest SHA256 -> [Word8]
forall a b. (a -> b) -> a -> b
$ (ByteString -> Digest SHA256
forall ba a.
(ByteArrayAccess ba, HashAlgorithm a) =>
ba -> Digest a
Crypto.hash ByteString
BS.empty :: Digest SHA256)
  Int
n -> SWord 256 -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes (SWord 256 -> [SWord 8]) -> SWord 256 -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ SInteger -> SInteger -> SWord 256
symSHA256N (Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
num Int
n) ([SWord 8] -> SInteger
toSInt [SWord 8]
bytes)

rawVal :: SymWord -> SWord 256
rawVal :: SymWord -> SWord 256
rawVal (S Whiff
_ SWord 256
v) = SWord 256
v

-- | Reconstruct the smt/sbv value from a whiff
-- Should satisfy (rawVal x .== whiffValue x)
whiffValue :: Whiff -> SWord 256
whiffValue :: Whiff -> SWord 256
whiffValue Whiff
w = case Whiff
w of
  w' :: Whiff
w'@(Todo [Char]
_ [Whiff]
_) -> [Char] -> SWord 256
forall a. HasCallStack => [Char] -> a
error ([Char] -> SWord 256) -> [Char] -> SWord 256
forall a b. (a -> b) -> a -> b
$ [Char]
"unable to get value of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Whiff -> [Char]
forall a. Show a => a -> [Char]
show Whiff
w'
  And Whiff
x Whiff
y       -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall a. Bits a => a -> a -> a
.&. Whiff -> SWord 256
whiffValue Whiff
y
  Or Whiff
x Whiff
y        -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall a. Bits a => a -> a -> a
.|. Whiff -> SWord 256
whiffValue Whiff
y
  Eq Whiff
x Whiff
y        -> SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Whiff -> SWord 256
whiffValue Whiff
y) SWord 256
1 SWord 256
0
  LT Whiff
x Whiff
y        -> SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Whiff -> SWord 256
whiffValue Whiff
y) SWord 256
1 SWord 256
0
  GT Whiff
x Whiff
y        -> SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> Whiff -> SWord 256
whiffValue Whiff
y) SWord 256
1 SWord 256
0
  ITE Whiff
b Whiff
x Whiff
y     -> SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (Whiff -> SWord 256
whiffValue Whiff
b SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
1) (Whiff -> SWord 256
whiffValue Whiff
x) (Whiff -> SWord 256
whiffValue Whiff
y)
  SLT Whiff
x Whiff
y       -> SymWord -> SWord 256
rawVal (SymWord -> SWord 256) -> SymWord -> SWord 256
forall a b. (a -> b) -> a -> b
$ SymWord -> SymWord -> SymWord
slt (Whiff -> SWord 256 -> SymWord
S Whiff
x (Whiff -> SWord 256
whiffValue Whiff
x)) (Whiff -> SWord 256 -> SymWord
S Whiff
y (Whiff -> SWord 256
whiffValue Whiff
y))
  SGT Whiff
x Whiff
y       -> SymWord -> SWord 256
rawVal (SymWord -> SWord 256) -> SymWord -> SWord 256
forall a b. (a -> b) -> a -> b
$ SymWord -> SymWord -> SymWord
sgt (Whiff -> SWord 256 -> SymWord
S Whiff
x (Whiff -> SWord 256
whiffValue Whiff
x)) (Whiff -> SWord 256 -> SymWord
S Whiff
y (Whiff -> SWord 256
whiffValue Whiff
y))
  IsZero Whiff
x      -> SBool -> SWord 256 -> SWord 256 -> SWord 256
forall a. Mergeable a => SBool -> a -> a -> a
ite (Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
0) SWord 256
1 SWord 256
0
  SHL Whiff
x Whiff
y       -> SWord 256 -> SWord 256 -> SWord 256
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sShiftLeft  (Whiff -> SWord 256
whiffValue Whiff
x) (Whiff -> SWord 256
whiffValue Whiff
y)
  SHR Whiff
x Whiff
y       -> SWord 256 -> SWord 256 -> SWord 256
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sShiftRight (Whiff -> SWord 256
whiffValue Whiff
x) (Whiff -> SWord 256
whiffValue Whiff
y)
  SAR Whiff
x Whiff
y       -> SWord 256 -> SWord 256 -> SWord 256
forall a b. (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a
sSignedShiftArithRight (Whiff -> SWord 256
whiffValue Whiff
x) (Whiff -> SWord 256
whiffValue Whiff
y)
  Add Whiff
x Whiff
y       -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall a. Num a => a -> a -> a
+ Whiff -> SWord 256
whiffValue Whiff
y
  Sub Whiff
x Whiff
y       -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall a. Num a => a -> a -> a
- Whiff -> SWord 256
whiffValue Whiff
y
  Mul Whiff
x Whiff
y       -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall a. Num a => a -> a -> a
* Whiff -> SWord 256
whiffValue Whiff
y
  Div Whiff
x Whiff
y       -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall a. SDivisible a => a -> a -> a
`sDiv` Whiff -> SWord 256
whiffValue Whiff
y
  Mod Whiff
x Whiff
y       -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall a. SDivisible a => a -> a -> a
`sMod` Whiff -> SWord 256
whiffValue Whiff
y
  Exp Whiff
x Whiff
y       -> Whiff -> SWord 256
whiffValue Whiff
x SWord 256 -> SWord 256 -> SWord 256
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^ Whiff -> SWord 256
whiffValue Whiff
y
  Neg Whiff
x         -> SWord 256 -> SWord 256
forall a. Bits a => a -> a
complement (SWord 256 -> SWord 256) -> SWord 256 -> SWord 256
forall a b. (a -> b) -> a -> b
$ Whiff -> SWord 256
whiffValue Whiff
x
  Var [Char]
_ SWord 256
v       -> SWord 256
v
  FromKeccak (ConcreteBuffer ByteString
bstr) -> WordN 256 -> SWord 256
forall a. SymVal a => a -> SBV a
literal (WordN 256 -> SWord 256) -> WordN 256 -> SWord 256
forall a b. (a -> b) -> a -> b
$ W256 -> WordN 256
forall a b. (Integral a, Num b) => a -> b
num (W256 -> WordN 256) -> W256 -> WordN 256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
keccak ByteString
bstr
  FromKeccak (SymbolicBuffer [SWord 8]
buf)  -> [SWord 8] -> SWord 256
symkeccak' [SWord 8]
buf
  Literal W256
x -> WordN 256 -> SWord 256
forall a. SymVal a => a -> SBV a
literal (WordN 256 -> SWord 256) -> WordN 256 -> SWord 256
forall a b. (a -> b) -> a -> b
$ W256 -> WordN 256
forall a b. (Integral a, Num b) => a -> b
num (W256 -> WordN 256) -> W256 -> WordN 256
forall a b. (a -> b) -> a -> b
$ W256
x
  FromBytes Buffer
buf -> SymWord -> SWord 256
rawVal (SymWord -> SWord 256) -> SymWord -> SWord 256
forall a b. (a -> b) -> a -> b
$ Word -> Buffer -> SymWord
readMemoryWord Word
0 Buffer
buf
  FromStorage Whiff
ind SArray (WordN 256) (WordN 256)
arr -> SArray (WordN 256) (WordN 256) -> SWord 256 -> SWord 256
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray (WordN 256) (WordN 256)
arr (Whiff -> SWord 256
whiffValue Whiff
ind)

-- | Special cases that have proven useful in practice
simplifyCondition :: SBool -> Whiff -> SBool
simplifyCondition :: SBool -> Whiff -> SBool
simplifyCondition SBool
_ (IsZero (IsZero (IsZero Whiff
a))) = Whiff -> SWord 256
whiffValue Whiff
a SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
0



-- | Overflow safe math can be difficult for smt solvers to deal with,
-- especially for 256-bit words. When we recognize terms arising from
-- overflow checks, we translate our queries into a more bespoke form,
-- outlined in:
-- Modular Bug-finding for Integer Overflows in the Large:
-- Sound, Efficient, Bit-precise Static Analysis
-- www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf
--
-- Addition overflow.
-- Written as
--    require (x <= (x + y))
-- or require (y <= (x + y))
-- or require (!(y < (x + y)))
simplifyCondition SBool
b (IsZero (IsZero (LT (Add Whiff
x Whiff
y) Whiff
z))) =
  let x' :: SWord 256
x' = Whiff -> SWord 256
whiffValue Whiff
x
      y' :: SWord 256
y' = Whiff -> SWord 256
whiffValue Whiff
y
      z' :: SWord 256
z' = Whiff -> SWord 256
whiffValue Whiff
z
      (SBool
_, SBool
overflow) = SWord 256 -> SWord 256 -> (SBool, SBool)
forall a. ArithOverflow a => a -> a -> (SBool, SBool)
bvAddO SWord 256
x' SWord 256
y'
  in
    SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SWord 256
x' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
z' SBool -> SBool -> SBool
.||
         SWord 256
y' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
z')
    SBool
overflow
    SBool
b

-- Multiplication overflow.
-- Written as
--    require (y == 0 || x * y / y == x)
-- or require (y == 0 || x == x * y / y)

-- proveWith cvc4 $ \x y z -> ite (y .== (z :: SWord 8)) (((x * y) `sDiv` z ./= x) .<=> (snd (bvMulO x y) .|| (z .== 0 .&& x .> 0))) (sTrue)
-- Q.E.D.
simplifyCondition SBool
b (IsZero (Eq Whiff
x (Div (Mul Whiff
y Whiff
z) Whiff
w))) =
  SBool -> Whiff -> SBool
simplifyCondition SBool
b (Whiff -> Whiff
IsZero (Whiff -> Whiff -> Whiff
Eq (Whiff -> Whiff -> Whiff
Div (Whiff -> Whiff -> Whiff
Mul Whiff
y Whiff
z) Whiff
w) Whiff
x))
simplifyCondition SBool
b (IsZero (Eq (Div (Mul Whiff
y Whiff
z) Whiff
w) Whiff
x)) =
  let x' :: SWord 256
x' = Whiff -> SWord 256
whiffValue Whiff
x
      y' :: SWord 256
y' = Whiff -> SWord 256
whiffValue Whiff
y
      z' :: SWord 256
z' = Whiff -> SWord 256
whiffValue Whiff
z
      w' :: SWord 256
w' = Whiff -> SWord 256
whiffValue Whiff
w
      (SBool
_, SBool
overflow) = SWord 256 -> SWord 256 -> (SBool, SBool)
forall a. ArithOverflow a => a -> a -> (SBool, SBool)
bvMulO SWord 256
y' SWord 256
z'
  in
    SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite
    ((SWord 256
y' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
x' SBool -> SBool -> SBool
.&& SWord 256
z' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
w') SBool -> SBool -> SBool
.||
      (SWord 256
z' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
x' SBool -> SBool -> SBool
.&& SWord 256
y' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
w'))
    (SBool
overflow SBool -> SBool -> SBool
.|| (SWord 256
w' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 256
0 SBool -> SBool -> SBool
.&& SWord 256
x' SWord 256 -> SWord 256 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SWord 256
0))
    SBool
b
simplifyCondition SBool
b Whiff
_ = SBool
b