ACSL++

The reader is expected to be familiar with the ACSL specification (see ACSL Documentation).

Major differences between ACSL and ACSL++

There are a few important differences to keep in mind when writing ACSL++ annotations, or converting existing ACSL annotations to ACSL++.

  • In ACSL, there is a single namespace for logic types, variables, functions and predicates. In ACSL++, these are separate namespaces - only functions and predicates share the same namespace.
  • Moreover, logic definitions reuse the qualification of the area (namespace, class, struct or union) they are defined in.
  • Implicit casts, which would be allowed in C but not in C++, are similarly not allowed in ACSL++. For example, void pointers require explicit casts to non-void pointer types.
  • Name lookup for logic declarations will, unless explicitly qualified, start from the qualification the annotation is written in, and go up in the qualification hierarchy until the proper declaration is found.

Let’s illustrate this with an example:

//@ logic integer one = 1;       // defines `one'

class Two {
    //@ logic integer one = 2;   // defines `Two::one'
public:
    //@ ensures \result == one;  // refers to `Two::one'
    int f()
    {
        return 2;
    }
    int f2();
};

//@ ensures \result == Two::one;
int
Two::f2()
{
    return 2;
}

//@ ensures \result == one;      // refers to `one'
int
main()
{
     Two t;
     return t.f() / t.f2();
}

Logic types

Similarly to ACSL, a constructor name can not be used by more than one type declaration, within the same qualification.

Logic methods

When declared in a struct or class, all logic functions and predicates behave as member logic functions, and get an implicit this pointer argument as their first argument. This argument does not need to be provided when invoking the function or predicate from a class method.

Because of this behavior, it is currently not possible to define logic variables within classes, struct or unions - they become logic functions with a pointer as first argument.

Unlike C++, it is possible to invoke member logic functions from outside their class context, by explicitly passing a properly typed class pointer as first argument.

Logic inheritance

Every derived class will inherit the logic declarations of its base classes, and may override them. Access specifiers (private, public, and protected) are ignored.

Although logic methods can be overridden in derived classes, they can not be virtual. Because of this, when a call to a logic method is resolved, the static type of the object is used to decide which class’ methods are used.

Beware of constructs mixing virtual methods and overridden logic methods like this:

class Foo {
public:
    //@ logic integer f(integer i) = i + 1;
    virtual int virt(int i) { return i + 1; }
};

class Bar: public Foo {
public:
    //@ logic integer f(integer i) = i + 2;
    virtual int virt(int i) { return i + 2; }
};

int
main() {
    Bar bar;
    int r = bar.virt(1);
    // Here, r == 3 and bar.f(1) == 3...

    Foo &foo = bar;
    r = foo.virt(1);
    // ...but here, r == 3 and foo.f(1) == 2.

    return 0;
}

Logic operators

All the C++ and logic operators may be defined or redefined as logic methods. For example, defining operator==>() will override the implication operator.

Name lookup

Symbol names in annotations are looked up in both program (C++ code) scope and logic scope.

When the lookup result is ambiguous (i.e. the lookup is successful in both scopes), logic functions and predicates will always be preferred to C++ functions and methods, but C++ types will be preferred to logic types.

In the example below, the T in the assert line is parsed as struct T, not logic type T.

/*@ axiomatic A { type T; } */

struct T {
    int field;

    void f()
    {
        /*@ assert \exists T y; y.field > 1; */;
    }
};

Lookup is performed on the integral scope, after the complete code has been parsed and typed, therefore C++ declarations occurring after an annotation will impact the way it gets parsed.

In the following example, the assertion in function f() has to be written with an explicit g(), as simply writing g will match the C function, despite it being declared after the annotation.

This is an important difference between C and C++ parsing.

void f();

/*@ axiomatic A {
  @ logic integer g;
  @ } */

void
f()
{
    double B;
    /*@ assert B==g(); */
}

int
g()
{
    return 0;
}

Class invariants

Class invariants are properties that have to be verified at the beginning and at the end of public methods of a class.

A class invariant needs only to be declared once; its contents will be automatically added as preconditions (requires) and postconditions (ensures) of all public instance (non-static) methods.

Private methods can break the invariant as they are seen as internal helpers for an object; enforcing the invariant would be too restrictive and inconvenient.

Class invariants also apply partially to constructors and destructors of a class: constructors only have them as postconditions, while destructors only have them as preconditions.

If a class has no public instance methods, invariants declared for this class are parsed, then discarded. The following example:

struct Two {
    int x = 2;
    //@ class invariant x_is_two = x == 2;
};

…declares no methods, therefore the invariant is discarded. As soon as a public method gets declared, like this:

struct Two {
    int x = 2;
    //@ class invariant x_is_two = x == 2;
    int get() { return x; }
    bool is_two();
};

…the invariant will be applied to the methods, as if they had been declared like this:

struct Two {
    int x = 2;
    /*@ requires x_is_two: x == 2;
        ensures x_is_two: x == 2; */
    int get() { return x; }
};

/*@ requires x_is_two: x == 2;
    ensures x_is_two: x == 2; */
bool Two::is_two();

Class axiomatics

Axiomatics and lemmas defined within a class are specific to these class. An implicit \forall class_type *this: is prepended to them. This allows the predicates to refer to the class fields as well as the class logic methods.

Macro expansion

Macro expansion in ACSL++ is performed, with the following limitations:

  • # and ## operators are not allowed.
  • variadic macros are not allowed.

Constexpr in annotations

Global variables (and global variables in disguise, such as static class members) which are declared constexpr will not necessarily have actual storage in the translation unit, if their address is never taken.

As a consequence of this, annotations referring to the value of these constexpr variables would not behave as intended, due to the value being unknown.

To avoid this, constexpr global variables appearing in annotations are substituted with their values, prefixed by the mangled name of the expression being substituted. This can lead to seemingly tautological annotations in the translation, such as:

static int constexpr succ(int number) { return number + 1; }

struct PeanoAxiomatic {
    static constexpr int zero = 0;
    static constexpr int one = succ(zero);
};

int
main()
{
    //@ assert PeanoAxiomatic::zero + 1 == PeanoAxiomatic::one;
}

where the assert line will appear as:

/*@
assert (_ZN14PeanoAxiomatic4zeroE: 0)+1 ≡ (_ZN14PeanoAxiomatic3oneE: 1);
 */
;

This value substitution is performed on all types, with the following limitations:

  • member pointer are not substituted.
  • only the initialized field of unions is substituted.
  • constexpr array values are substituted only when the array is indexed with a literal constant (other constant expressions not allowed).

Templates and annotations

In the current state of the analyzer, attaching annotations to templates must follow these rules: - when attaching to a “regular” template declaration, annotations must appear after the template keyword and parameters, and before the rest of the declaration. - when attaching to a template _specialization_, annotations must appear begore the template keyword and parameters.

For example:

template <int i>
//@ ensures \result == 42;
int fortytwo() { return 42; }

//@ ensures \result == 0;
template<> int fortytwo<0>() { return 0; }

ACSL++ limitations

A few ACSL constructs are not supported yet in ACSL++:

  • external specification (“include”)
  • custom annotations (“custom”)
  • ghost code and declarations
  • volatile annotations on trivially copyable structs and unions, if they are not declared within extern “C” blocks. Such types passed by value would be otherwise translated to a copy being passed by reference, which does not match the requirement of volatile annotation accessors.
  • volatile annotations on non-trivially copyable structs and unions are not allowed.