A bug in variable merging.
taol-assignments opened this issue · 1 comments
taol-assignments commented
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.
msprotz commented
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.