Merge pull request boogie-org#141 from amaurremi/master

Pass over Rustan's PR#140 comments. Added lambda-lifting tests.

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();

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

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<Expr, FunctionCall> liftedLambdas = 
         new Dictionary<Expr, FunctionCall>(new AlphaEquality());
 
@@ -118,7 +117,7 @@ public override Expr VisitLambdaExpr(LambdaExpr lambda) {
       /// free variables with bound ones.
       /// </summary>
       /// <param name="lambda">A lambda expression
-      ///   <code>(lambda x1: T1 ... x_n: T_n => t)</code>
+      ///   <code>(lambda x1: T1 ... x_n: T_n :: t)</code>
       /// where <c>t</c> contains the free variables <c>y1</c>, ..., <c>y_m</c>.
       /// </param>
       /// <returns>
@@ -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.
       /// </summary>
       /// <param name="lambda">A lambda expression
-      ///   <code>(lambda x1: T1 ... x_n: T_n => t)</code>
+      ///   <code>(lambda x1: T1 ... x_n: T_n :: t)</code>
       /// where <c>t</c> contains the subexpressions <c>e1</c>, ..., <c>e_m</c>. These are maximally large
       /// subexpressions that do not contain the lambda's bound variables.
       /// </param>
@@ -301,8 +300,6 @@ private Expr LiftLambdaFreeVars(LambdaExpr lambda) {
       ///   </item>
       /// </list>
       /// </returns>
-      // 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

Source/Core/LambdaLiftingMaxHolesFiller.cs

@@ -7,7 +7,7 @@ namespace Core {
 /// Traverses an expression, replacing all holes with bound variables taken from the <see cref="_replDummies"/>
 /// queue.
 /// </summary>
-class LambdaLiftingMaxHolesFiller : Duplicator {
+class LambdaLiftingMaxHolesFiller : StandardVisitor {
         private readonly List<Absy> _holes;
         private readonly Queue<Variable> _replDummies;
 

Source/Core/LambdaLiftingTemplate.cs

@@ -47,7 +47,7 @@ protected LambdaLiftingTemplate(List<Expr> llReplacements) {
         }
 
         public List<Expr> GetReplacements() {
-            return llReplacements; // todo (MR) make this readonly somewhere?
+            return llReplacements;
         }
 
         public abstract bool ContainsBoundVariables();

Source/Core/MaxHolesLambdaLifter.cs

@@ -9,16 +9,6 @@
 namespace Core {
 using Set = GSet<object>;
 
-// 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?
-
 /// <summary>
 /// This visitor performs the first phase of the MaxHoles lambda lifting (see <see cref="LambdaHelper.ExpandLambdas"/>),
 /// after which it invokes the second phase in the <see cref="VisitLambdaExpr"/> 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,18 +245,15 @@ 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<Expr>() : QKeyValueReplacements(node.Attributes);
         var llReplacementExprs = _templates[node.Body].GetReplacements();
         var allReplacementExprs = new List<Expr>(attribReplacementExprs);
         allReplacementExprs.AddRange(llReplacementExprs);
         var typedIdents = (from replExpr in allReplacementExprs
                 select new TypedIdent(replExpr.tok, FreshVarNameGen(new List<string>()),
-                    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;

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
+}

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