Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Modified Condition/Decision Coverage of Rust

Wanja Zaeske, Pietro Albini, Florian Gilcher, Umut Durak

TL;DR

The paper addresses the challenge of applying Modified Condition/Decision Coverage ($MCDC$) to Rust, focusing on how Rust's pattern matching and macro system complicate traditional instrumentation and interpretation. It proposes a formal framework that treats patterns as trees of sub-patterns and analyzes sub-pattern refutability to determine when a pattern constitutes a decision, including handling of nested conditionals and the question mark operator. Key contributions include a comprehensive categorization of sub-patterns (literal, identifier, wildcard, rest, range, reference, struct, tuple, slice, path, or) and rules for their direct or indirect refutability, enabling accurate $MCDC$ analysis for Rust code. The work discusses macro hygiene constraints, constants, and certification considerations, arguing that a Rust MCDC checker can be integrated into the compiler or closely mirror its front-end, and that achieving Level A coverage is feasible with a dedicated toolchain. Overall, the study lays the groundwork for Rust to be adopted in high-assurance domains by outlining concrete semantics for pattern-based decisions and a roadmap toward Rust-based $MCDC$ tooling within the compiler ecosystem.

Abstract

Testing is an essential tool to assure software, especially so in safety-critical applications. To quantify how thoroughly a software item has been tested, a test coverage metric is required. Maybe the strictest such metric known in the safety critical systems is Modified Condition/Decision Coverage (MC/DC), which DO-178C prescribes for the highest software assurance level in aviation. In the past, ambiguities in the interpretation of MC/DC have been resolved already, i. e. in CAST-10. However, some central features of the Rust programming language necessitate further clarification. This work investigates aforementioned features, in particular pattern matching, providing a consistent view on how to apply MC/DC to Rust. Hence, this paper informs the implementation of Rust MC/DC tools, paving the road towards Rust in high-assurance applications.

Towards Modified Condition/Decision Coverage of Rust

TL;DR

The paper addresses the challenge of applying Modified Condition/Decision Coverage () to Rust, focusing on how Rust's pattern matching and macro system complicate traditional instrumentation and interpretation. It proposes a formal framework that treats patterns as trees of sub-patterns and analyzes sub-pattern refutability to determine when a pattern constitutes a decision, including handling of nested conditionals and the question mark operator. Key contributions include a comprehensive categorization of sub-patterns (literal, identifier, wildcard, rest, range, reference, struct, tuple, slice, path, or) and rules for their direct or indirect refutability, enabling accurate analysis for Rust code. The work discusses macro hygiene constraints, constants, and certification considerations, arguing that a Rust MCDC checker can be integrated into the compiler or closely mirror its front-end, and that achieving Level A coverage is feasible with a dedicated toolchain. Overall, the study lays the groundwork for Rust to be adopted in high-assurance domains by outlining concrete semantics for pattern-based decisions and a roadmap toward Rust-based tooling within the compiler ecosystem.

Abstract

Testing is an essential tool to assure software, especially so in safety-critical applications. To quantify how thoroughly a software item has been tested, a test coverage metric is required. Maybe the strictest such metric known in the safety critical systems is Modified Condition/Decision Coverage (MC/DC), which DO-178C prescribes for the highest software assurance level in aviation. In the past, ambiguities in the interpretation of MC/DC have been resolved already, i. e. in CAST-10. However, some central features of the Rust programming language necessitate further clarification. This work investigates aforementioned features, in particular pattern matching, providing a consistent view on how to apply MC/DC to Rust. Hence, this paper informs the implementation of Rust MC/DC tools, paving the road towards Rust in high-assurance applications.
Paper Structure (33 sections, 1 figure)

This paper contains 33 sections, 1 figure.

Table of Contents

  1. Introduction
  2. Background
  3. Modified Condition/Decision Coverage
  4. Switch Case in C/C++
  5. Enums in Rust
  6. Pattern Matching in Rust
  7. Macro hygiene
  8. Role of pattern-matching in Rust
  9. MCDC for Rust's pattern matching
  10. Patterns as a tree of sub-patterns
  11. Pattern refutability
  12. Refutability of sub-patterns
  13. Literal sub-patterns
  14. Identifier sub-patterns
  15. Wildcard sub-patterns
  16. ...and 18 more sections

Figures (1)

  • Figure 1: Decomposition of example pattern into sub-patterns. The denotes an abitrary inner value