fix: Correctly substitute type variables in override checks

[cpitclaudel]

This is the "proper" fix for issue #2429 (#2519 was an easy workaround, now subsumed by this PR).

Note that it surfaces (or introduces?) a different bug: after applying that this patch I can make Dafny crash with the following input […] I suspect it's a problem in the substitution with let bindings, but I haven't completed the investigation. I have reported it at #2526, and I don't think it should block this PR.

Detailed explanation:

When Dafny translates a class, the override check that it performs mentions the
old ensures clauses, applied to its new arguments. For example, the following
code:

trait T           { method M(a: int) returns (b: int) ensures b > a     }
class C extends T { method M(a: int) returns (b: int) ensures b > a + 1 }

… leads to the following check:

implementation OverrideCheck(this: ref, a#0: int) returns (b#0: int) {
  assume b#0 > a#0 + 1;
  assert b#0 > a#0;
}

Problems pop up when argument types differ between the old and new ensures
clauses, which happens in the presence of type parameters:

predicate P<A>(s: seq<A>)
trait T<A> {
  method M(a: A) ensures P([a][0 := a])
}

predicate Q<A>(s: seq<A>)
class C extends T<object> {
  method M(a: object) ensures Q([a][0 := a])
}

When translating the original ensures clause (ensures P([a][0 := a])) to Boogie
in the override check, Dafny uses the old types in some places, and hence
assumes that [a] has type seq<A>, not type seq<object>. This causes it to
make a mistake about whether to insert a box, and generate the following Boogie
code:

assume _module.__default.Q(Tclass._System.object(),
  Seq#Update(Seq#Build(Seq#Empty(): Seq Box, $Box(a#0)), LitInt(0), $Box(a#0)));
assert _module.__default.P(_module.T$A,
  Seq#Update(Seq#Build(Seq#Empty(): Seq Box, $Box(a#0)), LitInt(0), a#0));

Notice how the assert line differs from the assume one: the former (with the
Q) correctly boxes a#0 twice: once in the sequence construction and once in
the update. In contrast, the latter (with P, corresponding to the trait's
ensures), incorrectly omits the box on the second a#0 (the argument to
Seq#Update).

The reason for the discrepancy is that the translation for Seq#Build uses the
type of the element to decide whether to insert a box (which evaluates to
object in both statements), whereas the translation for Seq#Update uses the
Arg field in the type of the sequence itself to decide whether to box a#0.
That type evaluates to object in the assume but to Q in the assert, and
hence no box is inserted.

Closes #2429.

[RustanLeino]

Looks good, but please add the extra tests.

[RustanLeino]

Please also add tests for the other clauses. For example:

predicate P<A>(s: seq<A>)

trait T<A> {
  method M(a: A)
    requires P([a][0 := a])
    modifies if P([a][0 := a]) then {} else {this}
    ensures P([a][0 := a])
    decreases if P([a][0 := a]) then 3 else 4
  function F(a: A): int
    requires P([a][0 := a])
    reads if P([a][0 := a]) then {} else {this}
    ensures F(a) == 5 ==> P([a][0 := a])
    decreases if P([a][0 := a]) then 3 else 4
}

predicate Q<A>(s: seq<A>) ensures Q(s) ==> P(s)

class C extends T<object> {
  // A missing type substitution in the translator used to cause issues here:
  method M(a: object)
    requires Q([a][0 := a])
    modifies if Q([a][0 := a]) then {} else {this}
    ensures Q([a][0 := a])
    decreases if Q([a][0 := a]) then 3 else 2
  function F(a: object): int
    requires Q([a][0 := a])
    reads if Q([a][0 := a]) then {} else {this}
    ensures F(a) == 5 ==> Q([a][0 := a])
    decreases if Q([a][0 := a]) then 3 else 4
}

Curiously, to trigger the bug for requiers/modifies/reads/ensures, it was necessary only to include the specification clause in the trait. But for decreases, one had to include it in both the trait and the class in order for the malformed Boogie to appear.