[SystemSafety] Critical systems Linux

[Olwen Morgan]

On 23/11/2018 12:33, Olivier Andrieu wrote:
>
> I’m not sure why you’re making this about the compilers. This program 
> has unequivocally an undefined behavior, so, whatever a compiler does, 
> it’s not wrong.
>
> Clang doesn’t even require an explicit warning option to point it out:
>
> |$ clang se.c se.c:14:19: warning: multiple unsequenced modifications 
> to 'i' [-Wunsequenced] PrintEvalOrder((++i), (++i), (++i)); ^ ~~ 1 
> warning generated. |

gcc gives a similar warning but still gets the compiled code wrong, AFAI 
can infer, by being gung-ho with optimisation.

As regards behaviour, AFAI can see it's not "undefined" but is covered 
by "unspecified" or "implementation-defined" behaviour (Derek Jones may 
correct me here.)

The multiple side effects on i are deliberately contrived to diagnose 
the order of evaluation of the arguments to the function call. Compile 
the following similar program with gcc:

#include <stdio.h>

static int a[3] = {0, 0, 0};

void PrintEvalOrder( int p1, int p2, int p3)
{
     printf("\np1, p2, p3 evaluated in order: p%i, p%i, p%i\n", p1, p2, p3);
     return;
}

int main(void)
{
     int i = 0;

     /* next line tests order of eval. of args to a function call */

     PrintEvalOrder((a[0]=++i), (a[1]=++i), (a[2]=++i));

     return 0;
}

and running it gives the output: "p1, p2, p3 evaluated in order: p3, p2, 
p1" , while compiling under clang and then running gives: "p1, p2, p3 
evaluated in order: p1, p2, p3".

Now, obviously, in compiling from SPARK Ada onto C, you would avoid 
usages like the above. The point I'm trying to make is that, given the 
laxness of C's definition, you cannot, AFAI can see, guarantee that any 
given subset actually steers you clear of implementation dependencies 
arising from optimisations - over which many C compilers give 
frustratingly little control.

Buy any commercial embedded C compiler and the vendors will almost all 
tell you that they pass testing using well-known validation suites 
(Plum-Hall, Perennial, and SuperTest). Yet stress test such compilers 
with Csmith, and it's by no means uncommon to encounter code generation 
errors due to faulty optimisation. Therein lies the Achilles heel of 
compiling SPARK Ada to C and compiling it with gcc.

Back in the 1990s, Programming Research Ltd. marketed a tool called QAC 
Dynamic, which aimed to augment its static checker QAC by instrumenting 
code to analyse run-time behaviour. The form of instrumentation involved 
transforming the code into a wholly applicative style, so

a = b + c

would become something like:

assign(a, add(b, c))

The trouble was that the transformation changed the behaviour of the 
program. Just a few of my pathological test programs sufficed to show 
that transformation to the applicative style changed the orders of 
evaluation of expressions and thereby invalidated the dynamic analysis. 
The instrumentation should have been transparent but it was not. If 
C-to-C translation can do that, do you feel confident that SPARK-to-C won't?

I don't.

Olwen



Olwen






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181123/13ea12ac/attachment-0001.html>