{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-}

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.ST (RealWorld, stToIO, ST)
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.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Map.Merge.Strict 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.Tree.Zipper qualified as Zipper
import Data.Tuple (swap)
import EVM (makeVm, abstractContract, 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, showVal, bsToHex)
import EVM.SMT (SMTCex(..), SMT2(..), assertProps)
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.FeeSchedule (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)
import EVM.Effects
import Control.Monad.IO.Unlift

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 -> [Char]
(Int -> LoopHeuristic -> ShowS)
-> (LoopHeuristic -> [Char])
-> ([LoopHeuristic] -> ShowS)
-> Show LoopHeuristic
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LoopHeuristic -> ShowS
showsPrec :: Int -> LoopHeuristic -> ShowS
$cshow :: LoopHeuristic -> [Char]
show :: LoopHeuristic -> [Char]
$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 [Char]
-> Parser [LoopHeuristic]
Maybe Text
-> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser LoopHeuristic
(Maybe Text
 -> Maybe Text
 -> Maybe Char
 -> Maybe [Char]
 -> Parser LoopHeuristic)
-> (Maybe Text
    -> Maybe Text
    -> Maybe Char
    -> Maybe [Char]
    -> Parser [LoopHeuristic])
-> ReadM LoopHeuristic
-> (forall (proxy :: * -> *). proxy LoopHeuristic -> [Char])
-> ParseField LoopHeuristic
forall a.
(Maybe Text
 -> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser a)
-> (Maybe Text
    -> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser [a])
-> ReadM a
-> (forall (proxy :: * -> *). proxy a -> [Char])
-> ParseField a
forall (proxy :: * -> *). proxy LoopHeuristic -> [Char]
$cparseField :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser LoopHeuristic
parseField :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser LoopHeuristic
$cparseListOfField :: Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe [Char]
-> Parser [LoopHeuristic]
parseListOfField :: Maybe Text
-> Maybe Text
-> Maybe Char
-> Maybe [Char]
-> Parser [LoopHeuristic]
$creadField :: ReadM LoopHeuristic
readField :: ReadM LoopHeuristic
$cmetavar :: forall (proxy :: * -> *). proxy LoopHeuristic -> [Char]
metavar :: forall (proxy :: * -> *). proxy LoopHeuristic -> [Char]
ParseField, ParseRecord LoopHeuristic
Maybe Text
-> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser LoopHeuristic
ParseRecord LoopHeuristic
-> (Maybe Text
    -> Maybe Text
    -> Maybe Char
    -> Maybe [Char]
    -> Parser LoopHeuristic)
-> ParseFields LoopHeuristic
forall a.
ParseRecord a
-> (Maybe Text
    -> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser a)
-> ParseFields a
$cparseFields :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe [Char] -> Parser LoopHeuristic
parseFields :: Maybe Text
-> Maybe Text -> Maybe Char -> Maybe [Char] -> 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 -> [Char]
(Int -> ProofResult a b c -> ShowS)
-> (ProofResult a b c -> [Char])
-> ([ProofResult a b c] -> ShowS)
-> Show (ProofResult a b c)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([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 -> [Char]
$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 -> [Char]
show :: ProofResult a b c -> [Char]
$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 -> 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 -> [Char]
(Int -> VeriOpts -> ShowS)
-> (VeriOpts -> [Char]) -> ([VeriOpts] -> ShowS) -> Show VeriOpts
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VeriOpts -> ShowS
showsPrec :: Int -> VeriOpts -> ShowS
$cshow :: VeriOpts -> [Char]
show :: VeriOpts -> [Char]
$cshowList :: [VeriOpts] -> ShowS
showList :: [VeriOpts] -> ShowS
Show)

defaultVeriOpts :: VeriOpts
defaultVeriOpts :: VeriOpts
defaultVeriOpts = VeriOpts
  { $sel:simp:VeriOpts :: Bool
simp = Bool
True
  , $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 }

extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
extractCex :: VerifyResult -> Maybe (Expr 'End, SMTCex)
extractCex (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))

-- | Abstract calldata argument generation
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 [Char] -> CalldataFragment
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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
    -- TODO: is this correct?
    then let v :: Expr 'EWord
v = Text -> Expr 'EWord
Var Text
name in [Prop] -> Expr 'EWord -> CalldataFragment
St [Int -> Expr 'EWord -> Prop
Expr.inRange Int
n Expr 'EWord
v] Expr 'EWord
v
    else [Char] -> CalldataFragment
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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 -> [Prop] -> Expr 'EWord -> CalldataFragment
St [] (Expr 'EAddr -> Expr 'EWord
WAddr (Text -> Expr 'EAddr
SymAddr Text
name))
  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 [Char] -> CalldataFragment
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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) [[Char] -> Text
T.pack (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n) | Int
n <- [Int
0..Int
szInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
  AbiType
t -> [Char] -> CalldataFragment
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> CalldataFragment) -> [Char] -> CalldataFragment
forall a b. (a -> b) -> a -> b
$ [Char]
"TODO: symbolic abi encoding for " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> AbiType -> [Char]
forall a. Show a => a -> [Char]
show AbiType
t

data CalldataFragment
  = St [Prop] (Expr EWord)
  | Dy [Prop] (Expr EWord) (Expr Buf)
  | Comp [CalldataFragment]
  deriving (Int -> CalldataFragment -> ShowS
[CalldataFragment] -> ShowS
CalldataFragment -> [Char]
(Int -> CalldataFragment -> ShowS)
-> (CalldataFragment -> [Char])
-> ([CalldataFragment] -> ShowS)
-> Show CalldataFragment
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CalldataFragment -> ShowS
showsPrec :: Int -> CalldataFragment -> ShowS
$cshow :: CalldataFragment -> [Char]
show :: CalldataFragment -> [Char]
$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)

-- | Generates calldata matching given type signature, optionally specialized
-- with concrete arguments.
-- Any argument given as "<symbolic>" or omitted at the tail of the list are
-- kept symbolic.
symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> (Expr Buf, [Prop])
symCalldata :: Text -> [AbiType] -> [[Char]] -> Expr 'Buf -> (Expr 'Buf, [Prop])
symCalldata Text
sig [AbiType]
typesignature [[Char]]
concreteArgs Expr 'Buf
base =
  let
    args :: [[Char]]
args = [[Char]]
concreteArgs [[Char]] -> [[Char]] -> [[Char]]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char] -> [[Char]]
forall a. Int -> a -> [a]
replicate ([AbiType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AbiType]
typesignature Int -> Int -> Int
forall a. Num a => a -> a -> a
- [[Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
concreteArgs) [Char]
"<symbolic>"
    mkArg :: AbiType -> String -> Int -> CalldataFragment
    mkArg :: AbiType -> [Char] -> Int -> CalldataFragment
mkArg AbiType
typ [Char]
"<symbolic>" Int
n = Text -> AbiType -> CalldataFragment
symAbiArg ([Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char]
"arg" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n) AbiType
typ
    mkArg AbiType
typ [Char]
arg Int
_ =
      case AbiType -> [Char] -> AbiValue
makeAbiValue AbiType
typ [Char]
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
_ -> [Char] -> CalldataFragment
forall a. HasCallStack => [Char] -> a
internalError [Char]
"TODO"
    calldatas :: [CalldataFragment]
calldatas = (AbiType -> [Char] -> Int -> CalldataFragment)
-> [AbiType] -> [[Char]] -> [Int] -> [CalldataFragment]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 AbiType -> [Char] -> Int -> CalldataFragment
mkArg [AbiType]
typesignature [[Char]]
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
                   Comp [CalldataFragment]
xs | (CalldataFragment -> Bool) -> [CalldataFragment] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all CalldataFragment -> Bool
isSt [CalldataFragment]
xs -> Expr 'EWord -> [CalldataFragment] -> Expr 'EWord
go Expr 'EWord
acc ([CalldataFragment]
xs [CalldataFragment] -> [CalldataFragment] -> [CalldataFragment]
forall a. Semigroup a => a -> a -> a
<> [CalldataFragment]
tl)
                   CalldataFragment
_ -> [Char] -> Expr 'EWord
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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
        -- static fragments get written as a word in place
        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)
        -- compound fragments that contain only static fragments get written in place
        Comp [CalldataFragment]
xs | (CalldataFragment -> Bool) -> [CalldataFragment] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all CalldataFragment -> Bool
isSt [CalldataFragment]
xs -> Expr 'EWord
-> [CalldataFragment] -> (Expr 'Buf, [Prop]) -> (Expr 'Buf, [Prop])
go Expr 'EWord
idx ([CalldataFragment]
xs [CalldataFragment] -> [CalldataFragment] -> [CalldataFragment]
forall a. Semigroup a => a -> a -> a
<> [CalldataFragment]
rest) (Expr 'Buf
buf,[Prop]
ps)
        -- dynamic fragments are not yet supported... :/
        CalldataFragment
s -> [Char] -> (Expr 'Buf, [Prop])
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> (Expr 'Buf, [Prop])) -> [Char] -> (Expr 'Buf, [Prop])
forall a b. (a -> b) -> a -> b
$ [Char]
"unsupported cd fragment: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> CalldataFragment -> [Char]
forall a. Show a => a -> [Char]
show CalldataFragment
s

isSt :: CalldataFragment -> Bool
isSt :: CalldataFragment -> Bool
isSt (St {}) = Bool
True
isSt CalldataFragment
_ = Bool
False


abstractVM
  :: (Expr Buf, [Prop])
  -> ByteString
  -> Maybe (Precondition s)
  -> Bool
  -> ST s (VM Symbolic s)
abstractVM :: forall s.
(Expr 'Buf, [Prop])
-> ByteString
-> Maybe (Precondition s)
-> Bool
-> ST s (VM 'Symbolic s)
abstractVM (Expr 'Buf, [Prop])
cd ByteString
contractCode Maybe (Precondition s)
maybepre Bool
create = do
  let value :: Expr 'EWord
value = Expr 'EWord
TxValue
  let code :: ContractCode
code = if Bool
create then ByteString -> Expr 'Buf -> ContractCode
InitCode ByteString
contractCode ((Expr 'Buf, [Prop]) -> Expr 'Buf
forall a b. (a, b) -> a
fst (Expr 'Buf, [Prop])
cd) else RuntimeCode -> ContractCode
RuntimeCode (ByteString -> RuntimeCode
ConcreteRuntimeCode ByteString
contractCode)
  VM 'Symbolic s
vm <- ContractCode
-> Expr 'EWord
-> (Expr 'Buf, [Prop])
-> Bool
-> ST s (VM 'Symbolic s)
forall s.
ContractCode
-> Expr 'EWord
-> (Expr 'Buf, [Prop])
-> Bool
-> ST s (VM 'Symbolic s)
loadSymVM ContractCode
code Expr 'EWord
value (if Bool
create then (Expr 'Buf, [Prop])
forall a. Monoid a => a
mempty else (Expr 'Buf, [Prop])
cd) Bool
create
  let precond :: [Prop]
precond = case Maybe (Precondition s)
maybepre of
                Maybe (Precondition s)
Nothing -> []
                Just Precondition s
p -> [Precondition s
p VM 'Symbolic s
vm]
  VM 'Symbolic s -> ST s (VM 'Symbolic s)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VM 'Symbolic s -> ST s (VM 'Symbolic s))
-> VM 'Symbolic s -> ST s (VM 'Symbolic s)
forall a b. (a -> b) -> a -> b
$ VM 'Symbolic s
vm VM 'Symbolic s
-> (VM 'Symbolic s -> VM 'Symbolic s) -> VM 'Symbolic s
forall a b. a -> (a -> b) -> b
& Optic A_Lens NoIx (VM 'Symbolic s) (VM 'Symbolic s) [Prop] [Prop]
-> ([Prop] -> [Prop]) -> VM 'Symbolic s -> VM 'Symbolic s
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 'Symbolic s) (VM 'Symbolic s) [Prop] [Prop]
#constraints ([Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
precond)

loadSymVM
  :: ContractCode
  -> Expr EWord
  -> (Expr Buf, [Prop])
  -> Bool
  -> ST s (VM Symbolic s)
loadSymVM :: forall s.
ContractCode
-> Expr 'EWord
-> (Expr 'Buf, [Prop])
-> Bool
-> ST s (VM 'Symbolic s)
loadSymVM ContractCode
x Expr 'EWord
callvalue (Expr 'Buf, [Prop])
cd Bool
create =
  (VMOpts 'Symbolic -> ST s (VM 'Symbolic s)
forall (t :: VMType) s. VMOps t => VMOpts t -> ST s (VM t s)
makeVm (VMOpts 'Symbolic -> ST s (VM 'Symbolic s))
-> VMOpts 'Symbolic -> ST s (VM 'Symbolic s)
forall a b. (a -> b) -> a -> b
$ VMOpts
    { $sel:contract:VMOpts :: Contract
contract = if Bool
create then ContractCode -> Contract
initialContract ContractCode
x else ContractCode -> Expr 'EAddr -> Contract
abstractContract ContractCode
x (Text -> Expr 'EAddr
SymAddr Text
"entrypoint")
    , $sel:otherContracts:VMOpts :: [(Expr 'EAddr, Contract)]
otherContracts = []
    , $sel:calldata:VMOpts :: (Expr 'Buf, [Prop])
calldata = (Expr 'Buf, [Prop])
cd
    , $sel:value:VMOpts :: Expr 'EWord
value = Expr 'EWord
callvalue
    , $sel:baseState:VMOpts :: BaseState
baseState = BaseState
AbstractBase
    , $sel:address:VMOpts :: Expr 'EAddr
address = Text -> Expr 'EAddr
SymAddr Text
"entrypoint"
    , $sel:caller:VMOpts :: Expr 'EAddr
caller = Text -> Expr 'EAddr
SymAddr Text
"caller"
    , $sel:origin:VMOpts :: Expr 'EAddr
origin = Text -> Expr 'EAddr
SymAddr Text
"origin"
    , $sel:coinbase:VMOpts :: Expr 'EAddr
coinbase = Text -> Expr 'EAddr
SymAddr Text
"coinbase"
    , $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 :: Gas 'Symbolic
gas = ()
    , $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
    , $sel:chainId:VMOpts :: W256
chainId = W256
1
    , $sel:create:VMOpts :: Bool
create = Bool
create
    , $sel:txAccessList:VMOpts :: Map (Expr 'EAddr) [W256]
txAccessList = Map (Expr 'EAddr) [W256]
forall a. Monoid a => a
mempty
    , $sel:allowFFI:VMOpts :: Bool
allowFFI = Bool
False
    })

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

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

  eval (Action 'Symbolic RealWorld b
action Operational.:>>= b -> Stepper 'Symbolic RealWorld (Expr 'End)
k) =
    case Action 'Symbolic RealWorld b
action of
      Action 'Symbolic RealWorld b
Stepper.Exec -> do
        (VMResult 'Symbolic RealWorld
r, VM 'Symbolic RealWorld
vm') <- IO (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
-> m (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
 -> m (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld))
-> IO (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
-> m (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
-> IO (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST
   RealWorld (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
 -> IO (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld))
-> ST
     RealWorld (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
-> IO (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ StateT
  (VM 'Symbolic RealWorld)
  (ST RealWorld)
  (VMResult 'Symbolic RealWorld)
-> VM 'Symbolic RealWorld
-> ST
     RealWorld (VMResult 'Symbolic RealWorld, VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT
  (VM 'Symbolic RealWorld)
  (ST RealWorld)
  (VMResult 'Symbolic RealWorld)
forall (t :: VMType) s. VMOps t => EVM t s (VMResult t s)
exec VM 'Symbolic RealWorld
vm
        Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm' (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
VMResult 'Symbolic RealWorld
r)
      Stepper.IOAct IO b
q -> do
        b
r <- IO b -> m b
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO b
q
        Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
r)
      Stepper.Ask (PleaseChoosePath Expr 'EWord
cond Bool -> EVM 'Symbolic RealWorld ()
continue) -> do
        IO (Expr 'End)
evalLeft <- m (Expr 'End) -> m (IO (Expr 'End))
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (IO a)
toIO (m (Expr 'End) -> m (IO (Expr 'End)))
-> m (Expr 'End) -> m (IO (Expr 'End))
forall a b. (a -> b) -> a -> b
$ do
          (()
ra, VM 'Symbolic RealWorld
vma) <- IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld))
-> IO ((), VM 'Symbolic RealWorld)
-> m ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM 'Symbolic RealWorld)
 -> IO ((), VM 'Symbolic RealWorld))
-> ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld ()
-> VM 'Symbolic RealWorld
-> ST RealWorld ((), VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool -> EVM 'Symbolic RealWorld ()
continue Bool
True) VM 'Symbolic RealWorld
vm { $sel:result:VM :: Maybe (VMResult 'Symbolic RealWorld)
result = Maybe (VMResult 'Symbolic RealWorld)
forall a. Maybe a
Nothing }
          Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vma (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
()
ra)
        IO (Expr 'End)
evalRight <- m (Expr 'End) -> m (IO (Expr 'End))
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (IO a)
toIO (m (Expr 'End) -> m (IO (Expr 'End)))
-> m (Expr 'End) -> m (IO (Expr 'End))
forall a b. (a -> b) -> a -> b
$ do
          (()
rb, VM 'Symbolic RealWorld
vmb) <- IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld))
-> IO ((), VM 'Symbolic RealWorld)
-> m ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM 'Symbolic RealWorld)
 -> IO ((), VM 'Symbolic RealWorld))
-> ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld ()
-> VM 'Symbolic RealWorld
-> ST RealWorld ((), VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool -> EVM 'Symbolic RealWorld ()
continue Bool
False) VM 'Symbolic RealWorld
vm { $sel:result:VM :: Maybe (VMResult 'Symbolic RealWorld)
result = Maybe (VMResult 'Symbolic RealWorld)
forall a. Maybe a
Nothing }
          Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vmb (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
()
rb)
        (Expr 'End
a, Expr 'End
b) <- IO (Expr 'End, Expr 'End) -> m (Expr 'End, Expr 'End)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr 'End, Expr 'End) -> m (Expr 'End, Expr 'End))
-> IO (Expr 'End, Expr 'End) -> m (Expr 'End, Expr 'End)
forall a b. (a -> b) -> a -> b
$ IO (Expr 'End) -> IO (Expr 'End) -> IO (Expr 'End, Expr 'End)
forall a b. IO a -> IO b -> IO (a, b)
concurrently IO (Expr 'End)
evalLeft IO (Expr 'End)
evalRight
        Expr 'End -> m (Expr 'End)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> m (Expr 'End)) -> Expr 'End -> m (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 'Symbolic RealWorld
q -> do
        let performQuery :: m (Expr 'End)
performQuery = do
              EVM 'Symbolic RealWorld ()
m <- Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Query 'Symbolic RealWorld
q
              (()
r, VM 'Symbolic RealWorld
vm') <- IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO(IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld))
-> IO ((), VM 'Symbolic RealWorld)
-> m ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM 'Symbolic RealWorld)
 -> IO ((), VM 'Symbolic RealWorld))
-> ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld ()
-> VM 'Symbolic RealWorld
-> ST RealWorld ((), VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT EVM 'Symbolic RealWorld ()
m VM 'Symbolic RealWorld
vm
              Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm' (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
()
r)

        case Query 'Symbolic RealWorld
q of
          PleaseAskSMT Expr 'EWord
cond [Prop]
preconds BranchCondition -> EVM 'Symbolic RealWorld ()
continue -> do
            let
              -- no concretiziation here, or we may lose information
              simpProps :: [Prop]
simpProps = [Prop] -> [Prop]
Expr.simplifyProps ((Expr 'EWord
cond Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= W256 -> Expr 'EWord
Lit W256
0)Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop]
preconds)
            case Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
Expr.concKeccakSimpExpr Expr 'EWord
cond of
              -- is the condition concrete?
              Lit W256
c ->
                -- have we reached max iterations, are we inside a loop?
                case (VM 'Symbolic RealWorld -> Maybe Integer -> Maybe Bool
forall s. VM 'Symbolic s -> Maybe Integer -> Maybe Bool
maxIterationsReached VM 'Symbolic RealWorld
vm Maybe Integer
maxIter, LoopHeuristic -> VM 'Symbolic RealWorld -> Maybe Bool
forall s. LoopHeuristic -> VM 'Symbolic s -> Maybe Bool
isLoopHead LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm) of
                  -- Yes. return a partial leaf
                  (Just Bool
_, Just Bool
True) ->
                    Expr 'End -> m (Expr 'End)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> m (Expr 'End)) -> Expr 'End -> m (Expr 'End)
forall a b. (a -> b) -> a -> b
$ [Prop] -> Traces -> PartialExec -> Expr 'End
Partial [] (Forest Trace -> Map (Expr 'EAddr) Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM 'Symbolic RealWorld
vm.traces) VM 'Symbolic RealWorld
vm.env.contracts) (PartialExec -> Expr 'End) -> PartialExec -> Expr 'End
forall a b. (a -> b) -> a -> b
$ Int -> Expr 'EAddr -> PartialExec
MaxIterationsReached VM 'Symbolic RealWorld
vm.state.pc VM 'Symbolic RealWorld
vm.state.contract
                  -- No. keep executing
                  (Maybe Bool, Maybe Bool)
_ -> do
                    (()
r, VM 'Symbolic RealWorld
vm') <- IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld))
-> IO ((), VM 'Symbolic RealWorld)
-> m ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM 'Symbolic RealWorld)
 -> IO ((), VM 'Symbolic RealWorld))
-> ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld ()
-> VM 'Symbolic RealWorld
-> ST RealWorld ((), VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (BranchCondition -> EVM 'Symbolic RealWorld ()
continue (Bool -> BranchCondition
Case (W256
c W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0))) VM 'Symbolic RealWorld
vm
                    Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm' (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
()
r)

              -- the condition is symbolic
              Expr 'EWord
_ ->
                -- are in we a loop, have we hit maxIters, have we hit askSmtIters?
                case (LoopHeuristic -> VM 'Symbolic RealWorld -> Maybe Bool
forall s. LoopHeuristic -> VM 'Symbolic s -> Maybe Bool
isLoopHead LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm, VM 'Symbolic RealWorld -> Integer -> Bool
forall s. VM 'Symbolic s -> Integer -> Bool
askSmtItersReached VM 'Symbolic RealWorld
vm Integer
askSmtIters, VM 'Symbolic RealWorld -> Maybe Integer -> Maybe Bool
forall s. VM 'Symbolic s -> Maybe Integer -> Maybe Bool
maxIterationsReached VM 'Symbolic RealWorld
vm Maybe Integer
maxIter) of
                  -- we're in a loop and maxIters has been reached
                  (Just Bool
True, Bool
_, Just Bool
n) -> do
                    -- continue execution down the opposite branch than the one that
                    -- got us to this point and return a partial leaf for the other side
                    (()
r, VM 'Symbolic RealWorld
vm') <- IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld))
-> IO ((), VM 'Symbolic RealWorld)
-> m ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM 'Symbolic RealWorld)
 -> IO ((), VM 'Symbolic RealWorld))
-> ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld ()
-> VM 'Symbolic RealWorld
-> ST RealWorld ((), VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (BranchCondition -> EVM 'Symbolic RealWorld ()
continue (Bool -> BranchCondition
Case (Bool -> BranchCondition) -> Bool -> BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
n)) VM 'Symbolic RealWorld
vm
                    Expr 'End
a <- Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm' (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
()
r)
                    Expr 'End -> m (Expr 'End)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> m (Expr 'End)) -> Expr 'End -> m (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 [] (Forest Trace -> Map (Expr 'EAddr) Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM 'Symbolic RealWorld
vm.traces) VM 'Symbolic RealWorld
vm.env.contracts) (Int -> Expr 'EAddr -> PartialExec
MaxIterationsReached VM 'Symbolic RealWorld
vm.state.pc VM 'Symbolic RealWorld
vm.state.contract))
                  -- we're in a loop and askSmtIters has been reached
                  (Just Bool
True, Bool
True, Maybe Bool
_) ->
                    -- ask the smt solver about the loop condition
                    m (Expr 'End)
performQuery
                  (Maybe Bool, Bool, Maybe Bool)
_ -> do
                    (()
r, VM 'Symbolic RealWorld
vm') <- case [Prop]
simpProps of
                      -- if we can statically determine unsatisfiability then we skip exploring the jump
                      [PBool Bool
False] -> IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld))
-> IO ((), VM 'Symbolic RealWorld)
-> m ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM 'Symbolic RealWorld)
 -> IO ((), VM 'Symbolic RealWorld))
-> ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld ()
-> VM 'Symbolic RealWorld
-> ST RealWorld ((), VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (BranchCondition -> EVM 'Symbolic RealWorld ()
continue (Bool -> BranchCondition
Case Bool
False)) VM 'Symbolic RealWorld
vm
                      -- otherwise we explore both branches
                      [Prop]
_ -> IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ((), VM 'Symbolic RealWorld) -> m ((), VM 'Symbolic RealWorld))
-> IO ((), VM 'Symbolic RealWorld)
-> m ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM 'Symbolic RealWorld)
 -> IO ((), VM 'Symbolic RealWorld))
-> ST RealWorld ((), VM 'Symbolic RealWorld)
-> IO ((), VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld ()
-> VM 'Symbolic RealWorld
-> ST RealWorld ((), VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (BranchCondition -> EVM 'Symbolic RealWorld ()
continue BranchCondition
EVM.Types.Unknown) VM 'Symbolic RealWorld
vm
                    Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm' (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
()
r)
          Query 'Symbolic RealWorld
_ -> m (Expr 'End)
performQuery

      Stepper.EVM EVM 'Symbolic RealWorld b
m -> do
        (b
r, VM 'Symbolic RealWorld
vm') <- IO (b, VM 'Symbolic RealWorld) -> m (b, VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (b, VM 'Symbolic RealWorld) -> m (b, VM 'Symbolic RealWorld))
-> IO (b, VM 'Symbolic RealWorld) -> m (b, VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (b, VM 'Symbolic RealWorld)
-> IO (b, VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (b, VM 'Symbolic RealWorld)
 -> IO (b, VM 'Symbolic RealWorld))
-> ST RealWorld (b, VM 'Symbolic RealWorld)
-> IO (b, VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Symbolic RealWorld b
-> VM 'Symbolic RealWorld
-> ST RealWorld (b, VM 'Symbolic RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT EVM 'Symbolic RealWorld b
m VM 'Symbolic RealWorld
vm
        Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret Fetcher 'Symbolic m RealWorld
Query 'Symbolic RealWorld -> m (EVM 'Symbolic RealWorld ())
fetcher Maybe Integer
maxIter Integer
askSmtIters LoopHeuristic
heuristic VM 'Symbolic RealWorld
vm' (b -> Stepper 'Symbolic RealWorld (Expr 'End)
k b
r)

maxIterationsReached :: VM Symbolic s -> Maybe Integer -> Maybe Bool
maxIterationsReached :: forall s. VM 'Symbolic s -> Maybe Integer -> Maybe Bool
maxIterationsReached VM 'Symbolic s
_ Maybe Integer
Nothing = Maybe Bool
forall a. Maybe a
Nothing
maxIterationsReached VM 'Symbolic s
vm (Just Integer
maxIter) =
  let codelocation :: CodeLocation
codelocation = VM 'Symbolic s -> CodeLocation
forall (t :: VMType) s. VM t s -> CodeLocation
getCodeLocation VM 'Symbolic s
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 'Symbolic s
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 'Symbolic s
vm.cache.path
     else Maybe Bool
forall a. Maybe a
Nothing

askSmtItersReached :: VM Symbolic s -> Integer -> Bool
askSmtItersReached :: forall s. VM 'Symbolic s -> Integer -> Bool
askSmtItersReached VM 'Symbolic s
vm Integer
askSmtIters = let
    codelocation :: CodeLocation
codelocation = VM 'Symbolic s -> CodeLocation
forall (t :: VMType) s. VM t s -> CodeLocation
getCodeLocation VM 'Symbolic s
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 'Symbolic s
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

{- | Loop head detection heuristic

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

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

 This heuristic is not perfect, and can certainly be tricked, but should generally be good enough for most compiler generated and non pathological user generated loops.
 -}
isLoopHead :: LoopHeuristic -> VM Symbolic s -> Maybe Bool
isLoopHead :: forall s. LoopHeuristic -> VM 'Symbolic s -> Maybe Bool
isLoopHead LoopHeuristic
Naive VM 'Symbolic s
_ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
isLoopHead LoopHeuristic
StackBased VM 'Symbolic s
vm = let
    loc :: CodeLocation
loc = VM 'Symbolic s -> CodeLocation
forall (t :: VMType) s. VM t s -> CodeLocation
getCodeLocation VM 'Symbolic s
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 'Symbolic s
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 'Symbolic s -> Int -> Bool
forall (t :: VMType) s. VM t s -> Int -> Bool
isValidJumpDest VM 'Symbolic s
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 'Symbolic s
vm.state.stack
       Maybe (Int, [Expr 'EWord])
Nothing -> Maybe Bool
forall a. Maybe a
Nothing

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

checkAssert
  :: App m
  => SolverGroup
  -> [Word256]
  -> ByteString
  -> Maybe Sig
  -> [String]
  -> VeriOpts
  -> m (Expr End, [VerifyResult])
checkAssert :: forall (m :: * -> *).
App m =>
SolverGroup
-> [Word256]
-> ByteString
-> Maybe Sig
-> [[Char]]
-> VeriOpts
-> m (Expr 'End, [VerifyResult])
checkAssert SolverGroup
solvers [Word256]
errs ByteString
c Maybe Sig
signature' [[Char]]
concreteArgs VeriOpts
opts =
  SolverGroup
-> ByteString
-> Maybe Sig
-> [[Char]]
-> VeriOpts
-> Maybe (Precondition RealWorld)
-> Maybe (Postcondition RealWorld)
-> m (Expr 'End, [VerifyResult])
forall (m :: * -> *).
App m =>
SolverGroup
-> ByteString
-> Maybe Sig
-> [[Char]]
-> VeriOpts
-> Maybe (Precondition RealWorld)
-> Maybe (Postcondition RealWorld)
-> m (Expr 'End, [VerifyResult])
verifyContract SolverGroup
solvers ByteString
c Maybe Sig
signature' [[Char]]
concreteArgs VeriOpts
opts Maybe (Precondition RealWorld)
forall a. Maybe a
Nothing (Postcondition RealWorld -> Maybe (Postcondition RealWorld)
forall a. a -> Maybe a
Just (Postcondition RealWorld -> Maybe (Postcondition RealWorld))
-> Postcondition RealWorld -> Maybe (Postcondition RealWorld)
forall a b. (a -> b) -> a -> b
$ [Word256] -> Postcondition RealWorld
forall s. [Word256] -> Postcondition s
checkAssertions [Word256]
errs)

getExpr
  :: App m
  => SolverGroup
  -> ByteString
  -> Maybe Sig
  -> [String]
  -> VeriOpts
  -> m (Expr End)
getExpr :: forall (m :: * -> *).
App m =>
SolverGroup
-> ByteString -> Maybe Sig -> [[Char]] -> VeriOpts -> m (Expr 'End)
getExpr SolverGroup
solvers ByteString
c Maybe Sig
signature' [[Char]]
concreteArgs VeriOpts
opts = do
      VM 'Symbolic RealWorld
preState <- IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld))
-> IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (VM 'Symbolic RealWorld)
-> IO (VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (VM 'Symbolic RealWorld)
 -> IO (VM 'Symbolic RealWorld))
-> ST RealWorld (VM 'Symbolic RealWorld)
-> IO (VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ (Expr 'Buf, [Prop])
-> ByteString
-> Maybe (Precondition RealWorld)
-> Bool
-> ST RealWorld (VM 'Symbolic RealWorld)
forall s.
(Expr 'Buf, [Prop])
-> ByteString
-> Maybe (Precondition s)
-> Bool
-> ST s (VM 'Symbolic s)
abstractVM (Maybe Sig -> [[Char]] -> (Expr 'Buf, [Prop])
mkCalldata Maybe Sig
signature' [[Char]]
concreteArgs) ByteString
c Maybe (Precondition RealWorld)
forall a. Maybe a
Nothing Bool
False
      Expr 'End
exprInter <- Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher 'Symbolic m RealWorld
forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
Fetch.oracle SolverGroup
solvers VeriOpts
opts.rpcInfo) VeriOpts
opts.maxIter VeriOpts
opts.askSmtIters VeriOpts
opts.loopHeuristic VM 'Symbolic RealWorld
preState Stepper 'Symbolic RealWorld (Expr 'End)
runExpr
      if VeriOpts
opts.simp then (Expr 'End -> m (Expr 'End)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> m (Expr 'End)) -> Expr 'End -> m (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 -> m (Expr 'End)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr 'End
exprInter

{- | Checks if an assertion violation has been encountered

  hevm recognises the following as an assertion violation:

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

  see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require
-}
checkAssertions :: [Word256] -> Postcondition s
checkAssertions :: forall s. [Word256] -> Postcondition s
checkAssertions [Word256]
errs VM 'Symbolic s
_ = \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

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

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

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

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

verifyContract
  :: App m
  => SolverGroup
  -> ByteString
  -> Maybe Sig
  -> [String]
  -> VeriOpts
  -> Maybe (Precondition RealWorld)
  -> Maybe (Postcondition RealWorld)
  -> m (Expr End, [VerifyResult])
verifyContract :: forall (m :: * -> *).
App m =>
SolverGroup
-> ByteString
-> Maybe Sig
-> [[Char]]
-> VeriOpts
-> Maybe (Precondition RealWorld)
-> Maybe (Postcondition RealWorld)
-> m (Expr 'End, [VerifyResult])
verifyContract SolverGroup
solvers ByteString
theCode Maybe Sig
signature' [[Char]]
concreteArgs VeriOpts
opts Maybe (Precondition RealWorld)
maybepre Maybe (Postcondition RealWorld)
maybepost = do
  VM 'Symbolic RealWorld
preState <- IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld))
-> IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (VM 'Symbolic RealWorld)
-> IO (VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (VM 'Symbolic RealWorld)
 -> IO (VM 'Symbolic RealWorld))
-> ST RealWorld (VM 'Symbolic RealWorld)
-> IO (VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ (Expr 'Buf, [Prop])
-> ByteString
-> Maybe (Precondition RealWorld)
-> Bool
-> ST RealWorld (VM 'Symbolic RealWorld)
forall s.
(Expr 'Buf, [Prop])
-> ByteString
-> Maybe (Precondition s)
-> Bool
-> ST s (VM 'Symbolic s)
abstractVM (Maybe Sig -> [[Char]] -> (Expr 'Buf, [Prop])
mkCalldata Maybe Sig
signature' [[Char]]
concreteArgs) ByteString
theCode Maybe (Precondition RealWorld)
maybepre Bool
False
  SolverGroup
-> VeriOpts
-> VM 'Symbolic RealWorld
-> Maybe (Postcondition RealWorld)
-> m (Expr 'End, [VerifyResult])
forall (m :: * -> *).
App m =>
SolverGroup
-> VeriOpts
-> VM 'Symbolic RealWorld
-> Maybe (Postcondition RealWorld)
-> m (Expr 'End, [VerifyResult])
verify SolverGroup
solvers VeriOpts
opts VM 'Symbolic RealWorld
preState Maybe (Postcondition RealWorld)
maybepost

-- | Stepper that parses the result of Stepper.runFully into an Expr End
runExpr :: Stepper.Stepper Symbolic RealWorld (Expr End)
runExpr :: Stepper 'Symbolic RealWorld (Expr 'End)
runExpr = do
  VM 'Symbolic RealWorld
vm <- Stepper 'Symbolic RealWorld (VM 'Symbolic RealWorld)
forall (t :: VMType) s. Stepper t s (VM t s)
Stepper.runFully
  let traces :: Traces
traces = Forest Trace -> Map (Expr 'EAddr) Contract -> Traces
Traces (TreePos Empty Trace -> Forest Trace
forall (t :: * -> *) a. PosType t => TreePos t a -> Forest a
Zipper.toForest VM 'Symbolic RealWorld
vm.traces) VM 'Symbolic RealWorld
vm.env.contracts
  Expr 'End -> Stepper 'Symbolic RealWorld (Expr 'End)
forall a. a -> ProgramT (Action 'Symbolic RealWorld) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'End -> Stepper 'Symbolic RealWorld (Expr 'End))
-> Expr 'End -> Stepper 'Symbolic RealWorld (Expr 'End)
forall a b. (a -> b) -> a -> b
$ case VM 'Symbolic RealWorld
vm.result of
    Just (VMSuccess Expr 'Buf
buf) -> [Prop]
-> Traces
-> Expr 'Buf
-> Map (Expr 'EAddr) (Expr 'EContract)
-> Expr 'End
Success VM 'Symbolic RealWorld
vm.constraints Traces
traces Expr 'Buf
buf ((Contract -> Expr 'EContract)
-> Map (Expr 'EAddr) Contract
-> Map (Expr 'EAddr) (Expr 'EContract)
forall a b. (a -> b) -> Map (Expr 'EAddr) a -> Map (Expr 'EAddr) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Contract -> Expr 'EContract
toEContract VM 'Symbolic RealWorld
vm.env.contracts)
    Just (VMFailure EvmError
e) -> [Prop] -> Traces -> EvmError -> Expr 'End
Failure VM 'Symbolic RealWorld
vm.constraints Traces
traces EvmError
e
    Just (Unfinished PartialExec
p) -> [Prop] -> Traces -> PartialExec -> Expr 'End
Partial VM 'Symbolic RealWorld
vm.constraints Traces
traces PartialExec
p
    Maybe (VMResult 'Symbolic RealWorld)
_ -> [Char] -> Expr 'End
forall a. HasCallStack => [Char] -> a
internalError [Char]
"vm in intermediate state after call to runFully"

toEContract :: Contract -> Expr EContract
toEContract :: Contract -> Expr 'EContract
toEContract Contract
c = ContractCode
-> Expr 'Storage -> Expr 'EWord -> Maybe W64 -> Expr 'EContract
C Contract
c.code Contract
c.storage Contract
c.balance Contract
c.nonce

-- | Converts a given top level expr into a list of final states and the
-- associated path conditions for each state.
flattenExpr :: Expr End -> [Expr End]
flattenExpr :: Expr 'End -> [Expr 'End]
flattenExpr = [Prop] -> Expr 'End -> [Expr 'End]
go []
  where
    go :: [Prop] -> Expr End -> [Expr End]
    go :: [Prop] -> Expr 'End -> [Expr 'End]
go [Prop]
pcs = \case
      ITE Expr 'EWord
c Expr 'End
t Expr 'End
f -> [Prop] -> Expr 'End -> [Expr 'End]
go (Prop -> Prop
PNeg ((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 Map (Expr 'EAddr) (Expr 'EContract)
store -> [[Prop]
-> Traces
-> Expr 'Buf
-> Map (Expr 'EAddr) (Expr 'EContract)
-> Expr 'End
Success ([Prop] -> [Prop]
forall a. Ord a => [a] -> [a]
nubOrd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) Traces
trace Expr 'Buf
msg Map (Expr 'EAddr) (Expr 'EContract)
store]
      Failure [Prop]
ps Traces
trace EvmError
e -> [[Prop] -> Traces -> EvmError -> Expr 'End
Failure ([Prop] -> [Prop]
forall a. Ord a => [a] -> [a]
nubOrd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [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] -> [Prop]
forall a. Ord a => [a] -> [a]
nubOrd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
pcs) Traces
trace PartialExec
p]
      GVar GVar 'End
_ -> [Char] -> [Expr 'End]
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot flatten an Expr containing a GVar"

-- | Strips unreachable branches from a given expr
-- Returns a list of executed SMT queries alongside the reduced expression for debugging purposes
-- Note that the reduced expression loses information relative to the original
-- one if jump conditions are removed. This restriction can be removed once
-- Expr supports attaching knowledge to AST nodes.
-- Although this algorithm currently parallelizes nicely, it does not exploit
-- the incremental nature of the task at hand. Introducing support for
-- incremental queries might let us go even faster here.
-- TODO: handle errors properly
reachable :: App m => SolverGroup -> Expr End -> m ([SMT2], Expr End)
reachable :: forall (m :: * -> *).
App m =>
SolverGroup -> Expr 'End -> m ([SMT2], Expr 'End)
reachable SolverGroup
solvers Expr 'End
e = do
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  ([SMT2], Maybe (Expr 'End))
res <- IO ([SMT2], Maybe (Expr 'End)) -> m ([SMT2], Maybe (Expr 'End))
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ([SMT2], Maybe (Expr 'End)) -> m ([SMT2], Maybe (Expr 'End)))
-> IO ([SMT2], Maybe (Expr 'End)) -> m ([SMT2], Maybe (Expr 'End))
forall a b. (a -> b) -> a -> b
$ Config -> [Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go Config
conf [] Expr 'End
e
  ([SMT2], Expr 'End) -> m ([SMT2], Expr 'End)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([SMT2], Expr 'End) -> m ([SMT2], Expr 'End))
-> ([SMT2], Expr 'End) -> m ([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 ([Char] -> Expr 'End
forall a. HasCallStack => [Char] -> a
internalError [Char]
"no reachable paths found")) ([SMT2], Maybe (Expr 'End))
res
  where
    {-
       Walk down the tree and collect pcs.
       Dispatch a reachability query at each leaf.
       If reachable return the expr wrapped in a Just. If not return Nothing.
       When walking back up the tree drop unreachable subbranches.
    -}
    go :: Config -> [Prop] -> Expr End -> IO ([SMT2], Maybe (Expr End))
    go :: Config -> [Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go Config
conf [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
          (Config -> [Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go Config
conf (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)
          (Config -> [Prop] -> Expr 'End -> IO ([SMT2], Maybe (Expr 'End))
go Config
conf (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 = Config -> [Prop] -> SMT2
assertProps Config
conf [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 -> [Char] -> IO ([SMT2], Maybe (Expr 'End))
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> IO ([SMT2], Maybe (Expr 'End)))
-> [Char] -> IO ([SMT2], Maybe (Expr 'End))
forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid solver result: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> CheckSatResult -> [Char]
forall a. Show a => a -> [Char]
show CheckSatResult
r

-- | Extract constraints stored in Expr End nodes
extractProps :: Expr End -> [Prop]
extractProps :: Expr 'End -> [Prop]
extractProps = \case
  ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_ -> []
  Success [Prop]
asserts Traces
_ Expr 'Buf
_ Map (Expr 'EAddr) (Expr 'EContract)
_ -> [Prop]
asserts
  Failure [Prop]
asserts Traces
_ EvmError
_ -> [Prop]
asserts
  Partial [Prop]
asserts Traces
_ PartialExec
_ -> [Prop]
asserts
  GVar GVar 'End
_ -> [Char] -> [Prop]
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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

-- | Symbolically execute the VM and check all endstates against the
-- postcondition, if available.
verify
  :: App m
  => SolverGroup
  -> VeriOpts
  -> VM Symbolic RealWorld
  -> Maybe (Postcondition RealWorld)
  -> m (Expr End, [VerifyResult])
verify :: forall (m :: * -> *).
App m =>
SolverGroup
-> VeriOpts
-> VM 'Symbolic RealWorld
-> Maybe (Postcondition RealWorld)
-> m (Expr 'End, [VerifyResult])
verify SolverGroup
solvers VeriOpts
opts VM 'Symbolic RealWorld
preState Maybe (Postcondition RealWorld)
maybepost = do
  IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn [Char]
"Exploring contract"

  Expr 'End
exprInter <- Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher 'Symbolic m RealWorld
forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
Fetch.oracle SolverGroup
solvers VeriOpts
opts.rpcInfo) VeriOpts
opts.maxIter VeriOpts
opts.askSmtIters VeriOpts
opts.loopHeuristic VM 'Symbolic RealWorld
preState Stepper 'Symbolic RealWorld (Expr 'End)
runExpr
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpExprs (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Text -> IO ()
T.writeFile [Char]
"unsimplified.expr" (Expr 'End -> Text
forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
exprInter)
  IO (Expr 'End, [VerifyResult]) -> m (Expr 'End, [VerifyResult])
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr 'End, [VerifyResult]) -> m (Expr 'End, [VerifyResult]))
-> IO (Expr 'End, [VerifyResult]) -> m (Expr 'End, [VerifyResult])
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> IO ()
putStrLn [Char]
"Simplifying expression"
    let expr :: Expr 'End
expr = if VeriOpts
opts.simp then (Expr 'End -> Expr 'End
forall (a :: EType). Expr a -> Expr a
Expr.simplify Expr 'End
exprInter) else Expr 'End
exprInter
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpExprs (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Text -> IO ()
T.writeFile [Char]
"simplified.expr" (Expr 'End -> Text
forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
expr)

    [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Explored contract (" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show (Expr 'End -> Int
Expr.numBranches Expr 'End
expr) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" 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 RealWorld)
maybepost of
      Maybe (Postcondition RealWorld)
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 RealWorld
post -> IO (Expr 'End, [VerifyResult]) -> IO (Expr 'End, [VerifyResult])
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr 'End, [VerifyResult]) -> IO (Expr 'End, [VerifyResult]))
-> IO (Expr 'End, [VerifyResult]) -> IO (Expr 'End, [VerifyResult])
forall a b. (a -> b) -> a -> b
$ do
        let
          -- Filter out any leaves from `flattened` that can be statically shown to be safe
          tocheck :: [([Prop], Expr 'End)]
tocheck = ((Expr 'End -> ([Prop], Expr 'End))
 -> [Expr 'End] -> [([Prop], Expr 'End)])
-> [Expr 'End]
-> (Expr 'End -> ([Prop], Expr 'End))
-> [([Prop], Expr 'End)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Expr 'End -> ([Prop], Expr 'End))
-> [Expr 'End] -> [([Prop], Expr 'End)]
forall a b. (a -> b) -> [a] -> [b]
map [Expr 'End]
flattened ((Expr 'End -> ([Prop], Expr 'End)) -> [([Prop], Expr 'End)])
-> (Expr 'End -> ([Prop], Expr 'End)) -> [([Prop], Expr 'End)]
forall a b. (a -> b) -> a -> b
$ \Expr 'End
leaf -> (Expr 'End -> [Prop] -> Postcondition RealWorld -> [Prop]
toPropsFinal Expr 'End
leaf VM 'Symbolic RealWorld
preState.constraints Postcondition RealWorld
post, Expr 'End
leaf)
          withQueries :: [(SMT2, Expr 'End)]
withQueries = (([Prop], Expr 'End) -> Bool)
-> [([Prop], Expr 'End)] -> [([Prop], Expr 'End)]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Prop], Expr 'End) -> Bool
forall {b}. ([Prop], b) -> Bool
canBeSat [([Prop], Expr 'End)]
tocheck [([Prop], Expr 'End)]
-> (([Prop], Expr 'End) -> (SMT2, Expr 'End))
-> [(SMT2, Expr 'End)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \([Prop]
a, Expr 'End
leaf) -> (Config -> [Prop] -> SMT2
assertProps Config
conf [Prop]
a, Expr 'End
leaf)
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Checking for reachability of "
                     [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show ([(SMT2, Expr 'End)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SMT2, Expr 'End)]
withQueries)
                     [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" potential property violation(s)"

        -- Dispatch the remaining branches to the solver to check for violations
        [(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
    toProps :: Expr 'End -> [Prop] -> Postcondition RealWorld -> [Prop]
toProps Expr 'End
leaf [Prop]
constr Postcondition RealWorld
post = Prop -> Prop
PNeg (Postcondition RealWorld
post VM 'Symbolic RealWorld
preState Expr 'End
leaf) Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
constr [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> Expr 'End -> [Prop]
extractProps Expr 'End
leaf
    toPropsFinal :: Expr 'End -> [Prop] -> Postcondition RealWorld -> [Prop]
toPropsFinal Expr 'End
leaf [Prop]
constr Postcondition RealWorld
post = if VeriOpts
opts.simp then [Prop] -> [Prop]
Expr.simplifyProps ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ Expr 'End -> [Prop] -> Postcondition RealWorld -> [Prop]
toProps Expr 'End
leaf [Prop]
constr Postcondition RealWorld
post
                                                 else Expr 'End -> [Prop] -> Postcondition RealWorld -> [Prop]
toProps Expr 'End
leaf [Prop]
constr Postcondition RealWorld
post
    canBeSat :: ([Prop], b) -> Bool
canBeSat ([Prop]
a, b
_) = case [Prop]
a of
        [PBool Bool
False] -> Bool
False
        [Prop]
_ -> Bool
True
    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, VM 'Symbolic RealWorld -> SMTCex -> SMTCex
forall s. VM 'Symbolic s -> SMTCex -> SMTCex
expandCex VM 'Symbolic RealWorld
preState 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 -> [Char] -> VerifyResult
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> VerifyResult) -> [Char] -> VerifyResult
forall a b. (a -> b) -> a -> b
$ [Char]
"solver responded with error: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
forall a. Show a => a -> [Char]
show Text
e

expandCex :: VM Symbolic s -> SMTCex -> SMTCex
expandCex :: forall s. VM 'Symbolic s -> SMTCex -> SMTCex
expandCex VM 'Symbolic s
prestate SMTCex
c = SMTCex
c { $sel:store:SMTCex :: Map (Expr 'EAddr) (Map W256 W256)
store = Map (Expr 'EAddr) (Map W256 W256)
-> Map (Expr 'EAddr) (Map W256 W256)
-> Map (Expr 'EAddr) (Map W256 W256)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union SMTCex
c.store Map (Expr 'EAddr) (Map W256 W256)
concretePreStore }
  where
    concretePreStore :: Map (Expr 'EAddr) (Map W256 W256)
concretePreStore = (Contract -> Maybe (Map W256 W256))
-> Map (Expr 'EAddr) Contract -> Map (Expr 'EAddr) (Map W256 W256)
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (Expr 'Storage -> Maybe (Map W256 W256)
maybeConcreteStore (Expr 'Storage -> Maybe (Map W256 W256))
-> (Contract -> Expr 'Storage) -> Contract -> Maybe (Map W256 W256)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (.storage))
                     (Map (Expr 'EAddr) Contract -> Map (Expr 'EAddr) (Map W256 W256))
-> (Map (Expr 'EAddr) Contract -> Map (Expr 'EAddr) Contract)
-> Map (Expr 'EAddr) Contract
-> Map (Expr 'EAddr) (Map W256 W256)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Contract -> Bool)
-> Map (Expr 'EAddr) Contract -> Map (Expr 'EAddr) Contract
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\Contract
v -> (forall (a :: EType). Expr a -> Bool) -> Expr 'Storage -> Bool
forall (b :: EType).
(forall (a :: EType). Expr a -> Bool) -> Expr b -> Bool
Expr.containsNode Expr a -> Bool
forall (a :: EType). Expr a -> Bool
isConcreteStore Contract
v.storage)
                     (Map (Expr 'EAddr) Contract -> Map (Expr 'EAddr) (Map W256 W256))
-> Map (Expr 'EAddr) Contract -> Map (Expr 'EAddr) (Map W256 W256)
forall a b. (a -> b) -> a -> b
$ (VM 'Symbolic s
prestate.env.contracts)
    isConcreteStore :: Expr a -> Bool
isConcreteStore = \case
      ConcreteStore Map W256 W256
_ -> Bool
True
      Expr a
_ -> Bool
False

type UnsatCache = TVar [Set Prop]

-- | Compares two contract runtimes for trace equivalence by running two VMs
-- and comparing the end states.
--
-- We do this by asking the solver to find a common input for each pair of
-- endstates that satisfies the path conditions for both sides and produces a
-- differing output. If we can find such an input, then we have a clear
-- equivalence break, and since we run this check for every pair of end states,
-- the check is exhaustive.
equivalenceCheck
  :: forall m . App m
  => SolverGroup
  -> ByteString
  -> ByteString
  -> VeriOpts
  -> (Expr Buf, [Prop])
  -> m [EquivResult]
equivalenceCheck :: forall (m :: * -> *).
App m =>
SolverGroup
-> ByteString
-> ByteString
-> VeriOpts
-> (Expr 'Buf, [Prop])
-> m [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 -> IO [EquivResult] -> m [EquivResult]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [EquivResult] -> m [EquivResult])
-> IO [EquivResult] -> m [EquivResult]
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> IO ()
putStrLn [Char]
"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 -> m [Expr 'End]
getBranches ByteString
bytecodeA
      [Expr 'End]
branchesB <- ByteString -> m [Expr 'End]
getBranches ByteString
bytecodeB
      SolverGroup -> [Expr 'End] -> [Expr 'End] -> m [EquivResult]
forall (m :: * -> *).
App m =>
SolverGroup -> [Expr 'End] -> [Expr 'End] -> m [EquivResult]
equivalenceCheck' SolverGroup
solvers [Expr 'End]
branchesA [Expr 'End]
branchesB
  where
    -- decompiles the given bytecode into a list of branches
    getBranches :: ByteString -> m [Expr End]
    getBranches :: ByteString -> m [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
      VM 'Symbolic RealWorld
prestate <- IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld))
-> IO (VM 'Symbolic RealWorld) -> m (VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (VM 'Symbolic RealWorld)
-> IO (VM 'Symbolic RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (VM 'Symbolic RealWorld)
 -> IO (VM 'Symbolic RealWorld))
-> ST RealWorld (VM 'Symbolic RealWorld)
-> IO (VM 'Symbolic RealWorld)
forall a b. (a -> b) -> a -> b
$ (Expr 'Buf, [Prop])
-> ByteString
-> Maybe (Precondition RealWorld)
-> Bool
-> ST RealWorld (VM 'Symbolic RealWorld)
forall s.
(Expr 'Buf, [Prop])
-> ByteString
-> Maybe (Precondition s)
-> Bool
-> ST s (VM 'Symbolic s)
abstractVM (Expr 'Buf, [Prop])
calldata ByteString
bytecode Maybe (Precondition RealWorld)
forall a. Maybe a
Nothing Bool
False
      Expr 'End
expr <- Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
forall (m :: * -> *).
App m =>
Fetcher 'Symbolic m RealWorld
-> Maybe Integer
-> Integer
-> LoopHeuristic
-> VM 'Symbolic RealWorld
-> Stepper 'Symbolic RealWorld (Expr 'End)
-> m (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher 'Symbolic m RealWorld
forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
Fetch.oracle SolverGroup
solvers RpcInfo
forall a. Maybe a
Nothing) VeriOpts
opts.maxIter VeriOpts
opts.askSmtIters VeriOpts
opts.loopHeuristic VM 'Symbolic RealWorld
prestate Stepper 'Symbolic RealWorld (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] -> m [Expr 'End]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Expr 'End] -> m [Expr 'End]) -> [Expr 'End] -> m [Expr 'End]
forall a b. (a -> b) -> a -> b
$ Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
simpl


equivalenceCheck'
  :: forall m . App m
  => SolverGroup -> [Expr End] -> [Expr End] -> m [EquivResult]
equivalenceCheck' :: forall (m :: * -> *).
App m =>
SolverGroup -> [Expr 'End] -> [Expr 'End] -> m [EquivResult]
equivalenceCheck' SolverGroup
solvers [Expr 'End]
branchesA [Expr 'End]
branchesB = do
      Bool -> m () -> m ()
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) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> IO ()
putStrLn [Char]
""
        [Char] -> IO ()
putStrLn [Char]
"WARNING: hevm was only able to partially explore the given contract due to the following issues:"
        [Char] -> IO ()
putStrLn [Char]
""
        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]
      IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Found " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show ([(Expr 'End, Expr 'End)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Expr 'End, Expr 'End)]
allPairs) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" total pairs of endstates"

      Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpEndStates (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"endstates in bytecodeA: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show ([Expr 'End] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'End]
branchesA)
                   [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\nendstates in bytecodeB: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
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)
      IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Asking the SMT solver for " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> [Char]) -> Int -> [Char]
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) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" pairs"
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpEndStates (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [(Set Prop, Integer)] -> ((Set Prop, Integer) -> m ()) -> m ()
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) ->
        IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Text -> IO ()
T.writeFile ([Char]
"prop-checked-" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
i [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
".prop") ([Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Set Prop -> [Char]
forall a. Show a => a -> [Char]
show Set Prop
x))

      TVar [Set Prop]
knownUnsat <- IO (TVar [Set Prop]) -> m (TVar [Set Prop])
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (TVar [Set Prop]) -> m (TVar [Set Prop]))
-> IO (TVar [Set Prop]) -> m (TVar [Set Prop])
forall a b. (a -> b) -> a -> b
$ [Set Prop] -> IO (TVar [Set Prop])
forall a. a -> IO (TVar a)
newTVarIO []
      Int
procs <- IO Int -> m Int
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO Int
getNumProcessors
      [(EquivResult, Bool)]
results <- [Set Prop] -> TVar [Set Prop] -> Int -> m [(EquivResult, Bool)]
App m =>
[Set Prop] -> TVar [Set Prop] -> Int -> m [(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
      IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Reuse of previous queries was Useful in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
useful) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" 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] -> m [EquivResult]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [() -> EquivResult
forall a b c. a -> ProofResult a b c
Qed ()]
        Bool
False -> [EquivResult] -> m [EquivResult]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([EquivResult] -> m [EquivResult])
-> [EquivResult] -> m [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
    -- we order the sets by size because this gives us more cache hits when
    -- running our queries later on (since we rely on a subset check)
    sortBySize :: [Set a] -> [Set a]
    sortBySize :: forall a. [Set a] -> [Set a]
sortBySize = (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)

    -- returns True if a is a subset of any of the sets in b
    subsetAny :: Set Prop -> [Set Prop] -> Bool
    subsetAny :: Set Prop -> [Set Prop] -> Bool
subsetAny Set Prop
a [Set Prop]
b = (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

    -- checks for satisfiability of all the props in the provided set. skips
    -- the solver if we can determine unsatisfiability from the cache already
    -- the last element of the returned tuple indicates whether the cache was
    -- used or not
    check :: Config -> UnsatCache -> (Set Prop) -> IO (EquivResult, Bool)
    check :: Config -> TVar [Set Prop] -> Set Prop -> IO (EquivResult, Bool)
check Config
conf TVar [Set Prop]
knownUnsat Set Prop
props = do
      let smt :: SMT2
smt = Config -> [Prop] -> SMT2
assertProps Config
conf (Set Prop -> [Prop]
forall a. Set a -> [a]
Set.toList Set Prop
props)
      [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
              -- nb: we might end up with duplicates here due to a
              -- potential race, but it doesn't matter for correctness
              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) -> [Char] -> IO (EquivResult, Bool)
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> IO (EquivResult, Bool))
-> [Char] -> IO (EquivResult, Bool)
forall a b. (a -> b) -> a -> b
$ [Char]
"solver returned: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Text -> [Char]
T.unpack Text
txt)

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


    -- Takes two branches and returns a set of props that will need to be
    -- satisfied for the two branches to violate the equivalence check. i.e.
    -- for a given pair of branches, equivalence is violated if there exists an
    -- input that satisfies the branch conditions from both sides and produces
    -- a differing result in each branch
    distinct :: Expr End -> Expr End -> Maybe (Set Prop)
    distinct :: Expr 'End -> Expr 'End -> Maybe (Set Prop)
distinct Expr 'End
aEnd Expr 'End
bEnd =
      case Expr 'End -> Expr 'End -> Prop
resultsDiffer Expr 'End
aEnd Expr 'End
bEnd of
        -- if the end states are the same, then they can never produce a
        -- different result under any circumstances
        PBool Bool
False -> Maybe (Set Prop)
forall a. Maybe a
Nothing
        -- if we can statically determine that the end states differ, then we
        -- ask the solver to find us inputs that satisfy both sets of branch
        -- conditions
        PBool Bool
True  -> 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
        -- if we cannot statically determine whether or not the end states
        -- differ, then we ask the solver if the end states can differ if both
        -- sets of path conditions are satisfiable
        Prop
_ -> 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 -> Expr 'End -> Prop
resultsDiffer Expr 'End
aEnd Expr 'End
bEnd 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

    resultsDiffer :: Expr End -> Expr End -> Prop
    resultsDiffer :: Expr 'End -> Expr 'End -> Prop
resultsDiffer Expr 'End
aEnd Expr 'End
bEnd = case (Expr 'End
aEnd, Expr 'End
bEnd) of
      (Success [Prop]
_ Traces
_ Expr 'Buf
aOut Map (Expr 'EAddr) (Expr 'EContract)
aState, Success [Prop]
_ Traces
_ Expr 'Buf
bOut Map (Expr 'EAddr) (Expr 'EContract)
bState) ->
        case (Expr 'Buf
aOut Expr 'Buf -> Expr 'Buf -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'Buf
bOut, Map (Expr 'EAddr) (Expr 'EContract)
aState Map (Expr 'EAddr) (Expr 'EContract)
-> Map (Expr 'EAddr) (Expr 'EContract) -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Expr 'EAddr) (Expr 'EContract)
bState) of
          (Bool
True, Bool
True) -> Bool -> Prop
PBool Bool
False
          (Bool
False, Bool
True) -> Expr 'Buf
aOut Expr 'Buf -> Expr 'Buf -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Buf
bOut
          (Bool
True, Bool
False) -> Map (Expr 'EAddr) (Expr 'EContract)
-> Map (Expr 'EAddr) (Expr 'EContract) -> Prop
statesDiffer Map (Expr 'EAddr) (Expr 'EContract)
aState Map (Expr 'EAddr) (Expr 'EContract)
bState
          (Bool
False, Bool
False) -> Map (Expr 'EAddr) (Expr 'EContract)
-> Map (Expr 'EAddr) (Expr 'EContract) -> Prop
statesDiffer Map (Expr 'EAddr) (Expr 'EContract)
aState Map (Expr 'EAddr) (Expr 'EContract)
bState 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 end states can't be compared to actual end states, so we always ignore them
      (Partial {}, Expr 'End
_) -> Bool -> Prop
PBool Bool
False
      (Expr 'End
_, Partial {}) -> Bool -> Prop
PBool Bool
False
      (ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_, Expr 'End
_) -> [Char] -> Prop
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Expressions must be flattened"
      (Expr 'End
_, ITE Expr 'EWord
_ Expr 'End
_ Expr 'End
_) -> [Char] -> Prop
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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

    statesDiffer :: Map (Expr EAddr) (Expr EContract) -> Map (Expr EAddr) (Expr EContract) -> Prop
    statesDiffer :: Map (Expr 'EAddr) (Expr 'EContract)
-> Map (Expr 'EAddr) (Expr 'EContract) -> Prop
statesDiffer Map (Expr 'EAddr) (Expr 'EContract)
aState Map (Expr 'EAddr) (Expr 'EContract)
bState
      = if [Expr 'EAddr] -> Set (Expr 'EAddr)
forall a. Ord a => [a] -> Set a
Set.fromList (Map (Expr 'EAddr) (Expr 'EContract) -> [Expr 'EAddr]
forall k a. Map k a -> [k]
Map.keys Map (Expr 'EAddr) (Expr 'EContract)
aState) Set (Expr 'EAddr) -> Set (Expr 'EAddr) -> Bool
forall a. Eq a => a -> a -> Bool
/= [Expr 'EAddr] -> Set (Expr 'EAddr)
forall a. Ord a => [a] -> Set a
Set.fromList (Map (Expr 'EAddr) (Expr 'EContract) -> [Expr 'EAddr]
forall k a. Map k a -> [k]
Map.keys Map (Expr 'EAddr) (Expr 'EContract)
bState)
        -- TODO: consider possibility of aliased symbolic addresses
        then Bool -> Prop
PBool Bool
True
        else let
          merged :: Map (Expr 'EAddr) (Expr 'EContract, Expr 'EContract)
merged = (SimpleWhenMissing
  (Expr 'EAddr) (Expr 'EContract) (Expr 'EContract, Expr 'EContract)
-> SimpleWhenMissing
     (Expr 'EAddr) (Expr 'EContract) (Expr 'EContract, Expr 'EContract)
-> SimpleWhenMatched
     (Expr 'EAddr)
     (Expr 'EContract)
     (Expr 'EContract)
     (Expr 'EContract, Expr 'EContract)
-> Map (Expr 'EAddr) (Expr 'EContract)
-> Map (Expr 'EAddr) (Expr 'EContract)
-> Map (Expr 'EAddr) (Expr 'EContract, Expr 'EContract)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
Map.merge SimpleWhenMissing
  (Expr 'EAddr) (Expr 'EContract) (Expr 'EContract, Expr 'EContract)
forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
Map.dropMissing SimpleWhenMissing
  (Expr 'EAddr) (Expr 'EContract) (Expr 'EContract, Expr 'EContract)
forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
Map.dropMissing ((Expr 'EAddr
 -> Expr 'EContract
 -> Expr 'EContract
 -> (Expr 'EContract, Expr 'EContract))
-> SimpleWhenMatched
     (Expr 'EAddr)
     (Expr 'EContract)
     (Expr 'EContract)
     (Expr 'EContract, Expr 'EContract)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
Map.zipWithMatched (\Expr 'EAddr
_ Expr 'EContract
x Expr 'EContract
y -> (Expr 'EContract
x,Expr 'EContract
y))) Map (Expr 'EAddr) (Expr 'EContract)
aState Map (Expr 'EAddr) (Expr 'EContract)
bState)
        in (Prop -> (Expr 'EContract, Expr 'EContract) -> Prop)
-> Prop
-> Map (Expr 'EAddr) (Expr 'EContract, Expr 'EContract)
-> Prop
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' (\Prop
a (Expr 'EContract
ac, Expr 'EContract
bc) -> Prop
a Prop -> Prop -> Prop
.|| Expr 'EContract -> Expr 'EContract -> Prop
contractsDiffer Expr 'EContract
ac Expr 'EContract
bc) (Bool -> Prop
PBool Bool
False) Map (Expr 'EAddr) (Expr 'EContract, Expr 'EContract)
merged

    contractsDiffer :: Expr EContract -> Expr EContract -> Prop
    contractsDiffer :: Expr 'EContract -> Expr 'EContract -> Prop
contractsDiffer Expr 'EContract
ac Expr 'EContract
bc = let
        balsDiffer :: Prop
balsDiffer = case (Expr 'EContract
ac.balance, Expr 'EContract
bc.balance) of
          (Lit W256
ab, Lit W256
bb) -> Bool -> Prop
PBool (Bool -> Prop) -> Bool -> Prop
forall a b. (a -> b) -> a -> b
$ W256
ab W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
bb
          (Expr 'EWord
ab, Expr 'EWord
bb) -> if Expr 'EWord
ab Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
bb then Bool -> Prop
PBool Bool
False else Expr 'EWord
ab Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'EWord
bb
        -- TODO: is this sound? do we need a more sophisticated nonce representation?
        noncesDiffer :: Prop
noncesDiffer = Bool -> Prop
PBool (Expr 'EContract
ac.nonce Maybe W64 -> Maybe W64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr 'EContract
bc.nonce)
        storesDiffer :: Prop
storesDiffer = case (Expr 'EContract
ac.storage, Expr 'EContract
bc.storage) of
          (ConcreteStore Map W256 W256
as, ConcreteStore Map W256 W256
bs) -> Bool -> Prop
PBool (Bool -> Prop) -> Bool -> Prop
forall a b. (a -> b) -> a -> b
$ Map W256 W256
as Map W256 W256 -> Map W256 W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= Map W256 W256
bs
          (Expr 'Storage
as, Expr 'Storage
bs) -> if Expr 'Storage
as Expr 'Storage -> Expr 'Storage -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'Storage
bs then Bool -> Prop
PBool Bool
False else Expr 'Storage
as Expr 'Storage -> Expr 'Storage -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr 'Storage
bs
      in Prop
balsDiffer Prop -> Prop -> Prop
.|| Prop
storesDiffer Prop -> Prop -> Prop
.|| Prop
noncesDiffer


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 :: App m => SolverGroup -> Expr End -> m [(Expr End, CheckSatResult)]
produceModels :: forall (m :: * -> *).
App m =>
SolverGroup -> Expr 'End -> m [(Expr 'End, CheckSatResult)]
produceModels SolverGroup
solvers Expr 'End
expr = do
  let flattened :: [Expr 'End]
flattened = Expr 'End -> [Expr 'End]
flattenExpr Expr 'End
expr
      withQueries :: Config -> [(SMT2, Expr 'End)]
withQueries Config
conf = (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 -> ((Config -> [Prop] -> SMT2
assertProps Config
conf) ([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
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  [(CheckSatResult, Expr 'End)]
results <- IO [(CheckSatResult, Expr 'End)] -> m [(CheckSatResult, Expr 'End)]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(CheckSatResult, Expr 'End)]
 -> m [(CheckSatResult, Expr 'End)])
-> IO [(CheckSatResult, Expr 'End)]
-> m [(CheckSatResult, Expr 'End)]
forall a b. (a -> b) -> a -> b
$ ((((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) (Config -> [(SMT2, Expr 'End)]
withQueries Config
conf) (((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)] -> m [(Expr 'End, CheckSatResult)]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Expr 'End, CheckSatResult)] -> m [(Expr 'End, CheckSatResult)])
-> [(Expr 'End, CheckSatResult)] -> m [(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 () -- ignore unreachable branches
    Error Text
e -> [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"smt solver returned an error: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
forall a. Show a => a -> [Char]
show Text
e
    CheckSatResult
EVM.Solvers.Unknown -> do
      [Char] -> IO ()
putStrLn [Char]
"--- Branch ---"
      [Char] -> IO ()
putStrLn [Char]
""
      [Char] -> IO ()
putStrLn [Char]
"Unable to produce a model for the following end state:"
      [Char] -> IO ()
putStrLn [Char]
""
      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
      [Char] -> IO ()
putStrLn [Char]
""
    Sat SMTCex
cex -> do
      [Char] -> IO ()
putStrLn [Char]
"--- Branch ---"
      [Char] -> IO ()
putStrLn [Char]
""
      [Char] -> IO ()
putStrLn [Char]
"Inputs:"
      [Char] -> IO ()
putStrLn [Char]
""
      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 -> Maybe Sig -> SMTCex -> Text
formatCex Expr 'Buf
cd Maybe Sig
forall a. Maybe a
Nothing SMTCex
cex
      [Char] -> IO ()
putStrLn [Char]
""
      [Char] -> IO ()
putStrLn [Char]
"End State:"
      [Char] -> IO ()
putStrLn [Char]
""
      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
      [Char] -> IO ()
putStrLn [Char]
""


formatCex :: Expr Buf -> Maybe Sig -> SMTCex -> Text
formatCex :: Expr 'Buf -> Maybe Sig -> SMTCex -> Text
formatCex Expr 'Buf
cd Maybe Sig
sig m :: SMTCex
m@(SMTCex Map (Expr 'EWord) W256
_ Map (Expr 'EAddr) Addr
_ Map (Expr 'Buf) BufModel
_ Map (Expr 'EAddr) (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
    -- we attempt to produce a model for calldata by substituting all variables
    -- and buffers provided by the model into the original calldata expression.
    -- If we have a concrete result then we display it, otherwise we display
    -- `Any`. This is a little bit of a hack (and maybe unsound?), but we need
    -- it for branches that do not refer to calldata at all (e.g. the top level
    -- callvalue check inserted by solidity in contracts that don't have any
    -- payable functions).
    cd' :: Text
cd' = case Maybe Sig
sig of
      Maybe Sig
Nothing -> Expr 'Buf -> Text
prettyBuf (Expr 'Buf -> Text)
-> (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
Expr.concKeccakSimpExpr (Expr 'Buf -> Expr 'Buf)
-> (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Expr 'Buf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
defaultSymbolicValues (Expr 'Buf -> Text) -> Expr 'Buf -> Text
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
      Just (Sig Text
n [AbiType]
ts) -> SMTCex -> Expr 'Buf -> Text -> [AbiType] -> Text
prettyCalldata SMTCex
m Expr 'Buf
cd Text
n [AbiType]
ts

    storeCex :: [Text]
    storeCex :: [Text]
storeCex
      | Map (Expr 'EAddr) (Map W256 W256) -> Bool
forall k a. Map k a -> Bool
Map.null Map (Expr 'EAddr) (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
$ (Expr 'EAddr -> Map W256 W256 -> [Text] -> [Text])
-> [Text] -> Map (Expr 'EAddr) (Map W256 W256) -> [Text]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\Expr 'EAddr
key Map W256 W256
val [Text]
acc ->
              (Text
"Addr " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack ([Char] -> Text) -> (Expr 'EAddr -> [Char]) -> Expr 'EAddr -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'EAddr -> [Char]
forall a. Show a => a -> [Char]
show (Expr 'EAddr -> Text) -> Expr 'EAddr -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'EAddr
key)
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [(W256, W256)] -> [Char]
forall a. Show a => a -> [Char]
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 (Expr 'EAddr) (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
<> ([Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ W256 -> [Char]
forall a. Show a => a -> [Char]
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
""
        ]

    -- strips the frame arg from frame context vars to make them easier to read
    showTxCtx :: Expr EWord -> Text
    showTxCtx :: Expr 'EWord -> Text
showTxCtx (Expr 'EWord
TxValue) = Text
"TxValue"
    showTxCtx Expr 'EWord
x = [Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> [Char]
forall a. Show a => a -> [Char]
show Expr 'EWord
x

    -- strips all frame context that doesn't come from the top frame
    filterSubCtx :: Map (Expr EWord) W256 -> Map (Expr EWord) W256
    filterSubCtx :: Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
filterSubCtx = (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 (Expr 'EWord
TxValue) W256
_ = Bool
True
        go (Balance {}) W256
_ = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
internalError [Char]
"TODO: BALANCE"
        go (Gas {}) W256
_ = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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 ->
            ([Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> [Char]
forall a. Show a => a -> [Char]
show Expr 'EWord
key [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
": " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> W256 -> [Char]
forall a. Show a => a -> [Char]
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
b = [Char] -> Text
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char]
"Unexpected symbolic buffer:\n" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
T.unpack (Expr 'Buf -> Text
forall (a :: EType). Expr a -> Text
formatExpr Expr 'Buf
b)

prettyCalldata :: SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
prettyCalldata :: SMTCex -> Expr 'Buf -> Text -> [AbiType] -> Text
prettyCalldata SMTCex
cex Expr 'Buf
buf Text
sig [AbiType]
types = [Text] -> Text
forall a. HasCallStack => [a] -> a
head (HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn Text
"(" Text
sig) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
body Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
  where
    argdata :: Expr 'Buf
argdata = W256 -> Expr 'Buf -> Expr 'Buf
Expr.drop W256
4 (Expr 'Buf -> Expr 'Buf)
-> (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Expr 'Buf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
Expr.simplify (Expr 'Buf -> Expr 'Buf)
-> (Expr 'Buf -> Expr 'Buf) -> Expr 'Buf -> Expr 'Buf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
defaultSymbolicValues (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
cex Expr 'Buf
buf
    body :: Text
body = case [AbiType] -> Expr 'Buf -> AbiVals
decodeBuf [AbiType]
types Expr 'Buf
argdata of
      CAbi [AbiValue]
v -> Text -> [Text] -> Text
T.intercalate Text
"," ((AbiValue -> Text) -> [AbiValue] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbiValue -> Text
showVal [AbiValue]
v)
      AbiVals
NoVals -> case Expr 'Buf
argdata of
          ConcreteBuf ByteString
c -> [Char] -> Text
T.pack (ByteString -> [Char]
bsToHex ByteString
c)
          Expr 'Buf
_ -> Text
err
      SAbi [Expr 'EWord]
_ -> Text
err
    err :: Text
err = [Char] -> Text
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char]
"unable to produce a concrete model for calldata: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Expr 'Buf -> [Char]
forall a. Show a => a -> [Char]
show Expr 'Buf
buf

-- | If the expression contains any symbolic values, default them to some
-- concrete value The intuition here is that if we still have symbolic values
-- in our calldata expression after substituting in our cex, then they can have
-- any value and we can safely pick a random value. This is a bit unsatisfying,
-- we should really be doing smth like: https://github.com/ethereum/hevm/issues/334
-- but it's probably good enough for now
defaultSymbolicValues :: Expr a -> Expr a
defaultSymbolicValues :: forall (a :: EType). Expr a -> Expr a
defaultSymbolicValues Expr a
e = Map (Expr 'Buf) ByteString -> Expr a -> Expr a
forall (a :: EType). Map (Expr 'Buf) ByteString -> Expr a -> Expr a
subBufs ((forall (b :: EType). Expr b -> Map (Expr 'Buf) ByteString)
-> Map (Expr 'Buf) ByteString
-> Expr a
-> Map (Expr 'Buf) ByteString
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> Expr a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> Map (Expr 'Buf) ByteString
forall (b :: EType). Expr b -> Map (Expr 'Buf) ByteString
symbufs Map (Expr 'Buf) ByteString
forall a. Monoid a => a
mempty Expr a
e)
                        (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 ((forall (b :: EType). Expr b -> Map (Expr 'EWord) W256)
-> Map (Expr 'EWord) W256 -> Expr a -> Map (Expr 'EWord) W256
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> Expr a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> Map (Expr 'EWord) W256
forall (b :: EType). Expr b -> Map (Expr 'EWord) W256
symwords Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty Expr a
e)
                        (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Expr 'EAddr) Addr -> Expr a -> Expr a
forall (a :: EType). Map (Expr 'EAddr) Addr -> Expr a -> Expr a
subAddrs ((forall (b :: EType). Expr b -> Map (Expr 'EAddr) Addr)
-> Map (Expr 'EAddr) Addr -> Expr a -> Map (Expr 'EAddr) Addr
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> Expr a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> Map (Expr 'EAddr) Addr
forall (b :: EType). Expr b -> Map (Expr 'EAddr) Addr
symaddrs Map (Expr 'EAddr) Addr
forall a. Monoid a => a
mempty Expr a
e) (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ Expr a
e
  where
    symaddrs :: Expr a -> Map (Expr EAddr) Addr
    symaddrs :: forall (b :: EType). Expr b -> Map (Expr 'EAddr) Addr
symaddrs = \case
      a :: Expr a
a@(SymAddr Text
_) -> Expr 'EAddr -> Addr -> Map (Expr 'EAddr) Addr
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EAddr
a (Word160 -> Addr
Addr Word160
0x1312)
      Expr a
_ -> Map (Expr 'EAddr) Addr
forall a. Monoid a => a
mempty
    symbufs :: Expr a -> Map (Expr Buf) ByteString
    symbufs :: forall (b :: EType). Expr b -> Map (Expr 'Buf) ByteString
symbufs = \case
      a :: Expr a
a@(AbstractBuf Text
_) -> Expr 'Buf -> ByteString -> Map (Expr 'Buf) ByteString
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'Buf
a ByteString
""
      Expr a
_ -> Map (Expr 'Buf) ByteString
forall a. Monoid a => a
mempty
    symwords :: Expr a -> Map (Expr EWord) W256
    symwords :: forall (b :: EType). Expr b -> Map (Expr 'EWord) W256
symwords = \case
      a :: Expr a
a@(Var Text
_) -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
Origin -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
Coinbase -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
Timestamp -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
BlockNumber -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
PrevRandao -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
GasLimit -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
ChainId -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      a :: Expr a
a@Expr a
BaseFee -> Expr 'EWord -> W256 -> Map (Expr 'EWord) W256
forall k a. k -> a -> Map k a
Map.singleton Expr a
Expr 'EWord
a W256
0
      Expr a
_ -> Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty

-- | Takes an expression and a Cex and replaces all abstract values in the buf with
-- concrete ones from the Cex.
subModel :: SMTCex -> Expr a -> Expr a
subModel :: forall (a :: EType). SMTCex -> Expr a -> Expr a
subModel SMTCex
c
  = 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 'EAddr) (Map W256 W256) -> Expr a -> Expr a
forall (a :: EType).
Map (Expr 'EAddr) (Map W256 W256) -> Expr a -> Expr a
subStores 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.vars
  (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) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Expr 'EAddr) Addr -> Expr a -> Expr a
forall (a :: EType). Map (Expr 'EAddr) Addr -> Expr a -> Expr a
subAddrs SMTCex
c.addrs
  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 ([Char] -> BufModel
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> BufModel) -> [Char] -> BufModel
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot flatten buffer: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> BufModel -> [Char]
forall a. Show a => a -> [Char]
show BufModel
b)
                (BufModel -> Maybe BufModel
SMT.collapse BufModel
b)

subVars :: Map (Expr EWord) W256 -> Expr a -> Expr a
subVars :: forall (a :: EType). 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
  where
    subVar :: Expr a -> Expr EWord -> W256 -> Expr a
    subVar :: forall (a :: EType). Expr a -> Expr 'EWord -> W256 -> Expr a
subVar Expr a
a 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
a
      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

subAddrs :: Map (Expr EAddr) Addr -> Expr a -> Expr a
subAddrs :: forall (a :: EType). Map (Expr 'EAddr) Addr -> Expr a -> Expr a
subAddrs Map (Expr 'EAddr) Addr
model Expr a
b = (Expr a -> Expr 'EAddr -> Addr -> Expr a)
-> Expr a -> Map (Expr 'EAddr) Addr -> Expr a
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey Expr a -> Expr 'EAddr -> Addr -> Expr a
forall (a :: EType). Expr a -> Expr 'EAddr -> Addr -> Expr a
subAddr Expr a
b Map (Expr 'EAddr) Addr
model
  where
    subAddr :: Expr a -> Expr EAddr -> Addr -> Expr a
    subAddr :: forall (a :: EType). Expr a -> Expr 'EAddr -> Addr -> Expr a
subAddr Expr a
a Expr 'EAddr
var Addr
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
a
      where
        go :: Expr a -> Expr a
        go :: forall (a :: EType). Expr a -> Expr a
go = \case
          v :: Expr a
v@(SymAddr Text
_) -> if Expr a
v Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr 'EAddr
var
                      then Addr -> Expr 'EAddr
LitAddr Addr
val
                      else Expr a
v
          Expr a
e -> Expr a
e

subBufs :: Map (Expr Buf) ByteString -> Expr a -> Expr a
subBufs :: forall (a :: EType). 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
  where
    subBuf :: Expr a -> Expr Buf -> ByteString -> Expr a
    subBuf :: forall (a :: EType). Expr a -> Expr 'Buf -> ByteString -> Expr a
subBuf Expr a
x 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
x
      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

subStores :: Map (Expr EAddr) (Map W256 W256) -> Expr a -> Expr a
subStores :: forall (a :: EType).
Map (Expr 'EAddr) (Map W256 W256) -> Expr a -> Expr a
subStores Map (Expr 'EAddr) (Map W256 W256)
model Expr a
b = (Expr a -> Expr 'EAddr -> Map W256 W256 -> Expr a)
-> Expr a -> Map (Expr 'EAddr) (Map W256 W256) -> Expr a
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey Expr a -> Expr 'EAddr -> Map W256 W256 -> Expr a
forall (a :: EType).
Expr a -> Expr 'EAddr -> Map W256 W256 -> Expr a
subStore Expr a
b Map (Expr 'EAddr) (Map W256 W256)
model
  where
    subStore :: Expr a -> Expr EAddr -> Map W256 W256 -> Expr a
    subStore :: forall (a :: EType).
Expr a -> Expr 'EAddr -> Map W256 W256 -> Expr a
subStore Expr a
x Expr 'EAddr
var Map W256 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
x
      where
        go :: Expr a -> Expr a
        go :: forall (a :: EType). Expr a -> Expr a
go = \case
          v :: Expr a
v@(AbstractStore Expr 'EAddr
a Maybe W256
_)
            -> if Expr 'EAddr
a Expr 'EAddr -> Expr 'EAddr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EAddr
var
               then Map W256 W256 -> Expr 'Storage
ConcreteStore Map W256 W256
val
               else Expr a
v
          Expr a
e -> Expr a
e

getCex :: ProofResult a b c -> Maybe b
getCex :: forall a b c. ProofResult a b c -> Maybe b
getCex (Cex b
c) = b -> Maybe b
forall a. a -> Maybe a
Just b
c
getCex ProofResult a b c
_ = Maybe b
forall a. Maybe a
Nothing

getTimeout :: ProofResult a b c -> Maybe c
getTimeout :: forall a b c. ProofResult a b c -> Maybe c
getTimeout (Timeout c
c) = c -> Maybe c
forall a. a -> Maybe a
Just c
c
getTimeout ProofResult a b c
_ = Maybe c
forall a. Maybe a
Nothing