Void safety

Abstract

Null pointer dereferencing is a well-known issue in object-oriented programming, and can be avoided by adding special validity rules to the programming language. However, just introducing a single rule is not enough: the whole language infrastructure has to be considered instead. The resulting guarantees are called void safety. The thesis reviews, in detail, engineering solutions and migration efforts that enabled the transition from classic to void safe code of multiple libraries and projects with lines of code ranging in the millions. Experience with the tiny details of the implementation can be an invaluable source of insight for researcher looking into making a language void safe. The void safety rules can be divided into three major categories. The first one is the extension of a regular type system with attached (non-null) and detachable (possibly-null) types. Generic programming opens a door to different interpretations. The thesis defines some base void safety properties for formal generic types and specifies void-safety-aware conformance rules. The second category of rules ensures that newly created objects reach a stable state maintaining the type system guarantees. The thesis proposes two solutions for this object initialization issue and compares them to previous work. It formalizes the rules in the Isabelle/HOL proof assistant and establishes some of their properties. To ensure safety at the end of object life cycle it also specifies validity rules for finalizers. A number of examples are used to demonstrate that the proposed solutions are of practical use and do not suffer from limited expressiveness caused by the lack of additional annotations describing intermediate object states. The third category of void safety rules covers a practical need to bridge the gap between attached and detachable types. The thesis proposes formal void safety rules for local variables in the context of an object-oriented language that do not require any marks to distinguish between attached and detachable types. It demonstrates advantages of the annotation-free approach with benchmarks based on open source code, discusses implementation decisions and how they are reflected in the formal model. The thesis concludes with a machine-checkable soundness proof for the rules involving local variables using the Isabelle/HOL proof assistant.