Jump forwarding

[ThomasHaas]

This PR adds a pass that simplifies the following types of code

lbl1; // Any jump to lbl1 can get forwarded to jump directly to lbl2
lbl2;

and

lbl; // Any jump to lbl can get forwarded to jump directly to X
goto X;

While this pass already deletes labels whose jumps can get forwarded, it still produces redundant code with e.g. multiple subsequent gotos. It would be good to run DCE (Dead Code Elimination) afterwards, but this has currently 2 problems:

• DCE is assumed to run before unrolling and it will update the oId of events.
• DCE can remove assertions (cause e.g. the last loop iteration is unreachable and it contains an assertion). Removing assertions causes a lot of problems right now, because Program stores state about the assertions which needs to get updated properly. But updating the assertion requires knowing whether we have litmus code or boogie code.

After DCE, Simplifier can also remove code of the form of goto lbl; lbl;. Running all these passes repeatedly also causes a lot of logging output which might be better summarized in a single logging message.

[ThomasHaas]

The forwarding is not applicable under Linux, because it can delete else-branches (which happens if those are empty). This causes the control-dependencies to end up being wrong (due to IfAsJump failing). So this adds another problem to this pass.

I think we need a tag DO_NOT_OPTIMIZE (or SYNTACTIC_DEPENDENCY to indicate that we need the syntactic element as is). We can tag bound events, fake dependencies and labels associated with if-then-else constructs to avoid accidental deletion of those.

I won't fix all these problems now, but maybe we should keep this PR as a sort of work in progress and as an indicator for what problems we still face (this PR reveals a lot of minor problems we eventually need to fix).