Detect non-returning functions
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.