# Extended Paper: API-driven Program Synthesis for Testing Static Typing
Implementations

Thodoris Sotiropoulos  ETH ZurichSwitzerland
<EMAIL_ADDRESS>,  Stefanos Chaliasos  Imperial College
LondonUK<EMAIL_ADDRESS>and  Zhendong Su  ETH ZurichSwitzerland
<EMAIL_ADDRESS>
###### Abstract.

We introduce a novel approach for testing static typing implementations based
on the concept of API-driven program synthesis. The idea is to synthesize
type-intensive but small and well-typed programs by leveraging and combining
application programming interfaces (APIs) derived from existing software
libraries. Our primary insight is backed up by real-world evidence: a
significant number of compiler typing bugs are caused by small test cases that
employ APIs from the standard library of the language under test. This is
attributed to the inherent complexity of the majority of these APIs, which
often exercise a wide range of sophisticated type-related features. The main
contribution of our approach is the ability to produce small client programs
with increased feature coverage, without bearing the burden of generating the
corresponding well-formed API definitions from scratch. To validate diverse
aspects of static typing procedures (i.e., soundness, precision of type
inference), we also enrich our API-driven approach with fault-injection and
semantics-preserving modes, along with their corresponding test oracles.

We evaluate our implemented tool, thalia, on testing the static typing
implementations of the compilers for three popular languages, namely, Scala,
Kotlin, and Groovy. thalia has uncovered $\sepnum{.}{,}{}{84}$ typing bugs
($\sepnum{.}{,}{}{77}$ confirmed and $\sepnum{.}{,}{}{22}$ fixed), most of
which are triggered by test cases featuring APIs that rely on parametric
polymorphism, overloading, and higher-order functions. Our comparison with
state-of-the-art shows that thalia yields test programs with distinct
characteristics, offering additional and complementary benefits.

compiler bugs, compiler testing, static typing, API, library, enumeration

††copyright: rightsretained††ccs: Software and its engineering Compilers††ccs:
Software and its engineering Software testing and debugging

##  1\. Introduction

Type safety is a fundamental property contributing to the correct execution of
computer programs. Static typing, an integral process in every statically-
typed programming language implementation (typically part of the compiler),
verifies that a source program is type-correct and type-safe based on a type
system. A type system lies at the heart of the design of a language—it
outlines a set of rules regarding the language’s types, and how these types
can be used and combined (Pierce, 2002). Language designers and researchers
strive to build sound type systems (Tate et al., 2011; Cortier et al., 2017;
Milano et al., 2022), which guarantee type safety, i.e., being able to
identify all potential type errors during compilation.

At the same time, modern languages continuously evolve with new (and often
sophisticated) features to provide users with a smoother programming
experience. However, integrating these new features into a language poses
significant challenges and considerations for implementing sound and practical
type systems. Indeed, recent work (Chaliasos et al., 2021, 2022) has shown
that the static typing implementations of well-established compilers suffer
from a substantial number of bugs (Amin and Tate, 2016). These implementation
flaws lead to (1) reliability and security ramifications on the programs
compiled with the faulty compilers, and (2) degradation of the programmers’
experience and productivity. In particular, compiler typing bugs typically
cause frustrating rejections of well-typed programs, dangerous acceptances of
erroneous, type-unsafe programs, or annoying crashes and compilation
performance issues.

In spite of the sharp rise of compiler testing research, improving the
reliability of compilers’ type checkers has been until recently a neglected
problem. Indeed, most of the existing compiler testing techniques target
optimizing compilers (Yang et al., 2011; Le et al., 2014; Zhang et al., 2017;
Donaldson et al., 2017; Livinskii et al., 2020, 2023). As shown in the
empirical work of Chaliasos et al. (2021), detecting typing bugs demands new
compiler testing methods, because typing bugs exhibit distinct characteristics
(e.g., symptoms, root causes) compared to optimization bugs.

Currently, there are only a few approaches to validating static typing
implementations. Focusing on Rust’s type checker, Dewey et al. (2015) have
introduced a fuzzing approach based on constraint logic programming. More
recently, Chaliasos et al. (2022) have developed hephaestus, which produces
type-intensive programs written in an intermediate language (IR) that supports
parametric polymorphism and type inference. This high-level IR allows
targeting multiple languages (i.e., Java, Groovy, and Kotlin).

All the aforementioned approaches rely on _generative compiler testing_ :
constructing programs entirely from scratch based on the syntactic and
semantic rules of a language under test. However, generative compiler testing
involves a significant limitation: it is unable to test features beyond what
the underlying code generator can handle and synthesize. Therefore, the
utility of generative techniques can easily saturate (Amalfitano et al.,
2015), producing programs that exhibit the same programming idioms, unless new
language constructs are implemented in the program generator.

Approach: We introduce a novel approach for testing static typing
implementations based on the concept of _API-driven program synthesis_. Our
approach is motivated by the findings of a recent empirical study (Chaliasos
et al., 2021): around one third of compiler typing bugs are triggered by small
test cases that employ application programming interfaces (APIs) from the
standard library of the language being tested. This finding is well-justified,
considering the inherent complexity of the included API definitions (e.g.,
functions, variables, types), which heavily rely on advanced type-related
features such as parametric polymorphism. Building upon this finding, our
approach leverages the abundance of existing APIs, and produces small (yet
complex) client programs, _without_ the burden of producing the corresponding
well-formed definitions from scratch. Our approach exploits the fact that
although libraries are pre-compiled, a compiler still performs type checking
on every client program that refers to components of a library API. This
ensures that the features provided by the API are used in a type-safe manner.

At the high level, our approach works as follows. The input is an API, which
is modeled as an  _API graph_ , a structure that captures the dependencies and
relations among API components. Then, our approach proceeds with the concept
of  _API enumeration_ : for every component $d$ (i.e., method/field) of the
input API, it systematically explores all unique, type-safe usages of $d$
w.r.t. the signature of $d$. Invoking an API component through different
typing patterns lets us exercise the implementation of many type-related
operations in the compiler (e.g., subtyping rules). The outcome of the API
enumeration process is a finite set of abstract typed expressions. An abstract
typed expression is encoded as a sequence of types that represents which
specific types are combined to employ a certain API entity. In turn, our
approach concretizes each abstract typed expression by replacing each type in
the sequence with an inhabitant (Urzyczyn, 1997) that re-uses code from the
input library. To synthesize an inhabitant, the approach consults the API
graph to identify sequences of method calls or field accesses that match the
given type. By default, our method yields well-typed client programs.
Consequently, a compiler is expected to successfully accept these generated
programs. Failures to do so indicate potential bugs in the compiler.

Our method is also equipped with two modes that allow the discovery of type
inference and soundness bugs respectively. Specifically, the first mode
produces well-typed programs with omitted type information. To do so, when
encountering a polymorphic call, our method provides no explicit type
arguments whenever these can be inferred by the surrounding context. The
second mode produces ill-typed programs by enumerating all those abstract-
typed expressions that employ a specific API component in a way that violates
typing rules. This mode enables the detection of soundness bugs by finding
cases where the compiler mistakenly accepts ill-typed programs.

Results: Our implementation, which we call thalia,111In Greek mythology,
Thalia was a nymph daughter of the smithing god Hephaestus. produces programs
written in three popular languages: Scala, Groovy, and Kotlin. In our
evaluation, we collected a large corpus of popular APIs taken from Maven’s
central software repository. Based on the collected APIs, thalia produced
small client programs that were able to trigger $\sepnum{.}{,}{}{84}$ unique
bugs, of which $\sepnum{.}{,}{}{77}$ have been either confirmed or fixed. Our
two modes helped identify $\sepnum{.}{,}{}{27}$ type inference bugs, and
$\sepnum{.}{,}{}{10}$ bugs triggered by wrongly-typed code. When comparing our
work with the state-of-the-art framework hephaestus (Chaliasos et al., 2022),
we find that, despite producing test programs one order of magnitude smaller
than prior work, thalia is able to detect at least 42 bugs missed by it.
Furthermore, thalia’s programs exercise previously unexplored compiler
regions, leading to an increase in hephaestus’ code coverage by up to $9\%$
(.,.,2567) for lines of code, 10% (.,.,17548) for branches, and 8% (.,.,581)
for functions.

Contributions: Our work makes the following contributions.

  * •

The notion of API enumeration, which systematically examines API component
usages via diverse valid (or invalid) typing patterns (aka abstract-typed
expressions). This allows the exploration of complex type-related
functionalities in the compiler, making our approach suitable for testing.

  * •

A novel API-driven program synthesis approach for producing small yet complex
client programs based on well-typed (or ill-typed) abstract-typed expressions
via API enumeration.

  * •

An open-source implementation called thalia, which is able to produce client
code written in three different languages: Scala, Kotlin, and Groovy.

  * •

An extensive evaluation of thalia covering several aspects, including bug-
finding capability, characteristics of test cases, code coverage, and
comparison with state-of-the-art. Overall, thalia uncovered
$\sepnum{.}{,}{}{84}$ new faults triggered in three widely-used compilers.
These failures were caused by a plethora of language features available in the
input APIs.

Availability: thalia is available as open-source software under the GNU
General Public License v3.0 at https://github.com/hephaestus-compiler-
project/thalia. The research artifact is available at
https://zenodo.org/record/8425071.

##  2\. Background and Illustrative Examples

This section presents the background and motivation of our API-driven approach
by discussing the limitations of the existing techniques in generative
compiler testing, especially those of hephaestus, and how we address them.

Limitations of Hephaestus: hephaestus (Chaliasos et al., 2022) is the state-
of-the-art tool for finding compiler typing bugs. It adopts a generative
process similar to that of Csmith (Yang et al., 2011). Specifically,
hephaestus creates a bunch of random class/method/field definitions that
respect the syntax and the semantics of a target language (in this case
hephaestus’ IR). This generative process involves three major limitations:

  * •

The generated programs contain  _only_ a limited set of features. This means
that the program generator is unable to exercise a certain feature, if this
feature is not supported by the implementation. Extending the program
generator with new features is technically hard, and often only works for a
specific language. This is because the program generator needs to apply a set
of language-specific semantic checks to ensure the validity of the generated
programs. For example, creating a well-formed class that implements multiple
interfaces requires checking that the interfaces have no conflicting method
signatures.

  * •

Even after using diverse configurations, the generative process easily comes
to a saturation point (Amalfitano et al., 2015), because the resulting
programs are somewhat biased in generating programs that exhibit the same
programming idioms.

  * •

To test a new language (e.g., Rust), someone typically needs to engineer a new
program generator.

⬇

1import java.util.LinkedList

2import com.google.common.collect.LinkedHashMultiset

3def test(): Unit {

4 val x: Tuple1[LinkedHashMultiset[String]] = ???

5 val res: Any = x._1.retainAll(new LinkedList())

6}

(a) Test case written in Scala.

⬇

1package com.google.common.collect;

2public class LinkedHashMultiset<T> extends AbstractMultiSet<T> { }

3class AbstractMultiSet<T> implements MultiSet<T> {

4 public void retailAll(Collection<?> p) {}

5}

(b) Definition of the LinkedHashMultiset API in the guava library.

Figure 1. DOTTY-17391: This program triggers a crash in Dotty. The program
exercises the guava API.

The benefits and power of APIs: To tackle these limitations of hephaestus, we
introduce a complementary approach that relies on real-world  _APIs_ , which
are well-engineered, expressive, and utilize diverse language features. Rather
than generating large programs consisting of random definitions, we synthesize
small but intricate client programs that invoke components (e.g., method) from
a given API. This allows us to (1) effortlessly exercise a rich set of
features without the added complexity of creating complex definitions from
scratch, and (2) combine individual features in interesting and unexpected
ways. In contrast to conventional generative processes (see hephaestus), API-
based test programs provide the following unique benefits:

  * •

Rich feature coverage for free: As APIs are typically designed for use in a
wide variety of contexts, they often combine diverse sophisticated and
demanding language features, such as bounded polymorphism, subtyping, or
overloading. Given that their interfaces are also likely to be well-tested and
widely used, they are free from type errors. Therefore, a feature-agnostic and
potent generation process can be achieved by creating test programs centered
around APIs without creating these complex and well-typed API definitions
ourselves. Furthermore, the huge variety of real-world APIs avoids, or at
least delays, the saturation of the generation process.

  * •

Applicability: APIs are ubiquitous in mainstream languages. Generating type-
intensive programs for a new language mostly requires the collection of its
APIs (see Section 3.6—Generalizability).

  * •

Efficient testing: Generating small programs improves the throughput of
testing, as the compilers under test require considerably less time to process
small inputs than large ones.

  * •

Simple test-case reduction: Test-case reduction is highly important for
compiler testing campaigns (Regehr et al., 2012). By construction, API-driven
program synthesis yields small, self-contained programs that require minimal
test-case reduction.

Consider the following two bugs found by API-driven programs synthesized by
our tool.

Internal compiler error in the Scala 3 compiler: Figure 1(a) shows a valid
program that triggers a crash in the compiler of Scala 3, also known as Dotty.
The program imports the LinkedHashMultiset class from com.google.guava:guava
(line 2), a popular library that extends the Java collections framework. On
line 4, the code uses the Scala standard library to create a tuple containing
an element of type LinkedHashMultiset<String>. Next, by accessing this
element, the program invokes the method retainAll found in the
LinkedHashMultiset class.

Figure 1(b) shows the LinkedHashMultiset class as defined in the guava
library. The class inherits retainAll from base class AbstractMultiSet.
Notably, AbstractMultiSet involves a default access modifier (line 3), meaning
that the class is inaccessible from code outside the package
com.google.common.collect. However, its method retainAll features a public
access modifier (line 4), which suggests that the method can be accessed by
any public subclass of AbstractMultiSet, including LinkedHashMultiset.
Although retainAll belongs to the API of LinkedHashMultiset, Dotty mistakenly
treats the method as inaccessible, which in turn leads to a compiler crash
while typing the method call on line 5 (Figure 1(a)). Surprisingly, replacing
the receiver expression x._1 with any other expression of type
LinkedHashMultiset<String> successfully compiles the program.

[thick, scale=0.82, every node/.style=scale=0.8, font=, node distance=0.4cm,
main/.style = draw=none, rectangle] [main](0) at (1,0)

⬇

1import org.apache.commons.lang3.ArrayUtils;

2class Test {

3 void test() {

4 byte x = new byte[0];

5 byte[] res = ArrayUtils.removeAll(x, 0);

6 }

7}

; [main] (1) at (7, 0.3)

⬇

package org.apache.commons.lang3.ArrayUtils;

class ArrayUtils {

static boolean[] removeAll(boolean[] array, int... indices)

static byte[] removeAll(byte[] array, int... indices)

static short[] removeAll(short[] array, int... indices)

static int[] removeAll(int[] array, int... indices)

static long[] removeAll(long[] array, int... indices)

static float[] removeAll(float[] array, int... indices)

static double[] removeAll(double[] array, int... indices)

static char[] removeAll(char[] array, int... indices)

static <T> T[] removeAll(T[] array, int... indices)

}

; [-¿] (1.6,-0.25) – (2.8,1.1); (3,1) rectangle (11.1,1.4);

Figure 2. GROOVY-11053: A well-typed program rejected by the Groovy compiler.
The program exercises the apache-commons-lang3 library.

