Make `old` a special case for trigger generation.

Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and
old(f(x)). This has a number of implications; see the new tests files for more
information.

1 files changed, 32 insertions, 0 deletions

diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
new file mode 100644
index 00000000..c54089f2
--- /dev/null
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
@@ -0,0 +1,32 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

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

+

+// This file shows cases where loops could hide behind equalities. In all three

+// cases we behave the same; that is, we don't warn for loops that would only

+// exist in the presence of an equality. The easiest way to understand the

+// issue, I (CPC) feel, is to look at the old case: f(x) could very well loop

+// with old(f(f(x))) if f(f(x)) did not change the heap at all.

+

+// This equality issue is generally undecidable. It could make sense to special

+// case `old`, but KRML and CPC decided against it on 2015-08-21. Future

+// experiences could cause a change of mind.

+

+class C { }

+function f(c: C): C

+function g(c: C): C

+function h(c: C, i: int): C

+

+// With explicit arguments

+method M0(i: int, j: int, sc: set<C>) {

+  assert forall c | c in sc :: true || h(c, i) == h(h(c, j), j);

+}

+

+// With implicit arguments (f and g respectively, to Apply)

+method M1(f: int -> int, g: int -> int) {

+  assert forall x :: true || f(x) == g(f(x));

+}

+

+// With implicit arguments (the heap, to old)

+method M2(sc: set<C>) {

+  assert forall c | c in sc :: true || f(c) == old(f(f(c)));

+}