A C/C++ front end for the Daikon dynamic invariant detection system

This thesis details the implementation and performance of a Daikon front end for the C and C++ languages. The Daikon dynamic invariant detection suite is a system designed to extract formal specifications from programs, in the form of information about their variables and their relationships to each other. The system consists of a front end and the analysis engine. The front end instruments the source code of a target program, inserting code that outputs the values of the program's variables when run. The user compiles and runs the instrumented program, generating a trace file that contains variable values. This data is then sent to Daikon proper, which performs analysis on it and reports invariants about the program variables. Daikon is a useful tool that can discover invariants that current static methods cannot find. While the invariant analysis tool is language independent, the front ends -- tools that instrument of the user code -- must be written for every language to be instrumented. There is a huge base of pre-existing code written in C/C++ for which invariants can be discovered. C and C++ are also widely deployed, comprise a large segment of software currently in development, and are therefore valuable candidates for analysis. The key difficulty in instrumenting a type-unsafe language like C is that the instrumented program has to determine what variables are valid, and to what extent; so that it does not output garbage values or cause a segmentation fault by dereferencing an invalid pointer.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2002

Author dc:creator

• Morse, Benjamin, 1979-

Advisor dc:contributor.advisor

• Michael D. Ernst.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/29653

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/29653