Mutex-Meet-TID less precise than Mutex-Meet

[michael-schwarz]

On this program

#include<pthread.h>
#include<stdlib.h>

void i() {
  char j, k = 0;
  int* f = malloc(8);

  while (k < j)
    k++;

  int r = *f;
}

void* l(void* args) {

};


void main() {
  pthread_t t;
  pthread_create(&t, 0, l, NULL);

  while (1)
    i();
 }

We observe

  Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(no-clusters,join)): [|j#1527+128.>=0; -j#1527+127.>=0; -j#1527+k#1528>=0; j#1527+k#1528+128.>=0;
    k#1528>=0; -j#1527-k#1528+382.>=0; j#1527-k#1528+128.>=0; -k#1528+255.>=0;
    -j#1527+r#1531+2147483775.>=0; j#1527+r#1531+2147483776.>=0;
    -k#1528+r#1531+2147483903.>=0; k#1528+r#1531+2147483648.>=0;
    r#1531+2147483648.>=0; -j#1527-r#1531+2147483774.>=0;
    j#1527-r#1531+2147483775.>=0; -k#1528-r#1531+2147483902.>=0;
    k#1528-r#1531+2147483647.>=0; -r#1531+2147483647.>=0|] (env: [|0> j#1527:int;
                                                                   1> k#1528:int;
                                                                   2> r#1531:int|])
  less precise than
  Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPriv): [|j#1527+128.>=0; -j#1527+127.>=0; -j#1527+k#1528>=0; j#1527+k#1528+128.>=0;
    k#1528>=0; -j#1527-k#1528+254.>=0; j#1527-k#1528+128.>=0; -k#1528+127.>=0;
    -j#1527+r#1531+2147483775.>=0; j#1527+r#1531+2147483776.>=0;
    -k#1528+r#1531+2147483775.>=0; k#1528+r#1531+2147483648.>=0;
    r#1531+2147483648.>=0; -j#1527-r#1531+2147483774.>=0;
    j#1527-r#1531+2147483775.>=0; -k#1528-r#1531+2147483774.>=0;
    k#1528-r#1531+2147483647.>=0; -r#1531+2147483647.>=0|] (env: [|0> j#1527:int;
                                                                   1> k#1528:int;
                                                                   2> r#1531:int|])
  diff: -j#1527-k#1528+254.>=0, -k#1528+127.>=0, -k#1528+r#1531+2147483775.>=0, -k#1528-r#1531+2147483774.>=0

Mutex-Meet-TID: -k#1528+255.>=0;
Mutex-Meet: -k#1528+127.>=0;

This could be related to widening / narrowing but that seems unlikely at first glance.

[michael-schwarz]

The culprit seems to be enabling mutex-meet-tid from base for the TID configuration vs sticking with mutex-meet from base where TIDs are not enabled.

[michael-schwarz]

#include<pthread.h>
#include<stdlib.h>
struct a {
  int (*b)();
} r;

struct a* t;
int m() {}

void* j(void* arg) {};

void main() {
    pthread_t tid;
    pthread_create(&tid, 0, j, NULL);
    t = calloc(1, sizeof(struct a));
    t->b = &m;
    r = *t;
    invalidate(&t);
}

This is an example extracted from another program. Here, the difference is:

[Debug] node 9 "return (0);": Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(no-clusters,join)) less precise than Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPriv)
  Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(no-clusters,join)): top (env: [||])
  less precise than
  Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPriv): bottom (env: [||])
  diff: -1.>=0

[michael-schwarz]

The difference is there even when the relational domain is disabled completely.

[michael-schwarz]

It seems mutex-meet-tid considers m reachable from invalidate, whereas mutex-meet does not...

[michael-schwarz]

For the other program the issue is addressed by #1558.

[michael-schwarz]

For the original program, one can get rid of the infinite loop and ends up with:

#include<pthread.h>
#include<stdlib.h>

void i() {
    signed char j, k = 0;
    int* f = malloc(8);

    while (k < j)
      k++;

    int r = *f;
  }


void* l(void* args) {

};


void main() {
  pthread_t t;
  pthread_create(&t, 0, l, NULL);

  i();
  i();
 }

[michael-schwarz]

After the fixes in #1558, setting widen=join for Apron removes the precision differences. Other such effects are likely due to widening and narrowing as well.