{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
module EVM.SymExec where
import Control.Concurrent.Async (concurrently, mapConcurrently)
import Control.Concurrent.Spawn (parMapIO, pool)
import Control.Concurrent.STM (atomically, TVar, readTVarIO, readTVar, newTVarIO, writeTVar)
import Control.Monad.Operational qualified as Operational
import Control.Monad.State.Strict
import Data.Bifunctor (second)
import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Data.Containers.ListUtils (nubOrd)
import Data.DoubleWord (Word256)
import Data.List (foldl', sortBy)
import Data.Maybe (fromMaybe, mapMaybe)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set, isSubsetOf, size)
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.IO qualified as T
import Data.Text.Lazy qualified as TL
import Data.Text.Lazy.IO qualified as TL
import Data.Tree.Zipper qualified as Zipper
import Data.Tuple (swap)
import EVM (makeVm, initialContract, getCodeLocation, isValidJumpDest)
import EVM.Exec
import EVM.Fetch qualified as Fetch
import EVM.ABI
import EVM.Expr qualified as Expr
import EVM.Format (formatExpr, formatPartial)
import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)
import EVM.SMT qualified as SMT
import EVM.Solvers
import EVM.Stepper (Stepper)
import EVM.Stepper qualified as Stepper
import EVM.Traversals
import EVM.Types
import EVM.Concrete (createAddress)
import EVM.FeeSchedule qualified as FeeSchedule
import EVM.Format (indent, formatBinary)
import GHC.Conc (getNumProcessors)
import GHC.Generics (Generic)
import Optics.Core
import Options.Generic (ParseField, ParseFields, ParseRecord)
import Witch (into, unsafeInto)
data Sig = Sig Text [AbiType]
data LoopHeuristic
= Naive
| StackBased
deriving (LoopHeuristic -> LoopHeuristic -> Bool
(LoopHeuristic -> LoopHeuristic -> Bool)
-> (LoopHeuristic -> LoopHeuristic -> Bool) -> Eq LoopHeuristic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LoopHeuristic -> LoopHeuristic -> Bool
== :: LoopHeuristic -> LoopHeuristic -> Bool
$c/= :: LoopHeuristic -> LoopHeuristic -> Bool
/= :: LoopHeuristic -> LoopHeuristic -> Bool
Eq, Int -> LoopHeuristic -> ShowS
[LoopHeuristic] -> ShowS
LoopHeuristic -> String
(Int -> LoopHeuristic -> ShowS)
-> (LoopHeuristic -> String)
-> ([LoopHeuristic] -> ShowS)
-> Show LoopHeuristic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LoopHeuristic -> ShowS
showsPrec :: Int -> LoopHeuristic -> ShowS
$cshow :: LoopHeuristic -> String
show :: LoopHeuristic -> String
$cshowList :: [LoopHeuristic] -> ShowS
showList :: [LoopHeuristic] -> ShowS
Show, ReadPrec [LoopHeuristic]
ReadPrec LoopHeuristic
Int -> ReadS LoopHeuristic
ReadS [LoopHeuristic]
(Int -> ReadS LoopHeuristic)
-> ReadS [LoopHeuristic]
-> ReadPrec LoopHeuristic
-> ReadPrec [LoopHeuristic]
-> Read LoopHeuristic
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS LoopHeuristic
readsPrec :: Int -> ReadS LoopHeuristic
$creadList :: ReadS [LoopHeuristic]
readList :: ReadS [LoopHeuristic]
$creadPrec :: ReadPrec LoopHeuristic
readPrec :: ReadPrec LoopHeuristic
$creadListPrec :: ReadPrec [LoopHeuristic]
readListPrec :: ReadPrec [LoopHeuristic]
Read, ReadM LoopHeuristic
Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser [LoopHeuristic]
Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
(Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser LoopHeuristic)
-> (Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser [LoopHeuristic])
-> ReadM LoopHeuristic
-> (forall (proxy :: * -> *). proxy LoopHeuristic -> String)
-> ParseField 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
$cparseField :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
parseField :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
$cparseListOfField :: Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser [LoopHeuristic]
parseListOfField :: Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser [LoopHeuristic]
$creadField :: ReadM LoopHeuristic
readField :: ReadM LoopHeuristic
$cmetavar :: forall (proxy :: * -> *). proxy LoopHeuristic -> String
metavar :: forall (proxy :: * -> *). proxy LoopHeuristic -> String
ParseField, ParseRecord LoopHeuristic
Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
ParseRecord LoopHeuristic
-> (Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe String
-> Parser LoopHeuristic)
-> ParseFields LoopHeuristic
forall a.
ParseRecord a
-> (Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser a)
-> ParseFields a
$cparseFields :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
parseFields :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic
ParseFields, Parser LoopHeuristic
Parser LoopHeuristic -> ParseRecord LoopHeuristic
forall a. Parser a -> ParseRecord a
$cparseRecord :: Parser LoopHeuristic
parseRecord :: Parser LoopHeuristic
ParseRecord, (forall x. LoopHeuristic -> Rep LoopHeuristic x)
-> (forall x. Rep LoopHeuristic x -> LoopHeuristic)
-> Generic LoopHeuristic
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
$cfrom :: forall x. LoopHeuristic -> Rep LoopHeuristic x
from :: forall x. LoopHeuristic -> Rep LoopHeuristic x
$cto :: forall x. Rep LoopHeuristic x -> LoopHeuristic
to :: forall x. Rep LoopHeuristic x -> LoopHeuristic
Generic)
data ProofResult a b c = Qed a | Cex b | Timeout c
deriving (Int -> ProofResult a b c -> ShowS
[ProofResult a b c] -> ShowS
ProofResult a b c -> String
(Int -> ProofResult a b c -> ShowS)
-> (ProofResult a b c -> String)
-> ([ProofResult a b c] -> ShowS)
-> Show (ProofResult a b c)
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
$cshowsPrec :: forall a b c.
(Show a, Show b, Show c) =>
Int -> ProofResult a b c -> ShowS
showsPrec :: Int -> ProofResult a b c -> ShowS
$cshow :: forall a b c.
(Show a, Show b, Show c) =>
ProofResult a b c -> String
show :: ProofResult a b c -> String
$cshowList :: forall a b c.
(Show a, Show b, Show c) =>
[ProofResult a b c] -> ShowS
showList :: [ProofResult a b c] -> ShowS
Show, ProofResult a b c -> ProofResult a b c -> Bool
(ProofResult a b c -> ProofResult a b c -> Bool)
-> (ProofResult a b c -> ProofResult a b c -> Bool)
-> Eq (ProofResult a b c)
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
$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
/= :: 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
(VeriOpts -> VeriOpts -> Bool)
-> (VeriOpts -> VeriOpts -> Bool) -> Eq VeriOpts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VeriOpts -> VeriOpts -> Bool
== :: VeriOpts -> VeriOpts -> Bool
$c/= :: VeriOpts -> VeriOpts -> Bool
/= :: VeriOpts -> VeriOpts -> Bool
Eq, Int -> VeriOpts -> ShowS
[VeriOpts] -> ShowS
VeriOpts -> String
(Int -> VeriOpts -> ShowS)
-> (VeriOpts -> String) -> ([VeriOpts] -> ShowS) -> Show VeriOpts
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VeriOpts -> ShowS
showsPrec :: Int -> VeriOpts -> ShowS
$cshow :: VeriOpts -> String
show :: VeriOpts -> String
$cshowList :: [VeriOpts] -> ShowS
showList :: [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 = Maybe Integer
forall a. Maybe a
Nothing
, $sel:askSmtIters:VeriOpts :: Integer
askSmtIters = Integer
1
, $sel:loopHeuristic:VeriOpts :: LoopHeuristic
loopHeuristic = LoopHeuristic
StackBased
, $sel:rpcInfo:VeriOpts :: RpcInfo
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 = (BlockNumber, Text) -> 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)
(Cex (Expr 'End, SMTCex)
c) = (Expr 'End, SMTCex) -> Maybe (Expr 'End, SMTCex)
forall a. a -> Maybe a
Just (Expr 'End, SMTCex)
c
extractCex VerifyResult
_ = Maybe (Expr 'End, SMTCex)
forall a. Maybe a
Nothing
bool :: Expr EWord -> Prop
bool :: Expr 'EWord -> Prop
bool Expr 'EWord
e = Prop -> Prop -> Prop
POr (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit W256
1)) (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit W256
0))
symAbiArg :: Text -> AbiType -> CalldataFragment
symAbiArg :: Text -> AbiType -> CalldataFragment
symAbiArg Text
name = \case
AbiUIntType Int
n ->
if Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
256
then let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Int -> Expr 'EWord -> Prop
Expr.inRange Int
n Expr 'EWord
v] Expr 'EWord
v
else String -> CalldataFragment
forall a. HasCallStack => String -> a
internalError String
"bad type"
AbiIntType Int
n ->
if Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
256
then let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Int -> Expr 'EWord -> Prop
Expr.inRange Int
n Expr 'EWord
v] Expr 'EWord
v
else String -> CalldataFragment
forall a. HasCallStack => String -> a
internalError 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
Expr.inRange Int
160 Expr 'EWord
v] Expr 'EWord
v
AbiBytesType Int
n ->
if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
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
Expr.inRange (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8) Expr 'EWord
v] Expr 'EWord
v
else String -> CalldataFragment
forall a. HasCallStack => String -> a
internalError String
"bad type"
AbiArrayType Int
sz AbiType
tp ->
[CalldataFragment] -> CalldataFragment
Comp ([CalldataFragment] -> CalldataFragment)
-> [CalldataFragment] -> CalldataFragment
forall a b. (a -> b) -> a -> b
$ (Text -> CalldataFragment) -> [Text] -> [CalldataFragment]
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 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n) AbiType
tp) [String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
n) | Int
n <- [Int
0..Int
szInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
AbiType
t -> String -> CalldataFragment
forall a. HasCallStack => String -> a
internalError (String -> CalldataFragment) -> String -> CalldataFragment
forall a b. (a -> b) -> a -> b
$ String
"TODO: symbolic abi encoding for " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> AbiType -> String
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
(Int -> CalldataFragment -> ShowS)
-> (CalldataFragment -> String)
-> ([CalldataFragment] -> ShowS)
-> Show CalldataFragment
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CalldataFragment -> ShowS
showsPrec :: Int -> CalldataFragment -> ShowS
$cshow :: CalldataFragment -> String
show :: CalldataFragment -> String
$cshowList :: [CalldataFragment] -> ShowS
showList :: [CalldataFragment] -> ShowS
Show, CalldataFragment -> CalldataFragment -> Bool
(CalldataFragment -> CalldataFragment -> Bool)
-> (CalldataFragment -> CalldataFragment -> Bool)
-> Eq CalldataFragment
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CalldataFragment -> CalldataFragment -> Bool
== :: CalldataFragment -> CalldataFragment -> Bool
$c/= :: CalldataFragment -> CalldataFragment -> Bool
/= :: CalldataFragment -> CalldataFragment -> Bool
Eq)
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 [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> Int -> String -> [String]
forall a. Int -> a -> [a]
replicate ([AbiType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbiType]
typesignature Int -> Int -> Int
forall a. Num a => a -> a -> a
- [String] -> Int
forall a. [a] -> Int
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 (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"arg" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
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 [] (Expr 'EWord -> CalldataFragment)
-> (Word256 -> Expr 'EWord) -> Word256 -> CalldataFragment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord)
-> (Word256 -> W256) -> Word256 -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word256 -> W256
forall target source. From source target => source -> target
into (Word256 -> CalldataFragment) -> Word256 -> CalldataFragment
forall a b. (a -> b) -> a -> b
$ Word256
w
AbiInt Int
_ Int256
w -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] (Expr 'EWord -> CalldataFragment)
-> (Int256 -> Expr 'EWord) -> Int256 -> CalldataFragment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Int256 -> W256) -> Int256 -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int256 -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int256 -> CalldataFragment) -> Int256 -> CalldataFragment
forall a b. (a -> b) -> a -> b
$ Int256
w
AbiAddress Addr
w -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] (Expr 'EWord -> CalldataFragment)
-> (Addr -> Expr 'EWord) -> Addr -> CalldataFragment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Addr -> W256) -> Addr -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> W256
forall target source. From source target => source -> target
into (Addr -> CalldataFragment) -> Addr -> CalldataFragment
forall a b. (a -> b) -> a -> b
$ Addr
w
AbiBool Bool
w -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] (Expr 'EWord -> CalldataFragment)
-> (W256 -> Expr 'EWord) -> W256 -> CalldataFragment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit (W256 -> CalldataFragment) -> W256 -> CalldataFragment
forall a b. (a -> b) -> a -> b
$ if Bool
w then W256
1 else W256
0
AbiValue
_ -> String -> CalldataFragment
forall a. HasCallStack => String -> a
internalError String
"TODO"
calldatas :: [CalldataFragment]
calldatas = (AbiType -> String -> Int -> CalldataFragment)
-> [AbiType] -> [String] -> [Int] -> [CalldataFragment]
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 W256 -> Integer -> W256
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
64 :: Integer))))
in (Expr 'Buf
withSelector, Prop
sizeConstraints Prop -> [Prop] -> [Prop]
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
_ -> String -> Expr 'EWord
forall a. HasCallStack => String -> a
internalError 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) (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeSel (W256 -> Expr 'EWord
Lit W256
1) (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeSel (W256 -> Expr 'EWord
Lit W256
2) (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Expr 'Buf
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 (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
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 [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
ps)
CalldataFragment
s -> String -> (Expr 'Buf, [Prop])
forall a. HasCallStack => String -> a
internalError (String -> (Expr 'Buf, [Prop])) -> String -> (Expr 'Buf, [Prop])
forall a b. (a -> b) -> a -> b
$ String
"unsupported cd fragment: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> CalldataFragment -> String
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' VM -> (VM -> VM) -> VM
forall a b. a -> (a -> b) -> b
& Optic A_Lens NoIx VM VM [Prop] [Prop]
-> ([Prop] -> [Prop]) -> VM -> VM
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over Optic A_Lens NoIx VM VM [Prop] [Prop]
#constraints ([Prop] -> [Prop] -> [Prop]
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 (VMOpts -> VM) -> VMOpts -> VM
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
, $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 = FeeSchedule Word64
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 = Map Addr [W256]
forall a. Monoid a => a
mempty
, $sel:allowFFI:VMOpts :: Bool
allowFFI = Bool
False
}) VM -> (VM -> VM) -> VM
forall a b. a -> (a -> b) -> b
& Optic
A_Lens
NoIx
VM
VM
(Maybe (IxValue (Map Addr Contract)))
(Maybe Contract)
-> Maybe Contract -> VM -> VM
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set (Optic A_Lens NoIx VM VM Env Env
#env Optic A_Lens NoIx VM VM Env Env
-> Optic
A_Lens NoIx Env Env (Map Addr Contract) (Map Addr Contract)
-> Optic A_Lens NoIx VM VM (Map Addr Contract) (Map Addr Contract)
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
% Optic A_Lens NoIx Env Env (Map Addr Contract) (Map Addr Contract)
#contracts Optic A_Lens NoIx VM VM (Map Addr Contract) (Map Addr Contract)
-> Optic
A_Lens
NoIx
(Map Addr Contract)
(Map Addr Contract)
(Maybe (IxValue (Map Addr Contract)))
(Maybe Contract)
-> Optic
A_Lens
NoIx
VM
VM
(Maybe (IxValue (Map Addr Contract)))
(Maybe Contract)
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
% Index (Map Addr Contract)
-> Lens' (Map Addr Contract) (Maybe (IxValue (Map Addr Contract)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (Addr -> W256 -> Addr
createAddress Addr
ethrunAddress W256
1))
(Contract -> Maybe Contract
forall a. a -> Maybe a
Just (ContractCode -> Contract
initialContract ContractCode
x))
interpret
:: Fetch.Fetcher
-> Maybe Integer
-> Integer
-> 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 (ProgramView Action (Expr 'End) -> IO (Expr 'End))
-> (Stepper (Expr 'End) -> ProgramView Action (Expr 'End))
-> Stepper (Expr 'End)
-> IO (Expr 'End)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stepper (Expr 'End) -> ProgramView Action (Expr 'End)
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) = Expr 'End -> IO (Expr 'End)
forall a. a -> IO a
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') = State VM VMResult -> VM -> (VMResult, 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 b
VMResult
r)
Action b
Stepper.Run -> do
let vm' :: VM
vm' = State VM VMResult -> 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 b
VM
vm')
Stepper.IOAct StateT VM IO b
q -> do
(b
r, VM
vm') <- StateT VM IO b -> VM -> IO (b, 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) <- IO (Expr 'End) -> IO (Expr 'End) -> IO (Expr 'End, Expr 'End)
forall a b. IO a -> IO b -> IO (a, b)
concurrently
(let (()
ra, VM
vma) = EVM () -> VM -> ((), VM)
forall s a. State s a -> s -> (a, s)
runState (Bool -> EVM ()
continue Bool
True) VM
vm { $sel:result:VM :: Maybe VMResult
result = Maybe VMResult
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 b
()
ra))
(let (()
rb, VM
vmb) = EVM () -> VM -> ((), VM)
forall s a. State s a -> s -> (a, s)
runState (Bool -> EVM ()
continue Bool
False) VM
vm { $sel:result:VM :: Maybe VMResult
result = Maybe VMResult
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 b
()
rb))
Expr 'End -> IO (Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> IO (Expr 'End)) -> Expr 'End -> IO (Expr 'End)
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 <- IO (EVM ()) -> IO (EVM ())
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Fetcher
fetcher Query
q)
let (()
r, VM
vm') = EVM () -> 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 b
()
r)
case Query
q of
PleaseAskSMT Expr 'EWord
cond [Prop]
_ BranchCondition -> EVM ()
continue -> do
case Expr 'EWord
cond of
Lit W256
c ->
case (VM -> Maybe Integer -> Maybe Bool
maxIterationsReached VM
vm Maybe Integer
maxIter, LoopHeuristic -> VM -> Maybe Bool
isLoopHead LoopHeuristic
heuristic VM
vm) of
(Just Bool
_, Just Bool
True) ->
Expr 'End -> IO (Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> IO (Expr 'End)) -> Expr 'End -> IO (Expr 'End)
forall a b. (a -> b) -> a -> b
$ [Prop] -> Traces -> PartialExec -> Expr 'End
Partial VM
vm.keccakEqs (Forest Trace -> Map Addr Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM
vm.traces) VM
vm.env.contracts) (PartialExec -> Expr 'End) -> PartialExec -> Expr 'End
forall a b. (a -> b) -> a -> b
$ Int -> Addr -> PartialExec
MaxIterationsReached VM
vm.state.pc VM
vm.state.contract
(Maybe Bool, Maybe Bool)
_ ->
let (()
r, VM
vm') = EVM () -> VM -> ((), VM)
forall s a. State s a -> s -> (a, s)
runState (BranchCondition -> EVM ()
continue (Bool -> BranchCondition
Case (W256
c W256 -> W256 -> Bool
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 b
()
r)
Expr 'EWord
_ ->
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
(Just Bool
True, Bool
_, Just Bool
n) -> do
let (()
r, VM
vm') = EVM () -> VM -> ((), VM)
forall s a. State s a -> s -> (a, s)
runState (BranchCondition -> EVM ()
continue (Bool -> BranchCondition
Case (Bool -> BranchCondition) -> Bool -> BranchCondition
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 b
()
r)
Expr 'End -> IO (Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> IO (Expr 'End)) -> Expr 'End -> IO (Expr 'End)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE Expr 'EWord
cond Expr 'End
a ([Prop] -> Traces -> PartialExec -> Expr 'End
Partial VM
vm.keccakEqs (Forest Trace -> Map Addr Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM
vm.traces) VM
vm.env.contracts) (Int -> Addr -> PartialExec
MaxIterationsReached VM
vm.state.pc VM
vm.state.contract))
(Just Bool
True, Bool
True, Maybe Bool
_) ->
IO (Expr 'End)
performQuery
(Maybe Bool, Bool, Maybe Bool)
_ ->
let (()
r, VM
vm') = EVM () -> 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 b
()
r)
Query
_ -> IO (Expr 'End)
performQuery
Stepper.EVM EVM b
m -> do
let (b
r, VM
vm') = EVM b -> VM -> (b, 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 = Maybe Bool
forall a. Maybe a
Nothing
maxIterationsReached VM
vm (Just Integer
maxIter) =
let codelocation :: CodeLocation
codelocation = VM -> CodeLocation
getCodeLocation VM
vm
(Int
iters, [Expr 'EWord]
_) = Optic'
A_Lens
NoIx
(Map CodeLocation (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
-> Map CodeLocation (Int, [Expr 'EWord]) -> (Int, [Expr 'EWord])
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (Index (Map CodeLocation (Int, [Expr 'EWord]))
-> Lens'
(Map CodeLocation (Int, [Expr 'EWord]))
(Maybe (IxValue (Map CodeLocation (Int, [Expr 'EWord]))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
Index (Map CodeLocation (Int, [Expr 'EWord]))
codelocation Optic
A_Lens
NoIx
(Map CodeLocation (Int, [Expr 'EWord]))
(Map CodeLocation (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
-> Optic
An_Iso
NoIx
(Maybe (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
(Int, [Expr 'EWord])
-> Optic'
A_Lens
NoIx
(Map CodeLocation (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
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
% (Int, [Expr 'EWord])
-> Optic
An_Iso
NoIx
(Maybe (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
(Int, [Expr 'EWord])
forall a. Eq a => a -> Iso' (Maybe a) a
non (Int
0, [])) VM
vm.iterations
in if Integer -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto Integer
maxIter Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
iters
then (CodeLocation, Int) -> Map (CodeLocation, Int) Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (CodeLocation
codelocation, Int
iters Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) VM
vm.cache.path
else Maybe Bool
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]
_) = Optic'
A_Lens
NoIx
(Map CodeLocation (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
-> Map CodeLocation (Int, [Expr 'EWord]) -> (Int, [Expr 'EWord])
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (Index (Map CodeLocation (Int, [Expr 'EWord]))
-> Lens'
(Map CodeLocation (Int, [Expr 'EWord]))
(Maybe (IxValue (Map CodeLocation (Int, [Expr 'EWord]))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at CodeLocation
Index (Map CodeLocation (Int, [Expr 'EWord]))
codelocation Optic
A_Lens
NoIx
(Map CodeLocation (Int, [Expr 'EWord]))
(Map CodeLocation (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
-> Optic
An_Iso
NoIx
(Maybe (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
(Int, [Expr 'EWord])
-> Optic'
A_Lens
NoIx
(Map CodeLocation (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
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
% (Int, [Expr 'EWord])
-> Optic
An_Iso
NoIx
(Maybe (Int, [Expr 'EWord]))
(Maybe (Int, [Expr 'EWord]))
(Int, [Expr 'EWord])
(Int, [Expr 'EWord])
forall a. Eq a => a -> Iso' (Maybe a) a
non (Int
0, [])) VM
vm.iterations
in Integer
askSmtIters Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall target source. From source target => source -> target
into Int
iters
isLoopHead :: LoopHeuristic -> VM -> Maybe Bool
isLoopHead :: LoopHeuristic -> VM -> Maybe Bool
isLoopHead LoopHeuristic
Naive VM
_ = Bool -> Maybe Bool
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 = CodeLocation
-> Map CodeLocation (Int, [Expr 'EWord])
-> Maybe (Int, [Expr 'EWord])
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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int
forall a. Bounded a => a
maxBound :: Int) Bool -> Bool -> Bool
&& VM -> Int -> Bool
isValidJumpDest VM
vm (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
wrd)
isValid Expr 'EWord
_ = Bool
False
in case Maybe (Int, [Expr 'EWord])
oldIters of
Just (Int
_, [Expr 'EWord]
oldStack) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ (Expr 'EWord -> Bool) -> [Expr 'EWord] -> [Expr 'EWord]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr 'EWord -> Bool
isValid [Expr 'EWord]
oldStack [Expr 'EWord] -> [Expr 'EWord] -> Bool
forall a. Eq a => a -> a -> Bool
== (Expr 'EWord -> Bool) -> [Expr 'EWord] -> [Expr 'EWord]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr 'EWord -> Bool
isValid VM
vm.state.stack
Maybe (Int, [Expr 'EWord])
Nothing -> Maybe Bool
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 Maybe Precondition
forall a. Maybe a
Nothing (Postcondition -> Maybe Postcondition
forall a. a -> Maybe a
Just (Postcondition -> Maybe Postcondition)
-> Postcondition -> Maybe Postcondition
forall a b. (a -> b) -> a -> b
$ [Word256] -> Postcondition
checkAssertions [Word256]
errs)
checkAssertions :: [Word256] -> Postcondition
checkAssertions :: [Word256] -> Postcondition
checkAssertions [Word256]
errs VM
_ = \case
Failure [Prop]
_ Traces
_ (Revert (ConcreteBuf ByteString
msg)) -> Bool -> Prop
PBool (Bool -> Prop) -> Bool -> Prop
forall a b. (a -> b) -> a -> b
$ ByteString
msg ByteString -> [ByteString] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Word256 -> ByteString) -> [Word256] -> [ByteString]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word256 -> ByteString
panicMsg [Word256]
errs)
Failure [Prop]
_ Traces
_ (Revert Expr 'Buf
b) -> (Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Prop -> Prop -> Prop
PAnd (Bool -> Prop
PBool Bool
True) ((Word256 -> Prop) -> [Word256] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Prop -> Prop
PNeg (Prop -> Prop) -> (Word256 -> Prop) -> Word256 -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'Buf -> Expr 'Buf -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'Buf
b (Expr 'Buf -> Prop) -> (Word256 -> Expr 'Buf) -> Word256 -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf)
-> (Word256 -> ByteString) -> Word256 -> Expr 'Buf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word256 -> ByteString
panicMsg) [Word256]
errs)
Expr 'End
_ -> Bool -> Prop
PBool Bool
True
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]
panicMsg :: Word256 -> ByteString
panicMsg :: Word256 -> ByteString
panicMsg Word256
err = Text -> ByteString
selector Text
"Panic(uint256)" ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> AbiValue -> ByteString
encodeAbiValue (Int -> Word256 -> AbiValue
AbiUInt Int
256 Word256
err)
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"
, [Expr 'Buf -> Expr 'EWord
Expr.bufLength (Text -> Expr 'Buf
AbstractBuf Text
"txdata") Expr 'EWord -> Expr 'EWord -> Prop
.< (W256 -> Expr 'EWord
Lit (W256
2 W256 -> Integer -> W256
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
runExpr :: Stepper.Stepper (Expr End)
runExpr :: Stepper (Expr 'End)
runExpr = do
VM
vm <- Stepper VM
Stepper.runFully
let asserts :: [Prop]
asserts = VM
vm.keccakEqs [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> VM
vm.constraints
Expr 'End -> Stepper (Expr 'End)
forall a. a -> ProgramT Action Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> Stepper (Expr 'End))
-> Expr 'End -> Stepper (Expr 'End)
forall a b. (a -> b) -> a -> b
$ case VM
vm.result of
Just (VMSuccess Expr 'Buf
buf) -> [Prop] -> Traces -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Success [Prop]
asserts (Forest Trace -> Map Addr Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM
vm.traces) VM
vm.env.contracts) Expr 'Buf
buf VM
vm.env.storage
Just (VMFailure EvmError
e) -> [Prop] -> Traces -> EvmError -> Expr 'End
Failure [Prop]
asserts (Forest Trace -> Map Addr Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM
vm.traces) VM
vm.env.contracts) EvmError
e
Just (Unfinished PartialExec
p) -> [Prop] -> Traces -> PartialExec -> Expr 'End
Partial [Prop]
asserts (Forest Trace -> Map Addr Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM
vm.traces) VM
vm.env.contracts) PartialExec
p
Maybe VMResult
_ -> String -> Expr 'End
forall a. HasCallStack => String -> a
internalError String
"vm in intermediate state after call to runFully"
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 ((Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
c (W256 -> Expr 'EWord
Lit W256
0))) Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
t [Expr 'End] -> [Expr 'End] -> [Expr 'End]
forall a. Semigroup a => a -> a -> a
<> [Prop] -> Expr 'End -> [Expr 'End]
go (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
c (W256 -> Expr 'EWord
Lit W256
0) Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
f
Success [Prop]
ps Traces
trace Expr 'Buf
msg Expr 'Storage
store -> [[Prop] -> Traces -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Success ([Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) Traces
trace Expr 'Buf
msg Expr 'Storage
store]
Failure [Prop]
ps Traces
trace EvmError
e -> [[Prop] -> Traces -> EvmError -> Expr 'End
Failure ([Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) Traces
trace EvmError
e]
Partial [Prop]
ps Traces
trace PartialExec
p -> [[Prop] -> Traces -> PartialExec -> Expr 'End
Partial ([Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) Traces
trace PartialExec
p]
GVar GVar 'End
_ -> String -> [Expr 'End]
forall a. HasCallStack => String -> a
internalError String
"cannot flatten an Expr containing a GVar"
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
([SMT2], Expr 'End) -> IO ([SMT2], Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([SMT2], Expr 'End) -> IO ([SMT2], Expr 'End))
-> ([SMT2], Expr 'End) -> IO ([SMT2], Expr 'End)
forall a b. (a -> b) -> a -> b
$ (Maybe (Expr 'End) -> Expr 'End)
-> ([SMT2], Maybe (Expr 'End)) -> ([SMT2], Expr 'End)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Expr 'End -> Maybe (Expr 'End) -> Expr 'End
forall a. a -> Maybe a -> a
fromMaybe (String -> Expr 'End
forall a. HasCallStack => String -> a
internalError String
"no reachable paths found")) ([SMT2], Maybe (Expr 'End))
res
where
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) <- IO ([SMT2], Maybe (Expr 'End))
-> IO ([SMT2], Maybe (Expr 'End))
-> IO (([SMT2], Maybe (Expr 'End)), ([SMT2], Maybe (Expr 'End)))
forall a b. IO a -> IO b -> IO (a, b)
concurrently
([Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (W256 -> Expr 'EWord
Lit W256
1) Expr 'EWord
c Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
t)
([Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (W256 -> Expr 'EWord
Lit W256
0) Expr 'EWord
c Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
pcs) Expr 'End
f)
let subexpr :: Maybe (Expr 'End)
subexpr = case (([SMT2], Maybe (Expr 'End)) -> Maybe (Expr 'End)
forall a b. (a, b) -> b
snd ([SMT2], Maybe (Expr 'End))
tres, ([SMT2], Maybe (Expr 'End)) -> Maybe (Expr 'End)
forall a b. (a, b) -> b
snd ([SMT2], Maybe (Expr 'End))
fres) of
(Just Expr 'End
t', Just Expr 'End
f') -> Expr 'End -> Maybe (Expr 'End)
forall a. a -> Maybe a
Just (Expr 'End -> Maybe (Expr 'End)) -> Expr 'End -> Maybe (Expr 'End)
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) -> Expr 'End -> Maybe (Expr 'End)
forall a. a -> Maybe a
Just Expr 'End
t'
(Maybe (Expr 'End)
Nothing, Just Expr 'End
f') -> Expr 'End -> Maybe (Expr 'End)
forall a. a -> Maybe a
Just Expr 'End
f'
(Maybe (Expr 'End)
Nothing, Maybe (Expr 'End)
Nothing) -> Maybe (Expr 'End)
forall a. Maybe a
Nothing
([SMT2], Maybe (Expr 'End)) -> IO ([SMT2], Maybe (Expr 'End))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([SMT2], Maybe (Expr 'End)) -> [SMT2]
forall a b. (a, b) -> a
fst ([SMT2], Maybe (Expr 'End))
tres [SMT2] -> [SMT2] -> [SMT2]
forall a. Semigroup a => a -> a -> a
<> ([SMT2], Maybe (Expr 'End)) -> [SMT2]
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
_ -> ([SMT2], Maybe (Expr 'End)) -> IO ([SMT2], Maybe (Expr 'End))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([SMT2
query], Expr 'End -> Maybe (Expr 'End)
forall a. a -> Maybe a
Just Expr 'End
leaf)
CheckSatResult
Unsat -> ([SMT2], Maybe (Expr 'End)) -> IO ([SMT2], Maybe (Expr 'End))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([SMT2
query], Maybe (Expr 'End)
forall a. Maybe a
Nothing)
CheckSatResult
r -> String -> IO ([SMT2], Maybe (Expr 'End))
forall a. HasCallStack => String -> a
internalError (String -> IO ([SMT2], Maybe (Expr 'End)))
-> String -> IO ([SMT2], Maybe (Expr 'End))
forall a b. (a -> b) -> a -> b
$ String
"Invalid solver result: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> CheckSatResult -> String
forall a. Show a => a -> String
show CheckSatResult
r
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 Expr a -> Expr a -> Bool
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 W256 -> W256 -> Bool
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 W256 -> W256 -> Bool
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 W256 -> W256 -> Bool
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 W256 -> W256 -> Bool
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
extractProps :: Expr End -> [Prop]
= \case
ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_ -> []
Success [Prop]
asserts Traces
_ Expr 'Buf
_ Expr 'Storage
_ -> [Prop]
asserts
Failure [Prop]
asserts Traces
_ EvmError
_ -> [Prop]
asserts
Partial [Prop]
asserts Traces
_ PartialExec
_ -> [Prop]
asserts
GVar GVar 'End
_ -> String -> [Prop]
forall a. HasCallStack => String -> a
internalError String
"cannot extract props from a GVar"
isPartial :: Expr a -> Bool
isPartial :: forall (a :: EType). Expr a -> Bool
isPartial (Partial [Prop]
_ Traces
_ PartialExec
_) = Bool
True
isPartial Expr a
_ = Bool
False
getPartials :: [Expr End] -> [PartialExec]
getPartials :: [Expr 'End] -> [PartialExec]
getPartials = (Expr 'End -> Maybe PartialExec) -> [Expr 'End] -> [PartialExec]
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]
_ Traces
_ PartialExec
p -> PartialExec -> Maybe PartialExec
forall a. a -> Maybe a
Just PartialExec
p
Expr 'End
_ -> Maybe PartialExec
forall a. Maybe a
Nothing
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
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Text -> IO ()
T.writeFile String
"unsimplified.expr" (Expr 'End -> Text
forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
exprInter)
String -> IO ()
putStrLn String
"Simplifying expression"
Expr 'End
expr <- if VeriOpts
opts.simp then (Expr 'End -> IO (Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> IO (Expr 'End)) -> Expr 'End -> IO (Expr 'End)
forall a b. (a -> b) -> a -> b
$ Expr 'End -> Expr 'End
forall (a :: EType). Expr a -> Expr a
Expr.simplify Expr 'End
exprInter) else Expr 'End -> IO (Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr 'End
exprInter
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Text -> IO ()
T.writeFile String
"simplified.expr" (Expr 'End -> Text
forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
expr)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Explored contract (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Expr 'End -> Int
Expr.numBranches Expr 'End
expr) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" branches)"
let flattened :: [Expr 'End]
flattened = Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
expr
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Expr 'End -> Bool) -> [Expr 'End] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr 'End -> Bool
forall (a :: EType). Expr a -> Bool
isPartial [Expr 'End]
flattened) (IO () -> IO ()) -> IO () -> IO ()
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 (Text -> IO ()) -> ([Expr 'End] -> Text) -> [Expr 'End] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
T.unlines ([Text] -> Text) -> ([Expr 'End] -> [Text]) -> [Expr 'End] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Text -> Text
indent Int
2 (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text
"- " <>)) ([Text] -> [Text])
-> ([Expr 'End] -> [Text]) -> [Expr 'End] -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PartialExec -> Text) -> [PartialExec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PartialExec -> Text
formatPartial ([PartialExec] -> [Text])
-> ([Expr 'End] -> [PartialExec]) -> [Expr 'End] -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr 'End] -> [PartialExec]
getPartials ([Expr 'End] -> IO ()) -> [Expr 'End] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Expr 'End]
flattened
case Maybe Postcondition
maybepost of
Maybe Postcondition
Nothing -> (Expr 'End, [VerifyResult]) -> IO (Expr 'End, [VerifyResult])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End
expr, [() -> VerifyResult
forall a b c. a -> ProofResult a b c
Qed ()])
Just Postcondition
post -> do
let
canViolate :: [Expr 'End]
canViolate = ((Expr 'End -> Bool) -> [Expr 'End] -> [Expr 'End])
-> [Expr 'End] -> (Expr 'End -> Bool) -> [Expr 'End]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Expr 'End -> Bool) -> [Expr 'End] -> [Expr 'End]
forall a. (a -> Bool) -> [a] -> [a]
filter [Expr 'End]
flattened ((Expr 'End -> Bool) -> [Expr 'End])
-> (Expr 'End -> Bool) -> [Expr 'End]
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 [Expr 'End]
-> (Expr 'End -> (SMT2, Expr 'End)) -> [(SMT2, Expr 'End)]
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) Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
assumes [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> Expr 'End -> [Prop]
extractProps Expr 'End
leaf), Expr 'End
leaf)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Checking for reachability of "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show ([(SMT2, Expr 'End)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SMT2, Expr 'End)]
withQueries)
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" potential property violation(s)"
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Int, (SMT2, Expr 'End))]
-> ((Int, (SMT2, Expr 'End)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Int] -> [(SMT2, Expr 'End)] -> [(Int, (SMT2, Expr 'End))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1 :: Int)..] [(SMT2, Expr 'End)]
withQueries) (((Int, (SMT2, Expr 'End)) -> IO ()) -> IO ())
-> ((Int, (SMT2, Expr 'End)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
idx, (SMT2
q, Expr 'End
leaf)) -> do
String -> Text -> IO ()
TL.writeFile
(String
"query-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
idx String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
".smt2")
(Text
"; " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String -> Text
TL.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'End -> String
forall a. Show a => a -> String
show Expr 'End
leaf) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SMT2 -> Text
formatSMT2 SMT2
q Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\n(check-sat)")
[(CheckSatResult, Expr 'End)]
results <- (((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> [(SMT2, Expr 'End)] -> IO [(CheckSatResult, Expr 'End)])
-> [(SMT2, Expr 'End)]
-> ((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> IO [(CheckSatResult, Expr 'End)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> [(SMT2, Expr 'End)] -> IO [(CheckSatResult, Expr 'End)]
forall (t :: * -> *) a b.
Traversable t =>
(a -> IO b) -> t a -> IO (t b)
mapConcurrently [(SMT2, Expr 'End)]
withQueries (((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> IO [(CheckSatResult, Expr 'End)])
-> ((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> IO [(CheckSatResult, Expr 'End)]
forall a b. (a -> b) -> a -> b
$ \(SMT2
query, Expr 'End
leaf) -> do
CheckSatResult
res <- SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers SMT2
query
(CheckSatResult, Expr 'End) -> IO (CheckSatResult, Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckSatResult
res, Expr 'End
leaf)
let cexs :: [(CheckSatResult, Expr 'End)]
cexs = ((CheckSatResult, Expr 'End) -> Bool)
-> [(CheckSatResult, Expr 'End)] -> [(CheckSatResult, Expr 'End)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(CheckSatResult
res, Expr 'End
_) -> Bool -> Bool
not (Bool -> Bool)
-> (CheckSatResult -> Bool) -> CheckSatResult -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckSatResult -> Bool
isUnsat (CheckSatResult -> Bool) -> CheckSatResult -> Bool
forall a b. (a -> b) -> a -> b
$ CheckSatResult
res) [(CheckSatResult, Expr 'End)]
results
(Expr 'End, [VerifyResult]) -> IO (Expr 'End, [VerifyResult])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expr 'End, [VerifyResult]) -> IO (Expr 'End, [VerifyResult]))
-> (Expr 'End, [VerifyResult]) -> IO (Expr 'End, [VerifyResult])
forall a b. (a -> b) -> a -> b
$ if [(CheckSatResult, Expr 'End)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [(CheckSatResult, Expr 'End)]
cexs then (Expr 'End
expr, [() -> VerifyResult
forall a b c. a -> ProofResult a b c
Qed ()]) else (Expr 'End
expr, ((CheckSatResult, Expr 'End) -> VerifyResult)
-> [(CheckSatResult, Expr 'End)] -> [VerifyResult]
forall a b. (a -> b) -> [a] -> [b]
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 -> (Expr 'End, SMTCex) -> VerifyResult
forall a b c. b -> ProofResult a b c
Cex (Expr 'End
leaf, SMTCex
model)
CheckSatResult
EVM.Solvers.Unknown -> Expr 'End -> VerifyResult
forall a b c. c -> ProofResult a b c
Timeout Expr 'End
leaf
CheckSatResult
Unsat -> () -> VerifyResult
forall a b c. a -> ProofResult a b c
Qed ()
Error Text
e -> String -> VerifyResult
forall a. HasCallStack => String -> a
internalError (String -> VerifyResult) -> String -> VerifyResult
forall a b. (a -> b) -> a -> b
$ String
"solver responded with error: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
forall a. Show a => a -> String
show Text
e
type UnsatCache = TVar [Set Prop]
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 ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
bytecodeB of
Bool
True -> do
String -> IO ()
putStrLn String
"bytecodeA and bytecodeB are identical"
[EquivResult] -> IO [EquivResult]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [() -> EquivResult
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
SolverGroup
-> [Expr 'End] -> [Expr 'End] -> VeriOpts -> IO [EquivResult]
equivalenceCheck' SolverGroup
solvers [Expr 'End]
branchesA [Expr 'End]
branchesB VeriOpts
opts
where
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 Maybe Precondition
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 RpcInfo
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 (Expr 'End -> Expr 'End
forall (a :: EType). Expr a -> Expr a
Expr.simplify Expr 'End
expr) else Expr 'End
expr
[Expr 'End] -> IO [Expr 'End]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Expr 'End] -> IO [Expr 'End]) -> [Expr 'End] -> IO [Expr 'End]
forall a b. (a -> b) -> a -> b
$ Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
simpl
equivalenceCheck' :: SolverGroup -> [Expr End] -> [Expr End] -> VeriOpts -> IO [EquivResult]
equivalenceCheck' :: SolverGroup
-> [Expr 'End] -> [Expr 'End] -> VeriOpts -> IO [EquivResult]
equivalenceCheck' SolverGroup
solvers [Expr 'End]
branchesA [Expr 'End]
branchesB VeriOpts
opts = do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Expr 'End -> Bool) -> [Expr 'End] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr 'End -> Bool
forall (a :: EType). Expr a -> Bool
isPartial [Expr 'End]
branchesA Bool -> Bool -> Bool
|| (Expr 'End -> Bool) -> [Expr 'End] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr 'End -> Bool
forall (a :: EType). Expr a -> Bool
isPartial [Expr 'End]
branchesB) (IO () -> IO ()) -> IO () -> IO ()
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 (Text -> IO ())
-> ([PartialExec] -> Text) -> [PartialExec] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
T.unlines ([Text] -> Text)
-> ([PartialExec] -> [Text]) -> [PartialExec] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Text -> Text
indent Int
2 (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text
"- " <>)) ([Text] -> [Text])
-> ([PartialExec] -> [Text]) -> [PartialExec] -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PartialExec -> Text) -> [PartialExec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PartialExec -> Text
formatPartial ([PartialExec] -> [Text])
-> ([PartialExec] -> [PartialExec]) -> [PartialExec] -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PartialExec] -> [PartialExec]
forall a. Ord a => [a] -> [a]
nubOrd ([PartialExec] -> IO ()) -> [PartialExec] -> IO ()
forall a b. (a -> b) -> a -> b
$ (([Expr 'End] -> [PartialExec]
getPartials [Expr 'End]
branchesA) [PartialExec] -> [PartialExec] -> [PartialExec]
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 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Found " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show ([(Expr 'End, Expr 'End)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Expr 'End, Expr 'End)]
allPairs) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" total pairs of endstates"
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"endstates in bytecodeA: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show ([Expr 'End] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'End]
branchesA)
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\nendstates in bytecodeB: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show ([Expr 'End] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'End]
branchesB)
let differingEndStates :: [Set Prop]
differingEndStates = [Set Prop] -> [Set Prop]
forall a. [Set a] -> [Set a]
sortBySize (((Expr 'End, Expr 'End) -> Maybe (Set Prop))
-> [(Expr 'End, Expr 'End)] -> [Set Prop]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Expr 'End -> Expr 'End -> Maybe (Set Prop))
-> (Expr 'End, Expr 'End) -> Maybe (Set Prop)
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 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Asking the SMT solver for " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [Set Prop] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Set Prop]
differingEndStates) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" pairs"
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Set Prop, Integer)] -> ((Set Prop, Integer) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Set Prop] -> [Integer] -> [(Set Prop, Integer)]
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-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i) (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Set Prop -> String
forall a. Show a => a -> String
show Set Prop
x))
TVar [Set Prop]
knownUnsat <- [Set Prop] -> IO (TVar [Set Prop])
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 = ((EquivResult, Bool) -> Integer -> Integer)
-> Integer -> [(EquivResult, Bool)] -> Integer
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(EquivResult
_, Bool
b) Integer
n -> if Bool
b then Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1 else Integer
n) (Integer
0::Integer) [(EquivResult, Bool)]
results
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Reuse of previous queries was Useful in " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Integer -> String
forall a. Show a => a -> String
show Integer
useful) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" cases"
case (EquivResult -> Bool) -> [EquivResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all EquivResult -> Bool
forall a b c. ProofResult a b c -> Bool
isQed ([EquivResult] -> Bool)
-> ([(EquivResult, Bool)] -> [EquivResult])
-> [(EquivResult, Bool)]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((EquivResult, Bool) -> EquivResult)
-> [(EquivResult, Bool)] -> [EquivResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (EquivResult, Bool) -> EquivResult
forall a b. (a, b) -> a
fst ([(EquivResult, Bool)] -> Bool) -> [(EquivResult, Bool)] -> Bool
forall a b. (a -> b) -> a -> b
$ [(EquivResult, Bool)]
results of
Bool
True -> [EquivResult] -> IO [EquivResult]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [() -> EquivResult
forall a b c. a -> ProofResult a b c
Qed ()]
Bool
False -> [EquivResult] -> IO [EquivResult]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([EquivResult] -> IO [EquivResult])
-> [EquivResult] -> IO [EquivResult]
forall a b. (a -> b) -> a -> b
$ (EquivResult -> Bool) -> [EquivResult] -> [EquivResult]
forall a. (a -> Bool) -> [a] -> [a]
filter (EquivResult -> EquivResult -> Bool
forall a. Eq a => a -> a -> Bool
/= () -> EquivResult
forall a b c. a -> ProofResult a b c
Qed ()) ([EquivResult] -> [EquivResult])
-> ([(EquivResult, Bool)] -> [EquivResult])
-> [(EquivResult, Bool)]
-> [EquivResult]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((EquivResult, Bool) -> EquivResult)
-> [(EquivResult, Bool)] -> [EquivResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (EquivResult, Bool) -> EquivResult
forall a b. (a, b) -> a
fst ([(EquivResult, Bool)] -> [EquivResult])
-> [(EquivResult, Bool)] -> [EquivResult]
forall a b. (a -> b) -> a -> b
$ [(EquivResult, Bool)]
results
where
sortBySize :: [Set a] -> [Set a]
sortBySize :: forall a. [Set a] -> [Set a]
sortBySize = (Set a -> Set a -> Ordering) -> [Set a] -> [Set a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\Set a
a Set a
b -> if Set a -> Int
forall a. Set a -> Int
size Set a
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Set a -> Int
forall a. Set a -> Int
size Set a
b then Ordering
Prelude.LT else Ordering
Prelude.GT)
subsetAny :: Set Prop -> [Set Prop] -> Bool
subsetAny :: Set Prop -> [Set Prop] -> Bool
subsetAny Set Prop
a [Set Prop]
b = (Set Prop -> Bool -> Bool) -> Bool -> [Set Prop] -> Bool
forall a b. (a -> b -> b) -> b -> [a] -> 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
|| Set Prop -> Set Prop -> Bool
forall a. Ord a => Set a -> Set a -> Bool
isSubsetOf Set Prop
a Set Prop
bp) Bool
False [Set Prop]
b
check :: UnsatCache -> (Set Prop) -> Int -> IO (EquivResult, Bool)
check :: TVar [Set Prop] -> Set Prop -> Int -> IO (EquivResult, Bool)
check TVar [Set Prop]
knownUnsat Set Prop
props Int
idx = do
let smt :: SMT2
smt = [Prop] -> SMT2
assertProps ([Prop] -> SMT2) -> [Prop] -> SMT2
forall a b. (a -> b) -> a -> b
$ Set Prop -> [Prop]
forall a. Set a -> [a]
Set.toList Set Prop
props
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when VeriOpts
opts.debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Text -> IO ()
TL.writeFile
(String
"equiv-query-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
idx String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
".smt2") (SMT2 -> Text
formatSMT2 SMT2
smt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\n(check-sat)")
[Set Prop]
ku <- TVar [Set Prop] -> IO [Set Prop]
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 (Bool, CheckSatResult) -> IO (Bool, CheckSatResult)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, CheckSatResult
Unsat)
else ((CheckSatResult -> (Bool, CheckSatResult))
-> IO CheckSatResult -> IO (Bool, CheckSatResult)
forall a b. (a -> b) -> IO a -> IO b
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) -> (EquivResult, Bool) -> IO (EquivResult, Bool)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMTCex -> EquivResult
forall a b c. b -> ProofResult a b c
Cex SMTCex
x, Bool
False)
(Bool
quick, CheckSatResult
Unsat) ->
case Bool
quick of
Bool
True -> (EquivResult, Bool) -> IO (EquivResult, Bool)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> EquivResult
forall a b c. a -> ProofResult a b c
Qed (), Bool
quick)
Bool
False -> do
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TVar [Set Prop] -> STM [Set Prop]
forall a. TVar a -> STM a
readTVar TVar [Set Prop]
knownUnsat STM [Set Prop] -> ([Set Prop] -> STM ()) -> STM ()
forall a b. STM a -> (a -> STM b) -> STM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TVar [Set Prop] -> [Set Prop] -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar [Set Prop]
knownUnsat ([Set Prop] -> STM ())
-> ([Set Prop] -> [Set Prop]) -> [Set Prop] -> STM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Prop
props :)
(EquivResult, Bool) -> IO (EquivResult, Bool)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> EquivResult
forall a b c. a -> ProofResult a b c
Qed (), Bool
False)
(Bool
_, CheckSatResult
EVM.Solvers.Unknown) -> (EquivResult, Bool) -> IO (EquivResult, Bool)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> EquivResult
forall a b c. c -> ProofResult a b c
Timeout (), Bool
False)
(Bool
_, Error Text
txt) -> String -> IO (EquivResult, Bool)
forall a. HasCallStack => String -> a
internalError (String -> IO (EquivResult, Bool))
-> String -> IO (EquivResult, Bool)
forall a b. (a -> b) -> a -> b
$ String
"issue while running solver: `" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
txt
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 <- Int -> IO (IO (EquivResult, Bool) -> IO (EquivResult, Bool))
forall a. Int -> IO (IO a -> IO a)
pool Int
numproc
((Set Prop, Int) -> IO (EquivResult, Bool))
-> [(Set Prop, Int)] -> IO [(EquivResult, Bool)]
forall a b. (a -> IO b) -> [a] -> IO [b]
parMapIO (IO (EquivResult, Bool) -> IO (EquivResult, Bool)
wrap (IO (EquivResult, Bool) -> IO (EquivResult, Bool))
-> ((Set Prop, Int) -> IO (EquivResult, Bool))
-> (Set Prop, Int)
-> IO (EquivResult, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Set Prop -> Int -> IO (EquivResult, Bool))
-> (Set Prop, Int) -> IO (EquivResult, Bool)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Set Prop -> Int -> IO (EquivResult, Bool))
-> (Set Prop, Int) -> IO (EquivResult, Bool))
-> (Set Prop -> Int -> IO (EquivResult, Bool))
-> (Set Prop, Int)
-> IO (EquivResult, Bool)
forall a b. (a -> b) -> a -> b
$ TVar [Set Prop] -> Set Prop -> Int -> IO (EquivResult, Bool)
check TVar [Set Prop]
cache)) ([(Set Prop, Int)] -> IO [(EquivResult, Bool)])
-> [(Set Prop, Int)] -> IO [(EquivResult, Bool)]
forall a b. (a -> b) -> a -> b
$ [Set Prop] -> [Int] -> [(Set Prop, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Set Prop]
input [Int
1..]
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]
_ Traces
_ Expr 'Buf
aOut Expr 'Storage
aStore, Success [Prop]
_ Traces
_ Expr 'Buf
bOut Expr 'Storage
bStore) ->
if Expr 'Buf
aOut Expr 'Buf -> Expr 'Buf -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'Buf
bOut Bool -> Bool -> Bool
&& Expr 'Storage
aStore Expr 'Storage -> Expr 'Storage -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'Storage
bStore
then Bool -> Prop
PBool Bool
False
else Expr 'Storage
aStore Expr 'Storage -> Expr 'Storage -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Storage
bStore Prop -> Prop -> Prop
.|| Expr 'Buf
aOut Expr 'Buf -> Expr 'Buf -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Buf
bOut
(Failure [Prop]
_ Traces
_ (Revert Expr 'Buf
a), Failure [Prop]
_ Traces
_ (Revert Expr 'Buf
b)) -> if Expr 'Buf
a Expr 'Buf -> Expr 'Buf -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'Buf
b then Bool -> Prop
PBool Bool
False else Expr 'Buf
a Expr 'Buf -> Expr 'Buf -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Buf
b
(Failure [Prop]
_ Traces
_ EvmError
a, Failure [Prop]
_ Traces
_ EvmError
b) -> if EvmError
a EvmError -> EvmError -> Bool
forall a. Eq a => a -> a -> Bool
== EvmError
b then Bool -> Prop
PBool Bool
False else Bool -> Prop
PBool Bool
True
(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
_) -> String -> Prop
forall a. HasCallStack => String -> a
internalError String
"Expressions must be flattened"
(Expr 'End
_, ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_) -> String -> Prop
forall a. HasCallStack => String -> a
internalError String
"Expressions must be flattened"
(Expr 'End
a, Expr 'End
b) -> if Expr 'End
a Expr 'End -> Expr 'End -> Bool
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
PBool Bool
False -> Maybe (Set Prop)
forall a. Maybe a
Nothing
PBool Bool
True -> Set Prop -> Maybe (Set Prop)
forall a. a -> Maybe a
Just (Set Prop -> Maybe (Set Prop))
-> ([Prop] -> Set Prop) -> [Prop] -> Maybe (Set Prop)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Prop] -> Set Prop
forall a. Ord a => [a] -> Set a
Set.fromList ([Prop] -> Maybe (Set Prop)) -> [Prop] -> Maybe (Set Prop)
forall a b. (a -> b) -> a -> b
$ Expr 'End -> [Prop]
extractProps Expr 'End
aEnd [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> Expr 'End -> [Prop]
extractProps Expr 'End
bEnd
Prop
_ -> Set Prop -> Maybe (Set Prop)
forall a. a -> Maybe a
Just (Set Prop -> Maybe (Set Prop))
-> ([Prop] -> Set Prop) -> [Prop] -> Maybe (Set Prop)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Prop] -> Set Prop
forall a. Ord a => [a] -> Set a
Set.fromList ([Prop] -> Maybe (Set Prop)) -> [Prop] -> Maybe (Set Prop)
forall a b. (a -> b) -> a -> b
$ Prop
differingResults Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: Expr 'End -> [Prop]
extractProps Expr 'End
aEnd [Prop] -> [Prop] -> [Prop]
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 = (Expr 'End -> (SMT2, Expr 'End))
-> [Expr 'End] -> [(SMT2, Expr 'End)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Expr 'End
e -> ([Prop] -> SMT2
assertProps ([Prop] -> SMT2) -> (Expr 'End -> [Prop]) -> Expr 'End -> SMT2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'End -> [Prop]
extractProps (Expr 'End -> SMT2) -> Expr 'End -> SMT2
forall a b. (a -> b) -> a -> b
$ Expr 'End
e, Expr 'End
e)) [Expr 'End]
flattened
[(CheckSatResult, Expr 'End)]
results <- (((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> [(SMT2, Expr 'End)] -> IO [(CheckSatResult, Expr 'End)])
-> [(SMT2, Expr 'End)]
-> ((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> IO [(CheckSatResult, Expr 'End)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> [(SMT2, Expr 'End)] -> IO [(CheckSatResult, Expr 'End)]
forall (t :: * -> *) a b.
Traversable t =>
(a -> IO b) -> t a -> IO (t b)
mapConcurrently [(SMT2, Expr 'End)]
withQueries (((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> IO [(CheckSatResult, Expr 'End)])
-> ((SMT2, Expr 'End) -> IO (CheckSatResult, Expr 'End))
-> IO [(CheckSatResult, Expr 'End)]
forall a b. (a -> b) -> a -> b
$ \(SMT2
query, Expr 'End
leaf) -> do
CheckSatResult
res <- SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers SMT2
query
(CheckSatResult, Expr 'End) -> IO (CheckSatResult, Expr 'End)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckSatResult
res, Expr 'End
leaf)
[(Expr 'End, CheckSatResult)] -> IO [(Expr 'End, CheckSatResult)]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Expr 'End, CheckSatResult)] -> IO [(Expr 'End, CheckSatResult)])
-> [(Expr 'End, CheckSatResult)]
-> IO [(Expr 'End, CheckSatResult)]
forall a b. (a -> b) -> a -> b
$ ((CheckSatResult, Expr 'End) -> (Expr 'End, CheckSatResult))
-> [(CheckSatResult, Expr 'End)] -> [(Expr 'End, CheckSatResult)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CheckSatResult, Expr 'End) -> (Expr 'End, CheckSatResult)
forall a b. (a, b) -> (b, a)
swap ([(CheckSatResult, Expr 'End)] -> [(Expr 'End, CheckSatResult)])
-> [(CheckSatResult, Expr 'End)] -> [(Expr 'End, CheckSatResult)]
forall a b. (a -> b) -> a -> b
$ ((CheckSatResult, Expr 'End) -> Bool)
-> [(CheckSatResult, Expr 'End)] -> [(CheckSatResult, Expr 'End)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(CheckSatResult
res, Expr 'End
_) -> Bool -> Bool
not (Bool -> Bool)
-> (CheckSatResult -> Bool) -> CheckSatResult -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckSatResult -> Bool
isUnsat (CheckSatResult -> Bool) -> CheckSatResult -> Bool
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 -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Error Text
e -> String -> IO ()
forall a. HasCallStack => String -> a
internalError (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"smt solver returned an error: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
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 (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indent Int
2 (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'End -> Text
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 (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indent Int
2 (Text -> Text) -> Text -> Text
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 (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
indent Int
2 (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'End -> Text
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 ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$
[ Text
"Calldata:"
, Int -> Text -> Text
indent Int
2 Text
cd'
, Text
""
]
[Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
storeCex
[Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
txCtx
[Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
blockCtx
where
cd' :: Text
cd' = Expr 'Buf -> Text
prettyBuf (Expr 'Buf -> Text) -> Expr 'Buf -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
Expr.simplify (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ SMTCex -> Expr 'Buf -> Expr 'Buf
forall (a :: EType). SMTCex -> Expr a -> Expr a
subModel SMTCex
m Expr 'Buf
cd
storeCex :: [Text]
storeCex :: [Text]
storeCex
| Map W256 (Map W256 W256) -> Bool
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 (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (W256 -> Map W256 W256 -> [Text] -> [Text])
-> [Text] -> Map W256 (Map W256 W256) -> [Text]
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 " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Addr -> String
forall a. Show a => a -> String
show (W256 -> Addr
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
key :: Addr))
Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ [(W256, W256)] -> String
forall a. Show a => a -> String
show (Map W256 W256 -> [(W256, W256)]
forall k a. Map k a -> [(k, a)]
Map.toList Map W256 W256
val))) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
acc
) [Text]
forall a. Monoid a => a
mempty Map W256 (Map W256 W256)
store
, Text
""
]
txCtx :: [Text]
txCtx :: [Text]
txCtx
| Map (Expr 'EWord) W256 -> Bool
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 (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Expr 'EWord -> W256 -> [Text] -> [Text])
-> [Text] -> Map (Expr 'EWord) W256 -> [Text]
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 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ W256 -> String
forall a. Show a => a -> String
show W256
val)) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
acc
) [Text]
forall a. Monoid a => a
mempty (Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
filterSubCtx Map (Expr 'EWord) W256
txContext)
, Text
""
]
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 (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> String
forall a. Show a => a -> String
show Expr 'EWord
x
filterSubCtx :: Map (Expr EWord) W256 -> Map (Expr EWord) W256
filterSubCtx :: Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
filterSubCtx = (Expr 'EWord -> W256 -> Bool)
-> Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
go (Caller Int
x) W256
_ = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
go (Address Int
x) W256
_ = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
go (Balance {}) W256
_ = String -> Bool
forall a. HasCallStack => String -> a
internalError String
"TODO: BALANCE"
go (SelfBalance {}) W256
_ = String -> Bool
forall a. HasCallStack => String -> a
internalError String
"TODO: SELFBALANCE"
go (Gas {}) W256
_ = String -> Bool
forall a. HasCallStack => String -> a
internalError String
"TODO: Gas"
go Expr 'EWord
_ W256
_ = Bool
False
blockCtx :: [Text]
blockCtx :: [Text]
blockCtx
| Map (Expr 'EWord) W256 -> Bool
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 (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Expr 'EWord -> W256 -> [Text] -> [Text])
-> [Text] -> Map (Expr 'EWord) W256 -> [Text]
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 (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> String
forall a. Show a => a -> String
show Expr 'EWord
key String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
": " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> W256 -> String
forall a. Show a => a -> String
show W256
val) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
acc
) [Text]
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"
subModel :: SMTCex -> Expr a -> Expr a
subModel :: forall (a :: EType). SMTCex -> Expr a -> Expr a
subModel SMTCex
c Expr a
expr =
Map (Expr 'Buf) ByteString -> Expr a -> Expr a
forall {a :: EType}. Map (Expr 'Buf) ByteString -> Expr a -> Expr a
subBufs ((BufModel -> ByteString)
-> Map (Expr 'Buf) BufModel -> Map (Expr 'Buf) ByteString
forall a b. (a -> b) -> Map (Expr 'Buf) a -> Map (Expr 'Buf) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BufModel -> ByteString
forceFlattened SMTCex
c.buffers) (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Expr 'EWord) W256 -> Expr a -> Expr a
forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars SMTCex
c.vars (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map W256 (Map W256 W256) -> Expr a -> Expr a
forall (a :: EType). Map W256 (Map W256 W256) -> Expr a -> Expr a
subStore SMTCex
c.store
(Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Expr 'EWord) W256 -> Expr a -> Expr a
forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars SMTCex
c.blockContext (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Expr 'EWord) W256 -> Expr a -> Expr a
forall {a :: EType}. Map (Expr 'EWord) W256 -> Expr a -> Expr a
subVars SMTCex
c.txContext (Expr a -> Expr a) -> Expr a -> Expr a
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 (BufModel -> ByteString) -> BufModel -> ByteString
forall a b. (a -> b) -> a -> b
$
BufModel -> Maybe BufModel -> BufModel
forall a. a -> Maybe a -> a
fromMaybe (String -> BufModel
forall a. HasCallStack => String -> a
internalError (String -> BufModel) -> String -> BufModel
forall a b. (a -> b) -> a -> b
$ String
"cannot flatten buffer: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> BufModel -> String
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 = (Expr a -> Expr 'EWord -> W256 -> Expr a)
-> Expr a -> Map (Expr 'EWord) W256 -> Expr a
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey Expr a -> Expr 'EWord -> W256 -> Expr a
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 (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
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 Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
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 = (Expr a -> Expr 'Buf -> ByteString -> Expr a)
-> Expr a -> Map (Expr 'Buf) ByteString -> Expr a
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey Expr a -> Expr 'Buf -> ByteString -> Expr a
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 (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
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 Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
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 (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
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