Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions hevm-cli/hevm-cli.hs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ import Control.Monad.State.Strict (execStateT, liftIO)
import Data.ByteString (ByteString)
import Data.List (intercalate, isSuffixOf)
import Data.Text (unpack, pack)
import Data.Maybe (fromMaybe, fromJust, mapMaybe)
import Data.Maybe (fromMaybe, mapMaybe)
import Data.Version (showVersion)
import Data.DoubleWord (Word256)
import System.IO (stderr)
Expand Down Expand Up @@ -560,7 +560,7 @@ vmFromCommand cmd = do
decipher = hexByteString "bytes" . strip0x
mkCode bs = if create cmd
then EVM.InitCode bs mempty
else EVM.RuntimeCode (fromJust $ Expr.toList (ConcreteBuf bs))
else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)
address' = if create cmd
then addr address (createAddress origin' (word nonce 0))
else addr address 0xacab
Expand Down Expand Up @@ -656,7 +656,7 @@ symvmFromCommand cmd calldata' = do
origin' = addr origin 0
mkCode bs = if create cmd
then EVM.InitCode bs mempty
else EVM.RuntimeCode (fromJust . Expr.toList $ ConcreteBuf bs)
else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)
address' = if create cmd
then addr address (createAddress origin' (word nonce 0))
else addr address 0xacab
Expand Down
148 changes: 94 additions & 54 deletions src/EVM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ import EVM.Types hiding (IllegalOverflow, Error)
import EVM.Solidity
import EVM.Concrete (createAddress, create2Address)
import EVM.Op
import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord, writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice, isLitByte)
import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord, writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice)
import EVM.FeeSchedule (FeeSchedule (..))
import Options.Generic as Options
import qualified EVM.Precompiled
Expand Down Expand Up @@ -305,10 +305,18 @@ data SubState = SubState
hopefully we do not have to deal with dynamic immutable before we get a real data section...
-}
data ContractCode
= InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation
| RuntimeCode (V.Vector (Expr Byte)) -- ^ "Instance" code, after contract creation
= InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation
| RuntimeCode RuntimeCode -- ^ "Instance" code, after contract creation
deriving (Show)

-- | We have two variants here to optimize the fully concrete case.
-- ConcreteRuntimeCode just wraps a ByteString
-- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).
data RuntimeCode
= ConcreteRuntimeCode ByteString
| SymbolicRuntimeCode (V.Vector (Expr Byte))
deriving (Show, Eq, Ord)

-- runtime err when used for symbolic code
instance Eq ContractCode where
(InitCode a b) == (InitCode c d) = a == c && b == d
Expand Down Expand Up @@ -392,7 +400,7 @@ blankState :: FrameState
blankState = FrameState
{ _contract = 0
, _codeContract = 0
, _code = RuntimeCode mempty
, _code = RuntimeCode (ConcreteRuntimeCode "")
, _pc = 0
, _stack = mempty
, _memory = mempty
Expand Down Expand Up @@ -421,7 +429,8 @@ makeLenses ''VM
bytecode :: Getter Contract (Expr Buf)
bytecode = contractcode . to f
where f (InitCode _ _) = mempty
f (RuntimeCode ops) = Expr.fromList ops
f (RuntimeCode (ConcreteRuntimeCode bs)) = ConcreteBuf bs
f (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops

instance Semigroup Cache where
a <> b = Cache
Expand Down Expand Up @@ -603,7 +612,8 @@ exec1 = do
else do
let ?op = case (the state code) of
InitCode conc _ -> BS.index conc (the state pc)
RuntimeCode ops ->
RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs (the state pc)
RuntimeCode (SymbolicRuntimeCode ops) ->
fromMaybe (error "could not analyze symbolic code") $
unlitByte $ ops V.! the state pc

Expand All @@ -614,13 +624,10 @@ exec1 = do
let !n = num x - 0x60 + 1
!xs = case the state code of
InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + the state pc) conc)
RuntimeCode ops ->
RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + the state pc) bs
RuntimeCode (SymbolicRuntimeCode ops) ->
let bytes = V.take n $ V.drop (1 + the state pc) ops
in if all isLitByte bytes then -- optimize concrete path
let litBytes = V.toList $ V.catMaybes $ unlitByte <$> bytes
padded = BS.replicate (32 - length litBytes) 0 <> BS.pack litBytes
in Lit $ word padded
else readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes
in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes
limitStack 1 $
burn g_verylow $ do
next
Expand Down Expand Up @@ -1075,7 +1082,9 @@ exec1 = do
case stk of
(x:xs) ->
burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->
checkJump x' xs
case toInt x' of
Nothing -> vmError EVM.BadJumpDestination
Just i -> checkJump i xs
_ -> underrun

-- op: JUMPI
Expand All @@ -1085,7 +1094,9 @@ exec1 = do
burn g_high $
let jump :: Bool -> EVM ()
jump False = assign (state . stack) xs >> next
jump _ = checkJump x' xs
jump _ = case toInt x' of
Nothing -> vmError EVM.BadJumpDestination
Just i -> checkJump i xs
in case maybeLitWord y of
Just y' -> jump (0 /= y')
-- if the jump condition is symbolic, we explore both sides
Expand Down Expand Up @@ -1674,7 +1685,8 @@ accountExists addr vm =
accountEmpty :: Contract -> Bool
accountEmpty c =
case view contractcode c of
RuntimeCode b -> null b
RuntimeCode (ConcreteRuntimeCode "") -> True
RuntimeCode (SymbolicRuntimeCode b) -> null b
_ -> False
&& (view nonce c == 0)
&& (view balance c == 0)
Expand Down Expand Up @@ -1703,10 +1715,17 @@ finalize = do
creation <- use (tx . isCreate)
createe <- use (state . contract)
createeExists <- (Map.member createe) <$> use (env . contracts)
case Expr.toList output of
Nothing -> vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]
Just ops ->
when (creation && createeExists) $ replaceCode createe (RuntimeCode ops)
let onContractCode contractCode =
when (creation && createeExists) $ replaceCode createe contractCode
case output of
ConcreteBuf bs ->
onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
_ ->
case Expr.toList output of
Nothing ->
vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]
Just ops ->
onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)

-- compute and pay the refund to the caller and the
-- corresponding payment to the miner
Expand Down Expand Up @@ -1735,7 +1754,7 @@ finalize = do
-- pay out the block reward, recreating the miner if necessary
preuse (env . contracts . ix miner) >>= \case
Nothing -> modifying (env . contracts)
(Map.insert miner (initialContract (EVM.RuntimeCode mempty)))
(Map.insert miner (initialContract (EVM.RuntimeCode (ConcreteRuntimeCode ""))))
Just _ -> noop
modifying (env . contracts)
(Map.adjust (over balance (+ blockReward)) miner)
Expand Down Expand Up @@ -2119,7 +2138,8 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
collision :: Maybe Contract -> Bool
collision c' = case c' of
Just c -> (view nonce c /= 0) || case view contractcode c of
RuntimeCode b -> not $ null b
RuntimeCode (ConcreteRuntimeCode "") -> False
RuntimeCode (SymbolicRuntimeCode b) -> not $ null b
_ -> True
Nothing -> False

Expand Down Expand Up @@ -2368,17 +2388,23 @@ finishFrame how = do
case how of
-- Case 4: Returning during a creation?
FrameReturned output -> do
case Expr.toList output of
Nothing -> vmError $
UnexpectedSymbolicArg
(view (state . pc) oldVm)
"runtime code cannot have an abstract length"
[output]
Just newCode -> do
replaceCode createe (RuntimeCode newCode)
let onContractCode contractCode = do
replaceCode createe contractCode
assign (state . returndata) mempty
reclaimRemainingGasAllowance
push (num createe)
case output of
ConcreteBuf bs ->
onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
_ ->
case Expr.toList output of
Nothing -> vmError $
UnexpectedSymbolicArg
(view (state . pc) oldVm)
"runtime code cannot have an abstract length"
[output]
Just newCode -> do
onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode)

-- Case 5: Reverting during a creation?
FrameReverted output -> do
Expand Down Expand Up @@ -2558,19 +2584,19 @@ stackOp3 cost f =

-- * Bytecode data functions

checkJump :: (Integral n) => n -> [Expr EWord] -> EVM ()
checkJump :: Int -> [Expr EWord] -> EVM ()
checkJump x xs = do
theCode <- use (state . code)
self <- use (state . codeContract)
theCodeOps <- use (env . contracts . ix self . codeOps)
theOpIxMap <- use (env . contracts . ix self . opIxMap)
let ops = case theCode of
InitCode ops' _ -> V.fromList $ LitByte <$> BS.unpack ops'
RuntimeCode ops' -> ops'
op = do
-- TODO: not a big fan of how bounds are checked, change this
b <- if x < num (length ops) then ops V.!? num x else Nothing
unlitByte b
let op = case theCode of
InitCode ops _ ->
if x > BS.length ops then Nothing else Just $ BS.index ops x
RuntimeCode (ConcreteRuntimeCode ops) ->
if x > BS.length ops then Nothing else Just $ BS.index ops x
RuntimeCode (SymbolicRuntimeCode ops) ->
ops V.!? x >>= unlitByte
case op of
Nothing -> vmError EVM.BadJumpDestination
Just b ->
Expand Down Expand Up @@ -2606,7 +2632,10 @@ mkOpIxMap (InitCode conc _)
go v (n, !i, !j, !m) _ =
{- PUSH data. -} (n - 1, i + 1, j, m >> Vector.write v i j)

mkOpIxMap (RuntimeCode ops)
mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =
mkOpIxMap (InitCode ops mempty) -- a bit hacky

mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))
= Vector.create $ Vector.new (length ops) >>= \v ->
let (_, _, _, m) = foldl (go v) (0, 0, 0, return ()) (stripBytecodeMetadataSym $ V.toList ops)
in m >> return v
Expand All @@ -2632,7 +2661,9 @@ vmOp vm =
(op, pushdata) = case code' of
InitCode xs' _ ->
(BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')
RuntimeCode xs' ->
RuntimeCode (ConcreteRuntimeCode xs') ->
(BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')
RuntimeCode (SymbolicRuntimeCode xs') ->
( fromMaybe (error "unexpected symbolic code") . unlitByte $ xs' V.! i , V.toList $ V.drop i xs')
in if (opslen code' < i)
then Nothing
Expand Down Expand Up @@ -2756,25 +2787,24 @@ readOp x _ = case x of

-- Maps operation indicies into a pair of (bytecode index, operation)
mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op)
mkCodeOps (InitCode bytes _) = RegularVector.fromList . toList $ go 0 bytes
mkCodeOps contractCode =
let l = case contractCode of
InitCode bytes _ ->
LitByte <$> (BS.unpack bytes)
RuntimeCode (ConcreteRuntimeCode ops) ->
LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)
RuntimeCode (SymbolicRuntimeCode ops) ->
stripBytecodeMetadataSym $ V.toList ops
in RegularVector.fromList . toList $ go 0 l
where
go !i !xs =
case BS.uncons xs of
Nothing ->
mempty
Just (x, xs') ->
let j = opSize x
in (i, readOp x (fmap LitByte $ BS.unpack xs')) Seq.<| go (i + j) (BS.drop j xs)
mkCodeOps (RuntimeCode ops) = RegularVector.fromList . toList $ go' 0 (stripBytecodeMetadataSym $ V.toList ops)
where
go' !i !xs =
case uncons xs of
Nothing ->
mempty
Just (x, xs') ->
let x' = fromMaybe (error "unexpected symbolic code argument") $ unlitByte x
j = opSize x'
in (i, readOp x' xs') Seq.<| go' (i + j) (drop j xs)
in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)

-- * Gas cost calculation helpers

Expand Down Expand Up @@ -2889,23 +2919,27 @@ log2 x = finiteBitSize x - 1 - countLeadingZeros x

hashcode :: ContractCode -> Expr EWord
hashcode (InitCode ops args) = keccak $ (ConcreteBuf ops) <> args
hashcode (RuntimeCode ops) = keccak . Expr.fromList $ ops
hashcode (RuntimeCode (ConcreteRuntimeCode ops)) = keccak (ConcreteBuf ops)
hashcode (RuntimeCode (SymbolicRuntimeCode ops)) = keccak . Expr.fromList $ ops

-- | The length of the code ignoring any constructor args.
-- This represents the region that can contain executable opcodes
opslen :: ContractCode -> Int
opslen (InitCode ops _) = BS.length ops
opslen (RuntimeCode ops) = length ops
opslen (RuntimeCode (ConcreteRuntimeCode ops)) = BS.length ops
opslen (RuntimeCode (SymbolicRuntimeCode ops)) = length ops

-- | The length of the code including any constructor args.
-- This can return an abstract value
codelen :: ContractCode -> Expr EWord
codelen c@(InitCode {}) = bufLength $ toBuf c
codelen (RuntimeCode ops) = Lit . num $ length ops
codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . num $ BS.length ops
codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . num $ length ops

toBuf :: ContractCode -> Expr Buf
toBuf (InitCode ops args) = ConcreteBuf ops <> args
toBuf (RuntimeCode ops) = Expr.fromList ops
toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = ConcreteBuf ops
toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops


codeloc :: EVM CodeLocation
Expand All @@ -2921,6 +2955,12 @@ toWord64 n =
then let (W256 (Word256 _ (Word128 _ n'))) = n in Just n'
else Nothing

toInt :: W256 -> Maybe Int
toInt n =
if n <= num (maxBound :: Int)
then let (W256 (Word256 _ (Word128 _ n'))) = n in Just (fromIntegral n')
else Nothing

-- * Emacs setup

-- Local Variables:
Expand Down
8 changes: 6 additions & 2 deletions src/EVM/Dapp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

module EVM.Dapp where

import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode)
import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode, RuntimeCode (..))
import EVM.ABI (Event, AbiType, SolError)
import EVM.Debug (srcMapCodePos)
import EVM.Solidity
Expand Down Expand Up @@ -176,7 +176,11 @@ findSrc c dapp = do
lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract
lookupCode (InitCode c _) a =
snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata c))) a
lookupCode (RuntimeCode c) a = let
lookupCode (RuntimeCode (ConcreteRuntimeCode c)) a =
case snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata c))) a of
Just x -> return x
Nothing -> snd <$> find (compareCode c . fst) (view dappSolcByCode a)
lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let
code = BS.pack $ mapMaybe unlitByte $ V.toList c
in case snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata code))) a of
Just x -> return x
Expand Down
3 changes: 1 addition & 2 deletions src/EVM/Dev.hs
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@ import GHC.Conc
import System.Exit (exitFailure)
import qualified EVM.Fetch as Fetch
import qualified EVM.FeeSchedule as FeeSchedule
import qualified Data.Vector as V

checkEquiv :: (Typeable a) => Expr a -> Expr a -> IO ()
checkEquiv a b = withSolvers Z3 1 Nothing $ \s -> do
Expand Down Expand Up @@ -363,7 +362,7 @@ vat = do
initVm :: ByteString -> VM
initVm bs = vm
where
contractCode = RuntimeCode $ V.fromList $ LitByte <$> unpack bs
contractCode = RuntimeCode (ConcreteRuntimeCode bs)
c = Contract
{ _contractcode = contractCode
, _balance = 0
Expand Down
2 changes: 1 addition & 1 deletion src/EVM/Exec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ vmForEthrunCreation creationCode =
, vmoptTxAccessList = mempty
, vmoptAllowFFI = False
}) & set (env . contracts . at ethrunAddress)
(Just (initialContract (RuntimeCode mempty)))
(Just (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))

exec :: MonadState VM m => m VMResult
exec =
Expand Down
Loading