Fix if-then-else simplifications

[peterschrammel]

Partially reverts 199d4cc, which accidentially disabled simplifications that require incomplete instructions to be marked GOTO.

Code such as

if (i > 0) x++;
else  x--;

will (now again) be converted to

IF i <= 0 THEN GOTO 1
x = x + 1;
GOTO 2
1: x = x - 1;

instead of

IF !(i <= 0) THEN GOTO 1
GOTO 2
1: x = x + 1;
GOTO 3
2: x = x - 1;

[allredj]

Passed Diffblue compatibility checks (cbmc commit: e2a32bd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76406298

[kroening]

This doesn't work; there is an expectation that a GOTO has a target. The one added doesn't, which will fail the precondition of get_target().

[tautschnig]

I'm of course unaware of any business constraints, and this proposed change may just be the quick fix that's needed right now. Just like @kroening said, this doesn't seem right. So I'm not really in favour of the change as proposed. There has definitively been a positive side effect here: a new test case more clearly describing expectations is going to be in place. Hence I'd propose the following:

1. Split the pull commit so that the regression test is in a separate commit, marked as KNOWNBUG.
2. If there are needs for an immediate fix, then use the change as proposed here (and as part of that commit turn the regression test into CORE).
3. If there is more time, investigate a way to optimise the generated goto program/generate a more optimised sequence of instructions for if/else without temporarily creating an invalid instruction.

[peterschrammel]

I'm afraid, we'll have to do 1+2 for now, because removing that optimisation is quite disruptive wrt coverage goal instrumentation.

I fully agree that we would like to make sure that certain invariants hold on each instruction in a goto program at any time. However, I don't see how an instruction with NO_INSTRUCTION_TYPE could be considered "valid". I doubt that such an instruction should be the mechanism for enabling the two-step initialisation of certain instructions that the current translation process requires (in particular, since the instruction type is already determined in the first initialisation step and this information is crucial for the optimisations performed in the second initialisation step).

[tautschnig]

In my opinion, the final solution should really be such as to never generate that instruction in the first place. Neither NO_INSTRUCTION_TYPE nor incomplete-goto seem right to me. Doing so may require some larger refactoring and additional data structures to maintain the information that this temporary instruction presently conveys. Doing this larger-scale work may be infeasible within minutes and may thus have to be put in an issue (@peterschrammel, please create one if you have to go that route).

[peterschrammel]

@kroening, I've added an issue here: #2357 Let's discuss what the preferred fix for this is.

[allredj]

Passed Diffblue compatibility checks (cbmc commit: 4394016).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76435965