a16z / halmos

A symbolic testing tool for EVM smart contracts
GNU Affero General Public License v3.0
802 stars 65 forks source link

fix: concretize calldatacopy #364

Closed daejunpark closed 2 weeks ago

daejunpark commented 2 weeks ago

there are two instructions that read calldata, and their concretization logic works as follows:

this behavior is based on typical calldata decoding logic, where the length of dynamic arguments is first read using calldataload, and their data is then read using either calldataload or calldatacopy. for example, see the test provided in #371.