Unexpected method ambiguity error in groovyc: Figure 2 shows another bug where
groovyc erroneously rejects a well-typed program. The code first defines an
array of byte (line 4), and then calls a static method from the ArrayUtils API
of the org.apache.commons:commons-lang3 library to remove the element of the
array at position 0 (line 5).

The API of ArrayUtils is quite complex: it provides nine overloaded methods
all named removeAll. Eight of them operate on primitive arrays, while the
remaining one is a polymorphic method operating on arrays of reference types.
When a compiler encounters a call to an overloaded method, it chooses to
invoke the most specific one based on a set of criteria, such as the types of
the provided arguments. Although it is clear from the context that the code
intends to call the method variant that takes an array of bytes, a bug in
groovyc’s method resolution causes the compiler to accidentally reject the
program with an error of the form: “reference to method removeAll is
ambiguous. Cannot choose between candidate methods.” The root cause of the
failure lies in the way variable arguments are matched against formal
parameter types related to primitive types.

As the two examples illustrate, although the invoked APIs seem simple at a
first glance, it is in fact challenging for the compilers to correctly handle
these APIs. Indeed, the guava API exercises access modifiers and complex
inheritance scenarios, while the apache-commons-lang3 API has many overloaded
methods mixed with plenty of type-related features (e.g., primitive types,
array types, and variable arguments). Interestingly, API components might hide
other typing features. For example, although calling method retainAll in
Figure 1(a) knows nothing about what an access modifier stands for, or the
inheritance chain of the receiver, the corresponding test case triggers a
compiler bug associated with these ‘‘hidden’’ features.

##  3\. API-driven Program Synthesis

Figure 3. The API-driven program synthesis approach for finding compiler
typing bugs.

Figure 3 gives an overview of our API-driven program synthesis approach. The
process begins with a corpus of APIs extracted from either the standard
library of the language being tested or its third-party libraries. These APIs
are represented in an  _API graph_ which captures the dependencies and type
signature of each API component (Section 3.2). Next, our approach performs
_API enumeration_ which systematically explores all possible invocations of
the encompassed API components through unique typing patterns (Section 3.3). A
typing pattern is a sequence of types that corresponds to  _abstract typed
expressions_. Conceptually, an abstract typed expression represents a
combination of types used to invoke a particular API entity (e.g, method). An
abstract expression can be either well-typed or ill-typed with regards to the
type signature of the corresponding API component. Then, the approach yields
well-typed or ill-typed programs by concretizing each abstract-typed
expression into a concrete one written in a reference language called API-IR.
To do so, it examines the API graph to find type inhabitants by enumerating
the set of paths that reach a specific type node via standard graph
reachability algorithms (Section 3.4).

As an optional step, our approach employs the type erasure process whose
purpose is to remove the type arguments of polymorphic calls, while
maintaining the type correctness of the original expression (Section 3.5). The
insight is that constructing polymorphic calls without explicit type arguments
helps exercise the implementations of type inference operations. The final
step is to employ language-specific translators that transform an expression
in API-IR into a source file written in an actual language (e.g., Scala).
Ultimately, the generated source files are given as input to the compiler
under test, whose output is checked against the given oracle for potential
bugs. In particular, we expect the compiler to accept the programs derived
from well-typed typing sequences, and reject those that come from ill-typed
ones. We now describe our approach in detail.

###  3.1. Preliminary Definitions

Figure 4 presents the core language (called API-IR) that we use as a base to
explain our approach. API-IR is a basic language that supports three major
programming constructs: classes, functions, and fields/variables. 222In our
implementation, the core language is extended with more sophisticated
features, such as lambdas, or wildcard types. API-IR is also equipped with
parametric polymorphism in the style of Java-like generics. The API-IR is
designed with simplicity in mind, ensuring that the principles of our approach
(discussed in subsequent sections) can be adapted to any language compatible
with API-IR. In what follows, we use the vector notation to represent a
sequence of elements. For example, $\overline{t}$ means a sequence of $t$
elements.

API-IR is parameterized by an API denoted as $\Lambda\in API$. An API is a set
consisting of (polymorphic) classes, (polymorphic) functions, and
field/variables. A class defined as $\text{{{\tt class}}}\
\mathcal{C}\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}\ \text{{{\tt
extends}}}\ \overline{t}:\overline{v}$ defines a sequence of formal type
variables $\overline{\alpha}$, and extends a sequence of types $\overline{t}$.
The body of a class represented by $\overline{v}$ contains other API members,
including nested class definitions. A function $\text{{{\tt fun}}}\
m\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}(\overline{x:t_{1}}):t_{2}$
with name $m$: (1) introduces a set of type variables $\overline{\alpha}$, (2)
takes a sequence of formal parameters, and (3) outputs a value of type
$t_{2}$. A class or a function is considered  _polymorphic_ only when the
sequence $\overline{\alpha}$ in their syntax is not empty. A program in API-IR
is a sequence of expressions that use components from the given API $\Lambda$.
An expression is either a constant of type $t\in\textit{Type}$ denoted as
$\textit{constant}(t)$, a local variable definition, a field access, or a
function call. The expression $\epsilon$ represents an empty expression used
to model the invocation of top-level methods and fields, e.g., methods with no
explicit receiver.

The type system in API-IR is nominal. The set of types includes the usual
$\bot$ and $\top$ types, or a type variable $\phi:t$ with an upper bound $t$.
A class type
$\mathcal{T}\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}:\overline{t}$ is
labeled with a name $\mathcal{T}$, a sequence of type variables
$\overline{\alpha}$, and a sequence of supertypes $\overline{t}$. A class type
is derived from a class $c\in\textit{Class}$ based on function
$\textit{type}:\textit{Class}\longrightarrow\textit{Type}$ shown in Figure 4.
When the sequence $\overline{\alpha}$ is not empty, the class type
$\mathcal{T}\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}:\overline{t}$ is
referred to a  _type constructor_. The type system of API-IR also features a
type instance ($N\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}$) that
instantiates a type constructor $N$ with a sequence of type arguments
$\overline{t}$.

$\Lambda\in\textit{API}$ $\overline{v}$
$v\in\textit{APIMember}$ $c$ $d$
$c\in\textit{Class}$ class
$\mathcal{C}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}\
\text{{{\scriptsize{\tt extends}}}}\ \overline{t}:\ \overline{v}$
$d\in\textit{Def}$ fun
$m\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}(\overline{x:t}):t$
var $f:t$
$p\in\textit{Program}$ $\overline{e}$
$e\in\textit{Expr}$ $\epsilon$ $\textit{constant}(t)$ $e.f$
local var $x:t=e$
$e.m\text{{{\scriptsize{\tt<}}}}\overline{t}\text{{{\scriptsize{\tt>}}}}(\overline{e})$
$f,x\in{\it VariableName}$ the set of field names in lib $\Lambda$
$m\in{\it MethodName}$ the set of method names in lib $\Lambda$
$\mathcal{C}\in{\it ClassName}$ the set of class names in lib $\Lambda$

(a) Syntax

$t\in{\it Type}$ $\top$$\bot$ $\alpha$ $N$
$N\text{{{\scriptsize{\tt<}}}}\overline{t}\text{{{\scriptsize{\tt>}}}}$
$\alpha\in{\it TypeVariable}$ $\phi:t$
$N\in\textit{ClassType}$
$\mathcal{T}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}$:
¯t
$\phi\in\textit{TypeVarName}$ the set of type variable names in lib $\Lambda$
$\mathcal{T}\in{\it TypeName}$ the set of type names in lib $\Lambda$

(b) Types

$\displaystyle\textit{UpBound}:\textit{TypeVariable}\longrightarrow\textit{Type}$
$\displaystyle\textit{UpBound}(\phi:t)=t$
$\displaystyle\textit{type}:\textit{Class}\longrightarrow\textit{Type}$
$\displaystyle\textit{type}(\text{{{\scriptsize{\tt class}}}}\
\mathcal{C}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}})\
\text{{{\scriptsize{\tt extends}}}}\
\overline{t}:\overline{d})=\mathcal{C}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}:\overline{t}$
$\displaystyle\textit{typeName}:\textit{Type}\longrightarrow\textit{TypeName}$
$\displaystyle\textit{typeName}(\mathcal{T}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}:\overline{t})=\mathcal{T}$
$\displaystyle\textit{typeName}(N\text{{{\scriptsize{\tt<}}}}\overline{t}\text{{{\scriptsize{\tt>}}}})=\textit{typeName}(N)$

$\displaystyle\textit{className}:\textit{Class}\longrightarrow\textit{ClassName}$
$\displaystyle\textit{className}(\text{{{\scriptsize{\tt class
}}}}\mathcal{C}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}\text{{{\scriptsize{\tt
extends }}}}\overline{t}:\overline{v})=\mathcal{C}$
$\displaystyle\textit{fields}:\textit{Class}\longrightarrow\textit{Def}$
$\displaystyle\textit{fields}(\text{{{\scriptsize{\tt class
}}}}\mathcal{C}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}\text{{{\scriptsize{\tt
extends }}}}\overline{t}:\overline{v})=\\{d\ |\ d\in\overline{v}\land
d\textit{ is a field}\\}$
$\displaystyle\textit{methods}:\textit{Class}\longrightarrow\textit{Def}$
$\displaystyle\textit{methods}(\text{{{\scriptsize{\tt class
}}}}\mathcal{C}\text{{{\scriptsize{\tt<}}}}\overline{\alpha}\text{{{\scriptsize{\tt>}}}}\text{{{\scriptsize{\tt
extends }}}}\overline{t}:\overline{v})=\\{d\ |\ d\in\overline{v}\land
d\textit{ is a function}\\}$

(c) Auxiliary functions operating on types and classes.

[field] c ∈Λ
c  is a class
typeName(t) = className(c)

var f: t ∈fields(c)
⟨t’, σ⟩= decompose(t) Field(Λ, t, f) = ⟨var f: t, σ⟩ [field-inheritance] c ∈Λ
c = class C<¯α> extends ¯t: ¯v

typeName(t) = className(c)
var f: t ／∈fields(c)

t’ ∈¯t
s = Field(Λ, t’, f) Field(Λ, t, f) = s [method] c ∈Λ
c  is a class
typeName(t) = className(c)

fun  m<¯α>(¯x: p): t ∈methods(c)

⟨t’, σ⟩= decompose(t) Method(Λ, t, m) = ⟨fun  m<¯α>(¯x: p): t , σ⟩ [method-
inheritance] c ∈Λ
c = class C<¯α> extends ¯t: ¯v

typeName(t) = className(c)
fun  m<¯α>(¯x: p): t ／∈methods(c)

t’ ∈¯t
s = Method(Λ, t’, f) Method(Λ, t, m) = s

(d) Lookup functions

[epsilon] Λ⊢ϵ: ⊥ [constant] Λ⊢constant(t): t [field] Λ⊢e: r
Field(Λ, r, f) = ⟨var  f: t, σ⟩ Λ⊢e.f: σt [method call] Λ⊢e_1: r
Λ⊢¯e_2: ¯p’

Method(Λ, r, m) = ⟨fun  m<¯α>(¯x: p): t, σ’⟩
σ= σ’ ∪[¯α ↦¯t]
¯p’ <: σ¯p Λ⊢e_1.m<¯t>(¯e_2): σt [local var] Λ⊢e: t’
t’ <: t Λ⊢local var  x: t = e: ⊥

(e) Typing rules of API-IR.

Figure 4. The syntax and the types in the API-IR.

Finally, the type system of API-IR follows the usual typing rules using the
judgment $\Lambda\vdash e:t$ as shown in Figure 4. In our setting, the given
API $\Lambda$ acts as our global typing environment, and the type of an empty
expression is $\bot$ ($\Lambda\vdash\epsilon:\bot$). In the text and examples,
we use the shorthand (1) $\phi$ for $\phi:\top$, (2)
$\mathcal{T}:\overline{t}$ for
$\mathcal{T}\text{{{\tt<}}}\emptyset\text{{{\tt>}}}:\overline{t}$, (3)
$\mathcal{T}$ for $\mathcal{T}:\top$, and (4)
$\mathcal{T}\text{{{\tt<}}}\overline{t_{2}}\text{{{\tt>}}}$ for
$(\mathcal{T}\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}:\overline{t_{1}})\text{{{\tt<}}}\overline{t_{2}}\text{{{\tt>}}}$.

Our language also defines the usual type substitution and type unification
operations. A type substitution $\sigma\in\Sigma$ is a mapping that replaces
all occurrences of a type variable $\alpha$ with a given type $t$. We use the
symbol $\sigma t$ to denote the application of a substitution $\sigma$ on type
$t$. In this work, type unification (unify:
$\textit{Type}\times\textit{Type}\longrightarrow\Sigma$) takes two types
($t_{1},t_{2}\in\textit{Type}$) and identifies a substitution $\sigma$ so that
the type $\sigma t_{2}$ is equal subtype of $t_{1}$. In the following, the
symbol $<:$ indicates the subtype relation, and $\textit{UpBound}(\alpha)$
gives the upper bound of a type variable $\alpha$ as shown in Figure 4.

###### Definition 3.1 (Validity of type substitution).

A type substitution $\sigma\in\Sigma$ is called  _valid_ when
$\forall\alpha\in\textit{Dom}(\sigma).\
\sigma(\alpha)<:\textit{UpBound}(\alpha)$.

This definition expresses that a type substitution is considered valid, when
every type variable in the substitution is instantiated with a type that
respects the upper bound of the type variable. For example, the substitution
$s=[\alpha\mapsto t_{1}]$ is valid when $\alpha$ has the upper bound $\top$,
because $t_{1}<:\top$. On the contrary, the substitution is invalid when
$\alpha$ is bounded to type $t_{2}$, and $t_{1}$ is not a subtype of $t_{2}$.

###### Definition 3.2 (Subsumption).

Consider two type substitutions $\sigma_{1},\sigma_{2}\in\Sigma$. We say that
substitution $\sigma_{1}$ subsumes $\sigma_{2}$, denoted as
$\sigma_{1}\sqsubseteq\sigma_{2}$, when
$\forall\alpha\in\textit{Dom}(\sigma_{1}).\
\sigma_{1}(\alpha)=\sigma_{2}(\alpha)$.

The subsumption relation holds between two type substitutions, when all type
variables in a substitution $\sigma_{1}$ are instantiated with exactly the
_same_ type as in another substitution $\sigma_{2}$. The subsumption relation
is reflexive, and for an empty substitution $\epsilon$, we have
$\forall\sigma\in\Sigma.\epsilon\sqsubseteq\sigma$.

###### Definition 3.3 (Type decomposition).

Type decomposition ($\textit{Type}\longrightarrow\Sigma\times\textit{Type}$)
is an operation that decomposes a given type $t_{1}\in\textit{Type}$ into a
substitution $\sigma$ and another type $t_{2}\in\textit{Type}$, so that
$\sigma t_{2}=t_{1}$. It is defined as:

decompose(t)
$\displaystyle=\langle[\overline{\alpha}\mapsto\overline{t_{2}}],\mathcal{T}\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}:\overline{t_{1}}\rangle$
$\displaystyle\text{if
}t=(\mathcal{T}\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}:\overline{t_{1}})\text{{{\tt<}}}\overline{t_{2}}\text{{{\tt>}}}$
$\displaystyle\textit{decompose}(t)$ $\displaystyle=\langle\epsilon,t\rangle$
otherwise

