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

module EVM.SymExec where


import Prelude hiding (Word)

import Control.Lens hiding (pre)
import EVM hiding (Query, push)
import qualified EVM
import EVM.Exec
import qualified EVM.Fetch as Fetch
import EVM.ABI
import EVM.Stepper (Stepper)
import qualified EVM.Stepper as Stepper
import qualified Control.Monad.Operational as Operational
import Control.Monad.State.Strict hiding (state)
import Data.Maybe (catMaybes, fromMaybe)
import EVM.Types
import EVM.Concrete (createAddress)
import qualified EVM.FeeSchedule as FeeSchedule
import Data.SBV.Trans.Control
import Data.SBV.Trans hiding (distinct, Word)
import Data.SBV hiding (runSMT, newArray_, addAxiom, distinct, sWord8s, Word)
import Data.Vector (toList, fromList)
import Data.Tree

import Data.ByteString (ByteString, pack)
import qualified Data.ByteString.Lazy as Lazy
import qualified Data.ByteString as BS
import Data.Text (Text, splitOn, unpack)
import Control.Monad.State.Strict (runState, get, put, zipWithM)
import qualified Control.Monad.State.Class as State
import Control.Applicative

-- | Convenience functions for generating large symbolic byte strings
sbytes32, sbytes128, sbytes256, sbytes512, sbytes1024 :: Query ([SWord 8])
sbytes32 :: Query [SWord 8]
sbytes32 = SBV (WordN 256) -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes (SBV (WordN 256) -> [SWord 8])
-> QueryT IO (SBV (WordN 256)) -> Query [SWord 8]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
forall (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal (WordN 256)) =>
m (SBV (WordN 256))
freshVar_ @ (WordN 256)
sbytes128 :: Query [SWord 8]
sbytes128 = SBV (WordN 1024) -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes (SBV (WordN 1024) -> [SWord 8])
-> QueryT IO (SBV (WordN 1024)) -> Query [SWord 8]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
forall (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal (WordN 1024)) =>
m (SBV (WordN 1024))
freshVar_ @ (WordN 1024)
sbytes256 :: Query [SWord 8]
sbytes256 = ([SWord 8] -> [SWord 8] -> [SWord 8])
-> Query [SWord 8] -> Query [SWord 8] -> Query [SWord 8]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. [a] -> [a] -> [a]
(++) Query [SWord 8]
sbytes128 Query [SWord 8]
sbytes128
sbytes512 :: Query [SWord 8]
sbytes512 = ([SWord 8] -> [SWord 8] -> [SWord 8])
-> Query [SWord 8] -> Query [SWord 8] -> Query [SWord 8]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. [a] -> [a] -> [a]
(++) Query [SWord 8]
sbytes256 Query [SWord 8]
sbytes256
sbytes1024 :: Query [SWord 8]
sbytes1024 = ([SWord 8] -> [SWord 8] -> [SWord 8])
-> Query [SWord 8] -> Query [SWord 8] -> Query [SWord 8]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. [a] -> [a] -> [a]
(++) Query [SWord 8]
sbytes512 Query [SWord 8]
sbytes512

mkByte :: Query [SWord 8]
mkByte :: Query [SWord 8]
mkByte = do SWord 8
x <- QueryT IO (SWord 8)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
            [SWord 8] -> Query [SWord 8]
forall (m :: * -> *) a. Monad m => a -> m a
return [SWord 8
x]

-- | Abstract calldata argument generation
symAbiArg :: AbiType -> Query ([SWord 8], W256)
symAbiArg :: AbiType -> Query ([SWord 8], W256)
symAbiArg (AbiUIntType n :: Int
n) | Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` 8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 256 =
  do [SWord 8]
x <- (Int -> Query [SWord 8]) -> [Int] -> Query [SWord 8]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (Query [SWord 8] -> Int -> Query [SWord 8]
forall a b. a -> b -> a
const Query [SWord 8]
mkByte) [0..(Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 8) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
     ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [SWord 8] -> [SWord 8]
forall a. Num a => Int -> [a] -> [a]
padLeft' 32 [SWord 8]
x, 32)
                          | Bool
otherwise = [Char] -> Query ([SWord 8], W256)
forall a. HasCallStack => [Char] -> a
error "bad type"

symAbiArg (AbiIntType n :: Int
n)  | Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` 8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 256 =
  do [SWord 8]
x <- (Int -> Query [SWord 8]) -> [Int] -> Query [SWord 8]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (Query [SWord 8] -> Int -> Query [SWord 8]
forall a b. a -> b -> a
const Query [SWord 8]
mkByte) [(0 :: Int) ..(Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 8) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
     ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [SWord 8] -> [SWord 8]
forall a. Num a => Int -> [a] -> [a]
padLeft' 32 [SWord 8]
x, 32)

                          | Bool
otherwise = [Char] -> Query ([SWord 8], W256)
forall a. HasCallStack => [Char] -> a
error "bad type"
symAbiArg AbiBoolType =
  do [SWord 8]
x <- Query [SWord 8]
mkByte
     ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [SWord 8] -> [SWord 8]
forall a. Num a => Int -> [a] -> [a]
padLeft' 32 [SWord 8]
x, 32)

symAbiArg AbiAddressType =
  do [SWord 8]
x <- (Int -> Query [SWord 8]) -> [Int] -> Query [SWord 8]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (Query [SWord 8] -> Int -> Query [SWord 8]
forall a b. a -> b -> a
const Query [SWord 8]
mkByte) [(0 :: Int)..19]
     ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [SWord 8] -> [SWord 8]
forall a. Num a => Int -> [a] -> [a]
padLeft' 32 [SWord 8]
x, 32)

symAbiArg (AbiBytesType n :: Int
n) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 32 =
  do [SWord 8]
x <- (Int -> Query [SWord 8]) -> [Int] -> Query [SWord 8]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (Query [SWord 8] -> Int -> Query [SWord 8]
forall a b. a -> b -> a
const Query [SWord 8]
mkByte) [0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
     ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [SWord 8] -> [SWord 8]
forall a. Num a => Int -> [a] -> [a]
padLeft' 32 [SWord 8]
x, 32)

                           | Bool
otherwise = [Char] -> Query ([SWord 8], W256)
forall a. HasCallStack => [Char] -> a
error "bad type"

-- TODO: is this encoding correct?
symAbiArg (AbiArrayType len :: Int
len typ :: AbiType
typ) =
  do [([SWord 8], W256)]
args <- (AbiType -> Query ([SWord 8], W256))
-> [AbiType] -> QueryT IO [([SWord 8], W256)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AbiType -> Query ([SWord 8], W256)
symAbiArg (Int -> AbiType -> [AbiType]
forall a. Int -> a -> [a]
replicate Int
len AbiType
typ)
     ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> [SWord 8]
litBytes (AbiValue -> ByteString
encodeAbiValue (Int -> Word256 -> AbiValue
AbiUInt 256 (Int -> Word256
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
len))) [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. Semigroup a => a -> a -> a
<> ([[SWord 8]] -> [SWord 8]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SWord 8]] -> [SWord 8]) -> [[SWord 8]] -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ ([SWord 8], W256) -> [SWord 8]
forall a b. (a, b) -> a
fst (([SWord 8], W256) -> [SWord 8])
-> [([SWord 8], W256)] -> [[SWord 8]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([SWord 8], W256)]
args),
             32 W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ ([W256] -> W256
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([W256] -> W256) -> [W256] -> W256
forall a b. (a -> b) -> a -> b
$ ([SWord 8], W256) -> W256
forall a b. (a, b) -> b
snd (([SWord 8], W256) -> W256) -> [([SWord 8], W256)] -> [W256]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([SWord 8], W256)]
args))

symAbiArg (AbiTupleType tuple :: Vector AbiType
tuple) =
  do [([SWord 8], W256)]
args <- (AbiType -> Query ([SWord 8], W256))
-> [AbiType] -> QueryT IO [([SWord 8], W256)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AbiType -> Query ([SWord 8], W256)
symAbiArg (Vector AbiType -> [AbiType]
forall a. Vector a -> [a]
toList Vector AbiType
tuple)
     ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return ([[SWord 8]] -> [SWord 8]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SWord 8]] -> [SWord 8]) -> [[SWord 8]] -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ ([SWord 8], W256) -> [SWord 8]
forall a b. (a, b) -> a
fst (([SWord 8], W256) -> [SWord 8])
-> [([SWord 8], W256)] -> [[SWord 8]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([SWord 8], W256)]
args, [W256] -> W256
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([W256] -> W256) -> [W256] -> W256
forall a b. (a -> b) -> a -> b
$ ([SWord 8], W256) -> W256
forall a b. (a, b) -> b
snd (([SWord 8], W256) -> W256) -> [([SWord 8], W256)] -> [W256]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([SWord 8], W256)]
args)
symAbiArg n :: AbiType
n =
  [Char] -> Query ([SWord 8], W256)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Query ([SWord 8], W256))
-> [Char] -> Query ([SWord 8], W256)
forall a b. (a -> b) -> a -> b
$ "Unsupported symbolic abiencoding for"
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> AbiType -> [Char]
forall a. Show a => a -> [Char]
show AbiType
n
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> ". Please file an issue at https://github.com/dapphub/dapptools if you really need this."

-- | Generates calldata matching given type signature, optionally specialized
-- with concrete arguments.
-- Any argument given as "<symbolic>" or omitted at the tail of the list are
-- kept symbolic.
symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], W256)
symCalldata :: Text -> [AbiType] -> [[Char]] -> Query ([SWord 8], W256)
symCalldata sig :: Text
sig typesignature :: [AbiType]
typesignature concreteArgs :: [[Char]]
concreteArgs =
  let args :: [[Char]]
args = [[Char]]
concreteArgs [[Char]] -> [[Char]] -> [[Char]]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char] -> [[Char]]
forall a. Int -> a -> [a]
replicate ([AbiType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbiType]
typesignature Int -> Int -> Int
forall a. Num a => a -> a -> a
- [[Char]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
concreteArgs)  "<symbolic>"
      mkArg :: AbiType -> [Char] -> Query ([SWord 8], W256)
mkArg typ :: AbiType
typ "<symbolic>" = AbiType -> Query ([SWord 8], W256)
symAbiArg AbiType
typ
      mkArg typ :: AbiType
typ arg :: [Char]
arg = let n :: [SWord 8]
n = ByteString -> [SWord 8]
litBytes (ByteString -> [SWord 8])
-> (AbiValue -> ByteString) -> AbiValue -> [SWord 8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbiValue -> ByteString
encodeAbiValue (AbiValue -> [SWord 8]) -> AbiValue -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ AbiType -> [Char] -> AbiValue
makeAbiValue AbiType
typ [Char]
arg
                      in ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SWord 8]
n, 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]
n))
      sig' :: [SWord 8]
sig' = ByteString -> [SWord 8]
litBytes (ByteString -> [SWord 8]) -> ByteString -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
selector Text
sig
  in do [([SWord 8], W256)]
calldatas <- (AbiType -> [Char] -> Query ([SWord 8], W256))
-> [AbiType] -> [[Char]] -> QueryT IO [([SWord 8], W256)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM AbiType -> [Char] -> Query ([SWord 8], W256)
mkArg [AbiType]
typesignature [[Char]]
args
        ([SWord 8], W256) -> Query ([SWord 8], W256)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SWord 8]
sig' [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. Semigroup a => a -> a -> a
<> [[SWord 8]] -> [SWord 8]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (([SWord 8], W256) -> [SWord 8]
forall a b. (a, b) -> a
fst (([SWord 8], W256) -> [SWord 8])
-> [([SWord 8], W256)] -> [[SWord 8]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([SWord 8], W256)]
calldatas), 4 W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ ([W256] -> W256
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([W256] -> W256) -> [W256] -> W256
forall a b. (a -> b) -> a -> b
$ ([SWord 8], W256) -> W256
forall a b. (a, b) -> b
snd (([SWord 8], W256) -> W256) -> [([SWord 8], W256)] -> [W256]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([SWord 8], W256)]
calldatas))

abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM
abstractVM :: Maybe (Text, [AbiType])
-> [[Char]] -> ByteString -> StorageModel -> Query VM
abstractVM typesignature :: Maybe (Text, [AbiType])
typesignature concreteArgs :: [[Char]]
concreteArgs x :: ByteString
x storagemodel :: StorageModel
storagemodel = do
  (cd' :: [SWord 8]
cd', cdlen :: SymWord
cdlen, cdconstraint :: (SBool, Whiff)
cdconstraint) <-
    case Maybe (Text, [AbiType])
typesignature of
      Nothing -> do [SWord 8]
cd <- Query [SWord 8]
sbytes256
                    SBV (WordN 256)
len <- QueryT IO (SBV (WordN 256))
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
                    ([SWord 8], SymWord, (SBool, Whiff))
-> QueryT IO ([SWord 8], SymWord, (SBool, Whiff))
forall (m :: * -> *) a. Monad m => a -> m a
return ([SWord 8]
cd, [Char] -> SBV (WordN 256) -> SymWord
var "calldataLength" SBV (WordN 256)
len, (SBV (WordN 256)
len SBV (WordN 256) -> SBV (WordN 256) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 256, [Char] -> [Whiff] -> Whiff
Todo "calldatalength < 256" []))
      Just (name :: Text
name, typs :: [AbiType]
typs) -> do (cd :: [SWord 8]
cd, cdlen :: W256
cdlen) <- Text -> [AbiType] -> [[Char]] -> Query ([SWord 8], W256)
symCalldata Text
name [AbiType]
typs [[Char]]
concreteArgs
                              ([SWord 8], SymWord, (SBool, Whiff))
-> QueryT IO ([SWord 8], SymWord, (SBool, Whiff))
forall (m :: * -> *) a. Monad m => a -> m a
return ([SWord 8]
cd, Whiff -> SBV (WordN 256) -> SymWord
S (W256 -> Whiff
Literal W256
cdlen) (WordN 256 -> SBV (WordN 256)
forall a. SymVal a => a -> SBV a
literal (WordN 256 -> SBV (WordN 256)) -> WordN 256 -> SBV (WordN 256)
forall a b. (a -> b) -> a -> b
$ W256 -> WordN 256
forall a b. (Integral a, Num b) => a -> b
num W256
cdlen), (SBool
sTrue, [Char] -> [Whiff] -> Whiff
Todo "Trivial" []))
  Storage
symstore <- case StorageModel
storagemodel of
    SymbolicS -> [(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
Symbolic [] (SArray (WordN 256) (WordN 256) -> Storage)
-> QueryT IO (SArray (WordN 256) (WordN 256)) -> QueryT IO Storage
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SBV (WordN 256))
-> QueryT IO (SArray (WordN 256) (WordN 256))
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
freshArray_ Maybe (SBV (WordN 256))
forall a. Maybe a
Nothing
    InitialS -> [(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
Symbolic [] (SArray (WordN 256) (WordN 256) -> Storage)
-> QueryT IO (SArray (WordN 256) (WordN 256)) -> QueryT IO Storage
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SBV (WordN 256))
-> QueryT IO (SArray (WordN 256) (WordN 256))
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
freshArray_ (SBV (WordN 256) -> Maybe (SBV (WordN 256))
forall a. a -> Maybe a
Just 0)
    ConcreteS -> Storage -> QueryT IO Storage
forall (m :: * -> *) a. Monad m => a -> m a
return (Storage -> QueryT IO Storage) -> Storage -> QueryT IO Storage
forall a b. (a -> b) -> a -> b
$ Map Word SymWord -> Storage
Concrete Map Word SymWord
forall a. Monoid a => a
mempty
  SAddr
c <- SWord 160 -> SAddr
SAddr (SWord 160 -> SAddr) -> QueryT IO (SWord 160) -> QueryT IO SAddr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO (SWord 160)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
  SymWord
value' <- [Char] -> SBV (WordN 256) -> SymWord
var "CALLVALUE" (SBV (WordN 256) -> SymWord)
-> QueryT IO (SBV (WordN 256)) -> QueryT IO SymWord
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO (SBV (WordN 256))
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
  VM -> Query VM
forall (m :: * -> *) a. Monad m => a -> m a
return (VM -> Query VM) -> VM -> Query VM
forall a b. (a -> b) -> a -> b
$ ContractCode
-> Storage
-> StorageModel
-> SAddr
-> SymWord
-> (Buffer, SymWord)
-> VM
loadSymVM (Buffer -> ContractCode
RuntimeCode (ByteString -> Buffer
ConcreteBuffer ByteString
x)) Storage
symstore StorageModel
storagemodel SAddr
c SymWord
value' ([SWord 8] -> Buffer
SymbolicBuffer [SWord 8]
cd', SymWord
cdlen) VM -> (VM -> VM) -> VM
forall a b. a -> (a -> b) -> b
& ASetter VM VM [(SBool, Whiff)] [(SBool, Whiff)]
-> ([(SBool, Whiff)] -> [(SBool, Whiff)]) -> VM -> VM
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter VM VM [(SBool, Whiff)] [(SBool, Whiff)]
Lens' VM [(SBool, Whiff)]
constraints ([(SBool, Whiff)] -> [(SBool, Whiff)] -> [(SBool, Whiff)]
forall a. Semigroup a => a -> a -> a
(<>) [(SBool, Whiff)
cdconstraint])

loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SymWord) -> VM
loadSymVM :: ContractCode
-> Storage
-> StorageModel
-> SAddr
-> SymWord
-> (Buffer, SymWord)
-> VM
loadSymVM x :: ContractCode
x initStore :: Storage
initStore model :: StorageModel
model addr :: SAddr
addr callvalue' :: SymWord
callvalue' calldata' :: (Buffer, SymWord)
calldata' =
  (VMOpts -> VM
makeVm (VMOpts -> VM) -> VMOpts -> VM
forall a b. (a -> b) -> a -> b
$ $WVMOpts :: Contract
-> (Buffer, SymWord)
-> SymWord
-> Addr
-> SAddr
-> Addr
-> W256
-> W256
-> W256
-> SymWord
-> Addr
-> W256
-> W256
-> W256
-> W256
-> FeeSchedule Integer
-> W256
-> Bool
-> StorageModel
-> Map Addr [W256]
-> VMOpts
VMOpts
    { vmoptContract :: Contract
vmoptContract = ContractCode -> Storage -> Contract
contractWithStore ContractCode
x Storage
initStore
    , vmoptCalldata :: (Buffer, SymWord)
vmoptCalldata = (Buffer, SymWord)
calldata'
    , vmoptValue :: SymWord
vmoptValue = SymWord
callvalue'
    , vmoptAddress :: Addr
vmoptAddress = Addr -> W256 -> Addr
createAddress Addr
ethrunAddress 1
    , vmoptCaller :: SAddr
vmoptCaller = SAddr
addr
    , vmoptOrigin :: Addr
vmoptOrigin = Addr
ethrunAddress --todo: generalize
    , vmoptCoinbase :: Addr
vmoptCoinbase = 0
    , vmoptNumber :: W256
vmoptNumber = 0
    , vmoptTimestamp :: SymWord
vmoptTimestamp = 0
    , vmoptBlockGaslimit :: W256
vmoptBlockGaslimit = 0
    , vmoptGasprice :: W256
vmoptGasprice = 0
    , vmoptDifficulty :: W256
vmoptDifficulty = 0
    , vmoptGas :: W256
vmoptGas = 0xffffffffffffffff
    , vmoptGaslimit :: W256
vmoptGaslimit = 0xffffffffffffffff
    , vmoptMaxCodeSize :: W256
vmoptMaxCodeSize = 0xffffffff
    , vmoptSchedule :: FeeSchedule Integer
vmoptSchedule = FeeSchedule Integer
forall n. Num n => FeeSchedule n
FeeSchedule.berlin
    , vmoptChainId :: W256
vmoptChainId = 1
    , vmoptCreate :: Bool
vmoptCreate = Bool
False
    , vmoptStorageModel :: StorageModel
vmoptStorageModel = StorageModel
model
    , vmoptTxAccessList :: Map Addr [W256]
vmoptTxAccessList = Map Addr [W256]
forall a. Monoid a => a
mempty
    }) VM -> (VM -> VM) -> VM
forall a b. a -> (a -> b) -> b
& ASetter VM VM (Maybe Contract) (Maybe Contract)
-> Maybe Contract -> VM -> VM
forall s t a b. ASetter s t a b -> b -> s -> t
set ((Env -> Identity Env) -> VM -> Identity VM
Lens' VM Env
env ((Env -> Identity Env) -> VM -> Identity VM)
-> ((Maybe Contract -> Identity (Maybe Contract))
    -> Env -> Identity Env)
-> ASetter VM VM (Maybe Contract) (Maybe Contract)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Addr Contract -> Identity (Map Addr Contract))
-> Env -> Identity Env
Lens' Env (Map Addr Contract)
contracts ((Map Addr Contract -> Identity (Map Addr Contract))
 -> Env -> Identity Env)
-> ((Maybe Contract -> Identity (Maybe Contract))
    -> Map Addr Contract -> Identity (Map Addr Contract))
-> (Maybe Contract -> Identity (Maybe Contract))
-> Env
-> Identity Env
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map Addr Contract)
-> Lens' (Map Addr Contract) (Maybe (IxValue (Map Addr Contract)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (Addr -> W256 -> Addr
createAddress Addr
ethrunAddress 1))
             (Contract -> Maybe Contract
forall a. a -> Maybe a
Just (ContractCode -> Storage -> Contract
contractWithStore ContractCode
x Storage
initStore))

data BranchInfo = BranchInfo
  { BranchInfo -> VM
_vm                 :: VM,
    BranchInfo -> Maybe Whiff
_branchCondition    :: Maybe Whiff
  }

doInterpret :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)
doInterpret :: Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)
doInterpret fetcher :: Fetcher
fetcher maxIter :: Maybe Integer
maxIter vm :: VM
vm = let
      f :: (VM, [Tree BranchInfo]) -> Tree BranchInfo
f (vm' :: VM
vm', cs :: [Tree BranchInfo]
cs) = BranchInfo -> [Tree BranchInfo] -> Tree BranchInfo
forall a. a -> Forest a -> Tree a
Node (VM -> Maybe Whiff -> BranchInfo
BranchInfo (if [Tree BranchInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tree BranchInfo]
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then VM
vm' else VM
vm) Maybe Whiff
forall a. Maybe a
Nothing) [Tree BranchInfo]
cs
    in (VM, [Tree BranchInfo]) -> Tree BranchInfo
f ((VM, [Tree BranchInfo]) -> Tree BranchInfo)
-> QueryT IO (VM, [Tree BranchInfo]) -> Query (Tree BranchInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fetcher -> Maybe Integer -> VM -> QueryT IO (VM, [Tree BranchInfo])
interpret' Fetcher
fetcher Maybe Integer
maxIter VM
vm

interpret' :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (VM, [(Tree BranchInfo)])
interpret' :: Fetcher -> Maybe Integer -> VM -> QueryT IO (VM, [Tree BranchInfo])
interpret' fetcher :: Fetcher
fetcher maxIter :: Maybe Integer
maxIter vm :: VM
vm = let
  cont :: State VM () -> QueryT IO (VM, [Tree BranchInfo])
cont s :: State VM ()
s = Fetcher -> Maybe Integer -> VM -> QueryT IO (VM, [Tree BranchInfo])
interpret' Fetcher
fetcher Maybe Integer
maxIter (VM -> QueryT IO (VM, [Tree BranchInfo]))
-> VM -> QueryT IO (VM, [Tree BranchInfo])
forall a b. (a -> b) -> a -> b
$ State VM () -> VM -> VM
forall s a. State s a -> s -> s
execState State VM ()
s VM
vm
  in case Getting (Maybe VMResult) VM (Maybe VMResult)
-> VM -> Maybe VMResult
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Maybe VMResult) VM (Maybe VMResult)
Lens' VM (Maybe VMResult)
EVM.result VM
vm of

    Nothing -> State VM () -> QueryT IO (VM, [Tree BranchInfo])
cont State VM ()
exec1

    Just (VMFailure (EVM.Query q :: Query
q@(PleaseAskSMT _ _ continue :: BranchCondition -> State VM ()
continue))) -> let
      codelocation :: CodeLocation
codelocation = VM -> CodeLocation
getCodeLocation VM
vm
      iteration :: Integer
iteration = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
num (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Getting (Maybe Int) VM (Maybe Int) -> VM -> Maybe Int
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Map CodeLocation Int -> Const (Maybe Int) (Map CodeLocation Int))
-> VM -> Const (Maybe Int) VM
Lens' VM (Map CodeLocation Int)
iterations ((Map CodeLocation Int -> Const (Maybe Int) (Map CodeLocation Int))
 -> VM -> Const (Maybe Int) VM)
-> ((Maybe Int -> Const (Maybe Int) (Maybe Int))
    -> Map CodeLocation Int
    -> Const (Maybe Int) (Map CodeLocation Int))
-> Getting (Maybe Int) VM (Maybe Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map CodeLocation Int)
-> Lens'
     (Map CodeLocation Int) (Maybe (IxValue (Map CodeLocation Int)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
Index (Map CodeLocation Int)
codelocation) VM
vm
      -- as an optimization, we skip consulting smt
      -- if we've been at the location less than 5 times
      in if Integer
iteration Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe 0 Maybe Integer
maxIter) 5)
         then State VM () -> QueryT IO (VM, [Tree BranchInfo])
cont (State VM () -> QueryT IO (VM, [Tree BranchInfo]))
-> State VM () -> QueryT IO (VM, [Tree BranchInfo])
forall a b. (a -> b) -> a -> b
$ BranchCondition -> State VM ()
continue BranchCondition
EVM.Unknown
         else IO (State VM ()) -> QueryT IO (State VM ())
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (Fetcher
fetcher Query
q) QueryT IO (State VM ())
-> (State VM () -> QueryT IO (VM, [Tree BranchInfo]))
-> QueryT IO (VM, [Tree BranchInfo])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State VM () -> QueryT IO (VM, [Tree BranchInfo])
cont

    Just (VMFailure (EVM.Query q :: Query
q)) -> IO (State VM ()) -> QueryT IO (State VM ())
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (Fetcher
fetcher Query
q) QueryT IO (State VM ())
-> (State VM () -> QueryT IO (VM, [Tree BranchInfo]))
-> QueryT IO (VM, [Tree BranchInfo])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State VM () -> QueryT IO (VM, [Tree BranchInfo])
cont

    Just (VMFailure (Choose (EVM.PleaseChoosePath whiff :: Whiff
whiff continue :: Bool -> State VM ()
continue)))
      -> case VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
vm Maybe Integer
maxIter of
        Nothing -> let
          lvm :: VM
lvm = State VM () -> VM -> VM
forall s a. State s a -> s -> s
execState (Bool -> State VM ()
continue Bool
True) VM
vm
          rvm :: VM
rvm = State VM () -> VM -> VM
forall s a. State s a -> s -> s
execState (Bool -> State VM ()
continue Bool
False) VM
vm
          in do
            Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
            (leftvm :: VM
leftvm, left :: [Tree BranchInfo]
left) <- Fetcher -> Maybe Integer -> VM -> QueryT IO (VM, [Tree BranchInfo])
interpret' Fetcher
fetcher Maybe Integer
maxIter VM
lvm
            Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
            Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
            (rightvm :: VM
rightvm, right :: [Tree BranchInfo]
right) <- Fetcher -> Maybe Integer -> VM -> QueryT IO (VM, [Tree BranchInfo])
interpret' Fetcher
fetcher Maybe Integer
maxIter VM
rvm
            Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
            (VM, [Tree BranchInfo]) -> QueryT IO (VM, [Tree BranchInfo])
forall (m :: * -> *) a. Monad m => a -> m a
return (VM
vm, [BranchInfo -> [Tree BranchInfo] -> Tree BranchInfo
forall a. a -> Forest a -> Tree a
Node (VM -> Maybe Whiff -> BranchInfo
BranchInfo VM
leftvm (Whiff -> Maybe Whiff
forall a. a -> Maybe a
Just Whiff
whiff)) [Tree BranchInfo]
left, BranchInfo -> [Tree BranchInfo] -> Tree BranchInfo
forall a. a -> Forest a -> Tree a
Node (VM -> Maybe Whiff -> BranchInfo
BranchInfo VM
rightvm (Whiff -> Maybe Whiff
forall a. a -> Maybe a
Just Whiff
whiff)) [Tree BranchInfo]
right])
        Just n :: Bool
n -> State VM () -> QueryT IO (VM, [Tree BranchInfo])
cont (State VM () -> QueryT IO (VM, [Tree BranchInfo]))
-> State VM () -> QueryT IO (VM, [Tree BranchInfo])
forall a b. (a -> b) -> a -> b
$ Bool -> State VM ()
continue (Bool -> Bool
not Bool
n)

    Just _
      -> (VM, [Tree BranchInfo]) -> QueryT IO (VM, [Tree BranchInfo])
forall (m :: * -> *) a. Monad m => a -> m a
return (VM
vm, [])

-- | Interpreter which explores all paths at
-- | branching points.
-- | returns a list of possible final evm states
interpret
  :: Fetch.Fetcher
  -> Maybe Integer --max iterations
  -> Stepper a
  -> StateT VM Query [a]
interpret :: Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret fetcher :: Fetcher
fetcher maxIter :: Maybe Integer
maxIter =
  ProgramView Action a -> StateT VM Query [a]
forall a. ProgramView Action a -> StateT VM Query [a]
eval (ProgramView Action a -> StateT VM Query [a])
-> (Stepper a -> ProgramView Action a)
-> Stepper a
-> StateT VM Query [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stepper a -> ProgramView Action a
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
Operational.view

  where
    eval
      :: Operational.ProgramView Stepper.Action a
      -> StateT VM Query [a]

    eval :: ProgramView Action a -> StateT VM Query [a]
eval (Operational.Return x :: a
x) =
      [a] -> StateT VM Query [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a
x]

    eval (action :: Action b
action Operational.:>>= k :: b -> ProgramT Action Identity a
k) =
      case Action b
action of
        Stepper.Exec ->
          StateT VM Query VMResult
forall (m :: * -> *). MonadState VM m => m VMResult
exec StateT VM Query VMResult
-> (VMResult -> StateT VM Query [a]) -> StateT VM Query [a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (ProgramT Action Identity a -> StateT VM Query [a])
-> (b -> ProgramT Action Identity a) -> b -> StateT VM Query [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        Stepper.Run ->
          StateT VM Query VM
forall (m :: * -> *). MonadState VM m => m VM
run StateT VM Query VM
-> (VM -> StateT VM Query [a]) -> StateT VM Query [a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (ProgramT Action Identity a -> StateT VM Query [a])
-> (b -> ProgramT Action Identity a) -> b -> StateT VM Query [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        Stepper.Ask (EVM.PleaseChoosePath _ continue :: Bool -> State VM ()
continue) -> do
          VM
vm <- StateT VM Query VM
forall s (m :: * -> *). MonadState s m => m s
get
          case VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
vm Maybe Integer
maxIter of
            Nothing -> do
              Int -> StateT VM Query ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
              [a]
a <- Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (State VM () -> Stepper ()
forall a. EVM a -> Stepper a
Stepper.evm (Bool -> State VM ()
continue Bool
True) Stepper ()
-> (() -> ProgramT Action Identity a) -> ProgramT Action Identity a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> ProgramT Action Identity a
() -> ProgramT Action Identity a
k)
              VM -> StateT VM Query ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put VM
vm
              Int -> StateT VM Query ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
              Int -> StateT VM Query ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
              [a]
b <- Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (State VM () -> Stepper ()
forall a. EVM a -> Stepper a
Stepper.evm (Bool -> State VM ()
continue Bool
False) Stepper ()
-> (() -> ProgramT Action Identity a) -> ProgramT Action Identity a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> ProgramT Action Identity a
() -> ProgramT Action Identity a
k)
              Int -> StateT VM Query ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
              [a] -> StateT VM Query [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> StateT VM Query [a]) -> [a] -> StateT VM Query [a]
forall a b. (a -> b) -> a -> b
$ [a]
a [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
b
            Just n :: Bool
n ->
              Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (State VM () -> Stepper ()
forall a. EVM a -> Stepper a
Stepper.evm (Bool -> State VM ()
continue (Bool -> Bool
not Bool
n)) Stepper ()
-> (() -> ProgramT Action Identity a) -> ProgramT Action Identity a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> ProgramT Action Identity a
() -> ProgramT Action Identity a
k)
        Stepper.Wait q :: Query
q -> do
          let performQuery :: StateT VM Query [a]
performQuery = do
                State VM ()
m <- IO (State VM ()) -> StateT VM Query (State VM ())
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Fetcher
fetcher Query
q)
                Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (State VM () -> Stepper ()
forall a. EVM a -> Stepper a
Stepper.evm State VM ()
m Stepper ()
-> (() -> ProgramT Action Identity a) -> ProgramT Action Identity a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> ProgramT Action Identity a
() -> ProgramT Action Identity a
k)

          case Query
q of
            PleaseAskSMT _ _ continue :: BranchCondition -> State VM ()
continue -> do
              CodeLocation
codelocation <- VM -> CodeLocation
getCodeLocation (VM -> CodeLocation)
-> StateT VM Query VM -> StateT VM Query CodeLocation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT VM Query VM
forall s (m :: * -> *). MonadState s m => m s
get
              Integer
iteration <- Int -> Integer
forall a b. (Integral a, Num b) => a -> b
num (Int -> Integer) -> (Maybe Int -> Int) -> Maybe Int -> Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 (Maybe Int -> Integer)
-> StateT VM Query (Maybe Int) -> StateT VM Query Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting (Maybe Int) VM (Maybe Int) -> StateT VM Query (Maybe Int)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Map CodeLocation Int -> Const (Maybe Int) (Map CodeLocation Int))
-> VM -> Const (Maybe Int) VM
Lens' VM (Map CodeLocation Int)
iterations ((Map CodeLocation Int -> Const (Maybe Int) (Map CodeLocation Int))
 -> VM -> Const (Maybe Int) VM)
-> ((Maybe Int -> Const (Maybe Int) (Maybe Int))
    -> Map CodeLocation Int
    -> Const (Maybe Int) (Map CodeLocation Int))
-> Getting (Maybe Int) VM (Maybe Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map CodeLocation Int)
-> Lens'
     (Map CodeLocation Int) (Maybe (IxValue (Map CodeLocation Int)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
Index (Map CodeLocation Int)
codelocation)

              -- if this is the first time we are branching at this point,
              -- explore both branches without consulting SMT.
              -- Exploring too many branches is a lot cheaper than
              -- consulting our SMT solver.
              if Integer
iteration Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe 0 Maybe Integer
maxIter) 5)
              then Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (State VM () -> Stepper ()
forall a. EVM a -> Stepper a
Stepper.evm (BranchCondition -> State VM ()
continue BranchCondition
EVM.Unknown) Stepper ()
-> (() -> ProgramT Action Identity a) -> ProgramT Action Identity a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> ProgramT Action Identity a
() -> ProgramT Action Identity a
k)
              else StateT VM Query [a]
performQuery

            _ -> StateT VM Query [a]
performQuery

        Stepper.EVM m :: EVM b
m ->
          (VM -> (b, VM)) -> StateT VM Query b
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state (EVM b -> VM -> (b, VM)
forall s a. State s a -> s -> (a, s)
runState EVM b
m) StateT VM Query b
-> (b -> StateT VM Query [a]) -> StateT VM Query [a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher
-> Maybe Integer
-> ProgramT Action Identity a
-> StateT VM Query [a]
forall a.
Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
interpret Fetcher
fetcher Maybe Integer
maxIter (ProgramT Action Identity a -> StateT VM Query [a])
-> (b -> ProgramT Action Identity a) -> b -> StateT VM Query [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k

maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
maxIterationsReached _ Nothing = Maybe Bool
forall a. Maybe a
Nothing
maxIterationsReached vm :: VM
vm (Just maxIter :: Integer
maxIter) =
  let codelocation :: CodeLocation
codelocation = VM -> CodeLocation
getCodeLocation VM
vm
      iters :: Int
iters = Getting Int VM Int -> VM -> Int
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Map CodeLocation Int -> Const Int (Map CodeLocation Int))
-> VM -> Const Int VM
Lens' VM (Map CodeLocation Int)
iterations ((Map CodeLocation Int -> Const Int (Map CodeLocation Int))
 -> VM -> Const Int VM)
-> ((Int -> Const Int Int)
    -> Map CodeLocation Int -> Const Int (Map CodeLocation Int))
-> Getting Int VM Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map CodeLocation Int)
-> Lens'
     (Map CodeLocation Int) (Maybe (IxValue (Map CodeLocation Int)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
Index (Map CodeLocation Int)
codelocation ((Maybe Int -> Const Int (Maybe Int))
 -> Map CodeLocation Int -> Const Int (Map CodeLocation Int))
-> ((Int -> Const Int Int) -> Maybe Int -> Const Int (Maybe Int))
-> (Int -> Const Int Int)
-> Map CodeLocation Int
-> Const Int (Map CodeLocation Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Iso' (Maybe Int) Int
forall a. Eq a => a -> Iso' (Maybe a) a
non 0) VM
vm
  in if Integer -> Int
forall a b. (Integral a, Num b) => a -> b
num Integer
maxIter Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
iters
     then Getting (Maybe Bool) VM (Maybe Bool) -> VM -> Maybe Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Cache -> Const (Maybe Bool) Cache) -> VM -> Const (Maybe Bool) VM
Lens' VM Cache
cache ((Cache -> Const (Maybe Bool) Cache)
 -> VM -> Const (Maybe Bool) VM)
-> ((Maybe Bool -> Const (Maybe Bool) (Maybe Bool))
    -> Cache -> Const (Maybe Bool) Cache)
-> Getting (Maybe Bool) VM (Maybe Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (CodeLocation, Int) Bool
 -> Const (Maybe Bool) (Map (CodeLocation, Int) Bool))
-> Cache -> Const (Maybe Bool) Cache
Lens' Cache (Map (CodeLocation, Int) Bool)
path ((Map (CodeLocation, Int) Bool
  -> Const (Maybe Bool) (Map (CodeLocation, Int) Bool))
 -> Cache -> Const (Maybe Bool) Cache)
-> ((Maybe Bool -> Const (Maybe Bool) (Maybe Bool))
    -> Map (CodeLocation, Int) Bool
    -> Const (Maybe Bool) (Map (CodeLocation, Int) Bool))
-> (Maybe Bool -> Const (Maybe Bool) (Maybe Bool))
-> Cache
-> Const (Maybe Bool) Cache
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (CodeLocation, Int) Bool)
-> Lens'
     (Map (CodeLocation, Int) Bool)
     (Maybe (IxValue (Map (CodeLocation, Int) Bool)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (CodeLocation
codelocation, Int
iters Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)) VM
vm
     else Maybe Bool
forall a. Maybe a
Nothing

type Precondition = VM -> SBool
type Postcondition = (VM, VM) -> SBool

checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
checkAssert :: ByteString
-> Maybe (Text, [AbiType])
-> [[Char]]
-> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
checkAssert c :: ByteString
c signature' :: Maybe (Text, [AbiType])
signature' concreteArgs :: [[Char]]
concreteArgs = ByteString
-> Maybe (Text, [AbiType])
-> [[Char]]
-> StorageModel
-> Precondition
-> Maybe Postcondition
-> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
verifyContract ByteString
c Maybe (Text, [AbiType])
signature' [[Char]]
concreteArgs StorageModel
SymbolicS (SBool -> Precondition
forall a b. a -> b -> a
const SBool
sTrue) (Postcondition -> Maybe Postcondition
forall a. a -> Maybe a
Just Postcondition
checkAssertions)

checkAssertions :: Postcondition
checkAssertions :: Postcondition
checkAssertions (_, out :: VM
out) = case Getting (Maybe VMResult) VM (Maybe VMResult)
-> VM -> Maybe VMResult
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Maybe VMResult) VM (Maybe VMResult)
Lens' VM (Maybe VMResult)
result VM
out of
  Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> SBool
sFalse
  _ -> SBool
sTrue

verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
verifyContract :: ByteString
-> Maybe (Text, [AbiType])
-> [[Char]]
-> StorageModel
-> Precondition
-> Maybe Postcondition
-> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
verifyContract theCode :: ByteString
theCode signature' :: Maybe (Text, [AbiType])
signature' concreteArgs :: [[Char]]
concreteArgs storagemodel :: StorageModel
storagemodel pre :: Precondition
pre maybepost :: Maybe Postcondition
maybepost = do
    VM
preStateRaw <- Maybe (Text, [AbiType])
-> [[Char]] -> ByteString -> StorageModel -> Query VM
abstractVM Maybe (Text, [AbiType])
signature' [[Char]]
concreteArgs ByteString
theCode  StorageModel
storagemodel
    -- add the pre condition to the pathconditions to ensure that we are only exploring valid paths
    let preState :: VM
preState = ASetter VM VM [(SBool, Whiff)] [(SBool, Whiff)]
-> ([(SBool, Whiff)] -> [(SBool, Whiff)]) -> VM -> VM
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter VM VM [(SBool, Whiff)] [(SBool, Whiff)]
Lens' VM [(SBool, Whiff)]
constraints ([(SBool, Whiff)] -> [(SBool, Whiff)] -> [(SBool, Whiff)]
forall a. [a] -> [a] -> [a]
(++) [(Precondition
pre VM
preStateRaw, [Char] -> [Whiff] -> Whiff
Todo "assumptions" [])]) VM
preStateRaw
    Either (Tree BranchInfo) (Tree BranchInfo)
v <- VM
-> Maybe Integer
-> Maybe (BlockNumber, Text)
-> Maybe Postcondition
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
verify VM
preState Maybe Integer
forall a. Maybe a
Nothing Maybe (BlockNumber, Text)
forall a. Maybe a
Nothing Maybe Postcondition
maybepost
    (Either (Tree BranchInfo) (Tree BranchInfo), VM)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Tree BranchInfo) (Tree BranchInfo)
v, VM
preState)

pruneDeadPaths :: [VM] -> [VM]
pruneDeadPaths :: [VM] -> [VM]
pruneDeadPaths =
  (VM -> Bool) -> [VM] -> [VM]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VM -> Bool) -> [VM] -> [VM]) -> (VM -> Bool) -> [VM] -> [VM]
forall a b. (a -> b) -> a -> b
$ \vm :: VM
vm -> case Getting (Maybe VMResult) VM (Maybe VMResult)
-> VM -> Maybe VMResult
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Maybe VMResult) VM (Maybe VMResult)
Lens' VM (Maybe VMResult)
result VM
vm of
    Just (VMFailure DeadPath) -> Bool
False
    _ -> Bool
True

consistentPath :: VM -> Query (Maybe VM)
consistentPath :: VM -> Query (Maybe VM)
consistentPath vm :: VM
vm = do
  QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
resetAssertions
  SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (SBool, Whiff) -> SBool
forall a b. (a, b) -> a
fst ((SBool, Whiff) -> SBool) -> [(SBool, Whiff)] -> [SBool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
-> VM -> [(SBool, Whiff)]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
Lens' VM [(SBool, Whiff)]
constraints VM
vm
  QueryT IO CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat QueryT IO CheckSatResult
-> (CheckSatResult -> Query (Maybe VM)) -> Query (Maybe VM)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Sat -> Maybe VM -> Query (Maybe VM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VM -> Query (Maybe VM)) -> Maybe VM -> Query (Maybe VM)
forall a b. (a -> b) -> a -> b
$ VM -> Maybe VM
forall a. a -> Maybe a
Just VM
vm
    Unk -> Maybe VM -> Query (Maybe VM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VM -> Query (Maybe VM)) -> Maybe VM -> Query (Maybe VM)
forall a b. (a -> b) -> a -> b
$ VM -> Maybe VM
forall a. a -> Maybe a
Just VM
vm -- the path may still be consistent
    Unsat -> Maybe VM -> Query (Maybe VM)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe VM
forall a. Maybe a
Nothing
    DSat _ -> [Char] -> Query (Maybe VM)
forall a. HasCallStack => [Char] -> a
error "unexpected DSAT"

consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo))
consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo))
consistentTree (Node (BranchInfo vm :: VM
vm w :: Maybe Whiff
w) []) = do
  VM -> Query (Maybe VM)
consistentPath VM
vm Query (Maybe VM)
-> (Maybe VM -> Query (Maybe (Tree BranchInfo)))
-> Query (Maybe (Tree BranchInfo))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Nothing  -> Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Tree BranchInfo)
forall a. Maybe a
Nothing
    Just vm' :: VM
vm' -> Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo)))
-> Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo))
forall a b. (a -> b) -> a -> b
$ Tree BranchInfo -> Maybe (Tree BranchInfo)
forall a. a -> Maybe a
Just (Tree BranchInfo -> Maybe (Tree BranchInfo))
-> Tree BranchInfo -> Maybe (Tree BranchInfo)
forall a b. (a -> b) -> a -> b
$ BranchInfo -> [Tree BranchInfo] -> Tree BranchInfo
forall a. a -> Forest a -> Tree a
Node (VM -> Maybe Whiff -> BranchInfo
BranchInfo VM
vm' Maybe Whiff
w) []
consistentTree (Node b :: BranchInfo
b xs :: [Tree BranchInfo]
xs) = do
  [Tree BranchInfo]
consistentChildren <- [Maybe (Tree BranchInfo)] -> [Tree BranchInfo]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Tree BranchInfo)] -> [Tree BranchInfo])
-> QueryT IO [Maybe (Tree BranchInfo)]
-> QueryT IO [Tree BranchInfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Tree BranchInfo]
-> (Tree BranchInfo -> Query (Maybe (Tree BranchInfo)))
-> QueryT IO [Maybe (Tree BranchInfo)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Tree BranchInfo]
xs Tree BranchInfo -> Query (Maybe (Tree BranchInfo))
consistentTree
  if [Tree BranchInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tree BranchInfo]
