FStarLang/karamel

A bug in variable merging.

taol-assignments opened this issue · 1 comments

KreMLin (version 4e48d26) generated incorrect C code with the -fmerge aggressive options.

Low* Code

open U32

inline_for_extraction
private let test1(b: U32.t{U32.v b < 10}): Tot U32.t =
  let g = 10ul +^ b in
  if g >^ 5ul then
    let d = g -^ 1ul in
    g +^ d
  else
    0ul

let rec test2(a: U32.t{U32.v a < 10}): Tot U32.t (decreases U32.v a) =
  let c = test1 a in
  if a >^ 0ul then
    test2 (a -^ 1ul)
  else
    c

Compiled C Code

uint32_t test2(uint32_t a0)
{
  uint32_t a = a0;
  while (true)
  {
    uint32_t g = (uint32_t)10U + a;
    uint32_t c;
    if (g > (uint32_t)5U)
    {
      a = g - (uint32_t)1U;
      c = g + a;
    }
    else
    {
      c = (uint32_t)0U;
    }
    if (a > (uint32_t)0U)
    {
      a--;
    }
    else
    {
      return c;
    }
  }
  KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
    __FILE__,
    __LINE__,
    "unreachable, returns inserted above");
  KRML_HOST_EXIT(255U);
}

The C code above will loop infinitely.

Is this using the combination of -fmerge and -ftail-calls?

Thanks for the repro. From the Changelog,

### Jan 13th, 2020
 
 - New *experimental* option: `-fmerge`, to merge variables, i.e. reuse existing

so, I don't think it's been extensively tested (and it's marked as experimental). I'd happily take a fix if you have one.