In essence, type decomposition allows us to decompose a type instance
$N\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}$ into (1) the type constructor
$N$, and (2) the type substitution that replaces all formal type variables in
$N$ with the provided type arguments $\overline{t}$. For example, consider the
type constructor $N=\mathcal{T}\text{{{\tt<}}}\alpha\text{{{\tt>}}}:\top$ and
its type instance $t=N\text{{{\tt<}}}t_{2}\text{{{\tt>}}}$. In this example,
$\textit{decompose}(t)$ returns $\langle[\alpha\mapsto t_{2}],N\rangle$. For a
non polymorphic type $t$, type decomposition simply returns an empty
substitution and the input type $t$.

###  3.2. API Graph

We define an API directed graph as $G=(V,E)$, where $V$ is the set of nodes
corresponding to either a type $t\in\textit{Type}$ or an API definition
$d\in\textit{Def}$ (i.e., a method or a field), $E\subseteq V\times V\times L$
is the set of edges whereas $L=\Sigma$ is the set of edge labels (representing
the set of valid type substitutions). To construct the API graph we examine a
given API $\Lambda\in\textit{API}$ and proceed as follows.

  * •

Iterate over the set of classes in topological order with regards to their
inheritance chain. Convert every class $c$ into a type $t$ based on function
type defined in Figure 4, and add the resulting type $t$ into the graph. Then,
we iterate over each member (i.e., a function or a field) $d\in\textit{Def}$
belonging to class $c$ and proceed as follows.

  * •

Add node $d$ to the API graph.

  * •

Add edge $t\overset{\epsilon}{\rightarrow}d$ to the API graph, if $d$ is an
_instance_ method or a field of the class $c$ and $t=\textit{type(c)}$.

  * •

Add edge $d\overset{\sigma}{\rightarrow}r^{\prime}$ to the API graph, if $r$
is the return type of $d$ and
$\textit{decompose}(r)=\langle\sigma,r^{\prime}\rangle$ according to
Definition 3.3.

⬇

1class Utils {

2 static <X> List<X> createList();

3}

4class List<T> {

5 List(int size);

6 boolean add(T elem);

7 Set<T> toSet();

8}

9class Set<E> {

10 Set(int size);

11 boolean add(E elem);

12 List<E> toList();

13}

Figure 5. An example API written in Groovy and its API graph. Oval nodes
represent types, while rectangular nodes denote definitions (e.g., methods).

Conceptually, the set of edges determines the following relationships. The
edge $t\overset{\epsilon}{\rightarrow}d$ indicates that the definition $d$ is
applied to a value of type $t$ (receiver type). The edge
$d\overset{\sigma}{\rightarrow}r^{\prime}$ denotes that the application of the
API definition $d$ returns the type given by $\sigma r^{\prime}$. For example,
consider a method $m$ whose return type is List<String>. In this scenario, we
add the following edge to the API graph:
$m\overset{\alpha\mapsto\texttt{String}}{\rightarrow}\texttt{List}\text{{{\tt<}}}\alpha\text{{{\tt>}}}$,
where the target node of the edge is the type constructor List. In a similar
manner, when the return type of method $m$ is a non-polymorphic type, such as
Int, decopose(Int) yields $\langle\epsilon,\texttt{Int}\rangle$. Therefore, we
add the edge $m\overset{\epsilon}{\rightarrow}\texttt{Int}$ to the graph. In
our examples, we use the shorthand $v_{1}\rightarrow v_{2}$ for
$v_{1}\overset{\epsilon}{\rightarrow}v_{2}$.

The API graph is directly inspired by the signature graph introduced in the
program synthesis work of Mandelin et al. (2005). In a similar manner to our
API graph, the signature graph encodes API components as unary functions
taking one input type (receiver type), and producing an output type (return
type). The intuition behind this is the identification of chains of method
calls/field accesses (e.g., x.f1.m1().f2...) that lead to a specific type
$t_{\textit{out}}$. This can be achieved by simply querying the graph for
paths between an input type $t_{\textit{in}}$ and the target type
$t_{\textit{out}}$ using standard graph reachability algorithms, such as
Dijkstra’s algorithm.

However, the presence of polymorphic components complicates this
straightforward approach. Our API graph addresses this by refining the
signature graph: we label edges with type substitutions, allowing us to handle
parametric polymorphism without compromising the size of the API graph. Our
detailed approach for identifying chains of method calls/field accesses in the
presence of parametric polymorphism is explained later in Section 3.4.

Example: Figure 5 shows an example API (written in Groovy) and its API graph.
The API graph contains seven definitions (i.e., methods) depicted with gray
color. Three definitions have no incoming edges, as their application does not
require a receiver object. Two of them (i.e., List<K>(int), Set<V>(int)) stand
for the constructors of the generic classes List and Set respectively (lines
4, 9), while one of them is for the static polymorphic method of class Utils.
Finally, the example API graph includes three types represented by oval nodes,
two of which denote the type constructors List and Set, while one type node
corresponds to boolean.

###  3.3. API Enumeration Problem Formulation

Having presented the notion of API graph (Section 3.2), we now formulate the
problem of API enumeration. API enumeration systematically explores all the
unique typing combinations that can be used to invoke a particular API
component, such as a function or a field. The intuition is that invoking an
API component through different typing patterns lets us exercise the
implementation of many type-related operations in the compiler, including,
subtyping rules, or method resolution. In what follows, we use an API graph as
our typing environment. In fact, an API graph can help type expressions that
use API components, because the type signatures of every API entity is
included in $G$. For example, hereafter, $G\vdash e.f:t$ means that the type
of the field access $e.f$ is $t$. This typing process is based on the type
signature of field $f$ found in $G$.

We first introduce  _abstract typed expressions_ , an abstraction over the
domain of expressions defined in API-IR (Figure 4). An abstract typed
expression is given by:  $\hat{e}\in\hat{\textit{Expr}}$ $[t]$ $[t].f$
$[t_{1}].m\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}(\overline{[t_{2}]})$
$\text{{{\tt local var}}}\ x:t=\hat{e}$ The notation $[t]$ represents an
_inhabitant_ of type $t$ (Urzyczyn, 1997), that is any concrete expression
$e\in\textit{Expr}$ whose type is $t$. An abstract typed expression hides the
contents and the value of a concrete expression $e$, and considers only the
type of $e$. For example, the abstract expression $[t].f$ indicates a field
$f$ accessed through  _any_ expression of type $t$. We encode every abstract
typed expression $\hat{e}$ using _typing sequences_. A typing sequence
succinctly captures the types found within the holes of abstract typed
expressions. A typing sequence is denoted by the symbol
$\llbracket\rrbracket$:

$\displaystyle\llbracket[t]\rrbracket$ $\displaystyle\rightarrow\langle
t\rangle$ $\displaystyle\llbracket[t].f\rrbracket$
$\displaystyle\rightarrow\langle t,\bot\rangle$
$\displaystyle\llbracket[t_{1}].m\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}(\overline{[t_{2}]})\rrbracket$
$\displaystyle\rightarrow\langle t_{1},\overline{t_{2}}\rangle$
$\displaystyle\llbracket\text{{{\tt local var}}}\ x:t=\hat{e}\rrbracket$
$\displaystyle\rightarrow\llbracket\hat{e}\rrbracket\boldsymbol{\cdot}t$

In the preceding rules, the symbol $\boldsymbol{\cdot}$ means appending an
element to the end of a sequence. A singleton sequence consisting of type $t$
represents an inhabitant of $t$. When a typing sequence contains more than two
types, the first element of the sequence stands for the receiver type of a
field access/method call, and the remaining elements correspond to the
parameter types of the application (if any). Finally, in the case of local
variable definitions, the final element of the typing sequence is the expected
type of the entire abstract expression found on the right-hand side.

We define a concretization function $\gamma$ that allows us to map a typing
sequence and an API definition $d$ into a set of concrete expressions written
in API-IR under a given type substitution $\sigma$.

###### Definition 3.4.

Let
$\gamma:G,\textit{Def},\textit{Type}\times\dots\times\textit{Type}\times\Sigma\longrightarrow\mathcal{P}(\textit{Expr})$
such that:

$\displaystyle\gamma(G,\bot,\langle t\rangle,\sigma)$ $\displaystyle=\\{e\ |\
G\vdash e:t\\}$ $\displaystyle\gamma(G,\text{{{\tt var}}}\ f:t,\langle
t,\bot\rangle,\sigma)$ $\displaystyle=\\{e.f\ |\ G\vdash e:t\\}$
$\displaystyle\gamma(G,\text{{{\tt fun}}}\
m\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}(\overline{x:p}):t,\langle
r,\overline{p^{\prime}}\rangle,\sigma)$
$\displaystyle=\left\\{e_{1}.m\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}(\overline{e_{2}})\
\middle|\ \begin{aligned} &G\vdash
e_{1}:r,G\vdash\overline{e_{2}}:\overline{p^{\prime}},\\\
&\overline{t}=(\sigma(\alpha_{i}))_{i=1}^{n}\end{aligned}\right\\}$
$\displaystyle\gamma(G,d,s\boldsymbol{\cdot}t,\sigma)$
$\displaystyle=\\{\text{{{\tt local var}}}\ x:t=e\ |\
e\in\gamma(G,d,s,\sigma)\\}$

The function $\gamma$ concretizes abstract typing sequences and definitions
into specific expressions that are typed under a given API graph and a type
substitution. When no API entity is provided to $\gamma$ (i.e., its second
parameter is $\bot$), the function returns all the inhabitants of type $t$.
This translates to every expression $e\in\textit{Expr}$ that satisfies
$G\vdash e:t$. Conversely, if an API component $d$ is provided, $\gamma$
yields all the possible expressions that invoke the definition $d$ with
respect to the given typing sequence $s$. For example, consider the field
$\text{{{\tt var}}}\ f:t$ and the typing sequence $s=\langle r,\bot\rangle$.
In this case, the function $\gamma$ gives all accesses of field $f$ via every
inhabitant of type $r$. When encountering a polymorphic function, $\gamma$
maps every formal type variable of the function into actual type arguments
attached to the resulting method calls based on the provided type
substitution, in particular $(\sigma(\alpha_{i}))_{i=1}^{n}$. Later, in
Section 3.4, we present an under-approximation of $\gamma$ called
$\hat{\gamma}$, introduced to address the practical concerns associated with
exhaustively enumerating all potential expressions in $\gamma$.

###### Definition 3.5 (API typing sequence).

Given an API component $d\in\textit{Def}$, the sequence $s_{d}$ is called an
_API typing sequence_ of $d$ when there is _an abstract typed expression_
$\hat{e}$, such that (1) $\llbracket\texttt{local var}\
x:t=\hat{e}\rrbracket=s_{d}$, and (2) the abstract expression $\hat{e}$
invokes the component $d$. We say that an expression $e\in\textit{Expr}$
_realizes_ the API typing sequence $s_{d}$ under the substitution $\sigma$, if
$e\in\gamma(G,d,s_{d},\sigma)$.

Based on Definition 3.5, an API typing sequence $s_{d}$ reveals two key
details: First, _how_ a set of types are combined together to invoke and use a
certain API component $d$ (represented by all elements of $s_{d}$ except the
last). Second, _what_ is the expected type that derives from the usage of $d$
(indicated by the last element of $s_{d}$).

Example: Consider two typing sequences for the method $d=\texttt{add(T)}$
defined in Figure 5 (line 6):
$s_{d_{1}}=\langle\bot,\texttt{int},\texttt{boolean}\rangle$ and
$s_{d_{2}}=\langle\texttt{List<Int>},\texttt{int},\texttt{boolean}\rangle$.
Listing LABEL:lst:example-listing contains three expressions that realize
$s_{d_{1}}$ and $s_{d_{2}}$. The first expression (although type incorrect)
realizes $s_{d_{1}}$, because the first element of $s_{d_{1}}$ (denoted as
$s_{d_{1}}\downarrow_{1}$) is $\bot$, which represents the absence of
receiver. The last two expressions of the listing realize the same API typing
sequence $s_{d_{2}}$, because the type of both new List<Int>(10) and
Utils.<Int>createList() is $s_{d_{2}}\downarrow_{1}=\texttt{List<Int>}$.

Listing 1: Expressions that realize typing sequences of method List.add(T).

⬇

1boolean x = add(1);

2boolean y = Utils.<Int>createList().add(1);

3boolean z = new List<Int>(10).add(1);

###### Definition 3.6 (API signature).

API signature
($G\times\textit{Def}\longrightarrow\textit{Type}\times\dots\times\textit{Type}$)
is a function that maps an API graph $G=(V,E)$ and one API definition $d\in V$
to a typing sequence as follows:

sig(G, var x: t) $\displaystyle=\langle r,\bot,t\rangle$
$\displaystyle\text{if }r\overset{l}{\rightarrow}d\in E$ sig(G, var x: t)
$\displaystyle=\langle\bot,\bot,t\rangle$ $\displaystyle\text{if }d\ \text{has
no incoming edges in }G$ $\displaystyle\textit{sig}(G,\texttt{fun}\
m\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}(\overline{x:p}):t)$
$\displaystyle=\langle r,\overline{p},t\rangle$ $\displaystyle\text{if
}r\overset{l}{\rightarrow}d\in E$ $\displaystyle\textit{sig}(G,\texttt{fun}\
m\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}(\overline{x:p}):t)$
$\displaystyle=\langle\bot,\overline{p},t\rangle$ $\displaystyle\text{if }d\
\text{has no incoming edges in }G$

For example, the API signature of the Utils.createList() method of Figure 5
(line 2) is
$\langle\bot,\bot,\texttt{List}\text{{{\tt<}}}X\text{{{\tt>}}}\rangle$. The
method is static and takes no parameters. That is why the first element
(receiver type) and the second element (parameter type) of the resulting
sequence are $\bot$.

###### Definition 3.7 (Well-typed API typing sequence).

Given an API graph $G$, a definition $d\in\textit{Def}$, and a type
substitution $\sigma\in\Sigma$, we say that an API typing sequence
$s_{d}=\langle r,\overline{p},t\rangle$ is  _well-typed_ under $G$ and
$\sigma$, if $\textit{sig(G,
d)}=(r^{\prime},\overline{p^{\prime}},t^{\prime})$ and $r<:\sigma
r^{\prime},\overline{p}<:\sigma\overline{p^{\prime}}$, and $t>:\sigma
t^{\prime}$.

In essence, this definition captures precisely the notion that given an API
component $d$, a typing sequence $s_{d}$ is well-typed under $\sigma$, if
$s_{d}$ describes a usage of $d$ with: (1) a receiver whose type $r$ is a
subtype of the formal receiver type extracted from the signature of $d$
($r<:\sigma r^{\prime}$), and (2) arguments (if present) whose types are
subtypes of the formal parameter types of $d$. Finally, the expected type of
$d$’s application should be any supertype of $d$’s formal return type.

###### Theorem 3.8.

Consider an API component $d\in\textit{Def}$, one well-typed typing sequence
$s_{d}$ of $d$, and a substitution $\sigma$. The programs derived from
$s_{d}$, that is $\gamma(G,d,s_{d},\sigma)$, are well-typed.

###### Proof.

This follows straightforwardly from Definition 3.4 and the typing rules of
API-IR. ∎

Example: Consider again the method $d=\texttt{add}(T)$ defined in the List
class of our example API (Figure 5, line 6). Also, consider a substitution
$\sigma=[T\mapsto{\tt Int}]$. The API typing sequence
$s_{d}=\langle\texttt{List<Int>},\texttt{Int},\texttt{boolean}\rangle$ is
well-typed under $\sigma$, because (1)
$\texttt{List<Int>}<:[T\mapsto\texttt{Int}]\texttt{List}\text{{{\tt<}}}T\text{{{\tt>}}}$,
(2) $\texttt{Int}<:[T\mapsto\texttt{Int}]T$, and (3)
$\texttt{boolean}>:[T\mapsto\texttt{Int}]\texttt{boolean}$. Hence, all the
concrete expressions that come from $s_{d}$, such as the last two expressions
of Listing LABEL:lst:example-listing, are well-typed.

###### Definition 3.9 (API enumeration).

Consider an API graph $G$ and an API component $d$ included in $G$. For every
type substitution $\sigma\in\Sigma$, API enumeration computes exhaustively a
set of  _well-typed_ API typing sequences $S_{d}$ under $\sigma$ such that for
every $s_{d}\in S_{d}$, we obtain a program $p\in\gamma(G,d,s_{d},\sigma)$.

The algorithm of API enumeration first enumerates  _all_ valid type
substitutions that instantiate the type variables of an API definition. Given
that in the presence of polymorphic types, substitutions are infinite
(consider List<List<List<…>>>), API enumeration can be set to produce all type
substitutions up to a certain depth. This is done by instantiating each type
variable with every concrete type found in a given API, including type
instances. For example, when it comes to enumerating all type substitutions of
length two, the result set includes a type of the form List<List<Int>>, but
not List<List<List<Int>>> (as the depth in this case is three). Based on a
substitution $\sigma$ and a library component $d$ with signature $\langle
r,p_{1}\dots p_{n},t\rangle$, API enumeration generates the Cartesian product
of sets $R,P_{1},\dots P_{n},T$, where $R$ is the set consisting of subtypes
of $\sigma r$, $P_{i}$ is the set consisting of subtypes of $\sigma p_{i}$
(with $1\leq i\leq n$), and $T$ is the set containing the supertypes of
$\sigma t$. API enumeration is exponential in terms of the number of types
included in the signature of $d$. For example, consider a substitution
$\sigma$ and an API signature that specifies four types: $\langle
r,p_{1},p_{2},t\rangle$. Each of $\sigma r$, $\sigma p_{1}$, and $\sigma
p_{2}$ contains ten subtypes, while there are also ten supertypes of $\sigma
t$. API enumeration gives $10^{4}=\sepnum{.}{,}{}{10000}$ well-typed typing
sequences under $\sigma$.

[x=0.75pt,y=0.75pt,yscale=-1,xscale=1] (8,110) node [anchor=north west][inner
sep=0.75pt] [align=left] $R_{m}=\\{A,B\\},P_{m}=\\{B\\},T_{m}=\\{A,B\\}$
$\sigma=\epsilon$

⬇

class A {

B m(B x);

}

class B extends A {}

; (190,150) node [align=left] $R_{m}\times P_{m}\times T_{m}=$ ; (270,100)
node [anchor=north west][inner sep=0.75pt] [align=right] $s_{m_{1}}=\langle
A,B,B\rangle$; (270,125) node [anchor=north west][inner sep=0.75pt]
[align=right] $s_{m_{2}}=\langle B,B,B\rangle$; (270,150) node [anchor=north
west][inner sep=0.75pt] [align=right] $s_{m_{3}}=\langle A,B,A\rangle$;
(270,175) node [anchor=north west][inner sep=0.75pt] [align=right]
$s_{m_{4}}=\langle B,B,A\rangle$; (370,95) node [anchor=north west][inner
sep=0.75pt] [align=right]

⬇

B res = new A().m(new B());

; ; (370,120) node [anchor=north west][inner sep=0.75pt] [align=right]

⬇

B res = new B().m(new B());

; (370,145) node [anchor=north west][inner sep=0.75pt] [align=right]

⬇

A res = new A().m(new B());

; (370,170) node [anchor=north west][inner sep=0.75pt] [align=right]

⬇

A res = new B().m(new B());

; [->] (230, 148) -- (270, 110); [->] (230, 148) -- (270, 135); [->] (230,
148) -- (270, 155); [->] (230, 148) -- (270, 180); [->] (340, 105) -- (365,
105) node[midway, above] $\gamma$; [->] (340, 130) -- (365, 130) node[midway,
above] $\gamma$; [->] (340, 155) -- (365, 155) node[midway, above] $\gamma$;
[->] (340, 180) -- (365, 180) node[midway, above] $\gamma$;

Figure 6. Enumerating well-typed API typing sequences for method B m(B x)
using substitution $\sigma=\epsilon$. The set $R_{m}$ contains the subtypes of
the formal receiver type of m, $P_{m}$ contains the subtypes of the first
formal parameter type of m, while $T_{m}$ contains the supertypes of the
return type of m. Using the function $\gamma$, each typing sequence leads to
programs that invoke method m via a unique typing pattern. This, in turn,
triggers various type-related operations in the compiler.

Example: Figure 6 illustrates the concept of API enumeration for the non-
polymorphic method B m(B x). Based on the signature of method m, we compute
the sets $R_{m}$, $P_{m}$, and $T_{m}$, and then we take their Cartesian
product. Each element of this product corresponds to a well-typed API typing
sequence, which eventually leads to concrete programs that invoke method m
through a unique typing combination. For example, the type of the receiver in
the first program is A, while the type of the receiver in the second program
is type B. API enumeration for polymorphic components follows a similar
process by enumerating well-typed API sequences under every valid type
substitution.

Enumerating ill-typed API typing sequences: An API typing sequence $s_{d}$ of
a definition $d$ is considered ill-typed when at least one enclosing type of
the sequence is  _incompatible_ with the signature of $d$. Consider an API
graph $G$, a definition $d$, and a substitution $\sigma$. An API typing
sequence $s_{d}=\langle r,\overline{p},t\rangle$ is ill-typed under $G$ and
$\sigma$, if $\textit{sig}(G,d)=\langle
r^{\prime},\overline{p^{\prime}},t^{\prime}\rangle$ and $r\not{<:}\sigma
r^{\prime}$ and $r\not{>:}\sigma r^{\prime}$, or
$\overline{p}\not{<:}\sigma\overline{p^{\prime}}$, or $t\not{>:}\sigma
t^{\prime}$. Notice that a receiver type is incompatible when it is neither a
supertype nor a subtype of the formal receiver type. This happens to avoid
constructing a well-typed sequence due to inheritance. In a similar manner to
Theorem 3.8, the programs derived from ill-typed API typing sequences are ill-
typed. Consider again the method $d=\texttt{List.add(T)}$ of Figure 5. Under
the substitution $\sigma=[T\mapsto{\tt Int}]$, the sequence
$s_{d}=\langle\texttt{List<Int>},\texttt{String},\texttt{boolean}\rangle$ is
ill-typed, because $\texttt{String}\not{<:}[T\mapsto\texttt{Int}]T$. An
expression that realizes this sequence is deemed ill-typed:

⬇

boolean x = Utils.<Int>createList("str value") // String is incompatible to
Int

###  3.4. Concretization of API Typing Sequences

Every API typing sequence that arises from API enumeration is converted into a
concrete test program. We present a method that  _under-approximates_ the
concretization function $\gamma$ presented in Definition 3.4. To identify type
inhabitants, our method examines the API graph and enumerates all paths that
reach a certain type $t$. Each path represents an inhabitant consisting of a
chain of method calls or field accesses. In the presence of parametric
polymorphism, some paths are infeasible, as the underlying type variables
found in these paths are instantiated with incompatible types that do not
ultimately lead to a given type $t$. We explain the details on how we
determine the feasibility of each path and properly instantiate the
corresponding type variables.

⬇

1class Utils {

2 static <X, Y> Map<X, Y> mapOf();

3 static Map<String, String> mapOfStrs();

4}

5class Map<K, V> {

6 Set<K> keySet();

7}

8class Set<E> {}

Figure 7. An API relying on parametric polymorphism and its API graph.

Finding type inhabitants via API graph reachability: In the simplest scenario,
where parametric polymorphism is not present, finding inhabitants of a type
$t$ is given by standard graph reachability algorithms that compute the set of
paths that reach node $t$ (Mandelin et al., 2005). However, parametric
polymorphism complicates the process, making the simple path search yield
incorrect results. To illustrate this, consider the API and its corresponding
API graph of Figure 7. Now assume that we want to find an inhabitant of
polymorphic type Set<Int>. The naïve path search identifies two potential
paths that reach the type constructor Set: path (1) and path (2). The
expression mapOfStrs().keySet(), which originates from path (1) ${\tt
Utils.mapOfStrs()}\rightarrow{\tt
Map}\text{{{\tt<}}}K,V\text{{{\tt>}}}\rightarrow{\tt keySet()}\rightarrow{\tt
Set}\text{{{\tt<}}}E\text{{{\tt>}}}$, leads to an incompatible type
Set<String>. In contrast, path (2) ${\tt
Utils.mapOf}\text{{{\tt<}}}X,Y\text{{{\tt>}}}{\tt()}\rightarrow{\tt
Map}\text{{{\tt<}}}K,V\text{{{\tt>}}}\rightarrow{\tt keySet()}\rightarrow{\tt
Set}\text{{{\tt<}}}E\text{{{\tt>}}}$ involves a polymorphic function
(Utils.mapOf). The expression from path (2) is correctly identified as an
inhabitant of Set<Int> _only_ if the type variable $X$ defined in Utils.mapOf
is instantiated with type Int. To identify infeasible paths and properly
instantiate type variables of polymorphic components, we now present a refined
path search approach that deals with parametric polymorphism.

Every path in an API graph may consist of polymorphic API components. Every
polymorphic component introduces some type variables. In the above example,
path (1) introduces type variables $K,V$ and $E$. Similarly, path (2)
introduces type variables, $X,Y,K,V$, and $E$. The labels (aka substitutions
---recall Section 3.2) found on top of each edge indicate instantiations of
the corresponding type variables. However, a path may also contain free type
variables whose instantiation is not given by such substitutions. For example,
path (1) of Figure 7 contains no free type variables, as both type variables
$K$ and $V$ are instantiated with String while type variable $E$ is
instantiated with type $K$. On the other hand, path (2) involves two free type
variables, namely, $X$ and $Y$. These type variables do not participate in the
left-hand side of a substitution. From now onwards, given a path $p$, we use
the notation TypeVar(p) to obtain the set of type variables of path $p$. To
take the set of free type variables of a path $p$, we use the symbol
$\textit{FV}(p)$.

###### Definition 3.10.

Let a type $t$ and its decomposition
$\textit{decompose}(t)=\langle\sigma,t^{\prime}\rangle$. Given an API graph
$G$, we say that a path $p$  _forms_ an inhabitant of type $t$, when (1) the
path $p$ leads to target node $t^{\prime}$, and (2) there is a _a valid_
substitution $\sigma^{\prime}$, such that
$\forall\alpha\in\textit{TypeVar(p)}.\ \alpha\in\textit{Dom}(\sigma^{\prime})$
and $\sigma\sqsubseteq\sigma^{\prime}$. Our goal is then to find the set of
paths $P$ so that every path $p\in P$ forms an inhabitant of type $t$.

The definition above summarizes the problem of path search, which aims to find
type inhabitants even in the presence of polymorphic types. Given a target
type $t$, we initially decompose it into a substitution $\sigma$ and a type
$t^{\prime}$ according to Definition 3.3. Then, we search the API graph $G$ to
find the set of paths that reach node $t^{\prime}$. A path $p$ forms a type
inhabitant if there is a  _valid_ substitution $\sigma^{\prime}$ (recall
Definition 3.1) that includes every type variable in TypeVar(p), and subsumes
the original substitution $\sigma$ according to Definition 3.2
($\sigma\sqsubseteq\sigma^{\prime}$). Conceptually, the substitution $\sigma$
that we obtain after performing the type decomposition on $t$, _constrains_
the instantiation of some type variables found in path $p$. Therefore, we need
to ensure that the substitution $\sigma^{\prime}$ contains compatible
assignments for the type variables included in $\sigma$. If no such valid
substitution $\sigma^{\prime}$ exists, then we consider the path as
_infeasible_ : it cannot yield an expression of the target type $t$.

Example: Consider again the API graph of Figure 7 and the problem of finding
inhabitants of type Set<Int>. This type is decomposed into the substitution
$\sigma=[E\mapsto{\tt Int}]$ and the type constructor Set<E>. Again, there are
two paths that reach the type constructor Set. Path (1) is infeasible as the
only substitution $\sigma$ that stems from this path is
$\sigma^{\prime}=[K\mapsto{\tt String},V\mapsto{\tt String},E\mapsto{\tt
String}$], which is incompatible with $\sigma$, because
$\sigma(E)\neq\sigma^{\prime}(E)$. On the other hand, path (2) is feasible
because there exists a substitution $\sigma^{\prime}$ such that
$\sigma\sqsubseteq\sigma^{\prime}$. Specifically, we have
$\sigma^{\prime}=[X\mapsto{\tt Int},Y\mapsto{\tt String},K\mapsto{\tt
Int},Y\mapsto{\tt String},E\mapsto{\tt Int}]$, as
$\sigma(E)=\sigma^{\prime}(E)={\tt Int}$.

1 fun  _find_API_paths(_$G,t$_)_=

2 $\langle\sigma,t^{\prime}\rangle\leftarrow\textit{decompose(t)}$

3 $\textit{paths}\leftarrow\\{\langle\langle t\rangle,\bot\rangle\\}$

4 for  _$p\in\textit{Paths}(G,t^{\prime})$_ do

5 $\textit{sub}\leftarrow\textit{gather all substitutions of path p}$

6 $\sigma^{\prime}\leftarrow\textit{perform constant propagation on }\sigma\
\textit{based on }\textit{subs}$

7 $t_{2}\leftarrow\sigma^{\prime}t^{\prime}$

8 $\sigma_{1}\leftarrow\textit{unify}(t,t_{2})$

9 if  _$\sigma_{1}=\epsilon$_ then continue

10 $\sigma_{2}\leftarrow\forall\alpha\in\textit{FV}(p).\ \textit{instantiate
}\alpha\>\>\>\textit{if }\alpha\not\in\sigma_{1}$

11 $\sigma^{\prime}\leftarrow\sigma_{1}\cup\sigma_{2}$

12 $\textit{paths}\leftarrow\textit{paths}\cup\\{\langle
p,\sigma^{\prime}\rangle\\}$

13

14 return _paths_

Algorithm 1 Algorithm for finding paths that form inhabitants of type $t$

(a) An infeasible path.

(b) An inhabitant of Set<Int>.

Figure 8. Determining which of the paths in the API graph of Figure 7 form an
inhabitant of type Set<Int>.

Algorithm: Algorithm 1 outlines our method for identifying paths that form
inhabitants of a given type. We describe the algorithm in the context of
finding inhabitants of Set<Int> based on the API graph shown in Figure 7. The
algorithm takes as input an API graph $G$ and a type $t$, and returns a set of
pairs, where each pair consists of a path and a substitution. The algorithm
starts with decomposing the given type $t$ into a substitution $\sigma$ and
another type $t^{\prime}$. Then, it enumerates all  _acyclic_ paths that reach
node $t^{\prime}$. In our example, the are two paths that reach the type
constructor Set---each of those paths is shown individually in Figure 8.

