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

[michael-schwarz]

All instances of this for domains not requiring widening are now resolved. For intervals, we have small examples where one can understand the seemingly paradoxical precision relationship by tracing and understanding how widening happens.