{-# Language TupleSections #-}
{-# Language DeriveAnyClass #-}
{-# Language DataKinds #-}

module EVM.SymExec where

import Prelude hiding (Word)

import Data.Tuple (swap)
import Optics.Core
import EVM hiding (push, bytecode, query, wrap)
import EVM.Exec
import qualified EVM.Fetch as Fetch
import EVM.ABI
import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)
import qualified EVM.SMT as SMT
import EVM.Solvers
import EVM.Traversals
import qualified EVM.Expr as Expr
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 EVM.Types
import EVM.Concrete (createAddress)
import qualified EVM.FeeSchedule as FeeSchedule
import Data.DoubleWord (Word256)
import Control.Concurrent.Async
import Data.Maybe
import Data.Containers.ListUtils
import Data.List (foldl', sortBy)
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import Data.Bifunctor (second)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Text as T
import qualified Data.Text.IO as T
import qualified Data.Text.Lazy as TL
import qualified Data.Text.Lazy.IO as TL
import EVM.Format (formatExpr, formatPartial)
import Data.Set (Set, isSubsetOf, size)
import qualified Data.Set as Set
import Control.Concurrent.Spawn (parMapIO, pool)
import Control.Concurrent.STM (atomically, TVar, readTVarIO, readTVar, newTVarIO, writeTVar)
import GHC.Conc (getNumProcessors)
import EVM.Format (indent, formatBinary)
import Options.Generic as Options


-- | A method name, and the (ordered) types of it's arguments
data Sig = Sig Text [AbiType]

data LoopHeuristic
  = Naive
  | StackBased
  deriving (LoopHeuristic -> LoopHeuristic -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LoopHeuristic -> LoopHeuristic -> Bool
$c/= :: LoopHeuristic -> LoopHeuristic -> Bool
== :: LoopHeuristic -> LoopHeuristic -> Bool
$c== :: LoopHeuristic -> LoopHeuristic -> Bool
Eq, Int -> LoopHeuristic -> ShowS
[LoopHeuristic] -> ShowS
LoopHeuristic -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LoopHeuristic] -> ShowS
$cshowList :: [LoopHeuristic] -> ShowS
show :: LoopHeuristic -> String
$cshow :: LoopHeuristic -> String
showsPrec :: Int -> LoopHeuristic -> ShowS
$cshowsPrec :: Int -> LoopHeuristic -> ShowS
Show, ReadPrec [LoopHeuristic]
ReadPrec LoopHeuristic
Int -> ReadS LoopHeuristic
ReadS [LoopHeuristic]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [LoopHeuristic]
$creadListPrec :: ReadPrec [LoopHeuristic]
readPrec :: ReadPrec LoopHeuristic
$creadPrec :: ReadPrec LoopHeuristic
readList :: ReadS [LoopHeuristic]
$creadList :: ReadS [LoopHeuristic]
readsPrec :: Int -> ReadS LoopHeuristic
$creadsPrec :: Int -> ReadS LoopHeuristic
Read, ReadM LoopHeuristic
Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser [LoopHeuristic]
Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
forall a.
(Maybe Text
 -> Maybe Text -> Maybe Char -> Maybe String -> Parser a)
-> (Maybe Text
    -> Maybe Text -> Maybe Char -> Maybe String -> Parser [a])
-> ReadM a
-> (forall (proxy :: * -> *). proxy a -> String)
-> ParseField a
forall (proxy :: * -> *). proxy LoopHeuristic -> String
metavar :: forall (proxy :: * -> *). proxy LoopHeuristic -> String
$cmetavar :: forall (proxy :: * -> *). proxy LoopHeuristic -> String
readField :: ReadM LoopHeuristic
$creadField :: ReadM LoopHeuristic
parseListOfField :: Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser [LoopHeuristic]
$cparseListOfField :: Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser [LoopHeuristic]
parseField :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
$cparseField :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
ParseField, ParseRecord LoopHeuristic
Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
forall a.
ParseRecord a
-> (Maybe Text
    -> Maybe Text -> Maybe Char -> Maybe String -> Parser a)
-> ParseFields a
parseFields :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
$cparseFields :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
ParseFields, Parser LoopHeuristic
forall a. Parser a -> ParseRecord a
parseRecord :: Parser LoopHeuristic
$cparseRecord :: Parser LoopHeuristic
ParseRecord, forall x. Rep LoopHeuristic x -> LoopHeuristic
forall x. LoopHeuristic -> Rep LoopHeuristic x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LoopHeuristic x -> LoopHeuristic
$cfrom :: forall x. LoopHeuristic -> Rep LoopHeuristic x
Generic)

data ProofResult a b c = Qed a | Cex b | Timeout c
  deriving (Int -> ProofResult a b c -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b c.
(Show a, Show b, Show c) =>
Int -> ProofResult a b c -> ShowS
forall a b c.
(Show a, Show b, Show c) =>
[ProofResult a b c] -> ShowS
forall a b c.
(Show a, Show b, Show c) =>
ProofResult a b c -> String
showList :: [ProofResult a b c] -> ShowS
$cshowList :: forall a b c.
(Show a, Show b, Show c) =>
[ProofResult a b c] -> ShowS
show :: ProofResult a b c -> String
$cshow :: forall a b c.
(Show a, Show b, Show c) =>
ProofResult a b c -> String
showsPrec :: Int -> ProofResult a b c -> ShowS
$cshowsPrec :: forall a b c.
(Show a, Show b, Show c) =>
Int -> ProofResult a b c -> ShowS
Show, ProofResult a b c -> ProofResult a b c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b c.
(Eq a, Eq b, Eq c) =>
ProofResult a b c -> ProofResult a b c -> Bool
/= :: ProofResult a b c -> ProofResult a b c -> Bool
$c/= :: forall a b c.
(Eq a, Eq b, Eq c) =>
ProofResult a b c -> ProofResult a b c -> Bool
== :: ProofResult a b c -> ProofResult a b c -> Bool
$c== :: forall a b c.
(Eq a, Eq b, Eq c) =>
ProofResult a b c -> ProofResult a b c -> Bool
Eq)
type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)
type EquivResult = ProofResult () (SMTCex) ()

isTimeout :: ProofResult a b c -> Bool
isTimeout :: forall a b c. ProofResult a b c -> Bool
isTimeout (Timeout c
_) = Bool
True
isTimeout ProofResult a b c
_ = Bool
False

isCex :: ProofResult a b c -> Bool
isCex :: forall a b c. ProofResult a b c -> Bool
isCex (Cex b
_) = Bool
True
isCex ProofResult a b c
_ = Bool
False

isQed :: ProofResult a b c -> Bool
isQed :: forall a b c. ProofResult a b c -> Bool
isQed (Qed a
_) = Bool
True
isQed ProofResult a b c
_ = Bool
False

data VeriOpts = VeriOpts
  { VeriOpts -> Bool
simp :: Bool
  , VeriOpts -> Bool
debug :: Bool
  , VeriOpts -> Maybe Integer
maxIter :: Maybe Integer
  , VeriOpts -> Integer
askSmtIters :: Integer
  , VeriOpts -> LoopHeuristic
loopHeuristic :: LoopHeuristic
  , VeriOpts -> RpcInfo
rpcInfo :: Fetch.RpcInfo
  }
  deriving (VeriOpts -> VeriOpts -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VeriOpts -> VeriOpts -> Bool
$c/= :: VeriOpts -> VeriOpts -> Bool
== :: VeriOpts -> VeriOpts -> Bool
$c== :: VeriOpts -> VeriOpts -> Bool
Eq, Int -> VeriOpts -> ShowS
[VeriOpts] -> ShowS
VeriOpts -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VeriOpts] -> ShowS
$cshowList :: [VeriOpts] -> ShowS
show :: VeriOpts -> String
$cshow :: VeriOpts -> String
showsPrec :: Int -> VeriOpts -> ShowS
$cshowsPrec :: Int -> VeriOpts -> ShowS
Show)

defaultVeriOpts :: VeriOpts
defaultVeriOpts :: VeriOpts
defaultVeriOpts = VeriOpts
  { $sel:simp:VeriOpts :: Bool
simp = Bool
True
  , $sel:debug:VeriOpts :: Bool
debug = Bool
False
  , $sel:maxIter:VeriOpts :: Maybe Integer
maxIter = forall a. Maybe a
Nothing
  , $sel:askSmtIters:VeriOpts :: Integer
askSmtIters = Integer
1
  , $sel:loopHeuristic:VeriOpts :: LoopHeuristic
loopHeuristic = LoopHeuristic
StackBased
  , $sel:rpcInfo:VeriOpts :: RpcInfo
rpcInfo = forall a. Maybe a
Nothing
  }

rpcVeriOpts :: (Fetch.BlockNumber, Text) -> VeriOpts
rpcVeriOpts :: (BlockNumber, Text) -> VeriOpts
rpcVeriOpts (BlockNumber, Text)
info = VeriOpts
defaultVeriOpts { $sel:rpcInfo:VeriOpts :: RpcInfo
rpcInfo = forall a. a -> Maybe a
Just (BlockNumber, Text)
info }

debugVeriOpts :: VeriOpts
debugVeriOpts :: VeriOpts
debugVeriOpts = VeriOpts
defaultVeriOpts { $sel:debug:VeriOpts :: Bool
debug = Bool
True }

extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
extractCex :: VerifyResult -> Maybe (Expr 'End, SMTCex)
extractCex (Cex (Expr 'End, SMTCex)
c) = forall a. a -> Maybe a
Just (Expr 'End, SMTCex)
c
extractCex VerifyResult
_ = forall a. Maybe a
Nothing

inRange :: Int -> Expr EWord -> Prop
inRange :: Int -> Expr 'EWord -> Prop
inRange Int
sz Expr 'EWord
e = Prop -> Prop -> Prop
PAnd (Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit W256
0)) (Expr 'EWord -> Expr 'EWord -> Prop
PLEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ W256
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz forall a. Num a => a -> a -> a
- W256
1))

bool :: Expr EWord -> Prop
bool :: Expr 'EWord -> Prop
bool Expr 'EWord
e = Prop -> Prop -> Prop
POr (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit W256
1)) (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit W256
0))

