RFC: Nullability qualifiers

* Based on your discussion of type system impact, I'm sure you are all well aware that the compiler support for "maintaining type sugar through semantic analysis" needed to make this proposal work is *almost* enough to support a full "plug-able type system" similar to what's available in recent versions of Java. Do you have any plans to address the missing pieces? Being able to support pluggable type information more broadly (while continuing to guarantee that adding such qualifiers/attributes/however-it's-expressed would have zero impact on generated code) would enable all sorts of interesting analyses. A few examples that spring to mind include compile-time enforcement of physical unit compatibility, various protocol-level checks (type states, a la Bierhoff & Aldrich), and many more. When last I investigated this question (about a year ago), the limitation regarding templates (your [6]) was the only significant missing piece. Closing that gap would greatly reduce the difficulty (and project risk) of implementing such analyses.

We’re almost there in Clang, although I doubt that I personally will have time any time soon to work on addressing the issue of type sugar flowing through template specializations. I don’t think it’s fundamentally that hard to do, and beyond that I expect that we’ll see a long tail of small issues where we’re not maintaining type sugar everywhere.

I’ve been working on a very hacky implementation of pluggable types for Clang. In fact, one of the prototypes I developed for the system is a simple nullability qualifier. There’s a little more detail on my blog:
http://homes.cs.washington.edu/~asampson/blog/quala.html
http://homes.cs.washington.edu/~asampson/blog/quala-codegen.html

So I’m very interested in generalizing mechanisms like what’s proposed here for __nonnull. This may be more straightforward to implement once __nonnull itself has landed. (At the very least, it should pave the way for my project’s patch to be smaller.) If anyone else is interested, let’s talk and perhaps put together a proposal.

Adrian Sampson
University of Washington

  • Based on your discussion of type system impact, I’m sure you are all well aware that the compiler support for “maintaining type sugar through semantic analysis” needed to make this proposal work is almost enough to support a full “plug-able type system” similar to what’s available in recent versions of Java. Do you have any plans to address the missing pieces? Being able to support pluggable type information more broadly (while continuing to guarantee that adding such qualifiers/attributes/however-it’s-expressed would have zero impact on generated code) would enable all sorts of interesting analyses. A few examples that spring to mind include compile-time enforcement of physical unit compatibility, various protocol-level checks (type states, a la Bierhoff & Aldrich), and many more. When last I investigated this question (about a year ago), the limitation regarding templates (your [6]) was the only significant missing piece. Closing that gap would greatly reduce the difficulty (and project risk) of implementing such analyses.

We’re almost there in Clang, although I doubt that I personally will have time any time soon to work on addressing the issue of type sugar flowing through template specializations. I don’t think it’s fundamentally that hard to do, and beyond that I expect that we’ll see a long tail of small issues where we’re not maintaining type sugar everywhere.

I’ve been working on a very hacky implementation of pluggable types for Clang. In fact, one of the prototypes I developed for the system is a simple nullability qualifier. There’s a little more detail on my blog:
http://homes.cs.washington.edu/~asampson/blog/quala.html
http://homes.cs.washington.edu/~asampson/blog/quala-codegen.html

So I’m very interested in generalizing mechanisms like what’s proposed here for __nonnull. This may be more straightforward to implement once __nonnull itself has landed. (At the very least, it should pave the way for my project’s patch to be smaller.) If anyone else is interested, let’s talk and perhaps put together a proposal.

Delesley - this is alls sounding a but familiar?

This does indeed look very familiar. I would love it if clang had a pluggable type system. It’s been a while since I last looked at the issues, but I ran into two big problems, and ended up deciding that the amount of work was too large for me to tackle.

(1) Templates

As Doug mentioned, a major goal of pluggable types is to support the type erasure property; if you erase all of the pluggable attributes (perhaps using #define to eliminate them), then the behavior of the program should not change. However, erasure and templates don’t mix well. For example std::vector<int*> and std::vector<__nonnull int*> must have the same instantiation, because the canonical type is the same. However, the two types must still be distinguished for the purpose of type checking.

In addition, type-checking of templatized code may produce errors for one attributed type (e.g. __nonnull int*), while having no errors in a type with a different attribute (e.g. int*). However, we only instantiated the template once, with the canonical type. Thus, we can either choose to (a) not produce errors in template code, or (b) try to type-check every template instantiation for all non-canonical variations in the template parameters, which may be infeasible.

(2) Dependent types

For thread safety analysis, my goal was to support dependent type attributes, e.g.

void processAll(Mutex* mu, std::vector<int GUARDED_BY(mu)>& array) { … }

Notice here that the type of ‘array’ depends on ‘mu’. This adds an additional wrinkle, especially when combined with (1), because you have to be extra careful about how you handle lexical scopes during template instantiation.

However, if these two problems were solved, then I could significantly improve the precision of thread safety analysis.

-DeLesley