Tracking implementation for MC/DC #124144
Comments
rustbot
added
the
needs-triage
|
@rustbot label +A-code-coverage |
rustbot
added
the
A-code-coverage
|
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. |
nit on the terminology, but I'd rather say that conditions are boolean expressions that have no logical operator. |
workingjubilee
added
the
T-compiler
|
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). |
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. |
|
Upon implementing mcdc for pattern match, I found that decisions here might be confusing. |
|
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
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. 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. |
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 |
Good idea, |
|
I have a few cleanup steps planned for after #123409/#124255:
|
…ons, r=oli-obk MCDC coverage: support nested decision coverage rust-lang#123409 provided the initial MCDC coverage implementation. As referenced in rust-lang#124144, it does not currently support "nested" decisions, like the following example : ```rust fn nested_if_in_condition(a: bool, b: bool, c: bool) { if a && if b || c { true } else { false } { say("yes"); } else { say("no"); } } ``` Note that there is an if-expression (`if b || c ...`) embedded inside a boolean expression in the decision of an outer if-expression. This PR proposes a workaround for this cases, by introducing a Decision context stack, and by handing several `temporary condition bitmaps` instead of just one. When instrumenting boolean expressions, if the current node is a leaf condition (i.e. not a `||`/`&&` logical operator nor a `!` not operator), we insert a new decision context, such that if there are more boolean expressions inside the condition, they are handled as separate expressions. On the codegen LLVM side, we allocate as many `temp_cond_bitmap`s as necessary to handle the maximum encountered decision depth.
…ons, r=Zalathar MCDC coverage: support nested decision coverage rust-lang#123409 provided the initial MCDC coverage implementation. As referenced in rust-lang#124144, it does not currently support "nested" decisions, like the following example : ```rust fn nested_if_in_condition(a: bool, b: bool, c: bool) { if a && if b || c { true } else { false } { say("yes"); } else { say("no"); } } ``` Note that there is an if-expression (`if b || c ...`) embedded inside a boolean expression in the decision of an outer if-expression. This PR proposes a workaround for this cases, by introducing a Decision context stack, and by handing several `temporary condition bitmaps` instead of just one. When instrumenting boolean expressions, if the current node is a leaf condition (i.e. not a `||`/`&&` logical operator nor a `!` not operator), we insert a new decision context, such that if there are more boolean expressions inside the condition, they are handled as separate expressions. On the codegen LLVM side, we allocate as many `temp_cond_bitmap`s as necessary to handle the maximum encountered decision depth.
saethlin
removed
the
needs-triage
|
Nested decisions might lead to unexpected results due to sorting mappings happened in llvm. See this patch to llvm for details. Let-chains for pattern matching is affected by this most. |
|
We treat decisions with only one condition as normal branches now, because mcdc won't give different results from normal branch coverage on such cases. |
|
I should write something to clarify thoughts on designing mcdc for pattern matching in case someone felt confused about the behaviors. Coverage results of pattern conditions seems to be wrong/unexpected. match tuple {
(A(Some(_)), B | C) => { /*...*/ },
(B | C, A(_)) => { /*...*/ },
(A(None), _) => { /*...*/ },
_ => { /*...*/ }
}rustc would check the first and the third arm first. The coverage results are derived from the actual control flow generated by the compiler, which might be not same as intuition.
|
I am not really convinced that this is something we want to do. In the 2-conditions case, even though the theorem proves it, I find it not trivial to understand that branch coverage implies MCDC. Moreover, in the context of MCDC, I tend to define decisions as boolean expressions composed of several conditions, so in that sense, we don't have to instrument 1-condition decisions by definition, while we still have to instrument decisions with 2+ conditions. At last, while we have historically never instrumented 1-condition decisions for successfully certified code, it may be harder to justify not instrumenting 2-cond. decisions to the certification authorities, even though, again, it is proved to be equivalent. Also, I don't feel like this will bring a consequent improvement for either runtime speed, or memory usage, compared to the gains of not instrumenting 1-cond., mostly because I think 1-cond decisions are the most frequently encountered. |
fmease
added
the
C-tracking-issue
|
We might need to make decisions about how to deal with constant folding. const CONSTANT_BOOL: bool = true;
fn foo(a: bool) {
if a && CONSTANT_BOOL {
/*...*/
}
}In such case llvm shows 100% coverage once But once if we changed I'd propose to eliminate these conditions and all other conditions effected by them from MCDC. That says,
And if a decision was always evaluated to solitary value, we remove it and transform its all conditions to normal branches. Let's request some nice insights. |
|
LLVM 19 has changed the start condition id from 1 to 0 at llvm #81257. This could break all mcdc tests once rustc upgraded its llvm backend. Since llvm 19 is still under development, I plan to deal with it when rust launches process to upgrade the backend . |
Sounds reasonable. Once the compiler switches over to LLVM 19, we might even want to stop supporting MC/DC on LLVM 18, to avoid the complexity of having to support big differences between 18 and 19. 🤔 |
I have several question regarding constant folding. First, when you say " In the case were Also, in the cases Nobody uses constants in decisions intentionnally, so we primarly need to think about generated code. One idea would be to write warning message saying something like "Condition X of the decision was resolved to constant False, this will make MCDC coverage impossible for conditions X,Y, Z". However, I am not really convinced by this approach, because this would introduce compilation "Warnings" that may be completely expected. The other idea would be to add metadata in the mappings, so that fn foo(a: bool) {
if a && false {
println!("success");
}
}One question that this arises, is how we consider "skipped" conditions. Do we account for them in the whole decision validation, or do we ignore them, and consider the decision is covered if all non-skipped conditions are covered ? Furthermore, the biggest downside of this solution is that is will probably involve a massive refactor of LLVM's ProfileData code. What do you think ? |
That's what I expect: constants are marked as "Folded" while all uncoverable conditions are noted. I've tried a bit on both rustc and llvm. It seems better to implement it on llvm side. Since in rust we know which conditions are folded after injecting statements, it's not elegant for rust to do these stuff. |
It's likely I don't understand the intricacies of constant folding in rust; given its unique use cases, ultimately you can handle these however you wish. However, I want to point out that in clang, we mark conditions that are constant folded so that they can be visualized for the user (both for branch coverage and MC/DC). In MC/DC, these constant folded conditions are excluded from measurement (as you know, they're uncoverable and therefore cannot have any independence pairs). However, a key distinction I want to make is that for MC/DC in clang, we actually do not fold the conditions (we disable this) and therefore we actually instrument the folded conditions in order to facilitate proper coverage of the other conditions in the decision. We have to do this to ensure we match the possible test vectors correctly. |
In my premature thoughts we can avoid remarkable divergences between rust and llvm. The changes I wish to make are:
This method does not invade instruments but only effects how llvm presents for users. For instance, suppose we have a decision With the scenario, we still have 4 mcdc branch mappings: After llvm-cov collects all test vectors, it can show practical test vectors by pick up whose folded conditions bits are expected. Say, in our example, only test vectors in this table are practical: (
As we see, the practical test vectors are whose bit for Next let's find which conditions are uncoverable or folded:
Briefly the scheme is:
I'm going to draft in this way hence not much of existed llvm code need to be refactored. Is it worth? (I've opened an issue on llvm llvm #93560, we can discuss the scheme there) |
|
Regarding Currently for #124278 I decide to treat each arm of // a: i32;
// val: enum Pat { A(i32), B }
match val {
Pat::A(f) if f == a => { /*...*/ }
Pat::A(1) if a > 0 => { /*...*/ }
_ => { /*...*/ }
}Now there are two decisions Then what result should us present to users? If we just ignore the latter arms, once the last arm is not wildcard, we can get a decision that never fails. Otherwise if we also record test vectors of the latter arms, it can show the weird result as above. cc @pietroalbini This may correspond to your paper. EDITIt seems that only update executed test vectors that records one arm and its all precede arms are more reasonable. Since it's true that there may be two or more candidates matching the value, we can not treat candidates as patterns joint with As a result, the last arm does not produce decision. That says, in // v: (Option<_>, Option<_>)
match v {
(Some(_), Some(_)) => say("both are some"),
(None, _) | (_, None) => say("at least one is none"),
}mcdc won't generate mappings for |
|
With the optimization to allow more conditions in a decision llvm has also introduces two options There are two hard limit as clang document describes:
The reason is trivial: llvm uses Still users can enforce stricter rules with First I'm not determined about how we name the option for Second I'm not very clear about how we process them as lints. The key difference is, we usually treat lints as something users should care about, while these options also control how the compiler work. It's a bit unusual to warn users or not based on compiler options. Instead a specified lint like |
This is the reason why I don't expose options to clang. (They are cc1options) "The number of test vectors" can be explained as; "The number of possible paths" or "The number of combinations of conditions". Would this be hint for you to name? |
|
Hmm, my instinct is to expose the “test vectors” knob directly, without trying to hide it for the user. It might seem less friendly to the user, but it's more honest. If we're actually limiting the number of test vectors, but hiding that behind a setting that claims to control something else, that might result in more confusion in the long run. But this is just an initial thought. |
Thanks for explanation! I want to discuss this question because I do not know what users more care about. I tried to replace
Good point. I was not aware that there might be more terms introduced in the future and making memory cost more undetermined. |
From a compiler user point of view (of MC/DC coverage measurement for safety-critical development): If you need to use MC/DC, you are well aware of terms like test vectors and condition combinations (since these are basic definitions to understand the coverage results). Please expose them in this way without further indirection :-). |
|
naively, "max-bitmap-mem" also implies some pretty hard bounds on memory usage, and people often get really fussy if you use even one byte more than they expect, whereas doing that might be sensible in many cases. |
Yeah, exhaustiveness checking ensures that the last arm catches all values that were not caught by another arm. In other words, a match like this: match foo {
<complicated pattern> => {}
<some other pattern> => {}
}is guaranteed to be the same (except bindings) as: match foo {
<complicated pattern> => {}
_ => {}
}which is also the same as: if let <complicated pattern> = foo {
} else {
}So a (By this reasoning, an irrefutable pattern such as |
Yeah, that's pretty much the conclusion I came to in #124154 when I was looking into branch coverage for |
[Coverage][MCDC] Adapt mcdc to llvm 19 Related issue: rust-lang#126672 Also finish task 4 at rust-lang#124144 [llvm rust-lang#82448](llvm/llvm-project#82448) has introduced some break changes into mcdc, causing incompatibility between llvm 18 and 19. This draft adapts to that change and gives up supporting for llvm-18.
|
We uploaded the preprint of the paper to arXiv: https://arxiv.org/abs/2409.08708 |
[Coverage][MCDC] Adapt mcdc to llvm 19 Related issue: rust-lang#126672 Also finish task 4 at rust-lang#124144 [llvm rust-lang#82448](llvm/llvm-project#82448) has introduced some break changes into mcdc, causing incompatibility between llvm 18 and 19. This draft adapts to that change and gives up supporting for llvm-18.
ZhuUx
changed the title
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 || bis not "condition" because it has an or operator whilea==bis.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
Here
(a || b) && cis a decision anda,b,care conditions.(a=true, b=false, c=true)and(a=false, b=false, c=true), we sayacan independently affect the decision because the value of decision is changed asachanges while keepbandcunchanged. So that we get 1/3 MC/DC here (1 foraand 3 fora,b,c).(a=false, b=true, c=true)and(a=false, b=false, c=false)also showbcan independently affect the decision. Though in the later casecis also changed but it is short-circuited and has no impacts (thus we can view it as same asc=true). Whilecis not acknowledged due to change ofb. Plus the two cases before we get 2/3 MC/DC.(a=true,b=false,c=true)and(a=true,b=false,c=false)showccan 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:
let val = a || b. Done atcoverage: Optionally instrument the RHS of lazy logical operators #125756
MCDC Coverage: instrument last boolean RHS operands from condition coverage #125766
Draft: Support mcdc analysis for pattern matching #124278
if (a || b) || inner_decision(c || d). Done at MCDC coverage: support nested decision coverage #124255[Coverage][MCDC] Adapt mcdc to llvm 19 #126733
Known Issue
The text was updated successfully, but these errors were encountered: