Open
Conversation
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
Member
Author
|
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!" |
Contributor
There was a problem hiding this comment.
Did you mean to leave this commented?
Member
Author
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 |
Contributor
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 |
Contributor
There was a problem hiding this comment.
Why do we need both of these contraints?
Member
Author
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" |
Contributor
There was a problem hiding this comment.
Did you mean to leave these commented?
|
|
||
| burnSym :: SymWord -> EVM () -> EVM () | ||
| burnSym n continue = case maybeLitWord n of | ||
| Nothing -> continue -- smt query (TODO: no gas mode) |
Contributor
There was a problem hiding this comment.
Does this mean no gas is deduced when dealing with symbolic values?
Member
Author
There was a problem hiding this comment.
currently yes. But there should really be a query made here unless run in --no-gas mode.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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