Fine-tune shrinking behavior

[aviggiano]

Description

In most cases, shrinking a transaction input is not necessary to understand why a property broke.

This is especially true when bounding the input parameters since what Medusa sees as a maximum/minimum value may differ from what the clamping algorithm considers the valid range.

In some cases, such as in external testing, addresses are often mapped to Medusa's default list of actors (address(0x10000), address(0x20000), address(0x30000)), so converting from address(0x1fffffffe) to address(0xdeadbeef) is even more pointless.

Feature Request

This is a feature request to add additional configuration parameters to fine-tune the shrinking behavior.

Currently, as I understand it, the fuzzer tries to minimize both the number of calls that led to a broken property and each call's inputs.

By splitting the shrinkLimit value into shrinkLimitCalls and shrinkLimitValues, for example, we would allow developers to select which behavior they want from the fuzzer.

[0xalpharush]

We can implement this level of granularity; however, if we use the same shrinking algo as Echidna, setting shrinkLimitValues to a low number may limit the ability of number of calls to be reduced. That is, sometimes the call sequence is shortened by discovering an alternative input during shrinking that makes another call redundant.

[aviggiano]

That is, sometimes the call sequence is shortened by discovering an alternative input during shrinking that makes another call redundant.

Good point, I hadn't considered that.

So maybe it's worth reconsidering if my idea makes sense.

One reason to still implement this is that I assume it would result in an improvement proportional to the number of input parameters, which can be significant. For example, if I have a function fn(uint, uint, uint, uint) and I don't care about simplifying its arguments, I assume this could result in a 4x speedup of this particular step, just by removing this optimization from the algorithm.

I guess this would be dependent on the specific scenario, but it may still be worth experimenting.