Dynamic buffers via SMT lists #500
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
MrChico
force-pushed
the
slistbuffer
branch
4 times, most recently
from
5b104f4 to
cb523e4
Compare
MrChico
force-pushed
the
slistbuffer
branch
from
1ad0b38 to
5472d0b
Compare
|
getting annoying, mysterious errors in the communication with the solver and sbv |
d-xo
approved these changes
Sep 16, 2020
Comment on lines
+151
to
+160
| -- testCase "calldata beyond length must be 0" $ runSMTWith z3 | ||
| -- $ query $ do calldatalist <- freshVar_ | ||
| -- -- works with length .< 10, but not 100... | ||
| -- constrain $ SL.length calldatalist .< 10 | ||
| -- let cd = DynamicSymBuffer calldatalist | ||
| -- constrain $ 0 ./= readSWord (sw256 $ sFromIntegral $ len cd) cd | ||
| -- checkSat >>= \case | ||
| -- Sat -> error "should be false" | ||
| -- Unsat -> return () | ||
| -- Unk -> error "timed out!" |
There was a problem hiding this comment.
Did you mean to leave this commented?
There was a problem hiding this comment.
I think I will remove this
| Unk -> error "timed out!" | ||
|
|
||
| , | ||
| testCase "comparing function selector" $ runSMTWith z3{transcript=Just "sameno.smt2"} $ do |
There was a problem hiding this comment.
did you mean to leave the transcript here?
Comment on lines
+166
to
+167
| constrain $ SL.length calldatalist .< 100 | ||
| constrain $ sw256 (sFromIntegral $ SL.length calldatalist) .< sw256 100 |
There was a problem hiding this comment.
Why do we need both of these contraints?
There was a problem hiding this comment.
it turned out to yield better performance in practice
Comment on lines
+147
to
+166
| # # OpCalldatacopy | ||
| # "loops/for_loop_array_assignment_memory_memory.sol" | ||
| # "loops/for_loop_array_assignment_memory_storage.sol" | ||
| # "loops/while_loop_array_assignment_memory_memory.sol" | ||
| # "loops/while_loop_array_assignment_memory_storage.sol" | ||
| # "types/address_call.sol" | ||
| # "types/address_delegatecall.sol" | ||
| # "types/address_staticcall.sol" | ||
| # "types/array_aliasing_storage_2.sol" | ||
| # "types/array_aliasing_storage_3.sol" | ||
| # "types/array_aliasing_storage_5.sol" | ||
| # "types/array_branch_1d.sol" | ||
| # "types/array_branches_1d.sol" | ||
| # "types/array_dynamic_parameter_1.sol" | ||
| # "types/array_dynamic_parameter_1_fail.sol" | ||
| # "types/bytes_1.sol" | ||
| # "types/bytes_2.sol" | ||
| # "types/bytes_2_fail.sol" | ||
| # "types/mapping_unsupported_key_type_1.sol" | ||
| # "types/function_type_array_as_reference_type.sol" |
There was a problem hiding this comment.
Did you mean to leave these commented?
| @@ -1721,8 +1721,13 @@ notStatic continue = do | |||
| then vmError StateChangeWhileStatic | |||
| else continue | |||
|
|
|||
| burnSym :: SymWord -> EVM () -> EVM () | |||
| burnSym n continue = case maybeLitWord n of | |||
| Nothing -> continue -- smt query (TODO: no gas mode) | |||
There was a problem hiding this comment.
Does this mean no gas is deduced when dealing with symbolic values?
There was a problem hiding this comment.
currently yes. But there should really be a query made here unless run in --no-gas mode.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Replaces #491