Tracking implementation for MC/DC

[ZhuUx]

View all comments

Introduction

Modified condition/decision coverage (MC/DC) is a code coverage criterion used widely in safety critical software components and is required by standards such as DO-178B and ISO26262.

Terminology
condition: boolean expressions that have no binary logical operators. For example, a || b is not "condition" because it has an or operator while a==b is.
decision: longest boolean expressions composed of conditions and binary boolean expressions only.

MC/DC requires each condition in a decision is shown to independently affect the outcome of the decision.
e.g Suppose we have code like

if (a || b) && c {
    todo!();
}

Here (a || b) && c is a decision and a,b,c are conditions.

• If test cases are (a=true, b=false, c=true) and (a=false, b=false, c=true), we say a can independently affect the decision because the value of decision is changed as a changes while keep b and c unchanged. So that we get 1/3 MC/DC here (1 for a and 3 for a,b,c).
• Test cases (a=false, b=true, c=true) and (a=false, b=false, c=false) also show b can independently affect the decision. Though in the later case c is also changed but it is short-circuited and has no impacts (thus we can view it as same as c=true). While c is not acknowledged due to change of b. Plus the two cases before we get 2/3 MC/DC.
• Test cases (a=true,b=false,c=true) and (a=true,b=false,c=false) show c can do the same. By now we get 3/3.

Notice that there are duplicate cases, so test cases collection {(a=true, b=false, c=true),(a=false, b=false, c=true),(a=false, b=true, c=true), (a=false, b=false, c=false),(a=true,b=false,c=false)} are sufficient to prove 3/3 MC/DC.
In fact we can use at least n+1 cases to prove 100% MC/DC of decision with n conditions. (In this example, {(a=true,b=false,c=true),(a=false,b=false,c=true),(a=false,b=true,c=true),(a=true,b=false,c=false)} are enough)

Progress

A basic implementation for MC/DC is filed on #123409 , which has some limits. There are still several cases need to handle:

• Support plain boolean expressions like let val = a || b. Done at
  coverage: Optionally instrument the RHS of lazy logical operators #125756
  MCDC Coverage: instrument last boolean RHS operands from condition coverage #125766
• Support pattern matching. Ferrous suggests that refutable patterns should be considered as decisions, which sounds certainly reasonable as these are considered as branches too.
  Draft: Support mcdc analysis for pattern matching #124278
• Support nested decisions like if (a || b) || inner_decision(c || d). Done at MCDC coverage: support nested decision coverage #124255
• So far only decisions with at most 6 conditions are counted due to resource cost. This limit should be relaxed now that the llvm backend had this optimization.
  [Coverage][MCDC] Adapt mcdc to llvm 19 #126733

Known Issues

• Decisions containing constant conditions may result incorrect report, where some non-constant conditions are regarded as constants or vice versa. This issue occurs because the way rustc produces counters for constants is not what llvm expects. It's fixed by llvm #112694 and can be solved once rustc upgraded in-tree llvm to 20.
• Some nested decisions may cause panic as llvm #91600 described.
• On some occasions rustc may painic with "instrprof failed to lower mcdc parameters", see [Coverage][MCDC] Do not initialize mcdc parameters for instances containing no mcdc statements #129989

[ZhuUx]

@rustbot label +A-code-coverage

[workingjubilee]

The tracking issue should probably include a (brief) definition of MCDC, as otherwise this is untrackable by anyone who does not already know what the issue is for.

[RenjiSann]

condition: boolean expressions that have no binary operators. For example, a || b is not "condition" because it has an or operator while a==b is.

nit on the terminology, but I'd rather say that conditions are boolean expressions that have no logical operator.
cf the BinOp and LogicalOp definitions.

[workingjubilee]

Excellent, that's much better, thank you! The teams every now and then review tracking issues and it is helpful if whoever is participating in the review can understand what the tracking issue is about without any domain expertise (even if only so they can fetch the appropriate subject-matter expert).

[ZhuUx]

nit on the terminology, but I'd rather say that conditions are boolean expressions that have no logical operator.

Thanks for correctness! I should have written "binary logical operators". It's a bit different with normal definition because I think treat conditions + unary operators as condition does not lead to different results in MC/DC.

[ZhuUx]

Upon implementing mcdc for pattern match, I found that decisions here might be confusing.
Consider pattern if let (A | B, C) = value, intuitively the decision here likes (matches(A) || matches(B)) && matches (C).
However, compiler will rearrange it and make its CFG look like matches (C) && (matches(A) || matches(B)) to reduce complexity.
This impacts mcdc analysis because the condition short-circuited is changed. We should find a way to determine the rearranged decision.

[RenjiSann]

I wonder how should let-chains be instrumented.

for example:

if let (A | B, C) = value && let Some(X | Y) = other && (x || y) {
}

Here, I can't decide whether we should insert 1 or 3 MCDC decision records here

• 3 decisions: 1 for each refutable pattern matching, and 1 for the top-level boolean expression
• 1 decision with

Maybe the 3 decisions would be better and easier to do, but I fear this would add a lot of verbosity to the report, and also increase the number of conditions in decisions, which therefore increase the complexity of the testing.

What do you think ?

[ZhuUx]

I wonder how should let-chains be instrumented.

for example:

if let (A | B, C) = value && let Some(X | Y) = other && (x || y) {
}

Here, I can't decide whether we should insert 1 or 3 MCDC decision records here

* 3 decisions: 1 for each refutable pattern matching, and 1 for the top-level boolean expression

* 1 decision with

Maybe the 3 decisions would be better and easier to do, but I fear this would add a lot of verbosity to the report, and also increase the number of conditions in decisions, which therefore increase the complexity of the testing.

What do you think ?

I'd tend to 3 decisions as it's more clear and easy to be implemented.
I have managed to construct decisions for refutable pattern matching and found it is very different with normal boolean expressions (eg. rustc does not promise evaluated order of pattern matching). Thus I'd rather view refutable pattern matching as something like try_extract_data_from(&mut bindings...) -> bool.

Besides, if we want to present consistent results in mcdc, we would better take all refutable pattern matching as decisions or not, otherwise we might face paradox like branch coverage in lazy expressions now.

[RenjiSann]

I'd tend to 3 decisions as it's more clear and easy to be implemented.
I have managed to construct decisions for refutable pattern matching and found it is very different with normal boolean expressions (eg. rustc does not promise evaluated order of pattern matching). Thus I'd rather view refutable pattern matching as something like try_extract_data_from(&mut bindings...) -> bool.

That makes sense, indeed. Let's go with this strategy then :)

Also, I think it would make sense to allow the user to disable pattern matching instrumentation if needed (for example to reduce the binary size if needed). Maybe we could do this with a flag -Z coverage-options=no-mcdc-in-pattern-matching (or smth shorter if possible).

[ZhuUx]

Maybe we could do this with a flag -Z coverage-options=no-mcdc-in-pattern-matching (or smth shorter if possible).

Good idea, -no-pattern-matching may be enough since normal branch coverage might also use this option and it is mutual exclusive with mcdc to some extent for now.