Pragma-based syntax

[nemequ]

Adpated from a post on the frama-c mailing list:

Using the first example from the tutorial:

/*@ ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/
int max (int x, int y) {
  return (x > y) ? x : y;
}

A pragma-based version might look something like:

#pragma acsl ensures \result >= x && \result >= y;
 #pragma acsl ensures \result == x || \result == y;
int max (int x, int y) {
  return (x > y) ? x : y;
}

One major advantage of the pragma syntax is integration with the preprocessor. For example, let's say I use a macro to define several variants of a function:

#define DEFINE_MAX_FN(T, id) \
  T id##_max (T x, T y) { \
    return (x > y) ? x : y; \
  }
DEFINE_MAX_FN(int, int)
DEFINE_MAX_FN(unsigned int, uint)
DEFINE_MAX_FN(int64_t, int64)

I realize that (ab)using the preprocessor like this is often considered to be something of an anti-pattern, but there are times where the benefits from code reuse vastly outweigh the decreased readability. I know several of my own projects would have been impractical without this feature.

As far as I know, with ACSL there is no good way to annotate the different versions; I would need to add a comment for each one:

/*@ ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/
DEFINE_MAX_FN(int, int)
/*@ ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/
DEFINE_MAX_FN(unsigned int, uint)
/*@ ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/
DEFINE_MAX_FN(int64_t, int64)

Which is especially onerous if the macro is considered to be part of the user-facing API and not just an implementation detail. This is pretty common for things like test harnesses and data structure implementations.

With a pragma-based implementation the annotations could be moved into the macro:

#define DEFINE_MAX_FN(T, id) \
  _Pragma("acsl ensures \\result >= x && \\result >= y") \
  _Pragma("acsl ensures \\result == x || \\result == y") \
  T id##_max (T x, T y) { \
    return (x > y) ? x : y;
  }

Just to give a bit of context, I'm interested in adding (partial) ACSL support to C compilers; not for full formal verification, but to help the compilers provide better compile-time warnings and errors.

I think the pragma-based syntax would also be more attractive for compilers as it would likely be easier to hook in to existing mechanisms in place to handle things like OpenMP, Cilk++, and compiler-specific directives. It's also seems a bit more palatable since the pragma mechanism is part of the C99 and C11 standards.

@vprevosto responded with:

I see your point. This might indeed be worth considering, even though I think that some clarifications are needed on what exactly can go after an acsl pragma. In particular, you seem to want to be able to split a single annotation into several pragmas, which implies an obvious question: how do we merge them? In particular, we should take care of easily distinguishing global annotations from function contracts, as in:

_Pragma("acsl lemma foo: \\true;")
_Pragma("acsl requires \\true;")
_Pragma("acsl ensures \\true;")
int f() { return 0; }

That's definitely a problem. I think that allowing people to split annotations across multiple pragmas is important for readability, though.

IMHO perhaps the most natural thing would be to have keywords like lemma apply to a single statement, but also add a begin/end syntax for multi-statement annotations. So, the above example would translate into something like

/*@ lemma foo: \true; */
/*@ requires: \true;
    ensures: \true;
  */
int f() { return 0; }

However, you changed the code to something like

#pragma acsl begin lemma foo: \true;
#pragma acsl requires: \true;
#pragma acsl ensures: \true;
#pragma acsl end lemma;

You would end up with

/*@ lemma foo: \true
    requires: \true;
    ensures: \true;
 */
int f() { return 0; }

Of course you could also go with end lemma foo, end foo, or even just end.