# Full Employment Theorem for Compiler Writers

## Informal Statement

The problem of given a program and a property that is true for some programs and false for other programs, check (precisely) whether program satisfies is undecidable if property talks only about the values computed by the program and program termination (and not e.g. how the values are computed).

This follows from Rice's theorem which follows from the undecidability of the Halting problem

• to check if terminates, we build a program such that and a program , that behaves like if does not terminate, and otherwise ## Consequences

Examples of undecidable problems:

• can a given program reach a state where null dereference happens
• is a given variable dynamically alive at a given program point in a given program
• is the given variable initialized before the execution reaches a given program point
• are the values of two given variables equal in all executions of the program
• does the given assertion evaluate to 'true' in all executions of a given program

How can we then build compilers?

• we do not attempt to answer this question precisely
• we either compute an answer, or we say “we do not know”
• we say compilers do “conservative” static analysis

In initialization analysis, output is:

• variable is definitely initialized
• variable is possibly un-initialized (either it is un-initialized, or it is initialized but it is too hard to see why)

In live-variable analysis, output is:

• variable is definitely not live
• variable is live (it is either dynamically live, or it is not dynamically live but it is difficult to see why)

## Proof Sketches

Halting Problem Undecidability Theorem (Turing): There is no program (think of it as analyzer that checks if programs are terminating) that takes as input a representation of an arbitrary program and the input of the program , and determines whether will terminate its computation if we ran on input .

Proof sketch: This is a proof by a diagonal argument. Suppose that we do have such program . Then define the following program that takes program descriptions as input:

`def F(Y) = if H(Y,Y) then (while(true){}) else true`

The question is then whether running will terminate. There are two cases, either holds, or not.

If holds, then , by definition of enters the 'true' branch and thus executes

`  while(true){}`

Thus, does not terminate. But this is in contradiction with the definition of , which says that terminates on input .

If does not hold, it then goes to 'else' branch and terminates. But this is in contradiction with the definition of being false, which says that should not terminate on input .

Impossibility of detecting dead code: There is no program (think of it as data-flow analyzer) that can take as an input a program and a program location , whether there exists an execution of that reaches .

Proof sketch: By reduction to previous theorem. We can always transform a given program into a program that always terminates in its last location (all 'halt' and 'exit' instructions are replaced by a jump to end of the program). Suppose p0 is such a program. To check if p0 terminates on an input , we consider the program

```def p = {
p0
L: {}
}```

Clearly, if p0 terminates, then it will execute L. Conversely, if p0 does not terminate, it will never reach L. Therefore, checking if would tell us whether p0 terminates. By Halting problem, this is undecidable, so cannot exist. QED

Impossibility of checking assertions: There is no program that will accept a program containing assertions and check whether these assertions are true in all executions.

Proof: By reduction to previous theorem. Given a program with assertions, we introduce a fresh location L and replace each assertion

`  assert(c)`

with the condition

```if (!c) {
goto L
}```

Then the assertions are true in all executions if and only if program never reaches location . QED