Set Constraints, Pattern Match Analysis, and SMT

TL;DR

This paper introduces a translation from set constraints to SMT problems, enabling efficient pattern match analysis in functional languages like Elm, ensuring unreachable cases are identified and verified practically.

Contribution

It presents a novel translation technique that allows arbitrary boolean set constraints to be solved efficiently using SMT solvers, enabling practical program analysis.

Findings

The translation is fast enough for practical use in the Elm compiler.

The approach effectively identifies unreachable pattern match cases.

It demonstrates the applicability of set constraints in real-world program verification.

Abstract

Set constraints provide a highly general way to formulate program analyses. However, solving arbitrary boolean combinations of set constraints is NEXPTIME-hard. Moreover, while theoretical algorithms to solve arbitrary set constraints exist, they are either too complex to realistically implement or too slow to ever run. We present a translation that converts a set constraint formula into an SMT problem. Our technique allows for arbitrary boolean combinations of set constraints, and leverages the performance of modern SMT solvers. To show the usefulness of unrestricted set constraints, we use them to devise a pattern match analysis for functional languages, which ensures that missing cases of pattern matches are always unreachable. We implement our analysis in the Elm compiler and show that our translation is fast enough to be used in practical verification.