Dynamic buffers #491
Dynamic buffers #491
Conversation
| vm1 calldata' callvalue' caller' | ||
| (contract'' | ||
| & set EVM.storage store | ||
| & set EVM.origStorage store) |
There was a problem hiding this comment.
this was a bug in the previous implementation right?
There was a problem hiding this comment.
Maybe some comparison of gas usage between seth --run-tx and seth send
| @@ -437,7 +437,7 @@ genAbiValue = \case | |||
| AbiTupleType ts -> | |||
| AbiTuple <$> mapM genAbiValue ts | |||
| where | |||
| genUInt n = AbiUInt n <$> arbitraryIntegralWithMax n | |||
| genUInt n = AbiUInt n <$> arbitraryIntegralWithMax (2^n-1) | |||
There was a problem hiding this comment.
this is the fix for the property based tests?
There was a problem hiding this comment.
yeah, I think I need to rebase this
| pre preVM = let SymbolicBuffer bs = ditch 4 (fst $ view (state . calldata) preVM) | ||
| (x, y) = splitAt 32 bs | ||
| pre preVM = let StaticSymBuffer bs = ditch 4 $ view (state . calldata) preVM | ||
| (x, y) = trace ("calldata length: " <> show (length bs)) $ splitAt 32 bs |
There was a problem hiding this comment.
did you mean to leave this trace in?
| @@ -170,7 +170,7 @@ data Cache = Cache | |||
| -- | A way to specify an initial VM state | |||
| data VMOpts = VMOpts | |||
| { vmoptContract :: Contract | |||
| , vmoptCalldata :: (Buffer, (SWord 32)) -- maximum size of uint32 as per eip 1985 | |||
| , vmoptCalldata :: Buffer -- maximum size of uint32 as per eip 1985 | |||
There was a problem hiding this comment.
I don't understand this comment
There was a problem hiding this comment.
We assume the length of calldata is limited to a uint32. But this isn't really relied upon here since we don't carry the length around anymore, so I'll remove this comment
| -- | Burn gas, failing if insufficient gas is available | ||
| burn :: Word -> EVM () -> EVM () |
There was a problem hiding this comment.
total nit but would put the space back here...
| -- RIPEMD-160 | ||
| 0x3 -> num $ (((len input + 31) `div` 32) * 120) + 600 | ||
| 0x3 -> num $ (((l input + 31) `div` 32) * 120) + 600 | ||
| where l i = fromMaybe (error "unsupported: dynamic data to SHA256") (unliteral $ len input) |
There was a problem hiding this comment.
error message seems wrong here?
| -- IDENTITY | ||
| 0x4 -> num $ (((len input + 31) `div` 32) * 3) + 15 | ||
| 0x4 -> num $ (((l input + 31) `div` 32) * 3) + 15 | ||
| where l i = fromMaybe (error "unsupported: dynamic data to SHA256") (unliteral $ len input) |
There was a problem hiding this comment.
error message seems wrong here?
| @@ -2561,11 +2574,13 @@ costOfPrecompile (FeeSchedule {..}) precompileAddr input = | |||
| -- ECMUL | |||
| 0x7 -> g_ecmul | |||
| -- ECPAIRING | |||
| 0x8 -> num $ ((len input) `div` 192) * (num g_pairing_point) + (num g_pairing_base) | |||
| 0x8 -> num $ ((l input) `div` 192) * (num g_pairing_point) + (num g_pairing_base) | |||
| where l i = fromMaybe (error "unsupported: dynamic data to SHA256") (unliteral $ len input) | |||
There was a problem hiding this comment.
error message seems wrong here?
|
|
||
| symAbiArg (AbiBytesType n) | ||
| | n <= 32 = sbytes32 | ||
| | otherwise = error "bad type" | ||
|
|
||
| -- TODO: is this encoding correct? |
There was a problem hiding this comment.
It hasn't really seen any testing yet so I'm not sure
| @@ -713,22 +713,18 @@ symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM | |||
| symvmFromCommand cmd = do | |||
| caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd) | |||
| callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd) | |||
| (calldata', cdlen, pathCond) <- case (calldata cmd, sig cmd) of | |||
| -- fully abstract calldata (up to 1024 bytes) | |||
| calldata' <- case (calldata cmd, sig cmd) of | |||
There was a problem hiding this comment.
If I'm reading this right, there is currently no command line flag that allows the user to execute with calldata set to a DynamicSymBuffer?
There was a problem hiding this comment.
Right now that's true. You can with loadSymVM though, which I've been experimenting with. Will include it in the cli once things mature
|
There are some test cases in the smt checker test suite that use dynamic data (under Unfortunately the smt checker tests are executed with |
Introduces support for dynamic data types in memory and calldata (and all over the place, really) through SMT lists. These are currently only supported by z3.
Some clean up needs to happen before this is ready to merge, but I am at the point where I want to trigger some more tests.
There will also be a need for some more execution modes, such as
--no-gas-checksor--no-memory-checksin order to avoid constantly queries z3 about stuff that isn't particularly interesting from a security perspective.