From Separate Compilation to Sound Language Composition

TL;DR

The paper addresses the challenge of modular language design with separate compilation by preventing runtime attribute errors in Neverlang through static analysis. It introduces nlgcheck, a data-flow based verifier that analyzes CFGs of semantic actions to ensure attributes are defined and typed along all feasible execution paths. The work formalizes a verification model, develops a robust CFG visiting algorithm with optimizations, and demonstrates substantial error-detection gains via mutation testing across multiple Neverlang-based languages. The results suggest that combining separate compilation with static guarantees is practical, with implications for broader adoption of modular language workbenches and future extension to other frameworks.

Abstract

The development of programming languages involves complex theoretical and practical challenges, particularly when addressing modularity and reusability through language extensions. While language workbenches aim to enable modular development under the constraints of the language extension problem, one critical constraint -- separate compilation -- is often relaxed due to its complexity. However, this relaxation undermines artifact reusability and integration with common dependency systems. A key difficulty under separate compilation arises from managing attribute grammars, as extensions may introduce new attributes that invalidate previously generated abstract syntax tree structures. Existing approaches, such as the use of dynamic maps in the Neverlang workbench, favor flexibility at the cost of compile-time correctness, leading to potential runtime errors due to undefined attributes. This work addresses this issue by introducing nlgcheck, a theoretically sound static analysis tool based on data-flow analysis for the Neverlang language workbench. nlgcheck detects potential runtime errors -- such as undefined attribute accesses -- at compile time, preserving separate compilation while maintaining strong static correctness guarantees. Experimental evaluation using mutation testing on Neverlang-based projects demonstrates that nlgcheck effectively enhances robustness without sacrificing modularity or flexibility and with a level of performance that does not impede its adoption in daily development activities.

Figures (5)

• Figure 1: Dominance frontier.
• Figure 2: Control dependency.
• Figure 4: Syntax and semantics for the backup task.
• Figure 5: Neverlang code implementing a C-like ternary expression language feature.
• Figure 6: Control flow graph generated by nlgcheck for the semantic action shown in Listing \ref{['lst:ternary']}.

Theorems & Definitions (30)

• Lemma 1
• proof : Proof
• Lemma 2
• proof : Proof
• Lemma 3
• proof : Proof
• Lemma 4
• proof : Proof
• Lemma 5
• proof : Proof