consistentChildren then
    Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Tree BranchInfo)
forall a. Maybe a
Nothing
  else
    Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo)))
-> Maybe (Tree BranchInfo) -> Query (Maybe (Tree BranchInfo))
forall a b. (a -> b) -> a -> b
$ Tree BranchInfo -> Maybe (Tree BranchInfo)
forall a. a -> Maybe a
Just (BranchInfo -> [Tree BranchInfo] -> Tree BranchInfo
forall a. a -> Forest a -> Tree a
Node BranchInfo
b [Tree BranchInfo]
consistentChildren)


leaves :: Tree BranchInfo -> [VM]
leaves :: Tree BranchInfo -> [VM]
leaves (Node x :: BranchInfo
x []) = [BranchInfo -> VM
_vm BranchInfo
x]
leaves (Node _ xs :: [Tree BranchInfo]
xs) = (Tree BranchInfo -> [VM]) -> [Tree BranchInfo] -> [VM]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Tree BranchInfo -> [VM]
leaves [Tree BranchInfo]
xs

-- | Symbolically execute the VM and check all endstates against the postcondition, if available.
-- Returns `Right (Tree BranchInfo)` if the postcondition can be violated, or
-- or `Left (Tree BranchInfo)`, if the postcondition holds for all endstates.
verify :: VM -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo))
verify :: VM
-> Maybe Integer
-> Maybe (BlockNumber, Text)
-> Maybe Postcondition
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
verify preState :: VM
preState maxIter :: Maybe Integer
maxIter rpcinfo :: Maybe (BlockNumber, Text)
rpcinfo maybepost :: Maybe Postcondition
maybepost = do
  State
smtState <- QueryT IO State
forall (m :: * -> *). MonadQuery m => m State
queryState
  Tree BranchInfo
tree <- Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)
doInterpret (Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
Fetch.oracle (State -> Maybe State
forall a. a -> Maybe a
Just State
smtState) Maybe (BlockNumber, Text)
rpcinfo Bool
False) Maybe Integer
maxIter VM
preState
  case Maybe Postcondition
maybepost of
    (Just post :: Postcondition
post) -> do
      let livePaths :: [VM]
livePaths = [VM] -> [VM]
pruneDeadPaths ([VM] -> [VM]) -> [VM] -> [VM]
forall a b. (a -> b) -> a -> b
$ Tree BranchInfo -> [VM]
leaves Tree BranchInfo
tree
      -- can also do these queries individually (even concurrently!). Could save time and report multiple violations
          postC :: SBool
postC = [SBool] -> SBool
sOr ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ Precondition -> [VM] -> [SBool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\postState :: VM
postState -> ([SBool] -> SBool
sAnd ((SBool, Whiff) -> SBool
forall a b. (a, b) -> a
fst ((SBool, Whiff) -> SBool) -> [(SBool, Whiff)] -> [SBool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
-> VM -> [(SBool, Whiff)]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
Lens' VM [(SBool, Whiff)]
constraints VM
postState)) SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (Postcondition
post (VM
preState, VM
postState))) [VM]
livePaths
      -- is there any path which can possibly violate
      -- the postcondition?
      QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
resetAssertions
      SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
postC
      IO () -> QueryT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn "checking postcondition..."
      QueryT IO CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat QueryT IO CheckSatResult
-> (CheckSatResult
    -> Query (Either (Tree BranchInfo) (Tree BranchInfo)))
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Unk -> do IO () -> QueryT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn "postcondition query timed out"
                  Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Tree BranchInfo) (Tree BranchInfo)
 -> Query (Either (Tree BranchInfo) (Tree BranchInfo)))
-> Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall a b. (a -> b) -> a -> b
$ Tree BranchInfo -> Either (Tree BranchInfo) (Tree BranchInfo)
forall a b. a -> Either a b
Left Tree BranchInfo
tree
        Unsat -> do IO () -> QueryT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn "Q.E.D."
                    Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Tree BranchInfo) (Tree BranchInfo)
 -> Query (Either (Tree BranchInfo) (Tree BranchInfo)))
-> Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall a b. (a -> b) -> a -> b
$ Tree BranchInfo -> Either (Tree BranchInfo) (Tree BranchInfo)
forall a b. a -> Either a b
Left Tree BranchInfo
tree
        Sat -> Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Tree BranchInfo) (Tree BranchInfo)
 -> Query (Either (Tree BranchInfo) (Tree BranchInfo)))
-> Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall a b. (a -> b) -> a -> b
$ Tree BranchInfo -> Either (Tree BranchInfo) (Tree BranchInfo)
forall a b. b -> Either a b
Right Tree BranchInfo
tree
        DSat _ -> [Char] -> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall a. HasCallStack => [Char] -> a
error "unexpected DSAT"

    Nothing -> do IO () -> QueryT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn "Nothing to check"
                  Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Tree BranchInfo) (Tree BranchInfo)
 -> Query (Either (Tree BranchInfo) (Tree BranchInfo)))
-> Either (Tree BranchInfo) (Tree BranchInfo)
-> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall a b. (a -> b) -> a -> b
$ Tree BranchInfo -> Either (Tree BranchInfo) (Tree BranchInfo)
forall a b. a -> Either a b
Left Tree BranchInfo
tree

-- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.
equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)
equivalenceCheck :: ByteString
-> ByteString
-> Maybe Integer
-> Maybe (Text, [AbiType])
-> Query (Either ([VM], [VM]) VM)
equivalenceCheck bytecodeA :: ByteString
bytecodeA bytecodeB :: ByteString
bytecodeB maxiter :: Maybe Integer
maxiter signature' :: Maybe (Text, [AbiType])
signature' = do
  let 
    bytecodeA' :: ByteString
bytecodeA' = if ByteString -> Bool
BS.null ByteString
bytecodeA then [Word8] -> ByteString
BS.pack [0] else ByteString
bytecodeA
    bytecodeB' :: ByteString
bytecodeB' = if ByteString -> Bool
BS.null ByteString
bytecodeB then [Word8] -> ByteString
BS.pack [0] else ByteString
bytecodeB
  VM
preStateA <- Maybe (Text, [AbiType])
-> [[Char]] -> ByteString -> StorageModel -> Query VM
abstractVM Maybe (Text, [AbiType])
signature' [] ByteString
bytecodeA' StorageModel
SymbolicS

  let preself :: Addr
preself = VM
preStateA VM -> Getting Addr VM Addr -> Addr
forall s a. s -> Getting a s a -> a
^. (FrameState -> Const Addr FrameState) -> VM -> Const Addr VM
Lens' VM FrameState
state ((FrameState -> Const Addr FrameState) -> VM -> Const Addr VM)
-> ((Addr -> Const Addr Addr)
    -> FrameState -> Const Addr FrameState)
-> Getting Addr VM Addr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Addr -> Const Addr Addr) -> FrameState -> Const Addr FrameState
Lens' FrameState Addr
contract
      precaller :: SAddr
precaller = VM
preStateA VM -> Getting SAddr VM SAddr -> SAddr
forall s a. s -> Getting a s a -> a
^. (FrameState -> Const SAddr FrameState) -> VM -> Const SAddr VM
Lens' VM FrameState
state ((FrameState -> Const SAddr FrameState) -> VM -> Const SAddr VM)
-> ((SAddr -> Const SAddr SAddr)
    -> FrameState -> Const SAddr FrameState)
-> Getting SAddr VM SAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SAddr -> Const SAddr SAddr)
-> FrameState -> Const SAddr FrameState
Lens' FrameState SAddr
caller
      callvalue' :: SymWord
callvalue' = VM
preStateA VM -> Getting SymWord VM SymWord -> SymWord
forall s a. s -> Getting a s a -> a
^. (FrameState -> Const SymWord FrameState) -> VM -> Const SymWord VM
Lens' VM FrameState
state ((FrameState -> Const SymWord FrameState)
 -> VM -> Const SymWord VM)
-> ((SymWord -> Const SymWord SymWord)
    -> FrameState -> Const SymWord FrameState)
-> Getting SymWord VM SymWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymWord -> Const SymWord SymWord)
-> FrameState -> Const SymWord FrameState
Lens' FrameState SymWord
callvalue
      prestorage :: Storage
prestorage = VM
preStateA VM -> Getting (Endo Storage) VM Storage -> Storage
forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! (Env -> Const (Endo Storage) Env) -> VM -> Const (Endo Storage) VM
Lens' VM Env
env ((Env -> Const (Endo Storage) Env)
 -> VM -> Const (Endo Storage) VM)
-> ((Storage -> Const (Endo Storage) Storage)
    -> Env -> Const (Endo Storage) Env)
-> Getting (Endo Storage) VM Storage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Addr Contract -> Const (Endo Storage) (Map Addr Contract))
-> Env -> Const (Endo Storage) Env
Lens' Env (Map Addr Contract)
contracts ((Map Addr Contract -> Const (Endo Storage) (Map Addr Contract))
 -> Env -> Const (Endo Storage) Env)
-> ((Storage -> Const (Endo Storage) Storage)
    -> Map Addr Contract -> Const (Endo Storage) (Map Addr Contract))