-- | Abstract calldata argument generation
symAbiArg :: Text -> AbiType -> CalldataFragment
symAbiArg :: Text -> AbiType -> CalldataFragment
symAbiArg Text
name = \case
  AbiUIntType Int
n ->
    if Int
n forall a. Integral a => a -> a -> a
`mod` Int
8 forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
<= Int
256
    then let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Int -> Expr 'EWord -> Prop
inRange Int
n Expr 'EWord
v] Expr 'EWord
v
    else forall a. HasCallStack => String -> a
error String
"bad type"
  AbiIntType Int
n ->
    if Int
n forall a. Integral a => a -> a -> a
`mod` Int
8 forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
<= Int
256
    -- TODO: is this correct?
    then let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Int -> Expr 'EWord -> Prop
inRange Int
n Expr 'EWord
v] Expr 'EWord
v
    else forall a. HasCallStack => String -> a
error String
"bad type"
  AbiType
AbiBoolType -> let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Expr 'EWord -> Prop
bool Expr 'EWord
v] Expr 'EWord
v
  AbiType
AbiAddressType -> let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Int -> Expr 'EWord -> Prop
inRange Int
160 Expr 'EWord
v] Expr 'EWord
v
  AbiBytesType Int
n ->
    if Int
n forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
<= Int
32
    then let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Int -> Expr 'EWord -> Prop
inRange (Int
n forall a. Num a => a -> a -> a
* Int
8) Expr 'EWord
v] Expr 'EWord
v
    else forall a. HasCallStack => String -> a
error String
"bad type"
  AbiArrayType Int
sz AbiType
tp ->
    [CalldataFragment] -> CalldataFragment
Comp forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Text
n -> Text -> AbiType -> CalldataFragment
symAbiArg (Text
name forall a. Semigroup a => a -> a -> a
<> Text
n) AbiType
tp) [String -> Text
T.pack (forall a. Show a => a -> String
show Int
n) | Int
n <- [Int
0..Int
szforall a. Num a => a -> a -> a
-Int
1]]
  AbiType
t -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"TODO: symbolic abi encoding for " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show AbiType
t

data CalldataFragment
  = St [Prop] (Expr EWord)
  | Dy [Prop] (Expr EWord) (Expr Buf)
  | Comp [CalldataFragment]
  deriving (Int -> CalldataFragment -> ShowS
[CalldataFragment] -> ShowS
CalldataFragment -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CalldataFragment] -> ShowS
$cshowList :: [CalldataFragment] -> ShowS
show :: CalldataFragment -> String
$cshow :: CalldataFragment -> String
showsPrec :: Int -> CalldataFragment -> ShowS
$cshowsPrec :: Int -> CalldataFragment -> ShowS
Show, CalldataFragment -> CalldataFragment -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CalldataFragment -> CalldataFragment -> Bool
$c/= :: CalldataFragment -> CalldataFragment -> Bool
== :: CalldataFragment -> CalldataFragment -> Bool
$c== :: CalldataFragment -> CalldataFragment -> Bool
Eq)

-- | 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] -> Expr Buf -> (Expr Buf, [Prop])
symCalldata :: Text -> [AbiType] -> [String] -> Expr 'Buf -> (Expr 'Buf, [Prop])
symCalldata Text
sig [AbiType]
typesignature [String]
concreteArgs Expr 'Buf
base =
  let
    args :: [String]
args = [String]
concreteArgs forall a. Semigroup a => a -> a -> a
<> forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbiType]
typesignature forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
concreteArgs) String
"<symbolic>"
    mkArg :: AbiType -> String -> Int -> CalldataFragment
    mkArg :: AbiType -> String -> Int -> CalldataFragment
mkArg AbiType
typ String
"<symbolic>" Int
n = Text -> AbiType -> CalldataFragment
symAbiArg (String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ String
"arg" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Int
n) AbiType
typ
    mkArg AbiType
typ String
arg Int
_ =
      case AbiType -> String -> AbiValue
makeAbiValue AbiType
typ String
arg of
        AbiUInt Int
_ Word256
w -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ Word256
w
        AbiInt Int
_ Int256
w -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ Int256
w
        AbiAddress Addr
w -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ Addr
w
        AbiBool Bool
w -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ if Bool
w then W256
1 else W256
0
        AbiValue
_ -> forall a. HasCallStack => String -> a
error String
"TODO"
    calldatas :: [CalldataFragment]
calldatas = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 AbiType -> String -> Int -> CalldataFragment
mkArg [AbiType]
typesignature [String]
args [Int
1..]
    (Expr 'Buf
cdBuf, [Prop]
props) = [CalldataFragment] -> Expr 'Buf -> (Expr 'Buf, [Prop])
combineFragments [CalldataFragment]
calldatas Expr 'Buf
base
    withSelector :: Expr 'Buf
withSelector = Expr 'Buf -> Text -> Expr 'Buf
writeSelector Expr 'Buf
cdBuf Text
sig
    sizeConstraints :: Prop
sizeConstraints
      = (Expr 'Buf -> Expr 'EWord
Expr.bufLength Expr 'Buf
withSelector Expr 'EWord -> Expr 'EWord -> Prop
.>= [CalldataFragment] -> Expr 'EWord
cdLen [CalldataFragment]
calldatas)
      Prop -> Prop -> Prop
.&& (Expr 'Buf -> Expr 'EWord
Expr.bufLength Expr 'Buf
withSelector Expr 'EWord -> Expr 'EWord -> Prop
.< (W256 -> Expr 'EWord
Lit (W256
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
64 :: Integer))))
  in (Expr 'Buf
withSelector, Prop
sizeConstraints forall a. a -> [a] -> [a]
: [Prop]
props)

cdLen :: [CalldataFragment] -> Expr EWord
cdLen :: [CalldataFragment] -> Expr 'EWord
cdLen = Expr 'EWord -> [CalldataFragment] -> Expr 'EWord
go (W256 -> Expr 'EWord
Lit W256
4)
  where
    go :: Expr 'EWord -> [CalldataFragment] -> Expr 'EWord
go Expr 'EWord
acc = \case
      [] -> Expr 'EWord
acc
      (CalldataFragment
hd:[CalldataFragment]
tl) -> case CalldataFragment
hd of
                   St [Prop]
_ Expr 'EWord
_ -> Expr 'EWord -> [CalldataFragment] -> Expr 'EWord
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
acc (W256 -> Expr 'EWord
Lit W256
32)) [CalldataFragment]
tl
                   CalldataFragment
_ -> forall a. HasCallStack => String -> a
error String
"unsupported"

writeSelector :: Expr Buf -> Text -> Expr Buf
writeSelector :: Expr 'Buf -> Text -> Expr 'Buf
writeSelector Expr 'Buf
buf Text
sig =
  Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeSel (W256 -> Expr 'EWord
Lit W256
0) forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeSel (W256 -> Expr 'EWord
Lit W256
1) forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeSel (W256 -> Expr 'EWord
Lit W256
2) forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeSel (W256 -> Expr 'EWord
Lit W256
3) Expr 'Buf
buf
  where
    sel :: Expr 'Buf
sel = ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Text -> ByteString
selector Text
sig
    writeSel :: Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeSel Expr 'EWord
idx = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
Expr.writeByte Expr 'EWord
idx (Expr 'EWord -> Expr 'Buf -> Expr 'Byte
Expr.readByte Expr 'EWord
idx Expr 'Buf
sel)

combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop])
combineFragments :: [CalldataFragment] -> Expr 'Buf -> (Expr 'Buf, [Prop])
combineFragments [CalldataFragment]
fragments Expr 'Buf
base = Expr 'EWord
-> [CalldataFragment] -> (Expr 'Buf, [Prop]) -> (Expr 'Buf, [Prop])
go (W256 -> Expr 'EWord
Lit W256
4) [CalldataFragment]
fragments (Expr 'Buf
base, [])
  where
    go :: Expr EWord -> [CalldataFragment] -> (Expr Buf, [Prop]) -> (Expr Buf, [Prop])
    go :: Expr 'EWord
