a16z / halmos

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

feat: support for new cheatcode of generating calldata #360

Closed daejunpark closed 2 months ago

daejunpark commented 2 months ago

done:

note:

future work:

karmacoma-eth commented 2 months ago

suggested test:

import pytest
from z3 import BitVec, BitVecSort
from halmos.cheatcodes import permutate_dyn_size, DynamicParams, DynamicArrayType
from halmos.bytevec import ByteVec

# Mock classes and functions
class MockSEVM:
    class Options:
        pass
    options = Options()

class MockExecutor:
    def new_symbol_id(self):
        return 0

class MockFunctionInfo:
    def __init__(self):
        self.name = "testFunction"
        self.signature = "testFunction(uint256[],string)"
        self.selector = "0x12345678"

def test_permutate_dyn_size():
    # Setup
    dyn_param_size = DynamicParams()
    dyn_param_size.append(("param1", 2, DynamicArrayType("uint256")))
    dyn_param_size.append(("param2", 32, str))  # Assuming str represents a dynamic string

    funselector = "0x12345678"
    abi = [
        {
            "name": "testFunction",
            "type": "function",
            "inputs": [
                {"name": "param1", "type": "uint256[]"},
                {"name": "param2", "type": "string"}
            ]
        }
    ]
    funinfo = MockFunctionInfo()
    sevm = MockSEVM()
    ex = MockExecutor()

    # Call the function
    result = permutate_dyn_size(dyn_param_size, funselector, abi, funinfo, sevm, ex)

    # Assertions
    assert len(result) == 12  # 3 options for param1 * 4 options for param2

    # Check that all expected sizes are present
    expected_sizes = {
        "param1": [0, 1, 2],
        "param2": [0, 32, 65, 1024]
    }

    for calldata in result:
        param1_size = int.from_bytes(calldata[36:68], "big")
        param2_size = int.from_bytes(calldata[100:132], "big")

        assert param1_size in expected_sizes["param1"]
        assert param2_size in expected_sizes["param2"]

    # Check that all combinations are present
    combinations = set((int.from_bytes(c[36:68], "big"), int.from_bytes(c[100:132], "big")) for c in result)
    assert len(combinations) == 12

    # Check the structure of the calldata
    for calldata in result:
        assert calldata[:4] == b'\x12\x34\x56\x78'  # function selector
        assert len(calldata) >= 132  # minimum length for two dynamic parameters

if __name__ == "__main__":
    pytest.main([__file__])

and in permutate_dyn_size:

        # consider all size combinations
        arrlen_lst = [
            {**arrlen, p_name: new_size}
            for arrlen in arrlen_lst
            for new_size in new_size_options
        ]
daejunpark commented 2 months ago

the cursor-generated test is added with slight modifications: https://github.com/a16z/halmos/pull/360/commits/7c00d34018740f3a0ee19945c31c6eb5c78cd670

daejunpark commented 2 months ago

@karmacoma-eth this is now ready to review. note that an interface name turns out to be already supported.

daejunpark commented 2 months ago

@karmacoma-eth this is ready for re-review. the multiple calldata encoding for dynamic sizes has been re-implemented to address issues in the previous approach.

btw, to keep this pr minimal, some of your suggestions will be addressed in a separate pr.

daejunpark commented 2 months ago

@karmacoma-eth i've addressed all your comments, and implemented some todo items. this should be enough for the scope of this pr. please take another look when you get a chance.