Certora/gambit

Issue with swap-arguments-function mutation in Gambit tool: Limited to functions with 2 arguments

Opened this issue · 2 comments

As a user of the Gambit tool, I have noticed an issue with the swap-arguments-function mutation, where the mutation is limited to functions with only 2 arguments.

According to the Gambit documentation, the swap-arguments-function mutation is intended to swap the arguments of a function call. However, I have observed that the mutation only swaps the arguments for functions with exactly 2 arguments. Functions with more than 2 arguments are not mutated.

I believe that this is a significant limitation of the mutation operator. In Solidity contracts, it is common to have functions with more than 2 arguments, and the swap-arguments-function mutation could be more effective if it could be applied to these functions as well.

I would like to suggest that the Gambit team review the implementation of the swap-arguments-function mutation and consider expanding its functionality to include functions with more than 2 arguments.

Thank you for your attention to this matter.

Hey @Sta1400! I'm going to be going over mutation operators at some point soon and I'm not sure that swap-arguments-function is going to make the cut. I'm going to chat with users at some point, and we might include an option to use this if it is explicitly indicated.

I welcome your feedback though, let me know if you think this is a useful operator! One of my worries is that it might have a high equivalence rate. E.g. max(a, b) is equivalent to max(b,a). Not sure how much this comes up in the wild.

Another issue is that it's not clear what the semantics should be on more than two arguments. With two arguments there is a clear canonical swap that we can perform. On a function with four args, say all ints, there are now 23 possible non-identity permutations to those arguments...which one do we pick? This could potentially introduce nondeterminism into our set, or it will overload our mutant set with this one kind of mutant.

Anyway, just thoughts I'm having, not sure the right solution yet, and definitely want to include this if it's useful for users!

Another solution: rotate the args instead of 'swapping' them. Just do a right rotate, or a left rotate