Detect non-returning functions

Bug #596829 reported by Matt Giuca
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
Mars
Triaged
Wishlist
Matt Giuca

Bug Description

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.

Tags: language
To post a comment you must log in.
This report contains Public information  
Everyone can see this information.

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.