Fix lambda-lifting issues

* Include triggers when computing free variables for quantifier expressions. * Don't create holes for local let-bound variables. * Fix order in which max-holes replaces holes in triggers. * Run test2/LambdaExt.bpl twice, once for the max-hole (default) lambda lifting and once for the free-variables lambda lifting. * Add newline to end of file in test2/LambdaLifting.bpl.expect.
alexanderjsummers · Jul 25, 2019 · d35bdcd · d35bdcd
1 parent 080fdfd
commit d35bdcd
Show file tree

Hide file tree

Showing 6 changed files with 134 additions and 36 deletions.
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
@@ -228,10 +228,10 @@ public override void Resolve(ResolutionContext rc) {
 
     public override void ComputeFreeVariables(Set freeVars) {
       //Contract.Requires(freeVars != null);
-      ComputeBinderFreeVariables(TypeParameters, Dummies, Body, Attributes, freeVars);
+      ComputeBinderFreeVariables(TypeParameters, Dummies, Body, null, Attributes, freeVars);
     }
 
-    public static void ComputeBinderFreeVariables(List<TypeVariable> typeParameters, List<Variable> dummies, Expr body, QKeyValue attributes, Set freeVars) {
+    public static void ComputeBinderFreeVariables(List<TypeVariable> typeParameters, List<Variable> dummies, Expr body, Trigger triggers, QKeyValue attributes, Set freeVars) {
       Contract.Requires(dummies != null);
       Contract.Requires(body != null);
 
@@ -240,6 +240,11 @@ public static void ComputeBinderFreeVariables(List<TypeVariable> typeParameters,
         Contract.Assert(!freeVars[v]);
       }
       body.ComputeFreeVariables(freeVars);
+      for (var trig = triggers; trig != null; trig = trig.Next) {
+        foreach (var e in trig.Tr) {
+          e.ComputeFreeVariables(freeVars);
+        }
+      }
       for (var a = attributes; a != null; a = a.Next) {
         foreach (var o in a.Params) {
           var e = o as Expr;
@@ -821,6 +826,10 @@ public override void Resolve(ResolutionContext rc) {
       }
     }
 
+    public override void ComputeFreeVariables(Set freeVars) {
+      //Contract.Requires(freeVars != null);
+      ComputeBinderFreeVariables(TypeParameters, Dummies, Body, Triggers, Attributes, freeVars);
+    }
 
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
@@ -186,7 +186,7 @@ private Expr LiftLambdaFreeVars(LambdaExpr lambda) {
 
         // compute the free variables of the lambda expression, but with lambdaBody instead of lambda.Body
         Set freeVars = new Set();
-        BinderExpr.ComputeBinderFreeVariables(lambda.TypeParameters, lambda.Dummies, lambdaBody, lambdaAttrs, freeVars);
+        BinderExpr.ComputeBinderFreeVariables(lambda.TypeParameters, lambda.Dummies, lambdaBody, null, lambdaAttrs, freeVars);
 
         foreach (object o in freeVars) {
           // 'o' is either a Variable or a TypeVariable.

diff --git a/Source/Core/MaxHolesLambdaLifter.cs b/Source/Core/MaxHolesLambdaLifter.cs
@@ -119,6 +119,7 @@ public override Expr VisitLiteralExpr(LiteralExpr node) {
     public override Expr VisitLetExpr(LetExpr node) {
         Contract.Requires(node != null);
         if (_templates.ContainsKey(node)) return node;
+        _nestedBoundVariables.AddRange(node.Dummies);
         base.VisitLetExpr(node);
         var bodyTemplate = _templates[node.Body];
         var varBodies = node.Rhss;
@@ -223,11 +224,14 @@ public override Trigger VisitTrigger(Trigger node) {
         base.VisitTrigger(node);
         var templates = (from e in node.Tr select _templates[e]).ToList();
         var replacements = new List<Expr>();
+        if (node.Next != null) {
+            // the replacements for .Next must be added first, since the standard visitor visits them first
+            replacements.AddRange(_templates[node.Next].GetReplacements());
+        }
         foreach (LambdaLiftingTemplate llt in templates) {
             replacements.AddRange(llt.GetReplacements());
         }
 
-        replacements.AddRange(node.Next == null ? new List<Expr>() : _templates[node.Next].GetReplacements());
         var nextNoBounds = node.Next == null || !_templates[node.Next].ContainsBoundVariables();
         if (nextNoBounds && templates.All(r => !r.ContainsBoundVariables())) {
             _templates[node] = new TemplateNoBoundVariablesTriggerOrKv(replacements);
@@ -264,7 +268,7 @@ public override Expr VisitLambdaExpr(LambdaExpr node) {
         dummies.AddRange(replDummies);
 
         Set freeVars = new Set();
-        BinderExpr.ComputeBinderFreeVariables(_lambda.TypeParameters, _lambda.Dummies, _lambda.Body, _lambda.Attributes,
+        BinderExpr.ComputeBinderFreeVariables(_lambda.TypeParameters, _lambda.Dummies, _lambda.Body, null, _lambda.Attributes,
             freeVars);
         var freeTypeVars = freeVars.OfType<TypeVariable>().ToList();
         var freeVarActuals = freeVars.OfType<Type>().ToList();

diff --git a/Test/test2/LambdaExt.bpl b/Test/test2/LambdaExt.bpl
@@ -1,4 +1,5 @@
 // RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %boogie -noinfer -freeVarLambdaLifting "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 procedure Simplest() {
@@ -112,7 +113,7 @@ procedure FreeVariables3() {
   f := (lambda r: bool :: m[a,a,b]);
   g := (lambda s: bool :: m[a,b,b]);
   if (a == b) {
-    assert f == g; // should be OK
+    assert f == g; // should fail for /freeVarLambdaLifting; OK for max-hole lambda lifting
   } else {
     assert f == g; // should fail because they are different lambda
   }
@@ -161,3 +162,29 @@ procedure Coercion() {
       == (lambda y: Box :: $Box($Unbox(y): int));
 }
 
+
+function F(int,int): int;
+const n: [int]bool;
+procedure FreeVarOnlyInTrigger() {
+  // The following once used to crash, because trigger expressions were not
+  // visited while computing free variables.
+  assert (forall m: int ::  // error
+    n == (lambda x: int :: (exists y: int :: { F(m,y) } true)));
+}
+
+type TA;
+type TB;
+function G(TA, TB): int;
+procedure MultipleTriggers() {
+  // The following once used to crash, because max holes for triggers were
+  // replaced in the wrong order.
+  assert (forall a: TA, m: [TB]bool ::  // error
+    m == (lambda y: TB :: (exists x: TB :: { G(a, x) } { m[x] } G(a, x) == 10)));
+}
+
+procedure LetBinder() {
+  var m: [bool]bool;
+  // The following once used to crash, because let-bound variables were not
+  // considered local.
+  m := (lambda b: bool :: (var u := b; u));
+}
diff --git a/Test/test2/LambdaExt.bpl.expect b/Test/test2/LambdaExt.bpl.expect
@@ -1,42 +1,100 @@
-LambdaExt.bpl(10,3): Error BP5001: This assertion might not hold.
+LambdaExt.bpl(11,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.
+    LambdaExt.bpl(7,7): anon0
+LambdaExt.bpl(27,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.
+    LambdaExt.bpl(18,5): anon0
+LambdaExt.bpl(31,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.
+    LambdaExt.bpl(18,5): anon0
+LambdaExt.bpl(35,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(34,3): anon0
-LambdaExt.bpl(81,5): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(35,3): anon0
+LambdaExt.bpl(82,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(76,5): anon0
-    LambdaExt.bpl(81,5): anon3_Else
-LambdaExt.bpl(99,5): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(77,5): anon0
+    LambdaExt.bpl(82,5): anon3_Else
+LambdaExt.bpl(100,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(94,5): anon0
-    LambdaExt.bpl(99,5): anon3_Else
-LambdaExt.bpl(117,5): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(95,5): anon0
+    LambdaExt.bpl(100,5): anon3_Else
+LambdaExt.bpl(118,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(112,5): anon0
-    LambdaExt.bpl(117,5): anon3_Else
-LambdaExt.bpl(129,3): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(113,5): anon0
+    LambdaExt.bpl(118,5): anon3_Else
+LambdaExt.bpl(130,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(125,5): anon0
-LambdaExt.bpl(136,3): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(126,5): anon0
+LambdaExt.bpl(137,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(134,5): anon0
-LambdaExt.bpl(138,3): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(135,5): anon0
+LambdaExt.bpl(139,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(134,5): anon0
-LambdaExt.bpl(140,3): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(135,5): anon0
+LambdaExt.bpl(141,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(134,5): anon0
-LambdaExt.bpl(151,5): Error BP5001: This assertion might not hold.
+    LambdaExt.bpl(135,5): anon0
+LambdaExt.bpl(152,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    LambdaExt.bpl(146,5): anon0
-    LambdaExt.bpl(151,5): anon3_Else
+    LambdaExt.bpl(147,5): anon0
+    LambdaExt.bpl(152,5): anon3_Else
+LambdaExt.bpl(171,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(171,3): anon0
+LambdaExt.bpl(181,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(181,3): anon0
+
+Boogie program verifier finished with 5 verified, 14 errors
+LambdaExt.bpl(11,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(7,7): anon0
+LambdaExt.bpl(27,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(18,5): anon0
+LambdaExt.bpl(31,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(18,5): anon0
+LambdaExt.bpl(35,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(35,3): anon0
+LambdaExt.bpl(82,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(77,5): anon0
+    LambdaExt.bpl(82,5): anon3_Else
+LambdaExt.bpl(100,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(95,5): anon0
+    LambdaExt.bpl(100,5): anon3_Else
+LambdaExt.bpl(116,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(113,5): anon0
+    LambdaExt.bpl(116,5): anon3_Then
+LambdaExt.bpl(118,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(113,5): anon0
+    LambdaExt.bpl(118,5): anon3_Else
+LambdaExt.bpl(130,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(126,5): anon0
+LambdaExt.bpl(137,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(135,5): anon0
+LambdaExt.bpl(139,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(135,5): anon0
+LambdaExt.bpl(141,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(135,5): anon0
+LambdaExt.bpl(152,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(147,5): anon0
+    LambdaExt.bpl(152,5): anon3_Else
+LambdaExt.bpl(171,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(171,3): anon0
+LambdaExt.bpl(181,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    LambdaExt.bpl(181,3): anon0
 
-Boogie program verifier finished with 4 verified, 12 errors
+Boogie program verifier finished with 5 verified, 15 errors
diff --git a/Test/test2/LambdaLifting.bpl.expect b/Test/test2/LambdaLifting.bpl.expect
@@ -11,4 +11,4 @@ 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
+Boogie program verifier finished with 1 verified, 4 errors