[SystemSafety] Correctness by construction: Godelian oddities

[david.haworth at elektrobit.com]

Hi Olwen & all,

I've been keeping quiet for a while - especially since I think that
code verifiers have a role to play - but I can't let this one go without
comment.

In the first program, any verifier worth its salt would complain at least
once (quite aside from the use of stdio), because bitwise operations
have (unspecified) implementation defined and undefined aspects (C99)
and char might be either signed or unsigned.

MISRA (for all its warts and blemishes) has two rules that are
violated here: Use of char except for characters (line 5) and
bitwise operations on a (potentially) unsigned type (line 7).

As for the second example: as far as I know, there's no requirement
in the C standard for  an uninitialized automatic variable to contain
the same value each time it is accessed. My imaginary "Dastardly Compiler
from Hell" generates a random result for each access.

If I were a competent compiler author, I'd be tempted to write
such a compiler that produces random results every time a construct with
undefined or implementation-defined is used. Any takers?  :-)

Dave


On 2020-07-11 10:10:18 +0100, Olwen Morgan wrote:
> 
> Here is a simple program in C. On the assumption that the integer
> representation is 1C, 2C, or SM (I can't recall using a compiler that
> doesn't use one of those three), it prints 0 if plain char is unsigned and
> something negative if it is signed, according to what the integer
> representation is:
> 
> 
> #include<stdio.h>
> 
> int main(void)
> {
>     char ch = 0;
> 
>     ch = ~(ch^ch);
> 
>     printf("%i\n", (int)ch);
> 
>     return 0;
> 
> }
> 
> The only way a C verifier can prove what this program will print is for it
> to be told  *a priori* somewhere in its configuration parameters what the
> integer representation is - which is here what the program is designed to
> reveal, i.e. the functional requirement that it satisfies is to produce a
> value that permits discrimination among 1C, 2C, and SM representations.
> Otherwise, AFAI can see, the best a verifier could do would be to say that
> the output is either 0 or the relevant negative value.
> 
> One gets an even weirder program by omitting the initialisation of the
> variable ch and putting the call to printf in the return statement - which
> breaks all kinds of SPARK-like rules:
> 
> 
> #include<stdio.h>
> 
> int main(void)
> {
>     char ch;
> 
>     return printf("%i\n", (int)(~(ch^ch)));
> 
> }
> 
> According to the C standard, the access to ch in the call to printf will
> produce undefined results because ch has never been initialised. In my tests
> clang-4.0.0 warned of an uninitialised variable at compile time but gcc
> 5.4.0 did not. Nevertheless, even if the storage used for ch has
> unpredictable contents, the value will still be some bit pattern and the
> expression "~(ch^ch) will set the bits to all ones, thereby producing (under
> 1C, 2C, or SM) a defined value. Thus, although a verifier might warn of
> undefinedness, it is possible in some circumstances for the program to
> produce a result that is unambiguously defined for the purposes of
> determining the representation of the char type. Indeed, I do not know of
> any C compiler that, AFAI recall, would generate code that would bomb out or
> produce a result other than 0 or the relevant negative value. What an
> interpreter might do with it is anybody's guess but then the way an
> interpreter handles a program is closer how a verifier handles it.
> 
> Anyone got any apt names for this kind of situation? AFAI can see it's not a
> case of a long-span requirement. Perhaps one might call them "Gödelian
> oddities"?
> 
> 
> Olwen
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety