On Static Analysis for Expressive Pattern Matching

paper ps   
Pattern matching is a widespread programming language construct that enables definitions of values by cases, generalizing if-then-else and case statements. The cases in a pattern matching expression should be exhaustive: when the value does not match any of the cases, the expression throws a run-time exception. Similarly, each pattern should be reachable, and, if possible, patterns should be disjoint to facilitate reasoning. Current compilers use simple analyses to check patterns. Such analyses ignore pattern guards, use static types to approximate possible expression values, and do not take into account properties of user-defined functions. We present a design and implementation of a new analysis of pattern matching expressions. Our analysis detects a wider class of errors and reports fewer false alarms than previous approaches. It checks disjointness, reachability, and exhaustiveness of patterns by expressing these conditions as formulas and proving them using decision procedures and theorem provers. It achieves precision by propagating possible values through nested expressions and approximating pattern-matching guards with formulas. It supports user-defined “extractor” functions in patterns by relying on specifications of relationships between the domains of such functions. The result is the first analysis that enables verified, declarative pattern matching with guards in the presence of data abstraction. We have implemented our analysis and describe our experience in checking a range of pattern matching expressions in a subset of the Scala programming language.

Citation

Mirco Dotta, Philippe Suter, and Viktor Kuncak. On static analysis for expressive pattern matching. Technical Report LARA-REPORT-2008-004, EPFL, 2008.

BibTex Entry

@techreport{DottaETAL08OnStaticAnalysisExpressivePatternMatching,
  author = {Mirco Dotta and Philippe Suter and Viktor Kuncak},
  title = {On Static Analysis for Expressive Pattern Matching},
  institution = {EPFL},
  year = 2008,
  number = {LARA-REPORT-2008-004},
  abstract = {
Pattern matching is a widespread programming language
construct that enables definitions of values by cases,
generalizing if-then-else and case statements.  The cases in
a pattern matching expression should be exhaustive: when the
value does not match any of the cases, the expression throws
a run-time exception.  Similarly, each pattern should be
reachable, and, if possible, patterns should be disjoint to
facilitate reasoning.  Current compilers use simple analyses
to check patterns. Such analyses ignore pattern guards, 
use static types to approximate possible
expression values, and do not take into account properties
of user-defined functions.

We present a design and implementation of a new analysis of
pattern matching expressions.  Our analysis detects a wider
class of errors and reports fewer false alarms than previous
approaches.  It checks disjointness, reachability, and
exhaustiveness of patterns by expressing these conditions as
formulas and proving them using decision procedures and
theorem provers.  It achieves precision by propagating
possible values through nested expressions and approximating
pattern-matching guards with formulas.  It supports
user-defined ``extractor'' functions in patterns by relying
on specifications of relationships between the domains of
such functions.  The result is the first analysis that
enables verified, declarative pattern matching with guards
in the presence of data abstraction.  We have implemented
our analysis and describe our experience in checking a range
of pattern matching expressions in a subset of the Scala
programming language.
}
}