Open sim642 opened 5 months ago
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
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.
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_*
.
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.
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
.
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.
I extracted the problem in the issue_1140
branch.
Thanks for the minimized test case, it indeed highlights the problem. Turns out it's the same issue as https://github.com/goblint/analyzer/pull/1407#issuecomment-2037220588, but now with soundness consequences. I'll see if a quick fix to change the type would help.
During #1394 I implemented ghost witness generation for relational mutex-meet. The benchmarks revealed unsoundness which is also present on master (2fa4f55e682da3ad937e394fe20449eeef4c9634) in:
__VERIFIER_atomic_*()
) (#1441)__VERIFIER_atomic_*()
) (#1441)The unsoundness only reveals itself when activating the Apron analysis unconditionally.
For example
has 60/100 lines dead. Without unconditional apron, it has 1/104 lines dead. Oddly, if loop unrolling is disabled, things are also sound.