-
Notifications
You must be signed in to change notification settings - Fork 86
errors
This page explains common error messages from Halmos and how to avoid them.
This error usually occurs when an external call is made with dynamic arrays with a symbolic size.
Halmos currently requires dynamically-sized arrays, including bytes and string, to be given with a constant size.
In case of test parameters, the size of dynamic arrays can be specified using the --array-lengths option, or it will be set to the default value if not explicitly specified.
However, when a function is invoked via a low-level call, symbolic-sized arrays might accidentally be provided, leading to this error.
For example, suppose an arbitrary external call is made to an ERC721 token as follows:
function check_NoBackdoor(bytes4 selector) {
bytes memory args = svm.createBytes(1024, 'args');
(bool success,) = address(token).call(abi.encodePacked(selector, args)); // may fail with the error "symbolic CALLDATALOAD offset"
}Since the function selector is symbolic, all external functions will be invoked durin
7D41
g the call, where the symbolic arguments args will be decoded according to the interface of each function.
However, the error will occur when decoding args for the ERC721.safeTransferFrom(address,address,uint256,bytes) function, because the size of the fourth argument bytes is given as symbolic.
This error can be avoided by explicitly constructing the arguments for the safeTransferFrom function as follows:
function check_NoBackdoor(bytes4 selector) {
bytes memory args;
if (selector == bytes4(0xb88d4fde)) { // bytes4(keccak256("safeTransferFrom(address,address,uint256,bytes)"))
args = abi.encode(svm.createAddress('from'), svm.createAddress('to'), svm.createUint256('tokenId'), svm.createBytes(96, 'data'));
} else {
args = svm.createBytes(1024, 'args');
}
(bool success,) = address(token).call(abi.encodePacked(selector, args));
}We plan to provide additional halmos cheatcodes (e.g., this) that can improve usability when making an arbitrary external call.
Halmos expects a single path out of the constructor, otherwise it's not clear what the starting state should be.
Solutions:
- avoid executing code in the constructor, especially if it introduces potential failure conditions. Instead, move it to
setUp()and addvm.assume()calls to rule out the paths you don't want. - run with
halmos --solver-timeout-branching 0(see non-determinism)
Halmos supports only a subset of the Foundry cheatcodes. The list of currently supported cheatcodes can be found here.