C11: Translation of compound assignment into normal assignment introduces additional behavior

[michael-schwarz]

CIL lowers compound assignments such as g += 1 to normal assignments g = g + 1. For C11 programs, this is not a semantics preserving operation (see C11 draft (https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1548.pdf), 6.5.16.2)

In the program below, the assertion holds:

#include <assert.h>
#include <pthread.h>
#include <stdatomic.h>

static _Atomic int g;

void *t1(void *arg)
{
    g += 4;
    return NULL;
}

int main(void)
{
    pthread_t thread;

    pthread_create(&thread, NULL, t1, NULL);

    g += 4;

    pthread_join(thread, NULL);
    assert(g == 8);

    return 0;
}

CIL transforms the program into something like

#include <assert.h>
#include <pthread.h>
#include <stdatomic.h>

static _Atomic int g;

void *t1(void *arg)
{
    g  = g + 4;
    return NULL;
}

int main(void)
{
    pthread_t thread;

    pthread_create(&thread, NULL, t1, NULL) ;

    g = g+4;

    pthread_join(thread, NULL);
    assert(g == 8);

    return 0;
}

where after the assert g may also be 4, but no race has occurred. For usage within Goblint this is only a precision problem, but more generally I think this could be considered a miscompilation.

[michael-schwarz]

I don't really see a clean way to handle this other than complicating the CIL AST with support for compound assignment statements, and disabling lowering whenever the variable is declared to be atomic.

@sim642: Any thoughts? Perhaps we should add such a test to SV-COMP to see if other tools handle this feature in a precise way?

[sim642]

I don't really see a clean way to handle this other than complicating the CIL AST with support for compound assignment statements, and disabling lowering whenever the variable is declared to be atomic.

That seems like a very niche specialization.
It might be easier to attach a custom attribute to something to indicate that it was properly compound before Cabs2cil transformed it away. There might not be anything convenient to attach the attribute to though, maybe it could be wrapped into a CIL Block with the attribute?
I wouldn't bother with it unless we actually really want to distinguish it in Goblint and can actually get any precision out of it.

Perhaps we should add such a test to SV-COMP to see if other tools handle this feature in a precise way?

That might be a good idea because Hernan has been pushing the switch from __VERIFIER_atomic* to C11 atomics. It would probably be annoying for precise tools.