stainless icon indicating copy to clipboard operation
stainless copied to clipboard

Tail recursion elimination for genc

Open vkuncak opened this issue 3 years ago • 0 comments

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.

vkuncak avatar May 30 '22 09:05 vkuncak