Protection-Based Privatization more Precise than Write-Centered

[michael-schwarz]

Starting from minimizing one of the larger programs, I have now arrived at this example program, where the Protection-Based Privatization is more precise than the Write-Centered (without intervals or other domains that require a widening).

#include<pthread.h>
#include<stdlib.h>
struct a {
  struct a *b;
  struct a *c;
};

struct a i;

pthread_mutex_t m;

void doit() {
  void *newa = malloc(sizeof(struct a));

  pthread_mutex_lock(&m);
  i.c->b = newa;
  i.c = newa;
  pthread_mutex_unlock(&m);
}

void* k(void *arg) {
  doit();
  return NULL;
}

int main() {
    struct a other;
    i.c = &other;

    pthread_t t1;
    pthread_create(&t1, 0, k, 0);

    doit();
    return 0;
}

The program compiles with GCC and runs without segfaults.

Script to run comparison: ./goblint --conf conf/traces.json --set ana.base.privatization protection 2.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.protection.prec && ./goblint --conf conf/traces.json --set ana.base.privatization write 2.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.write.prec && ./privPrecCompare level-ip.protection.prec level-ip.write.prec &> out.txt

The diff output is:

[Debug] 2.c:17:3-17:13 (alloc@sid:10@tid:[main]): protection more precise than write
  protection: {
                b -> {&(alloc@sid:10@tid:[main])}
                c -> Uninitialized
              }
  more precise than
  write: (value:{
                  b -> {&(alloc@sid:10@tid:[main]), &(alloc@sid:10@tid:[main, k@2.c:31:5-31:33])}
                  c -> Uninitialized
                }, size:(16,[16,16],{16}), no zeroinit:true)
  reverse diff: compound: (value:{
                                   b -> {&(alloc@sid:10@tid:[main]), &(alloc@sid:10@tid:[main, k@2.c:31:5-31:33])}
                                   c -> Uninitialized
                                 }, size:(16,[16,16],{16}), no zeroinit:true) not same type as {
                                                                                                   b -> {&(alloc@sid:10@tid:[main])}
                                                                                                   c -> Uninitialized
                                                                                                 }

[Debug] 2.c:17:3-17:13 (alloc@sid:10@tid:[main, k@2.c:31:5-31:33]): protection more precise than write
  protection: {
                b -> {&(alloc@sid:10@tid:[main, k@2.c:31:5-31:33])}
                c -> Uninitialized
              }
  more precise than
  write: (value:{
                  b -> {&(alloc@sid:10@tid:[main]), &(alloc@sid:10@tid:[main, k@2.c:31:5-31:33])}
                  c -> Uninitialized
                }, size:(16,[16,16],{16}), no zeroinit:true)
  reverse diff: compound: (value:{
                                   b -> {&(alloc@sid:10@tid:[main]), &(alloc@sid:10@tid:[main, k@2.c:31:5-31:33])}
                                   c -> Uninitialized
                                 }, size:(16,[16,16],{16}), no zeroinit:true) not same type as {
                                                                                                   b -> {&(alloc@sid:10@tid:[main, k@2.c:31:5-31:33])}
                                                                                                   c -> Uninitialized
                                                                                                 }

The difference because of blob / no-blob is disregarded by the comparison, so the issue of interest seem to be the points-to sets that are smaller for protection.

This already is on my branch (c.f. #1417) where a lot of the critical precision-comparison issues should be solved.

[sim642]

The difference because of blob / no-blob is disregarded by the comparison, so the issue of interest seem to be the points-to sets that are smaller for protection.

I find the blob vs no-blob difference already quite noteworthy. The two differences correspond to the two cases that have been merged in the blob. I think if the types matched for both (either both blobs or non-blobs), then they should both be merged or unmerged and the difference should disappear.

[michael-schwarz]

After some further simplification, we end up with

#include<pthread.h>
#include<stdlib.h>
struct a {
  struct a *b;
};

struct a *ptr;


pthread_mutex_t m;

void doit() {
  void *newa = malloc(sizeof(struct a));

  pthread_mutex_lock(&m);
  ptr->b = newa;
  ptr = newa;
  pthread_mutex_unlock(&m);
}

void* k(void *arg) {
  doit();
  return NULL;
}

int main() {
    struct a other;
    ptr = &other;

    pthread_t t1;
    pthread_create(&t1, 0, k, 0);

    doit();
    return 0;
}

[michael-schwarz]

I experimentally disabled widening, and as assumed, this problem is unrelated to widening.

[michael-schwarz]

It seems that, in fact, in the concrete, the variable can never have the value

(alloc@sid:10@tid:[main]): protection more precise than write
  protection: {
                b -> {&(alloc@sid:10@tid:[main])}
              }

claimed by the more precise privatization, as ptr->b is modified before ptr is set to the newly allocated blob, and this must, therefore, refer either to orig or to the blob allocated by the other thread.

[michael-schwarz]

With #1458, the original example works here. However, we get a new counterexample:

#include<pthread.h>
struct a {
  char* b;
};

struct a *c;
struct a h = {""};
struct a i = {"string"};

void* d(void* args) {
  struct a r;
  if (c->b)
    r = *c;
}

int main() {
  int top;

  if(top) {
    c = &h;
  } else {
    c = &i;
  }

  pthread_t t;
  pthread_create(&t, 0, d, 0);
  return 0;
}

[Debug] 2.c:13:5-13:11 h: protection more precise than write
  protection: {
                b -> {""}
              }
  more precise than
  write: {
           b -> {(unknown string)}
         }
  reverse diff: {Map: b = Map: (unknown string) = Map: (unknown string) = address (lval (offset (IntDomLifter(intdomtuple)))): (unknown string) not leq "" ...}

[Debug] 2.c:13:5-13:11 i: protection more precise than write
  protection: {
                b -> {"string"}
              }
  more precise than
  write: {
           b -> {(unknown string)}
         }
  reverse diff: {Map: b = Map: (unknown string) = Map: (unknown string) = address (lval (offset (IntDomLifter(intdomtuple)))): (unknown string) not leq "string" ...}

[Debug] 2.c:13:5-13:11 h: write less precise than protection
  write: {
           b -> {(unknown string)}
         }
  less precise than
  protection: {
                b -> {""}
              }
  diff: {Map: b = Map: (unknown string) = Map: (unknown string) = address (lval (offset (IntDomLifter(intdomtuple)))): (unknown string) not leq "" ...}

[Debug] 2.c:13:5-13:11 i: write less precise than protection
  write: {
           b -> {(unknown string)}
         }
  less precise than
  protection: {
                b -> {"string"}
              }
  diff: {Map: b = Map: (unknown string) = Map: (unknown string) = address (lval (offset (IntDomLifter(intdomtuple)))): (unknown string) not leq "string" ...}

protection more precise than write    (equal: 4, more precise: 2, less precise: 0, incomparable: 0, total: 6)
write less precise than protection    (equal: 4, more precise: 0, less precise: 2, incomparable: 0, total: 6)

[michael-schwarz]

With this modification, it is even observable as an assertion failing resp. succeeding:

// PARAM: --set ana.base.privatization write
#include<pthread.h>
struct a {
  char* b;
};

struct a *c;
struct a h = {""};
struct a i = {"string"};

void* d(void* args) {
  struct a r;
  if (c->b) {
    __goblint_check(strlen(h.b) == 0); // Works for protection
  }
}

int main() {
  int top;

  if(top) {
    c = &h;
  } else {
    c = &i;
  }

  pthread_t t;
  pthread_create(&t, 0, d, 0);
  return 0;
}

[michael-schwarz]

It seems like this check does not trigger here when it should:

analyzer/src/analyses/base.ml

Lines 1616 to 1625 in bffc5e3

	else if invariant then (
	(* without this, invariant for ambiguous pointer might worsen precision for each individual address to their join *)
	try
	VD.meet old_value new_value
	with Lattice.Uncomparable ->
	new_value
	)
	else
	new_value
	in

[michael-schwarz]

There is something strange going on with the meet:

%%% set: (tests/regression/13-privatized/89-write-lacking-precision.c:13:7-13:11)   meety-meet-meet:update_offset {
    b -> {""}
  } \sqcap {
        b -> {(unknown string)}
      } = {
            b -> {(unknown string)}
          }

[michael-schwarz]

There remains at least one case of this. I did a creduce run on it overnight, but I'll have to see whether it came up with something useful.

[michael-schwarz]

The resulting program now is

#include<pthread.h>
#include<stdlib.h>
#include<string.h>
union g {
  int h;
  char i;
};
struct j {
  union g data;
};
struct j *jptr;

void* af(void* arg) {
  jptr = (struct j*) malloc(sizeof(struct j));
  memset(jptr, 0, sizeof(struct j));

  while (1) {
    if (jptr->data.i)
    ;
  }
}

void main() {
  pthread_t ah;
  pthread_create(&ah, 0, af, 0);
}

where we have

[Debug] 2.c:18:9-18:21 (alloc@sid:10@tid:[main, af@2.c:25:3-25:32]): protection more precise than write
  protection: (value:{
                       data -> (lifted fieldinfo:fieldinfo:h, compound:(0,[0,0],{0}))
                     }, size:(4,[4,4],{4}), no zeroinit:true)
  more precise than
  write: (value:{
                  data -> (lifted fieldinfo:Unknown field, compound:Unknown)
                }, size:(4,[4,4],{4}), no zeroinit:true)
  reverse diff: {Map: data = Unknown field instead of fieldinfo:h ...}