[SystemSafety] Correctness by construction: Godelian oddities
Olwen Morgan
olwen at phaedsys.com
Tue Jul 14 12:51:11 CEST 2020
On 14/07/2020 07:48, david.haworth at elektrobit.com wrote:
> 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.
Indeed. The QAC static checker moans prolifically about this sort of
thing. But it is, in fact, a very controlled use of unspecified
behaviour (or it would be if I'd got it right - see below). The C99
definitions of the bitwise operators actually say what the effect on the
bit patterns is. What is unspecified is what the corresponding resulting
value is in the case of signed operands. The use of bitwise operators in
the first example will produce all ones in ch (though whether this is
stored as all-ones is unspecified - it may be stored as all zeros in 1C
representation).
BIG CONFESSION: I SCREWED THIS ONE UP ...AARGH !!! .... Derek Jones
will, *quite rightly*, never let me forget it ... :-)).
What I posted was an out-of-context fragment of a larger program that
subsequently checks the different possible values to discriminate
between 1C, 2C, and Sm representations. In a 1 C representation , this
will not tell you whether ch is signed or unsigned. In fact, I should
have used an alternating patterns of 0s, and 1s instead of setting
things all to 1. I'll post a correct version later on.
But the *principle* is the same. You put a controlled bit-pattern with a
MSB of 1 into a plain char and then check whether it is negative. This
kind of controlled use of unspecified aspects of program behaviour is
typically used by compiler testers to determine by testing what the
implementation-defined and unspecified aspects of a C implementation
actually are.
> MISRA (for all its warts and blemishes) ...
For which I beseech the Gods to forgive me.
<snip>
> 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? :-)
You're certainly not the first to have mulled that one over. :-))
Olwen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200714/17596b4e/attachment.html>
More information about the systemsafety
mailing list