(c) 2013 Galois, Inc.

Author: Erlend Hamberg and Lee Pike (leepike@galois.com)

Overview

This package generates run-time monitors for C/C++ programs compiled via GCC. The user adds an instrumented attribute to global variables to be monitored. A GCC plugin automatically instruments every occurrence in the program in which the variables are updated to save the variable's value. Thus, a stream of variable values is generated. The user can then write temporal properties over the streams of variables to check properties of the variables on-line.

Installing

Install the GCC plugin:

> cd GCC-Plugin
> make
> make test

This should result in some sample output from an instrumented program. Read gcc-plugin/README.md for more information about building and testing the plugin.

For cross-compilers, the plugin can be generated with a compiler on the host platform, but compilation must (1) be 32-bit if the cross-compiler is 32-bit, and (2) compile as C++ if cross-compilation is C++. Adjust the definitions of the compiler appropriately in the Makefile (e.g., gcc, g++, etc.). To compile as 32-bit, do

> make EXPLICIT32=1

After building and confirming the plugin works, do

> cd rtv-lib; cabal install

To install the Haskell package that depends on the plugin.

Usage

In rtv-example is a toy example using the framework. This will show a simple example of how to declare global variables to be instrumented so that GCC automatically records their history. Then, the values taken by the variables can be checked off-line or by a separate process.

The example contains hand-written and auto-generated C. To generate the example, do something like the following:

bash ../../rtv-lib/build-tools/find-instrumented.sh ./ > instrumented-decls
cabal install
./LOCATION_OF_CABAL_EXECS/bin/rtv-example
make

find-instrumented.sh greps C sources recursively from the directory provided for a file that contains global declarations like

int a __attribute__((instrument(0))) = 1;

The results are placed into the file instrumented-decls, which is assumed to exist in the current directory. The contents of instrumented-decls are parsed and used by Template Haskell to generate Haskell code implementing correctly-typed setter and getter functions at compile-time. The declarations are assumed to not require pre-processing, and there is lightweight parsing of the declarations, which may be broken with other specifiers. The user can manually put post-processed declarations in an instrumented-decls file.

The Template Haskell splices are generated by calling gettersAndHist from the rtv-lib package. See examples/PropertiesExamples.hs for an example.

After building the package, executing it should generate an out directory containing C sources and headers generated by the runtime verification system:

• out/instrumented.c: For each variable, generates an API for storing and retrieving variable values.

• out/ivory.h: Ivory is the C code generator used, which is a Haskell EDSL. This is the standard lib for Ivory.

• out/runtime-checker.c: The property checker generated. Properties are specified in examples/PropertiesExamples.hs using temporal operators. The interface to check the conjunction of all generated properties is check_properties(). In our case, we are checking if instrumented variable 0 (a) is always less than or equal to instrumented variable 1 (b).

In example/ are hand-written C files:

• example/checker_task.c: This specifies what to do if runtime checks fail, which is application specific.

• example/record_assignment.c: This specifies what should be done whenever a variable that contains an instrument attribute is updated. The user writes a function with the signature

  void record_assignment(int var_id, void* value)

  That takes the identifier of a variable (the argument to the instrument attribute) and the value before the variable is reassigned. What is done is implementation-specific. (In our RTOS implementation, the value is sent to a checker task on a channel, and the checker task stores it.) In this example, we'll simply make a call append_to_history, defined in instrumented.c.

• example/monitored_task.c: This is the program we're monitoring. GCC will automatically instrument each location in which a global variable that has an instrument attribute is updated with a call to record_assignment(). Note that we currently don't do pointer analysis, so it is possible to change a variable's value without GCC instrumenting it. If you look at the executable in function update, you should see the call; e.g.:

  400642:       e8 29 00 00 00          callq  400670 <record_assignment>
  400647:       89 1d f7 09 20 00       mov    %ebx,0x2009f7(%rip)
  

Current Limitations/Future Work

• No pointer-analysis is done, so if GCC can not figure out that the variable is being modified, no record_assignment() call will be inserted.

• While record_assignment() is relatively cheap, if a variable is updated frequently in a tight loop, exceptional overhead will be added to the program.

• Struct and array monitoring are not supported, only base types.

• We grep instrumented attributes from sources and do lightweight parsing. We assume no pre-processing is needed and some modifiers may break the parser. Please report bugs in parsing.