From cbabeb3fdef4f1ad2aed7f32ba375ad4fdd6c298 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 28 Jul 2014 16:32:51 +0100 Subject: Fix bug in NAryExpr where Equals() override was not correctly implemented. The previous implementation which called object.Equals(this.Args, other.Args) would in turn call ``this.Args.Equals(others.Args)`` which for List<> is reference equality. Equals() is purposely overloaded on Expr classes in Boogie to provide structural equality so this has been fixed so a comparision of elements in the list is performed. --- Source/Core/AbsyExpr.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/Core/AbsyExpr.cs') diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index bc603ea5..0a7bfa33 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2110,7 +2110,7 @@ namespace Microsoft.Boogie { return false; NAryExpr other = (NAryExpr)obj; - return object.Equals(this.Fun, other.Fun) && object.Equals(this.Args, other.Args); + return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args); } [Pure] public override int GetHashCode() { -- cgit v1.2.3 From a1f80cb9e477aba98aef11add502dbeef0670c35 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 29 Jul 2014 14:41:48 +0100 Subject: Fix bug in NAryExpr where is was possible for A.Equals(B) to return true but A.GetHashCode() == B.GetHashCode() return false. The case of the bug was that Args.GetHashCode() was being used which uses Object.GetHashCode() which uses references to compute GetHashCode(). This is wrong because we want hash codes to equal for structural equality. To fix this I've implemented a really simple hashing method. I have not tested how resilient this is to collisions. --- Source/Core/AbsyExpr.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'Source/Core/AbsyExpr.cs') diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 0a7bfa33..8d372b0c 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2115,7 +2115,11 @@ namespace Microsoft.Boogie { [Pure] public override int GetHashCode() { int h = this.Fun.GetHashCode(); - h ^= this.Args.GetHashCode(); + // DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references + // We want structural equality + foreach (var arg in Args) { + h = (97*h) + arg.GetHashCode(); + } return h; } public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { -- cgit v1.2.3