Language-Parametric Reference Synthesis (Extended)

TL;DR

This paper introduces a language-parametric method for synthesizing references in automated refactoring tools, leveraging type system specifications and scope graphs to improve correctness across multiple programming languages.

Contribution

It proposes automatically deriving inverse name lookup functions from language specifications using scope graphs, enabling more reliable automated refactorings.

Findings

Successfully synthesized references for thousands of Java, ChocoPy, and Featherweight Generic Java programs.

Provides a principled, language-parametric approach to reference synthesis in IDE refactoring.

Enhances correctness and safety of automated refactorings in modern IDEs.

Abstract

Modern Integrated Development Environments (IDEs) offer automated refactorings to aid programmers in developing and maintaining software. However, implementing sound automated refactorings is challenging, as refactorings may inadvertently introduce name-binding errors or cause references to resolve to incorrect declarations. To address these issues, previous work by Sch\"afer et al. proposed replacing concrete references with locked references to separate binding preservation from transformation. Locked references vacuously resolve to a specific declaration, and after transformation must be replaced with concrete references that also resolve to that declaration. Synthesizing these references requires a faithful inverse of the name lookup functions of the underlying language. Manually implementing such inverse lookup functions is challenging due to the complex name-binding features in modern programming languages. Instead, we propose to automatically derive this function from type system specifications written in the Statix meta-DSL. To guide the synthesis of qualified references we use scope graphs, which represent the binding structure of a program, to infer their names and discover their syntactic structure. We evaluate our approach by synthesizing concrete references for locked references in 2528 Java, 196 ChocoPy, and 49 Featherweight Generic Java test programs. Our approach yields a principled language-parametric method for synthesizing references.