Tail recursion elimination for GenC (#1275)

[zhekai-jiang]

This is to address #1275 . We added a new phase to perform tail recursion elimination.

We added test cases in the GenCSuite.

As discussed during the presentation, we may want to take a closer look at ghost elimination and see whether it is doing the job correctly.

[CLAassistant]

All committers have signed the CLA.

[vkuncak]

Verification of TailRecComplexArgs.scala failed on the CI.

[vkuncak]

also of TailRecUnitIf.scala
https://github.com/epfl-lara/stainless/actions/runs/12630587164/job/35190698906

[zhekai-jiang]

Could we try to run the tests again? (Apparently it was because we didn't add the decreases measures for our new test cases, so Stainless was not able to verify everything, but this issue was not related to the generated C code.)

[zhekai-jiang]

By the way, I removed the test case TailRecReturnInLoop because apparently this kind of thing is not allowed by Stainless, because the loop will be rewritten into a function, and if we make a recursive call in the loop, it will make the inner function mutually recursive with the enclosing function and Stainless throws an error (which I think is from

stainless/core/src/main/scala/stainless/verification/TypeChecker.scala

Lines 1236 to 1251 in 88e4de5

	val errorInfo = tc.currentFid flatMap { currentFid =>
	val currentDeps = dependencies(currentFid)
	val mutuallyRecursiveDeps = currentDeps.filter { did =>
	dependencies(did).contains(currentFid)
	}
	if (mutuallyRecursiveDeps.contains(id)) {
	Some(s", because it is mutually recursive with the current function ${currentFid.asString}")
	} else {
	None
	}
	}
	reporter.fatalError(in.getPos,
	s"Call to function ${id.asString} is not allowed here${errorInfo.getOrElse("")}"
	)

)

[samuelchassot]

I rerun the CI 👍

By the way, I removed the test case TailRecReturnInLoop because apparently this kind of thing is not allowed by Stainless, because the loop will be rewritten into a function, and if we make a recursive call in the loop, it will make the inner function mutually recursive with the enclosing function and Stainless throws an error (which I think is from

stainless/core/src/main/scala/stainless/verification/TypeChecker.scala

Lines 1236 to 1251 in 88e4de5

	val errorInfo = tc.currentFid flatMap { currentFid =>
	val currentDeps = dependencies(currentFid)
	val mutuallyRecursiveDeps = currentDeps.filter { did =>
	dependencies(did).contains(currentFid)
	}
	if (mutuallyRecursiveDeps.contains(id)) {
	Some(s", because it is mutually recursive with the current function ${currentFid.asString}")
	} else {
	None
	}
	}
	reporter.fatalError(in.getPos,
	s"Call to function ${id.asString} is not allowed here${errorInfo.getOrElse("")}"
	)

)

About that: can't we keep the benchmark with the while loop then?

[samuelchassot]

Oh sorry, they're all new test cases! My bad!

[zhekai-jiang]

I see 3 failed tests, but they are not related to our part. Anyone has any idea why...?

[samuelchassot]

@vkuncak They're the same failing tests as on the other PR.
That's even more puzzling

[samuelchassot]

@sankalpgambhir could it be related to some Princess versions? They're not changing anything in the build file though.

[samuelchassot]

We investigated and these tests failing have nothing to do with your PR. It is happening because of the latest release of the Princess Solver. We will ignore those tests in a soon-to-be-merged PR.
You'll be able to update your branch and the CI should then pass :)