-> (Storage -> Const (Endo Storage) Storage)
-> Env
-> Const (Endo Storage) Env
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map Addr Contract)
-> Traversal' (Map Addr Contract) (IxValue (Map Addr Contract))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map Addr Contract)
Addr
preself ((Contract -> Const (Endo Storage) Contract)
 -> Map Addr Contract -> Const (Endo Storage) (Map Addr Contract))
-> ((Storage -> Const (Endo Storage) Storage)
    -> Contract -> Const (Endo Storage) Contract)
-> (Storage -> Const (Endo Storage) Storage)
-> Map Addr Contract
-> Const (Endo Storage) (Map Addr Contract)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Storage -> Const (Endo Storage) Storage)
-> Contract -> Const (Endo Storage) Contract
Lens' Contract Storage
storage
      (calldata' :: Buffer
calldata', cdlen :: SymWord
cdlen) = Getting (Buffer, SymWord) VM (Buffer, SymWord)
-> VM -> (Buffer, SymWord)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((FrameState -> Const (Buffer, SymWord) FrameState)
-> VM -> Const (Buffer, SymWord) VM
Lens' VM FrameState
state ((FrameState -> Const (Buffer, SymWord) FrameState)
 -> VM -> Const (Buffer, SymWord) VM)
-> (((Buffer, SymWord)
     -> Const (Buffer, SymWord) (Buffer, SymWord))
    -> FrameState -> Const (Buffer, SymWord) FrameState)
-> Getting (Buffer, SymWord) VM (Buffer, SymWord)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Buffer, SymWord) -> Const (Buffer, SymWord) (Buffer, SymWord))
-> FrameState -> Const (Buffer, SymWord) FrameState
Lens' FrameState (Buffer, SymWord)
calldata) VM
preStateA
      pathconds :: [(SBool, Whiff)]
pathconds = Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
-> VM -> [(SBool, Whiff)]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
Lens' VM [(SBool, Whiff)]
constraints VM
preStateA
      preStateB :: VM
preStateB = ContractCode
-> Storage
-> StorageModel
-> SAddr
-> SymWord
-> (Buffer, SymWord)
-> VM
loadSymVM (Buffer -> ContractCode
RuntimeCode (ByteString -> Buffer
ConcreteBuffer ByteString
bytecodeB')) Storage
prestorage StorageModel
SymbolicS SAddr
precaller SymWord
callvalue' (Buffer
calldata', SymWord
cdlen) VM -> (VM -> VM) -> VM
forall a b. a -> (a -> b) -> b
& ASetter VM VM [(SBool, Whiff)] [(SBool, Whiff)]
-> [(SBool, Whiff)] -> VM -> VM
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter VM VM [(SBool, Whiff)] [(SBool, Whiff)]
Lens' VM [(SBool, Whiff)]
constraints [(SBool, Whiff)]
pathconds

  State
smtState <- QueryT IO State
forall (m :: * -> *). MonadQuery m => m State
queryState
  Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
  Tree BranchInfo
aVMs <- Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)
doInterpret (Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
Fetch.oracle (State -> Maybe State
forall a. a -> Maybe a
Just State
smtState) Maybe (BlockNumber, Text)
forall a. Maybe a
Nothing Bool
False) Maybe Integer
maxiter VM
preStateA
  Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
  Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
  Tree BranchInfo
bVMs <- Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)
doInterpret (Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
Fetch.oracle (State -> Maybe State
forall a. a -> Maybe a
Just State
smtState) Maybe (BlockNumber, Text)
forall a. Maybe a
Nothing Bool
False) Maybe Integer
maxiter VM
preStateB
  Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
  -- Check each pair of endstates for equality:
  let differingEndStates :: [SBool]
differingEndStates = (VM -> Precondition) -> Postcondition
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry VM -> Precondition
distinct Postcondition -> [(VM, VM)] -> [SBool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VM
a,VM
b) | VM
a <- [VM] -> [VM]
pruneDeadPaths (Tree BranchInfo -> [VM]
leaves Tree BranchInfo
aVMs), VM
b <- [VM] -> [VM]
pruneDeadPaths (Tree BranchInfo -> [VM]
leaves Tree BranchInfo
bVMs)]
      distinct :: VM -> Precondition
distinct a :: VM
a b :: VM
b =
        let (aPath :: [(SBool, Whiff)]
aPath, bPath :: [(SBool, Whiff)]
bPath) = (VM -> [(SBool, Whiff)])
-> (VM, VM) -> ([(SBool, Whiff)], [(SBool, Whiff)])
forall a b. (a -> b) -> (a, a) -> (b, b)
both' (Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
-> VM -> [(SBool, Whiff)]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [(SBool, Whiff)] VM [(SBool, Whiff)]
Lens' VM [(SBool, Whiff)]
constraints) (VM
a, VM
b)
            (aSelf :: Addr
aSelf, bSelf :: Addr
bSelf) = (VM -> Addr) -> (VM, VM) -> (Addr, Addr)
forall a b. (a -> b) -> (a, a) -> (b, b)
both' (Getting Addr VM Addr -> VM -> Addr
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((FrameState -> Const Addr FrameState) -> VM -> Const Addr VM
Lens' VM FrameState
state ((FrameState -> Const Addr FrameState) -> VM -> Const Addr VM)
-> ((Addr -> Const Addr Addr)
    -> FrameState -> Const Addr FrameState)
-> Getting Addr VM Addr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Addr -> Const Addr Addr) -> FrameState -> Const Addr FrameState
Lens' FrameState Addr
contract)) (VM
a, VM
b)
            (aEnv :: Map Addr Contract
aEnv, bEnv :: Map Addr Contract
bEnv) = (VM -> Map Addr Contract)
-> (VM, VM) -> (Map Addr Contract, Map Addr Contract)
forall a b. (a -> b) -> (a, a) -> (b, b)
both' (Getting (Map Addr Contract) VM (Map Addr Contract)
-> VM -> Map Addr Contract
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Env -> Const (Map Addr Contract) Env)
-> VM -> Const (Map Addr Contract) VM
Lens' VM Env
env ((Env -> Const (Map Addr Contract) Env)
 -> VM -> Const (Map Addr Contract) VM)
-> ((Map Addr Contract
     -> Const (Map Addr Contract) (Map Addr Contract))
    -> Env -> Const (Map Addr Contract) Env)
-> Getting (Map Addr Contract) VM (Map Addr Contract)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Addr Contract
 -> Const (Map Addr Contract) (Map Addr Contract))
-> Env -> Const (Map Addr Contract) Env
Lens' Env (Map Addr Contract)
contracts)) (VM
a, VM
b)
            (aResult :: Maybe VMResult
aResult, bResult :: Maybe VMResult
bResult) = (VM -> Maybe VMResult)
-> (VM, VM) -> (Maybe VMResult, Maybe VMResult)
forall a b. (a -> b) -> (a, a) -> (b, b)
both' (Getting (Maybe VMResult) VM (Maybe VMResult)
-> VM -> Maybe VMResult
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Maybe VMResult) VM (Maybe VMResult)
Lens' VM (Maybe VMResult)
result) (VM
a, VM
b)
            (Symbolic _ aStorage :: SArray (WordN 256) (WordN 256)
aStorage, Symbolic _ bStorage :: SArray (WordN 256) (WordN 256)
bStorage) = (Getting Storage Contract Storage -> Contract -> Storage
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Storage Contract Storage
Lens' Contract Storage
storage (Map Addr Contract
aEnv Map Addr Contract
-> Getting (Endo Contract) (Map Addr Contract) Contract -> Contract
forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! Index (Map Addr Contract)
-> Traversal' (Map Addr Contract) (IxValue (Map Addr Contract))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map Addr Contract)
Addr
aSelf), Getting Storage Contract Storage -> Contract -> Storage
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Storage Contract Storage
Lens' Contract Storage
storage (Map Addr Contract
bEnv Map Addr Contract
-> Getting (Endo Contract) (Map Addr Contract) Contract -> Contract
forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! Index (Map Addr Contract)
-> Traversal' (Map Addr Contract) (IxValue (Map Addr Contract))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map Addr Contract)
Addr
bSelf))
            differingResults :: SBool
differingResults = case (Maybe VMResult
aResult, Maybe VMResult
bResult) of

              (Just (VMSuccess aOut :: Buffer
aOut), Just (VMSuccess bOut :: Buffer
bOut)) ->
                Buffer
aOut Buffer -> Buffer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= Buffer
bOut SBool -> SBool -> SBool
.|| SArray (WordN 256) (WordN 256)
aStorage SArray (WordN 256) (WordN 256)
-> SArray (WordN 256) (WordN 256) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SArray (WordN 256) (WordN 256)
bStorage SBool -> SBool -> SBool
.|| Bool -> SBool
fromBool (Addr
aSelf Addr -> Addr -> Bool
forall a. Eq a => a -> a -> Bool
/= Addr
bSelf)

              (Just (VMFailure UnexpectedSymbolicArg), _) ->
                [Char] -> SBool
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBool) -> [Char] -> SBool
forall a b. (a -> b) -> a -> b
$ "Unexpected symbolic argument at opcode: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> (Op -> [Char]) -> Maybe Op -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "??" Op -> [Char]
forall a. Show a => a -> [Char]
show (VM -> Maybe Op
vmOp VM
a) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> ". Not supported (yet!)"

              (_, Just (VMFailure UnexpectedSymbolicArg)) ->
                [Char] -> SBool
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBool) -> [Char] -> SBool
forall a b. (a -> b) -> a -> b
$ "Unexpected symbolic argument at opcode: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> (Op -> [Char]) -> Maybe Op -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "??" Op -> [Char]
forall a. Show a => a -> [Char]
show (VM -> Maybe Op
vmOp VM
a) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> ". Not supported (yet!)"

              (Just (VMFailure _), Just (VMFailure _)) -> SBool
