{-# Language DataKinds #-}

module EVM.SymExec where

import Prelude hiding (Word)

import Control.Lens hiding (pre)
import EVM hiding (Query, Revert, push)
import qualified EVM
import EVM.Exec
import qualified EVM.Fetch as Fetch
import EVM.ABI
import EVM.SMT
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.List (foldl')
import Data.Tuple (swap)
import Data.ByteString (ByteString)
import Data.List (find)
import Data.ByteString (null, pack)
import qualified Control.Monad.State.Class as State
import Data.Bifunctor (first, second)
import Data.Text (Text)
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, indent, formatBinary)

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 EquivalenceResult = ProofResult ([VM], [VM]) VM ()

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

containsA :: Eq a => Eq b => Eq c => ProofResult a b c -> [(d , e, ProofResult a b c)] -> Bool
containsA :: forall a b c d e.
(Eq a, Eq b, Eq c) =>
ProofResult a b c -> [(d, e, ProofResult a b c)] -> Bool
containsA ProofResult a b c
a [(d, e, ProofResult a b c)]
lst = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
Data.List.find (\(d
_, e
_, ProofResult a b c
c) -> ProofResult a b c
c forall a. Eq a => a -> a -> Bool
== ProofResult a b c
a) [(d, e, ProofResult a b c)]
lst

data VeriOpts = VeriOpts
  { VeriOpts -> Bool
simp :: Bool
  , VeriOpts -> Bool
debug :: Bool
  , VeriOpts -> Maybe Integer
maxIter :: Maybe Integer
  , VeriOpts -> Maybe Integer
askSmtIters :: Maybe Integer
  , 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
  { simp :: Bool
simp = Bool
True
  , debug :: Bool
debug = Bool
False
  , maxIter :: Maybe Integer
maxIter = forall a. Maybe a
Nothing
  , askSmtIters :: Maybe Integer
askSmtIters = forall a. Maybe a
Nothing
  , rpcInfo :: RpcInfo
rpcInfo = forall a. Maybe a
Nothing
  }

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

debugVeriOpts :: VeriOpts
debugVeriOpts :: VeriOpts
debugVeriOpts = VeriOpts
defaultVeriOpts { debug :: 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
_ = let v :: AbiValue
v = AbiType -> String -> AbiValue
makeAbiValue AbiType
typ String
arg
                        in case AbiValue
v 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 :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> Maybe Precondition -> StorageModel -> VM
abstractVM :: Maybe (Text, [AbiType])
-> [String]
-> ByteString
-> Maybe Precondition
-> StorageModel
-> VM
abstractVM Maybe (Text, [AbiType])
typesignature [String]
concreteArgs ByteString
contractCode Maybe Precondition
maybepre StorageModel
storagemodel = VM
finalVm
  where
    (Expr 'Buf
calldata', [Prop]
calldataProps) = case Maybe (Text, [AbiType])
typesignature of
                 Maybe (Text, [AbiType])
Nothing -> (Text -> Expr 'Buf
AbstractBuf Text
"txdata", [])
                 Just (Text
name, [AbiType]
typs) -> Text -> [AbiType] -> [String] -> Expr 'Buf -> (Expr 'Buf, [Prop])
symCalldata Text
name [AbiType]
typs [String]
concreteArgs (Text -> Expr 'Buf
AbstractBuf Text
"txdata")
    store :: Expr 'Storage
store = case StorageModel
storagemodel of
              StorageModel
SymbolicS -> Expr 'Storage
AbstractStore
              StorageModel
InitialS -> Expr 'Storage
EmptyStore
              StorageModel
ConcreteS -> Map W256 (Map W256 W256) -> Expr 'Storage
ConcreteStore forall a. Monoid a => a
mempty
    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
calldata' [Prop]
calldataProps
    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 s t a b. ASetter s t a b -> (a -> b) -> s -> t
over Lens' VM [Prop]
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
calldata' [Prop]
calldataProps =
  (VMOpts -> VM
makeVm forall a b. (a -> b) -> a -> b
$ VMOpts
    { vmoptContract :: Contract
vmoptContract = ContractCode -> Contract
initialContract ContractCode
x
    , vmoptCalldata :: (Expr 'Buf, [Prop])
vmoptCalldata = (Expr 'Buf
calldata', [Prop]
calldataProps)
    , vmoptValue :: Expr 'EWord
vmoptValue = Expr 'EWord
callvalue'
    , vmoptStorageBase :: StorageBase
vmoptStorageBase = StorageBase
Symbolic
    , vmoptAddress :: Addr
vmoptAddress = Addr -> W256 -> Addr
createAddress Addr
ethrunAddress W256
1
    , vmoptCaller :: Expr 'EWord
vmoptCaller = Expr 'EWord
addr
    , vmoptOrigin :: Addr
vmoptOrigin = Addr
ethrunAddress --todo: generalize
    , vmoptCoinbase :: Addr
vmoptCoinbase = Addr
0
    , vmoptNumber :: W256
vmoptNumber = W256
0
    , vmoptTimestamp :: Expr 'EWord
vmoptTimestamp = (W256 -> Expr 'EWord
Lit W256
0)
    , vmoptBlockGaslimit :: Word64
vmoptBlockGaslimit = Word64
0
    , vmoptGasprice :: W256
vmoptGasprice = W256
0
    , vmoptPrevRandao :: W256
vmoptPrevRandao = W256
42069
    , vmoptGas :: Word64
vmoptGas = Word64
0xffffffffffffffff
    , vmoptGaslimit :: Word64
vmoptGaslimit = Word64
0xffffffffffffffff
    , vmoptBaseFee :: W256
vmoptBaseFee = W256
0
    , vmoptPriorityFee :: W256
vmoptPriorityFee = W256
0
    , vmoptMaxCodeSize :: W256
vmoptMaxCodeSize = W256
0xffffffff
    , vmoptSchedule :: FeeSchedule Word64
vmoptSchedule = forall n. Num n => FeeSchedule n
FeeSchedule.berlin
    , vmoptChainId :: W256
vmoptChainId = W256
1
    , vmoptCreate :: Bool
vmoptCreate = Bool
False
    , vmoptTxAccessList :: Map Addr [W256]
vmoptTxAccessList = forall a. Monoid a => a
mempty
    , vmoptAllowFFI :: Bool
vmoptAllowFFI = Bool
False
    }) forall a b. a -> (a -> b) -> b
& forall s t a b. ASetter s t a b -> b -> s -> t
set (Lens' VM Env
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Env (Map Addr Contract)
contracts forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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))
       forall a b. a -> (a -> b) -> b
& forall s t a b. ASetter s t a b -> b -> s -> t
set (Lens' VM Env
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Env (Expr 'Storage)
EVM.storage) Expr 'Storage
initStore


-- | Interpreter which explores all paths at branching points.
-- returns an Expr representing the possible executions
interpret
  :: Fetch.Fetcher
  -> Maybe Integer -- max iterations
  -> Maybe Integer -- ask smt iterations
  -> Stepper (Expr End)
  -> StateT VM IO (Expr End)
interpret :: Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters =
  ProgramView Action (Expr 'End) -> StateT VM 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)
      -> StateT VM IO (Expr End)

    eval :: ProgramView Action (Expr 'End) -> StateT VM 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 ->
          forall (m :: * -> *). MonadState VM m => m VMResult
exec forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Stepper (Expr 'End)
k
        Action b
Stepper.Run ->
          forall (m :: * -> *). MonadState VM m => m VM
run forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Stepper (Expr 'End)
k
        Stepper.IOAct StateT VM IO b
q ->
          forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
mapStateT forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO StateT VM IO b
q forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Stepper (Expr 'End)
k
        Stepper.Ask (EVM.PleaseChoosePath Expr 'EWord
cond Bool -> EVM ()
continue) -> do
          forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
assign Lens' VM (Maybe VMResult)
result forall a. Maybe a
Nothing
          VM
vm <- forall s (m :: * -> *). MonadState s m => m s
get
          case VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
vm Maybe Integer
maxIter of
            -- TODO: parallelise
            Maybe Bool
Nothing -> do
              Expr 'End
a <- Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters (forall a. EVM a -> Stepper a
Stepper.evm (Bool -> EVM ()
continue Bool
True) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> Stepper (Expr 'End)
k)
              forall s (m :: * -> *). MonadState s m => s -> m ()
put VM
vm
              Expr 'End
b <- Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters (forall a. EVM a -> Stepper a
Stepper.evm (Bool -> EVM ()
continue Bool
False) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> Stepper (Expr 'End)
k)
              forall (m :: * -> *) a. Monad m => a -> m a
return 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
            Just Bool
n ->
              -- Let's escape the loop. We give no guarantees at this point
              Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters (forall a. EVM a -> Stepper a
Stepper.evm (Bool -> EVM ()
continue (Bool -> Bool
not Bool
n)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> Stepper (Expr 'End)
k)
        Stepper.Wait Query
q -> do
          let performQuery :: StateT VM IO (Expr 'End)
performQuery = do
                EVM ()
m <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Fetcher
fetcher Query
q)
                Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters (forall a. EVM a -> Stepper a
Stepper.evm EVM ()
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> Stepper (Expr 'End)
k)

          case Query
q of
            PleaseAskSMT Expr 'EWord
_ [Prop]
_ BranchCondition -> EVM ()
continue -> do
              CodeLocation
codelocation <- VM -> CodeLocation
getCodeLocation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
              Integer
iteration <- forall a b. (Integral a, Num b) => a -> b
num forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe Int
0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use (Lens' VM (Map CodeLocation Int)
iterations forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
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 forall a. Ord a => a -> a -> Bool
< (forall a. a -> Maybe a -> a
fromMaybe Integer
5 Maybe Integer
askSmtIters)
              then Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters (forall a. EVM a -> Stepper a
Stepper.evm (BranchCondition -> EVM ()
continue BranchCondition
EVM.Unknown) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> Stepper (Expr 'End)
k)
              else StateT VM IO (Expr 'End)
performQuery

            Query
_ -> StateT VM IO (Expr 'End)
performQuery

        Stepper.EVM EVM b
m ->
          forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state (forall s a. State s a -> s -> (a, s)
runState EVM b
m) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret Fetcher
fetcher Maybe Integer
maxIter Maybe Integer
askSmtIters forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Stepper (Expr 'End)
k

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
      iters :: Int
iters = forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' VM (Map CodeLocation Int)
iterations forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
codelocation forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => a -> Iso' (Maybe a) a
non Int
0) VM
vm
  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 s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' VM Cache
cache forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Cache (Map (CodeLocation, Int) Bool)
path forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (CodeLocation
codelocation, Int
iters forall a. Num a => a -> a -> a
- Int
1)) VM
vm
     else forall a. Maybe a
Nothing


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


checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult])
checkAssert :: SolverGroup
-> [Word256]
-> ByteString
-> Maybe (Text, [AbiType])
-> [String]
-> VeriOpts
-> IO (Expr 'End, [VerifyResult])
checkAssert SolverGroup
solvers [Word256]
errs ByteString
c Maybe (Text, [AbiType])
signature' [String]
concreteArgs VeriOpts
opts = SolverGroup
-> ByteString
-> Maybe (Text, [AbiType])
-> [String]
-> VeriOpts
-> StorageModel
-> Maybe Precondition
-> Maybe Postcondition
-> IO (Expr 'End, [VerifyResult])
verifyContract SolverGroup
solvers ByteString
c Maybe (Text, [AbiType])
signature' [String]
concreteArgs VeriOpts
opts StorageModel
SymbolicS 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
  Revert [Prop]
_ (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)
  Revert [Prop]
_ 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 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)") forall a. Semigroup a => a -> a -> a
<> (AbiValue -> ByteString
encodeAbiValue forall a b. (a -> b) -> a -> b
$ Int -> Word256 -> AbiValue
AbiUInt Int
256 Word256
err)

verifyContract :: SolverGroup -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])
verifyContract :: SolverGroup
-> ByteString
-> Maybe (Text, [AbiType])
-> [String]
-> VeriOpts
-> StorageModel
-> Maybe Precondition
-> Maybe Postcondition
-> IO (Expr 'End, [VerifyResult])
verifyContract SolverGroup
solvers ByteString
theCode Maybe (Text, [AbiType])
signature' [String]
concreteArgs VeriOpts
opts StorageModel
storagemodel Maybe Precondition
maybepre Maybe Postcondition
maybepost = do
  let preState :: VM
preState = Maybe (Text, [AbiType])
-> [String]
-> ByteString
-> Maybe Precondition
-> StorageModel
-> VM
abstractVM Maybe (Text, [AbiType])
signature' [String]
concreteArgs ByteString
theCode Maybe Precondition
maybepre StorageModel
storagemodel
  SolverGroup
-> VeriOpts
-> VM
-> Maybe Postcondition
-> IO (Expr 'End, [VerifyResult])
verify SolverGroup
solvers VeriOpts
opts VM
preState Maybe Postcondition
maybepost

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

-- | 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 = forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' VM [Prop]
keccakEqs VM
vm
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' VM (Maybe VMResult)
result VM
vm of
    Maybe VMResult
Nothing -> forall a. HasCallStack => String -> a
error String
"Internal Error: vm in intermediate state after call to runFully"
    Just (VMSuccess Expr 'Buf
buf) -> [Prop] -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Return [Prop]
asserts Expr 'Buf
buf (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' VM Env
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Env (Expr 'Storage)
EVM.storage) VM
vm)
    Just (VMFailure Error
e) -> case Error
e of
      UnrecognizedOpcode Word8
_ -> [Prop] -> Error -> Expr 'End
Failure [Prop]
asserts Error
Invalid
      Error
SelfDestruction -> [Prop] -> Error -> Expr 'End
Failure [Prop]
asserts Error
SelfDestruct
      Error
EVM.StackLimitExceeded -> [Prop] -> Error -> Expr 'End
Failure [Prop]
asserts Error
EVM.Types.StackLimitExceeded
      Error
EVM.IllegalOverflow -> [Prop] -> Error -> Expr 'End
Failure [Prop]
asserts Error
EVM.Types.IllegalOverflow
      EVM.Revert Expr 'Buf
buf -> [Prop] -> Expr 'Buf -> Expr 'End
EVM.Types.Revert [Prop]
asserts Expr 'Buf
buf
      Error
EVM.InvalidMemoryAccess -> [Prop] -> Error -> Expr 'End
Failure [Prop]
asserts Error
EVM.Types.InvalidMemoryAccess
      Error
EVM.BadJumpDestination -> [Prop] -> Error -> Expr 'End
Failure [Prop]
asserts Error
EVM.Types.BadJumpDestination
      Error
e' -> [Prop] -> Error -> Expr 'End
Failure [Prop]
asserts forall a b. (a -> b) -> a -> b
$ String -> Error
EVM.Types.TmpErr (forall a. Show a => a -> String
show Error
e')

-- | Converts a given top level expr into a list of final states and the associated path conditions for each state
flattenExpr :: Expr End -> [([Prop], Expr End)]
flattenExpr :: Expr 'End -> [([Prop], Expr 'End)]
flattenExpr = [Prop] -> Expr 'End -> [([Prop], Expr 'End)]
go []
  where
    go :: [Prop] -> Expr End -> [([Prop], Expr End)]
    go :: [Prop] -> Expr 'End -> [([Prop], Expr 'End)]
go [Prop]
pcs = \case
      ITE Expr 'EWord
c Expr 'End
t Expr 'End
f -> [Prop] -> Expr 'End -> [([Prop], 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 -> [([Prop], 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
      e :: Expr 'End
e@(Revert [Prop]
_ Expr 'Buf
_) -> [([Prop]
pcs, Expr 'End
e)]
      e :: Expr 'End
e@(Return [Prop]
_ Expr 'Buf
_ Expr 'Storage
_) -> [([Prop]
pcs, Expr 'End
e)]
      Failure [Prop]
_ (TmpErr String
s) -> forall a. HasCallStack => String -> a
error String
s
      e :: Expr 'End
e@(Failure [Prop]
_ Error
_) -> [([Prop]
pcs, Expr 'End
e)]
      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
_ -> []
  Revert [Prop]
asserts Expr 'Buf
_ -> [Prop]
asserts
  Return [Prop]
asserts Expr 'Buf
_ Expr 'Storage
_ -> [Prop]
asserts
  Failure [Prop]
asserts Error
_ -> [Prop]
asserts
  GVar GVar 'End
_ -> forall a. HasCallStack => String -> a
error String
"cannot extract props from a GVar"


-- | 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 <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher
Fetch.oracle SolverGroup
solvers (VeriOpts -> RpcInfo
rpcInfo VeriOpts
opts)) (VeriOpts -> Maybe Integer
maxIter VeriOpts
opts) (VeriOpts -> Maybe Integer
askSmtIters VeriOpts
opts) Stepper (Expr 'End)
runExpr) VM
preState
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VeriOpts -> Bool
debug VeriOpts
opts) 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 -> Bool
simp VeriOpts
opts) 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 -> Bool
debug VeriOpts
opts) 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)"

  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 :: [([Prop], Expr 'End)]
canViolate = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (a -> Bool) -> [a] -> [a]
filter (Expr 'End -> [([Prop], Expr 'End)]
flattenExpr Expr 'End
expr) forall a b. (a -> b) -> a -> b
$
          \([Prop]
_, 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 = forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' VM [Prop]
constraints VM
preState
        withQueries :: [(SMT2, Expr 'End)]
withQueries = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([Prop]
pcs, 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 forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs), Expr 'End
leaf)) [([Prop], Expr 'End)]
canViolate
      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 -> Bool
debug VeriOpts
opts) 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.SMT.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

-- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.
equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> Maybe (Text, [AbiType]) -> IO [(Maybe SMTCex, Prop, ProofResult () () ())]
equivalenceCheck :: SolverGroup
-> ByteString
-> ByteString
-> VeriOpts
-> Maybe (Text, [AbiType])
-> IO [(Maybe SMTCex, Prop, ProofResult () () ())]
equivalenceCheck SolverGroup
solvers ByteString
bytecodeA ByteString
bytecodeB VeriOpts
opts Maybe (Text, [AbiType])
signature' = do
  let
    bytecodeA' :: ByteString
bytecodeA' = if ByteString -> Bool
Data.ByteString.null ByteString
bytecodeA then [Word8] -> ByteString
Data.ByteString.pack [Word8
0] else ByteString
bytecodeA
    bytecodeB' :: ByteString
bytecodeB' = if ByteString -> Bool
Data.ByteString.null ByteString
bytecodeB then [Word8] -> ByteString
Data.ByteString.pack [Word8
0] else ByteString
bytecodeB
    preStateA :: VM
preStateA = Maybe (Text, [AbiType])
-> [String]
-> ByteString
-> Maybe Precondition
-> StorageModel
-> VM
abstractVM Maybe (Text, [AbiType])
signature' [] ByteString
bytecodeA' forall a. Maybe a
Nothing StorageModel
SymbolicS
    preStateB :: VM
preStateB = Maybe (Text, [AbiType])
-> [String]
-> ByteString
-> Maybe Precondition
-> StorageModel
-> VM
abstractVM Maybe (Text, [AbiType])
signature' [] ByteString
bytecodeB' forall a. Maybe a
Nothing StorageModel
SymbolicS

  Expr 'End
aExpr <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher
Fetch.oracle SolverGroup
solvers forall a. Maybe a
Nothing) (VeriOpts -> Maybe Integer
maxIter VeriOpts
opts) (VeriOpts -> Maybe Integer
askSmtIters VeriOpts
opts) Stepper (Expr 'End)
runExpr) VM
preStateA
  Expr 'End
bExpr <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher
Fetch.oracle SolverGroup
solvers forall a. Maybe a
Nothing) (VeriOpts -> Maybe Integer
maxIter VeriOpts
opts) (VeriOpts -> Maybe Integer
askSmtIters VeriOpts
opts) Stepper (Expr 'End)
runExpr) VM
preStateB
  Expr 'End
aExprSimp <- if (VeriOpts -> Bool
simp VeriOpts
opts) 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
aExpr) else forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr 'End
aExpr
  Expr 'End
bExprSimp <- if (VeriOpts -> Bool
simp VeriOpts
opts) 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
bExpr) else forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr 'End
bExpr
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VeriOpts -> Bool
debug VeriOpts
opts) forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"num of aExprSimp endstates:" 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 forall a b. (a -> b) -> a -> b
$ Expr 'End -> [([Prop], Expr 'End)]
flattenExpr Expr 'End
aExprSimp) forall a. Semigroup a => a -> a -> a
<> String
"\nnum of bExprSimp endstates:" 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 forall a b. (a -> b) -> a -> b
$ Expr 'End -> [([Prop], Expr 'End)]
flattenExpr Expr 'End
bExprSimp)

  -- Check each pair of end states for equality:
  let
      differingEndStates :: [Prop]
