errors

This page explains common error messages from Halmos and how to avoid them.

symbolic CALLDATALOAD offset

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 during 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.

Error: setUp() failed: ValueError: constructor: # of paths: 2

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 add vm.assume() calls to rule out the paths you don't want.
• run with halmos --solver-timeout-branching 0 (see non-determinism)