[CN] global ghost state and enforcing call protocols

[peterohanley]

It is not currently possible to have a global ghost variable. Here are examples of critical section/ISR enforcement and library init enforcement.

typedef enum {NORMAL, ISR, CRITICALSECTION} runstate;

runstate rs = NORMAL;

void isr(void)
/*@
  accesses rs;
  requires rs == (u32)ISR;
  ensures rs == (u32)ISR;
@*/
{

}

void entercritical(void)
/*@
  accesses rs;
  requires rs == (u32)NORMAL;
  ensures rs == (u32)CRITICALSECTION;
@*/
{

    rs = CRITICALSECTION;

}

void exitcritical(void)
/*@
  accesses rs;
  requires rs == (u32)CRITICALSECTION;
  ensures rs == (u32)NORMAL;
@*/
{

    rs = NORMAL;
}

void test(int x)
 /*@
  accesses rs;
  requires rs == (u32)NORMAL;
  ensures rs == (u32)NORMAL;
@*/
{
    entercritical();
    if (x) {
        exitcritical();
        return;
    } else {
        exitcritical();
    }
}

Note that we have to use an actual global, every function that transitively calls entercritical needs to explicitly mention the run status, and the ISR requires run status to be ISR which is valid because there are no calls to an ISR in the source, they're generated at runtime. If anything reads run status this would cause a problem.

typedef enum {NOT_READY, INITIALIZED} libstatus;

libstatus ls = NOT_READY;

int lib_foo(int x)
/*@ accesses ls;
  requires ls == (u32)INITIALIZED;
  ensures ls == (u32)INITIALIZED;
@*/
{
  return x;
}

void lib_init(void)
/*@ accesses ls;
  ensures ls == (u32)INITIALIZED;
@*/
{
    ls = INITIALIZED;
}

void test2(void)
/*@ accesses ls;
  ensures ls == (u32)INITIALIZED;
@*/
{
    lib_init();
    lib_foo(1);
}

This is an example of a library function that does not have any error checking and does not return an error code, it just uses the library state so must be called after initialization. This occurs in system bring-up for many systems, for example memory allocation is not available in very early boot or many language runtimes need to start up various subsystems.

Note that test2 needs to mention that it initialized the library.

This is currently possible but very verbose. Global ghost state will help with requiring an actual global (as well as the ridiculous cast required by the standard) but some new mechanism will be required to help with requiring a mention of every invariant at every function. Any such mechanism needs to keep in mind that the whole call graph needs to be known to propagate call requirements like this, it can't happen only on one translation unit AFAICT.

[peterohanley]

Unfortunately this would still not be enough to specify the obvious example xSemaphoreTakeFromISR because it needs locks as described in #363

[dc-mak]

Related: https://github.com/rems-project/cerberus/issues/363