How does CBMC handle padding bytes?

[celinval]

CBMC version: 6.4.0 Operating system: Ubuntu 22.04 Exact command line resulting in the issue: cbmc memcmp.c What behaviour did you expect: I expected the verification to fail since the memory being compared contains padding bytes. However, CBMC seems to be initializing all the padding bytes with 0s. What happened instead: Verification succeeded

Example:

#include <string.h>
#include <stdint.h>

struct WPad {
    uint8_t u8;
    uint32_t u32;
} WPad;

int main() {
    struct WPad val = { 255, 0 };
    struct WPad new_val = { 255, 0 };
    struct WPad copy = val;
    assert(memcmp(&val, &copy, 8) == 0);
    assert(memcmp(&new_val, &copy, 8) == 0);

    uint8_t* array = (uint8_t*) (void*) &val;
    assert(array[0] == 255);
    assert(array[1] == 0);
    assert(array[2] == 0);
    assert(array[3] == 0);
    assert(array[4] == 0);
    assert(array[5] == 0);
    assert(array[6] == 0);
    assert(array[7] == 0);

}

From what I can tell, the C spec says that the values of padding bytes are unspecified.

When a value is stored in an object of structure or union type, including in a member object, the bytes of the object representation that correspond to any padding bytes take unspecified values

Running the same example using gcc with address sanitizer and maybe uninitialized warnings gives me the following result:

$ gcc -o memcmp -fsanitize=undefined -g -fno-omit-frame-pointer -O2 memcmp.c -Wmaybe-uninitialized
In file included from memcmp.c:3:
memcmp.c: In function ‘main’:
memcmp.c:19:17: warning: ‘val’ may be used uninitialized [-Wmaybe-uninitialized]
   19 |     assert(array[1] == 0);
      |            ~~~~~^~~
memcmp.c:11:17: note: ‘val’ declared here
   11 |     struct WPad val = { 255, 0 };
      |                 ^~~
In file included from memcmp.c:3:
memcmp.c:20:17: warning: ‘val’ may be used uninitialized [-Wmaybe-uninitialized]
   20 |     assert(array[2] == 0);
      |            ~~~~~^~~
memcmp.c:11:17: note: ‘val’ declared here
   11 |     struct WPad val = { 255, 0 };
      |                 ^~~
In file included from memcmp.c:3:
memcmp.c:21:17: warning: ‘val’ may be used uninitialized [-Wmaybe-uninitialized]
   21 |     assert(array[3] == 0);
      |            ~~~~~^~~
memcmp.c:11:17: note: ‘val’ declared here
   11 |     struct WPad val = { 255, 0 };
      |                 ^~~

[tautschnig]

The C standard, however, also says (C11, 6.7.9 Initialization, paragraph 10)

If an object that has automatic storage duration is not initialized explicitly, its value is indeterminate. If an object that has static or thread storage duration is not initialized explicitly, then: — if it has pointer type, it is initialized to a null pointer; — if it has arithmetic type, it is initialized to (positive or unsigned) zero; — if it is an aggregate, every member is initialized (recursively) according to these rules, and any padding is initialized to zero bits; — if it is a union, the first named member is initialized (recursively) according to these rules, and any padding is initialized to zero bits;

and then (C11, 6.7.9 Initialization, paragraph 21)

If there are fewer initializers in a brace-enclosed list than there are elements or members of an aggregate, or fewer characters in a string literal used to initialize an array of known size than there are elements in the array, the remainder of the aggregate shall be initialized implicitly the same as objects that have static storage duration.

So I am not yet convinced that CBMC is getting this wrong.

[celinval]

Ah! That's a good point! The part that confuses me is this part of the General section of Representation of types:

When a value is stored in an object of structure or union type, including in a member object, the bytes of the object representation that correspond to any padding bytes take unspecified values.

So I was expecting that this assignment would generate padding bytes with unspecified values.

struct WPad copy = val;

[kroening]

struct S
{
  char ch;
  double d;
} q;

int main()
{
  struct S s = { 1, 0 };
  q = s;
}

Compiling the above with clang 14 and gcc 11.4, the following can be observed:

• clang will initialize and copy the entire struct, including the padding.
• gcc does not initialize the padding, but does copy it.

We should make the padding bytes "uninitialized".