This project is read-only.
1

Closed

Checking for Expr equality is utterly Broken in Boogie

description

There is a comment in AbsyExpr.cs about Expr classes
  //---------------------------------------------------------------------
  // Expressions
  //
  // For expressions, we override the Equals and GetHashCode method to
  // implement structural equality.  Note this is not logical equivalence
  // and is not modulo alpha-renaming.
  //---------------------------------------------------------------------
However the overloads as they are implemented right now check for reference equality which is utterly pointless because that's what the default version of Equals() does.

Example for LiteralExpr
    public override bool Equals(object obj) {
      if (obj == null)
        return false;
      if (!(obj is LiteralExpr))
        return false;

      LiteralExpr other = (LiteralExpr)obj;
      return object.Equals(this.Val, other.Val);
    }
This isn't doing structural equality because it's calling object.Equals(this.Val, other.Val) which is reference equality!

similarly for NAryExpr
    public override bool Equals(object obj) {
      if (obj == null)
        return false;
      if (!(obj is NAryExpr))
        return false;

      NAryExpr other = (NAryExpr)obj;
      return object.Equals(this.Fun, other.Fun) && object.Equals(this.Args, other.Args);
    }
Again using object.Equals() is completely wrong because this checking for reference equality!

Is there a reason for the current situation? The only thing I can think of is that having Equals() overloaded to means reference equality could hinder performance if an Expr is used as a Key in a Dictionary or other hash based data structured.

Are there any objections to be modifying the Equals() overrides on Expr classes to behave as structural equality rather than reference? Alternatively I could add a virtual bool StructuralEquality(Expr other) method of Expr and implement structural equality in those methods instead.
Closed Sep 21, 2014 at 10:22 PM by danliew

comments

danrosen wrote Jul 31, 2014 at 5:49 PM

Hi Dan,

It is not as bad as it looks, the equality is just slightly broken.

The call object.Equals(a,b) does not do reference equality if the dynamic type of a overrides bool Equals(object other), and that is what the Absy nodes do.

For NAryExpr, it is indeed broken since object.Equals on the lists indeed means reference equality on the spine.

I have recently looked into this because I implemented an alpha equivalence check to make boogie lambdas equal up to alpha renaming, and for this I had to fix the equals. I haven't touched the hash codes generation, though.

I would like to push my patch in the upcoming days, but it seems like you and me are the only one who cares about this piece of Boogie, so here is a question for you. The Quantifier expressions say that they are doing equivalence without caring about triggers and attributes. This is not so good for the alpha equivalence check, since the expressions in these may contain free variables. So I changed so that Quantifier expressions also check the structural equivalence of their triggers and attributes. Does that sound alright for you?

Finally, I'm curious about what you are using the equality for.

Thanks,
Dan

danliew wrote Jul 31, 2014 at 8:55 PM

It is not as bad as it looks, the equality is just slightly broken.
Yes I realised this when I fixed the issues recently. NAryExpr and BinderExpr were broken. I've fixed Equals() and GetHashCode() on these classes in recent commits (e1dd6c7b9f3b, 024a3b37a940, 156096b4abcd c618a7dfa7a7)
I have recently looked into this because I implemented an alpha equivalence check to make boogie lambdas equal up to alpha renaming, and for this I had to fix the equals. I haven't touched the hash codes generation, though.
Sorry I am not that familiar with "alpha renaming" so I'd like to check we're talking about the same thing. Is alpha renaming where bound variables in quantifiers can be renamed so two logically (but not syntactically) equivalent expressions become syntactically equivalent?

e.g.

∀ X :: f(X) <==> X > 15

∀ Y:: f(Y) <==> Y > 15

These are logically equivalent but not syntactically equivalent. I believe Boogie's current implementation would consider these expressions not be equal.

but if Y is renamed to X in the above formula then the two formulas become syntactically equivalent.

Assuming I've understood "alpha renaming" correctly, when you say "to make boogie lambdas equal up to alpha renaming", are you saying you've implemented Equals() with or without doing any alpha-renaming?
I would like to push my patch in the upcoming days
If you don't want alpha renaming in Equals() you should take what is currently in upstream Boogie because I fixed BinderExpr which in turn has fixed LambdaExpr already.

If you do want to support alpha renaming in Equals() I would be heavily against that because for my use case Equals() needs to be fast. I don't know how you would implement Equals() with alpha-renaming but I suspect it would be very slow.
The Quantifier expressions say that they are doing equivalence without caring about triggers and attributes. This is not so good for the alpha equivalence check, since the expressions in these may contain free variables.
I'm sorry I don't understand the above. You need to explain exactly what you mean by "alpha equivalence" here. Sorry, this may sound dumb but I don't know Lambda calculus and never studied it. Until I can fully understand what you're doing I can't say if I think it's okay.
Finally, I'm curious about what you are using the equality for.
Here's how I'm using equality: Basically I'm currently implementing a symbolic execution engine for Boogie. Equality is useful to me in the following scenarios.
  • Constant Folding. If I find an == in the expression tree I can try constant folding it by seeing if it's children are structurally equal. If they are structurally equal then I can fold this to True. For this use case ignoring triggers and attributes is a good thing because they have nothing to do with the Truth of the expression.
  • Constraint caching. I'm using the Expr classes to represent boolean constraints and execution paths. Being able to know whether or not a constraint has been seen before requires GetHashCode() and Equals() to function correctly.
Both of these use cases ideally require Equals() and GetHashCode() to be as fast as possible.

danrosen wrote Jul 31, 2014 at 11:47 PM

Hi Dan,

Alpha equivalence means equivalence up to renaming, so yes, your example with the quantifiers would indeed be alpha equivalent.

The alpha equivalence check I have implemented calls the equals method, but it does not change it in any way. It just requires that it is real structural equivalence. To check for alpha equivalence, you call a different function than equals.

Regarding the quantifiers: you have a point that in some aspect the triggers don't matter for constant folding, but they might matter for equivalence. Say that you have
(lambda x :: (forall y :: { f(g(x,y)) } f(g(x,y)) == x + y))
and
(lambda x :: (forall y :: f(g(x,y)) == x + y)).
You don't really want to treat these as the same lambda, as they have different performance.

I don't know how to settle this. I would have equivalence including the triggers and attributes, but I can see that you don't. It would be nice if you could parameterise the equals function. We could add such an attribute.

Thanks,
Dan

danliew wrote Aug 1, 2014 at 11:02 AM

Alpha equivalence means equivalence up to renaming, so yes, your example with the quantifiers would indeed be alpha equivalent.

The alpha equivalence check I have implemented calls the equals method, but it does not change it in any way. It just requires that it is real structural equivalence. To check for alpha equivalence, you call a different function than equals.
Thanks for the clarification. Are you intending make the code that checks for alpha equivalence part of Boogie. I suspect others may find it useful?
I don't know how to settle this. I would have equivalence including the triggers and attributes, but I can see that you don't. It would be nice if you could parameterise the equals function. We could add such an attribute.
How about this? We add a public static bool StructuralEqualityIncludesTriggersAndAttributes to BinderExpr
that defaults to false (implementing the old behaviour by default) and then add the code to Equals() and GetHashCode() in BinderExpr to use the Triggers and Attributes if StructuralEqualityIncludesTriggersAndAttributes is set to true.

Because the bool is public you can modify it to change the behaviour of Equals() and GetHashCode() if you need to.

This of course is not thread safe (consider the case where Equals() is being computed in one thread and another thread changes the value of StructuralEqualityIncludesTriggersAndAttributes). I don't think this is a very likely scenario though. If it does become and issue we can always add locks so it is not possible to change StructuralEqualityIncludesTriggersAndAttributes whilst Equals() or GetHashCode() is being computed.

danrosen wrote Aug 1, 2014 at 6:16 PM

Dan,

I followed your suggestion and added a static boolean to the BinderExpr to be able to choose whether to consider triggers and attributes when checking equivalence. It is off by default.

The patch is pushed, let me know if you have any problems with it.

Thanks! /Dan