analyzer
analyzer copied to clipboard
goblint
Unsoundness for Two SV-Comp benchmarks
- [ ]
ldv-validator-v0.6/linux-stable-af3071a-1-130_7a-drivers--hwmon--s3c-hwmon.ko-entry_point.cil.c - [ ]
ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--input--touchscreen--usbtouchscreen.ko-entry_point.cil
The first benchmark seem to miss some sort of initialization (setting s3c_hwmon_driver_group0 to anything other than what zalloc yields), which leads to an immediate abort in s3c_hwmon_probe, making code further down that is supposed to contain the call to reach_error unreachable.
I think it might be mislabled (CPAChecker and PESCO somehow produce a counterexample, I'll try to inspect that)
Originally posted by @michael-schwarz in https://github.com/goblint/analyzer/issues/755#issuecomment-1181526369
When I did SV-COMP performance comparisons for #770, I actually saw 5 unsound tasks, including the ones you listed above: https://goblint.cs.ut.ee/results/72-all-fast-evalint-opt-after/table-generator.table.html#/table?filter=0(0status(category(in(wrong)))). Have you not seen the others in your recent SV-COMP runs? Maybe those are just in categories you haven't included recently?
The fourth one is the one fixed in #755, the other two might well be there additionally, these two are the ones we noticed a while back with affine equalities.
Right now these two are the only two unsoundness cases that haven't been dealt with AFAIK. Are you still planning to look into these?
Both are still there with the most recent Goblint version in the sv-comp config.
Plus we newly have
- [x]
ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--iowarrior.ko.cil.yml
iowarrior is not new, but it hasn't just been mentioned in any issue. The program itself is problematic, so there's already an sv-benchmarks MR for it: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1374 (EDIT: merged).
Both of the two tasks stem from the same problem: due to all zero memory from ldv_zalloc, a lot of the code is dead.
CPAchecker's violation witness for the first one actually hinges on the fact that ldv_zalloc may explicitly return NULL and that is dereferenced (to an arbitrary value I guess). In our SV-COMP configuration we assume that doesn't happen (#838).
So really the problem is with the programs. I made a MR to change them to valid-deref instead: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1392.