Lecture Notes on Static Analysis.pdf

1 Introduction

There are many interesting questions that can be asked about a given program:

Other questions concern individual program points in the source code:

existence of an analyzer that decides if a variable in a program has a constant

value. We could exploit this analyzer to also decide the halting problem by

using as input the program:

Here x has a constant value if and only if the j’th Turing machine halts on

empty input.

such properties but rather to solve practical problems like making the program

run faster or use less space, or finding bugs in the program. The solution is

may only answer yes if the variable really is a constant and must answer no if

the variable may or may not be a constant. The trivial solution is of course to

answer no all the time, so we are facing the engineering challenge of answering

point? If our intended application is to replace *p with x in order to save a

dereference operation, then the analysis may only answer “&x” if p certainly

must point to x and must answer “?” if this is false or the answer cannot be

determined. If our intended application is instead to determine the maximal size

of *p, then the analysis must reply with a possibly too large set {&x,&y,&z,...}

which may be viewed as a weak form of program verification. As a case in

point, consider programming with pointers in the C language. This is fraught

with dangers such as null dereferences, dangling pointers, leaking memory, and

unintended aliases. The standard compiler technology, based on type checking,

offers little protection from pointer errors. Consider the following small program

which performs every kind of error:

The standard tools such as gcc -Wall and lint detect no errors. If we had

even approximative answers to questions about null values and pointer targets,

then many of the above errors could be caught.

2 A Tiny Example Language

We use a tiny imperative programming language, called TIP, throughout the

The input expression reads an integer from the input stream. The comparison

operators yield 0 for false and 1 for true. Pointer expressions will be added later.

The simple statements are familiar: