Recursive decreases not checked properly

[RustanLeino]

Dafny version

4.9.1

Code to produce this issue

function F(x: int): int
  decreases G(x)
{
  G(x) - 1
}

function G(x: int): int
  decreases F(x)
{
  F(x)
}

method Main() {
  print F(5), "\n";
}

Command to run and resulting output

% dafny run test.dfy

Dafny program verifier finished with 2 verified, 0 errors
Stack overflow.
Repeat 52270 times:
--------------------------------
   at _module.__default.G(System.Numerics.BigInteger)
   at _module.__default.F(System.Numerics.BigInteger)
--------------------------------
   at _module.__default._Main(Dafny.ISequence`1<Dafny.ISequence`1<Dafny.Rune>>)
   at __CallToMain+<>c__DisplayClass0_0.<Main>b__0()
   at Dafny.Helpers.WithHaltHandling(System.Action)
   at __CallToMain.Main(System.String[])

What happened?

The decreases clauses of the mutually recursive F and G mention F and G themselves. This lets the local proof obligations go through, despite the fact that F and G always continue to call each other.

This is a regression bug from the recent CanCall PR. Essentially, the new CanCall assumptions allows access to the decreases clause of what's being called. Previously, these CanCall assumptions were missing, so access was not possible via CanCall. Previously, there was also another disjunct that allowed access to the function definition, but that part of the definition axiom was restricted to uses from outside the same strong connected component (SCC) of the call graph.

The fix is to forbid a decreases to mention anything from the same SCC. This is best checked in the resolver.

What type of operating system are you experiencing the problem on?

Mac