Application of SMT in a Meta-Complier

Building a compiler for a programming language is a notoriously hard task, especially when starting from scratch. That’s why we developed Langkit, a meta-compiler which allows language designers to focus on the high-level aspects of their language. In particular, the specification of type systems is done in a declarative manner by writing equations in a high-level logic DSL. Those equations are then resolved by a custom solver embedded in the generated compiler front-end whenever a code fragment of the target language needs to be analyzed. This framework is successfully used at AdaCore to implement name and type resolution of Ada, powering navigation in IDEs and enabling development of deep static analysis tools. We discuss the implementation of our solver, and how a recent switch to using a DPLL(T) solver backend with a custom theory allowed us both to address long-standing combinatorial explosion problems we had with our previous approach, but also to gain new insights in how to emit human-readable diagnostics for type errors.