Modified Condition/Decision Coverage in the GNU Compiler Collection

TL;DR

The paper presents a language-agnostic approach to Modified Condition/Decision Coverage (MC/DC) in GCC 14 by treating Boolean expressions as Binary Decision Diagrams (BDDs) embedded in the control-flow graph. It introduces an offline masking-table computation on reduced, ordered BDDs and uses a bitset-based runtime to record independently contributing conditions, enabling efficient instrumentation across languages. The implementation demonstrates MC/DC support for C, C++, D, and Rust, highlighting the CFG-based, language-agnostic pipeline and its scalability through fixed-size bitsets. Limitations include a 64-bit cap on the number of basic conditions and reliance on front-end CFGs that reflect BDD structure, with future work aiming to relax bitset size and support additional MC/DC forms.

Abstract

We describe the implementation of the masking Modified Condition/Decision Coverage (MC/DC) support in GCC 14, a powerful structural coverage metric with wide industry adoption for safety critical applications. By analyzing the structure of Boolean expressions with Binary Decision Diagrams we can observe the key property of MC/DC, the power to independently affect the outcome, and map to the edges of the Control Flow Graph. This mapping can be translated to a few bitwise instructions and enables GCC to instrument programs to efficiently observe and record when conditions have been taken and have an independent effect on the outcome of a decision. By analyzing the BDD rather than the program syntax, GCC can measure MC/DC for almost all of its languages with a single language-agnostic implementation, including support for C, C++, D, and Rust.

Figures (8)

• Figure 1: \ref{['fig:truth-table:1']} is the truth table for the Boolean operators. \ref{['fig:truth-table:2']} and \ref{['fig:truth-table:3']} are the truth tables for $\lor$ in left-to-right and right-to-left evaluation order with conditions short circuited (*).
• Figure 2: $(x_1 \lor x_2)$ as a BDD. The regular edges make up the path for the given input vector. \ref{['fig:bdd:or:2']} demonstrates masking; changing $x_1$ does not change the decision ($1$).
• Figure 3: A Boolean function (\ref{['fig:bdd:pseudo-terminals:1']}) and its subexpression (\ref{['fig:bdd:pseudo-terminals:2']}). The terminals $x_4$ and $1$ in (\ref{['fig:bdd:pseudo-terminals:2']}) become pseudo-terminals in (\ref{['fig:bdd:pseudo-terminals:1']}). The masking effects in subexpressions will be preserved in the superexpression.
• Figure 4: $(x_1 \lor x_2 \lor x_3)$ and the short circuited (*) and masked (-) terms when a basic condition takes on 1.
• Figure 5: Two equivalent Boolean functions where a subexpression is computed outside the function. All edges from the subgraph $(x_2 \land x_2)$ go to $x_3$ and $1$, which are the successors $x_1x_2$.