differingEndStates = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([Prop], Expr 'End) -> ([Prop], Expr 'End) -> Prop
distinct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(([Prop], Expr 'End)
a,([Prop], Expr 'End)
b) | ([Prop], Expr 'End)
a <- Expr 'End -> [([Prop], Expr 'End)]
flattenExpr Expr 'End
aExprSimp, ([Prop], Expr 'End)
b <- Expr 'End -> [([Prop], Expr 'End)]
flattenExpr Expr 'End
bExprSimp]
      distinct :: ([Prop], Expr End) -> ([Prop], Expr End) -> Prop
      distinct :: ([Prop], Expr 'End) -> ([Prop], Expr 'End) -> Prop
distinct ([Prop]
aProps, Expr 'End
aEnd) ([Prop]
bProps, Expr 'End
bEnd) =
        let
          differingResults :: Prop
differingResults = case (Expr 'End
aEnd, Expr 'End
bEnd) of
            (Return [Prop]
_ Expr 'Buf
aOut Expr 'Storage
aStore, Return [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
            (Return {}, Expr 'End
_) -> Bool -> Prop
PBool Bool
True
            (Expr 'End
_, Return {}) -> Bool -> Prop
PBool Bool
True
            (Revert [Prop]
_ Expr 'Buf
a, Revert [Prop]
_ Expr 'Buf
b) -> if Expr 'Buf
aforall 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
            (Revert [Prop]
_ Expr 'Buf
_, Expr 'End
_) -> Bool -> Prop
PBool Bool
True
            (Expr 'End
_, Revert [Prop]
_ Expr 'Buf
_) -> Bool -> Prop
PBool Bool
True
            (Failure [Prop]
_ Error
erra, Failure [Prop]
_ Error
errb) -> if Error
erraforall a. Eq a => a -> a -> Bool
==Error
errb then Bool -> Prop
PBool Bool
False else Bool -> Prop
PBool Bool
True
            (GVar GVar 'End
_, Expr 'End
_) -> forall a. HasCallStack => String -> a
error String
"Expressions cannot contain global vars"
            (Expr 'End
_ , GVar GVar 'End
_) -> forall a. HasCallStack => String -> a
error String
"Expressions cannot contain global vars"
            (Failure [Prop]
_ (TmpErr String
s), Expr 'End
_) -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unhandled error: " forall a. Semigroup a => a -> a -> a
<> String
s
            (Expr 'End
_, Failure [Prop]
_ (TmpErr String
s)) -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unhandled error: " forall a. Semigroup a => a -> a -> a
<> String
s
            (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"

        -- if the SMT solver can find a common input that satisfies BOTH sets of path conditions
        -- AND the output differs, then we are in trouble. We do this for _every_ pair of paths, which
        -- makes this exhaustive
        in
        if Prop
differingResults forall a. Eq a => a -> a -> Bool
== Bool -> Prop
PBool Bool
False
           then Bool -> Prop
PBool Bool
False
           else (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Prop -> Prop -> Prop
PAnd (Bool -> Prop
PBool Bool
True) [Prop]
aProps) Prop -> Prop -> Prop
.&& (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Prop -> Prop -> Prop
PAnd (Bool -> Prop
PBool Bool
True) [Prop]
bProps)  Prop -> Prop -> Prop
.&& Prop
differingResults
  -- If there exists a pair of end states where this is not the case,
  -- the following constraint is satisfiable

  let diffEndStFilt :: [Prop]
diffEndStFilt = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Bool -> Prop
PBool Bool
False) [Prop]
differingEndStates
  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Equivalence checking " 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 [Prop]
diffEndStFilt) forall a. Semigroup a => a -> a -> a
<> String
" combinations"
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VeriOpts -> Bool
debug VeriOpts
opts) 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 [Prop]
diffEndStFilt [Integer
1 :: Integer ..]) (\(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 Prop
x))
  [(Maybe SMTCex, Prop, ProofResult () () ())]
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 (forall a b. [a] -> [b] -> [(a, b)]
zip [Prop]
diffEndStFilt [Integer
1 :: Integer ..]) forall a b. (a -> b) -> a -> b
$ \(Prop
prop, Integer
i) -> do
    let assertedProps :: SMT2
