fmsd12

Seyster/Dixit/Huang/Grosu/Havelund/Smolka/Stoller/Zadok.

InterAspect: Aspect-Oriented Instrumentation with GCC.*

J. Seyster, K. Dixit, X. Huang, R. Grosu, K. Havelund, S.A. Smolka, S.D. Stoller, E. Zadok.

 

We present the InterAspect instrumentation framework for GCC, a widely used compiler infrastructure. The addition of plug-in support in the latest release of GCC makes it an attractive platform for runtime instrumentation, as GCC plug-ins can directly add instrumentation by transforming the compiler’s intermediate representation. Such transformations, however, require expert knowledge of GCC internals. InterAspect addresses this situation by allowing instrumentation plug-ins to be developed using the familiar vocabulary of Aspect-Oriented Programming: pointcuts, join points, and advice functions. Moreover, InterAspect uses specific information about each join point in a pointcut, possibly including results of static analysis, to support powerful customized instrumentation. We describe the InterAspect API and present several examples that illustrate its practical utility as a runtime-verification platform. We also introduce a tracecut system that uses InterAspect to construct program monitors that are formally specified as regular expressions.

 

To appear in FMSD'12, Formal Methods in Systems Design, 2012, Springer.

*This work was partially supported by the NSF Expeditions Award CNS-09-26190, the and the AFOSR FA-0550-09-1-0481 Award.