Introduction

What is a Program? §1.1

To talk about program analysis, we first have to define what we mean when we say program. A program, in the context of this course, is an object from a language that, when executed in a machine, produces some behaviour.

When executing a program, we state with an initial state, then we often want to run the step function it until it no longer changes the state. This is called a fixpoint, or running the program to completion. The sequence of states visited by the program is called a Trace.

What is Program Analysis? §1.2

Program analysis is the art of extracting facts about the structure or possible behavior of a program. These facts could include does the program eventually come to a halt, is the program well-formatted, or will my program exhibit a bug? In this course, we are going to investigate multiple approaches to answer these questions, ranging from manual to automatic, from syntactic to semantic, and from dynamic to static.

In summary, program analysis is:

Using automatic techniques to figure out facts about a computer program.

For simple languages, it is relatively easy to figure out what they do. For example, 1 + 2 will always execute to 3. But program analysis in general is extremely hard.

A Turing-Complete Mess §1.3

We are going to focus most of our energy on programs from languages that are Turing complete. Turing complete languages are languages in which you can write any program executable on a machine. This class of programs is also what you are mostly familiar with. Java, C, Python, etc. are all Turing complete languages. Even Brainfuck and PowerPoint are Turing complete.

Using a Turing-complete language is a double-edged sword: while it is nice that it is powerful enough to do everything, it is also powerful enough to:

• fire the missiles,

• not fire the missiles,

• never terminate,

• kill grandma, and worst of all

• throw a null pointer exception!

So it would be nice to be warned if any of these things might happen. However, that turns out to be very hard.

The Halting problem §1.4

Consider the mother of all analysis problems, the halting problem:

This problem turns out to be impossible to solve correctly for all programs of a Turing-complete language. It is, in fact, undecidable. While it is easy to say with confidence that some programs do terminate, we cannot build a mechanical procedure which can do this for every program.

The argument goes a little like this. Suppose you have a mechanical procedure for solving the halting problem; in that case, we can encode it as a program:

def does_halt(p : Program) -> bool:
    # A program returns true if p halts

Now we can use this program in another program:

def main():
    while does_halt(main):
        print("Running")

This is a weird program. We can see that if main halts, it runs forever, and if it runs forever it will eventually halt. This is of course impossible, which strongly suggests that does_halt cannot exist.

General Undecidability of Program Analysis §1.5

We could hope that the problem of determining whether a program terminates is special and does not affect other properties we would like to know about the program. But, sadly, this is not the case. Almost any non-trivial property you would like to know about the behavior of a program can be reduced to the halting problem. This fact is called Rice's theorem.

For example, since figuring out the halting problem is impossible, we can't say if the following problem actually fires the nukes:

def main():
    something_that_might_go_forever()
    fire_the_nukes()

Sound or Complete... Choose one. §1.6

There is hope, however. In most cases, you either care that something may happen, or that it must happen. In the program from before, we can quite easily say that it may fire the nukes. If we do not want the nukes to fire, we can flag this as a bug. However, we might also build a missile launcher, in which case the nukes must be fired when you press the red button.

These kinds of analyses allow us to err on one side. Here we borrow some nomenclature from logic. Essentially, the problem is that not everything we can prove is true, and not everything that we can't prove is false. To differentiate between proveable things and true things, use the notation $⊢$ (provable) and $\models$ (true):

In logic soundness means that every provable statement is true, and completeness means that every true statement is provable.

The dual of soundness is completeness:

Translated into program analysis jargon, we say an analysis is sound if, when it produces a fact, then that is a true fact about the program. Furthermore, we say an analysis is complete if it can always find a fact about the program if one exists. Because the problem we are talking about is undecidable, we can't both be sound and complete.

It is also useful to talk about how a program analysis has performed on individual programs or bugs. To do this we use nomenclature from classification.

A sound analysis, therefore, has no false positives, and a complete analysis has no false negatives.

A Relaxed Goal §1.7

Actually, it turns out that in most real-world language settings, it is very hard to write analyses that are sound. So in this course, instead of working with trivial programs, we relax the goal, and instead of requiring our analyses to be sound or complete, we aim to produce the best result in the shortest amount of time.

