Hash collision for constants

[karlwessel]

I am using the latest version from ale/3.0 branch and spend a few hours tracking down a bug caused by a hash collision of two constants.

Here is a minimal working example:

julia> using Metatheory

julia> a = [0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100]
4-element Vector{UInt64}:
 0x0000000000000080
 0x0000000000100000
 0x0000000000000400
 0x0000000000000100

julia> b = [0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400]
4-element Vector{UInt64}:
 0x0000000000000100
 0x0000000000100000
 0x0000000000000080
 0x0000000000000400

julia> a == b
false

julia> hash(a) == hash(b)
true

julia> EGraph(:($a - $b))
EGraph{Expr, Nothing} with 2 e-classes:
  1 => [UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100]]
  2 => [%1 - %1]

I don't know how to solve this problem since VecExpr of a constant only stores the hash, I think, and therefore can't be used to point to the correct constant.

PS: Thanks to mxhbl from discourse for documenting a simple hash collision in julia :).

[0x0f0f0f]

thanks @karlwessel . good MWE of a problem we have seen already

cc @gkronber - i remember we discussed this a while ago, to handle hash collisions in the consmap. do we have anything in mind on how to fix this issue?

[gkronber]

I briefly tried to understand the problem.
I believe the hash collisions we had in #261 was a different problem.

Without looking into it in detail, I believe that the problem here is that VecExpr only holds a hash of an expression in "position 4" and instead it should be able to compare the full expression.

Metatheory.jl/src/vecexpr.jl

Lines 39 to 44 in 74f9d5b

	An e-node is represented by `Vector{Id}` where:
	* Position 1 stores the hash of the rest of the `VecExpr`.
	* Position 2 stores the bit flags (`isexpr` or `iscall`).
	* Position 3 stores the signature
	* Position 4 stores the hash of the `head` (if `isexpr`) or node value in the e-graph constants.
	* The rest of the positions store the e-class ids of the children nodes.

Generally, I'm not sure if the example shows a valid use case at all, because a and b are mutable types.
Is it meaningful to create an e-graph for the expression Int[1,2,3] - Int[4,5,6]?

[karlwessel]

The direct solution I can think of is changing the map of constants from Dict{UInt, Any} to Dict{UInt, Vector{Any}} and before adding a constant to the map check each element of the vector the hash maps to for equality with the new constant. So basically how you typically handle hash collisions in a hash table.

VecExpr then would need to store store a Tuple of the hash and the index in the array instead of only the hash.

This would make it slower, since you always have to do at least one equality check additionally to the hash calculation when adding new or existing constants. But I think to correctly handle hash collisions you will always have to do that.

[gkronber]

After thinking a bit more about this, I have to correct myself. The way how this is handled in VecExpr is probably not the underlying issue.

I played around with your example. It seems it is the interpolation of a and b which does not work (and I am not sure if it should).

# reproduce
using Metatheory

julia> a = [0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100]
4-element Vector{UInt64}:
 0x0000000000000080
 0x0000000000100000
 0x0000000000000400
 0x0000000000000100

julia> b = [0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400]
4-element Vector{UInt64}:
 0x0000000000000100
 0x0000000000100000
 0x0000000000000080
 0x0000000000000400

julia> hash(a) == hash(b)
true

julia> EGraph(:($a - $b))
EGraph{Expr, Nothing} with 2 e-classes:
  1 => [UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100]]
  2 => [%1 - %1]

# but...

julia> EGraph(:(UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100] - UInt64[0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400]))
EGraph{Expr, Nothing} with 8 e-classes:
  1 => [UInt64]
  2 => [128]
  3 => [1048576]
  4 => [1024]
  5 => [256]
  6 => [(%1)[%2, %3, %4, %5]]
  7 => [(%1)[%5, %3, %2, %4]]
  8 => [%6 - %7]

julia> expr = :(UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100] - UInt64[0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400])
:(UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100] - UInt64[0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400])

