Parsing VCC annotations with clang

Hey everyone,

I'd like to work with VCC [1] annotations and clang.

This is an example for a functional contract specified in VCC's annotation
language:

int min(int a, int b)
  _(requires \true)
  _(ensures \result <= a && \result <= b)
{
  if (a <= b)
  return a;
  else return b;
}

This is an example for object invariants specified in VCC's annotation
language:

#define SSTR_MAXLEN 100
typedef struct SafeString {
  unsigned len;
  char content[SSTR_MAXLEN + 1];
  _(invariant \this−>len <= SSTR_MAXLEN)
  _(invariant content[len] == ’\0’)
} SafeString;

What would be necessary to make clang able to parse VCC [1] annotations like
_(requires ...), _(ensures ...) and _(invariant) in the example above. I'd
like to be able to turn these into run time checks for these properties.

Best regards,
Florian

[1] http://vcc.codeplex.com/

Hi Florian,

I'm not familiar with the extension, but this would likely rewrite a lot of parser work, as well as AST and code generation work. This is an interesting research extension, but not likely something we'd take back into mainline.

-Chris

Hey Chris,

thank you for your response and the information you provided.

If I used a macro such as

  #define _(x) // x

so that x is not removed but turned into a comment instead. Can this comment
be accessed in clang and can I determine the corresponding
function/struct/loop with this? It seems like clang::CommentHandler is able to
handle comments and determine the range of the comment in the source file. From
there I'd expect to be able to determine the surrounding object easily. Am I
on the right track with this?

Regards,
Florian

IIRC the comment gets removed before the #define is processed, so the
macro definition won't even see the comment and this won't work.

I was /going/ to suggest
    #define _(x) __attribute__((annotate(#x)))
because if it would work then you could just look for functions in the
AST with an AnnotateAttr attribute whose getAnnotation() starts with
"requires " or "ensures ". (You'd have to parse the expressions
yourself though, as the AST would consider them to just be strings)

Unfortunately it seems the place your _() appears isn't currently a
valid attribute location though. The GCC manual does say "An attribute
specifier list may, in future, be permitted to appear after the
declarator in a function definition (before any old-style parameter
declarations or the function body)."[1], but both GCC and Clang don't
currently seem to like attributes there (and __attribute((annotate))
isn't recognized by GCC anyway).

Maybe a patch to Clang to allow them there would be accepted though?

[1]: http://gcc.gnu.org/onlinedocs/gcc/Attribute-Syntax.html

Hey Chris,

thank you for your response and the information you provided.

If I used a macro such as

#define _(x) // x

so that x is not removed but turned into a comment instead.

As Frits points out, the C preprocessor doesn't work this way. You could use:

#define _(x)

which will just strip them out, allowing the non-annotations to be parsed.

Can this comment
be accessed in clang and can I determine the corresponding
function/struct/loop with this? It seems like clang::CommentHandler is able to
handle comments and determine the range of the comment in the source file. From
there I'd expect to be able to determine the surrounding object easily. Am I
on the right track with this?

The right track to implementing this doesn't involve a macro, or involves a macro along the lines of what frits says where you turn "_" into an attribute. You'll still have to implement the parser logic either way though.

-Chris