Erweitern der Einsatzmöglichkeiten von automatisch generierten und vom Programmierer definierten Zusicherungen

BearbeiterIn:Tobias Stoll
Titel:Erweitern der Einsatzmöglichkeiten von automatisch generierten und vom Programmierer definierten Zusicherungen
Betreuer:Veldema, R.; Philippsen, M.
Status:abgeschlossen am 18. Mai 2005

However good a programmer is, he will make bugs. Good programmers know this about themselves and therefore write large numbers of consistency checks in their programs. C, C++ and Java have a standardized mechanism to aid the programmer write these checks: the assert statement or macro.

The syntax of the assert statement is usually: "assert(condition)" where the program will abort if the condition evaluates to false at that position in the program. Looking at the semantics above, there is one glaring problem: the assert is ONLY checked at that position in the source code. If a few statements later the assertion is violated, the bug is not caught.

Our proposal is to 1) make the assert statement a first class citizen in the compiler. 2) fully automatically propagate the assert statement, from statement to statement.

This opens up two possibilities: 1) as the assert is now a normal compiler entity in all compiler passes, we can use the extra, programmer supplied programmer information to aid in the program's optimization process and 2) we can perform better static analysises to see if at compile time the assertion is valid everywhere, over all control flow paths.

Another thing a compiler can then do is to automatically insert assert statements whenever some knowledge is discovered. For example whenever an if statement is executed, we can insert an assert that the if-condition is true in the if-part and an inverted assert statement in the else-part. Another example: after an for statement "(i=0;i<10;i++)", the loop-counter will equal 10, and we can insert an assert(i == 10); If in the loop an array bounds check for array 'X" was executed we can additionally add an assert(X.length >= 10); Whenever we then later 'see' a bounds check in a loop with an associated assert that the index is large enough, we can remove the bounds check. Or if we see a loop to array.length and we know the array length to be 10 as an propagated assert tells us so, we can better decide if loop-unrolling will be usefull. etc. etc. etc.

A small example:
assert(a != null);
assert(a.length > 10);
assert(P == 10);
assert(P < a.length);
assert(a instance of int[]);
for (int i=0; i smallerthan P; i++) {
if (a == null) throw
if (a.length < i) throwboundscheck();
a[i] = expr((int[])a);

Here, any cast-checks, bounds checks and null pointer checks can be removed as the assertions allow us to.


Extend the backend of the Jackal compiler (LASM) to support assertions as first class citizens. Therefore, extend the C/C++/Java frontend to generate intermediate code for assert() instead of making them macros/front-end only. Generate a compiler pass that propagates the assertions and use them for 1) program verification and 2) to create some small optimizations to use the assertions (e.g. if-statement and cast/bounds check removal).

watermark seal