Show simple item record

dc.contributor.authorLi, Jianchu 15:45:48 (GMT) 15:45:48 (GMT)
dc.description.abstractJava'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 constraints 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 in the 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 extendability 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 approximately 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 approximately 23,000 type qualifiers were inferred. These results suggest that our system can efficiently give correct solution for type constraints.en
dc.publisherUniversity of Waterlooen
dc.titleA General Pluggable Type Inference Framework and its use for Data-flow Analysisen
dc.typeMaster Thesisen
dc.pendingfalse and Computer Engineeringen and Computer Engineeringen of Waterlooen
uws-etd.degreeMaster of Applied Scienceen
uws.contributor.advisorDietl, Werner
uws.contributor.affiliation1Faculty of Engineeringen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages