Poor coverage with solc 0.5.8

VeraBE commented 5 years ago

OS / Environment

Description: Linux Mint 18.3 Sylvia Release: 18.3 Codename: sylvia

Manticore version

Version: 0.2.5

Python version

Python 3.6.5 :: Anaconda, Inc.

Summary of the problem

A simple example works properly on solc version 0.4.25 but it doesn't when using 0.5.8. I would expect a message on the repo if a specific version is required for it to work.

Step to reproduce the behavior

Analyze this contract using the client and both solc versions:

contract FindParam {
    function alwaysFails(int param) public {
       if (param == 1) {
                assert(false);
       }  
    }
}

Expected behavior

I would expect a transaction that calls the function with the value needed for it to get a full code coverage.

Actual behavior

It doesn't even call the function.

feliam commented 5 years ago

Hello @VeraBE thank you for trying our tool. This is somehow an expected issue. We have plans to solve this but you may just downgrade to an older solidity compiler to make it just work for now.

-- This issue happens because ethereum changed the semantics of some the instructions in the EVM spec and manticore still just implement an older version of it. Solc 0.5.8 makes this evident because it seems to use the new meaning of such instruction.

Previously the instruction with opcode 1C meant THROW(as implemented by mcoreEVM) but it was changed to some shift operation, see https://eips.ethereum.org/EIPS/eip-145. ((Note that contracts - code is law - that relied on old specification changed their behavior in the fork ))

0x5c09cd29967fafcc2ddef00adda37b01d04c71ee: ---------------------------------------------------------------------------------------------------------------------------------------------------
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee: 0x001d: (1c)INVALID  Unspecified invalid instruction.
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee: Stack                                                                           Memory
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:          top 0x00000000000000000000000000000000000000000000000000000000000000e0 0000  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:              <BitVecConcat at 7f8b8020a978>                                     0010  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:                                                                                 0020  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:                                                                                 0030  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:                                                                                 0040  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:                                                                                 0050  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:                                                                                 0060  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee:                                                                                 0070  00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00   ................
0x5c09cd29967fafcc2ddef00adda37b01d04c71ee: Gas: 2999928

VeraBE commented 5 years ago

I understand, but I reported this mostly because I consider it should at least be documented somewhere to avoid people wasting their time

trailofbits / manticore