Fork me on GitHub

TypeChef

TypeChef is a research project with the goal of analyzing ifdef variability in C code with the goal of finding variability-induced bugs in large-scale real-world systems, such as the Linux kernel with several thousand features (or configuration options).

Instead of analyzing each variant for each feature combination in isolation, TypeChef parses the entire source code containing all variability in a variability-aware fashion without preprocessing. The resulting abstract syntax tree contains the variability in form of choice nodes. Eventually, a variability-aware type system performs type checking on these trees, variability-aware data-flow analysis performs data-flow analysis and so forth.

TypeChef was started with the goal of building a type system for C code with compile-time configurations. TypeChef was originally short for Type Checking Ifdef Variability. Over time it has grown into an infrastructure of all kinds of analyses. In all cases, the goal is to detect errors in all possible feature combinations, without resorting to a brute-force approach.

TypeChef Poster

Architecture and Subprojects

The TypeChef project contains of four main components and several helper libraries.

Installation and Usage

For simple experimentation, try our online version.

Alternatively, you can download a .jar file including all necessary libraries TypeChef.jar. Run as usual

java -jar TypeChef.jar ...

TypeChef is also available as a maven repository. With sbt you can include TypeChef with the following line:

scala libraryDependencies += "de.fosd.typechef" %% "frontend" % "0.3.4"

To build TypeChef from source, we use sbt. Install git and download and compile the code as follows

git clone git://github.com/ckaestne/TypeChef.git
cd TypeChef
java -Xmx512M -Xss10m -jar sbt-launch.jar clean update compile

Due to library dependencies, setting up the TypeChef classpath can be difficult. There are two convenient mechanisms: Use sbt assembly to build a single jar file. Alternatively, call sbt mkrun to create a script typechef.sh that sets a correct classpath.

Most functionality of TypeChef is accessible through parameters of the main de.fosd.typechef.Frontend class. Call TypeChef with --help to see a list of configuration parameters. See also Parameter.txt. You will need to set up system include paths with -I and a header file with the compiler’s macro definitions with -h (generate, for example, with echo - | gcc -dM - -E -std=gnu99 for gcc). Have a look at existing projects using TypeChef or contact us in case of questions.

IntelliJ Idea users should run sbt gen-idea to create corresponding project and classpath information for the IDE. Similar sbt plugins for Eclipse are available, but we have not tried or integrated them yet. In general avoid to set the classpath in IDEs manually, but let sbt generate corresponding files for you.

Evaluation

Details on our syntax analysis of Linux have been published in an OOPSLA paper (see below). You find additional information on that evaluation at http://www.mathematik.uni-marburg.de/~kaestner/TypeChef/

Details of the type checking and linker checking of Busybox were publishing in an subsequent OOPSLA paper (see below).

The implementation of the data-flow analysis has been evaluated in two case studies (BusyBox and Linux) and the result of this evaluation is available from http://fosd.net/vaa

The setups for running TypeChef on these projects are available as separate github projects, for example:

Credits

The project was only possible with fruitful collaboration of many researchers.

The variability-aware lexer is implemented on top of jcpp, an implementation of the C preprocessor in Java. An alternative based on xtc/superc is included experimentally as well.

For reasoning about propositional formulas, we use the SAT solver sat4j.

The GNU C parser is based on an ANTLR grammar for GNU C.

The Java parser is based on a grammar that can be traced back to the Java 1.5 grammar in the JavaCC repository.

Experimentally, the Xtc/SuperC parser is included as .jar file to provide an alternative lexer.

For convenience, we include a binary of sbt in the repository.

This work was supported in part by the European Research Council, grant #203099.

Contributing

Fork the project, write bug reports, contact us, …. We are open for collaborations and extensions and other scenarios.

Publications

An indepth discussion of the parsing approach and our experience with parsing Linux was published at OOPSLA 2011:

Christian Kaestner, Paolo G. Giarrusso, Tillmann Rendel, Sebastian Erdweg, Klaus Ostermann, and Thorsten Berger. Variability-Aware Parsing in the Presence of Lexical Macros and Conditional Compilation. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (Portland, OR), New York, NY, October 2011. ACM Press.

In the context of a variability-aware module system, we discussed type checking and linker checks on the example of Busybox, published at OOPSLA 2012:

Christian Kästner, Klaus Ostermann, and Sebastian Erdweg. A Variability-Aware Module System. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 773–792, New York, NY: ACM Press, October 2012.

A description of how we scaled type system and data-flow analysis and a performance comparison with sampling strategies can be found here:

J. Liebig, A. von Rhein, C. Kästner, S. Apel, J. Dörre, and C. Lengauer. Scalable Analysis of Variable Software. In Proceedings of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), New York, NY: ACM Press, August 2013.

A more detailed discussion of the variability-aware lexer (or partial preprocessor) was presented at VaMoS 2011:

Christian Kästner, Paolo G. Giarrusso, and Klaus Ostermann. Partial Preprocessing C Code for Variability Analysis. In Proceedings of the Fifth International Workshop on Variability Modelling of Software-intensive Systems (VaMoS) (Namur, Belgium), pages 137-140, New York, NY, USA, January 2011. ACM Press.

A simple variability-aware interpreter for executing test cases was build on top of TypeChef and published at FOSD 2012:

C. Kästner, A. von Rhein, S. Erdweg, J. Pusch, S. Apel, T. Rendel, and K. Ostermann. Toward Variability-Aware Testing. In Proceedings of the 4th International Workshop on Feature-Oriented Software Development (FOSD), pages 1–8, New York, NY: ACM Press, September 2012.

For an overview of variability-aware analysis in general, please refer to the a technical report on the following webpage http://fosd.net/spl-strategies and the following reports:

T. Thüm, S. Apel, C. Kästner, M. Kuhlemann, I. Schaefer, and G. Saake. Analysis Strategies for Software Product Lines. Technical Report FIN-2012-04, Magdeburg, Germany: University of Magdeburg, April 2012.

A. von Rhein, S. Apel, C. Kästner, T. Thüm, and I. Schaefer. The PLA Model: On the Combination of Product-Line Analyses. In Proceedings of the 7th Int’l Workshop on Variability Modelling of Software-Intensive Systems (VaMoS), pages 14:1–14:8, New York, NY: ACM Press, January 2013.

Finally, an early overview of the project with a very preliminary implementation (now terribly outdated and superseeded by the papers above) was published at

Andy Kenner, Christian Kästner, Steffen Haase, and Thomas Leich. TypeChef: Toward Type Checking #ifdef Variability in C. In Proceedings of the Second Workshop on Feature-Oriented Software Development (FOSD) (Eindhoven, The Netherlands), pages 25-32, New York, NY, USA, October 2010. ACM Press.

Change Log

License

TypeChef is published as open source under LGPL 3.0. See LICENSE.

Download

You can download this project in either zip or tar formats.

You can also clone the project with Git by running:

$ git clone git://github.com/ckaestne/TypeChef