Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow to use the FFI cheatcode from HEVM in Echidna #750

Merged
merged 6 commits into from
Jan 26, 2023
Merged

Conversation

ggrieco-tob
Copy link
Member

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.

@ggrieco-tob ggrieco-tob mentioned this pull request Apr 4, 2022
@patrickd-
Copy link

patrickd- commented Apr 4, 2022

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-
Copy link

patrickd- commented Apr 4, 2022

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)

@ggrieco-tob
Copy link
Member Author

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-
Copy link

patrickd- commented Apr 4, 2022

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

@ggrieco-tob
Copy link
Member Author

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-
Copy link

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

@ggrieco-tob
Copy link
Member Author

@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-
Copy link

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!

@ggrieco-tob
Copy link
Member Author

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-
Copy link

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

@ggrieco-tob ggrieco-tob merged commit 89cbbb4 into master Jan 26, 2023
@ggrieco-tob ggrieco-tob deleted the dev-ffi branch January 26, 2023 08:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants