vm.createFork() not supported

[fyang1024]

Describe the bug
halmos threw an error when the setUp() function invokes vm operations.

The error on the console was

Traceback (most recent call last):
File "/Users/.../Library/Python/3.9/bin/halmos", line 8, in
sys.exit(main())
File "/Users/.../Library/Python/3.9/lib/python/site-packages/halmos/main.py", line 474, in main
setup_ex = setup(hexcode, abi, srcmap, srcs, args, setup_sig, options)
File "/Users/.../Library/Python/3.9/lib/python/site-packages/halmos/main.py", line 132, in setup
if (setup_opcode != 'STOP' and setup_opcode != 'RETURN') or setup_ex.failed: raise ValueError('setUp() failed')
ValueError: setUp() failed

To Reproduce

1. Create a simple test in a foundry project as below

// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity ^0.8.13;

import "forge-std/Test.sol";

contract MyTest is Test {

    function setUp() public {
       vm.createFork(vm.envString("RPC_URL_MAINNET"));
    }

    function testFailX() pure public {
        revert();
    }
}

2. run forge test

3. run halmos

Environment:

• OS: macOS
• Python version: 3.9.6
• Halmos and other dependency versions:
  • halmos 0.0.4
  • crytic-compile 0.3.0
  • z3-solver 4.12.1.0

Additional context

If we comment out the vm call like this:

   function setUp() public {
       // vm.createFork(vm.envString("RPC_URL_MAINNET"));
    }

halmos can do the verification, but it produces opposite result for testFail... tests. When foundry reports a PASS, halmos reports a FAILURE, and vice versa.

[daejunpark]

Fork testing (as well as other cheat codes) are currently not supported. However, depending on your use case, you may be able to achieve similar results without them in Halmos. Please consider joining the Halmos chat to discuss further: https://t.me/+4UhzHduai3MzZmUx

Additionally, please note that the testFail prefix is not currently recognized, and is treated as a normal test. We plan to add support for this in the future (#15).