Add alpha equivalence check for Expr, and use it when lambda lifting

2 files changed, 202 insertions, 0 deletions

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<A> x: A :: x) == (lambda<A>x: A :: x); // fails because of type parameters. this could be fixed.
+  /* // more tests, when it is fixed
+  var k1 : <A1>[A1]<B1>[B1]A1;
+  var k2 : <A2>[A2]<B2>[B2]A2;
+  k1 := (lambda<A> x: A :: (lambda<B> y: B :: x));
+  k2 := (lambda<A> x: A :: (lambda<C> z: C :: x));
+  assert k1 == k2;
+  k2 := (lambda<X> u: X :: (lambda<Y> 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>(T) : Box;
+function $Unbox<T>(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