crytic / medusa

Parallelized, coverage-guided, mutational Solidity smart contract fuzzing, powered by go-ethereum
https://secure-contracts.com/program-analysis/medusa/docs/src/
GNU Affero General Public License v3.0
303 stars 40 forks source link

revert in property function is treated as failure and a trace is not given #327

Closed 0xalpharush closed 3 months ago

0xalpharush commented 8 months ago

I had an overflow in the property (in an inner call) and it was failing without showing the trace or indicating that the property is false. It's not very intuitive to classify this as a failure and difficult to debug. In fact, it can obscure truly failing property tests (that return false) due to the first failing input being shown https://github.com/crytic/medusa/blob/72e9b8586ad93b37ff9063ccf3f5b471f934c264/fuzzing/test_case_property_provider.go#L101-L104

I would expect this to be configurable like assertion mode (perhaps they could just be shared?)

                "panicCodeConfig": {
                    "failOnCompilerInsertedPanic": false,
                    "failOnAssertion": true,
                    "failOnArithmeticUnderflow": false,
                    "failOnDivideByZero": false,
                    "failOnEnumTypeConversionOutOfBounds": false,
                    "failOnIncorrectStorageAccess": false,
                    "failOnPopEmptyArray": false,
                    "failOnOutOfBoundsArrayAccess": false,
                    "failOnAllocateTooMuchMemory": false,
                    "failOnCallUninitializedVariable": false
                }
            },
anishnaik commented 8 months ago

Well so this is expected behavior and also a bug at the same time.

Expected behavior: A property test that reverts or panics is still considered a test failure. I'm pretty sure this is how echidna does it as well?

Bug: We should attach an execution trace in case of reverts/panics. We should update this.