Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Keep empty ifs when wanted #140

Merged
merged 1 commit into from
Apr 14, 2023
Merged

Keep empty ifs when wanted #140

merged 1 commit into from
Apr 14, 2023

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Apr 13, 2023

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.

@sim642 sim642 added the bug label Apr 13, 2023
@sim642 sim642 added this to the 2.0.2 milestone Apr 13, 2023
@michael-schwarz michael-schwarz self-requested a review April 14, 2023 07:27
@sim642 sim642 merged commit e6b15c9 into develop Apr 14, 2023
@sim642 sim642 deleted the empty-if branch April 14, 2023 07:48
sim642 added a commit to goblint/analyzer that referenced this pull request Apr 17, 2023
nathanschmidt pushed a commit to nathanschmidt/goblint-analyzer that referenced this pull request Apr 30, 2023
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 11, 2023
CHANGES:

* Rename `Rmtmps` to `RmUnused` (goblint/cil#135).
* Add option to add return statement to `noreturn` functions (goblint/cil#129).
* Fix empty `if`s being removed (goblint/cil#140).
* Fix `_Float128` support (goblint/cil#118, goblint/cil#119).
* Fix C11 `_Alignas` computation (goblint/cil#130).
* Fix renaming and merging of `inline` functions based on C standard (goblint/cil#120, goblint/cil#124).
* Fix `Pretty` not resetting all global state between calls (goblint/cil#133, goblint/cil#134).
* Fix `fundec` location in merger (goblint/cil#139).
* Fix `cilly` patcher (goblint/cil#128).
* Disable basename by default in parser.
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

* Rename `Rmtmps` to `RmUnused` (goblint/cil#135).
* Add option to add return statement to `noreturn` functions (goblint/cil#129).
* Fix empty `if`s being removed (goblint/cil#140).
* Fix `_Float128` support (goblint/cil#118, goblint/cil#119).
* Fix C11 `_Alignas` computation (goblint/cil#130).
* Fix renaming and merging of `inline` functions based on C standard (goblint/cil#120, goblint/cil#124).
* Fix `Pretty` not resetting all global state between calls (goblint/cil#133, goblint/cil#134).
* Fix `fundec` location in merger (goblint/cil#139).
* Fix `cilly` patcher (goblint/cil#128).
* Disable basename by default in parser.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants