Allow to use the FFI cheatcode from HEVM in Echidna

[gustavo-grieco]

This PR allows to use the FFI cheatcode from HEVM in Echidna if the allowFFI: true is used in the configuration yaml. This is disabled by default.

[patrickd-]

Gave it a quick try, but as soon as I add allowFFI: true to config it's stuck on startup

$ echidna-test --contract Test --config test.yaml src/test/test.sol

                                                                                                                                                        
                ┌─────────────────────────────────────────────────────Echidna 2.0.0────────────────────────────────────────────────────┐                
                │ Tests found: 0                                                                                                       │                
                │ Seed: 0                                                                                                              │                
                │─────────────────────────────────────────────────────────Tests────────────────────────────────────────────────────────│                
                │ Starting up, please wait...                                                                                          │                
                └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘                

Same contract works as expected with foundry:

$ forge test --match-path src/test/test.sol 
[⠒] Compiling...
No files changed, compilation skipped

Running 1 test for src/test/test.sol:Test
[FAIL. Reason: Assertion violated. Counterexample: calldata=0x2f570a2300000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000000, args=[0x]] test(bytes) (runs: 0, μ: 0, ~: 0)
Traces:
  [7049] Test::test(0x) 
    ├─ [0] VM::ffi(["echo", "-n", "0x00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000002676d000000000000000000000000000000000000000000000000000000000000"]) 
    │   └─ ← 0x00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000002676d000000000000000000000000000000000000000000000000000000000000
    └─ ← "Assertion violated"

Test result: FAILED. 0 passed; 1 failed; finished in 19.37ms

---

Source:

testMode: assertion
seqLen: 1
allowFFI: true

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.9;

address constant HEVM_ADDRESS = 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D;
interface CheatCodes {
    // Performs a foreign function call via terminal
    function ffi(string[] calldata) external returns (bytes memory);
}

contract Test {
    function test(bytes memory input) external {
        string[] memory inputs = new string[](3);
        inputs[0] = "echo";
        inputs[1] = "-n";
        // ABI encoded "gm", as a string
        inputs[2] = "0x00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000002676d000000000000000000000000000000000000000000000000000000000000";

        bytes memory res = CheatCodes(HEVM_ADDRESS).ffi(inputs);
        string memory output = abi.decode(res, (string));
        // Should fail.
        assert(keccak256(bytes(output)) == keccak256("gm2"));
    }
}

[patrickd-]

testMode: assertion
seqLen: 1
allowFFI: true
initialize: echidna.json

After adding an initialization file it's no longer stuck at startup but then the FFI call apparently reverts and the assertion that is supposed to fail does not. (same behavior as if allowFFI is off)

Ah, I assume it's because of this?

       (Right (ethenoInit :: [Etheno])) -> do
         -- Execute contract creations and initial transactions,
         let initVM = foldM execEthenoTxs () ethenoInit
-        (_, vm') <- runStateT initVM initialVM
+        (_, vm') <- runStateT initVM (initialVM False) -- No FFI is allowed here

Is using FFI with init files really not possible? (Asking because foundry allows something similar via --fork-url with --ffi flag stil working)

[gustavo-grieco]

You don't need to add echidna initiation here. However, hevm seems to be crashing for some reason:

echidna-test: VM failed for unhandled reason, Query <EVM.Query: do ffi: ["echo","-n","0x00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000002676d000000000000000000000000000000000000000000000000000000000000"]. This shouldn't happen. Please file a ticket with this error message and steps to reproduce!

I'm investigating this issue.

[patrickd-]

Thanks!

I'd like to use the echidna initialize config to deploy some contracts with incompatible solidity version and then fuzz on a contract that also makes use of the FFI cheatcode, that's why I'm asking about initiation

[gustavo-grieco]

Uhm, I see. I will keep working on ths PR to include that feature. Btw, it seems that FFI is implemented using oracles in HEVM:

https://github.com/dapphub/dapptools/blob/74a54da1dc77fe71eab5d8b93ed3f63904f151a1/src/hevm/src/EVM/Fetch.hs#L171-L179

This can take a little longer to implement, but it still should be doable soon.

[patrickd-]

I don't know anything about Haskell but let me know if I can help somehow

[gustavo-grieco]

@patrickd- can you re-try using the latest commit in this branch? It should work with the example (but the .json initialization is still need to be fixed before you can use it)

[patrickd-]

The only difference to foundry that I noticed is that in Echidna the stdout hex always needs to be prefixed with 0x while foundry is fine with omitting that.

But that's not much of an issue.. besides that everything seems to be working as expected!

[gustavo-grieco]

Just push the code to allow ffi when using a json initialization. However, the code is very preliminary, so consider this like an a beta code that will be improved in the future before merging it.

[patrickd-]

Awesome! Everything seems to work fine at least. I'll let you know if I notice any issues