Pluggable Type Inference for Free

Martin Kellogg, Daniel Daskiewicz, Loi Ngo Duc Nguyen, Muyeed Ahmed, Michael D. Ernst

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

Abstract

A pluggable type system extends a host programming language with type qualifiers. It lets programmers write types like unsigned int, secret string, and nonnull object. Typechecking with pluggable types detects and prevents more errors than the host type system. However, programmers must write type qualifiers; this is the biggest obstacle to use of pluggable types in practice. Type inference can solve this problem. Traditional approaches to type inference are type-system-specific: for each new pluggable type system, the type inference algorithm must be extended to build and then solve a system of constraints corresponding to the rules of the underlying type system. We propose a novel type inference algorithm that can infer type qualifiers for any pluggable type system with little to no new type-system-specific code-that is, 'for free'. The key insight is that extant practical pluggable type systems are flow-sensitive and therefore already implement local type inference. Using this insight, we can derive a global inference algorithm by re-using existing implementations of local inference. Our algorithm runs iteratively in rounds. Each round uses the results of local type inference to produce summaries (specifications) for procedures and fields. These summaries enable improved inference throughout the program in subsequent rounds. The algorithm terminates when the inferred summaries reach a fixed point. In practice, many pluggable type systems are built on frameworks. By implementing our algorithm once, at the framework level, it can be reused by any typechecker built using that frame-work. Using that insight, we have implemented our algorithm for the open-source Checker Framework project, which is widely used in industry and on which dozens of specialized pluggable typecheckers have been built. In experiments with 11 distinct pluggable type systems and 12 projects, our algorithm reduced, by 45 % on average, the number of warnings that developers must resolve by writing annotations.

Original languageEnglish (US)
Title of host publicationProceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1542-1554
Number of pages13
ISBN (Electronic)9798350329964
DOIs
StatePublished - 2023
Event38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023 - Echternach, Luxembourg
Duration: Sep 11 2023Sep 15 2023

Publication series

NameProceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023

Conference

Conference38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
Country/TerritoryLuxembourg
CityEchternach
Period9/11/239/15/23

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality
  • Control and Optimization

Keywords

  • Pluggable type systems
  • static analysis
  • type inference
  • type qualifiers
  • type-checking

Fingerprint

Dive into the research topics of 'Pluggable Type Inference for Free'. Together they form a unique fingerprint.

Cite this