assertedProps = [Prop] -> SMT2
assertProps [Prop
prop]
    let filename :: String
filename = String
"eq-check-" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Integer
i forall a. Semigroup a => a -> a -> a
<> String
".smt2"
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VeriOpts -> Bool
debug VeriOpts
opts) forall a b. (a -> b) -> a -> b
$ String -> Text -> IO ()
T.writeFile (String
filename) forall a b. (a -> b) -> a -> b
$ (Text -> Text
TL.toStrict forall a b. (a -> b) -> a -> b
$ SMT2 -> Text
formatSMT2 SMT2
assertedProps) forall a. Semigroup a => a -> a -> a
<> Text
"\n(check-sat)"
    CheckSatResult
res <- case Prop
prop of
      PBool Bool
False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unsat
      Prop
_ -> SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers SMT2
assertedProps
    case CheckSatResult
res of
     Sat SMTCex
a -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just SMTCex
a, Prop
prop, forall a b c. b -> ProofResult a b c
Cex ())
     CheckSatResult
Unsat -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, Prop
prop, forall a b c. a -> ProofResult a b c
Qed ())
     CheckSatResult
EVM.SMT.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, Prop
prop, forall a b c. c -> ProofResult a b c
Timeout ())
     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 forall a. Semigroup a => a -> a -> a
<> String
"` SMT file was: `" forall a. Semigroup a => a -> a -> a
<> String
filename forall a. Semigroup a => a -> a -> a
<> String
"`"
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (\(Maybe SMTCex
_, Prop
_, ProofResult () () ()
res) -> ProofResult () () ()
res forall a. Eq a => a -> a -> Bool
/= forall a b c. a -> ProofResult a b c
Qed ()) [(Maybe SMTCex, Prop, ProofResult () () ())]
results

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 :: [([Prop], Expr 'End)]
flattened = Expr 'End -> [([Prop], Expr 'End)]
flattenExpr Expr 'End
expr
      withQueries :: [(SMT2, Expr 'End)]
withQueries = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first [Prop] -> SMT2
assertProps) [([Prop], 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.SMT.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) ByteString
_ 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]
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

    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 (SMTCex -> Map (Expr 'Buf) ByteString
buffers SMTCex
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars (SMTCex -> Map (Expr 'EWord) W256
vars SMTCex
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars (SMTCex -> Map (Expr 'EWord) W256
blockContext SMTCex
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars (SMTCex -> Map (Expr 'EWord) W256
txContext SMTCex
c) forall a b. (a -> b) -> a -> b
$ Expr a
expr
  where
    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