RTEMS qualification and code annotations

[Andrew Butterfield]

Dear RTEMS developers,

as some of you may be aware, I am leading a task as part of the RTEMS
Qualification activity that explores the use of formal methods to assist with
code verifications.

Some of these techniques work best if annotations are added to source code, but
these annotations are *not* lightweight.

I am fairly sure that having these annotations in code is not going to be
viable, and neither is maintaining two code versions, one with annotations, and
one without.

PROPOSAL (part 1):

Lightweight annotation - that just identifies the relevant code point, with a
separate file that provides the full annotation. We add an annotation
pre-processor step that merges the two before handing off to the relevant tool.
(part 2 shows how this might work in an example below: `max_seq`)

We would all be very interested in your feedback.

The rest of this email shows some concrete examples to give you some idea of
what is involved (based on a tool called Frama-C that has been used by Airbus,
among others).

A header file with pre-/post condition annotations:
  swap.h:
        /*@ requires \valid(a) && \valid(b);
        @ ensures A: *a == \old(*b) ;
        @ ensures B: *b == \old(*a) ;
        @ assigns *a,*b ;
        @*/
      void swap(int *a,int *b) ;

The implementation, *in this case*,  needs no further annotations

  swap.c:
      #include "swap.h"

      void swap(int *a,int *b)
      {
        int tmp = *a ;
        *a = *b ;
        *b = tmp ;
        return ;
      }

It illustrates that annotations associated with a C function (pre- and
post-conditions) can be put in the header file, which is where you currently use
Doxygen to document the function call. This is probably fairly low impact from
your perspective.

However, if the implementation code contains loops, then we need annotations in
the code at those loops. The following, from the Frama-C ACSL Tutorial
(https://frama-c.com/acsl_tutorial_index.html) shows the annotations required to
verify the correctness of a function that finds the maximum of a sequence of
integers.

  maxseq.c:
        int max_seq(int* p, int n) {
          int res = *p;
          //@ ghost int e = 0;
          /*@ loop invariant \forall integer j;
                   0 <= j < i ==> res >= \at(p[j],Pre);
              loop invariant
                   \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res;
              loop invariant 0<=i<=n;
              loop invariant p==\at(p,Pre)+i;
              loop invariant 0<=e<n;
          */
          for(int i = 0; i < n; i++) {
            if (res < *p) {
              res = *p;
              //@ ghost e = i;
            }
            p++;
          }
          return res;
        }

20 lines of code, of which 10 are annotations.

PROPOSAL (part 2):

We have maxseq.a:
    maxseq.loop
    //@ ghost int e = 0;
    /*@ loop invariant \forall integer j;
            0 <= j < i ==> res >= \at(p[j],Pre);
       loop invariant
            \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res;
       loop invariant 0<=i<=n;
       loop invariant p==\at(p,Pre)+i;
       loop invariant 0<=e<n;
    */
    maxseq.body
      //@ ghost e = i;

and maxseq.c looks like:
        int max_seq(int* p, int n) {
          int res = *p;
          //@ maxseq.loop
          for(int i = 0; i < n; i++) {
            if (res < *p) {
              res = *p;
              //@ maxseq.body
            }
            p++;
          }
          return res;
        }

Again, feedback would be much appreciated!

Best regards,
  Andrew Butterfield

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------