Fix: Tail recursion not activated if cannot

[MikaelMayer]

This PR fixes #2726 and fixes #2706
I converted contracts to if-conditions, since the next case is the default non-recursive case.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[atomb]

My interpretation of the purpose of these calls to Contract.Assert is to check properties that are expected to always hold if the surrounding conditional expression is true. Although adding them to the conditional will prevent a crash, I'm wondering whether you've done any deeper investigation into why they're not always true in this case. I worry that there could be a deeper bug lurking that this just temporarily hides away.

[MikaelMayer]

Good question.
So here is the story as I understand it. The following code is a heuristic to check if a function is tail-recursive or not. It goes from bottom-up.
Look at u.size() + 1 in the code.
For binary operators, if the left operation is tail-recursive (which it is u.size()), and if the right operand is Triviallytailrecursive (1 is trivially tail recursive), then the binaryExpr's accumulator AccumulatesForTailRecursion is set to BinaryExpr.AccumulationOperand.Right, which makes sense. If the function is tail-recursive, the accumulation operand is the right one. But at this point, we haven't determined if the function is really tail-recursive or not.

dafny/Source/DafnyCore/Resolver.cs

Lines 7617 to 7646 in 8e2c073

	if (accumulationOp != Function.TailStatus.TriviallyTailRecursive) {
	var s0 = CheckTailRecursiveExpr(bin.E0, enclosingFunction, false, reportErrors);
	Function.TailStatus s1;
	switch (s0) {
	case Function.TailStatus.NotTailRecursive:
	// Any errors have already been reported, but still descend down bin.E1 (possibly reporting
	// more errors) before returning with NotTailRecursive
	s1 = CheckTailRecursiveExpr(bin.E1, enclosingFunction, false, reportErrors);
	return s0;
	case Function.TailStatus.TriviallyTailRecursive:
	// We are in a state that would allow AcculumateLeftTailRecursive. See what bin.E1 is like:
	if (accumulatesOnlyOnRight) {
	s1 = CheckHasNoRecursiveCall(bin.E1, enclosingFunction, reportErrors);
	} else {
	s1 = CheckTailRecursiveExpr(bin.E1, enclosingFunction, false, reportErrors);
	}
	if (s1 == Function.TailStatus.TailRecursive) {
	bin.AccumulatesForTailRecursion = BinaryExpr.AccumulationOperand.Left;
	} else {
	Contract.Assert(s1 == Function.TailStatus.TriviallyTailRecursive || s1 == Function.TailStatus.NotTailRecursive);
	return s1;
	}
	return accumulationOp;
	case Function.TailStatus.TailRecursive:
	// We are in a state that would allow right-accumulative tail recursion. Check that the enclosing
	// function is not mentioned in bin.E1.
	s1 = CheckHasNoRecursiveCall(bin.E1, enclosingFunction, reportErrors);
	if (s1 == Function.TailStatus.TriviallyTailRecursive) {
	bin.AccumulatesForTailRecursion = BinaryExpr.AccumulationOperand.Right;
	if (accumulationOp == Function.TailStatus.AccumulateLeft_Concat) {

What makes no sense is, in the function SinglePassCompiler.TrExprOpt, to convert a binary expression to a tail-recursive equivalent only on the basis that BinaryExpr.AccumulationOperand is not None, because, as we've seen earlier, this was a conditional accumulation. There was another branch l.size() + r.size() that would eventually make the function not tail-recursive.

[atomb]

I think that makes sense. It perhaps would be a good idea at some point to change the way the accumulation operand is set (e.g., have it be None if the function isn't tail recursive), but I think it clarifies that the additional condition seems like the right approach.

[atomb]

I'm convinced that this is the right solution now! :)

[atomb]

I think that makes sense. It perhaps would be a good idea at some point to change the way the accumulation operand is set (e.g., have it be None if the function isn't tail recursive), but I think it clarifies that the additional condition seems like the right approach.

[cpitclaudel]

It's surprising to me that the whole invariant needs to be converted to a check. Are these really all independent parameters?

[cpitclaudel]

Suggested change

	&& enclosingFunction != null
	&& enclosingFunction.IsAccumulatorTailRecursive) {
	&& enclosingFunction is { IsAccumulatorTailRecursive: true }) {

[cpitclaudel]

(Just a question of taste, so don't feel that you have to apply this one)