a16z / halmos

A symbolic testing tool for EVM smart contracts
GNU Affero General Public License v3.0
819 stars 68 forks source link

Unsupported cheat code `vm.readFile` #213

Open PatrickAlphaC opened 1 year ago

PatrickAlphaC commented 1 year ago

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.
karmacoma-eth commented 1 year ago

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

karmacoma-eth commented 1 year ago

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

karmacoma-eth commented 1 year ago

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

PatrickAlphaC commented 1 year ago

Awesome!