-> [CalldataFragment] -> (Expr 'Buf, [Prop]) -> (Expr 'Buf, [Prop])
go Expr 'EWord
_ [] (Expr 'Buf, [Prop])
acc = (Expr 'Buf, [Prop])
acc
    go Expr 'EWord
idx (CalldataFragment
f:[CalldataFragment]
rest) (Expr 'Buf
buf, [Prop]
ps) =
      case CalldataFragment
f of
        St [Prop]
p Expr 'EWord
w -> Expr 'EWord
-> [CalldataFragment] -> (Expr 'Buf, [Prop]) -> (Expr 'Buf, [Prop])
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
idx (W256 -> Expr 'EWord
Lit W256
32)) [CalldataFragment]
rest (Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
Expr.writeWord Expr 'EWord
idx Expr 'EWord
w Expr 'Buf
buf, [Prop]
p forall a. Semigroup a => a -> a -> a
<> [Prop]
ps)
        CalldataFragment
s -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"unsupported cd fragment: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show CalldataFragment
s


abstractVM
  :: (Expr Buf, [Prop])
  -> ByteString
  -> Maybe Precondition
  -> Expr Storage
  -> VM
abstractVM :: (Expr 'Buf, [Prop])
-> ByteString -> Maybe Precondition -> Expr 'Storage -> VM
abstractVM (Expr 'Buf, [Prop])
cd ByteString
contractCode Maybe Precondition
maybepre Expr 'Storage
store = VM
finalVm
  where
    caller' :: Expr 'EWord
caller' = Int -> Expr 'EWord
Caller Int
0
    value' :: Expr 'EWord
value' = Int -> Expr 'EWord
CallValue Int
0
    code' :: ContractCode
code' = RuntimeCode -> ContractCode
RuntimeCode (ByteString -> RuntimeCode
ConcreteRuntimeCode ByteString
contractCode)
    vm' :: VM
vm' = ContractCode
-> Expr 'Storage
-> Expr 'EWord
-> Expr 'EWord
-> (Expr 'Buf, [Prop])
-> VM
loadSymVM ContractCode
code' Expr 'Storage
store Expr 'EWord
caller' Expr 'EWord
value' (Expr 'Buf, [Prop])
cd
    precond :: [Prop]
precond = case Maybe Precondition
maybepre of
                Maybe Precondition
Nothing -> []
                Just Precondition
p -> [Precondition
p VM
vm']
    finalVm :: VM
finalVm = VM
vm' forall a b. a -> (a -> b) -> b
& forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over forall a. IsLabel "constraints" a => a
#constraints (forall a. Semigroup a => a -> a -> a
<> [Prop]
precond)

loadSymVM
  :: ContractCode
  -> Expr Storage
  -> Expr EWord
  -> Expr EWord
  -> (Expr Buf, [Prop])
  -> VM
loadSymVM :: ContractCode
-> Expr 'Storage
-> Expr 'EWord
-> Expr 'EWord
-> (Expr 'Buf, [Prop])
-> VM
loadSymVM ContractCode
x Expr 'Storage
initStore Expr 'EWord
addr Expr 'EWord
callvalue' (Expr 'Buf, [Prop])
cd =
  (VMOpts -> VM
makeVm forall a b. (a -> b) -> a -> b
$ VMOpts
    { $sel:contract:VMOpts :: Contract
contract = ContractCode -> Contract
initialContract ContractCode
x
    , $sel:calldata:VMOpts :: (Expr 'Buf, [Prop])
calldata = (Expr 'Buf, [Prop])
cd
    , $sel:value:VMOpts :: Expr 'EWord
value = Expr 'EWord
callvalue'
    , $sel:initialStorage:VMOpts :: Expr 'Storage
initialStorage = Expr 'Storage
initStore
    , $sel:address:VMOpts :: Addr
address = Addr -> W256 -> Addr
createAddress Addr
ethrunAddress W256
1
    , $sel:caller:VMOpts :: Expr 'EWord
caller = Expr 'EWord
addr
    , $sel:origin:VMOpts :: Addr
origin = Addr
ethrunAddress --todo: generalize
    , $sel:coinbase:VMOpts :: Addr
coinbase = Addr
0
    , $sel:number:VMOpts :: W256
number = W256
0
    , $sel:timestamp:VMOpts :: Expr 'EWord
timestamp = W256 -> Expr 'EWord
Lit W256
0
    , $sel:blockGaslimit:VMOpts :: Word64
blockGaslimit = Word64
0
    , $sel:gasprice:VMOpts :: W256
gasprice = W256
0
    , $sel:prevRandao:VMOpts :: W256
prevRandao = W256
42069
    , $sel:gas:VMOpts :: Word64
gas = Word64
0xffffffffffffffff
    , $sel:gaslimit:VMOpts :: Word64
gaslimit = Word64
0xffffffffffffffff
    , $sel:baseFee:VMOpts :: W256
baseFee = W256
0
    , $sel:priorityFee:VMOpts :: W256
priorityFee = W256
0
    , $sel:maxCodeSize:VMOpts :: W256
maxCodeSize = W256
0xffffffff
    , $sel:schedule:VMOpts :: FeeSchedule Word64
schedule = forall n. Num n => FeeSchedule n
FeeSchedule.berlin
    , $sel:chainId:VMOpts :: W256
chainId = W256
1
    , $sel:create:VMOpts :: Bool
create = Bool
False
    , $sel:txAccessList:VMOpts :: Map Addr [W256]
txAccessList = forall a. Monoid a => a
mempty
    , $sel:allowFFI:VMOpts :: Bool
allowFFI = Bool
False
    }) forall a b. a -> (a -> b) -> b
& forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set (forall a. IsLabel "env" a => a
#env forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% forall a. IsLabel "contracts" a => a
#contracts forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (Addr -> W256 -> Addr
createAddress Addr
ethrunAddress W256
1))
             (forall a. a -> Maybe a
Just (ContractCode -> Contract
initialContract ContractCode
x))

-- | Interpreter which explores all paths at branching points. Returns an
-- 'Expr End' representing the possible executions.
interpret
  :: Fetch.Fetcher
  -> Maybe Integer -- max iterations
  -> Integer -- ask smt iterations
  -> LoopHeuristic
  -> VM
  -> Stepper (Expr End)
  -> IO (Expr End)
interpret :: Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm =
  ProgramView Action (Expr 'End) -> IO (Expr 'End)
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
Operational.view
  where
  eval
    :: Operational.ProgramView Stepper.Action (Expr End)
    -> IO (Expr End)

  eval :: ProgramView Action (Expr 'End) -> IO (Expr 'End)
eval (Operational.Return Expr 'End
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr 'End
x

  eval (Action b
action Operational.:>>= b -> Stepper (Expr 'End)
k) =
    case Action b
action of
      Action b
Stepper.Exec -> do
        let (VMResult
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState State VM VMResult
exec VM
vm
        Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k VMResult
r)
      Action b
Stepper.Run -> do
        let vm' :: VM
vm' = forall s a. State s a -> s -> s
execState State VM VMResult
exec VM
vm
        Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k VM
vm')
      Stepper.IOAct StateT VM IO b
q -> do
        (b
r, VM
vm') <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT VM IO b
q VM
vm
        Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k b
r)
      Stepper.Ask (PleaseChoosePath Expr 'EWord
cond Bool -> EVM ()
continue) -> do
        (Expr 'End
a, Expr 'End
b) <- forall a b. IO a -> IO b -> IO (a, b)
concurrently
          (let (()
ra, VM
vma) = forall s a. State s a -> s -> (a, s)
runState (Bool -> EVM ()
continue Bool
True) VM
vm { $sel:result:VM :: Maybe VMResult
result = forall a. Maybe a
Nothing }
           in Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vma (b -> Stepper (Expr 'End)
k ()
ra))
          (let (()
rb, VM
vmb) = forall s a. State s a -> s -> (a, s)
runState (Bool -> EVM ()
continue Bool
False) VM
vm { $sel:result:VM :: Maybe VMResult
result = forall a. Maybe a
Nothing }
           in Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vmb (b -> Stepper (Expr 'End)
k ()
rb))

        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE Expr 'EWord
cond Expr 'End
a Expr 'End
b
      Stepper.Wait Query
q -> do
        let performQuery :: IO (Expr 'End)
performQuery = do
              EVM ()
m <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Fetcher
fetcher Query
q)
              let (()
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState EVM ()
m VM
vm
              Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k ()
r)

        case Query
q of
          PleaseAskSMT Expr 'EWord
cond [Prop]
_ BranchCondition -> EVM ()
continue -> do
            case Expr 'EWord
cond of
              -- is the condition concrete?
              Lit W256
c ->
                -- have we reached max iterations, are we inside a loop?
                case (VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
vm Maybe Integer
maxIter, LoopHeuristic -> VM -> Maybe Bool
isLoopHead LoopHeuristic
heuristic VM
vm) of
                  -- Yes. return a partial leaf
                  (Just Bool
_, Just Bool
True) ->
                    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Prop] -> PartialExec -> Expr 'End
Partial VM
vm.keccakEqs forall a b. (a -> b) -> a -> b
$ Int -> Addr -> PartialExec
MaxIterationsReached VM
vm.state.pc VM
vm.state.contract
                  -- No. keep executing
                  (Maybe Bool, Maybe Bool)
_ ->
                    let (()
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState (BranchCondition -> EVM ()
continue (Bool -> BranchCondition
Case (W256
c forall a. Ord a => a -> a -> Bool
> W256
0))) VM
vm
                    in Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k ()
r)

              -- the condition is symbolic
              Expr 'EWord
_ ->
                -- are in we a loop, have we hit maxIters, have we hit askSmtIters?
                case (LoopHeuristic -> VM -> Maybe Bool
isLoopHead LoopHeuristic
heuristic VM
vm, VM -> Integer -> Bool
askSmtItersReached VM
vm Integer
askSmtIters, VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
vm Maybe Integer
maxIter) of
                  -- we're in a loop and maxIters has been reached
                  (Just Bool
True, Bool
_, Just Bool
n) -> do
                    -- continue execution down the opposite branch than the one that
                    -- got us to this point and return a partial leaf for the other side
                    let (()
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState (BranchCondition -> EVM ()
continue (Bool -> BranchCondition
Case forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
n)) VM
vm
                    Expr 'End
a <- Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k ()
r)
                    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE Expr 'EWord
cond Expr 'End
a ([Prop] -> PartialExec -> Expr 'End
Partial VM
vm.keccakEqs (Int -> Addr -> PartialExec
MaxIterationsReached VM
vm.state.pc VM
vm.state.contract))
                  -- we're in a loop and askSmtIters has been reached
                  (Just Bool
True, Bool
True, Maybe Bool
_) ->
                    -- ask the smt solver about the loop condition
                    IO (Expr 'End)
performQuery
                  -- otherwise just try both branches and don't ask the solver
                  (Maybe Bool, Bool, Maybe Bool)
_ ->
                    let (()
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState (BranchCondition -> EVM ()
continue BranchCondition
EVM.Types.Unknown) VM
vm
                    in Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k ()
r)

          Query
_ -> IO (Expr 'End)
performQuery

      Stepper.EVM EVM b
m -> do
        let (b
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState EVM b
m VM
vm
        Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM
vm' (b -> Stepper (Expr 'End)
k b
r)

maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
_ Maybe Integer
Nothing = forall a. Maybe a
Nothing
maxIterationsReached VM
vm (Just Integer
maxIter) =
  let codelocation :: CodeLocation
codelocation = VM -> CodeLocation
getCodeLocation VM
vm
      (Int
iters, [Expr 'EWord]
_) = forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
codelocation forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% forall a. Eq a => a -> Iso' (Maybe a) a
non (Int
0, [])) VM
vm.iterations
  in if forall a b. (Integral a, Num b) => a -> b
num Integer
maxIter forall a. Ord a => a -> a -> Bool
<= Int
iters
     then forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CodeLocation
codelocation, Int
iters forall a. Num a => a -> a -> a
- Int
1) VM
vm.cache.path
     else forall a. Maybe a
Nothing

askSmtItersReached :: VM -> Integer -> Bool
askSmtItersReached :: VM -> Integer -> Bool
askSmtItersReached VM
vm Integer
askSmtIters = let
    codelocation :: CodeLocation
codelocation = VM -> CodeLocation
getCodeLocation VM
vm
    (Int
iters, [Expr 'EWord]
_) = forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
codelocation forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% forall a. Eq a => a -> Iso' (Maybe a) a
non (Int
0, [])) VM
vm.iterations
  in Integer
askSmtIters forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
num Int
iters

{- | Loop head detection heuristic

 The main thing we wish to differentiate between, are actual loop heads, and branch points inside of internal functions that are called multiple times.

 One way to do this is to observe that for internal functions, the compiler must always store a stack item representing the location that it must jump back to. If we compare the stack at the time of the previous visit, and the time of the current visit, and notice that this location has changed, then we can guess that the location is a jump point within an internal function instead of a loop (where such locations should be constant between iterations).

 This heuristic is not perfect, and can certainly be tricked, but should generally be good enough for most compiler generated and non pathological user generated loops.
 -}
isLoopHead :: LoopHeuristic -> VM -> Maybe Bool
isLoopHead :: LoopHeuristic -> VM -> Maybe Bool
isLoopHead LoopHeuristic
Naive VM
_ = forall a. a -> Maybe a
Just Bool
True
isLoopHead LoopHeuristic
StackBased VM
vm = let
    loc :: CodeLocation
loc = VM -> CodeLocation
getCodeLocation VM
vm
    oldIters :: Maybe (Int, [Expr 'EWord])
oldIters = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CodeLocation
loc VM
vm.iterations
    isValid :: Expr 'EWord -> Bool
isValid (Lit W256
wrd) = W256
wrd forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
num (forall a. Bounded a => a
maxBound :: Int) Bool -> Bool -> Bool
&& VM -> Int -> Bool
isValidJumpDest VM
vm (forall a b. (Integral a, Num b) => a -> b
num W256
wrd)
    isValid Expr 'EWord
_ = Bool
False
  in case Maybe (Int, [Expr 'EWord])
oldIters of
       Just (Int
_, [Expr 'EWord]
oldStack) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter Expr 'EWord -> Bool
isValid [Expr 'EWord]
oldStack forall a. Eq a => a -> a -> Bool
== forall a. (a -> Bool) -> [a] -> [a]
filter Expr 'EWord -> Bool
isValid VM
vm.state.stack
       Maybe (Int, [Expr 'EWord])
Nothing -> forall a. Maybe a
Nothing

type Precondition = VM -> Prop
type Postcondition = VM -> Expr End -> Prop

checkAssert
  :: SolverGroup
  -> [Word256]
  -> ByteString
  -> Maybe Sig
  -> [String]
  -> VeriOpts
  -> IO (Expr End, [VerifyResult])
checkAssert :: SolverGroup
-> [Word256]
-> ByteString
-> Maybe Sig
-> [String]
-> VeriOpts
-> IO (Expr 'End, [VerifyResult])
checkAssert SolverGroup
solvers [Word256]
errs ByteString
c Maybe Sig
signature' [String]
concreteArgs VeriOpts
opts =
  SolverGroup
-> ByteString
-> Maybe Sig
-> [String]
-> VeriOpts
-> Expr 'Storage
-> Maybe Precondition
-> Maybe Postcondition
-> IO (Expr 'End, [VerifyResult])
verifyContract SolverGroup
solvers ByteString
c Maybe Sig
signature' [String]
concreteArgs VeriOpts
opts Expr 'Storage
AbstractStore forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just 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
_ = \case
  Failure [Prop]
_ (Revert (ConcreteBuf ByteString
msg)) -> Bool -> Prop
PBool forall a b. (a -> b) -> a -> b
$ ByteString
msg forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word256 -> ByteString
panicMsg [Word256]
errs)
  Failure [Prop]
_ (Revert Expr 'Buf
b) -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Prop -> Prop -> Prop
PAnd (Bool -> Prop
PBool Bool
True) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Prop -> Prop
PNeg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'Buf
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Expr 'Buf
ConcreteBuf forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word256 -> ByteString
panicMsg) [Word256]
errs)
  Expr 'End
_ -> Bool -> Prop
PBool Bool
True

-- | By default hevm only checks for user-defined assertions
defaultPanicCodes :: [Word256]
defaultPanicCodes :: [Word256]
defaultPanicCodes = [Word256
0x01]

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)" forall a. Semigroup a => a -> a -> a
<> AbiValue -> ByteString
encodeAbiValue (Int -> Word256 -> AbiValue
AbiUInt Int
256 Word256
err)

-- | Builds a buffer representing calldata from the provided method description
-- and concrete arguments
mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop])
mkCalldata :: Maybe Sig -> [String] -> (Expr 'Buf, [Prop])
mkCalldata Maybe Sig
Nothing [String]
_ =
  ( Text -> Expr 'Buf
AbstractBuf Text
"txdata"
  -- assert that the length of the calldata is never more than 2^64
  -- this is way larger than would ever be allowed by the gas limit
  -- and avoids spurious counterexamples during abi decoding
  -- TODO: can we encode calldata as an array with a smaller length?
  , [Expr 'Buf -> Expr 'EWord
Expr.bufLength (Text -> Expr 'Buf
AbstractBuf Text
"txdata") Expr 'EWord -> Expr 'EWord -> Prop
.< (W256 -> Expr 'EWord
Lit (W256
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
64 :: Integer)))]
  )
mkCalldata (Just (Sig Text
name [AbiType]
types)) [String]
args =
  Text -> [AbiType] -> [String] -> Expr 'Buf -> (Expr 'Buf, [Prop])
symCalldata Text
name [AbiType]
types [String]
args (Text -> Expr 'Buf
AbstractBuf Text
"txdata")

verifyContract
  :: SolverGroup
  -> ByteString
  -> Maybe Sig
  -> [String]
  -> VeriOpts
  -> Expr Storage
  -> Maybe Precondition
  -> Maybe Postcondition
  -> IO (Expr End, [VerifyResult])
verifyContract :: SolverGroup
-> ByteString
-> Maybe Sig
-> [String]
-> VeriOpts
-> Expr 'Storage
-> Maybe Precondition
-> Maybe Postcondition
-> IO (Expr 'End, [VerifyResult])
verifyContract SolverGroup
solvers ByteString
theCode Maybe Sig
signature' [String]
concreteArgs VeriOpts
opts Expr 'Storage
initStore Maybe Precondition
maybepre Maybe Postcondition
maybepost =
  let preState :: VM
preState = (Expr 'Buf, [Prop])
-> ByteString -> Maybe Precondition -> Expr 'Storage -> VM
abstractVM (Maybe Sig -> [String] -> (Expr 'Buf, [Prop])
mkCalldata Maybe Sig
signature' [String]
concreteArgs) ByteString
theCode Maybe Precondition
maybepre Expr 'Storage
initStore
  in SolverGroup
-> VeriOpts
-> VM
-> Maybe Postcondition
-> IO (Expr 'End, [VerifyResult])
verify SolverGroup
solvers VeriOpts
opts VM
preState Maybe Postcondition
maybepost

-- | Stepper that parses the result of Stepper.runFully into an Expr End
runExpr :: Stepper.Stepper (Expr End)
runExpr :: Stepper (Expr 'End)
runExpr = do
  VM
vm <- Stepper VM
Stepper.runFully
  let asserts :: [Prop]
asserts = VM
vm.keccakEqs forall a. Semigroup a => a -> a -> a
<> VM
vm.constraints
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case VM
vm.result of
    Just (VMSuccess Expr 'Buf
buf) -> [Prop] -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Success [Prop]
asserts Expr 'Buf
buf VM
vm.env.storage
    Just (VMFailure EvmError
e) -> [Prop] -> EvmError -> Expr 'End
Failure [Prop]
asserts EvmError
e
    Just (Unfinished PartialExec
p) -> [Prop] -> PartialExec -> Expr 'End
Partial [Prop]
asserts PartialExec
p
    Maybe VMResult
_ -> forall a. HasCallStack => String -> a
error String
"Internal Error: vm in intermediate state after call to runFully"

-- | Converts a given top level expr into a list of final states and the
-- associated path conditions for each state.
flattenExpr :: Expr End -> [Expr End]
flattenExpr :: Expr 'End -> [Expr 'End]
flattenExpr = [Prop] -> Expr 'End -> [Expr 'End]
go []
  where
    go :: [Prop] -> Expr End -> [Expr End]
    go :: [Prop] -> Expr 'End -> [Expr 'End]
go [Prop]
pcs = \case
      ITE Expr 'EWord
c Expr 'End
t Expr 'End
f -> [Prop] -> Expr 'End -> [Expr 'End]
go (Prop -> Prop
PNeg ((forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
c (W256 -> Expr 'EWord
Lit W256
0))) forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
t forall a. Semigroup a => a -> a -> a
<> [Prop] -> Expr 'End -> [Expr 'End]
go (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
c (W256 -> Expr 'EWord
Lit W256
0) forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
f
      Success [Prop]
ps Expr 'Buf
msg Expr 'Storage
store -> [[Prop] -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Success ([Prop]
ps forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) Expr 'Buf
msg Expr 'Storage
store]
      Failure [Prop]
ps EvmError
e -> [[Prop] -> EvmError -> Expr 'End
Failure ([Prop]
ps forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) EvmError
e]
      Partial [Prop]
ps PartialExec
p -> [[Prop] -> PartialExec -> Expr 'End
Partial ([Prop]
ps forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) PartialExec
p]
      GVar GVar 'End
_ -> forall a. HasCallStack => String -> a
error String
"cannot flatten an Expr containing a GVar"

-- | Strips unreachable branches from a given expr
-- Returns a list of executed SMT queries alongside the reduced expression for debugging purposes
-- Note that the reduced expression loses information relative to the original
-- one if jump conditions are removed. This restriction can be removed once
-- Expr supports attaching knowledge to AST nodes.
-- Although this algorithm currently parallelizes nicely, it does not exploit
-- the incremental nature of the task at hand. Introducing support for
-- incremental queries might let us go even faster here.
-- TODO: handle errors properly
reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End)
reachable :: SolverGroup -> Expr 'End -> IO ([SMT2], Expr 'End)
reachable SolverGroup
solvers Expr 'End
e = do
  ([SMT2], Maybe (Expr 'End))
res <- [Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go [] Expr 'End
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
"Internal Error: no reachable paths found")) ([SMT2], Maybe (Expr 'End))
res
  where
    {-
       Walk down the tree and collect pcs.
       Dispatch a reachability query at each leaf.
       If reachable return the expr wrapped in a Just. If not return Nothing.
       When walking back up the tree drop unreachable subbranches.
    -}
    go :: [Prop] -> Expr End -> IO ([SMT2], Maybe (Expr End))
    go :: [Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go [Prop]
pcs = \case
      ITE Expr 'EWord
c Expr 'End
t Expr 'End
f -> do
        (([SMT2], Maybe (Expr 'End))
tres, ([SMT2], Maybe (Expr 'End))
fres) <- forall a b. IO a -> IO b -> IO (a, b)
concurrently
          ([Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (W256 -> Expr 'EWord
Lit W256
1) Expr 'EWord
c forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
t)
          ([Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (W256 -> Expr 'EWord
Lit W256
0) Expr 'EWord
c forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
f)
        let subexpr :: Maybe (Expr 'End)
subexpr = case (forall a b. (a, b) -> b
snd ([SMT2], Maybe (Expr 'End))
tres, forall a b. (a, b) -> b
snd ([SMT2], Maybe (Expr 'End))
fres) of
              (Just Expr 'End
t', Just Expr 'End
f') -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE Expr 'EWord
c Expr 'End
t' Expr 'End
f'
              (Just Expr 'End
t', Maybe (Expr 'End)
Nothing) -> forall a. a -> Maybe a
Just Expr 'End
t'
              (Maybe (Expr 'End)
Nothing, Just Expr 'End
f') -> forall a. a -> Maybe a
Just Expr 'End
f'
              (Maybe (Expr 'End)
Nothing, Maybe (Expr 'End)
Nothing) -> forall a. Maybe a
Nothing
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> a
fst ([SMT2], Maybe (Expr 'End))
tres forall a. Semigroup a => a -> a -> a
<> forall a b. (a, b) -> a
fst ([SMT2], Maybe (Expr 'End))
fres, Maybe (Expr 'End)
subexpr)
      Expr 'End
leaf -> do
        let query :: SMT2
query = [Prop] -> SMT2
assertProps [Prop]
pcs
        CheckSatResult
res <- SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers SMT2
query
        case CheckSatResult
res of
          Sat SMTCex
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([SMT2
query], forall a. a -> Maybe a
Just Expr 'End
leaf)
          CheckSatResult
Unsat -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([SMT2
query], forall a. Maybe a
Nothing)
          CheckSatResult
r -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Invalid solver result: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show CheckSatResult
r


-- | Evaluate the provided proposition down to its most concrete result
evalProp :: Prop -> Prop
evalProp :: Prop -> Prop
evalProp = \case
  o :: Prop
o@(PBool Bool
_) -> Prop
o
  o :: Prop
o@(PNeg Prop
p)  -> case Prop
p of
              (PBool Bool
b) -> Bool -> Prop
PBool (Bool -> Bool
not Bool
b)
              Prop
_ -> Prop
o
  o :: Prop
o@(PEq Expr a
l Expr a
r) -> if Expr a
l forall a. Eq a => a -> a -> Bool
== Expr a
r
                 then Bool -> Prop
PBool Bool
True
                 else Prop
o
  o :: Prop
o@(PLT (Lit W256
l) (Lit W256
r)) -> if W256
l forall a. Ord a => a -> a -> Bool
< W256
r
                             then Bool -> Prop
PBool Bool
True
                             else Prop
o
  o :: Prop
o@(PGT (Lit W256
l) (Lit W256
r)) -> if W256
l forall a. Ord a => a -> a -> Bool
> W256
r
                             then Bool -> Prop
PBool Bool
True
                             else Prop
o
  o :: Prop
o@(PGEq (Lit W256
l) (Lit W256
r)) -> if W256
l forall a. Ord a => a -> a -> Bool
>= W256
r
                              then Bool -> Prop
PBool Bool
True
                              else Prop
o
  o :: Prop
o@(PLEq (Lit W256
l) (Lit W256
r)) -> if W256
l forall a. Ord a => a -> a -> Bool
<= W256
r
                              then Bool -> Prop
PBool Bool
True
                              else Prop
o
  o :: Prop
o@(PAnd Prop
l Prop
r) -> case (Prop -> Prop
evalProp Prop
l, Prop -> Prop
evalProp Prop
r) of
                    (PBool Bool
True, PBool Bool
True) -> Bool -> Prop
PBool Bool
True
                    (PBool Bool
_, PBool Bool
_) -> Bool -> Prop
PBool Bool
False
                    (Prop, Prop)
_ -> Prop
o
  o :: Prop
o@(POr Prop
l Prop
r) -> case (Prop -> Prop
evalProp Prop
l, Prop -> Prop
evalProp Prop
r) of
                   (PBool Bool
False, PBool Bool
False) -> Bool -> Prop
PBool Bool
False
                   (PBool Bool
_, PBool Bool
_) -> Bool -> Prop
PBool Bool
True
                   (Prop, Prop)
_ -> Prop
o
  Prop
o -> Prop
o


-- | Extract contraints stored in Expr End nodes
extractProps :: Expr End -> [Prop]
extractProps :: Expr 'End -> [Prop]
extractProps = \case
  ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_ -> []
  Success [Prop]
asserts Expr 'Buf
_ Expr 'Storage
_ -> [Prop]
asserts
  Failure [Prop]
asserts EvmError
_ -> [Prop]
asserts
  Partial [Prop]
asserts PartialExec
_ -> [Prop]
asserts
  GVar GVar 'End
_ -> forall a. HasCallStack => String -> a
error String
"cannot extract props from a GVar"

isPartial :: Expr a -> Bool
isPartial :: forall (a :: EType). Expr a -> Bool
isPartial (Partial [Prop]
_ PartialExec
_) = Bool
True
isPartial Expr a
_ = Bool
False

getPartials :: [Expr End] -> [PartialExec]
getPartials :: [Expr 'End] -> [PartialExec]
getPartials = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'End -> Maybe PartialExec
go
  where
    go :: Expr End -> Maybe PartialExec
    go :: Expr 'End -> Maybe PartialExec
go = \case
      Partial [Prop]
_ PartialExec
p -> forall a. a -> Maybe a
Just PartialExec
p
      Expr 'End
_ -> forall a. Maybe a
Nothing

-- | Symbolically execute the VM and check all endstates against the
-- postcondition, if available.
verify
  :: SolverGroup
  -> VeriOpts
  -> VM
  -> Maybe Postcondition
  -> IO (Expr End, [VerifyResult])
verify :: SolverGroup
-> VeriOpts
-> VM
-> Maybe Postcondition
-> IO (Expr 'End, [VerifyResult])
verify SolverGroup
solvers VeriOpts
opts VM
preState Maybe Postcondition
maybepost = do
  String -> IO ()
putStrLn String
"Exploring contract"

  Expr 'End
exprInter <- Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher
Fetch.oracle SolverGroup
solvers VeriOpts
opts.rpcInfo) VeriOpts
opts.maxIter VeriOpts
opts.askSmtIters VeriOpts
opts.loopHeuristic VM
preState Stepper (Expr 'End)
runExpr
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug forall a b. (a -> b) -> a -> b
$ String -> Text -> IO ()
T.writeFile String
"unsimplified.expr" (forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
exprInter)

  String -> IO ()
putStrLn String
"Simplifying expression"
  Expr 'End
expr <- if VeriOpts
opts.simp then (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Expr a
Expr.simplify Expr 'End
exprInter) else forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr 'End
exprInter
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug forall a b. (a -> b) -> a -> b
$ String -> Text -> IO ()
T.writeFile String
"simplified.expr" (forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
expr)

  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Explored contract (" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (Expr 'End -> Int
Expr.numBranches Expr 'End
expr) forall a. Semigroup a => a -> a -> a
<> String
" branches)"

  let flattened :: [Expr 'End]
flattened = Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
expr
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (a :: EType). Expr a -> Bool
isPartial [Expr 'End]
flattened) forall a b. (a -> b) -> a -> b
$ do
    Text -> IO ()
T.putStrLn Text
""
    Text -> IO ()
T.putStrLn Text
"WARNING: hevm was only able to partially explore the given contract due to the following issues:"
    Text -> IO ()
T.putStrLn Text
""
    Text -> IO ()
T.putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
T.unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Text -> Text
indent Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text
"- " <>)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PartialExec -> Text
formatPartial forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr 'End] -> [PartialExec]
getPartials forall a b. (a -> b) -> a -> b
$ [Expr 'End]
flattened

  case Maybe Postcondition
maybepost of
    Maybe Postcondition
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End
expr, [forall a b c. a -> ProofResult a b c
Qed ()])
    Just Postcondition
post -> do
      let
        -- Filter out any leaves that can be statically shown to be safe
        canViolate :: [Expr 'End]
canViolate = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (a -> Bool) -> [a] -> [a]
filter [Expr 'End]
flattened forall a b. (a -> b) -> a -> b
$
          \Expr 'End
leaf -> case Prop -> Prop
evalProp (Postcondition
post VM
preState Expr 'End
leaf) of
            PBool Bool
True -> Bool
False
            Prop
_ -> Bool
True
        assumes :: [Prop]
assumes = VM
preState.constraints
        withQueries :: [(SMT2, Expr 'End)]
withQueries = [Expr 'End]
canViolate forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Expr 'End
leaf ->
          ([Prop] -> SMT2
assertProps (Prop -> Prop
PNeg (Postcondition
post VM
preState Expr 'End
leaf) forall a. a -> [a] -> [a]
: [Prop]
assumes forall a. Semigroup a => a -> a -> a
<> Expr 'End -> [Prop]
extractProps Expr 'End
leaf), Expr 'End
leaf)
      String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Checking for reachability of "
                   forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SMT2, Expr 'End)]
withQueries)
                   forall a. Semigroup a => a -> a -> a
<> String
" potential property violation(s)"

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1 :: Int)..] [(SMT2, Expr 'End)]
withQueries) forall a b. (a -> b) -> a -> b
$ \(Int
idx, (SMT2
q, Expr 'End
leaf)) -> do
        String -> Text -> IO ()
TL.writeFile
          (String
"query-" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Int
idx forall a. Semigroup a => a -> a -> a
<> String
".smt2")
          (Text
"; " forall a. Semigroup a => a -> a -> a
<> (String -> Text
TL.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Expr 'End
leaf) forall a. Semigroup a => a -> a -> a
<> Text
"\n\n" forall a. Semigroup a => a -> a -> a
<> SMT2 -> Text
formatSMT2 SMT2
q forall a. Semigroup a => a -> a -> a
<> Text
"\n\n(check-sat)")

      -- Dispatch the remaining branches to the solver to check for violations
      [(CheckSatResult, Expr 'End)]
results <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a b.
Traversable t =>
(a -> IO b) -> t a -> IO (t b)
mapConcurrently [(SMT2, Expr 'End)]
withQueries forall a b. (a -> b) -> a -> b
$ \(SMT2
query, Expr 'End
leaf) -> do
        CheckSatResult
res <- SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers SMT2
query
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckSatResult
res, Expr 'End
leaf)
      let cexs :: [(CheckSatResult, Expr 'End)]
cexs = forall a. (a -> Bool) -> [a] -> [a]
filter (\(CheckSatResult
res, Expr 'End
_) -> Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckSatResult -> Bool
isUnsat forall a b. (a -> b) -> a -> b
$ CheckSatResult
res) [(CheckSatResult, Expr 'End)]
results
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [(CheckSatResult, Expr 'End)]
cexs then (Expr 'End
expr, [forall a b c. a -> ProofResult a b c
Qed ()]) else (Expr 'End
expr, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CheckSatResult, Expr 'End) -> VerifyResult
toVRes [(CheckSatResult, Expr 'End)]
cexs)
  where
    toVRes :: (CheckSatResult, Expr End) -> VerifyResult
    toVRes :: (CheckSatResult, Expr 'End) -> VerifyResult
toVRes (CheckSatResult
res, Expr 'End
leaf) = case CheckSatResult
res of
      Sat SMTCex
model -> forall a b c. b -> ProofResult a b c
Cex (Expr 'End
leaf, SMTCex
model)
      CheckSatResult
EVM.Solvers.Unknown -> forall a b c. c -> ProofResult a b c
Timeout Expr 'End
leaf
      CheckSatResult
Unsat -> forall a b c. a -> ProofResult a b c
Qed ()
      Error Text
e -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: solver responded with error: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Text
e

type UnsatCache = TVar [Set Prop]

-- | Compares two contract runtimes for trace equivalence by running two VMs
-- and comparing the end states.
--
-- We do this by asking the solver to find a common input for each pair of
-- endstates that satisfies the path conditions for both sides and produces a
-- differing output. If we can find such an input, then we have a clear
-- equivalence break, and since we run this check for every pair of end states,
-- the check is exhaustive.
equivalenceCheck
  :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop])
  -> IO [EquivResult]
equivalenceCheck :: SolverGroup
-> ByteString
-> ByteString
-> VeriOpts
-> (Expr 'Buf, [Prop])
-> IO [EquivResult]
equivalenceCheck SolverGroup
solvers ByteString
bytecodeA ByteString
bytecodeB VeriOpts
opts (Expr 'Buf, [Prop])
calldata' = do
  case ByteString
bytecodeA forall a. Eq a => a -> a -> Bool
== ByteString
bytecodeB of
    Bool
True -> do
      String -> IO ()
putStrLn String
"bytecodeA and bytecodeB are identical"
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall a b c. a -> ProofResult a b c
Qed ()]
    Bool
False -> do
      [Expr 'End]
branchesA <- ByteString -> IO [Expr 'End]
getBranches ByteString
bytecodeA
      [Expr 'End]
branchesB <- ByteString -> IO [Expr 'End]
getBranches ByteString
bytecodeB

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (a :: EType). Expr a -> Bool
isPartial [Expr 'End]
branchesA Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (a :: EType). Expr a -> Bool
isPartial [Expr 'End]
branchesB) forall a b. (a -> b) -> a -> b
$ do
        String -> IO ()
putStrLn String
""
        String -> IO ()
putStrLn String
"WARNING: hevm was only able to partially explore the given contract due to the following issues:"
        String -> IO ()
putStrLn String
""
        Text -> IO ()
T.putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
T.unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Text -> Text
indent Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text
"- " <>)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PartialExec -> Text
formatPartial forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ (([Expr 'End] -> [PartialExec]
getPartials [Expr 'End]
branchesA) forall a. Semigroup a => a -> a -> a
<> ([Expr 'End] -> [PartialExec]
getPartials [Expr 'End]
branchesB))

      let allPairs :: [(Expr 'End, Expr 'End)]
allPairs = [(Expr 'End
a,Expr 'End
b) | Expr 'End
a <- [Expr 'End]
branchesA, Expr 'End
b <- [Expr 'End]
branchesB]
      String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Found " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Expr 'End, Expr 'End)]
allPairs) forall a. Semigroup a => a -> a -> a
<> String
" total pairs of endstates"

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug forall a b. (a -> b) -> a -> b
$
        String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"endstates in bytecodeA: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'End]
branchesA)
                   forall a. Semigroup a => a -> a -> a
<> String
"\nendstates in bytecodeB: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'End]
branchesB)

      let differingEndStates :: [Set Prop]
differingEndStates = forall a. [Set a] -> [Set a]
sortBySize (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr 'End -> Expr 'End -> Maybe (Set Prop)
distinct) [(Expr 'End, Expr 'End)]
allPairs)
      String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Asking the SMT solver for " forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Set Prop]
differingEndStates) forall a. Semigroup a => a -> a -> a
<> String
" pairs"
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Set Prop]
differingEndStates [(Integer
1::Integer)..]) (\(Set Prop
x, Integer
i) ->
        String -> Text -> IO ()
T.writeFile (String
"prop-checked-" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Integer
i) (String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Set Prop
x))

      TVar [Set Prop]
knownUnsat <- forall a. a -> IO (TVar a)
newTVarIO []
      Int
procs <- IO Int
getNumProcessors
      [(EquivResult, Bool)]
results <- [Set Prop] -> TVar [Set Prop] -> Int -> IO [(EquivResult, Bool)]
checkAll [Set Prop]
differingEndStates TVar [Set Prop]
knownUnsat Int
procs

      let useful :: Integer
useful = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(EquivResult
_, Bool
b) Integer
n -> if Bool
b then Integer
nforall a. Num a => a -> a -> a
+Integer
1 else Integer
n) (Integer
0::Integer) [(EquivResult, Bool)]
results
      String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Reuse of previous queries was Useful in " forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> String
show Integer
useful) forall a. Semigroup a => a -> a -> a
<> String
" cases"
      case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a b c. ProofResult a b c -> Bool
isQed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [(EquivResult, Bool)]
results of
        Bool
True -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall a b c. a -> ProofResult a b c
Qed ()]
        Bool
False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= forall a b c. a -> ProofResult a b c
Qed ()) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [(EquivResult, Bool)]
results
  where
    -- we order the sets by size because this gives us more cache hits when
    -- running our queries later on (since we rely on a subset check)
    sortBySize :: [Set a] -> [Set a]
    sortBySize :: forall a. [Set a] -> [Set a]
sortBySize = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\Set a
a Set a
b -> if forall a. Set a -> Int
size Set a
a forall a. Ord a => a -> a -> Bool
> forall a. Set a -> Int
size Set a
b then Ordering
Prelude.LT else Ordering
Prelude.GT)

    -- returns True if a is a subset of any of the sets in b
    subsetAny :: Set Prop -> [Set Prop] -> Bool
    subsetAny :: Set Prop -> [Set Prop] -> Bool
subsetAny Set Prop
a [Set Prop]
b = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Set Prop
bp Bool
acc -> Bool
acc Bool -> Bool -> Bool
|| forall a. Ord a => Set a -> Set a -> Bool
isSubsetOf Set Prop
a Set Prop
bp) Bool
False [Set Prop]
b

    -- decompiles the given bytecode into a list of branches
    getBranches :: ByteString -> IO [Expr End]
    getBranches :: ByteString -> IO [Expr 'End]
getBranches ByteString
bs = do
      let
        bytecode :: ByteString
bytecode = if ByteString -> Bool
BS.null ByteString
bs then [Word8] -> ByteString
BS.pack [Word8
0] else ByteString
bs
        prestate :: VM
prestate = (Expr 'Buf, [Prop])
-> ByteString -> Maybe Precondition -> Expr 'Storage -> VM
abstractVM (Expr 'Buf, [Prop])
calldata' ByteString
bytecode forall a. Maybe a
Nothing Expr 'Storage
AbstractStore
      Expr 'End
expr <- Fetcher
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM
-> Stepper (Expr 'End)
-> IO (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher
Fetch.oracle SolverGroup
solvers forall a. Maybe a
Nothing) VeriOpts
opts.maxIter VeriOpts
opts.askSmtIters VeriOpts
opts.loopHeuristic VM
prestate Stepper (Expr 'End)
runExpr
      let simpl :: Expr 'End
simpl = if VeriOpts
opts.simp then (forall (a :: EType). Expr a -> Expr a
Expr.simplify Expr 'End
expr) else Expr 'End
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
simpl

    -- checks for satisfiability of all the props in the provided set. skips
    -- the solver if we can determine unsatisfiability from the cache already
    -- the last element of the returned tuple indicates whether the cache was
    -- used or not
    check :: UnsatCache -> Set Prop -> IO (EquivResult, Bool)
    check :: TVar [Set Prop] -> Set Prop -> IO (EquivResult, Bool)
check TVar [Set Prop]
knownUnsat Set Prop
props = do
      let smt :: SMT2
smt = [Prop] -> SMT2
assertProps forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Prop
props
      [Set Prop]
ku <- forall a. TVar a -> IO a
readTVarIO TVar [Set Prop]
knownUnsat
      (Bool, CheckSatResult)
res <- if Set Prop -> [Set Prop] -> Bool
subsetAny Set Prop
props [Set Prop]
ku
             then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, CheckSatResult
Unsat)
             else (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool
False),) (SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers SMT2
smt))
      case (Bool, CheckSatResult)
res of
        (Bool
_, Sat SMTCex
x) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b c. b -> ProofResult a b c
Cex SMTCex
x, Bool
False)
        (Bool
quick, CheckSatResult
Unsat) ->
          case Bool
quick of
            Bool
True  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b c. a -> ProofResult a b c
Qed (), Bool
quick)
            Bool
False -> do
              -- nb: we might end up with duplicates here due to a
              -- potential race, but it doesn't matter for correctness
              forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. TVar a -> STM a
readTVar TVar [Set Prop]
knownUnsat forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. TVar a -> a -> STM ()
writeTVar TVar [Set Prop]
knownUnsat forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Prop
props :)
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b c. a -> ProofResult a b c
Qed (), Bool
False)
        (Bool
_, CheckSatResult
EVM.Solvers.Unknown) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b c. c -> ProofResult a b c
Timeout (), Bool
False)
        (Bool
_, Error Text
txt) -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Error while running solver: `" forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
txt -- <> "` SMT file was: `" <> filename <> "`"

    -- Allows us to run it in parallel. Note that this (seems to) run it
    -- from left-to-right, and with a max of K threads. This is in contrast to
    -- mapConcurrently which would spawn as many threads as there are jobs, and
    -- run them in a random order. We ordered them correctly, though so that'd be bad
    checkAll :: [(Set Prop)] -> UnsatCache -> Int -> IO [(EquivResult, Bool)]
    checkAll :: [Set Prop] -> TVar [Set Prop] -> Int -> IO [(EquivResult, Bool)]
checkAll [Set Prop]
input TVar [Set Prop]
cache Int
numproc = do
       IO (EquivResult, Bool) -> IO (EquivResult, Bool)
wrap <- forall a. Int -> IO (IO a -> IO a)
pool Int
numproc
       forall a b. (a -> IO b) -> [a] -> IO [b]
parMapIO (IO (EquivResult, Bool) -> IO (EquivResult, Bool)
wrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TVar [Set Prop] -> Set Prop -> IO (EquivResult, Bool)
check TVar [Set Prop]
cache)) [Set Prop]
input

    -- Takes two branches and returns a set of props that will need to be
    -- satisfied for the two branches to violate the equivalence check. i.e.
    -- for a given pair of branches, equivalence is violated if there exists an
    -- input that satisfies the branch conditions from both sides and produces
    -- a differing result in each branch
    distinct :: Expr End -> Expr End -> Maybe (Set Prop)
    distinct :: Expr 'End -> Expr 'End -> Maybe (Set Prop)
distinct Expr 'End
aEnd Expr 'End
bEnd =
      let
        differingResults :: Prop
differingResults = case (Expr 'End
aEnd, Expr 'End
bEnd) of
          (Success [Prop]
_ Expr 'Buf
aOut Expr 'Storage
aStore, Success [Prop]
_ Expr 'Buf
bOut Expr 'Storage
bStore) ->
            if Expr 'Buf
aOut forall a. Eq a => a -> a -> Bool
== Expr 'Buf
bOut Bool -> Bool -> Bool
&& Expr 'Storage
aStore forall a. Eq a => a -> a -> Bool
== Expr 'Storage
bStore
            then Bool -> Prop
PBool Bool
False
            else Expr 'Storage
aStore forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Storage
bStore Prop -> Prop -> Prop
.|| Expr 'Buf
aOut forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Buf
bOut
          (Failure [Prop]
_ (Revert Expr 'Buf
a), Failure [Prop]
_ (Revert Expr 'Buf
b)) -> if Expr 'Buf
a forall a. Eq a => a -> a -> Bool
== Expr 'Buf
b then Bool -> Prop
PBool Bool
False else Expr 'Buf
a forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Buf
b
          (Failure [Prop]
_ EvmError
a, Failure [Prop]
_ EvmError
b) -> if EvmError
a forall a. Eq a => a -> a -> Bool
== EvmError
b then Bool -> Prop
PBool Bool
False else Bool -> Prop
PBool Bool
True
          -- partial end states can't be compared to actual end states, so we always ignore them
          (Partial {}, Expr 'End
_) -> Bool -> Prop
PBool Bool
False
          (Expr 'End
_, Partial {}) -> Bool -> Prop
PBool Bool
False
          (ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_, Expr 'End
_) -> forall a. HasCallStack => String -> a
error String
"Expressions must be flattened"
          (Expr 'End
_, ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_) -> forall a. HasCallStack => String -> a
error String
"Expressions must be flattened"
          (Expr 'End
a, Expr 'End
b) -> if Expr 'End
a forall a. Eq a => a -> a -> Bool
== Expr 'End
b
                    then Bool -> Prop
PBool Bool
False
                    else Bool -> Prop
PBool Bool
True
      in case Prop
differingResults of
        -- if the end states are the same, then they can never produce a
        -- different result under any circumstances
        PBool Bool
False -> forall a. Maybe a
Nothing
        -- if we can statically determine that the end states differ, then we
        -- ask the solver to find us inputs that satisfy both sets of branch
        -- conditions
        PBool Bool
True  -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ Expr 'End -> [Prop]
extractProps Expr 'End
aEnd forall a. Semigroup a => a -> a -> a
<> Expr 'End -> [Prop]
extractProps Expr 'End
bEnd
        -- if we cannot statically determine whether or not the end states
        -- differ, then we ask the solver if the end states can differ if both
        -- sets of path conditions are satisfiable
        Prop
_ -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ Prop
differingResults forall a. a -> [a] -> [a]
: Expr 'End -> [Prop]
extractProps Expr 'End
aEnd forall a. Semigroup a => a -> a -> a
<> Expr 'End -> [Prop]
extractProps Expr 'End
bEnd

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

produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)]
produceModels :: SolverGroup -> Expr 'End -> IO [(Expr 'End, CheckSatResult)]
produceModels SolverGroup
solvers Expr 'End
expr = do
  let flattened :: [Expr 'End]
flattened = Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
expr
      withQueries :: [(SMT2, Expr 'End)]
withQueries = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Expr 'End
e -> ([Prop] -> SMT2
assertProps forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'End -> [Prop]
extractProps forall a b. (a -> b) -> a -> b
$ Expr 'End
e, Expr 'End
e)) [Expr 'End]
flattened
  [(CheckSatResult, Expr 'End)]
results <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a b.
Traversable t =>
(a -> IO b) -> t a -> IO (t b)
mapConcurrently [(SMT2, Expr 'End)]
withQueries forall a b. (a -> b) -> a -> b
$ \(SMT2
query, Expr 'End
leaf) -> do
    CheckSatResult
res <- SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers SMT2
query
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckSatResult
res, Expr 'End
leaf)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> (b, a)
swap forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (\(CheckSatResult
res, Expr 'End
_) -> Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckSatResult -> Bool
isUnsat forall a b. (a -> b) -> a -> b
$ CheckSatResult
res) [(CheckSatResult, Expr 'End)]
results

showModel :: Expr Buf -> (Expr End, CheckSatResult) -> IO ()
showModel :: Expr 'Buf -> (Expr 'End, CheckSatResult) -> IO ()
showModel Expr 'Buf
cd (Expr 'End
expr, CheckSatResult
res) = do
  case CheckSatResult
res of
    CheckSatResult
Unsat -> forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- ignore unreachable branches
    Error Text
e -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal error: smt solver returned an error: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Text
e
    CheckSatResult
EVM.Solvers.Unknown -> do
      String -> IO ()
putStrLn String
"--- Branch ---"
      String -> IO ()
putStrLn String
""
      String -> IO ()
putStrLn String
"Unable to produce a model for the following end state:"
      String -> IO ()
putStrLn String
""
      Text -> IO ()
T.putStrLn forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
expr
      String -> IO ()
putStrLn String
""
    Sat SMTCex
cex -> do
      String -> IO ()
putStrLn String
"--- Branch ---"
      String -> IO ()
putStrLn String
""
      String -> IO ()
putStrLn String
"Inputs:"
      String -> IO ()
putStrLn String
""
      Text -> IO ()
T.putStrLn forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indent Int
2 forall a b. (a -> b) -> a -> b
$ Expr 'Buf -> SMTCex -> Text
formatCex Expr 'Buf
cd SMTCex
cex
      String -> IO ()
putStrLn String
""
      String -> IO ()
putStrLn String
"End State:"
      String -> IO ()
putStrLn String
""
      Text -> IO ()
T.putStrLn forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
expr
      String -> IO ()
putStrLn String
""


formatCex :: Expr Buf -> SMTCex -> Text
formatCex :: Expr 'Buf -> SMTCex -> Text
formatCex Expr 'Buf
cd m :: SMTCex
m@(SMTCex Map (Expr 'EWord) W256
_ Map (Expr 'Buf) BufModel
_ Map W256 (Map W256 W256)
store Map (Expr 'EWord) W256
blockContext Map (Expr 'EWord) W256
txContext) = [Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$
  [ Text
"Calldata:"
  , Int -> Text -> Text
indent Int
2 Text
cd'
  , Text
""
  ]
  forall a. Semigroup a => a -> a -> a
<> [Text]
storeCex
  forall a. Semigroup a => a -> a -> a
<> [Text]
txCtx
  forall a. Semigroup a => a -> a -> a
<> [Text]
blockCtx
  where
    -- we attempt to produce a model for calldata by substituting all variables
    -- and buffers provided by the model into the original calldata expression.
    -- If we have a concrete result then we diplay it, otherwise we diplay
    -- `Any`. This is a little bit of a hack (and maybe unsound?), but we need
    -- it for branches that do not refer to calldata at all (e.g. the top level
    -- callvalue check inserted by solidity in contracts that don't have any
    -- payable functions).
    cd' :: Text
cd' = Expr 'Buf -> Text
prettyBuf forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Expr a
Expr.simplify forall a b. (a -> b) -> a -> b
$ forall (a :: EType). SMTCex -> Expr a -> Expr a
subModel SMTCex
m Expr 'Buf
cd

    storeCex :: [Text]
    storeCex :: [Text]
storeCex
      | forall k a. Map k a -> Bool
Map.null Map W256 (Map W256 W256)
store = []
      | Bool
otherwise =
          [ Text
"Storage:"
          , Int -> Text -> Text
indent Int
2 forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\W256
key Map W256 W256
val [Text]
acc ->
              (Text
"Addr " forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word160 -> Addr
Addr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ W256
key)
                forall a. Semigroup a => a -> a -> a
<> Text
": " forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (forall k a. Map k a -> [(k, a)]
Map.toList Map W256 W256
val))) forall a. a -> [a] -> [a]
: [Text]
acc
            ) forall a. Monoid a => a
mempty Map W256 (Map W256 W256)
store
          , Text
""
          ]

    txCtx :: [Text]
    txCtx :: [Text]
txCtx
      | forall k a. Map k a -> Bool
Map.null Map (Expr 'EWord) W256
txContext = []
      | Bool
otherwise =
        [ Text
"Transaction Context:"
        , Int -> Text -> Text
indent Int
2 forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\Expr 'EWord
key W256
val [Text]
acc ->
            (Expr 'EWord -> Text
showTxCtx Expr 'EWord
key forall a. Semigroup a => a -> a -> a
<> Text
": " forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show W256
val)) forall a. a -> [a] -> [a]
: [Text]
acc
          ) forall a. Monoid a => a
mempty (Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
filterSubCtx Map (Expr 'EWord) W256
txContext)
        , Text
""
        ]

    -- strips the frame arg from frame context vars to make them easier to read
    showTxCtx :: Expr EWord -> Text
    showTxCtx :: Expr 'EWord -> Text
showTxCtx (CallValue Int
_) = Text
"CallValue"
    showTxCtx (Caller Int
_) = Text
"Caller"
    showTxCtx (Address Int
_) = Text
"Address"
    showTxCtx Expr 'EWord
x = String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Expr 'EWord
x

    -- strips all frame context that doesn't come from the top frame
    filterSubCtx :: Map (Expr EWord) W256 -> Map (Expr EWord) W256
    filterSubCtx :: Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
filterSubCtx = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey Expr 'EWord -> W256 -> Bool
go
      where
        go :: Expr EWord -> W256 -> Bool
        go :: Expr 'EWord -> W256 -> Bool
go (CallValue Int
x) W256
_ = Int
x forall a. Eq a => a -> a -> Bool
== Int
0
        go (Caller Int
x) W256
_ = Int
x forall a. Eq a => a -> a -> Bool
== Int
0
        go (Address Int
x) W256
_ = Int
x forall a. Eq a => a -> a -> Bool
== Int
0
        go (Balance {}) W256
_ = forall a. HasCallStack => String -> a
error String
"TODO: BALANCE"
        go (SelfBalance {}) W256
_ = forall a. HasCallStack => String -> a
error String
"TODO: SELFBALANCE"
        go (Gas {}) W256
_ = forall a. HasCallStack => String -> a
error String
"TODO: Gas"
        go Expr 'EWord
_ W256
_ = Bool
False

    blockCtx :: [Text]
    blockCtx :: [Text]
blockCtx
      | forall k a. Map k a -> Bool
Map.null Map (Expr 'EWord) W256
blockContext = []
      | Bool
otherwise =
        [ Text
"Block Context:"
        , Int -> Text -> Text
indent Int
2 forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\Expr 'EWord
key W256
val [Text]
acc ->
            (String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Expr 'EWord
key forall a. Semigroup a => a -> a -> a
<> String
": " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show W256
val) forall a. a -> [a] -> [a]
: [Text]
acc
          ) forall a. Monoid a => a
mempty Map (Expr 'EWord) W256
txContext
        , Text
""
        ]

    prettyBuf :: Expr Buf -> Text
    prettyBuf :: Expr 'Buf -> Text
prettyBuf (ConcreteBuf ByteString
"") = Text
"Empty"
    prettyBuf (ConcreteBuf ByteString
bs) = ByteString -> Text
formatBinary ByteString
bs
    prettyBuf Expr 'Buf
_ = Text
"Any"

-- | Takes a buffer and a Cex and replaces all abstract values in the buf with
-- concrete ones from the Cex.
subModel :: SMTCex -> Expr a -> Expr a
subModel :: forall (a :: EType). SMTCex -> Expr a -> Expr a
subModel SMTCex
c Expr a
expr =
  forall {a :: EType}. Map (Expr 'Buf) ByteString -> Expr a -> Expr a
subBufs (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BufModel -> ByteString
forceFlattened SMTCex
c.buffers) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars SMTCex
c.vars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: EType). Map W256 (Map W256 W256) -> Expr a -> Expr a
subStore SMTCex
c.store
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars SMTCex
c.blockContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars SMTCex
c.txContext forall a b. (a -> b) -> a -> b
$ Expr a
expr
  where
    forceFlattened :: BufModel -> ByteString
forceFlattened (SMT.Flat ByteString
bs) = ByteString
bs
    forceFlattened b :: BufModel
b@(SMT.Comp CompressedBuf
_) = BufModel -> ByteString
forceFlattened forall a b. (a -> b) -> a -> b
$
      forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: cannot flatten buffer: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show BufModel
b)
                (BufModel -> Maybe BufModel
SMT.collapse BufModel
b)

    subVars :: Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars Map (Expr 'EWord) W256
model Expr a
b = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey forall (a :: EType). Expr a -> Expr 'EWord -> W256 -> Expr a
subVar Expr a
b Map (Expr 'EWord) W256
model
    subVar :: Expr a -> Expr EWord -> W256 -> Expr a
    subVar :: forall (a :: EType). Expr a -> Expr 'EWord -> W256 -> Expr a
subVar Expr a
b Expr 'EWord
var W256
val = forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
go Expr a
b
      where
        go :: Expr a -> Expr a
        go :: forall (a :: EType). Expr a -> Expr a
go = \case
          v :: Expr a
v@(Var Text
_) -> if Expr a
v forall a. Eq a => a -> a -> Bool
== Expr 'EWord
var
                      then W256 -> Expr 'EWord
Lit W256
val
                      else Expr a
v
          Expr a
e -> Expr a
e

    subBufs :: Map (Expr 'Buf) ByteString -> Expr a -> Expr a
subBufs Map (Expr 'Buf) ByteString
model Expr a
b = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey forall (a :: EType). Expr a -> Expr 'Buf -> ByteString -> Expr a
subBuf Expr a
b Map (Expr 'Buf) ByteString
model
    subBuf :: Expr a -> Expr Buf -> ByteString -> Expr a
    subBuf :: forall (a :: EType). Expr a -> Expr 'Buf -> ByteString -> Expr a
subBuf Expr a
b Expr 'Buf
var ByteString
val = forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
go Expr a
b
      where
        go :: Expr a -> Expr a
        go :: forall (a :: EType). Expr a -> Expr a
go = \case
          a :: Expr a
a@(AbstractBuf Text
_) -> if Expr a
a forall a. Eq a => a -> a -> Bool
== Expr 'Buf
var
                      then ByteString -> Expr 'Buf
ConcreteBuf ByteString
val
                      else Expr a
a
          Expr a
e -> Expr a
e

    subStore :: Map W256 (Map W256 W256) -> Expr a -> Expr a
    subStore :: forall (a :: EType). Map W256 (Map W256 W256) -> Expr a -> Expr a
subStore Map W256 (Map W256 W256)
m Expr a
b = forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
go Expr a
b
      where
        go :: Expr a -> Expr a
        go :: forall (a :: EType). Expr a -> Expr a
go = \case
          Expr a
AbstractStore -> Map W256 (Map W256 W256) -> Expr 'Storage
ConcreteStore Map W256 (Map W256 W256)
m
          Expr a
e -> Expr a
e