[llvm-cov][MC/DC][Qualification] Boolean Terms with XOR are not analyzed correctly for MCDC coverage

[escherle-validas]

Boolean Terms with XOR are not analyzed correctly for MCDC coverage

Criticality: HIGH

During qualification of MCDC coverage at Validas we found that
In the following example the term “(v0^v1) && v2” is not analyzed correctly.
the exclusive operator ^ takes two boolean inputs and produces a boolean output.
Therefore it has to be instrumented as well such that the impact from v0 to the result can be analyzed.
This results in a wrongly calculated MCDC coverage measured by LLVMCov.
Note: In plain C there is no native boolean type defined, therefore instrumentation is restricted to && and ||,
but for C++ and Rust the boolean type exists and therefore operators on it should be considered for MCDC coverage.
The problem occurs within Rust and C++.

Rust example:

Source Code and generated reports:
Test_000009.zip

C++ example:

Source Code and generated reports:
Test_000009.zip

[escherle-validas]

Since we have no reply from you yet, I would like to ask for a status update for this issue. Are there any plans how this will be handled?

[evodius96]

This issue, along with #109950 ("!=") and #109947 ("=="), will involve some research. I know some tools instrument XOR operator when the types are boolean, but I'm not sure about the others ("!=", "==") or if these are simplistic. For example, what does LDRA do for each of these?

cc. @Lambdaris, @chapuni Thoughts?

[Lambdaris]

Sorry for delay I was waiting for LDRA access.

LDRA looks like it does not think !=, ==, | or ^ are logical operations.

Here is LDRA's analysis for (a != b) || c

and (a | b) || (c ^ b)

Besides LDRA treats constants as our --mcdc-exclude=none thus all constants are counted.

Personally I think such operations are different from && and || because it is self-evident that any operands can affect the output independently. Hence as long as we could prove the whole expressions including == or != or ^ or | can affect output of the decision independently, we know the indivisible expressions could too.

So it seems that we could not get remarkable benefit from supporting breaking such conditions, for certification practice (at least LDRA proves it's not essential for those security critical certifications) or theoretical proof.

But I'd still wait for more insights.