Never say never, part two

Posted on February 24, 2011 by Eric Lippert

This is part two of a two-part series about determining whether the endpoint of a method is never reachable. Part one is here. A follow-up article is here.

Whether we have a "never" return type or not, we need to be able to determine when the end point of a method is unreachable for error reporting in methods that have non-void return type. The compiler is pretty clever about working that out; it can handle situations like

int M()
{
  try
  {
    while(true) N();
  }
  catch(Exception ex)
  {
    throw new WrappingException(ex);
  }
}

The compiler knows that N either throws or it doesn't, and that if it doesn't, then the try block never exits, and if it does, then either the construction of the exception throws, or the construction succeeds and the catch throws the new exception. No matter what, the end point of M is never reached.

However, the compiler is not infinitely clever. It is easy to fool it:

int M()
{
  int x = 123;
  try
  {
    while(x >= x / 2) 
      x = x / 2;
  }
  catch(Exception ex)
  {
    throw new WrappingException(ex);
  }
}

Here x is always going to be a small, non-negative integer, and a small, non-negative integer is always greater than or equal to half of it. You know that, I know that, but the compiler doesn't know that. The compiler complains that this method has a reachable end point, even though clearly the end point will never be reached. We could put that logic into the compiler if we really wanted to; we could be more clever.

How much more clever could we be? Is there any limit to our cleverness? Could we in theory produce a compiler that perfectly determined whether the end point of a method was reachable?

Turns out, no. A proof of that fact is a bit tricky, but we're tough, we can do it.

First off, let's restrict the problem to a particular pattern. Consider programs of this form:

class Program
{
  private static string data = @"some data goes here";
  public static int DoIt()
  {
    // some code goes here
  }
}

The question is "given values for 'some data' and 'some code', does DoIt have a reachable end point?" If we can't solve the problem for programs with this very restrictive format then we can't solve it in general, so let's explore whether we can solve problems in this limited format.

Let's suppose that we have a class in our compiler library with a public method that answers that question, and deduce a contradiction. We assume that "code" is a legal body of a C# program and "data" is the legal contents of a string literal.

public class Compiler
{
  public static bool HasReachableEndPoint(string code, string data)
  {
    // [Omitted: work out the result and return it]
  }
}

And now things get really weird. What if we call:

string weird = @"
  if (Compiler.HasReachableEndPoint(data, data))
    return 123;
"; 
// Recall that C# has multi-line string literals. 
// The "code" above is in the string.
bool result = Compiler.HasReachableEndPoint(weird, weird);

What does that do? It attempts to work out whether DoIt has a reachable end point in this program:

class Program
{
  private static string data = @"
    if (Compiler.HasReachableEndPoint(data, data))
    return 123;
  ";
  public static int DoIt()
  {
    if (Compiler.HasReachableEndPoint(data, data))
    return 123;
  }
}

What is the value of result? Suppose it is true. Then that means that DoIt has a reachable end point. Which means that when we run DoIt, the call in the conditional statement returns false. But data and weird refer to the same string, so why is result true if the result of the same call is going to be false? That's logically inconsistent, so result cannot be true. Clearly I cannot drink from the cup closest to me.

Suppose result is false. That means that DoIt does not have a reachable end point. Which means that Compiler.HasReachableEndPoint(data, data) always either returns true, or throws an exception, or runs forever. But again, data and weird are the same string, so why would it return true, throw, or run forever here, when by assumption it returns false normally when given that input? Clearly result is not false either, since that leads to a contradiction. Clearly I cannot drink from the cup closest to you.

Since result can logically be neither true nor false, HasReachableEndPoint must either throw or go into an infinite loop when given these inputs. But if it does that then there are some inputs for our reachability tester which cause the compiler to fail or run forever, which seems bad. The compiler needs to be able to compile all legal programs and error on all illegal programs; ideally we don't want to crash, run forever, or give a wrong answer for any possible input.

What we've shown here is, first, that you should never go up against a Sicilian when death is on the line, and second, that an endpoint reachability tester logically must either (1) sometimes give the wrong answer, or (2) sometimes fail to give an answer. The reachable endpoint problem is in general not reliably solvable by compilers no matter how clever the compiler writers are.

Now, you might reasonably push back on this proof, noting that the proof relies upon an absolutely crazy situation, namely, a program that contains part of its own code as data that itself calls the reachability analyzer in what Douglas Hofstadter calls a "strange loop". Even if you don't like the proof though, we have other evidence that a "perfect" reachable end point detector that always returns a correct result in finite time is probably impossible. Consider for example this totally trivial little method, with just five loops and some calculations on an arbitrary-precision integer type:

public static int DoIt()
{
  Integer max = 0;
  while(true)
  {
    max += 1;
    for (Integer x = 1; x <= max; ++x)
      for (Integer y = 1; y <= max; ++y)
        for (Integer z = 1; z <= max; ++z)
          for (Integer n = 1; n <= max; ++n)
            if (x.Power(n+2) + y.Power(n+2) == z.Power(n+2)) 
              goto done;
  }
  done: ;
  // Uh oh, we "forgot" to return an int.
  // But that's only a problem if the label is reachable.
}

Want to know if Fermat's Last Theorem is true? Just run your magical perfect C# compiler on a class containing that method and see if it compiles. If it fails with a "reachable end point in non-void-returning method" error then the goto must have been reachable, which means that there is a non-trivial solution to the equation, and Fermat's Last Theorem is false. If compilation succeeds (with a warning that there's an unreachable label!) then the goto was unreachable and the theorem is true. To answer the question you don't even need to run the program, you just have to run the compiler! The fact that this program is insanely inefficient in the amount of recalculation it performs is irrelevant, since we're not going to even run it.

Such a compiler would enable us to answer any open question in finite mathematics simply by writing a program that terminates if the hypothesis is true and runs forever if it is not. It seems inconceivable that we could even in theory construct a compiler that had the ability to answer all unsolved problems in the entire history of finite mathematics.

This famous problem is called the "Halting Problem" because it is usually posed for computational systems that do not have "throw an exception" as an option. The only alternatives are "halt with a result", or "go into an infinite loop".

The Halting Problem is of course solvable by heuristics provided that you can tolerate false positives. The C# compiler will cheerfully tell you if the end point of a method is absolutely guaranteed to be unreachable, but as we've seen, you can fool it into telling you that some unreachable end points are reachable. As long as it does not have false negatives (that is, sometimes tells you that the reachable end point of a method is unreachable) everything is fine.

This is part two of a two-part series about determining whether the endpoint of a method is never reachable. Part one is here. A follow-up article is here.

Never say never, part one

Posted on February 21, 2011 by Eric Lippert

This is part one of a two-part series. Part two is here.

Can you find a lambda expression that can be implicitly converted to Func<T> for any possible T?

Hint: The same lambda is convertible to Action as well.

Func<int> function = () => { throw new Exception(); };

The rule for assigning lambdas to delegates that return int is not "the body must return an int". Rather, the rules are:

All returns in the block must return an expression convertible to int.
The end point of the block must not be reachable.

Both those conditions are met. The first one is vacuously met; zero out of zero returns meet the condition, so that's all of them. The second one is met because the compiler can deduce that no possible code path hits that end brace. Either new Exception() throws, or it goes into an infinite loop, or it succeeds and its value is thrown; no matter what, there's no possibility of the function completing normally. Of course the conditions are met for any type argument, not just int.

Similarly, it's assignable to Action because the rule for Action is simply that every return in the block must not have an expression. Again, that condition is met vacuously.

The rule for lambdas is just a special case of the rule for regular functions. This is perfectly legal, for precisely the same reasons:

int I.M()
{
  throw new NotImplementedException();
}

Why then is this application of the "extract method" refactoring not legal?

private static void AlwaysThrows()
{
  throw new NotImplementedException();
}
int I.M()
{
  AlwaysThrows();
}

The problem here is that the C# compiler does not perform interprocedural control flow analysis. We do analysis of one method body at a time, and we trust the declared return type of the method to be accurate. The declared return type of AlwaysThrows is void, and void means that it returns no value, but it does possibly return. Therefore, the end point of the call to AlwaysThrows is reachable, and therefore the end point of M is reachable without returning an integer. You and I both know that it is not reachable, but the compiler is not sophisticated enough to know that.

Of course, this is a silly example, but it doesn't take much to turn this into a realistic example. You see this sort of thing in unit testing frameworks all the time:

Frog frog;
try
{
  frog = Animals.MakeFrog();
}
catch(Exception ex)
{
  LogAndThrowTestFailure(ex); // always throws
}
frog.Ribbit();

The compiler complains that frog.Ribbit() is illegal because MakeFrog might have thrown before frog was assigned, and LogAndThrowTestFailure -- which we know always throws but the compiler doesn't know that -- might have returned normally, in which case frog is not definitely assigned at the point of the call. If instead it had been

catch(Exception ex)
{
  throw LogTestFailureAndReturnAnotherException(ex);
}

then the compiler would correctly reason that the call to Ribbit is only reachable if the assignment succeeded.

What, if anything, can we do about this?

In practice, nothing. You've got to write something like

int I.M()
{
  AlwaysThrows();
  return 0;
}

to shut the compiler up, or make AlwaysThrows return the exception and then throw it.

What about in theory? Is there anything the language designers could have done to ease this burden?

As I mentioned before, we could do interprocedural analysis, but in practice that gets real messy real fast. Imagine a hundred mutually recursive methods that all go into an infinite loop, throw, or call another method in the group. Designing a compiler that can logically deduce reachability from a complex topology of calls is doable, but potentially a lot of work. Also, interprocedural analysis only works if you have the source code for the procedures; what if one of these methods is in an assembly, and all we have to work with is the metadata? (Moreover, as we'll see next time, even interprocedural flow analysis is insufficient to solve the problem in general.)

What we need to solve this problem without interprocedural analysis of source code is a another kind of return type. The CLR supports three kinds of return types today. You can return values of value type or reference type, like int or string. You can return nothing, in which case the method is marked "void". Or you can return an alias to a variable.¹ What we need is a fourth kind of return type, the "this method never returns normally" return type. Such a method would have to contain no returns whatsoever and not have a reachable end point. We could know that it does not have a reachable end point by checking whether on every possible code path it always throws, always goes into an infinite loop, or always calls another "never" method.

Some programming languages do have a "never" return type; Curl, for example. A similar function annotation has also been proposed for ECMAScript. But since doing it properly in C# requires support from the verifier in the CLR, it's unlikely that it will become a feature of mainstream CLR languages. Particularly when there are such easy workarounds for the rare circumstances in which you are calling a method that never returns.²

Next time on FAIC: could we be more clever? Just how clever can we be?

C# does not support this latter feature; C# only supports "ref" on variables going in to a method call, but we could also support ref on variables coming out if we chose to. Don't hold your breath while waiting for it. See my article on this subject for more details. ↩
For additional thoughts on programming styles in which methods never return, see my long series of articles on Continuation Passing Style. ↩

Fabulous Adventures In Coding

Eric Lippert's blog

Monthly Archives: February 2011

Never say never, part two

Never say never, part one