Hash-related evaluation discrepancies

[pschanely]

This is hub for conversations about hash-related evaluation discrepancies.

Background

To make CrossHair effective at reasoning about sets and dictionaries, we avoid hashing at all costs. For example item in myset, when run under CrossHair, iterates over each element in myset and checks whether it is equal to item. Yes, this turns the containment check from O(1) to O(N), but it's a small price to pay to avoid reasoning about the hash within the SMT solver.

The Problem

Because CrossHair will perform more comparisons, elements that have unusual __eq__ definitions could cause CrossHair to behave differently than the code would otherwise.

For example:

@dataclasses.dataclass
class Foo:
  x: int
  def __hash__(self):
    return hash(self.x)
  def __eq__(self, other):
    return self.x == other.x

The last line should (likely) be return isinstance(other, Foo) and self.x == other.x - but let's assume you forgot the type check. Now, let's say you have a set of Foo objects, foo_set, and evaluate "stringy" in foo_set. In regular Python, it probably just returns False. But, if you evaluate this under CrossHair, you'll get: AttributeError: 'str' object has no attribute 'x'.

Solutions/Mitigations

Currently, we just accept this inconsistency, and encourage users to use tests or contracts to ensure that __eq__ and __hash__ methods are well-formed, pure, and consistent with each other.

But there are other approaches we might consider. For instance,

• We might wait to find a counterexample and then re-run it in a more faithful manner afterwards to check it.
• Alternatively, we might "solve" the problem by making it easier to run CPython like CrossHair. Similar to how we deal with time.time(), we could provide a context manager that causes all objects to hash to zero.

Feel free to weigh in with your own ideas or opinions here.

[Zac-HD]

We might wait to find a counterexample and then re-run it in a more faithful manner afterwards to check it.

I'm a fan of this one, because it'd work for hypothesis-crosshair: you just mark that iteration as invalid, and try again next time (including maybe learning that a particular object has a weird hash/eq definition? hmm...)

[amacfie]

The Python docs say "The only required property [for __hash__] is that objects which compare equal have the same hash value". I would want CrossHair to flag violations of this by default as a kind of implicit contract.