diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 28d67a075..d3cdf4e6b 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -575,7 +575,6 @@ public override bool Equals(object obj) { } } - // todo (MR) this was implemented to throw an error; is this bad? public override int GetHashCode() { int hash = 17; hash = hash * 23 + tr.GetHashCode(); diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index cda1870e3..5e976c5ee 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1919,9 +1919,8 @@ identifies variables /freeVarLambdaLifting : Boogie's lambda lifting transforms the bodies of lambda expressions into templates with holes. By default, holes are maximally large subexpressions that do not contain - bound variables (see Section 8 of Boogie 3 paper). - This option performs a form of lambda lifting - in which holes are the lambda's free variables. + bound variables. This option performs a form of lambda + lifting in which holes are the lambda's free variables. /overlookTypeErrors : skip any implementation with resolution or type checking errors diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 1fb7346ed..27c5c6215 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -84,7 +84,6 @@ public static void ExpandLambdas(Program prog) { } private class LambdaVisitor : StandardVisitor { - // todo (MR) why are we not using this map as a cache for lifted lambdas? why are we recomputing them? private readonly Dictionary liftedLambdas = new Dictionary(new AlphaEquality()); @@ -118,7 +117,7 @@ public override Expr VisitLambdaExpr(LambdaExpr lambda) { /// free variables with bound ones. /// /// A lambda expression - /// (lambda x1: T1 ... x_n: T_n => t) + /// (lambda x1: T1 ... x_n: T_n :: t) /// where t contains the free variables y1, ..., y_m. /// /// @@ -284,7 +283,7 @@ private Expr LiftLambdaFreeVars(LambdaExpr lambda) { /// maximally large subexpressions of a lambda that do not contain any of the lambda's bound variables. /// /// A lambda expression - /// (lambda x1: T1 ... x_n: T_n => t) + /// (lambda x1: T1 ... x_n: T_n :: t) /// where t contains the subexpressions e1, ..., e_m. These are maximally large /// subexpressions that do not contain the lambda's bound variables. /// @@ -301,8 +300,6 @@ private Expr LiftLambdaFreeVars(LambdaExpr lambda) { /// /// /// - // todo (MR) move old handling into MaxHolesLambdaLifter? Maybe try merging MaxHolesLambdaLifter with LambdaVisitor - // todo (MR) do I need to handle a more general temporal modifier (e.g. labels)? private Expr LiftLambdaMaxHoles(LambdaExpr lambda) { // We start by getting rid of `old` expressions. Instead, we replace the free variables `x_i` that are diff --git a/Source/Core/LambdaLiftingMaxHolesFiller.cs b/Source/Core/LambdaLiftingMaxHolesFiller.cs index 492daf416..360af993f 100644 --- a/Source/Core/LambdaLiftingMaxHolesFiller.cs +++ b/Source/Core/LambdaLiftingMaxHolesFiller.cs @@ -7,7 +7,7 @@ namespace Core { /// Traverses an expression, replacing all holes with bound variables taken from the /// queue. /// -class LambdaLiftingMaxHolesFiller : Duplicator { +class LambdaLiftingMaxHolesFiller : StandardVisitor { private readonly List _holes; private readonly Queue _replDummies; diff --git a/Source/Core/LambdaLiftingTemplate.cs b/Source/Core/LambdaLiftingTemplate.cs index c8371c179..97330520f 100644 --- a/Source/Core/LambdaLiftingTemplate.cs +++ b/Source/Core/LambdaLiftingTemplate.cs @@ -47,7 +47,7 @@ protected LambdaLiftingTemplate(List llReplacements) { } public List GetReplacements() { - return llReplacements; // todo (MR) make this readonly somewhere? + return llReplacements; } public abstract bool ContainsBoundVariables(); diff --git a/Source/Core/MaxHolesLambdaLifter.cs b/Source/Core/MaxHolesLambdaLifter.cs index 5224beb5f..1b6602b23 100644 --- a/Source/Core/MaxHolesLambdaLifter.cs +++ b/Source/Core/MaxHolesLambdaLifter.cs @@ -9,16 +9,6 @@ namespace Core { using Set = GSet; -// todo (MR) It would be better if this class were a private class within LambdaHelper because -// this class relies on the lambda not having old expressions any more (only old free variables). -// But this makes LambdaHelper very long so I'm leaving this class in a separate file for now. - -// todo (MR) test nested lambdas, triggers that need replacements, assert, assume, multiple triggers, -// todo (MR) multiple expressions in triggers, multiple bound vars, more complicated repl expressions, -// todo (MR) type parameters, global variables - -// todo (MR) do I need to handle AsgnLhs? MapAsgnLhs? Assert/Assume? - /// /// This visitor performs the first phase of the MaxHoles lambda lifting (see ), /// after which it invokes the second phase in the method. @@ -93,7 +83,6 @@ public override Expr VisitNAryExpr(NAryExpr node) { _templates[node] = new TemplateWithBoundVariables(replacements); } else { - // todo (MR) Could we avoid the casting? Could we encode in type system that all children of hole nodes are holes? var newArgs = from arg in nodeArgs select ((TemplateNoBoundVariables) _templates[arg]).GetReplacement(); var llReplacementExpr = new NAryExpr(node.tok, node.Fun, newArgs.ToList(), node.Immutable) { @@ -146,11 +135,10 @@ public override Expr VisitLetExpr(LetExpr node) { var newRhss = from arg in varBodies select ((TemplateNoBoundVariables) _templates[arg]).GetReplacement(); LambdaLiftingTemplate template = new TemplateNoBoundVariables( new LetExpr(node.tok, node.Dummies, newRhss.ToList(), - node.Attributes, // todo (MR) document says attributes should be dropped? + node.Attributes, ((TemplateNoBoundVariables) _templates[node.Body]) - .GetReplacement())); + .GetReplacement()) {Type = node.Type}); _templates[node] = template; - // todo (MR) explicitly set type of let expr here? } return node; @@ -169,9 +157,8 @@ public override Expr VisitForallExpr(ForallExpr node) { var newBody = bt.GetReplacement(); var newTrigger = ReplacementTrigger(trigger); _templates[node] = new TemplateNoBoundVariables( - new ForallExpr(node.tok, node.TypeParameters, node.Dummies, node.Attributes, newTrigger, newBody, - node.Immutable)); - // todo (MR) explicitly set type of binder expr here? + new ForallExpr(node.tok, node.TypeParameters, node.Dummies, node.Attributes, newTrigger, + newBody, node.Immutable) {Type = node.Type}); } else { var replacements = bodyTemplate.GetReplacements(); if (trigger != null) { @@ -198,8 +185,7 @@ public override Expr VisitExistsExpr(ExistsExpr node) { var newTrigger = ReplacementTrigger(trigger); _templates[node] = new TemplateNoBoundVariables( new ExistsExpr(node.tok, node.TypeParameters, node.Dummies, node.Attributes, newTrigger, newBody, - node.Immutable)); - // todo (MR) explicitly set type of binder expr here? + node.Immutable) {Type = node.Type}); } else { var replacements = bodyTemplate.GetReplacements(); if (trigger != null) { @@ -259,10 +245,7 @@ public override Expr VisitLambdaExpr(LambdaExpr node) { VisitQKeyValue(node.Attributes); } - // Phase II of the lambda lifting. - // todo (MR) this code should not be in a visitlambdaexpr but in a separate function I think so that we don't confuse Phase I and Phase II. - - // todo (MR) more efficient to do in loop but I find this more clear + // Phase II of the lambda lifting. var attribReplacementExprs = node.Attributes == null ? new List() : QKeyValueReplacements(node.Attributes); var llReplacementExprs = _templates[node.Body].GetReplacements(); @@ -270,7 +253,7 @@ public override Expr VisitLambdaExpr(LambdaExpr node) { allReplacementExprs.AddRange(llReplacementExprs); var typedIdents = (from replExpr in allReplacementExprs select new TypedIdent(replExpr.tok, FreshVarNameGen(new List()), - replExpr.Type ?? replExpr.ShallowType)) // todo (MR) what's the difference between Type and ShallowType? + replExpr.Type ?? replExpr.ShallowType)) .ToList(); var formals = allReplacementExprs.Zip(typedIdents, (replExpr, typedIdent) => (Variable) new Formal(replExpr.tok, typedIdent, true)); @@ -359,9 +342,6 @@ public override Expr VisitLambdaExpr(LambdaExpr node) { return call; } - // todo (MR) will this take care of all types of variables? - // todo (MR) will this take care of constants? - // todo (MR) do I need to do something special for global variables? public override Variable VisitVariable(Variable node) { Contract.Requires(node != null); if (_templates.ContainsKey(node)) return node; diff --git a/Test/test2/LambdaLifting.bpl b/Test/test2/LambdaLifting.bpl new file mode 100644 index 000000000..6b1100d8d --- /dev/null +++ b/Test/test2/LambdaLifting.bpl @@ -0,0 +1,52 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure ReducingLambdaBodies() { + var a, b: int; + var f, g: [int]int; + + f := (lambda x: int :: a + b); + g := (lambda x: int :: b + a); + assert f == g; // should pass + + f := (lambda x: int :: x + a); + g := (lambda x: int :: a + x); + assert f == g; // should fail +} + +procedure ReducingLambdaBodies2() { + var a, b: int; + var f, g: [int]int; + var f2, g2: [int,int]int; + + f := (lambda x: int :: x + a); + g := (lambda x: int :: a + x); + assert f != g; // should fail +} + +procedure ReducingLambdaBodies3() { + var a, b: int; + var f, g: [int,int]int; + f := (lambda x, y: int :: x + y); + g := (lambda x, y: int :: y + x); + assert f == g; // should fail +} + +procedure MultibleBoundVars() { + var a, b: int; + var f, g: [int,int,bool]bool; + f := (lambda x: int, y: int, z: bool :: if y == (a - b) then x + (a + b * a) > b else z == (a > b)); + g := (lambda x: int, y: int, z: bool :: if y == (b + a - 2*b) then x + (a * b + a) > b else z == (b < a)); + assert f == g; // should pass +} + +function g(int,int) : int; + +procedure Triggers'(w: int, w': int) { + var a,b : [int]bool; + a := (lambda x:int :: (forall u:int :: { g(u,w) } x == g(u,w))); + b := (lambda y:int :: (forall v:int :: { g(v,w') } y == g(v,w'))); + assert w == w' ==> a == b; + b := (lambda y:int :: (forall v:int :: y == g(v,w'))); + assert w == w' ==> a == b; // should fail because triggers are different +} diff --git a/Test/test2/LambdaLifting.bpl.expect b/Test/test2/LambdaLifting.bpl.expect new file mode 100644 index 000000000..e751dc649 --- /dev/null +++ b/Test/test2/LambdaLifting.bpl.expect @@ -0,0 +1,14 @@ +LambdaLifting.bpl(14,2): Error BP5001: This assertion might not hold. +Execution trace: + LambdaLifting.bpl(8,4): anon0 +LambdaLifting.bpl(24,2): Error BP5001: This assertion might not hold. +Execution trace: + LambdaLifting.bpl(22,4): anon0 +LambdaLifting.bpl(32,2): Error BP5001: This assertion might not hold. +Execution trace: + LambdaLifting.bpl(30,4): anon0 +LambdaLifting.bpl(51,2): Error BP5001: This assertion might not hold. +Execution trace: + LambdaLifting.bpl(47,4): anon0 + +Boogie program verifier finished with 1 verified, 4 errors \ No newline at end of file