[...], virtually all published wholeprogram analyses are unsound and omit conservative handling of common language features when applied to real programming languages.

— In Defense of Soundiness: A Manifesto

To this end, in our course we are going to see every analysis as a classifier, which should not only report facts but also how confident that the facts are true.

Manual vs Automatic Analysis §2.1

The difference between manual and automatic analysis is whether we have a well-defined procedure for analyzing the code.

In many cases, manual inspection is a crucial companion to automatic analysis. If taken to the extreme, we can actually require the user of the tool to prove to us that the code is correct. Now we only have to check the proof, in which case we are entering the world of Program Verification.

Syntactic vs Semantic Analysis §2.2

The difference between syntactic and semantic analysis is whether we focus on the structure of the program or on the meaning of the program. The structure of the program, or syntax, is often represented as a tree of nodes as recognized by the parser. In contrast, the meaning of the program, or semantics, is represented as a set of all possible traces of a program. Here, a trace means a sequence of states and operations possible by the program.

Dynamic vs Static Analysis §2.3

Finally, we can differentiate between dynamic and static analysis. A dynamic analysis infers the meaning of the program from a single trace, whereas a static analysis tries to predict all possible behaviors.

Dynamic analysis is often just executing the programs, and then reporting any behavior it exhibits. A dynamic analysis often provides proof of the bad behavior. A dynamic analysis is sound if every behavior it finds is a real behavior, and complete if it can find all behaviors.

Static analyses, in contrast, consider the entire program and then report if the program is without bugs or problems. When a good static analysis says your program is good, it probably is; however, when it finds a potential bug, it often cannot prove it to you. A static analysis is sound if every program it flags exhibits some behavior, and complete if it flags all programs that contain the behavior.

It is sometimes a great idea to do a mix of dynamic and static analysis, in which case we call it a hybrid analysis.

The JPAMB §3.1

In this course, we are going to build the best analysis that we can for the JPAMB suite. The goal of the game is to write analysis which can score the highest, and do that in the shortest amount of time.

$ git clone https://github.com/kalhauge/jpamb.git

The Key Idea §3.2

The goal is to build the best program analysis, of small Java methods. You are measured on performance, and on accuracy of prediction. Here is an example:

@Case("(false) -> assertion error")
@Case("(true) -> ok")
public static void assertBoolean(boolean shouldFail) {
    assert shouldFail;
}

The cases above the are examples of inputs that produce different outcomes or behaviors in the method. For example false makes the method raise an Assertion Error, while true makes the method finish normally.

The goal is now to report what you think is possible behavior of the method, given any input, as well as how confident you are. The perfect solution would be:

assertion error;100% # I'm totally sure this happens
ok;100%
<the-others>;0% # I'm totally sure this never happens. 

In practice, due to Rice ' Theorem, there is no perfect solution, so we have to hedge our bets, and lower our confidence. Finding the perfect confidence level is hard so we have added a category system, which allows you to simply group predictions:

assertion error;yes # I think this happens
ok;maybe # This might happen, I don't know
<the-others>;no # I think this does not happen

Each category is then replaced by the percentage that categorized behaviors can be emitted across all methods in the benchmark suite. You can use any combination of letters to create your categories.

$ jpamb -vv analyse syntactic-regex

for q in jpamb.QUERIES:
    if q != "assertion error":
        print(f"{q};skip")

divide_or_end = re.search(r"/|(^\s*})", rest, re.MULTILINE)

if not divide_or_end:
    log.error("Could not find end of method or divide")
    log.error(rest)
    sys.exit(1)

log.debug(f"found divide {divide_or_end}")
divide_found = divide_or_end.group(0) == "/"

if divide_found:
    log.debug("Found divide")
    print("divide by zero;found-div")
else:
    log.debug("No divide")
    print("divide by zero;not-found-div")

for q in jpamb.QUERIES:
    if q != "assertion error" and q != "divide by zero":
        print(f"{q};skip")

jpamb -vv analyse syntactic-regex