julia> EGraph(expr)
EGraph{Expr, Nothing} with 8 e-classes:
  1 => [UInt64]
  2 => [128]
  3 => [1048576]
  4 => [1024]
  5 => [256]
  6 => [(%1)[%2, %3, %4, %5]]
  7 => [(%1)[%5, %3, %2, %4]]
  8 => [%6 - %7]

julia> expr = :($a - $b)
:(UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100] - UInt64[0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400])

julia> EGraph(expr)
EGraph{Expr, Nothing} with 2 e-classes:
  1 => [UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100]]
  2 => [%1 - %1]


julia> dump(expr)
Expr
  head: Symbol call
  args: Array{Any}((3,))
    1: Symbol -
    2: Array{UInt64}((4,)) UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100]
    3: Array{UInt64}((4,)) UInt64[0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400]

julia> dump(:(UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100] - UInt64[0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400]))
Expr
  head: Symbol call
  args: Array{Any}((3,))
    1: Symbol -
    2: Expr
      head: Symbol ref
      args: Array{Any}((5,))
        1: Symbol UInt64
        2: UInt64 0x0000000000000080
        3: UInt64 0x0000000000100000
        4: UInt64 0x0000000000000400
        5: UInt64 0x0000000000000100
    3: Expr
      head: Symbol ref
      args: Array{Any}((5,))
        1: Symbol UInt64
        2: UInt64 0x0000000000000100
        3: UInt64 0x0000000000100000
        4: UInt64 0x0000000000000080
        5: UInt64 0x0000000000000400

As you see the two expressions are different, one contains arrays and the other contains the subexpressions to construct arrays (using [...] syntax). I think the second case is correct.

Currently only the hash value is stored in the VecExprs generated for the arrays in

Expr
  head: Symbol call
  args: Array{Any}((3,))
    1: Symbol -
    2: Array{UInt64}((4,)) UInt64[0x0000000000000080, 0x0000000000100000, 0x0000000000000400, 0x0000000000000100]
    3: Array{UInt64}((4,)) UInt64[0x0000000000000100, 0x0000000000100000, 0x0000000000000080, 0x0000000000000400]

[karlwessel]

I think that is just a matter of whether those arrays should be interpreted as a constant or as an expression.

But anyway, the MWE meants to illustrate, that Metatheory currently can't handle hash collisions for constants. And while it might be rare that this happens, it can always happen, and then Metatheory silently returns incorrect results.

A better example would using BigInts instead of Vectors as constants, there it is guarantied that there will be two different BigInts with the same hash value.

[gkronber]

Agree.

The direct solution I can think of is changing the map of constants from Dict{UInt, Any} to Dict{UInt, Vector{Any}}

Can/should we use the existing collision handling of dictionaries by changing from Dict{UInt, Any} to Dict{Any, Nothing} and changing VecExpr to hold the constant value instead of its hash?

This would make it slower, since you always have to do at least one equality check additionally to the hash calculation when adding new or existing constants. But I think to correctly handle hash collisions you will always have to do that.

But only when there is a collision, right?

In any case, if you want to prepare a PR, I'm happy to help in reviewing.

[0x0f0f0f]

I think that is just a matter of whether those arrays should be interpreted as a constant or as an expression.

See #89 - related.

But anyway, the MWE meants to illustrate, that Metatheory currently can't handle hash collisions for constants. And while it might be rare that this happens, it can always happen, and then Metatheory silently returns incorrect results.

A better example would using BigInts instead of Vectors as constants, there it is guarantied that there will be two different BigInts with the same hash value.

Agree. I was thinking of what changes to the hashcons data structure can be made to avoid collisions without sacrificing performance. Applications in theorem proving require correctness. Big efforts were made in making EGraph.memo type stable, by vectorizing expressions and hash/metadata caching in VecExpr, that were major performance improvements.

[karlwessel]

Can/should we use the existing collision handling of dictionaries by changing from Dict{UInt, Any} to Dict{Any, Nothing} and changing VecExpr to hold the constant value instead of its hash?

VecExpr should stay a Vector of Ids.

If there is some hash table implementation in Julia that returns a unique key for any item added, one could use that one instead of the hash value, without needing to change anything else.