Unsoundness on SV-COMP for No-Overflow & Memory Properties

michael-schwarz commented 4 months ago

Noticed during benchmarking of #1354 but already present on master at 8c485c924

No-Overflow

[ ] ./goblint --conf conf/svcomp24.json --sets ana.specification ~/Documents/sv-comp/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit ~/Documents/sv-comp/sv-benchmarks/c/ldv-regression/test_overflow.i (#54)

Mem-Safety

[x] ./goblint --conf conf/svcomp24.json --sets ana.specification ~/Documents/sv-comp/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit ~/Documents/sv-comp/sv-benchmarks/c/list-ext3-properties/sll_shallow_copy-2.i (#1388)

Mem-Cleanup

[x] ./goblint --conf conf/svcomp24.json --sets ana.specification ~/Documents/sv-comp/sv-benchmarks/c/properties/valid-memcleanup.prp --sets exp.architecture 32bit ~/Documents/sv-comp/sv-benchmarks/c/list-properties/list_search-1.i (#1388)
[x] ./goblint --conf conf/svcomp24.json --sets ana.specification ~/Documents/sv-comp/sv-benchmarks/c/properties/valid-memcleanup.prp --sets exp.architecture 32bit ~/Documents/sv-comp/sv-benchmarks/c/list-properties/list_search-2.i (#1388)

sim642 commented 4 months ago

The test_overflow.i task wasn't in SV-COMP 2024 as such: at that sv-benchmarks repo tag, it didn't have a no-overflow property. This was added later in https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1526 to fix https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1405.

Since the task actually is specific to 32bit, but we use the current machine's CIL Machdep for everything, we'll be wrong. Therefore, we'll have to finally implement #54, there's no way around it anymore. It's surprising that SV-COMP hasn't had an overflow task specifically to check the 32bit vs 64bit difference.

I didn't check the others, but they could also be tasks that were excluded from SV-COMP 2024 due to last-minute modifications.

michael-schwarz commented 3 months ago

For at least one of the mem-cleanup issues, there is another separate problem from what #1354 fixes for the relational analyses:

// PARAM: --set ana.malloc.unique_address_count 2 --enable ana.autotune.enabled --set ana.autotune.activated  "['singleThreaded']"

typedef struct list {
 int key;
 struct list *next;
} mlist;

mlist *head;

mlist* search_list(mlist *l, int k){
  l = head;
  while(l!=((void *)0) && l->key!=k) {
    l = l->next;
  }
  return l;
}

int insert_list(mlist *l, int k){
  l = (mlist*)malloc(sizeof(mlist));
  l->key = k;
  if (head==((void *)0)) {
    l->next = ((void *)0);
  } else {
    l->key = k;
    l->next = head;
  }
  head = l;
  return 0;
}

int main(void){
  mlist *mylist;
  insert_list(mylist,2);
  insert_list(mylist,5);

  search_list(head,2);

  __goblint_check(1);
}

In this config, the analysis claims that search_list does not return.

michael-schwarz commented 3 months ago

Other than the No-Overflow for which Simmo described the issue above, the other three are fixed when setting --enable dbg.full-output and are thus regressions of #1312 (see #1388).

goblint / analyzer