halmos
halmos copied to clipboard
TypeError: object of type 'BitVecRef' has no len() in padded_slice
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