# General

This document examines MC/DC Coverage from the perspective of code inspection, code instrumentation, information generation, and data structure usage.

The definitions of key terms in this document are taken from the "[A Practical Approach to Modified Condition/Decision Coverage](https://ntrs.nasa.gov/api/citations/20040086014/downloads/20040086014.pdf)" paper by Kelly Hayhurst and Dan Veerhusen.

From the paper:

* **Condition** – A Boolean expression containing no Boolean operators.
* **Decision** – A Boolean expression composed of conditions and zero or more Boolean operators. A decision without a Boolean operator is a condition. If a condition appears more than once in a decision, each occurrence is a distinct condition.
* **Modified Condition/Decision Coverage** – Every point of entry and exit in the program has been invoked at least once, every condition in a decision in the program has taken all possible outcomes at least once, every decision in the program has taken all possible outcomes at least once, and each condition in a decision has been shown to independently affect that decision’s outcome. A condition is shown to independently affect a decision’s outcome by varying just that condition while holding fixed all other possible conditions.

# Instrumentation

## Conditions and Decisions

An MC/DC tool starts by processing the source code of a program, looking for boolean expression subtrees (BES) at the syntactic level. A BES denotes a decision, while its leaves denote conditions. Note that a leaf could contain a BES of its own (for example, the leaf could be a function call which evaluates to a boolean, where one of its arguments is a decision), in which case this BES is considered a distinct decision.

Once such a BES is discovered, the MC/DC tool traverses the subtree from its root, and constructs a **Binary Decision Diagram** ([BDD](https://en.wikipedia.org/wiki/Binary_decision_diagram)). An entry in the BDD's truth table denotes a **test vector** - a set of values for all conditions of the decision. The BDD is analyzed to count the number of paths leading to an outcome, thus determining the total number of possible test vectors. In theory, there are at most `2^C` test vectors, where `C` is the number of conditions. In practice, since the boolean operators of the decision are short-circuiting, many test vectors end up producing the same control flow.

For each decision, the MC/DC tool modifies the code of the program to create a **decision counter**. The decision counter acts as an accumulator, and is incremented by a specific **weight** for every condition on a particular path through the BES. The specific weights are chosen during BDD construction. The range of a decision counter is `[0 .. test_vector_count]`.

For the decision

(A and B) or C

the BDD along with the decision counter (`idx`) and specific weights (numbers on the right-hand side of operator `+=`) are (ignore `in` and `w`):

The MC/DC tool would (naively) instrument the decision as follows (assuming Rust):

# before statements
if (A && B) || C {
    # if statements
}
# after statements

becomes

# before statements
let mut counter = base_index;
if A {
    counter += 0;
    if B {
        decision_idx += 4;
        save_counter(counter);      // 4
        # if statements
    }
    else {
        counter += 0;
        if C {
            counter += 2;
            save_counter(counter);  // 2
            # if statements
        } else {
            counter += 0;
            save_counter(counter);  // 0
        }
    }
} else {
    counter += 1;
    if C {
        counter += 2;
        save_counter(counter);      // 3
        # if statements
    } else {
        counter += 0;
        save_counter(counter);      // 1
    }
}
# after statements

Note that the final values of `counter` are unique, they also uniquely identify a path through the BDD, which in turn implies the Boolean values of the individual conditions on that path.

## Program

While the MC/DC tool is processing all decisions and conditions, it keeps track of:
* The source span of each condition.
* Which decision counter value involves which conditions.
* The total number of test vectors across all decisions.

The MC/DC tool modifies the code of the program to create a single **bit vector**, and emit it upon program termination. The size of the bit vector is equal to the total number of test vectors across all decisions. The bit vector is indexed by decision counter + `base_index` (see example). The bit vector is laid out as follows:

| Index | Comment |
| ----- | --------|
| 0 | The `base_index` for `(A && B) \|\| C` is `0`, since (it is assumed that) it is the first decision. |
| 1 | |
| 2 | |
| 3 | |
| 4 | |
| 5 | The `base_index` for the next decision is the `base_index` of the previous decision (`0`) plus the number of test vectors of the previous decision (`5`). |
| . . . | And so on. |

Every time the decision counter is saved (see `save_counter` in the example), the bit at that position in the bit vector is set to one.

The MC/DC tool uses the remaining collected information to produce **Source Information Data** (SID). The SID contains
* ID and span information for each condition.
* Map from decision counter to conditions.

**Conditions**
| ID | Span |
| -- | ---- |
| 0 | file, line, column_start, column_end |
| 1 | file, line, column_start, column_end |
| . . . | And so on. |

**Map**
| Decision counter | Condition IDs |
| ---------------- | ------------- |
| 0 | 1, 4, 5 |
| 1 | 3, 4 |
| . . . | And so on. |

The SID is emitted by the MC/DC tool.

# Coverage Workflow

1. The MC/DC tool processes the program, and produces an instrumented binary along with the SID.
1. The instrumented binary is executed, possibly multiple times. Each execution emits a distinct bit vector.
1. The MC/DC tool consumes the SID and the individual bit vectors to produce a coverage report.

# Decision recognition from MIR

Assume the following code:

fn condition1() -> bool {
    black_box(true)
}

fn condition2() -> bool {
    black_box(false)
}

fn id(id: bool) -> bool {
    black_box(id)
}

fn foo(a: bool, b: bool) {
    if a && condition1() || condition2() {
        if b || id(a && b) {
            println!("If If");
        }
    } else {
        println!("Else");
    }
}

Here, the function `foo` has 3 decisions:
1. `a && condition1() && condition2()`
2. `b || id(...)`
3. `a && b`

The following diagram shows the MIR representation of `foo`, with the basic blocks related to the decisions being circled in blue, orange and green, respectively.


In this graph, there is no trivially recognizable pattern to differentiate the decisions, let alone detect the number of decisions, knowing if a decision comes from syntactic desugaring or from actual source code, and mapping back the nodes to specific spans in the source code to create de mappings.

In addition, note that not every *condition* is transformed into a SwitchInt. For example, the `b` condition of the green decision `a && b` is simplified, since we are passing the result of the decision as a parameter instead of branching from it.

This makes it very difficult for MC/DC instrumentation to rely on MIR for decision detection.