{-# 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.DoubleWord (Word256)

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 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 Int
n) | Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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) [Int
0..(Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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' Int
32 [SWord 8]
x, W256
32)
                          | Bool
otherwise = [Char] -> Query ([SWord 8], W256)
forall a. HasCallStack => [Char] -> a
error [Char]
"bad type"

symAbiArg (AbiIntType Int
n)  | Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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) [(Int
0 :: Int) ..(Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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' Int
32 [SWord 8]
x, W256
32)

                          | Bool
otherwise = [Char] -> Query ([SWord 8], W256)
forall a. HasCallStack => [Char] -> a
error [Char]
"bad type"
symAbiArg AbiType
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' Int
32 [SWord 8]
x, W256
32)

symAbiArg AbiType
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) [(Int
0 :: Int)..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' Int
32 [SWord 8]
x, W256
32)

symAbiArg (AbiBytesType Int
n) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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) [Int
0..Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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' Int
32 [SWord 8]
x, W256
32)

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

-- TODO: is this encoding correct?
symAbiArg (AbiArrayType Int
len 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 Int
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),
             W256
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 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 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
$ [Char]
"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
<> [Char]
". 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 Text
sig [AbiType]
typesignature [[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)  [Char]
"<symbolic>"
      mkArg :: AbiType -> [Char] -> Query ([SWord 8], W256)
mkArg AbiType
typ [Char]
"<symbolic>" = AbiType -> Query ([SWord 8], W256)
symAbiArg AbiType
typ
      mkArg AbiType
typ [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), W256
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 Maybe (Text, [AbiType])
typesignature [[Char]]
concreteArgs ByteString
x StorageModel
storagemodel = do
  ([SWord 8]
cd', SymWord
cdlen, (SBool, Whiff)
cdconstraint) <-
    case Maybe (Text, [AbiType])
typesignature of
      Maybe (Text, [AbiType])
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 [Char]
"calldataLength" SBV (WordN 256)
len, (SBV (WordN 256)
len SBV (WordN 256) -> SBV (WordN 256) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV (WordN 256)
256, [Char] -> [Whiff] -> Whiff
Todo [Char]
"calldatalength < 256" []))
      Just (Text
name, [AbiType]
typs) -> do ([SWord 8]
cd, 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 [Char]
"Trivial" []))
  Storage
symstore <- case StorageModel
storagemodel of
    StorageModel
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
    StorageModel
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 SBV (WordN 256)
0)
    StorageModel
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 [Char]
"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 ContractCode
x Storage
initStore StorageModel
model SAddr
addr SymWord
callvalue' (Buffer, SymWord)
calldata' =
  (VMOpts -> VM
makeVm (VMOpts -> VM) -> VMOpts -> VM
forall a b. (a -> b) -> a -> b
$ VMOpts :: Contract
-> (Buffer, SymWord)
-> SymWord
-> Addr
-> SAddr
-> Addr
-> W256
-> W256
-> W256
-> SymWord
-> Addr
-> W256
-> W256
-> W256
-> W256
-> FeeSchedule Integer
-> W256
-> Bool
-> StorageModel
-> Map Addr [W256]
-> Bool
-> 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 W256
1
    , vmoptCaller :: SAddr
vmoptCaller = SAddr
addr
    , vmoptOrigin :: Addr
vmoptOrigin = Addr
ethrunAddress --todo: generalize
    , vmoptCoinbase :: Addr
vmoptCoinbase = Addr
0
    , vmoptNumber :: W256
vmoptNumber = W256
0
    , vmoptTimestamp :: SymWord
vmoptTimestamp = SymWord
0
    , vmoptBlockGaslimit :: W256
vmoptBlockGaslimit = W256
0
    , vmoptGasprice :: W256
vmoptGasprice = W256
0
    , vmoptDifficulty :: W256
vmoptDifficulty = W256
0
    , vmoptGas :: W256
vmoptGas = W256
0xffffffffffffffff
    , vmoptGaslimit :: W256
vmoptGaslimit = W256
0xffffffffffffffff
    , vmoptMaxCodeSize :: W256
vmoptMaxCodeSize = W256
0xffffffff
    , vmoptSchedule :: FeeSchedule Integer
vmoptSchedule = FeeSchedule Integer
forall n. Num n => FeeSchedule n
FeeSchedule.berlin
    , vmoptChainId :: W256
vmoptChainId = W256
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
    , vmoptAllowFFI :: Bool
vmoptAllowFFI = Bool
False
    }) 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 W256
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 Maybe Integer
maxIter VM
vm = let
      f :: (VM, [Tree BranchInfo]) -> Tree BranchInfo
f (VM
vm', [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
== Int
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 Maybe Integer
maxIter VM
vm = let
  cont :: State VM () -> QueryT IO (VM, [Tree BranchInfo])
cont 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

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

    Just (VMFailure (EVM.Query q :: Query
q@(PleaseAskSMT SBool
_ [SBool]
_ 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 Int
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 Integer
0 Maybe Integer
maxIter) Integer
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 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 Bool -> State VM ()
continue)))
      -> case VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
vm Maybe Integer
maxIter of
        Maybe Bool
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 Int
1
            (VM
leftvm, [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 Int
1
            Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
1
            (VM
rightvm, [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 Int
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 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 VMResult
_
      -> (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 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 a
x) =
      [a] -> StateT VM Query [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a
x]

    eval (Action b
action Operational.:>>= b -> ProgramT Action Identity a
k) =
      case Action b
action of
        Action b
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
        Action b
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.IOAct StateT VM IO b
q ->
          (IO (b, VM) -> Query (b, VM))
-> StateT VM IO b -> StateT VM Query b
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
mapStateT IO (b, VM) -> Query (b, VM)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io StateT VM IO b
q 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
        Stepper.Ask (EVM.PleaseChoosePath Whiff
_ 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
            Maybe Bool
Nothing -> do
              Int -> StateT VM Query ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
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 Int
1
              Int -> StateT VM Query ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
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 Int
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 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 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 SBool
_ [SBool]
_ 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 Int
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 Integer
0 Maybe Integer
maxIter) Integer
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

            Query
_ -> StateT VM Query [a]
performQuery

        Stepper.EVM 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 VM
_ Maybe Integer
Nothing = Maybe Bool
forall a. Maybe a
Nothing
maxIterationsReached VM
vm (Just 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 Int
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
- Int
1)) VM
vm
     else Maybe Bool
forall a. Maybe a
Nothing

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

checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
checkAssert :: [Word256]
-> ByteString
-> Maybe (Text, [AbiType])
-> [[Char]]
-> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
checkAssert [Word256]
errs ByteString
c Maybe (Text, [AbiType])
signature' [[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 -> Maybe Postcondition)
-> Postcondition -> Maybe Postcondition
forall a b. (a -> b) -> a -> b
$ [Word256] -> Postcondition
checkAssertions [Word256]
errs)

{- |Checks if an assertion violation has been encountered

  hevm recognises the following as an assertion violation:

  1. the invalid opcode (0xfe) (solc < 0.8)
  2. a revert with a reason of the form `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of the following (solc >= 0.8):
    - 0x00: Used for generic compiler inserted panics.
    - 0x01: If you call assert with an argument that evaluates to false.
    - 0x11: If an arithmetic operation results in underflow or overflow outside of an unchecked { ... } block.
    - 0x12; If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0).
    - 0x21: If you convert a value that is too big or negative into an enum type.
    - 0x22: If you access a storage byte array that is incorrectly encoded.
    - 0x31: If you call .pop() on an empty array.
    - 0x32: If you access an array, bytesN or an array slice at an out-of-bounds or negative index (i.e. x[i] where i >= x.length or i < 0).
    - 0x41: If you allocate too much memory or create an array that is too large.
    - 0x51: If you call a zero-initialized variable of internal function type.

  see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require
-}
checkAssertions :: [Word256] -> Postcondition
checkAssertions :: [Word256] -> Postcondition
checkAssertions [Word256]
errs (VM
_, 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 Word8
254)) -> SBool
sFalse
  Just (EVM.VMFailure (EVM.Revert ByteString
msg)) -> if ByteString
msg ByteString -> [ByteString] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Word256 -> ByteString) -> [Word256] -> [ByteString]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word256 -> ByteString
panicMsg [Word256]
errs) then SBool
sFalse else SBool
sTrue
  Maybe VMResult
_ -> SBool
sTrue

-- |By default hevm checks for all assertions except those which result from arithmetic overflow
defaultPanicCodes :: [Word256]
defaultPanicCodes :: [Word256]
defaultPanicCodes = [ Word256
0x00, Word256
0x01, Word256
0x12, Word256
0x21, Word256
0x22, Word256
0x31, Word256
0x32, Word256
0x41, Word256
0x51 ]

allPanicCodes :: [Word256]
allPanicCodes :: [Word256]
allPanicCodes = [ Word256
0x00, Word256
0x01, Word256
0x11, Word256
0x12, Word256
0x21, Word256
0x22, Word256
0x31, Word256
0x32, Word256
0x41, Word256
0x51 ]

-- |Produces the revert message for solc >=0.8 assertion violations
panicMsg :: Word256 -> ByteString
panicMsg :: Word256 -> ByteString
panicMsg Word256
err = (Text -> ByteString
selector Text
"Panic(uint256)") ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> (AbiValue -> ByteString
encodeAbiValue (AbiValue -> ByteString) -> AbiValue -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> Word256 -> AbiValue
AbiUInt Int
256 Word256
err)

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 ByteString
theCode Maybe (Text, [AbiType])
signature' [[Char]]
concreteArgs StorageModel
storagemodel Precondition
pre 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 [Char]
"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 -> 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 Error
DeadPath) -> Bool
False
    Maybe VMResult
_ -> Bool
True

consistentPath :: VM -> Query (Maybe VM)
consistentPath :: VM -> Query (Maybe VM)
consistentPath 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
    CheckSatResult
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
    CheckSatResult
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
    CheckSatResult
Unsat -> Maybe VM -> Query (Maybe VM)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe VM
forall a. Maybe a
Nothing
    DSat Maybe [Char]
_ -> [Char] -> Query (Maybe VM)
forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected DSAT"

consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo))
consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo))
consistentTree (Node (BranchInfo VM
vm 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
    Maybe VM
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' -> 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 BranchInfo
b [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 BranchInfo
x []) = [BranchInfo -> VM
_vm BranchInfo
x]
leaves (Node BranchInfo
_ [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 VM
preState Maybe Integer
maxIter Maybe (BlockNumber, Text)
rpcinfo 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 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 (\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 [Char]
"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
        CheckSatResult
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 [Char]
"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
        CheckSatResult
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 [Char]
"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
        CheckSatResult
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 Maybe [Char]
_ -> [Char] -> Query (Either (Tree BranchInfo) (Tree BranchInfo))
forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected DSAT"

    Maybe Postcondition
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 [Char]
"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 ByteString
bytecodeA ByteString
bytecodeB Maybe Integer
maxiter Maybe (Text, [AbiType])
signature' = do
  let
    bytecodeA' :: ByteString
bytecodeA' = if ByteString -> Bool
BS.null ByteString
bytecodeA then [Word8] -> ByteString
BS.pack [Word8
0] else ByteString
bytecodeA
    bytecodeB' :: ByteString
bytecodeB' = if ByteString -> Bool
BS.null ByteString
bytecodeB then [Word8] -> ByteString
BS.pack [Word8
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
      (Buffer
calldata', 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 Int
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 Int
1
  Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
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 Int
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 VM
a VM
b =
        let ([(SBool, Whiff)]
aPath, [(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)
            (Addr
aSelf, 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)
            (Map Addr Contract
aEnv, 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)
            (Maybe VMResult
aResult, 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 [(SymWord, SymWord)]
_ SArray (WordN 256) (WordN 256)
aStorage, Symbolic [(SymWord, SymWord)]
_ 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 Buffer
aOut), Just (VMSuccess 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 Error
UnexpectedSymbolicArg), Maybe VMResult
_) ->
                [Char] -> SBool
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBool) -> [Char] -> SBool
forall a b. (a -> b) -> a -> b
$ [Char]
"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 [Char]
"??" 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
<> [Char]
". Not supported (yet!)"

              (Maybe VMResult
_, Just (VMFailure Error
UnexpectedSymbolicArg)) ->
                [Char] -> SBool
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBool) -> [Char] -> SBool
forall a b. (a -> b) -> a -> b
$ [Char]
"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 [Char]
"??" 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
<> [Char]
". Not supported (yet!)"

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

              (Just VMResult
_, Just VMResult
_) -> SBool
sTrue

              (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
     CheckSatResult
Unk -> [Char] -> Query (Either ([VM], [VM]) VM)
forall a. HasCallStack => [Char] -> a
error [Char]
"solver said unknown!"
     CheckSatResult
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
     CheckSatResult
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 Maybe [Char]
_ -> [Char] -> Query (Either ([VM], [VM]) VM)
forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected DSAT"

both' :: (a -> b) -> (a, a) -> (b, b)
both' :: (a -> b) -> (a, a) -> (b, b)
both' a -> b
f (a
x, 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 Maybe (Text, [AbiType])
maybesig = do
  let (Buffer
calldata', S Whiff
_ 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 Whiff
_ 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 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 [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 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 [Char]
"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 (Text
name, [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
"(" 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 Int
4 ByteString
calldatainput))
      Maybe (Text, [AbiType])
Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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