Unsoundness in SV-COMP Prerun

[michael-schwarz]

In the following cases we were unsound for the pre-runs:

• bitvector/s3_clnt_3.BV.c.cil-2a.yml
  • Turns into a timeout with Add proper handling of integer-overflows #121
• float-benchs/nan_double.yml
  • Still happens after merging Add proper handling of integer-overflows #121
• float-benchs/nan_float.yml
  • Still happens after merging Add proper handling of integer-overflows #121
• float-newlib/double_req_bl_1210.yml
  • Still happens after merging Add proper handling of integer-overflows #121
• float-newlib/float_req_bl_1210.yml
  • Still happens after merging Add proper handling of integer-overflows #121
• ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--iowarrior.ko.cil.yml
  • Still happens after merging Add proper handling of integer-overflows #121
  • See Fix var_eq from keeping equalities with pointers to globals #143
• pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.yml
  • Still happens after merging Add proper handling of integer-overflows #121
  • See Fix var_eq from keeping equalities with pointers to globals #143
• goblint-regression/28-race_reach_45-escape_racing.yml
  • Still happens after merging Add proper handling of integer-overflows #121
  • See Fix var_eq analysis not invalidating escaped variable #142
• ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--lustre--lustre--llite--llite_lloop.ko-entry_point.cil.out.yml
  • Fixed by 7d0fbee and unknown result on current master

[michael-schwarz]

I'll check which of these are problematic also after merging #121

[michael-schwarz]

The ones involving floats are all variations of this:

/* Assertion can be violated because uninitialized doubles can be NaN.  */

int main()
{
  double x;
  x = __VERIFIER_nondet_double();

  __VERIFIER_assert(x==x);
  return 0;
}

[sim642]

Right now on master the last one gives unknown for me. This was fixed by 7d0fbee. Does #121 break it again or what?

[michael-schwarz]

Right now on master the last one gives unknown for me. This was fixed by 7d0fbee. Does #121 break it again or what?

It doesn't I was running with the wrong property 🤦
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

[sim642]

Annoyingly, pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.yml also is because of var_eq issues, specifically the following:

 *ppos = i;
 __VERIFIER_assert(*ppos == i);

var_eq makes the assertion go through while it actually doesn't, because ppos points to a malloc-ed memory, which is shared between threads.

And I think ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--iowarrior.ko.cil.yml has a similar problem with this snippet:

  old = dev->opened;
  ldv_mutex_unlock_73(& dev->mutex);
  ldv_mutex_unlock_74(& iowarrior_open_disc_lock);
  }
  ldv_assert("", old == dev->opened);

[michael-schwarz]

Annoyingly, pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.yml also is because of var_eq issues, specifically the following:

 *ppos = i;
 __VERIFIER_assert(*ppos == i);

var_eq makes the assertion go through while it actually doesn't, because ppos points to a malloc-ed memory, which is shared between threads.

This is strange, shouldn't

analyzer/src/analyses/varEq.ml

Lines 364 to 366 in 9c5d9b0

	if Exp.is_global_var (Lval lv) = Some false
	&& Exp.interesting rv
	&& Exp.is_global_var rv = Some false

prevent any global variables from ending up in these equivalence classes? And all malloced memory is generated via Goblintutil.create_var (makeGlobalVar name voidType)