SSA fails on program with infinite loop

[aaronbembenek]

I've run this script (using bincaml commit f6421ac):

(load-il ssa-fail.il)
(run-transforms ssa)

And I get this error:

Failure("not found: #nondet_32_1:bv32 likely a read-uninitialised variable")

However, this variable is initialized:

  block %main_entry {.address = 0x400640; .originalLabel = "KTHyjTW0SWiGwqylcMDw6Q=="} [
    var Stack_n16_n8: bv64 := R29_in:bv64 { .label = "4195904_1" };
    var Stack_n8_0: bv64 := R30_in:bv64 { .label = "4195904_2" };
    (var #nondet_32_1: bv32) := call @_havoc();
    goto(%phi_4, %phi_5);
  ];

I suspect it has to do with the fact that the program has an infinite loop (the same error has popped up in other programs with infinite loops).

ssa-fail.zip

[agle]

Yeah; minimized the loop is sufficient to make it fail:

prog entry @main_4195904;

proc @main_4195904 () -> ()
[
  block %main_entry [
    var #nondet_32_1: bv32 := 5:bv32;
    goto(%i);
  ];
  block %i [
    assert bvsgt(#nondet_32_1:bv32, 0x5:bv32);
    goto(%main_loop1_5);
  ];
  block %main_loop1_5 [
    goto(%main_loop1_5);
  ]
];

This is because we only perform SSA on live variables, and nothing is live in a procedure which does not return.