Detect non-returning functions

[Matt Giuca]

Some functions in Mars can never return under any circumstances. This includes functions which never terminate, and also those which always abort.

A current problem is that Mars requires all code paths in a function to return a value, even if those code paths would never complete or always abort. This creates awkward errors for code such as:

    if x:
        return y
    else:
        error(z)

Error: Function may not return a value.

The workaround is to write "return error(z)", but that's not ideal.

The language should specify a simple termination analysis, where each function is tagged with a boolean property "noreturn". The analysis states that:
- All functions are tagged "noreturn" by default unless shown through fixpoint to return on at least one code path.
- Calling a noreturn function invalidates a code path (that code path does not return).
- A conditional branch with a constant condition of 0 invalidates the "then" branch; with a constant nonzero condition invalidates the "else" branch. (Thus "while true" loops are shown not to terminate.)
- The "error" primitive is noreturn; all other primitives are not.

This allows infinite loops and calls to nonterminating functions to avoid compiler errors for not returning on that branch.