allow calldata to be either a buffer or pseudodynamic (old approach)

src/hevm/src/EVM.hs

@@ -16,6 +16,7 @@ module EVM where
 import Prelude hiding (log, Word, exponent)
 
 import Data.SBV hiding (Word, output, Unknown)
+import Data.SBV.List (implode, subList)
 import Data.Proxy (Proxy(..))
 import EVM.ABI
 import EVM.Types
@@ -170,7 +171,7 @@ data Cache = Cache
 -- | A way to specify an initial VM state
 data VMOpts = VMOpts
   { vmoptContract :: Contract
-  , vmoptCalldata :: Buffer -- maximum size of uint32 as per eip 1985
+  , vmoptCalldata :: Calldata
   , vmoptValue :: SymWord
   , vmoptAddress :: Addr
   , vmoptCaller :: SAddr
@@ -225,7 +226,7 @@ data FrameState = FrameState
   , _stack        :: [SymWord]
   , _memory       :: Buffer
   , _memorySize   :: SWord 32
-  , _calldata     :: Buffer
+  , _calldata     :: Calldata
   , _callvalue    :: SymWord
   , _caller       :: SAddr
   , _gas          :: Word
@@ -312,6 +313,14 @@ data StorageModel
 
 instance ParseField StorageModel
 
+-- | Calldata can either by a normal buffer, or a custom "pseudo dynamic" encoding. See EVM.Symbolic for details
+data CalldataModel
+  = BufferCD
+  | BoundedCD
+  deriving (Read, Show)
+
+instance ParseField CalldataModel
+
 -- | Various environmental data
 data Env = Env
   { _contracts    :: Map Addr Contract
@@ -342,7 +351,7 @@ blankState = FrameState
   , _stack        = mempty
   , _memory       = mempty
   , _memorySize   = 0
-  , _calldata     = mempty
+  , _calldata     = CalldataBuffer mempty
   , _callvalue    = 0
   , _caller       = 0
   , _gas          = 0
@@ -501,8 +510,8 @@ exec1 = do
     -- call to precompile
 
     let ?op = 0x00 -- dummy value
-    copyBytesToMemory (the state calldata) (len $ the state calldata) 0 0
-    executePrecompile self (the state gas) 0 (len $ the state calldata) 0 0 []
+    copyCalldataToMemory (the state calldata) (cdlen $ the state calldata) 0 0
+    executePrecompile self (the state gas) 0 (cdlen $ the state calldata) 0 0 []
     vmx <- get
     case view (state.stack) vmx of
       (x:_) -> case maybeLitWord x of
@@ -712,12 +721,14 @@ exec1 = do
 
         -- op: CALLDATALOAD
         0x35 -> stackOp1 (const g_verylow) $
-          flip readSWord (the state calldata)
+          case the state calldata of
+            CalldataBuffer bf -> flip readSWord bf
+            CalldataDynamic bf -> \(S _ i) -> readStaticWordWithBound (sFromIntegral i) bf
 
         -- op: CALLDATASIZE
         0x36 ->
           limitStack 1 . burn g_base $
-            next >> pushSym (len $ the state calldata)
+            next >> pushSym (cdlen $ the state calldata)
 
         -- op: CALLDATACOPY
         0x37 ->
@@ -727,7 +738,7 @@ exec1 = do
                 accessUnboundedMemoryRange fees xTo xSize $ do
                   next
                   assign (state . stack) xs
-                  copyBytesToMemory (the state calldata) xSize xFrom xTo
+                  copyCalldataToMemory (the state calldata) xSize xFrom xTo
             _ -> underrun
 
         -- op: CODESIZE
@@ -1909,7 +1920,7 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
               assign memory mempty
               assign memorySize 0
               assign returndata mempty
-              assign calldata (readMemory xInOffset xInSize vm0)
+              assign calldata (CalldataBuffer $ readMemory xInOffset xInSize vm0)
 
             continue
 
@@ -2195,6 +2206,17 @@ accessMemoryWord
   :: FeeSchedule Word -> SymWord -> EVM () -> EVM ()
 accessMemoryWord fees x = accessMemoryRange fees x 32
 
+copyCalldataToMemory
+ :: Calldata -> SymWord -> SymWord -> SymWord -> EVM ()
+copyCalldataToMemory (CalldataBuffer bf) size xOffset yOffset =
+  copyBytesToMemory bf size xOffset yOffset
+copyCalldataToMemory (CalldataDynamic (b, l)) size xOffset yOffset =
+  case (maybeLitWord size, maybeLitWord xOffset, maybeLitWord yOffset) of
+    (Just size', Just xOffset', Just yOffset') ->
+      copyBytesToMemory (StaticSymBuffer [ite (i .<= l) x 0 | (x, i) <- zip b [1..]]) size' xOffset' yOffset'
+    _ ->
+      copyBytesToMemory (DynamicSymBuffer (subList (implode b) 0 (sFromIntegral l))) size xOffset yOffset
+
 copyBytesToMemory
   :: Buffer -> SymWord -> SymWord -> SymWord -> EVM ()
 copyBytesToMemory bs size xOffset yOffset =

src/hevm/src/EVM/Exec.hs

@@ -2,7 +2,7 @@ module EVM.Exec where
 
 import EVM
 import EVM.Concrete (createAddress)
-import EVM.Symbolic (litAddr)
+import EVM.Symbolic (litAddr, Calldata(..))
 import EVM.Types
 
 import qualified EVM.FeeSchedule as FeeSchedule
@@ -22,7 +22,7 @@ vmForEthrunCreation :: ByteString -> VM
 vmForEthrunCreation creationCode =
   (makeVm $ VMOpts
     { vmoptContract = initialContract (InitCode creationCode)
-    , vmoptCalldata = mempty
+    , vmoptCalldata = CalldataBuffer mempty
     , vmoptValue = 0
     , vmoptAddress = createAddress ethrunAddress 1
     , vmoptCaller = litAddr ethrunAddress

src/hevm/src/EVM/SymExec.hs

@@ -16,7 +16,7 @@ import EVM.Stepper (Stepper)
 import qualified EVM.Stepper as Stepper
 import qualified Control.Monad.Operational as Operational
 import EVM.Types hiding (Word)
-import EVM.Symbolic (litBytes, SymWord(..), sw256, Buffer(..))
+import EVM.Symbolic (litBytes, SymWord(..), sw256, Buffer(..), Calldata(..))
 import EVM.Concrete (createAddress, Word)
 import qualified EVM.FeeSchedule as FeeSchedule
 import Data.SBV.Trans.Control
@@ -93,19 +93,28 @@ staticCalldata sig typesignature concreteArgs =
 
     sig' = litBytes $ selector sig
 
-abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM
-abstractVM typesignature concreteArgs x storagemodel = do
+-- | Construct a VM out of a type signature, possibly with specialized concrete arguments
+-- ,bytecode, storagemodel and calldata structure.
+abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> CalldataModel -> Query VM
+abstractVM typesignature concreteArgs x storagemodel calldatamodel = do
   (cd',pathCond) <- case typesignature of
-           Nothing -> do list <- freshVar_
-                         return (DynamicSymBuffer list,
-                                 -- due to some current z3 shenanegans (possibly related to: https://github.com/Z3Prover/z3/issues/4635)
-                                 -- we assume the list length to be shorter than max_length both as a bitvector and as an integer.
-                                 -- The latter implies the former as long as max_length fits in a bitvector, but assuming it explitly
-                                 -- improves z3 (4.8.8) performance.
-                                 SList.length list .< 1000 .&&
-                                  sw256 (sFromIntegral (SList.length list)) .< sw256 1000)
+           Nothing -> case calldatamodel of
+                        BufferCD -> do
+                          list <- freshVar_
+                          return (CalldataBuffer (DynamicSymBuffer list),
+                            -- due to some current z3 shenanegans (possibly related to: https://github.com/Z3Prover/z3/issues/4635)
+                            -- we assume the list length to be shorter than max_length both as a bitvector and as an integer.
+                            -- The latter implies the former as long as max_length fits in a bitvector, but assuming it explitly
+                            -- improves z3 (4.8.8) performance.
+                            SList.length list .< 1000 .&&
+                             sw256 (sFromIntegral (SList.length list)) .< sw256 1000)
+
+                        BoundedCD -> do
+                           cd <- sbytes256
+                           len <- freshVar_
+                           return (CalldataDynamic (cd, len), len .<= 256)
            Just (name, typs) -> do symbytes <- staticCalldata name typs concreteArgs
-                                   return (StaticSymBuffer symbytes, sTrue)
+                                   return (CalldataBuffer (StaticSymBuffer symbytes), sTrue)
 
   symstore <- case storagemodel of
     SymbolicS -> Symbolic <$> freshArray_ Nothing
@@ -116,7 +125,7 @@ abstractVM typesignature concreteArgs x storagemodel = do
   return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' cd'
     & over pathConditions (<> [pathCond])
 
-loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> Buffer -> VM
+loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> Calldata -> VM
 loadSymVM x initStore model addr callvalue' calldata' =
     (makeVm $ VMOpts
     { vmoptContract = contractWithStore x initStore
@@ -196,17 +205,21 @@ maxIterationsReached vm (Just maxIter) =
 type Precondition = VM -> SBool
 type Postcondition = (VM, VM) -> SBool
 
+checkAssertBuffer :: ByteString -> Query (Either (VM, [VM]) VM)
+checkAssertBuffer c = verifyContract c Nothing [] SymbolicS BufferCD (const sTrue) (Just checkAssertions)
+
+
 checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)
-checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)
+checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS BoundedCD (const sTrue) (Just checkAssertions)
 
 checkAssertions :: Postcondition
 checkAssertions (_, out) = case view result out of
   Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse
   _ -> sTrue
 
-verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
-verifyContract theCode signature' concreteArgs storagemodel pre maybepost = do
-    preStateRaw <- abstractVM signature' concreteArgs theCode  storagemodel
+verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> CalldataModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
+verifyContract theCode signature' concreteArgs storagemodel calldatamodel pre maybepost = do
+    preStateRaw <- abstractVM signature' concreteArgs theCode  storagemodel calldatamodel
     -- add the pre condition to the pathconditions to ensure that we are only exploring valid paths
     let preState = over pathConditions ((++) [pre preStateRaw]) preStateRaw
     verify preState Nothing Nothing maybepost
@@ -247,7 +260,7 @@ verify preState maxIter rpcinfo maybepost = do
 -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.
 equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)
 equivalenceCheck bytecodeA bytecodeB maxiter signature' = do
-  preStateA <- abstractVM signature' [] bytecodeA SymbolicS
+  preStateA <- abstractVM signature' [] bytecodeA SymbolicS BoundedCD
 
   let preself = preStateA ^. state . contract
       precaller = preStateA ^. state . caller
@@ -310,8 +323,12 @@ showCounterexample vm maybesig = do
       SAddr caller' = view (EVM.state . EVM.caller) vm
 --  cdlen' <- num <$> getValue cdlen
   calldatainput <- case calldata' of
-    StaticSymBuffer cd -> mapM (getValue.fromSized) cd >>= return . pack
-    ConcreteBuffer cd  -> return $ cd
+    CalldataDynamic (cd, cdlen) -> do
+      cdlen' <- num <$> getValue cdlen
+      mapM (getValue.fromSized) (take cdlen' cd) >>= return . pack
+    CalldataBuffer (StaticSymBuffer cd) -> mapM (getValue.fromSized) cd >>= return . pack
+    CalldataBuffer (ConcreteBuffer cd)  -> return $ cd
+    CalldataBuffer (DynamicSymBuffer cd) -> (fmap fromSized) <$> getValue cd >>= return . pack
   callvalue' <- num <$> getValue cvalue
   caller'' <- num <$> getValue caller'
   io $ do

src/hevm/src/EVM/Symbolic.hs

@@ -206,7 +206,6 @@ readByteOrZero'' i bs =
   (bs .!! (sFromIntegral i))
   (literal 0)
 
-
 -- pad up to 1000 bytes
 sslice :: SymWord -> SymWord -> SList (WordN 8) -> SList (WordN 8)
 sslice (S _ o) (S _ l) bs = case (unliteral $ SL.length bs, unliteral (o + l)) of
@@ -299,12 +298,26 @@ instance Semigroup Buffer where
 instance Monoid Buffer where
   mempty = ConcreteBuffer mempty
 
+-- | Althogh calldata can be modeled perfectly well directly as a Buffer,
+-- we allow for it to take on a special form; the pair ([SWord 8], SWord 32)
+-- where the second argument is understood as the length of the list.
+-- This allows us to 'fake' dynamically sized calldata arrays in a way
+-- that has proven more efficient than `SList`.
+data Calldata
+  = CalldataBuffer Buffer
+  | CalldataDynamic ([SWord 8], SWord 32)
+  deriving Show
+
 -- a whole foldable instance seems overkill, but length is always good to have!
 len :: Buffer -> SymWord --SWord 32
 len (DynamicSymBuffer a) = sw256 $ sFromIntegral $ SL.length a
 len (StaticSymBuffer bs) = litWord . num $ length bs
 len (ConcreteBuffer bs) = litWord . num $ BS.length bs
 
+cdlen :: Calldata -> SymWord
+cdlen (CalldataBuffer bf) = len bf
+cdlen (CalldataDynamic (_, a)) = sw256 $ sFromIntegral a
+
 grab :: Int -> Buffer -> Buffer
 grab n (StaticSymBuffer bs) = StaticSymBuffer $ take n bs
 grab n (ConcreteBuffer bs) = ConcreteBuffer $ BS.take n bs
@@ -393,6 +406,20 @@ readSWord i bf = case (maybeLitWord i, bf) of
   (Just i', ConcreteBuffer x) -> num $ Concrete.readMemoryWord i' x
   _  -> readSWord'' i (dynamize bf)
 
+
+select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a
+select' xs err ind = walk xs ind err
+    where walk []     _ acc = acc
+          walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc)
+
+-- Generates a ridiculously large set of constraints (roughly 25k) when
+-- the index is symbolic, but it still seems (kind of) manageable
+-- for the solvers.
+readStaticWordWithBound :: SWord 32 -> ([SWord 8], SWord 32) -> SymWord
+readStaticWordWithBound ind (xs, bound) =
+  let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
+  in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]
+
 -- | Custom instances for SymWord, many of which have direct
 -- analogues for concrete words defined in Concrete.hs
 

src/hevm/src/EVM/TTY.hs

@@ -12,7 +12,7 @@ import Brick.Widgets.List
 
 import EVM
 import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi)
-import EVM.Symbolic (SymWord(..), Buffer(..))
+import EVM.Symbolic (SymWord(..), Buffer(..), Calldata(..))
 import EVM.SymExec (maxIterationsReached)
 import EVM.Dapp (DappInfo, dappInfo)
 import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources)
@@ -868,12 +868,16 @@ prettyIfConcrete (StaticSymBuffer x) = show x
 prettyIfConcrete (DynamicSymBuffer x) = show x
 prettyIfConcrete (ConcreteBuffer x) = prettyHex 40 x
 
+prettyIfConcreteCd :: Calldata -> String
+prettyIfConcreteCd (CalldataBuffer bf) = prettyIfConcrete bf
+prettyIfConcreteCd (CalldataDynamic (x, l)) = show x
+
 drawTracePane :: UiVmState -> UiWidget
 drawTracePane s =
   case view uiShowMemory s of
     True ->
       hBorderWithLabel (txt "Calldata")
-      <=> str (prettyIfConcrete $ view (uiVm . state . calldata) s)
+      <=> str (prettyIfConcreteCd $ view (uiVm . state . calldata) s)
       <=> hBorderWithLabel (txt "Returndata")
       <=> str (prettyIfConcrete (view (uiVm . state . returndata) s))
       <=> hBorderWithLabel (txt "Output")

src/hevm/src/EVM/UnitTest.hs

@@ -553,7 +553,7 @@ setupCall TestVMParams{..} sig args  = do
   use (env . contracts) >>= assign (tx . txReversion)
   assign (tx . isCreate) False
   loadContract testAddress
-  assign (state . calldata) (ConcreteBuffer $ abiMethod sig args)
+  assign (state . calldata) (CalldataBuffer (ConcreteBuffer $ abiMethod sig args))
   assign (state . caller) (litAddr testCaller)
   assign (state . gas) (w256 testGasCall)
 
@@ -563,7 +563,7 @@ initialUnitTestVm (UnitTestOptions {..}) theContract =
     TestVMParams {..} = testParams
     vm = makeVm $ VMOpts
            { vmoptContract = initialContract (InitCode (view creationCode theContract))
-           , vmoptCalldata = mempty
+           , vmoptCalldata = CalldataBuffer mempty
            , vmoptValue = 0
            , vmoptAddress = testAddress
            , vmoptCaller = litAddr testCaller

src/hevm/src/EVM/VMTest.hs

@@ -255,7 +255,7 @@ parseVmOpts v =
        (JSON.Object env, JSON.Object exec) ->
          EVM.VMOpts
            <$> (dataField exec "code" >>= pure . EVM.initialContract . EVM.RuntimeCode)
-           <*> (dataField exec "data" >>= pure . ConcreteBuffer)
+           <*> (dataField exec "data" >>= pure . CalldataBuffer . ConcreteBuffer)
            <*> (w256lit <$> wordField exec "value")
            <*> addrField exec "address"
            <*> (litAddr <$> addrField exec "caller")
@@ -376,7 +376,7 @@ fromCreateBlockchainCase block tx preState postState =
       in Right $ Case
          (EVM.VMOpts
           { vmoptContract      = EVM.initialContract (EVM.InitCode (txData tx))
-          , vmoptCalldata      = mempty
+          , vmoptCalldata      = CalldataBuffer mempty
           , vmoptValue         = w256lit $ txValue tx
           , vmoptAddress       = createdAddr
           , vmoptCaller        = (litAddr origin)
@@ -415,7 +415,7 @@ fromNormalBlockchainCase block tx preState postState =
       (_, _, Just origin, Just checkState) -> Right $ Case
         (EVM.VMOpts
          { vmoptContract      = EVM.initialContract theCode
-         , vmoptCalldata      = ConcreteBuffer $ txData tx
+         , vmoptCalldata      = CalldataBuffer $ ConcreteBuffer $ txData tx
          , vmoptValue         = litWord (EVM.w256 $ txValue tx)
          , vmoptAddress       = toAddr
          , vmoptCaller        = (litAddr origin)