Find counter-examples without nan while performing diffbehavior

[Abhiram98]

While performing diffbehavior with float arguments, crosshair finds some funny counter-examples.

Crosshair reports a counter-example while comparing the below functions:

def original(num: float):
    return num+1

def rewrite(num: float):
    return num+1

Crosshair output:

Given: (num=nan),
  temp.test.original : returns nan
   temp.test.rewrite : returns nan

This is happening because python itself treats nan to be unequal.

float('nan')==float('nan') #False

[pschanely]

Ah. Yes, I agree with your assessment. I've got a few options for handling this, but will need to do some experimentation. The case you mention is easy to handle, but more generally we need to be able to detect nans that are nested inside containers and other objects, so it's not as easy a fix as you might expect. More soon.

[Abhiram98]

I agree that this is a very trivial example.
To add more nuance, the line 230 in run_iteration was also checking that the args are equal after execution -- but this fails in case the arguments are nan or list[nan].

I also tried patching ‎PreciseIeeeSymbolicFloat, to make nans equal, but that didn't fully work.

[pschanely]

I agree that this is a very trivial example. To add more nuance, the line 230 in run_iteration was also checking that the args are equal after execution -- but this fails in case the arguments are nan or list[nan].

Good catch!

I also tried patching ‎PreciseIeeeSymbolicFloat, to make nans equal, but that didn't fully work.

Ha, you are in the weeds already! Yeah, first, concrete NaNs could still be generated and returned, so patching the symbolics is insufficient, and second, we don't want to universally change the NaN equality behavior, because that may be important for correctly analyzing user code - we only want to change the behavior when comparing the returns (and arguments) for diff_behavior.

I spent some time today investigating a fully correct implementation, and ... it's difficult. It looks like many equality checks are done at the C level - __eq__ often won't get trace events, and many checks don't even hit a comparison opcode. For the moment, I think I'm inclined to implement a partial solution - something like this (still needs docs & tests), which would handle NaNs in containers at least (but not when inside user-defined objects). I generally detest partial solutions, but this issue seems common enough that it makes sense to do what we can. Opinions welcome!

[pschanely]

I've released an initial revision addressing this in v0.0.79!

[Abhiram98]

Awesome! Thank you