Relational mutex-meet unsound on ConcurrencySafety-Main

[sim642]

During #1394 I implemented ghost witness generation for relational mutex-meet. The benchmarks revealed unsoundness which is also present on master (2fa4f55) in:

• ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil (Fix relation analysis ignoring extern inits #1444)
• ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil (Fix relation analysis ignoring extern inits #1444)
• pthread-driver-races/char_generic_nvram_read_nvram_write_nvram
• weaver/popl20-more-buffer-mult.wvr (does not use locks but only __VERIFIER_atomic_*()) (Fix unsoundness from relation analysis reading special mutexes as integer variables #1441)
• weaver/popl20-more-buffer-series.wvr (does not use locks but only __VERIFIER_atomic_*()) (Fix unsoundness from relation analysis reading special mutexes as integer variables #1441)

The unsoundness only reveals itself when activating the Apron analysis unconditionally.

For example

./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/unreach-call.prp ../sv-benchmarks/c/weaver/popl20-more-buffer-mult.wvr.c --set ana.activated[+] apron

has 60/100 lines dead.
Without unconditional apron, it has 1/104 lines dead. Oddly, if loop unrolling is disabled, things are also sound.

[michael-schwarz]

For pthread-driver-races/char_generic_nvram_read_nvram_write_nvram we get:

[Error][Analyzer][Unsound] both branches over condition '*ppos >= (loff_t )nvram_len' are dead (../../sv-comp/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i:6715:6-6715:24)
[Error][Analyzer][Unsound] both branches over condition '*ppos >= (loff_t )nvram_len' are dead (../../sv-comp/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i:6732:6-6732:24)
SV-COMP result: true

[michael-schwarz]

At first glance, it seems that for pthread-driver-races/char_generic_nvram_read_nvram_write_nvram our result is correct, as the parameter ppos points to whoop_loff_t for which a blob is allocated but never initialized. I'll try to do a detailed write-up tomorrow.

[michael-schwarz]

In pthread-driver-races/char_generic_nvram_read_nvram_write_nvram there are only three references to whoo_loff_t.

• A declaration: loff_t *whoop_loff_t;

• In main: whoop_loff_t = (loff_t *) malloc(sizeof(loff_t));

• Passed as last argument (*ppos) to write_nvram, read_nvram

• main starts two threads pthread_t_write_nvram and pthread_t_read_nvram that start with whoop_wrapper_write_nvram and whoop_wrapper_read_nvram respectively. These then call write_nvram and read_nvram respectively.

• read_nvram dereference the pointer ( ssize_t lppos = *ppos;)

Thus, this tasks seems to have UB. Interestingly, fixing this does not fix the UB issues. For this to work, one needs to remove the __VERIFIER_atomic_*.

[sim642]

This is with just mutex-meet, not the experimental mutex-meet-atomic, so there should be no special handling of SV-COMP atomics. The same behavior should be observable when replacing them with a single normal pthread mutex I think.

[michael-schwarz]

Hmm, the problem seems to indeed be with the handling of atomic. I extracted this from pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.

analyzer/tests/regression/29-svcomp/35-atomic.c

Lines 1 to 26 in fa62bdd

	//PARAM: --set ana.activated[+] apron --enable ana.sv-comp.functions
	#include <pthread.h>
	#include <stdlib.h>
	#include <goblint.h>
	pthread_mutex_t mutex;
	void *fun(void* args)
	{
	pthread_mutex_lock(&mutex);
	pthread_mutex_unlock(&mutex);
	__goblint_assert(1); //Reachable
	__VERIFIER_atomic_begin();
	__goblint_assert(1); //Reachable
	__VERIFIER_atomic_end();
	__goblint_assert(1); //Reachable
	}
	int main(void)
	{
	pthread_t t;
	pthread_create(&t, ((void *)0), fun, ((void *)0));
	}

Everything after __VERIFIER_atomic_begin is reported as dead here. (The mutexes are only to demonstrate that they do not cause any issues and can be removed).

As I do not use __VERIFIER_atomic_* in the programs for my thesis, I need to focus on those benchmarks currently and cannot investigate the cause right now. But hopefully this already points in the right direction.

[michael-schwarz]

I extracted the problem in the issue_1140 branch.

[sim642]

Thanks for the minimized test case, it indeed highlights the problem. Turns out it's the same issue as #1407 (comment), but now with soundness consequences. I'll see if a quick fix to change the type would help.

[sim642]

The remaining task here was also mentioned in #1498, which should be fixed by #1492. Its initialization issue should be fixed in sv-benchmarks (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1551), but that is unrelated to our unsoundness here.