Candidate
Jianchu Li
Title
A General Pluggable Type Inference Framework and its use for Data-flow Analysis
Supervisor
Werner Dietl
Abstract
Java’s pluggable type systems provide valuable compile-time guarantees, but annotating the program with pluggable types can be a significant burden on programmers. Checker Framework Inference, a framework that aims to provide a constraint-based type inference for pluggable types, can generate type constraint over the occurrence of type qualifier of expressions according to type rules. However, there is no efficient approach to solve type constraints generated by Checker Framework Inference.
This thesis presents a system called Type Constraint Solver that can solve the type constraint by encoding the constraint as a Max-SAT problem and LogiQL language. The system takes advantage of existing Max-SAT solvers and LogicBlox to solve the corresponding forms, and gets the concrete pluggable type qualifiers for program expressions. Type Constraint Solver provides options to separate constraints into groups and solve them in parallel. It also has scalability that can be easily extended with custom encoding logic. We developed a pluggable type system called Dataflow Type System on top of Checker Framework Inference to verify the functionality of Type Constraint Solver. The type system and its inference can perform data-flow analysis by inferring all possible run-time Java types of return types, parameters, fields, and variables at compile time. We applied Checker Framework Inference to six real-world applications of up to 39kLOC with Dataflow Type System and OsTrusted Type system resulting 58,000 type constraints. We used our tool to solve these type constraints and analyzed the experimentation statistics. We manually examined the inference result and found that Type Constraint Solver is able to automatically infer the expected type qualifiers for benchmarks. Inferring the largest application with fastest inference options took about 10 seconds on average, and 23,000 type qualifiers were inferred. These results suggest that our system can efficiently give correct solution for type constraints.