sFalse

              (Just _, Just _) -> SBool
sTrue

              errormsg :: (Maybe VMResult, Maybe VMResult)
errormsg -> [Char] -> SBool
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBool) -> [Char] -> SBool
forall a b. (a -> b) -> a -> b
$ (Maybe VMResult, Maybe VMResult) -> [Char]
forall a. Show a => a -> [Char]
show (Maybe VMResult, Maybe VMResult)
errormsg

        in [SBool] -> SBool
sAnd ((SBool, Whiff) -> SBool
forall a b. (a, b) -> a
fst ((SBool, Whiff) -> SBool) -> [(SBool, Whiff)] -> [SBool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SBool, Whiff)]
aPath) SBool -> SBool -> SBool
.&& [SBool] -> SBool
sAnd ((SBool, Whiff) -> SBool
forall a b. (a, b) -> a
fst ((SBool, Whiff) -> SBool) -> [(SBool, Whiff)] -> [SBool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SBool, Whiff)]
bPath) SBool -> SBool -> SBool
.&& SBool
differingResults
  -- If there exists a pair of endstates where this is not the case,
  -- the following constraint is satisfiable
  SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sOr [SBool]
differingEndStates

  QueryT IO CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat QueryT IO CheckSatResult
-> (CheckSatResult -> Query (Either ([VM], [VM]) VM))
-> Query (Either ([VM], [VM]) VM)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     Unk -> [Char] -> Query (Either ([VM], [VM]) VM)
forall a. HasCallStack => [Char] -> a
error "solver said unknown!"
     Sat -> Either ([VM], [VM]) VM -> Query (Either ([VM], [VM]) VM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ([VM], [VM]) VM -> Query (Either ([VM], [VM]) VM))
-> Either ([VM], [VM]) VM -> Query (Either ([VM], [VM]) VM)
forall a b. (a -> b) -> a -> b
$ VM -> Either ([VM], [VM]) VM
forall a b. b -> Either a b
Right VM
preStateA
     Unsat -> Either ([VM], [VM]) VM -> Query (Either ([VM], [VM]) VM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ([VM], [VM]) VM -> Query (Either ([VM], [VM]) VM))
-> Either ([VM], [VM]) VM -> Query (Either ([VM], [VM]) VM)
forall a b. (a -> b) -> a -> b
$ ([VM], [VM]) -> Either ([VM], [VM]) VM
forall a b. a -> Either a b
Left (Tree BranchInfo -> [VM]
leaves Tree BranchInfo
aVMs, Tree BranchInfo -> [VM]
leaves Tree BranchInfo
bVMs)
     DSat _ -> [Char] -> Query (Either ([VM], [VM]) VM)
forall a. HasCallStack => [Char] -> a
error "unexpected DSAT"

both' :: (a -> b) -> (a, a) -> (b, b)
both' :: (a -> b) -> (a, a) -> (b, b)
both' f :: a -> b
f (x :: a
x, y :: a
y) = (a -> b
f a
x, a -> b
f a
y)

showCounterexample :: VM -> Maybe (Text, [AbiType]) -> Query ()
showCounterexample :: VM -> Maybe (Text, [AbiType]) -> QueryT IO ()
showCounterexample vm :: VM
vm maybesig :: Maybe (Text, [AbiType])
maybesig = do
  let (calldata' :: Buffer
calldata', S _ cdlen :: SBV (WordN 256)
cdlen) = Getting (Buffer, SymWord) VM (Buffer, SymWord)
-> VM -> (Buffer, SymWord)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((FrameState -> Const (Buffer, SymWord) FrameState)
-> VM -> Const (Buffer, SymWord) VM
Lens' VM FrameState
EVM.state ((FrameState -> Const (Buffer, SymWord) FrameState)
 -> VM -> Const (Buffer, SymWord) VM)
-> (((Buffer, SymWord)
     -> Const (Buffer, SymWord) (Buffer, SymWord))
    -> FrameState -> Const (Buffer, SymWord) FrameState)
-> Getting (Buffer, SymWord) VM (Buffer, SymWord)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Buffer, SymWord) -> Const (Buffer, SymWord) (Buffer, SymWord))
-> FrameState -> Const (Buffer, SymWord) FrameState
Lens' FrameState (Buffer, SymWord)
EVM.calldata) VM
vm
      S _ cvalue :: SBV (WordN 256)
cvalue = Getting SymWord VM SymWord -> VM -> SymWord
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((FrameState -> Const SymWord FrameState) -> VM -> Const SymWord VM
Lens' VM FrameState
EVM.state ((FrameState -> Const SymWord FrameState)
 -> VM -> Const SymWord VM)
-> ((SymWord -> Const SymWord SymWord)
    -> FrameState -> Const SymWord FrameState)
-> Getting SymWord VM SymWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymWord -> Const SymWord SymWord)
-> FrameState -> Const SymWord FrameState
Lens' FrameState SymWord
EVM.callvalue) VM
vm
      SAddr caller' :: SWord 160
caller' = Getting SAddr VM SAddr -> VM -> SAddr
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((FrameState -> Const SAddr FrameState) -> VM -> Const SAddr VM
Lens' VM FrameState
EVM.state ((FrameState -> Const SAddr FrameState) -> VM -> Const SAddr VM)
-> ((SAddr -> Const SAddr SAddr)
    -> FrameState -> Const SAddr FrameState)
-> Getting SAddr VM SAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SAddr -> Const SAddr SAddr)
-> FrameState -> Const SAddr FrameState
Lens' FrameState SAddr
EVM.caller) VM
vm
  Int
cdlen' <- WordN 256 -> Int
forall a b. (Integral a, Num b) => a -> b
num (WordN 256 -> Int) -> QueryT IO (WordN 256) -> QueryT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV (WordN 256) -> QueryT IO (WordN 256)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue SBV (WordN 256)
cdlen
  ByteString
calldatainput <- case Buffer
calldata' of
    SymbolicBuffer cd :: [SWord 8]
cd -> (SWord 8 -> QueryT IO Word8) -> [SWord 8] -> QueryT IO [Word8]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SBV Word8 -> QueryT IO Word8
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue(SBV Word8 -> QueryT IO Word8)
-> (SWord 8 -> SBV Word8) -> SWord 8 -> QueryT IO Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
.SWord 8 -> SBV Word8
forall a. FromSizedBV a => a -> FromSized a
fromSized) (Int -> [SWord 8] -> [SWord 8]
forall a. Int -> [a] -> [a]
take Int
cdlen' [SWord 8]
cd) QueryT IO [Word8]
-> ([Word8] -> QueryT IO ByteString) -> QueryT IO ByteString
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString -> QueryT IO ByteString
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> QueryT IO ByteString)
-> ([Word8] -> ByteString) -> [Word8] -> QueryT IO ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
pack
    ConcreteBuffer cd :: ByteString
cd -> ByteString -> QueryT IO ByteString
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> QueryT IO ByteString)
-> ByteString -> QueryT IO ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take Int
cdlen' ByteString
cd
  WordN 256
callvalue' <- SBV (WordN 256) -> QueryT IO (WordN 256)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue SBV (WordN 256)
cvalue
  Word160
caller'' <- WordN 160 -> Word160
forall a b. (Integral a, Num b) => a -> b
num (WordN 160 -> Word160)
-> QueryT IO (WordN 160) -> QueryT IO Word160
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord 160 -> QueryT IO (WordN 160)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue SWord 160
caller'
  IO () -> QueryT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> IO ()
putStrLn "Calldata:"
    ByteStringS -> IO ()
forall a. Show a => a -> IO ()
print (ByteStringS -> IO ()) -> ByteStringS -> IO ()
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteStringS
ByteStringS ByteString
calldatainput

    -- pretty print calldata input if signature is available
    case Maybe (Text, [AbiType])
maybesig of
      Just (name :: Text
name, types :: [AbiType]
types) -> [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> [Char]
unpack ([Text] -> Text
forall a. [a] -> a
head (Text -> Text -> [Text]
splitOn "(" Text
name)) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
        AbiValue -> [Char]
forall a. Show a => a -> [Char]
show (AbiType -> ByteString -> AbiValue
decodeAbiValue (Vector AbiType -> AbiType
AbiTupleType ([AbiType] -> Vector AbiType
forall a. [a] -> Vector a
fromList [AbiType]
types)) (ByteString -> AbiValue) -> ByteString -> AbiValue
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
Lazy.fromStrict (Int -> ByteString -> ByteString
BS.drop 4 ByteString
calldatainput))
      Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    [Char] -> IO ()
putStrLn "Caller:"
    Addr -> IO ()
forall a. Show a => a -> IO ()
print (Word160 -> Addr
Addr Word160
caller'')
    [Char] -> IO ()
putStrLn "Callvalue:"
    WordN 256 -> IO ()
forall a. Show a => a -> IO ()
print WordN 256
callvalue'