Covering all interlacings in a single short context

Answering the two questions from last post in reverse order:

What shorter analysis context would test arbitrarily long sequences of interrupts, with repetitions?

There was a hint in the previous post in the link to the Skein-256 tutorial. A stronger hint would have been to link directly to this post [removed dead link] where an analysis context that encompasses many possible executions is offered. The analysis context there is for arbitrary numbers of calls to Skein_256_Update() and the key part of the analysis context is:

  ...
  Skein_256_Init(&skein_context  HASHLEN * 8);
  while (Frama_C_interval(0 1))
    {
      for (i=0; i<80; i++)
        msg[i] = Frama_C_interval(0  255);
      Skein_256_Update(&skein_context  msg  80);
    }
  Skein_256_Final( &skein_context  hash);
  ...

By similarity with the above example an analysis context for arbitrarily long sequences of interrupts with repetitions can be written:

...
void analysis_context(void)
{
  main();
  while (Frama_C_interval(0 1))
    {
       if (Frama_C_interval(0 1)) interrupt_device1();
       if (Frama_C_interval(0 1)) interrupt_device2();
       if (Frama_C_interval(0 1)) interrupt_device3();
    }
}

Most pitfalling value analysis usability pitfall number one: when using Frama_C_interval() one should not forget to include file builtin.c as part of the analysis project.

The first question was actually more difficult:

What shorter analysis context would test in a single analysis exactly the same behaviors as the lengthy six entry points ?

Answer: the function below would.

int called1  called2  called3;
...
void analysis_context(void)
{
  main();
  while (!(called1 && called2 && called3))
    {
       if (Frama_C_interval(0 1) && !called1) { called1 = 1; interrupt_device1(); }
       if (Frama_C_interval(0 1) && !called2) { called2 = 1; interrupt_device2(); }
       if (Frama_C_interval(0 1) && !called3) { called3 = 1; interrupt_device3(); }
    }
}

Variables called1 called2 called3 are defined as zero-initialized global variables and are used to remember whether each interrupt has already been called.

The value analysis will provide results that hold for all possible executions of the above context. It does not matter that some of the possible executions of the above code escape in livelock and fail to terminate. All the executions in which the three interrupts are called in some order and the program then terminates are taken into account which is what matters for verifying safety.

To reiterate we are not yet worried about how the verification will be done at this stage. It may turn out later that changing the context code slightly makes it easier while still covering all the same executions. Or the value analysis may be able to brute-force its way through with an option such as -slevel-function analysis_context:33. We'll let the person in charge of verification make his choices and justify them if he needs to. Writing the analysis context is in a way a specification activity. While not completely ignoring the verification's feasibility it should be done without worrying too much about such details.

And what if the execution of interrupts are in fact interlaced (that is if they are in fact interruptible)? There is a plug-in for that (a phrase I would like to suggest as new Frama-C slogan). That plug-in is not distributed at this stage but if you are interested in the verification of comparatively precise properties on code with fine-grained concurrency write in and we'll tell you about it.

Post-scriptum: here is a complete example:

int t[20]  s[30];
int *p  i  r;
main()
{
  p = t;
  i = 0;
}
void interrupt_device1(void)
{
  r = p[i + Frama_C_interval(0 9)];
}
void interrupt_device2(void)
{
  p = (Frama_C_interval(0 1)) ? t : (s + Frama_C_interval(0 10));
}
void interrupt_device3(void)
{
  i = Frama_C_interval(0 10);
}
void analysis_context(void)
{
  main();
  while (Frama_C_interval(0 1))
    {
       if (Frama_C_interval(0 1)) interrupt_device1();
       if (Frama_C_interval(0 1)) interrupt_device2();
       if (Frama_C_interval(0 1)) interrupt_device3();
    }
}

For some reason this example does not even need the -slevel option to be found safe:

$ frama-c -val -main analysis_context  .../share/builtin.c t.c
...
[value] Values for function analysis_context:
          p ∈ {{ &t ; &s + [0..40] 0%4 }}
          i ∈ [0..10]
          r ∈ {0}
...

Oh variable r remains zero throughout the infinite loop. The silliness of my examples sometimes...