TY - GEN
T1 - Pluggable Type Inference for Free
AU - Kellogg, Martin
AU - Daskiewicz, Daniel
AU - Duc Nguyen, Loi Ngo
AU - Ahmed, Muyeed
AU - Ernst, Michael D.
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - Pluggable type systems
KW - static analysis
KW - type inference
KW - type qualifiers
KW - type-checking
UR - http://www.scopus.com/inward/record.url?scp=85174887527&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85174887527&partnerID=8YFLogxK
U2 - 10.1109/ASE56229.2023.00186
DO - 10.1109/ASE56229.2023.00186
M3 - Conference contribution
AN - SCOPUS:85174887527
T3 - Proceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
SP - 1542
EP - 1554
BT - Proceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
Y2 - 11 September 2023 through 15 September 2023
ER -