halmos icon indicating copy to clipboard operation
halmos copied to clipboard

TypeError: object of type 'BitVecRef' has no len() in padded_slice

Open 0xkarmacoma opened this issue 10 months ago • 1 comments

Repro with:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.15;

import "forge-std/Test.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";
import {console2} from "forge-std/console2.sol";

contract WithImmutable {
    address immutable target;

    constructor(address _target) {
        target = _target;
        console2.log("address(withImmutable).code (in constructor)");
        dumpcode();
    }

    function isTarget(address other) external returns (bool) {
        // console2.log("address(withImmutable).code (in isTarget)");
        // dumpcode();
        return other == target;
    }

    function dumpcode() internal {
        uint256 codelength;
        assembly {
            codelength := codesize()
        }

        bytes memory code = new bytes(codelength);
        assembly {
            codecopy(add(code, 0x20), 0, codesize())
        }
        console2.logBytes(code);
    }
}

contract Test71 is Test, SymTest {
    WithImmutable withImmutable;

    function setUp() public {
        address x = svm.createAddress("x");
        withImmutable = new WithImmutable(x);
        // console2.log("type(WithImmutable).creationCode");
        // console2.logBytes(type(WithImmutable).creationCode);
    }

    function test_withConcreteImmutable() external {
        assert(!withImmutable.isTarget(address(0)));
    }

    // counterexample expected
    function test_symbolicImmutable(address y) external {
        assert(!withImmutable.isTarget(y));
    }
}

Results in:

Running 1 tests for test/71_symbolicImmutable.t.sol:Test71
[console.log] address(withImmutable).code (in constructor)
Error: setUp() failed: TypeError: object of type 'BitVecRef' has no len()
Traceback (most recent call last):
  File "/Users/karma/projects/halmos/src/halmos/__main__.py", line 957, in run_sequential
    setup_ex = setup(
               ^^^^^^
  File "/Users/karma/projects/halmos/src/halmos/__main__.py", line 463, in setup
    for idx, setup_ex in enumerate(setup_exs_all):
  File "/Users/karma/projects/halmos/src/halmos/sevm.py", line 2515, in run
    data = padded_slice(calldata, offset, size, con(0, 8))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/karma/projects/halmos/src/halmos/sevm.py", line 125, in padded_slice
    n = len(lst)
        ^^^^^^^^
TypeError: object of type 'BitVecRef' has no len()
Symbolic test result: 0 passed; 1 failed; time: 0.31s

0xkarmacoma avatar Mar 30 '24 00:03 0xkarmacoma