stainless
stainless copied to clipboard
Tail recursion elimination for genc
Investigate if it is feasible to peroform tail recursion elimination in genc itself, for non-mutual recursion.
Currently, this is not needed when using genc with GCC output, which performs tail recursion elimination; doing it inside genc would allow the use in those compilers that do not do it, or fail to do it in particular case.
In particular, the code we generate sometimes looks like this:
def f(...) =
...
val res = f(...)
return res
which may confuse the C compiler.
Also, C comiler may not have as precise escape information when we pass variables by reference, see e.g.: https://groups.google.com/g/llvm-dev/c/JP2cxsL9yWI/m/Q3rnf-W8BwAJ whereas we have tight alias control policy.