Candidate: Jenny Xiang
Title: Type Checking and Whole-program Inference for Value and Interval Analysis
Date: October 8, 2020
Time: 2:00 PM
Place: Remote
Supervisor(s): Dietl, Werner
Abstract:
Value analysis is important in many software domains for ensuring the safety and reliability of a program and is a crucial facet in software development. This thesis explore the use of static analysis with type systems for value analysis. Properly formalized type systems can provide mathematical guarantees for the correctness of a program at compile time. This thesis presents (1) a novel type system, the Narrowing and Widening Checker,
(2) a whole-program type inference, the Value Inference for Integral Values, (3) a unitsof- measurement type system, PUnits, and (4) an improved algorithm to statically analyze the data-ow of programs.
The Narrowing and Widening Checker is a type system that prevents loss of information during narrowing conversion of primitive integral data types and automatically distinguishes the signedness of variables to eliminate the ambiguity of a widening conversion from type byte and short to type int in Java during program compilation. This additional type system ensures soundness in programs by restricting operations which violate the type rules de ned.
While type checking veri
es whether the given type declarations are consistent with their use, type inference can automatically nds the properties at each location in the program, and reduce the annotation burden of the developer. The Value Inference for Integral Values is a constraint-based whole-program type inference for integral analysis. It supports the relevant type quali ers used by the Narrowing and Widening type system, and reduces the annotation burden when using the Narrowing and Widening Checker.
Value Inference can infer types in two modes: (1) ensure a valid integral typing exists, and
(2) annotate a program with precise and relevant values. Annotation mode allows human inspection and is essential since having a valid typing does not guarantee that the inferred speci cation expresses design intent.
PUnits is a type system for expressive units of measurement types and a precise, wholeprogram inference approach for these types. This paper presents a new type quali er for this type system to handle cases where the method return and method parameter type are context-sensitive to the method receiver type. Related work and the bene ts and trade-o s of using PUnits versus existing Java unit libraries are discussed. This thesis demonstrates how PUnits can enable Java developers to reap the performance bene ts of using primitive types instead of abstract data types for unit-wise consistent scienti c computations in real-world projects.
The Dataow Framework is a data-ow analysis for Java [44] used to evaluate the types of the values at each program location. Data-ow analysis is considered a terminating,imprecise abstract interpretation of a program and many false-positives are issued by the Narrowing and Widening Checker due to its imprecision. Three improvements to the algorithm in the framework are presented to increase the precision of the analysis: (1) implementing a dead-branch analysis, (2) proposing a path-sensitive analysis, and (3) discussing how loop precision can be improved.
The Narrowing and Widening Checker is evaluated on 22 of the Apache Commons project with 224k lines of code. Out of these projects, 18 projects failed with 717 errors.
The Value Inference for Integral Values is evaluated on these 18 Apache Commons project.
Out of these projects, 5 projects successfully evaluated to SAT and the Value Inference inferred 10639 annotations. The 13 projects that evaluated to UNSAT are manually examined and all of them contain a real narrowing error. Manual annotations are added to 5 of these projects to resolve the reported errors. In these 5 projects, the Narrowing and Widening Checker detects 69 real errors and 26 false-positives, with a false-positive rate of 37.7%. The type system performs adequately with a compilation time overhead of 5.188x for the Narrowing and Widening Checker and 24.43x for the Value Inference.
These projects are then evaluated with the addition of dead-branch analysis added to the framework; the additional evaluation time is negligible. Its performance is suitable for use in a real-world software development environment.
All the type systems presented build on techniques from type quali er systems and constraint-based type inference, expanding them to the rst system that provides a practical interval and value type system. Our implementation and evaluation of these type systems shows that these techniques are necessary and are e ective in ensuring correctness of real-world programs.