linux v2.4.1 experiment

using mygcc

introduction

This directory contains an experiment consisting in applying mygcc to retrieve over 100 already reported bugs in Linux v2.4.1.
These bugs were originally detected using a much more complex, never distributed, C checker called MC, that later evolved as a commercial product. The list of bugs detected by MC is available as an on-line bug database.

To validate mygcc, we chose three checkers used by MC (called NULL, FREE, and BLOCK), rewrote them as constrained reachability properties, and checked 89 among the  concerned C files.

results

The short story is that mygcc found all the bugs except only 4, introduced only 2 false positives (= false errors), and found 4 new, unknown bugs. This demonstrates that simple reachability properties are sufficient to detect many useful bugs.

You may browse the results, and compare them with MC's database. The results contain one *.check file for each C file that was checked, containing all mygcc messages. Every user-check message contains the name of the C file, the name of the function that failed a user check, and the buggy statement.

Note: As mygcc works on a simplified AST internal to gcc called Gimple, the buggy statement may look different from the source statement, because complex sub-expressions have been replaced by temporary variables. We are working on printing the buggy statement in its original source form.

contents

The contents of the directory is as follows:

• All the checks are contained in a single file: mc.crc.

• The checks are driven by the Makefile.

• There are two simple Awk scripts performing simple pre-processing of the C files: chfun.awk and protect-multiline-strings.awk. These scripts are used by the Makefile, you do not have to call them directly.

• The ref/ directory contains the results.

running

To run the tests yourself, you need a Linux/x86 machine. Perform the following steps:

• download Linux v2.4.1 sources, from an appropriate site and uncompress them on your site in directory $LINUX of your choice

• download mygcc version 0.1.0 and uncompress it on your site in directory $MYGCC of your choice
  Note: do not try to reproduce the examples with a more recent version of mygcc, because kernel v2.4.1 does not compile with any recent gcc version.

• download libdlcheck.so to a directory of your choice, and add that directory to the environment variable LD_LIBRARY_PATH

• customize the first two definitions in $MYGCC/ex/linux/2.4.1/Makefile to point to $LINUX and $MYGCC respectively

• cd $MYGCC/ex/linux/2.4.1/

• make

Running the tests will create, for each C file called "f.c", the following files:

• f.i: the C file after cpp

• f.i.c: the f.i file after our simple pre-processing using the two Awk scripts

• f.i.c.t09.gimple: the simplified AST form on which checks are performed

• f.i.c.check: the log of running mygcc on f.i.c

• f.i.o: the compiled object file (recall that mygcc is an extensible gcc version, so it generates object code as usual)

After that, you might want to compare your results with the reference results in ref/.
Finally, you might want to erase all the produced files using "make clean".