From a32ac3bff9a24b812d133883fb9f8df5341b7bb9 Mon Sep 17 00:00:00 2001 From: Dan Rosén Date: Fri, 1 Aug 2014 09:57:25 -0700 Subject: Add alpha equivalence check for Expr, and use it when lambda lifting --- Source/Core/AbsyExpr.cs | 16 +++- Source/Core/AbsyQuant.cs | 75 ++++++++++++++++--- Source/Core/AlphaEquality.cs | 162 ++++++++++++++++++++++++++++++++++++++++ Source/Core/Core.csproj | 1 + Source/Core/LambdaHelper.cs | 85 +++++++++++++-------- Source/Core/Util.cs | 12 +++ Test/test2/LambdaExt.bpl | 146 ++++++++++++++++++++++++++++++++++++ Test/test2/LambdaExt.bpl.expect | 56 ++++++++++++++ 8 files changed, 510 insertions(+), 43 deletions(-) create mode 100644 Source/Core/AlphaEquality.cs create mode 100644 Test/test2/LambdaExt.bpl create mode 100644 Test/test2/LambdaExt.bpl.expect diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index bc603ea5..7e71453b 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1893,7 +1893,19 @@ namespace Microsoft.Boogie { this.Type = type; } - public string/*!*/ FunctionName { + public override bool Equals(object obj) { + TypeCoercion other = obj as TypeCoercion; + if (other == null) { + return false; + } else { + return object.Equals(Type, other.Type); + } + } + + + + public + string/*!*/ FunctionName { get { Contract.Ensures(Contract.Result() != null); @@ -2110,7 +2122,7 @@ namespace Microsoft.Boogie { return false; NAryExpr other = (NAryExpr)obj; - return object.Equals(this.Fun, other.Fun) && object.Equals(this.Args, other.Args); + return this.Args.ListEquals(other.Args) && object.Equals(this.Fun, other.Fun); } [Pure] public override int GetHashCode() { diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index c9e8f210..9425f698 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -57,7 +57,6 @@ namespace Microsoft.Boogie { Contract.Invariant(Body != null); } - public BinderExpr(IToken/*!*/ tok, List/*!*/ typeParameters, List/*!*/ dummies, QKeyValue kv, Expr/*!*/ body) : base(tok) @@ -77,26 +76,45 @@ namespace Microsoft.Boogie { get; } + protected static bool CompareAttributesAndTriggers = false; + + public static bool EqualWithAttributesAndTriggers(object a, object b) { + CompareAttributesAndTriggers = true; + var res = object.Equals(a, b); + Contract.Assert(CompareAttributesAndTriggers); + CompareAttributesAndTriggers = false; + return res; + } + [Pure] [Reads(ReadsAttribute.Reads.Nothing)] public override bool Equals(object obj) { - if (obj == null) + return BinderEquals(obj); + } + + public bool BinderEquals(object obj) { + if (obj == null) { return false; + } if (!(obj is BinderExpr) || - this.Kind != ((BinderExpr)obj).Kind) + this.Kind != ((BinderExpr) obj).Kind) { return false; + } - BinderExpr other = (BinderExpr)obj; - // Note, we consider quantifiers equal modulo the Triggers. - return object.Equals(this.TypeParameters, other.TypeParameters) - && object.Equals(this.Dummies, other.Dummies) - && object.Equals(this.Body, other.Body); + var other = (BinderExpr) obj; + + var a = this.TypeParameters.ListEquals(other.TypeParameters); + var b = this.Dummies.ListEquals(other.Dummies); + var c = !CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes); + var d = object.Equals(this.Body, other.Body); + + return a && b && c && d; } [Pure] public override int GetHashCode() { int h = this.Dummies.GetHashCode(); - // Note, we consider quantifiers equal modulo the Triggers. + // Note, we don't hash triggers and attributes h ^= this.Body.GetHashCode(); h = h * 5 + this.TypeParameters.GetHashCode(); h *= ((int)Kind + 1); @@ -335,6 +353,22 @@ namespace Microsoft.Boogie { public override Absy StdDispatch(StandardVisitor visitor) { return visitor.VisitQKeyValue(this); } + + public override bool Equals(object obj) { + var other = obj as QKeyValue; + if (other == null) { + return false; + } else { + return Key == other.Key && object.Equals(Params, other.Params) && + (Next == null + ? other.Next == null + : object.Equals(Next, other.Next)); + } + } + + public override int GetHashCode() { + throw new NotImplementedException(); + } } public class Trigger : Absy { @@ -432,6 +466,20 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return visitor.VisitTrigger(this); } + + public override bool Equals(object obj) { + var other = obj as Trigger; + if (other == null) { + return false; + } else { + return this.Tr.ListEquals(other.Tr) && + (Next == null ? other.Next == null : object.Equals(Next, other.Next)); + } + } + + public override int GetHashCode() { + throw new NotImplementedException(); + } } public class ForallExpr : QuantifierExpr { @@ -720,6 +768,15 @@ namespace Microsoft.Boogie { } } + public override bool Equals(object obj) { + var other = obj as QuantifierExpr; + if (other == null) { + return false; + } else { + return this.BinderEquals(obj) && + (!CompareAttributesAndTriggers || object.Equals(Triggers, other.Triggers)); + } + } } diff --git a/Source/Core/AlphaEquality.cs b/Source/Core/AlphaEquality.cs new file mode 100644 index 00000000..1d4a1d95 --- /dev/null +++ b/Source/Core/AlphaEquality.cs @@ -0,0 +1,162 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- + +using System.ComponentModel; + +namespace Microsoft.Boogie +{ + + using System; + using System.IO; + using System.Collections; + using System.Collections.Generic; + using System.Diagnostics; + using System.Diagnostics.Contracts; + + public class AlphaEquality : IEqualityComparer + { + private readonly DeBruijnRenamer deBruijn = new DeBruijnRenamer(); + + bool IEqualityComparer.Equals(Expr x, Expr y) { + var nx = deBruijn.Rename(x); + var ny = deBruijn.Rename(y); + return BinderExpr.EqualWithAttributesAndTriggers(nx, ny); + } + + int IEqualityComparer.GetHashCode(Expr obj) { + return 0; + // Best we can do because GetHashCode for Expression don't respect its equality. + // When it does, we can instead use: + // return deBruijn.Rename(obj).GetHashCode(); + } + + // Renames expressions into deBruijn indicies, such as + // (lambda x : int :: x + a) + // into + // (lambda bv#0 : int :: bv#0 + fv#0) + // It does not handle type variables yet, but it could be added. + // + // This class could be made public, but it is not since the Rename method + // could then leak FreeVariables out of here. + private class DeBruijnRenamer : Duplicator + { + + // Maps from index positions and types to new variables + private readonly TypeDict boundVars = + new TypeDict("bv", ti => new BoundVariable(Token.NoToken, ti)); + + private readonly TypeDict freeVars = + new TypeDict("fv", ti => new FreeVariable(ti)); + + // These three variables are reset at the beginning of every renaming + private int boundVarCount, freeVarCount; + private Dictionary freeVarMap; + + // Cached, previous results + private readonly Dictionary cache = new Dictionary(); + + public Expr Rename(Expr e) { + Expr ne; + if (!cache.TryGetValue(e, out ne)) { + boundVarCount = 0; + freeVarCount = 0; + freeVarMap = new Dictionary(); + + ne = VisitExpr(e); + cache[e] = ne; +#if DEBUG_ALPHA_RENAMING + var wr = new TokenTextWriter("", Console.Out, true); + Console.Write("nm( "); + e.Emit(wr); + Console.WriteLine(" )"); + Console.Write(" = "); + ne.Emit(wr); + Console.WriteLine(""); + Console.WriteLine("h = " + ne.GetHashCode()); +#endif + } + return ne; + } + + public override BinderExpr VisitBinderExpr(BinderExpr node) { + var subst = new Dictionary(); + var newBound = new List(); + foreach (var bv in node.Dummies) { + var bvNew = boundVars[boundVarCount++, bv.TypedIdent.Type]; + newBound.Add(bvNew); + subst[bv] = new IdentifierExpr(Token.NoToken, bvNew); + } + node.Dummies = this.VisitVariableSeq(newBound); + node.Body = this.VisitExpr(Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), node.Body)); + return node; + } + + public override Variable VisitVariable(Variable node) { + FreeVariable fv; + var bv = node as BoundVariable; + if (boundVars.ContainsValue(bv)) { + return node; + } else if (freeVarMap.TryGetValue(node, out fv)) { + return fv; + } else { + return freeVarMap[node] = freeVars[freeVarCount++, node.TypedIdent.Type]; + } + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) { + var ie = (IdentifierExpr) base.VisitIdentifierExpr(node); + // Need to fix up the name, since IdentifierExpr's equality also checks the name + ie.Name = ie.Decl.TypedIdent.Name; + return ie; + } + + private class TypeDict + { + private readonly Dictionary, A> vars = new Dictionary, A>(); + + private readonly string Prefix; // either "bv" or "fv" + private readonly Func Mk; // either new BoundVar or new FreeVar + + public TypeDict(string prefix, Func mk) { + Prefix = prefix; + Mk = mk; + } + + // For debugging purposes, we create unique names when types differ, but the index are the same. + private int created = 0; + + // Make sure that this index and this type is always mapped to the same variable + public A this[int i, Type t] { + get { + A v; + if (!vars.TryGetValue(Tuple.Create(i, t), out v)) { + v = Mk(new TypedIdent(Token.NoToken, Prefix + i + "#" + created++, t)); + vars[Tuple.Create(i, t)] = v; + } + return v; + } + } + + public bool ContainsValue(A a) { + return vars.ContainsValue(a); + } + } + + private class FreeVariable : Variable + { + public FreeVariable(TypedIdent ti) : base(Token.NoToken, ti) {} + + public override bool IsMutable { + get { throw new cce.UnreachableException(); } + } + + public override void Register(ResolutionContext rc) { + throw new cce.UnreachableException(); + } + } + } + } +} diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 881daa7f..27f4eea7 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -164,6 +164,7 @@ + diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index c884be3c..45c68fdd 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -52,6 +52,9 @@ namespace Microsoft.Boogie { } private class LambdaVisitor : StandardVisitor { + private readonly Dictionary liftedLambdas = + new Dictionary(new AlphaEquality()); + internal List/*!*/ lambdaAxioms = new List(); internal List/*!*/ lambdaFunctions = new List(); [ContractInvariantMethod] @@ -148,43 +151,61 @@ namespace Microsoft.Boogie { } } + var sw = new System.IO.StringWriter(); + var wr = new TokenTextWriter(sw, true); + lambda.Emit(wr); + string lam_str = sw.ToString(); + + FunctionCall fcall; IToken tok = lambda.tok; Formal res = new Formal(tok, new TypedIdent(tok, TypedIdent.NoName, cce.NonNull(lambda.Type)), false); - Function fn = new Function(tok, "lambda@" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function", - Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs)); - lambdaFunctions.Add(fn); - FunctionCall fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name)); - fcall.Func = fn; // resolve here + if (liftedLambdas.TryGetValue(lambda, out fcall)) { + if (CommandLineOptions.Clo.TraceVerify) { + Console.WriteLine("Old lambda: {0}", lam_str); + } + } else { + if (CommandLineOptions.Clo.TraceVerify) { + Console.WriteLine("New lambda: {0}", lam_str); + } + Function fn = new Function(tok, "lambda#" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function", + Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs)); + + fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name)); + fcall.Func = fn; // resolve here + liftedLambdas[lambda] = fcall; - List selectArgs = new List(); - foreach (Variable/*!*/ v in lambda.Dummies) { - Contract.Assert(v != null); - selectArgs.Add(new IdentifierExpr(v.tok, v)); - } - NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs); - axcall.Type = res.TypedIdent.Type; - axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals); - NAryExpr select = Expr.Select(axcall, selectArgs); - select.Type = lambdaBody.Type; - List selectTypeParamActuals = new List(); - List forallTypeVariables = new List(); - foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) { - Contract.Assert(tp != null); - selectTypeParamActuals.Add(tp); - forallTypeVariables.Add(tp); + List selectArgs = new List(); + foreach (Variable/*!*/ v in lambda.Dummies) { + Contract.Assert(v != null); + selectArgs.Add(new IdentifierExpr(v.tok, v)); + } + NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs); + axcall.Type = res.TypedIdent.Type; + axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals); + NAryExpr select = Expr.Select(axcall, selectArgs); + select.Type = lambdaBody.Type; + List selectTypeParamActuals = new List(); + List forallTypeVariables = new List(); + foreach (TypeVariable/*!*/ tp in lambda.TypeParameters) { + Contract.Assert(tp != null); + selectTypeParamActuals.Add(tp); + forallTypeVariables.Add(tp); + } + forallTypeVariables.AddRange(freeTypeVars); + select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals); + + Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaBody); + NAryExpr body = Expr.Eq(select, bb); + body.Type = Type.Bool; + body.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + Trigger trig = new Trigger(select.tok, true, new List { select }); + + lambdaFunctions.Add(fn); + lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies, + Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaAttrs), + trig, body)); } - forallTypeVariables.AddRange(freeTypeVars); - select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals); - - Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaBody); - NAryExpr body = Expr.Eq(select, bb); - body.Type = Type.Bool; - body.TypeParameters = SimpleTypeParamInstantiation.EMPTY; - Trigger trig = new Trigger(select.tok, true, new List { select }); - lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies, - Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambdaAttrs), - trig, body)); NAryExpr call = new NAryExpr(tok, fcall, callArgs); call.Type = res.TypedIdent.Type; diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 75cb25aa..1b8353e1 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -66,6 +66,18 @@ namespace Microsoft.Boogie { { return source1.Zip(source2, (e1, e2) => new Tuple(e1, e2)); } + + public static bool ListEquals(this List xs, List ys) { + var equal = xs.Count == ys.Count; + for (int i = 0; equal && i < xs.Count; i++) { + equal = object.Equals(xs[i], ys[i]); + } + return equal; + } + + public static int ListHash(this List xs) { + return xs.Aggregate(xs.Count, (current, x) => current ^ xs.GetHashCode()); + } } public class TokenTextWriter : IDisposable { diff --git a/Test/test2/LambdaExt.bpl b/Test/test2/LambdaExt.bpl new file mode 100644 index 00000000..be0d84ee --- /dev/null +++ b/Test/test2/LambdaExt.bpl @@ -0,0 +1,146 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure Simplest() { + var id1, id2 : [int]int; + id1 := (lambda x: int :: x); + id2 := (lambda x: int :: x); + assert id1 == id2; + id2 := (lambda x: int :: 0); + assert id1 == id2; // fail +} + +procedure Const() { + var v, w : [int][int]int; + var f, g : [int, int]int; + + v := (lambda x : int :: (lambda y : int :: x)); + + w := (lambda x : int :: (lambda i : int :: x)); + assert v == w; + + w := (lambda i : int :: (lambda y : int :: i)); + assert v == w; + + w := (lambda a : int :: (lambda b : int :: b)); + assert v == w; // should fail, now two different functions + + f := (lambda x : int, y : int :: x); + assert f == (lambda p : int, q : int :: p); + assert f == (lambda p : int, q : int :: q); // should fail, different functions +} + +procedure PolyConst() { + assert (lambda x: A :: x) == (lambdax: A :: x); // fails because of type parameters. this could be fixed. + /* // more tests, when it is fixed + var k1 : [A1][B1]A1; + var k2 : [A2][B2]A2; + k1 := (lambda x: A :: (lambda y: B :: x)); + k2 := (lambda x: A :: (lambda z: C :: x)); + assert k1 == k2; + k2 := (lambda u: X :: (lambda v: Y :: u)); + assert k1 == k2; */ +} + +procedure FreeVarP() { + var k : real; + var m : [int]real; + m := (lambda x:int :: k); + assert m[0] == k; +} + +procedure FreeVarQ() { + var k : int; + var m : [int]int; + m := (lambda x:int :: k); // should be a different lambda from in FreeVarP, because they have different types + assert m[0] == k; +} + +procedure Quantifiers() { + var k1 : [int]bool; + var k2 : [int]bool; + k1 := (lambda x: int :: (exists y: int :: x > y)); + k2 := (lambda x: int :: (exists y: int :: x > y)); + assert k1 == k2; + k2 := (lambda x: int :: (exists z: int :: x > z)); + assert k1 == k2; +} + +procedure FreeVariables() { + var m : [bool,bool,bool]bool; + var k : [bool,bool]bool; + + var f : [bool]bool; + var g : [bool]bool; + + var a : bool; + var b : bool; + + f := (lambda r: bool :: a); + g := (lambda s: bool :: b); + if (a == b) { + assert f == g; // should be OK + } else { + assert f == g; // should fail + } + + f := (lambda r: bool :: k[a,b]); + g := (lambda s: bool :: k[b,a]); + if (a == b) { + assert f == g; // should be OK + } else { + assert f == g; // should fail + } + + f := (lambda r: bool :: m[a,a,b]); + g := (lambda s: bool :: m[a,b,b]); + if (a == b) { + assert f == g; // should fail because they are different lambda + } else { + assert f == g; // should fail because they are different lambda + } +} + +function f(int) : int; + +procedure Triggers() { + var a,b : [int]bool; + a := (lambda x:int :: (forall u:int :: { f(u) } x == f(u))); + b := (lambda y:int :: (forall v:int :: { f(v) } y == f(v))); + assert a == b; + b := (lambda y:int :: (forall v:int :: y == f(v))); + assert a == b; // should fail because triggers are different +} + +procedure Attributes() { + var a,b : [int]bool; + a := (lambda x:int :: (forall u:int :: {:attrib f(u) } x == f(u))); + b := (lambda y:int :: (forall v:int :: {:attrib f(v) } y == f(v))); + assert a == b; + b := (lambda y:int :: (forall v:int :: {:battrib f(v) } y == f(v))); + assert a == b; // should fail since attributes are different + a := (lambda x:int :: (forall u:int :: {:battrib f(x) } x == f(u))); + assert a == b; // should fail since attributes are different +} + +procedure Old() { + var u,v : [int]int; + var a,b : int; + u := (lambda x:int :: old(x+a)); + v := (lambda y:int :: old(y+b)); + if (a == b) { + assert u == v; // ok + } else { + assert u == v; // fails + } +} + +type Box; +function $Box(T) : Box; +function $Unbox(Box) : T; + +procedure Coercion() { + assert (lambda x: Box :: $Box($Unbox(x): int)) + == (lambda y: Box :: $Box($Unbox(y): int)); +} + diff --git a/Test/test2/LambdaExt.bpl.expect b/Test/test2/LambdaExt.bpl.expect new file mode 100644 index 00000000..fac42eb2 --- /dev/null +++ b/Test/test2/LambdaExt.bpl.expect @@ -0,0 +1,56 @@ +LambdaExt.bpl(10,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(6,7): anon0 +LambdaExt.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(17,5): anon0 +LambdaExt.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(17,5): anon0 +LambdaExt.bpl(34,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(34,3): anon0 +LambdaExt.bpl(84,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(84,5): anon9_Else +LambdaExt.bpl(92,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(84,5): anon9_Else + LambdaExt.bpl(87,5): anon3 + LambdaExt.bpl(92,5): anon10_Else +LambdaExt.bpl(98,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(82,5): anon9_Then + LambdaExt.bpl(87,5): anon3 + LambdaExt.bpl(90,5): anon10_Then + LambdaExt.bpl(95,5): anon6 + LambdaExt.bpl(98,5): anon11_Then +LambdaExt.bpl(100,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(79,5): anon0 + LambdaExt.bpl(84,5): anon9_Else + LambdaExt.bpl(87,5): anon3 + LambdaExt.bpl(92,5): anon10_Else + LambdaExt.bpl(95,5): anon6 + LambdaExt.bpl(100,5): anon11_Else +LambdaExt.bpl(112,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(108,5): anon0 +LambdaExt.bpl(119,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(117,5): anon0 +LambdaExt.bpl(121,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(117,5): anon0 +LambdaExt.bpl(123,3): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(117,5): anon0 +LambdaExt.bpl(134,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaExt.bpl(129,5): anon0 + LambdaExt.bpl(134,5): anon3_Else + +Boogie program verifier finished with 4 verified, 13 errors -- cgit v1.2.3