Generalized Use-After-Free in a Multithreaded setting

[Wherekonshade]

Current situation Goblint currently cannot find/analyze undefined behavior like:

Use-After-Free

There are 2 general ways this can happen:

1. Runs alright but returns a random value

#include <stdio.h>
#include <stdlib.h>

int main() {
  int *a = malloc(sizeof(int));
  if (a != NULL) {
    *a = 1;
    int *b = a;
    free(b); // detects the free even when the pointer is aliased to b
    return *a; // use after ‘free’ of ‘a’
  }
  return 0;
}

Output:

2. First couple values are somewhat random and the last six are left at a set value

#include<stdio.h>
#include<stdlib.h>

int main() {
  int* a = malloc(10*sizeof(int));
  for(int i = 0; i < 10; i++) {
    a[i] = 0xff;
  }

  free(a);

  for(int i = 0; i < 10; i++) {
    printf("%d ", a[i]); // use after free
  }
  printf("\n");
  return 0;
}

Output:

1530302590 5 1762123792 21939 255 255 255 255 255 255

Situation after Resolving this Issue Goblint can detect Use-After-Free

@vandah @edincitaku

[michael-schwarz]

This would equally apply to using a mutex after pthread_mutex_destroy has been called, and also using a condition variable after pthread_cond_destroy has been called. The additional complication is that these appear mostly in multi-threaded code, so it is not immediately obvious if @vogler's automata based approach would work here.

In fact, there one would probably require that due to MHP information it can be excluded that any accesses happen after the destroy has happened.