[SystemSafety] Fwd: Re: Correcting the SECOND screw-up (grovelling apologies)

[Roberto Bagnara]

The code below is affected by undefined behavior, e.g., in the case:

   sizeof(char) == sizeof(int) == 1
   signedness of plain char == signed

independently from the integer representation adopted.
An example of such an architecture is TMS320C28x (where both chars and
ints are 16 bits wide).  On that architecture, after a few iterations
the loop will be entered with ch1 == 2730 and ch2 == 10922, so that
the right shift by 2 position (ch1 << 2) would have to compute
10922 x 2^2 = 43688, which does not fit into int, i.e., into the result
type, whence the undefined behavior.

The relevant standard paragraphs (taken from C18, but other versions
equally apply) are:

6.5.7p3
The integer promotions are performed on each of the operands. The type
of the result is that of the promoted left operand. If the value of
the right operand is negative or is greater than or equal to the width
of the promoted left operand, the behavior is undefined.

6.5.7p4
The result of E1 << E2 is E1 left-shifted E2 bit positions; vacated
bits are filled with zeros. If E1 has an unsigned type, the value of
the result is E1 x 2^E2 , reduced modulo one more than the maximum
value representable in the result type. If E1 has a signed type and
nonnegative value, and E1 x 2^E2 is representable in the result type,
then that is the resulting value; otherwise, the behavior is
undefined.

     Roberto Bagnara
     (Member of WG14 and of the MISRA C WG.  Two working groups that,
     apparently, you can insult with impunity on this list.  Ah, I am
     also a FM researcher and practitioners: bingo!)

On 7/14/20 1:36 PM, Olwen Morgan wrote:
 >
 >
 > Even screwed up the attempted correction!
 >
 > Should have formed the ch2 values using bitwise OR instead of addition:
 >
 > Corrected code is:
 >
 > #include <stdio.h>
 >
 > /* program to test for signedness of plain char in C      */
 >
 > /* assumes that all integral types have an even number of bits */
 >
 > static const char diag[2][9] = { "UNSIGNED", "SIGNED" };
 > static const char two           = (char)2;
 >
 > int main (void)
 > {
 >      int ch1 = (char)2;
 >      int ch2 = (char)((ch1 << 2) | two);
 >
 >      printf("\nPlain char signedness test: ");
 >
 >      while (ch2 != ch1)
 >      {
 >          ch1 = (char)ch2;
 >          ch2 = (char)((ch1 << 2) | two);
 >      }
 >
 >      printf ("ch1 = %i, plain char is %s\n", ch1, diag[ (ch1 < 0) ]);
 >
 >      return 0;
 > }
 >
 > Just goes to show how you can mess things up in a language you've been using for decades ... and why CbyC tooling is your friend. I feel terribly exposed writing C without decent tools.
 >
 > Heading for evidently necessary recaffeination,
 >
 > Olwen

-- 
      Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                               BUGSENG srl - http://bugseng.com
                               mailto:roberto.bagnara at bugseng.com