[cfe-dev] RFC: Nullability qualifiers

[Delesley Hutchins]

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


On Sun, Mar 15, 2015 at 4:58 PM, David Blaikie <dblaikie at gmail.com> wrote:

>
> On Mar 15, 2015 3:55 PM, "Adrian Sampson" <asampson at cs.washington.edu>
> wrote:
> >
> > >> * 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?
>
> >
> > Adrian Sampson
> > University of Washington
> >
> >
> > _______________________________________________
> > cfe-dev mailing list
> > cfe-dev at cs.uiuc.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
>



-- 
DeLesley Hutchins | Software Engineer | delesley at google.com | 505-206-0315
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20150317/a2b12c6e/attachment.html>