New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Specification: Specify static analysis of function body execution that "falls through" at the end #35330

Open
eernstg opened this Issue Dec 5, 2018 · 4 comments

Comments

2 participants
@eernstg
Member

eernstg commented Dec 5, 2018

The language specification is currently silent on the treatment of the situation where a function body completes normally (that is, we reach the end rather than reaching an explicit return statement), but it should say that this situation is treated like encountering an explicit return; which is added at the end of the function body.

This means that, for instance, we will make it an error to fall through in a function with return type int:

int f() {
} // Error, as if `return;` had been added at the end of the body.

However, in the case where the location just after the body cannot be reached, we do not wish to emit an error:

int f() {
  return 42;
} // No error: Body will return a value, cannot complete normally.

The property of being unreachable is obviously undecidable in general, so we will approximate it conservatively (as in "this location can definitely not be reached", as opposed to "this location cannot be proven to be reachable"). So we may still raise an error in a situation where the end of the body cannot actually be reached, but that's a fact that we cannot prove. Consequently, some function bodies will need to contain code which is semantically unreachable, but in return we get the guarantee that no function execution will fall through at the end, except for the ones where return; would be OK.

We will probably want to specify a notion of having an explicit return or throw statement on every path in the control flow graph, possibly including known-infinite loops, evaluation of expressions of type bottom (if we add such a type, evaluation of such an expression will not complete normally), and whatever else is considered worthwhile.

Currently, the specification says that the notion of being statically unreachable will be specified in the future, and this issue is concerned with doing that.

@lrhn

This comment has been minimized.

Member

lrhn commented Dec 5, 2018

The subject and lead-in sounds like this is about the dynamic behavior.
I believe the spec says that if the body completes normally, the invocation gets a null returned:

\subsection{Function Invocation}
...
If the execution of the body of $f$ returns a value, $v$, (\ref{completion}), the invocation evaluates to $v$.
If the execution completes normally or it returns without a value, the invocation evaluates to the null object (\ref{null}).
If the execution throws an exception object and stack trace, the invocation throws the same exception object and stack trace (\ref{evaluation}).
\commentary{
A complete function body can never break or contine (\ref{completion})
because a \BREAK{} or \CONTINUE{} statement must always occur inside the statement that is the target of the \BREAK{} or \CONTINUE{}.
This means that a function body can only either complete normally, throw, or return.
Completing normally or returning without a value is treated the same as returning the null object (\ref{null}), so the result of executing a function body can always be used as the result of evaluating an expression, either by evaluating to a value or by the evaluation throwing.
}

(my emphasis).

The remaining text sounds like it's discussing static errors from not having a return on all branches.
We are, as usual, very bad at flow analysis, and the Dart 1 spec only said that all method bodies end with return null; (which does not count towards not having both return; and return e; in the same body).
The typical way we would handle this is to say that the body must "end with" a return or a throw statement (or that it "definitely throws or returns"). We can then either specify that cleverly, or take it literally, like we usually do (q.v. switch cases that must "end with" a control flow statement).

@eernstg

This comment has been minimized.

Member

eernstg commented Dec 5, 2018

The subject and lead-in sounds like this is about the dynamic behavior.

No, this is intended to be about the static analysis, and about compile-time errors, which is also the reason why I wrote

The property of being unreachable is obviously undecidable in general, so we will approximate it

Adjusted the title to make this explicit.

The remaining text sounds like it's discussing static errors

Exactly, and

The typical way we would handle this is to say that the body must
"end with" a return or a throw statement (or that it "definitely throws or returns")

Yes, and this issue is concerned with the task to say exactly such things in a way that is both reasonably precise, realistically implementable, and pragmatically non-stupid. ;-)

@eernstg eernstg changed the title from Specification: Specify treatment of function body execution that "falls through" at the end to Specification: Specify static analysis of function body execution that "falls through" at the end Dec 5, 2018

@lrhn

This comment has been minimized.

Member

lrhn commented Dec 5, 2018

and pragmatically non-stupid. ;-)

You just had to add that, didn't you?!
There goes our normal strategy.

@eernstg

This comment has been minimized.

Member

eernstg commented Dec 5, 2018

You just had to add that, didn't you?!

Of course! ;-)

But, seriously, we want that property, as opposed to the situation where developers are thinking "why can't the compiler understand that we will always return something?" because the static approximation that we've chosen is unable to see that the body could indeed never fall through at the end.

There goes our normal strategy.

We can still be strategically stupid. ;-)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment