Unsupported cheat code `vm.readFile`

[PatrickAlphaC]

trafficstars

Describe the bug I am attempting to use my compiled huff contract without hard-coding it into my scripts. I have compiled my huff to compiled_huff.txt. Foundry has a cheatcode called readFile that allows you to read the file in. However, it looks like Halmos doesn't expect this and reverts when this happens.

        string memory path = "compiled_huff.txt";
        string memory huffString = vm.readFile(path);
        bytes memory huffDeployBytecode = vm.parseBytes(huffString);

        address horseStoreHuffAddr;
        assembly {
            horseStoreHuffAddr := create(0, add(huffDeployBytecode, 0x20), mload(huffDeployBytecode))
        }

When running a halmos test, you get this output:

Running 1 tests for test/HorseStoreSymbolic.t.sol:HorseStoreSymbolic
WARNING:Halmos:Warning: setUp() execution encountered an issue at STATICCALL: Unsupported cheat code: calldata = 0x60f9bb1100000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000011636f6d70696c65645f687566662e747874000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
Error: setUp() failed: HalmosException: No successful path found in setUp()

To Reproduce

1. Create a new forge project

forge init

2. Put really anything into a file at the root dir called compiled_huff.txt.

3. Add this file to the test dir

// SPDX-License-Identifier: MIT
pragma solidity 0.8.20;

import {Test, console2} from "forge-std/Test.sol";

contract Base_Test is Test {
    function setUp() public virtual {
        string memory path = "compiled_huff.txt";
        string memory huffString = vm.readFile(path);
    }

    function check_something() public {
        assert(true);
    }
}

4. Run a halmos check

halmos --function check_storeAndReadAreIdentical

Environment:

• OS: MacOS
• Python version: Python
• Halmos and other dependency versions:

halmos==0.1.9
z3-solver==4.12.2.0

Additional context Add any other context about the problem here.

[0xkarmacoma]

This was an attempted workaround for https://github.com/a16z/halmos/issues/214

[0xkarmacoma]

We can implement vm.readFile, in the mean time you can approximate the behavior with

        string[] memory command = new string[](2);
        command[0] = "cat";
        command[1] = "compiled_huff.txt";

        bytes memory bytecode = vm.ffi(command);

⚠️ heads up though, foundry's ffi will parse the hex string and turn it into the equivalent bytes but halmos' ffi will just return the hex string which can't be deployed directly. We will also need to support that for compatibility

[0xkarmacoma]

@PatrickAlphaC As soon as this is merged, it would be a nicer workaround: https://github.com/a16z/halmos/pull/215

[PatrickAlphaC]

Awesome!