106 Unreachable

The statement unreachable; asserts that execution cannot reach its position. It terminates the current control-flow path and does not complete normally.

A program that can execute an unreachable; statement violates that assertion and is illegal. A compiler should reject as many such illegal programs as it can prove will, or may, reach the statement. This requirement is not a promise that every violation can be detected statically: reachability may depend on input data or on computations that cannot in general be decided at compile time.

func Integer sign(Integer x)
{
    if x < 0 {
        return -1;
    }
    if x = 0 {
        return 0;
    }
    if x > 0 {
        return 1;
    }

    unreachable;
}

The final statement records the programmer's assertion that the three preceding conditions are exhaustive. It is useful when that fact follows from an invariant or from knowledge that the compiler's ordinary control-flow analysis does not establish.

Standard library assertions

The unreachable statement allows the standard library assert operation to be implemented in Predica:

proc assert(Boolean condition)
{
    if ¬condition {
        unreachable;
    }
}

When condition is true, assert completes normally. When it is false, execution reaches unreachable; and the program is illegal. The compiler should reject calls whose failed assertion it can establish statically. The language does not prescribe whether an undetected failed assertion produces a diagnostic trap or any other particular runtime behaviour.

Static control-flow effect

For static analysis, unreachable; has no normally completing successor. Consequently, a path ending in unreachable; does not need to return a value from a block-bodied function and does not contribute an uninitialised location state to a later program point.

Before applying that control-flow effect, the compiler should attempt to establish whether the assertion can be violated. If it can prove that control reaches the statement, or that some possible execution reaches it, it should reject the program as illegal rather than merely emit an unreachable-code warning. Failure to prove a violation does not establish that the assertion is true.

func String describe(Boolean known, String text)
{
    var String result;

    if known {
        result := text;
    } else {
        unreachable;
    }

    return result;
}

The read of result is legal: every control-flow path that can complete normally and reach the return has initialised it. The assertion does not prove its own premise and does not make an otherwise invalid expression, update, or declaration well-typed. All statements that are analyzed before it remain subject to the ordinary static rules.

An unconditional return, break, continue, or unreachable makes the remainder of the same block unreachable by normal control flow. Such statements are permitted, but an implementation should diagnose them as unreachable-code warnings. They are not static errors, because generated code and temporarily disabled code may deliberately contain them.

Execution of an illegal program

If execution reaches unreachable;, the program has violated a programmer assertion and is illegal, even when the compiler did not detect the violation statically. The language does not prescribe what happens after that point. In particular, it does not require a Predica runtime exception, a trap, termination, or continuation with any particular behaviour.

An implementation may insert a diagnostic trap, for example in a debug build, and may omit it in another build. Optimizers may rely on the assertion that the statement is not reached. These implementation choices do not alter the legality rule and are not prescribed by the language.

Relationship to other terminating statements

• return completes the enclosing function or procedure normally.
• break transfers control beyond the nearest enclosing loop.
• continue transfers control to the next iteration of the nearest enclosing loop.
• an uncaught exception propagates through enclosing statement contexts.
• unreachable asserts that its position cannot be reached; reaching it makes the program illegal.

The statement may appear wherever a statement is allowed. Unlike break and continue, it need not be enclosed by a loop. Unlike return, it carries no expression and is independent of the enclosing function's result type.