Probable bug in `LoopRefine` about rellic HOT 4 CLOSED

Uninformed guess: the code to go from while to do+while finds the conditional break, but either doesn't check that it is lexically first, or that all sub-statements of the while are conditional.

from rellic.

Here is a fun idea! What if the transform proceeded like this, and I am not claiming correctness of this:

while(1U) {
  a = sth;
  if(a == 10) {  <-- break condition identifier
    break;  <-- break objserved
  }
  if(a != 10) {
    body;
  }
}

wrap all sub-statements in exit condition, after re-forming do-which

  if (a != 10) {
    a = sth;
  }
  if (a != 10) {
    if(a == 10) {
      break;
    }
  }
  if (a != 10) {
    if(a != 10) {
      body;
    }
  }
} while (a != 10);

refine1:

do {
  if (a != 10) {
    a = sth;
  }
  if (a != 10) {
    if(0) {
      break;
    }
  }
  if (a != 10) {
    if(1) {
      body;
    }
  }
} while (a != 10);

refine2:

do {
  if (a != 10) {
    a = sth;
  }
  if (a != 10) {
    
  }
  if (a != 10) {
    body;
  }
} while (a != 10);

refine3:

do {
  if (a != 10) {
    a = sth;
  }
  if (a != 10) {
    body;
  }
} while (a != 10);

refine4:

do {
  if (a != 10) {
    a = sth;
    body;
  }
} while (a != 10);

not sure where this is going

from rellic.

anyway, could it possibly be because the do-while condition refinement asserts the while condition before entering the do, which wouldn't be valid?

from rellic.

What is happening is:

1. the if(a == 10) { break; } if(!(a == 10)) { body; } is turned into if(a == 10) {break;} else {body;}
2. the if is recognized as being the stopping condition for a do...while by LoopRefine. The else body is added to the loop without a guard

What should happen instead is that the else body should be added guarded by !(a == 10).

from rellic.