goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
40 stars 16 forks source link

Keep empty ifs when wanted #140

Closed sim642 closed 1 year ago

sim642 commented 1 year ago

Currently CIL removes empty if statements like

if (x) {
}

For Goblint's use case there are two reasons to keep them, just like we prevent removal of other kinds of branching from the CFG:

  1. We are unsound by missing races to variables in the conditional expression

    #include <pthread.h>
    #include <stdio.h>
    
    int myglobal;
    pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
    pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
    
    void *t_fun(void *arg) {
      pthread_mutex_lock(&mutex1);
      if (myglobal) { // RACE!
    
      }
      pthread_mutex_unlock(&mutex1);
      return NULL;
    }
    
    int main(void) {
      pthread_t id;
      pthread_create(&id, NULL, t_fun, NULL);
      pthread_mutex_lock(&mutex2);
      myglobal=myglobal+1; // RACE!
      pthread_mutex_unlock(&mutex2);
      pthread_join (id, NULL);
      return 0;
    }
  2. In automaton witnesses when speaking about branching edges, we should account for all branching edges present in the actual code and not implementation-dependently exclude those which we can syntactically eliminate.