Bug: Ultimate C translation generates incorrect union field accesses

[bahnwaerter]

The current C translation generates incorrect accesses to an union field.This issue can be reproduced with Ultimate Automizer (0.3.0-dev-23b7c4e042 with OpenJDK 21.0.9) using the following input:

union u {
    int a;
    int b;
};

int main()
{
    union u foo;

    foo.a = 10;
    foo.b = 20;

    //@ assert (foo.a == 20);
    //@ assert (foo.b == 20);

    return 0;
}

The input program is not proven to be correct as expected, because the ACSL assertion foo.a == 20 is found to be violated. The reason for this erroneous result is the incorrect generation of accesses to the union fields. The generated Boogie code for the accesses looks like this:

[...]
main_~foo~0#1!a := 10;
main_~foo~0#1!b := 20;
assert 20 == main_~foo~0#1!a;
assert 20 == main_~foo~0#1!b;
[...]

The incorrectly generated Boogie code shows that writing to the last field of a union does not invalidate the values ​​written by previous accesses. Instead, reading all fields of the union should return the last written value (assuming, according to the C standard, that the value can be reinterpreted in a suitable representation, which is the case in this example with two identical types). This error only occurs when field accesses are generated based on a LocalLValue. If the access is based on a HeapLValue, the C translation for a union works as expected, as a slightly modified program of the example witnesses:

union u {
    int a;
    int b;
};

int main()
{
    union u foo;

    foo.a = 10;
    foo.b = 20;

    int a = foo.a;
    int b = foo.b;

    //@ assert (a == 20);
    //@ assert (b == 20);

    return 0;
}

The modified program is proven to be correct, as expected. The correctly generated Boogie code for the accesses looks like this:

[...]
call write~int(10, { base: main_~#foo~0#1!base, offset: main_~#foo~0#1!offset }, 4);
call write~int(20, { base: main_~#foo~0#1!base, offset: main_~#foo~0#1!offset }, 4);
[...]
call main_#t~mem0#1 := read~int({ base: main_~#foo~0#1!base, offset: main_~#foo~0#1!offset }, 4);
main_~a~0#1 := main_#t~mem0#1;
[...]
call main_#t~mem1#1 := read~int({ base: main_~#foo~0#1!base, offset: main_~#foo~0#1!offset }, 4);
main_~b~0#1 := main_#t~mem1#1;
[...]
assert 20 == main_~a~0#1;
assert 20 == main_~b~0#1;
[...]

Since access to the shared memory is granted for all fields of a union, the reinterpreted value of the last written field is always correctly returned.

[maul-esel]

Thanks for reporting this issue.

Can you point us to the relevant parts of the C standard? I am not very familiar with unions. Intuitively, I could not be sure whether your first example program is indeed correct. On one hand, I see that if the members have the same type, it is reasonable that this could work. On the other hand, that is a very specific special case of a union, and I'd like to see if/how the C standard treats this.

In a quick search in the C99 standard, I could only find 6.2.6.1, paragraph 7:

With only this, I would say the first program is indeed incorrect. However, that doesn't mean there isn't a problem here: the generated Boogie code looks like we could prove foo.a == 10, which might also be wrong. I have a vague memory that when we assign a member of a union, we havoc the other members? But that does not seem to be the case here.

[maul-esel]

(Also, I am once again somewhat surprised which small program changes cause us to store values on the heap. I would have expected your second program to be translated in the same way as the first. 🤔 )

[bahnwaerter]

Can you point us to the relevant parts of the C standard?

You can find more information about unions in the C11 standard. First, there is an introduction of a union type in the subsection 6.2.5:

6.2.5 Types

20 [...] A union type describes an overlapping nonempty set of member objects, each of which has an optionally specified name and possibly distinct type. [...]

22 [...] Footnote 46) Note that aggregate type does not include union type because an object with union type can only contain one member at a time.

28 [...] All pointers to union types shall have the same representation and alignment requirements as each other. Pointers to other types need not have the same representation or alignment requirements.

Footnote 48) The same representation and alignment requirements are meant to imply interchangeability as arguments to functions, return values from functions, and members of unions.

The more interesting content regarding the representation and use of unions follows in subsection 6.2.6.1 and 6.5.2.3 where footnote 95 provides a particularly interesting example:

6.2.6 Representation of types

6.2.6.1 General

6 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.

7 When a value is stored in a member of an object of union type, the bytes of the object representation that do not correspond to that member but do correspond to other members take unspecified values.

6.5.2.3 Structure and union members

3 [...] Footnote 95) If the member used to read the contents of a union object is not the same as the member last used to store a value in the object, the appropriate part of the object representation of the value is reinterpreted as an object representation in the new type as described in 6.2.6 (a process sometimes called type punning). This might be a trap representation.

5 Accessing a member of an atomic structure or union object results in undefined behavior.

6.7.2.1 Structure and union specifiers

16 The size of a union is sufficient to contain the largest of its members. The value of at most one of the members can be stored in a union object at any time. A pointer to a union object, suitably converted, points to each of its members (or if a member is a bit-field, then to the unit in which it resides), and vice versa.

The following aspect mentioned in the appendix J.1 is particularly interesting: accessing a member that is not the same as the member last used to access the union is not undefined behavior, but unspecified behavior:

J.1 Unspecified behavior

• The values of bytes that correspond to union members other than the one last stored into (6.2.6.1)

Both example programs therefore exhibit unspecified behavior, like many other SV-COMP programs that use unions. The fundamental question here is how we should handle unspecified behavior from a verification perspective? Ultimate should at least issue a warning when there is unspecified behavior.

[bahnwaerter]

(Also, I am once again somewhat surprised which small program changes cause us to store values on the heap. I would have expected your second program to be translated in the same way as the first. 🤔 )

That surprised me too, and I had to reproduce it several times before I really believed it.

[maul-esel]

Ok, footnote 95 and the term "type punning" seem to be what I was missing. With that, we can also find a mention of this behaviour in GNU C: here and here (first bullet point).