Hi Jordan,
Thanks for your answer. My comments below.
– Mathieu
Hi, Mathieu…sorry for the delay. There’s no reason why a new checker wouldn’t be able to check new kinds of annotations, but the annotations it supports today are the same attributes provided by the Clang compiler. Now, we can always add attributes to the compiler, but that’s not something we usually want to do lightly.
Excellent. Sure!
Anna, Ted, and I have kicked around the idea of a more generic ‘analyzer_annotate’ attribute, which could make one-off analyzer language extensions cheaper, but we didn’t quite finish designing it. Does this sound like the sort of thing you’re asking about? This would require modifying Clang’s attribute parser to support this generic attribute and provide convenient access to its possible fields for any checkers.
Yes this is totally what I am interested in.
Ideally (some of) these custom attributes should be attachable to types so that we can annotate structures in depth and share annotations between function declarations.
See example below.
(Meanwhile, we’ve hacked some things together using the existing string-only ‘annotate’ attribute; see IvarInvalidationChecker. You could use this to prototype your checker if you didn’t want to work on the general attribute problem just yet.)
In this particular case, something else we’ve thought of is an attribute that stipulates that a function return value is always non-null, and another requiring that the result is checked. These also haven’t been fully designed yet (are they inherited? do they piggyback on existing attributes like ‘nonnull’, or do they get their own syntax?).
As far as semantics is concerned, a solution that comes to my mind is to hack the usual 4-value lattice with a 5th “magic” value duplicating the “absurd” state. This 5-th value would propagate but otherwise would not be produced by unification.
nullable (check required)
/
/
null nonnull
\ /
\ /
absurd (unreachable)
magic (don’t care) ← actually the default in the absence of annotation
// merging values from possible paths
union(null, nonnull) = nullable // one of the path explicitly null-ed the value, we can’t feed a function requiring a nonnull value anymore
union(magic, null) = null // idem
union(magic, nonnull) = nonnull // ignore the magic value and pretend we know it is nonnull (strange but I could not find any problematic example)
// unifying values
intersection(null, nonnull) = absurd // cut the path
intersection(magic, nonnull) = magic // continue to ignore this runtime value
Here is one motivating example using this vocabulary as type annotations.
struct list;
typedef struct list nullable list_t; // activate null-value checking
struct list {
int key;
struct blob value
list_t next; // here as well
};
int buggy_length(list_t l) {
int x = 1;
while(l → next) { // boom
x++;
l = l → next;
}
return x;
}
list_t buggy_next(struct list st) {
return st.next; // re-boom
}
int find(list_t l, int value, struct blob *nonnull result) {
// some code to find a node in the list and write it to *result
}