A bug in tail recursive optimization.

[taol-assignments]

KreMLin (version 4e48d26) generated incorrect C code when compiling some trailing recursive Low* functions. Here is an example I found.

KreMLin Flags

-fextern-c -ftail-calls -fparentheses -fcurly-braces

Low* Code

let rec test (a b c: U32.t): Tot U32.t (decreases U32.v c) =
  let open U32 in
  if c >^ 0ul then test b a (c -^ 1ul) else a

Generated C code

uint32_t test(uint32_t a0, uint32_t b0, uint32_t c0)
{
  uint32_t a = a0;
  uint32_t b = b0;
  uint32_t c = c0;
  while (true)
  {
    if (c > (uint32_t)0U)
    {
      a = b;
      b = a;
      c--;
    }
    else
    {
      return a;
    }
  }
  KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
    __FILE__,
    __LINE__,
    "unreachable, returns inserted above");
  KRML_HOST_EXIT(255U);
}

The generated C function should swap a and b when c is greater than 0.

[msprotz]

Thanks for the report, I pushed a fix to a branch that should fix the problem.