Fix: Read clauses should be checked before lit lifting

The function IgnoreFuel in UnfoldingPerformance.dfy used to be lit-wrapped. It
shouldn't be, because its reads clause is non-empty. This is not a soundness
bug, but fixing it improves performance in cases where a function call would be
incorrectly unrolled.

Test case written by Rustan.

1 files changed, 61 insertions, 0 deletions

diff --git a/Test/dafny0/UnfoldingPerformance.dfy b/Test/dafny0/UnfoldingPerformance.dfy
new file mode 100644
index 00000000..3eed689a
--- /dev/null
+++ b/Test/dafny0/UnfoldingPerformance.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+class C {

+  var x: nat

+  function method IgnoreFuel(): nat

+    reads this

+  {

+    x

+  }

+}

+

+function method Fib(n: int): int

+{

+  if n < 2 then n else Fib(n-2) + Fib(n-1)

+}

+

+method Test0() {

+  var c := new C;

+  var f := Fib(c.IgnoreFuel());

+  // with the bug, the following wwould take a long time before it reports an error

+  // after the bug fix, this still fails, but quickly

+  assert 0 <= f;

+}

+

+method Test1() {

+  var c := new C;

+  var f := Fib(c.x);

+  // the following assert will also fail, but quickly

+  assert 0 <= f;

+}

+

+method Test2() {

+  var c := new C;

+  c.x := 10;

+  var f := Fib(c.IgnoreFuel());

+  assert 0 <= f;  // passes

+}

+

+method Test3() {

+  var c := new C;

+  c.x := 10;

+  var f := Fib(c.x);

+  assert 0 <= f;  // passes

+}

+

+method Test4() {

+  var c := new C;

+  c.x := 10;

+  var f := Fib(c.x - 2);

+  assert 0 <= f;  // fails

+}

+

+method Test5(x: int)

+  requires 9 <= x - 1 && x + 1 <= 11

+{

+  var c := new C;

+  c.x := x;

+  var f := Fib(c.x);

+  assert 0 <= f;  // succeeds?

+}