Problem due to initialisation of statically defined variables

[hernanponcedeleon]

Our analysis returns PASS for this program while it should clearly return FAIL since the use of different mutexes does not guarantee mutual exclusion.

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

int data[10];
pthread_mutex_t m[10];

void *t_fun(void *arg) {
  pthread_mutex_lock(&m[4]);
  int in = data[4];
  data[4]++; // RACE!
  int out = data[4];
  assert(out == in + 1);
  pthread_mutex_unlock(&m[4]);
  return NULL;
}

int main() {
  for (int i = 0; i < 10; i++)
    pthread_mutex_init(&m[i], NULL);

  pthread_t id;
  pthread_create(&id, NULL, t_fun, NULL);
  pthread_mutex_lock(&m[3]);
  int in = data[4];
  data[4]++; // RACE!
  int out = data[4];
  assert(out == in + 1);
  pthread_mutex_unlock(&m[3]);
  return 0;
}

[hernanponcedeleon]

I think I finally have a working solution for the allocation of memory (might not be optimal yet, but at least I think it is correct).

For bpl programs, there are three ways an Address is created

• using programBuilder.getOrCreateLocation
• using programBuilder.addDeclarationArray
• using programBuilder.initLocEqConst

The first case is the usual way of creating variables from visitVar_decl.

The second method is only used when boogie assigned a fixed address to a variable. Here we use the information provided by smack via the allocSize tag to know the size. While this size might be bigger than the addresses that are actually accessed (e.g. for int x we will get const x {:allocSize 4} at the boogie level, but the rest of the program will always access it as x or x+0). In the worst case scenario, I think we fully need all these addresses (see * below). For arrays smack also provides a count tag specifying the number of elements, but we cannot use this one because future accesses are at the byte level, i.e. array[2] results in const {:count 2} {:allocSize 8} and then array[1] results in array+4 which would be an overflow if we use size 2.

The third case is when we get information from __SMACK_static_init. In general programBuilder.initLocEqConst could create new addresses if they do not exists, but since __SMACK_static_init is parsed after the global constants, this method will never create new addresses.

(*) For the time being, I don't see an easy way of getting rid of some of these "extra" addresses. If the program does not load addresses via Loads, our alias analysis might be quite precise and we could have a pass that checks addresses that are never read and remove them. But this relies on alias analysis which is normally the reason why we want a small address space, so we end up in kind of a circular dependency. The experiments I just did suggest that even a huge memory space might not impact performance (unless we compute addresses from Loads like in benchmarks like M&S). @ThomasHaas and I discussed the idea of using some information coming from __SMACK_static_init, but this does not always provides information for structures (see this file at commit f10092f which only initialises one of the fields of the structure using $M.0 := $store.ref($M.0, lock, $0.ref);).

[ThomasHaas]

The issue with arrays is only a problem if the array contains structs. If it does not, you can use the allocation size as well as the count to infer the offsets via offset = allocSize / count. And then you create count many addresses, each with an offset of k*offset (0 <= k < count). But I guess we cannot know if it contains structs or not.

[hernanponcedeleon]

The problem was solved by f10092f.

The program in this issue was a reachability variant on some wrong results we got in the data-race category in svcomp 2022. Most of those problem are also fixed now. I added regressions tests in 83f1b1b.