RFC: allow to concretize dynamic arrays in calldata up to N values#1057
RFC: allow to concretize dynamic arrays in calldata up to N values#1057gustavo-grieco wants to merge 3 commits intomainfrom
Conversation
|
Nice! Let's add 2-3 test cases where the calldata would need to be longer than 100 to be able to find the CEX. In these cases, the system should give the user an |
| } |] | ||
| let sig = Just $ Sig "fun(bytes)" [AbiBytesDynamicType] | ||
| (e, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts | ||
| assertBoolM "must report partial due to bounded bytes" $ any isPartial e |
|
Looking a LOT better, thanks!!! |
|
I think this is okay-ish? @blishko do you wanna have a look? The only thing I don't like is the "insert a Partial in the result to warn" because it feels like that should be kinda automatic the way the system works. But it's possible that I am wrong, so I approve. |
|
@msooseth, you are bringing up a very good point. I don't understand why should the analysis be inserting this extra |
|
Maybe we need a different kind of partial type? |
3 participants
Description
This is an attempt to introduce size concretization for dynamic arrays to fix #847 with a similar approach to halmos. Some limitations: (1) it will only work with
calldataparameters and (2) it will not work with recursive/complex dynamic types.Checklist