Semantics of if-simplification transform

semantics_of_transform.md

if-goto transformation

An if-else-if-else statement in C is written as follows:

if (/* cond1 */) {
    /* cond1 true branch */
} else if (/* cond2 */) {
    /* cond2 true branch */
} else {
    /* false branch */
}

And can be expressed using S-expressions:

(
    (if cond1
        (cond1-true-branch)
        (if cond2
            (cond2-true-branch)
            (false-branch)
        )
    )
)

The if-goto transformation replaces else-if and else clauses with a series of if statements with a goto statement appended to its if-true branch that jumps to a label at the end of the construct.

The resulting AST as S-expressions would look something like this:

(
    (if cond1
        (
            (cond1-true-branch)
            (goto end)
        )
    )
    (if cond2
        (
            (cond2-true-branch)
            (goto end)
        )
    )
    (false-branch)
    (label end)
)

As the false branch can only be executed if the true brunch does not execute, the above is semantically equivalent to:

(
    (if cond1
        (
            (cond1-true-branch)
            (goto end)
        )
    )
    (if cond2
        (cond2-true-branch)
        (false-branch)
    )
    (label end)
)

And then, in turn:

(
    (if cond1
        (cond1-true-branch)
        (if cond2
            (cond2-true-branch)
            (false-branch)
        )
    )
)

Therefore the original if-else-if-else statement above is semantically equivalent to the transformed if-goto statement and thus the transformation is semantic-preserving.

The transformed C would then be:

if (/* cond1 */) {
    /* cond1 true branch */
    goto end;
}
if (/* cond2 */) {
    /* cond2 true branch */
    goto end;
}
/* false branch */
end: