Echidna fails to detect assertions in solc 0.8.x

[ggrieco-tob]

pragma solidity ^0.8.0;
contract Test{    
    function fail(uint x) public{
        assert(false);
    }
    function f() public{}
}

solc implements assertions as requires, but emits the panic event. However, hevm clears the events as expected by any standard EVM implementation.

[MrChico]

actually, hevm keeps logs around even though they are cleared by other implementations. Since they don't effect the state we think it's more valuable to have them around in a testing environment. But I think the Panic thing is an abi-encoded revert output than an event anyway?

[ggrieco-tob]

actually, hevm keeps logs around even though they are cleared by other implementations. Since they don't effect the state we think it's more valuable to have them around in a testing environment.

Right. I just fixed that in an upcoming branch.

But I think the Panic thing is an abi-encoded revert output than an event anyway?

However, it seems hevm fails to provide anything when there is a assertion failure (regardless of how it is encoded). I'm using this code:

type EventMap = M.Map W256 Event
type Events = [Text]

emptyEvents :: TreePos Empty a
emptyEvents = fromForest []

extractEvents :: EventMap -> VM -> Events
extractEvents em vm =
  let forest = traceForest vm
      showTrace trace =
        let ?context = DappContext { _contextInfo = emptyDapp, _contextEnv = vm ^?! EVM.env } in
        case view traceData trace of
          EventTrace (Log _ bytes topics) ->
            case maybeLitWord =<< listToMaybe topics of
              Nothing   -> []
              Just word -> case M.lookup (wordValue word) em of
                             Just (Event name _ types) ->
                               [name <> showValues [t | (t, NotIndexed) <- types] bytes]
                             Nothing -> [pack $ show word]
          ErrorTrace e ->
            case e of
              Revert out -> ["merror " <> "Revert " <> showError out]
              _ -> ["merror " <> pack (show e)]

          _ -> []
  in concat $ concatMap flatten $ fmap (fmap showTrace) forest

but the list of "events" are always empty even with assert(false) using solc 0.8.x.

Any hints?

[ggrieco-tob]

This is already fixed in #674

[ducquangkstn]

Is there any way to bypass this?
I can not find anyway to call opcode 0xfe from assembly script

[ggrieco-tob]

You can either try echidna 2.0 (which is not released yet, but already solved this) or use a special event to signal failure.

[Jack-ZooFiLabs]

How do I install echidna 2.0? tarball/master still points to 1.7.2

[julianmrodri]

As mentioned above, had to use the special event to get it to work in 0.8.x. It is worth to notice that this should replace all asserts.If I place an assert like assert(false); before emitting the event, the failure is missed as well even if the event is emitted later.

pragma solidity ^0.8.7;

contract Test{    
    event AssertionFailed();
 
    function fail(uint x) public{
        emit AssertionFailed();
    }
    
    function f() public{}
}

[ggrieco-tob]

Exactly. this is because reverting deletes all the event. Try echidna 2.0 if you can, to solve this issue.

[julianmrodri]

Where can I find instructions on how to install and run echidna 2.0? Thanks

[ggrieco-tob]

You can get prebuilt binaries here or built the corresponding branch from its PR. Keep in mind that there are small differences in the command line and config options, but let's keep the discussion in that PR so other people can follow it.

[ggrieco-tob]

Already fixed in 2.0.0