It is now time to determine which of the available paths are feasible. For
every path $p$, the algorithm examines and gathers all substitutions (i.e.,
edge labels) found in $p$ (line 5). For example, the first path (Figure 8(a))
contains three substitutions (e.g., $[K\mapsto{\tt String},V\mapsto{\tt
String},E\mapsto T]$), while the second path (Figure 8(b)) includes the
following substitutions: $[K\mapsto X,V\mapsto Y,E\mapsto K]$. Next, the
algorithm performs constant propagation on the collected substitutions and
creates a new substitution $\sigma^{\prime}$ (line 6). For example, the
substitution of path (1) becomes $\sigma^{\prime}=[K\mapsto{\tt
String},V\mapsto{\tt String},E\mapsto{\tt String}]$, while the substitution
when handling path (2) is $[K\mapsto X,V\mapsto Y,E\mapsto X]$. Using the new
substitution $\sigma^{\prime}$, we create a new type $t_{2}$ that is given by
$\sigma^{\prime}t^{\prime}$. For example, for the path of Figure 8(a) $t_{2}$
is Set<String>, while $t_{2}$ stands for Set<X> when dealing with the path of
Figure 8(b). Then, the algorithm unifies the type $t_{2}$ with the target type
$t$ (line 8). Essentially, this type unification operation identifies
assignments for the free type variables of path $p$ so that the resulting type
of the path expression is compatible with the target type $t$. If the two
types are not unifiable, the path is considered infeasible, and the algorithm
proceeds to the next iteration (line 9). For example, the type
$t_{2}=\texttt{Set<String>}$ of Figure 8(a) is not unifiable with the target
type Set<Int>. This means that path (1) is an infeasible path, not leading to
an expression of type Set<Int>. When the types are unifiable, the outcome of
type unification ($\sigma_{1}$\---line 8) instantiates some of the free type
variables of $p$. For example, consider again Figure 8(b): the algorithm
unifies types Set<Int> and Set<X> by returning the substitution
$\sigma_{1}=[X\mapsto{\tt Int}]$.

In the final step, the algorithm instantiates any free type variables of $p$,
not instantiated by the previous unification operation (line 10). Such free
type variables do  _not_ affect the type of the underlying expression and
therefore, the algorithm is free to instantiate them with any valid type that
respects their upper bounds. For example, $Y$ is another free type variable
that stems from the path of Figure 8(b). The algorithm instantiates it with a
randomly selected type, e.g., String. The final substitution $\sigma^{\prime}$
is then the union of substitutions $\sigma_{1}$ and $\sigma_{2}$ (line 11).
The final substitution and the corresponding path $p$ are added to the set $P$
(line 12). For example, the path of Figure 8(b) forms an inhabitant of type
Set<Int> if using the substitution $[X\mapsto{\tt Int},Y\mapsto{\tt
String},K\mapsto{\tt Int},V\mapsto{\tt String},E\mapsto{\tt Int}]$.

Termination: The function Paths(G, t) on line 4 of Algorithm 1 enumerates all
paths in graph $G$ that reach the target node $t$. Since an API graph may
contain cycles, there might be an infinite number of paths. To tackle this, we
consider only acyclic paths, which are guaranteed to be finite.

1 fun  _inhabitants(_$G,t$_)_=

2 $\textit{inhabitants}\leftarrow\emptyset$

3 for  _$\langle p,\sigma\rangle\in{\tt find\\_API\\_paths}(G,t)$_ do

4
$\textit{inhabitants}\leftarrow\textit{inhabitants}\cup\textit{2expr}(p,\sigma)$

5

6 return _inhabitants_

Algorithm 2 Algorithm for converting paths into concrete expressions

Converting a path into an expression: Having computing the set of paths that
form inhabitants of a type $t$, we employ Algorithm 2 to convert every path
into a concrete expression. The algorithm employs the function 2expr, which
given an API graph $G$, and a substitution $\sigma$, converts a path $p$ into
an expression as follows:

$\displaystyle\textit{2expr}(G,p\boldsymbol{\cdot}\text{{{\tt fun
}}}m\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}(\overline{x:p}):t,\sigma)$
$\displaystyle=\textit{2expr}(G,p,\sigma).m\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}(\overline{e})$
where $\displaystyle\begin{aligned} &\overline{e}=e_{i}\in{\tt
inhabitants}(G,\sigma p_{i}),\forall i\in\\{1\dots n\\}\\\
&\overline{t}=(\sigma(\alpha_{i}))_{i=1}^{n}\end{aligned}$
$\displaystyle\textit{2expr}(G,p\boldsymbol{\cdot}\text{{{\tt var
}}}f:t,\sigma)$ $\displaystyle=\textit{2expr}(G,p,\sigma).f$
$\displaystyle\textit{2expr}(G,d,\sigma)$ $\displaystyle=\textit{constant}(d)$
$\displaystyle\text{if }d\in\textit{Type}$
$\displaystyle\textit{2expr}(G,p\boldsymbol{\cdot}d,\sigma)$
$\displaystyle=\textit{2expr}(G,p,\sigma)$ $\displaystyle\text{if
}d\in\textit{Type}$ $\displaystyle\textit{2expr}(G,[],\sigma)$
$\displaystyle=\epsilon$

For a path consisting of a single type node, the function 2expr simply returns
a constant expression $\textit{constant}(t)$, which is typically translated
into a cast null expression (e.g., ???.asInstanceOf[T] in Scala). Type nodes
found in intermediate positions within a path are ignored. To illustrate this
path conversion process, consider the path of Figure 8(b). When using the
substitution $[X\mapsto{\tt Int},Y\mapsto{\tt String}]$, this path results in
the expression Utils.mapOf<Int, String>().keySet().

Realization of $\gamma$: Based on the aforementioned definitions and
algorithms, we finally present the realization of the concretization function
$\gamma$, previously shown in Definition 3.4. The function $\gamma$ is an
abstract concept that generates  _all_ API-IR expressions that originate from
a given typing sequence and an API graph. Our realization function called
$\hat{\gamma}$ under-approximates the behavior of $\gamma$, meaning that for a
given API graph $G$, a typing sequence $s_{d}$, an API component $d$, and a
type substitution, we have
$\hat{\gamma}(G,s_{d},d,\sigma)\subseteq\gamma(G,s_{d},d,\sigma)$. To do so,
the $\hat{\gamma}$ function relies on Algorithm 2 as follows:

###### Definition 3.11.

Let
$\hat{\gamma}:G,\textit{Def},\textit{Type}\times\dots\times\textit{Type}\times\Sigma\longrightarrow\mathcal{P}(\textit{Expr})$
such that:

$\displaystyle\hat{\gamma}(G,\bot,t,\sigma)$ $\displaystyle=\\{e\ |\
e\in\texttt{inhabitants}(G,t)\\}$ $\displaystyle\hat{\gamma}(G,\text{{{\tt
var}}}\ f:t,\langle t,\bot\rangle,\sigma)$ $\displaystyle=\\{e.f\ |\
e\in\texttt{inhabitants}(G,t)\\}$ $\displaystyle\hat{\gamma}(G,\text{{{\tt
fun}}}\
m\text{{{\tt<}}}\overline{\alpha}\text{{{\tt>}}}(\overline{x:p}):t,\langle
r,\overline{p^{\prime}}\rangle,\sigma)$
$\displaystyle=\left\\{e_{1}.m\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}(\overline{e_{2}})\
\middle|\ \begin{aligned} &e_{1}\in{\tt inhabitants}(G,r)\\\
&\overline{e_{2}}=e_{2_{i}}\in{\tt inhabitants}(G,p_{i}^{\prime}),\\\ &\forall
i\in\\{1\dots
n\\},\overline{t}=(\sigma(\alpha_{i}))_{i=1}^{n}\end{aligned}\right\\}$
$\displaystyle\hat{\gamma}(G,d,s\boldsymbol{\cdot}t,\sigma)$
$\displaystyle=\\{\text{{{\tt local var}}}\ x:t\ |\
e\in\hat{\gamma}(G,d,s,\sigma)\\}$

###### Theorem 3.12 (Soundness).

Given an API graph $G$, an API definition $d\in\textit{Def}$, a typing
sequence $s$, and a substitution $\sigma$, if $\hat{\gamma}(G,d,s,\sigma)$
returns $E$, then $E\subseteq\gamma(G,d,s,\sigma)$.

###### Proof.

The theorem follows straightforwardly from lines 8–9 of Algorithm 1 as we
consider only paths that result in a type unifiable with the target type $t$.
∎

###### Theorem 3.13 (Completeness).

Given an API graph $G$, an API definition $d\in\textit{Def}$, a typing
sequence $s$, and a substitution $\sigma$,
$\hat{\gamma}(G,d,s,\sigma)\neq\emptyset$.

###### Proof.

This can be proven by Algorithm 1. The algorithm always returns a non-empty
solution, even if there is no path to the target type $t$. In this case, the
algorithm returns a singleton path containing the given type $t$ (line 3,
Algorithm 1), which is in turn translated into a constant expression according
to function 2expr. ∎

###  3.5. Type Erasure

Next, an API-IR expression obtained from an API typing sequence (Section 3.4)
is passed as input to the type erasure process. The objective is to remove
types from an API-IR expression, while still maintaining the type correctness
of the input expression. Type erasure helps our approach stress-test the
implementation of compiler type inference procedures (Chaliasos et al., 2022).

Type erasure aims to construct polymorphic invocations with no explicit type
arguments. Our method relies on local type inference algorithms (Pierce and
Turner, 2000), which are commonly supported by mainstream programming
languages. In the context of local type inference, the type arguments of
polymorphic invocations are deduced in a manner that satisfies two conditions:
(1) the method arguments must be compatible with the formal parameter types of
the method being invoked, and (2) the type of the entire polymorphic
invocation must be compatible with a target type derived from the surrounding
context.

Specifically, our type erasure process leverages the following key insight: a
type argument of a polymorphic invocation can be safely erased if it can be
inferred by either the arguments of the invocation, or the target type of the
invocation. At the same time, the explicit type argument should be the same as
its inferred counterpart. More formally:

###### Definition 3.14.

Consider an API graph $G$, a polymorphic method $m$ with signature
$\textit{sig}(G,m)=\langle r,\overline{p},t\rangle$ and its invocation
$e=r.m\text{{{\tt<}}}\overline{t}\text{{{\tt>}}}(\overline{e^{\prime}})$, a
target type $k$ for $e$, and a substitution $\sigma$ that maps every type
variable of method $m$ to their type arguments in $e$. We say that the type
argument of a type variable of method $m$ can be  _safely removed_ from
expression $e$, when:

  * •

$\sigma(\alpha)=\sigma^{\prime}(\alpha)$, where
$\sigma^{\prime}=\textit{unify}(k,t)$

  * •

or $\sigma(\alpha)=\sigma^{\prime}(\alpha)$, where
$\sigma^{\prime}=\bigcup_{i=1}^{n}\textit{unify}(p_{i}^{\prime},p_{i})$ and
$G\vdash\overline{e^{\prime}}:\overline{p^{\prime}}$

[constant] erasure(G, constant(t), t’) = constant(t) [field access] erasure(G,
e.f, t) = erasure(G, e, ⊥).f [method call] e = e_1.m<¯t>(¯e_2)
G ⊢¯e_2: ¯p

∀α∈TypeVar(m). the type argument of α can be safely erased from e when the
target type is k erasure(G, e, k) = erasure(G, e_1, ⊥).m(erasure(G, ¯e_2,
¯p)…) [local var] erasure(G, local var  x: t = e, t’) = local var  x: t =
erasure(G, e, t)

Figure 9. Defintion of type erasure. The erasure function
($G\times\textit{Expr}\times\textit{Type}\longrightarrow\textit{Expr}$) takes
an API graph, an expression $e$, and a target type $t$, and yields another
expression $e^{\prime}$ with erased type information.

Based on the preceding property, we define the function erasure
($G\times\textit{Expr}\times\textit{Type}\longrightarrow\textit{Expr}$), which
takes an API graph, an input expression $e$, and a target type $t$. It outputs
another expression with type information removed. The full definition of
erasure is shown in Figure 9. The function erasure is recursively applied to
any sub-expression included in $e$. When handling a method call $e$, the type
arguments are removed by erasure, but only when  _every_ type argument of the
call can be safely erased according to Definition 3.14 ([method call]).

Example: Consider the following code snippet:

⬇

1<T> void m1(T x) {}

2<X, Y> Y m2(X p1)

3m1<Object>("str");

4m1<String>("str");

5m2<String, String>("f");

6String x = m2<String, String>("str");

⬇

<T> void m1(T x) {}

<X, Y> Y m2(X p1)

m1<Object>("str"); // Not erased

m1("str"); // Erased

m2<String, String>("f"); // Not erased

String x = m2("str"); // Erased

After applying the (optional) function erasure, we get the method calls shown
on the right. erasure removes the type arguments from the second and fourth
polymorphic invocation (lines 4, 6), while the first and the third call remain
the same. Specifically, if we chose to erase the type argument of the first
call (line 3), the inferred type of T would become String, which is not
equivalent with the explicit type argument Object. Similarly, we do not remove
the type arguments from the method call on line 5, because the type argument
of type variable Y cannot be safely erased. This is because there is no target
type for the entire call that helps with the inference of Y.

Relation to hephaestus’ type erasure approach: Erasing types has proven useful
in finding bugs in type inference implementations, as demonstrated by the
hephaestus tool (Chaliasos et al., 2022). hephaestus comes with a mutation
that erases types from an  _existing_ program. In contrast, our approach
differs by incorporating type erasure directly into the synthesis process.
During the generation of a method call, we check whether the method call’s
type arguments can be omitted based on the inference rules outlined in Figure
9. Notably, integrating type erasure into the synthesis process makes our
approach efficient, as we further show in Section 4.5 of our evaluation. One
distinct difference is the overhead in hephaestus, which is attributed to an
intra-procedural analysis that preserves the type correctness of the input
program during the type erasure mutation.

###  3.6. Implementation and Discussion

Having presented the theory behind the main components of the approach, this
section focuses on noteworthy technical details. We have implemented our
techniques on top of hephaestus, the modern framework for testing compilers’
type checkers (Chaliasos et al., 2022). Our implementation, which we call
thalia, extends hephaestus using roughly .,5k additional lines of Python code.

The input of thalia is a set of JSON files that describe a given API. We have
developed an auxiliary script that automatically produces such JSON files by
parsing a library’s API documentation web pages (e.g., generated by javadoc)
via the beatifulsoup4 Python package. thalia then examines the input JSON
files and builds the corresponding API graph.

Producing typing sequences: API enumeration is exponential in terms of the
number of types found in the signature of an API component. To make API
enumeration practical, thalia employs randomization. When dealing with a
polymorphic API component $d$, thalia first generates a  _valid_ type
substitution $\sigma$ at random. Based on the randomly generated substitution
$\sigma$, thalia then computes the set $S_{d}$ containing the typing sequences
of $d$ as described in Section 3.3. thalia generates one test case for every
$s_{d}\in S_{d}$ by applying function $\hat{\gamma}(G,d,s_{d},\sigma)$ as
detailed in Section 3.4.

Enumerating API paths: To compute all simple paths that reach a specific node,
thalia employs Yen’s algorithm (Yen, 1971), which computes the $k$-shortest
loopless paths in a graph. During the concretization of an API typing
sequence, thalia invokes a variant of Algorithm 1 presented in Section 3.4.
thalia iterates over the paths given by Yen’s algorithm in a  _random_ order,
and rather than returning all feasible paths, thalia returns the first random
path that forms a type inhabitant.

API graph size: Intuitively, the input API affects the size of the underlying
API graph, and thus the scalability of our approach. However, as we show in
our evaluation, our tool can easily handle real-world APIs with more than
$25$k edges, and synthesize programs in milliseconds.

Incomplete APIs: Although our realization function $\hat{\gamma}$ (Section
3.4) always returns a non-empty set of expressions, we may be unable to
exercise a specific API component due to the presence of recursive bounds and
the use of an API with missing type information. To illustrate this, consider:

⬇

class A<T extends A<T>> { int getSize(); }

We are unable to produce a typing sequence that invokes getSize as we cannot
construct a proper receiver type derived from the type constructor A. This is
because, there is no valid instantiation of type variable T that is compatible
with the bound A<T>. This is unavoidable because the preceding API does not
contain subtypes of A (e.g., a subclass class B extends A<B>). To tackle this,
our enumeration skips all API entities for which we cannot produce well-typed
typing sequences.

Generalizability: thalia currently produces programs written in three popular
languages: Scala, Kotlin, and Groovy. Adding a new language requires (1) the
collection of its APIs, (2) the implementation of a parser that transforms the
string representation of a type (as it appears in the input JSON) into its in-
memory counterpart supported by API-IR, and (3) a translator to convert API-IR
programs into source files written in the target language.

Although our approach enables increased feature coverage (see Section 4.3), we
might encounter an API that exhibits type system-related features that are not
currently understood by API-IR. By default, we skip exercising API entities
that involve such unsupported features. As a result, our current
implementation might not be as effective for languages, such as Rust, OCaml,
or TypeScript because the type system of API-IR does not currently support
many of their core type system features, including currying, type aliases,
structural types, associated types or more expressive bound constraints.
However, the fundamental concepts of our approach (e.g., API enumeration) are
still applicable to any modern language, because APIs are ubiquitous. For
example, one has the option to enhance our API-IR language with new type-
related features. We have already done so to accommodate Scala’s higher-kinded
types, and Kotlin’s nullable types.

##  4\. Evaluation

Our evaluation answers the following research questions:

  1. RQ1

Is thalia effective in finding new compiler typing bugs? (Section 4.2)

Short answer: During a five-month period of developing thalia and testing
industrial-strength compilers, a total of .,84 bugs were detected by thalia.
Out of these, .,77 bugs have been confirmed or fixed.

  2. RQ2

What are the characteristics of the test cases generated by thalia? (Section
4.3)

Short answer: thalia’s test cases are concise, averaging only 11--13 lines of
code across various languages. To reveal bugs, these compact test cases
effectively combine key features, such as parametric polymorphism,
overloading, and higher-order functions. Rather than solely relying on a
generative process, these features originate from  _existing_ API definitions.

  3. RQ3

What is the impact of libraries and synthesis modes on the effectiveness of
thalia? (Section 4.4)

Short answer: Using diverse libraries as input seeds increases code coverage
across all tested compilers. Different synthesis settings further boost (1)
the bug-finding capability by uncovering 36 additional bugs, and (2) the line
coverage by up to $5$%--$11.9$% across all compilers. thalia scales well even
with libraries containing large APIs, with an average synthesis time (per
program) of $161$ to $256$ milliseconds, depending on the target language.

  4. RQ4

How does thalia compare to the state-of-the-art, namely hephaestus? (Section
4.5)

Short answer: thalia and hephaestus complement each other effectively. thalia
has detected at least 42 bugs missed by prior work. hephaestus and thalia
achieve similar code coverage. However, combining the results of both tools
significantly increases code coverage (up to 4.4%), demonstrating thalia’s
ability to test previously unexplored components.

###  4.1. Experimental Setup

Hardware and compiler versions: We performed all experiments on commodity
servers (32 cores and 64 GB of RAM per machine) running Ubuntu 22.04 (x86_64).
Our testing efforts focused on the compilers of Groovy, Kotlin, and Scala.
Although thalia can produce Java programs, we did not consider Java in our
evaluation. The reason is that the issue tracker of OpenJDK is not open to the
public, and therefore we were unable to directly interact with its compiler’s
developers. For each compiler, we tested (1) its latest development version by
regularly building the compiler on its latest commit, or (2) its most recent
stable version.

API collection: We collected APIs from two sources. Initially, we examined the
APIs found in the standard library of the corresponding language, such as
collections API, I/O API. Beyond standard libraries, we also considered APIs
from third-party libraries found in the Maven central repository.
Specifically, we examined the Maven repository and Scala index (Scaladex,
2023) to gather the group ID, artifact ID, and the latest versions of the most
popular Kotlin, Java, and Scala libraries. Rather than selecting libraries
solely based on their popularity, we could establish a feature coverage
criterion. This criterion would (1) exclude libraries that exhibit the same
features with previously explored libraries, or (2) prioritize libraries with
new and complex typing features. This is not a straightforward task, so we
leave it as future work.

For each library, we searched in the Maven central repository to fetch: (1)
the API documentation of the library, (2) the JAR files of the library and its
dependencies. The documentation was converted into JSON files given as input
to thalia. Then, we built a classpath that pointed to the retrieved JAR files
so that the compiler under test could locate the external symbols defined in
external libraries. In total, we selected 95 libraries whose characteristics
are shown in Table 1. The entry ‘‘other’’ shows the average metrics of the
libraries not shown in the table.

We ran thalia on each selected API under four different synthesis modes. In
particular, on each API, we used thalia to synthesize (1) well-typed programs
with and without type erasure, and (2) wrongly-typed programs with and without
type erasure.

Table 1. Characteristics of ten selected libraries. Each table entry indicates
the number of nodes and edges of the API graph, the number of methods
(including the polymorphic ones), the number of fields, the number of
constructors, the number of types (including type constructors), the average
size of the inheritance chain, and the average size of API signatures.

Library | Nodes | Edges | Poly. M/Methods | Fields | Constr | Type Con/Types | Inhr size |  Sig size
---|---|---|---|---|---|---|---|---
com.fasterxml.jackson.core:jackson-core |  .,6775 |  .,10158 |  .,16/.,1442 |  .,54 |  .,82 |  .,4/.,98 |  .,3.80 |  .,2.47
com.google.guava:guava |  .,10235 |  .,14469 |  .,975/.,4363 |  .,188 |  .,0 |  .,214/.,412 |  .,3.31 |  .,2.68
org.apache.commons:commons-lang3 |  .,8559 |  .,11514 |  .,272/.,2643 |  .,307 |  .,193 |  .,93/.,211 |  .,2.80 |  .,2.60
org.apache.logging.log4j:log4j-api |  .,7207 |  .,10805 |  .,49/.,1771 |  .,66 |  .,122 |  .,12/.,134 |  .,3.77 |  .,4.05
org-assertj-assertj-core |  .,11321 |  .,16169 |  .,633/.,5250 |  .,179 |  .,0 |  .,151/.,656 |  .,4.41 |  .,2.67
org.clojure:clojure |  .,9032 |  .,12532 |  .,1/.,2676 |  .,466 |  .,169 |  .,2/.,624 |  .,3.85 |  .,3.23
org.mockito:mockito-core |  .,5783 |  .,8048 |  .,98/.,510 |  .,9 |  .,0 |  .,27/.,136 |  .,3.39 |  .,2.28
groovy-stdlib |  .,14817 |  .,22303 |  .,461/.,10982 |  .,1108 |  .,1159 |  .,164/.,1276 |  .,4.21 |  .,2.46
kotlin-stdlib |  .,6020 |  .,8986 |  .,205/.,3808 |  .,1108 |  .,438 |  .,70/.,395 |  .,5.47 |  .,2.37
scala-stdlib |  .,3933 |  .,5928 |  .,390/.,2439 |  .,688 |  .,246 |  .,93/.,331 |  .,4.23 |  .,2.49
other |  .,6900 |  .,9974 |  .,43/.,1330 |  .,150 |  .,97 |  .,16/.,204 |  .,3.32 |  .,2.37
Avg |  .,7052 |  .,10192 |  .,71/.,1563 |  .,177 |  .,112 |  .,23/.,227 |  .,3.38 |  .,2.4

Configuration: thalia comes with a set of constants that affect the number of
the synthesized programs (Section 3.6). For enumerating ill-typed typing
sequences, we configured thalia so that every type set contains at most five
incompatible types selected randomly. Regarding type inhabitant selection, we
configured Yen’s algorithm to return the shortest path between two nodes. This
is the equivalent to calling Dijkstra’s algorithm for the shortest path
calculation. Finally, the maximum depth of the generated programs is two.
Based on our exploratory experiments, these configurations provide a good
balance between bug-finding capability and performance.

###  4.2. RQ1: Bug-Finding Results

Table 2.  (a) Status of the reported bugs in groovyc, kotlinc, and Dotty, (b)
number of bugs with unexpected compile-time error (UCTE), unexpected runtime
behavior (URB), crash, or compilation performance (CPI) symptom, (c) bugs
revealed by well-typed programs, well-typed programs with erased types (TE),
or ill-typed ones.

Status | groovyc | kotlinc | Dotty |  Total
---|---|---|---|---
Confirmed |  .,38 |  .,9 |  .,8 |  .,55
Fixed |  .,20 |  .,1 |  .,1 |  .,22
Duplicate |  .,2 |  .,0 |  .,1 |  .,3
Won’t fix |  .,2 |  .,1 |  .,1 |  .,4
Total |  .,62 |  .,11 |  .,11 |  .,84

(a)

Symptom | groovyc | kotlinc | Dotty |  Total
---|---|---|---|---
UCTE |  .,47 |  .,7 |  .,7 |  .,61
URB |  .,6 |  .,0 |  .,0 |  .,6
Crash |  .,8 |  .,3 |  .,4 |  .,15
CPI |  .,1 |  .,1 |  .,0 |  .,2

(b)

Program type | groovyc | kotlinc | Dotty |  Total
---|---|---|---|---
Well-typed |  .,32 |  .,8 |  .,7 |  .,47
Well-typed (TE) |  .,21 |  .,3 |  .,3 |  .,27
Ill-typed |  .,9 |  .,0 |  .,1 |  .,10

(c)

Table 2(a) summarizes the bug-finding results of thalia. Overall, within five
months of concurrent development and testing, we reported .,84 bugs to
developers, .,77 of which are either confirmed or fixed. To prevent duplicate
bug reports, we conducted a comprehensive search in the issue tracker prior to
submission, to identify potential related bugs. After reporting a small number
of bugs to each development team, we waited a couple of weeks for the
developers to fix or triage them. This helped us avoid overwhelming developers
with an extreme number of unfixed/untriaged bugs. In the end, four of the
reported bugs were marked as ‘‘won’t fix’’. One ‘‘won’t fix’’ issue is a
compiler crash in Dotty. Scala developers think that it is not worth fixing
it, although the issue is a regression introduced in Scala 3. Another one is a
known limitation issue of groovyc.

Symptoms of compiler typing bugs: The symptoms of the discovered bugs are
shown in Table 2(b). The majority (.,61/.,84) lies in unexpected compile-time
errors (UTCE): a compiler  _unintentionally_ rejects a well-typed program.
UTCE is followed by compiler crash (.,15) and unexpected runtime behavior
(.,6). An unexpected runtime behavior (URB)333 We follow the same terminology
used in the study of Chaliasos et al. (2021). thalia detects URB bugs at
compile-time, and not at runtime, based on our test oracle for soundness bugs,
that is, erroneous acceptance of ill-typed programs. is the symptom of a
compiler bug that becomes evident at runtime. For example, soundness bugs
typically lead to URB symptoms, e.g., runtime errors that should have been
caught at compile-time. Two discovered bugs trigger severe compilation
performance issues (CPI) in the type checkers of groovyc and kotlinc.

Bug-finding under different synthesis modes: Table 2(c) shows the bug-finding
results of each synthesis mode. Most of the bugs (.,47/.,84) are triggered in
the base mode, where thalia produces well-typed programs that contain full
type information (i.e., type erasure is disabled). This suggests that thalia
is effective in detecting compiler typing bugs, even when generating simple
client code (at least at first blush). Using the type erasure process, thalia
has identified .,27 additional bugs. All of these bugs are related to issues
found in the type inference procedures of the compilers. Finally, thalia has
discovered .,10 bugs that originate from ill-typed code. The low number of
bugs triggered by ill-typed code in relation to the number of bugs that arise
from well-typed programs is consistent with the findings of Chaliasos et al.
(2021, 2022).

Intricacy of typing bugs: As highlighted by the study of Chaliasos et al.
(2021), fixing compiler typing bugs often becomes particularly challenging.
This insight is indeed confirmed by most of the compiler development teams we
have interacted with: many reported bugs require much expertise in the areas
of overload resolution and type inference.

Our interaction with developers has revealed another noteworthy observation:
typing bugs take a fair amount of effort to understand their root causes,
particularly identifying which specific components in type checking procedure
break down. Therefore, additional tooling for root cause analysis would be
beneficial for compiler developers. Furthermore, thalia has helped us reveal
interesting bugs that stem from issues in the language design. These bugs are
exceptionally challenging to fix, as their fix requires pervasive changes in
the compiler code base. These changes are susceptible to breaking other
language features.

###  4.3. RQ2: Test Case Characteristics

Table 3.  The language features that appear in the minimized test cases of our
reported bugs. A check mark indicates whether the corresponding feature is
supported by the state-of-the-art tool hephaestus.

|  |  | Supported by
---|---|---|---
Feature type | Feature | Frequency | hephaestus
Declaration | Polymorphic class |  .,58/.,84 | ✓
Polymorphic function |  .,45/.,84 | ✓
Single Abstract Method (SAM) |  .,30/.,84 | ✓
Overloading |  .,22/.,84 | ✗
Inheritance/Implementation of multiple interfaces |  .,8/.,84 | ✗
Variable argument |  .,5/.,84 | ✓
Access modifier |  .,2/.,84 | ✗
Inner class |  .,3/.,84 | ✗
Bridge method |  .,1/.,84 | ✗
Default method |  .,1/.,84 | ✗
Static method |  .,2/.,84 | ✗
Operator |  .,1/.,84 | ✗
Type inference | Type argument inference |  .,23/.,84 | ✓
Variable type inference |  .,2/.,84 | ✓

|  |  | Supported by
---|---|---|---
Feature type | Feature | Frequency | hephaestus
Type | Polymorphic type |  .,58/.,84 | ✓
Wildcard type |  .,19/.,84 | ✓
Bounded type parameter |  .,15/.,84 | ✓
Array type |  .,7/.,84 | ✓
Subtyping |  .,7/.,84 | ✓
Recursive upper bound |  .,3/.,84 | ✗
Primitive type |  .,3/.,84 | ✓
Nullable type |  .,2/.,84 | ✗
Expression | Function reference |  .,21/.,84 | ✓
Lambda |  .,10/.,84 | ✓
Conditionals |  .,4/.,84 | ✓

We manually identified what language features appear in every minimized test
case that accompanies our bug reports. Table 3 shows the frequency of the
identified features. Features related to parametric polymorphism (e.g.,
polymorphic function, wildcard type, etc.) are the top features in terms of
bug-finding capability. Roughly 85% (70/.,84) of the bug-triggering test cases
contain at least one feature related to parametric polymorphism. This finding
is in line with the work of Chaliasos et al. (2021, 2022). Our finding is
further supported by compiler developers who have acknowledged that working
with generics is a highly demanding task that requires a high level of
expertise. Parametric polymorphism is followed by functional programming
features (e.g., lambdas, function references), type inference features, and
overloading. Figure 10 shows the overlap of parametric polymorphism,
functional programming, and overloading. Overall, these features are found in
all but eight test cases. Finally, Table 3 confirms that thalia increases
feature coverage, especially for definition-related features. This means that
thalia can exercise the implementation of these features in an agnostic way,
as long as they they are part of the input APIs.

Figure 10. The Venn diagram of features related to parametric polymorphism,
functional programming, and overloading.

Size of test cases: : The test cases given by thalia are consistently small
across the examined languages. On average, a Groovy test case measures
$\sepnum{.}{,}{}{1.6}$kB and contains $\sepnum{.}{,}{}{13}$ lines of code
(LoC), while a Scala test case measures $\sepnum{.}{,}{}{1.6}$kB and consists
of $\sepnum{.}{,}{}{11}$ LoC. Similarly, Kotlin test cases have an average
size of $\sepnum{.}{,}{}{1.4}$kB and an average of $\sepnum{.}{,}{}{11}$ LoC.
The compact size of these test cases facilitates efficient testing with higher
throughput and simplifies the generation of minimal test-cases.

Overall, the above results indicate that although the test cases produced by
thalia are small in size, they are able to discover bugs triggered by a
combination of complicated languages features.

###  4.4. RQ3: Impact of Library Selection and Synthesis Modes

(a) groovyc

(b) Dotty

(c) kotlinc

Figure 11.  Compiler line coverage when using top 95 Maven libraries. Notably,
when combining the results of all libraries (highlighted in blue), there is an
increase in line coverage, ranging between $1.6$%--$4$% when compared to the
best individual library of each language.

To evaluate the impact of library selection and investigate the effectiveness
of different synthesis modes, we conducted a comprehensive evaluation using 95
top libraries found in the Maven repository, including the standard library of
each language.

Figure 12 shows how many well-typed and ill-typed test cases (typing
sequences) have been produced by our API enumeration technique. In total, the
examined 95 libraries yielded roughly 1.6 million programs for each language.
Based on these programs, we performed an analysis on the time spent
synthesizing them, as well as the code coverage achieved by each library and
mode.

Code coverage analysis: We used the JaCoCo library (EclEmma, 2023) to measure
the code coverage in each compiler. Figure 11 shows the line coverage achieved
by programs derived from each library in all synthesis modes. We observe that
the input library and its corresponding API significantly affects the
resulting line coverage. Libraries with limited methods and polymorphic
components tend to have lower line coverage, indicating that the extent of
code coverage depends on the richness of the input API. When combining the
programs that arise from all the input libraries (see blue bars), there is a
noteworthy code coverage increase in all the examined compilers. For example,
in groovyc, the combination of libraries surpasses the line coverage achieved
by the best individual library by $1.6$%. This percentage translates to
hundreds of additional covered lines. Similarly, in Dotty and kotlinc, the
line coverage improvement ranges between $3\%$ and $4\%$. Similar patterns
have been observed when considering branch and function coverage. Based on the
above, using APIs with distinct characteristics avoids saturation and
exercises unexplored code.

Table 4 illustrates the impact of each mode on line coverage in comparison to
the base mode, where thalia produces well-typed programs with type erasure
disabled. thalia’s different modes contribute to a line coverage increase up
to $5\%$\--$11.9\%$ across all compilers. While the goal is not to explore the
entire code base, but rather to exercise specific compiler parts, such as type
inference, employing multiple modes is crucial in maximizing the effectiveness
of thalia. This is further supported by the number of bugs (36/.,84) that were
discovered when using a mode other than the base mode (see Table 2(c)). Many
of them concern important type inference and soundness issues.

Figure 12. Number of test cases produced by thalia categorized by their type.

Table 4. Statistics regarding the increase in line coverage achieved by each
synthesis mode. The baseline is when thalia synthesizes well-typed programs
with complete type information. Numbers outside parentheses indicate absolute
change, while percentages in parentheses show relative change. The type
erasure mode (TE) exhibits the highest line coverage increase, followed by
producing ill-typed programs with missing type information (Both).

Compiler | Mode | Statistics |
---|---|---|---
Min | Max | Median | Mean | Std
groovyc | TE | +0 (0%) |  +.,4306 (11.9%) | +166 (0.5%) | +265 (0.7%) | 1.6%
Ill-typed | +0 (0%) |  +.,2952 (8.1%) | +45 (0.1%) | +118 (0.3%) | 1.1%
Both | +0 (0%) |  +.,3087 (8.5%) | +163 (0.5%) | +195 (0.5%) | 0.9%
0-7 Dotty | TE | +0 (0%) |  +.,5548 (7.1%) | +934 (1.2%) | +1087 (1.4%) | 1.1%
Ill-typed | +7 (0.01%) |  +.,3595 (4.6%) | +475 (0.6%) | +615 (0.8%) | 0.7%
Both | +117 (0.2%) |  +.,4192 (5.3%) | +852 (1.1%) | +975 (1.24%) | 0.8%
0-7 kotlinc | TE | +3 (0.01%) |  +.,2144 (3.7%) | +523 (0.9%) | +566 (1%) | 0.5%
Ill-typed | +1 (0%) |  +.,3030 (5.2%) | +175 (0.3%) | +291 (0.5%) | 0.7%
Both | +45 (0.1%) |  +.,2175 (3.7%) | +347 (0.6%) | +420 (0.7%) | 0.6%

Synthesis time: Figure 13 shows how the size of the underlying API graph
influences the time spent on the synthesis of a  _single_ test case. The
correlation between the size of the API graph and the synthesis time is almost
linear for all the compilers. thalia takes less than 400 milliseconds to
synthesize one program coming from large libraries with more than 25k edges in
the corresponding API graph. The average synthesis time is $256$, $161$, and
$178$ milliseconds for Groovy, Scala, and Kotlin programs respectively. This
demonstrates the practicality of thalia in synthesizing client programs in
milliseconds, even if they come from large libraries and complex APIs.

(a) groovyc

(b) Dotty

(c) kotlinc

Figure 13.  The synthesis time per program (in milliseconds) as a function of
the size of the API graph.

There are some exceptional cases where the synthesis time is relatively high
(see data points above the regression lines). This is explained by the high
number of polymorphic definitions with bounded type parameters included in the
corresponding APIs. For example, the org.assertj:assertj-core library has a
larger number of type constructors and polymorphic methods that define type
parameters with recursive upper bounds (e.g., T extends A<T>) In such cases,
thalia spends significant time seeking appropriate type arguments to
instantiate these polymorphic definitions.

###  4.5. RQ4: Comparison of Thalia vs. Hephaestus

(a) groovyc

(b) Dotty

(c) kotlinc

Figure 14.  Comparison between code coverage of hephaestus and thalia.

We compared our work with hephaestus (Chaliasos et al., 2022), which is the
state-of-the-art framework for validating static typing implementations.
Originally, hephaestus had support for three languages, two of which were also
included in our evaluation (Kotlin, Groovy). To make hephaestus also generate
Scala programs, we followed the guidelines in the work Chaliasos et al. (2022)
and implemented a translator that allows the conversion of programs written in
the hephaestus’s IR into concrete Scala programs.

Bug-finding capability: We manually analyzed the bug-revealing test cases of
thalia to identify how many bugs are missed by hephaestus. Looking at Table 3,
it is clear that the bug-revealing test cases exercise a plethora of
characteristics, such as overloading and the use of inner classes, which fall
outside the capabilities of hephaestus. Specifically, out of the .,84 bugs
identified by thalia, hephaestus fails to detect 42 of them, accounting for a
51% miss rate. Interestingly, these 42 bugs were found  _effortlessly_ by
thalia, as it leverages existing compiled code instead of explicitly
supporting the generation of intricate definitions.

For the remaining detected bugs, we also examined whether these bugs existed
in the compiler versions used in the testing campaign by Chaliasos et al.
(2022). Remarkably, out of these bugs, $9$ were found to exist in those
versions, and hephaestus failed to detect them despite the thorough efforts.
This is explained by the expressiveness of real-world APIs that made thalia
produce code featuring complex combinations of typing features. For example,
GROOVY-11020 is triggered by passing a function reference to a polymorphic
method that defines a type parameter bounded with a SAM type. Although
hephaestus supports polymorphic methods and SAM types, there is an extremely
low probability of generating code with such a programming idiom.

Nevertheless, there are certain bugs triggered by hephaestus that cannot be
detected by thalia. Most of these bugs have to do with implementation flaws
that are related to the semantic validation of definitions. Since thalia
employs pre-compiled API definitions, it fails to detect these types of
compiler errors. For example, KT-49583 is a bug, previously-reported by the
team of hephaestus. The accompanying test case contains an anonymous function
that encompasses another nested function declaration. This issue is out of
thalia’s reach, because rather than producing new declarations (e.g., a
function in a lambda), thalia re-uses existing code.

Code coverage analysis: We conducted a $12$-hour run for both tools in every
language, using all available modes and generating as many test cases as
possible within that time frame. We ran hephaestus using the same settings as
described in the work of Chaliasos et al. (2022). We assessed the code
coverage in each compiler using the programs generated by each tool.

Figure 14 illustrates the code coverage attained by hephaestus and thalia.
hephaestus slightly outperforms thalia on all the examined compilers. This
outcome aligns with our expectations, as hephaestus produces larger programs
and heavily emphasizes the utilization of declarations. However, thalia offers
the advantage of easily testing arbitrary features (Section 4.3).
Consequently, when combining the two approaches, we observe a percentage
increase in hephaestus’ line coverage of $7\%$ for groovyc and Dotty, and
$9\%$ for kotlinc. This translates to
$\sepnum{.}{,}{}{\sepnum{.}{,}{}{1118}}$\--$\sepnum{.}{,}{}{\sepnum{.}{,}{}{2567}}$
additionally covered lines of code. For branch coverage, the combination of
thalia and hephaestus leads to a $7\%$ increase for groovyc, $9\%$ for Dotty,
and $10\%$ for kotlinc. This translates to
$\sepnum{.}{,}{}{\sepnum{.}{,}{}{5395}}$\--$\sepnum{.}{,}{}{\sepnum{.}{,}{}{22334}}$
additionally covered branches. Finally, when considering function coverage,
thalia contributes to calling $5\%$ more functions in groovyc and Dotty, and
$8\%$ more functions in kotlinc. This translates to
$\sepnum{.}{,}{}{\sepnum{.}{,}{}{173}}$\--$\sepnum{.}{,}{}{\sepnum{.}{,}{}{654}}$
functions that were previously unexplored by hephaestus. We looked further
into some packages and classes

Table 5.  Average time of compiling and generating hephaestus and thalia
programs. Generation time is per program, whereas compilation time is per
batch of 45 programs.

Compiler | Compilation time (sec) |  Generation time (sec)
---|---|---
thalia | hephaestus | thalia | hephaestus
groovyc | 3.1 | 6.6 | 0.3 | 0.7
Dotty | 5.4 | 7.9 | 0.3 | 1
kotlinc | 6.5 | 26.5 | 0.2 | 1.3

to get an insight about that newly-explored code. Some noteworthy examples
include: (1) the org.jetbrains.kotlin.resolve.* package, which implements the
name resolution procedure in kotlinc, (2) a couple of classes in Dotty (e.g.,
dotty.tools.dotc.core.TypeComparer) that handle polymorphic types and type
comparisons. As expected, thalia missed a lot of code associated with
declarations and types of expressions (e.g., binary operators) supported only
by hephaestus. Overall, our findings indicate that thalia helps explore new
code in the compilers’ code base, addressing the current limitations of
hephaestus.

Code size: Within the 12-hour time period, the average size of thalia’s
programs written in Groovy, Scala, and Kotlin is $15$, $12$, and $11$ LoC,
respectively. hephaestus generated programs that are one order of magnitude
larger, with an average size of $304$, $262$, and $257$ LoC for Groovy, Scala,
and Kotlin respectively. The smaller size of thalia’s programs simplifies the
generation of minimal test-cases, which are invaluable for compiler writers
(Regehr et al., 2012).

Generation and compilation time: Table 5 presents the average time spent by
each tool on generating and compiling programs. hephaestus features higher
times compared to thalia, with varying performance across different languages.
For example, groovyc spends an average time of $6.6$ seconds for compiling 45
hephaestus’ programs, while it needs only $3.1$ seconds, on average, to
compile 45 programs given by thalia. At the same time, thalia synthesizes a
Groovy test case in 0.3 seconds, while hephaestus requires 0.7 seconds to
generate a single Groovy program. These findings highlight that thalia can
achieve greater throughput than the state-of-the-art work.

In short, our comparative analysis highlights four distinct differences
between thalia and hephaestus. (1) thalia’s programs are considerably smaller
than those of hephaestus (code size). (2) thalia’s programs involve faster
synthesis and compilation times (generation and compilation time). (3) Despite
the reduced size of its test cases, thalia still explores compiler regions
that hephaestus does not reach (code coverage analysis). (4) Relying on
existing compiled libraries makes thalia effortlessly uncover 51 bugs missed
by hephaestus (bug-finding capability).

###  4.6. Bug-Revealing Test Samples

⬇

1def test() {

2 val x: String = "strVal"

3 Predef.identify[Function1[? >: Int, String]](x.substring)

4}

5// Definition of the API

6class String {

7 def substring(begin: Int): String

8 def substring(begin: Int, end: Int): String

9}

10object Predef {

11 def identity[A](x: A): A

12}

(a) DOTTY-17310: Fail to resolve the reference to method String.substring.

⬇

1fun test() {

2 val x: Iterable<HashSet<Number>> = TODO()

3 val y: HashSet<Number> = TODO()

4 // Type mismatch: inferred type is Number

5 val res: List<HashSet<Number>> = x.minus(y)

6}

7// Definition of the API

8package kotlin.collections;

9

10operator fun <T> Iterable<T>.minus(element: T): List<T>

11operator fun <T> Iterable<T>.minus(elements: Iterable<T>): List<T>

(b) KT-57596: Resolving wrong method in the presence of operator overloading.

⬇

1import com.google.common.collect.HashBasedTable;

2 void test() {

3 Number x = HashBasedTable.<Number, Number, Number>create().get(null, null);

4 }

5}

6// Definition of the API

7package com.google.common.collect;

8interface Table<R,C,V> {

9 default V get(Object x, Object y);

10}

11class HashBasedTable<R,C,V> implements Table<R,C,V> {

12 static <R,C,V> HashBasedTable<R,C,V> create();

13}

(c) GROOVY-11012: A bug in the treatment of default methods leads to an UTCE.

⬇

1import java.util.Map

2import org.apache.commons.lang3.Validate.notEmpty;

3def test(): Unit = {

4 val x: Map[String, String] = ???

5 val res: Map[String, String] = notEmpty[Map[String, String]](x, "foo");

6}

7// Definition of the API

8package org.apache.commons.lang3

9object Validate {

10 def notEmpty[T](x: Array[T]): T

11 def notEmpty[T <: CharSequence](chars: T): T

12 def notEmpty[T <: Map[?, ?]](map: T): T

13}

(d) DOTTY-17412: Dotty is unable to call an overloaded method with bounded
type parameters.

Figure 15. Sample test programs that trigger typing bugs.

Figure 15(a): This is a regression introduced in Scala 3. The code creates a
reference to an overloaded method of class String named substring and passes
it as an argument to the higher-order function identity which expects
something of type Function1[? >: Int, String] (line 3). Although the intention
is to make a reference to the overloaded method defined on line 7, Dotty
rejects the program with an error of the form: “None of the overloaded
alternatives of method substring match expected type”. Interestingly, when the
expected type is Function1[Int, String], Dotty resolves the correct method as
expected.

Figure 15(b): The code demonstrates an issue in the design of Kotlin. As with
C++ and other languages, Kotlin supports operator overloading. The standard
library of Kotlin defines two overloaded methods for the operator - (minus).
When calling method minus, kotlinc decides to resolve the method defined on
line 11. However, this decision leads to a type mismatch, as the inferred type
of the method call becomes List<Number>, while the expected type is
List<HashSet<Number>>. The compiler should have resolved the overloaded
variant on line 10, where the type variable T is instantiated by the type
HashSet<Number>. This issue prevents the removal of polymorphic items from
mutable collections (e.g., lists, sets) via the corresponding operator, i.e.,
x - y.

Figure 15(c): In this example, the compiler erroneously rejects a well-typed
program. The root cause of this failure lies in the way Groovy treats
interfaces with default methods (see lines 8--10). In Groovy, an interface
with a default method is implemented as a trait, a structural construct that
allows composition of behaviors and implementation of interfaces. groovyc
fails to propagate the given type arguments when calling create (line 3) to
the trait that implements the interface Table (lines 8, 12). Consequently,
while checking the method call on line 3, groovyc infers the return type of
the method get as Object. This leads to an UCTE, as the expected type is
Number.

Figure 15(d): This program calls an overloaded method named notEmpty that
comes from the org.apache.commons:commons-lang3 library (line 5). The library
contains a few polymorphic variants of method notEmpty; each of them defines a
type parameter with a unique upper bound (lines 10--12). The intention is to
call the third overloaded alternative (line 12), as the explicit type argument
of the method call on line 5 comes in line with the bound of the underlying
type parameter (i.e., Map[?,?]). Nevertheless, an issue in Dotty’s overload
resolution procedure makes the compiler reject the program by reporting an
ambiguous method call. This issue stems from the design choice of Dotty
developers to check bounds only after type checking (to avoid cycles due to
recursive upper bounds). Therefore, bounds do not influence overload
resolution. In this context, it is impossible to properly call the intended
method from the given library. Surprisingly, when the definition on line 10 is
removed, the compiler behaves as expected.

##  5\. Related Work

Generative compiler testing: Generative compiler testing is an umbrella term
for methods that construct test programs completely from scratch. Csmith (Yang
et al., 2011) is the most influential program generator which produces well-
typed C programs while avoiding undefined behaviour. Many subsequent
generators have leveraged the power of Csmith to test other compilers (e.g.,
OpenCL) (Lidbury et al., 2015) and compiler components (Le et al., 2015b), or
enhance the diversity of the generated programs (Even-Mendoza et al., 2020,
2022). A more recent program generator for C/C++ programs, YARPGen (Livinskii
et al., 2020), produces programs with complex arithmetic expressions that are
more likely to trigger optimization bugs. Its re-implementation (Livinskii et
al., 2023) focuses on validating loop optimizers.

A key challenge associated with generative compiler testing is the
construction of code generators for syntactically- and semantically-valid
programs that help test beyond the front-end of a compiler. This typically
involves a large amount of engineering effort, while the corresponding
implementation is usually crafted for a single target language. Exploiting
well-formed definitions taken from existing software libraries allows us to
synthesize programs from scratch, but at the same time, easily port our
program generator to multiple languages.

Mutation-based compiler testing: Mutation-based compiler testing produces new
test programs by modifying existing ones. The most effective compiler testing
method that lies in this category is equivalence modulo input (EMI) (Le et
al., 2014, 2015a; Sun et al., 2016). EMI profiles the execution of a seed
program and applies a set of transformations so that the resulting programs
have the same output as the original one. Applying semantics-preserving
transformations to existing programs has been shown highly effective in the
graphics driver domain (Donaldson et al., 2017, 2021).

A primary limitation of mutation-based testing is that its effectiveness is
limited to the quality of the available seed programs. Our work tackles this
limitation, as mainstream languages come with a rich library ecosystem.
Library APIs expose a wide variety of advanced features that are more likely
to trigger typing bugs (Chaliasos et al., 2021).

Program enumeration for compiler testing: A number of enumeration techniques
have been developed for detecting issues in deep compiler phases, such as
optimizations and code generation. Skeletal program enumeration (SPE) (Zhang
et al., 2017) takes a program skeleton and enumerates all program variants
that involve unique variable usage combinations. SPE aims at exhibiting
diverse control- and data-dependence. Type-centric enumeration (TCE) (Stepanov
et al., 2021) finds crashes in the Kotlin compiler by first generating a
reference program of a certain structure and then replacing all program
expressions with other compatible expressions of the same type. In contrast to
our work, the outcome of TCE is not guaranteed to be type correct.

In this work, we propose a different enumeration technique: API enumeration
focuses on exposing diverse typing patterns of API invocations to exercise
interesting compiler behaviours with regards to subtyping and compile-time
name resolution.

Finding compiler typing bugs: Most of the aforementioned techniques target
optimizing compilers. The CLP-based (Constraint Logic Programming) program
generator proposed by Dewey et al. (2015) and hephaestus (Chaliasos et al.,
2022) represent the work most closely related to our approach. The CLP-based
method works by encoding the semantics rules of the language under test into a
set of logical constraints. Querying a CLP engine under the given constraints
enables the generation of well-typed or ill-typed programs. Despite its
application to the Rust compiler, CLP-based program generation comes with many
caveats that limit its generality and practicality, e.g., poor performances,
and even non-termination.

hephaestus employs type graphs with the primary goal of capturing (1) the
dependencies between type variables (i.e., determining whether a type variable
can be inferred by another), and (2) the inferred or declaration type of local
variables. A type graph is constructed using an intra-procedural analysis on
an existing program. hephaestus consults type graphs to maintain type
correctness in its type erasure mutation (Section 3.5). In contrast, our API
graph captures (1) all API definitions (methods, fields) found in an API, (2)
what types are needed to perform an application or a field access, and (3)
what is the type of each application or field access. An API graph is
constructed by traversing a given API specification, rather than a program.
The main purpose of API graphs is to identify type inhabitants.

Section 4.5 thoroughly compares our work with hephaestus. In short, thalia’s
underlying process, which relies on API enumeration rather than randomized
program generation, yields programs with distinct characteristics (smaller
code size) and enables exercising compiler regions that have been previously
unexplored by hephaestus.

Component-based program synthesis: Our work is also related to program
synthesis techniques that generate small code fragments using components of
existing libraries. The purpose of these techniques is not to test compilers,
but rather to assist developers in programming tasks via library code reuse.
In this context, a developer provides an incomplete expression (Perelman et
al., 2012; Gvero et al., 2013) or a method signature (Guo et al., 2022; Feng
et al., 2017; Guo et al., 2019). A program synthesis tool then produces a
ranked list of implementation sketches that better match the developer’s
intent.

The idea of labelling API graphs with type substitutions shares similarities
with a graph data structure called equality-constrained tree automata (ECTA)
(Koppel et al., 2022). In ECTA, nodes are annotated with equality constraints.
While our API graph constrains type variable instantiations, ECTA goes further
by constraining arbitrary types, such as matching an argument type with its
corresponding formal parameter type. ECTA is more expressive than API graphs,
because it solves the more general program synthesis problem, where the
relevancy of the proposed solutions matters. In contrast, the primary use of
API graphs is much simpler: we aim to identify chains of method calls/field
accesses of a certain type. This allows for (1) a compact representation,
especially the treatment of polymorphic types, (2) an efficient enumeration
done by  _standard_ graph reachability algorithms (e.g., Yen’s algorithm), and
(3) identification of variable-length chains of method calls/field accesses,
in contrast to ECTA’s fixed size approach.

API graph is inspired by prospector (Mandelin et al., 2005). prospector
introduces the signature graph, which treats every API component as a unary
function that takes an input type (receiver type), and produces an output type
(return type). Contrary to our API graph, prospector does not handle
parametric polymorphism which is a key language feature for revealing typing
bugs (Chaliasos et al., 2021). To handle parametric polymorphism, we enrich
prospector with Algorithm 1 and type substitution labels. A generalization of
prospector is SyPet (Feng et al., 2017), which models the structure of an API
using a Petri-net. Guo et al. (2019) extend SyPet by introducing the type-
guided abstraction refinement that allows program synthesis over polymorphic
types using an SMT encoding. Finally, InSynth (Gvero et al., 2013) assigns
weights to both API definitions and types, modeling program synthesis as an
optimization problem. InSyth leverages these weights to guide its search for
type inhabitants, selecting expressions that minimize a specific weight
function.

The goal of these techniques is different from ours. They strive to synthesize
the most optimal solution e.g., in terms of code size, number of API method
invocations, type distance, or users’ intent. Also many of these tools lack
support for parametric polymorphism, or exhibit high running times. Such
challenges can make these tools less suitable for our compiler testing
scenarios.

SyRust (Takashima et al., 2021) is a semantic-aware program synthesis
technique for testing Rust libraries. Using a manually-generated code template
and inputs, it encodes the typing rules of Rust (w.r.t. ownership, variable
lifetime) into a satisfiability problem and synthesizes test cases of
increasing size. Contrary to our work, SyRust is semi-automatic and faces
scalability issues, because it is capable of handling 15 API definitions
(e.g., methods) per library. Also, SyRust’s focus lies in identifying memory-
safety bugs in library implementations, rather than producing test cases that
showcase diverse typing patterns (e.g., type inference reasoning) to test
compilers.

##  6\. Conclusion

We have presented an API-driven program synthesis approach for testing the
implementation of compilers’ static typing procedures. Our method harnesses
the ubiquity and complexity of APIs extracted from established software
libraries, and synthesizes concise client programs that employ API entities
(e.g., types, functions, fields) through different typing patterns. This helps
us exercise a broad spectrum of type-related compiler functionalities, without
the need to generate complex API definitions ourselves. Our evaluation on the
compilers of Scala, Kotlin, and Groovy has shown the effectiveness of our
approach. Indeed, our implementation has uncovered $\sepnum{.}{,}{}{84}$ bugs
($\sepnum{.}{,}{}{77}$ bugs are either confirmed or fixed), $51$ of which
could not have been detected by prior work.

Our API-driven program synthesis approach opens up further opportunities for
combining synthetic and real-world code to discover bugs in compiler
implementations. For example, in addition to generating client programs, we
can extend our approach to create intricate definitions (e.g., classes) that
build upon existing ones found in an API (e.g., through inheritance
constructs). We believe that this extension will enable the identification of
new compiler bugs.

## References

  * (1)
  * Amalfitano et al. (2015) Domenico Amalfitano, Nicola Amatucci, Anna Rita Fasolino, Porfirio Tramontana, Emily Kowalczyk, and Atif M. Memon. 2015.  Exploiting the Saturation Effect in Automatic Random Testing of Android Applications. In _Proceedings of the Second ACM International Conference on Mobile Software Engineering and Systems_ (Florence, Italy) _(MOBILESoft ’15)_. IEEE Press, 33–43.
  * Amin and Tate (2016) Nada Amin and Ross Tate. 2016.  Java and scala’s type systems are unsound: the existential crisis of null pointers. In _Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016_ , Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 838--848.  https://doi.org/10.1145/2983990.2984004
  * Chaliasos et al. (2021) Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Mitropoulos, Dimitris Mitropoulos, and Diomidis Spinellis. 2021\.  Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 123 (Oct. 2021), 30 pages.  https://doi.org/10.1145/3485500
  * Chaliasos et al. (2022) Stefanos Chaliasos, Thodoris Sotiropoulos, Diomidis Spinellis, Arthur Gervais, Benjamin Livshits, and Dimitris Mitropoulos. 2022\.  Finding Typing Compiler Bugs. In _Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ (San Diego, CA, USA) _(PLDI 2022)_. Association for Computing Machinery, New York, NY, USA, 183–198.  https://doi.org/10.1145/3519939.3523427
  * Cortier et al. (2017) Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. 2017.  A Type System for Privacy Properties. In _Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security_ (Dallas, Texas, USA) _(CCS ’17)_. Association for Computing Machinery, New York, NY, USA, 409–423.  https://doi.org/10.1145/3133956.3133998
  * Dewey et al. (2015) Kyle Dewey, Jared Roesch, and Ben Hardekopf. 2015.  Fuzzing the Rust Typechecker Using CLP. In _Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering_ (Lincoln, Nebraska) _(ASE ’15)_. IEEE Press, 482–493.  https://doi.org/10.1109/ASE.2015.65
  * Donaldson et al. (2017) Alastair F. Donaldson, Hugues Evrard, Andrei Lascu, and Paul Thomson. 2017.  Automated Testing of Graphics Shader Compilers.  _Proc. ACM Program. Lang._ 1, OOPSLA, Article 93 (Oct. 2017), 29 pages.  https://doi.org/10.1145/3133917
  * Donaldson et al. (2021) Alastair F. Donaldson, Paul Thomson, Vasyl Teliman, Stefano Milizia, André Perez Maselco, and Antoni Karpiński. 2021\.  Test-Case Reduction and Deduplication Almost for Free with Transformation-Based Compiler Testing. In _Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ (Virtual, Canada) _(PLDI 2021)_. Association for Computing Machinery, New York, NY, USA, 1017–1032.  https://doi.org/10.1145/3453483.3454092
  * EclEmma (2023) EclEmma. 2023\.  EclEmma Jacoco.  https://www.eclemma.org/jacoco/.  Online accessed; 04-07-2023.
  * Even-Mendoza et al. (2020) Karine Even-Mendoza, Cristian Cadar, and Alastair F. Donaldson. 2020.  Closer to the Edge: Testing Compilers More Thoroughly by Being Less Conservative about Undefined Behaviour. In _Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering_ (Virtual Event, Australia) _(ASE ’20)_. Association for Computing Machinery, New York, NY, USA, 1219–1223.  https://doi.org/10.1145/3324884.3418933
  * Even-Mendoza et al. (2022) Karine Even-Mendoza, Cristian Cadar, and Alastair F. Donaldson. 2022.  CsmithEdge: More Effective Compiler Testing by Handling Undefined Behaviour Less Conservatively.  _Empirical Softw. Engg._ 27, 6 (nov 2022), 35 pages.  https://doi.org/10.1007/s10664-022-10146-1
  * Feng et al. (2017) Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. 2017.  Component-Based Synthesis for Complex APIs _(POPL ’17)_. Association for Computing Machinery, New York, NY, USA, 599–612.  https://doi.org/10.1145/3009837.3009851
  * Guo et al. (2022) Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, and Nadia Polikarpova. 2022.  Type-Directed Program Synthesis for RESTful APIs. In _Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ (San Diego, CA, USA) _(PLDI 2022)_. Association for Computing Machinery, New York, NY, USA, 122–136.  https://doi.org/10.1145/3519939.3523450
  * Guo et al. (2019) Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. 2019.  Program Synthesis by Type-Guided Abstraction Refinement.  _Proc. ACM Program. Lang._ 4, POPL, Article 12 (dec 2019), 28 pages.  https://doi.org/10.1145/3371080