GNU Cauldron 2012, Prague, talk14: Part 2/2

Control-flow preservation in GCC for safety-critical uses

Presenter: Olivier Hainque

The proposed presentation is about the introduction of a "-fpreserve-control-flow" option in GCC, which directs the compiler operations so that the control-flow expressed in a source persists in the generated assembly code.

The interest is twofold: Facilitate source to object traceability analysis, sometimes required as part of safety critical certification processes Allow non-intrusive coverage analysis using an instrumented execution environment instead of program instrumentation, also attractive in certification contexts Beyond traceability analysis requirements, control flow preservation is key to support the non-intrusive analysis of coverage criteria that care about source boolean expressions and their operands, such as the "Decision" or "MCDC" coverage metrics in the avionics certification area (DO178-B standard).

The basic idea is to allow inferring which values were taken by boolean operands or expressions from information on the execution flow at the corresponding machine branch points (provided by the instrumented execution environment). Very roughly, we need the relevant branches to remain there and accurate enough debug info to map them to source expressions in presence of arbitrarily complex constructs, which poses a few challenges to solve in the compiler.

At this point, we have a stable implementation in our local gcc 4.5 series, supporting optimizations up to -O1. We use this to offer a non-intrusive coverage analysis framework, using valgrind or qemu as virtual execution environments instrumented to produce execution traces.

We are about to port this to gcc 4.7 and would be happy to contribute to mainline after exchanging with other developers on the approach.

The presentation will include an introduction to the major motivations for this work general implementation scheme challenges encountered and resolutions current status & results future plans

• Category

  Science & Technology