Project

General

Profile

Actions
Copy link

Bug #1012

open

BLAST and CPAchecker do not agree on safety of certain drivers

Added by Pavel Shved about 13 years ago. Updated about 11 years ago.

Status:
New
Priority:
Normal
Assignee:
Mikhail Mandrykin
Category:
BLAST
Start date:
03/31/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
v0.2.1
Platform:
Published in build:

Description

After CPAchecker support was restored, I run driver verification on a stable revision v0.2.1. It turned out that CPAchecker, aside from being three times slower, found some errors in the drivers proved safe by BLAST. The results of CPAchecker are attached.

Files

cpa_media_32.pax (22 MB) cpa_media_32.pax CPAchecker run on drivers/media/ Pavel Shved, 03/31/2011 12:20 PM

Related issues 1 (1 open — 0 closed)

Blocked by Linux Driver Verification - Bug #1019: Our models are not correctly understood by CPAcheckerNewMikhail Mandrykin04/04/2011

Actions
Actions
Copy link
 #1

Updated by Alexey Khoroshilov about 13 years ago

Pavel Shved wrote:

It turned out that CPAchecker, aside from being three times slower, found some errors in the drivers proved safe by BLAST.

It is not surprising keeping in mind that rerouting is implemented in BLAST itself.

Actions
Copy link
 #2

Updated by Pavel Shved about 13 years ago

Alexey Khoroshilov wrote:

It is not surprising keeping in mind that rerouting is implemented in BLAST itself.

I held the comparison on 32_1 rule implemented without the rerouter. Both with BLAST and CPAchecker.

Actions
Copy link
 #3

Updated by Alexey Khoroshilov about 13 years ago

That is good to know.
Which CPAChecker UNSAFEs are not present in BLAST?

Actions
Copy link
 #4

Updated by Pavel Shved about 13 years ago

Note that this is an plain model, not sequence_infinite. Therefore, while it could be the case described in bug #1018, this requires further investigation.

In the archive uploaded the "unsafes" BLAST misses (kernel 31.6) are

BLAST says unknown, CPAchecker says unsafe:

  1. drivers/media/dvb/dvb-core/dvb-core.ko ldv_main5_plain_sorted_withcheck
  2. drivers/media/dvb/dvb-usb/dvb-usb-af9005.ko ldv_main1_plain_sorted_withcheck
  3. drivers/media/dvb/dvb-usb/dvb-usb-dw2102.ko ldv_main0_plain_sorted_withcheck
  4. drivers/media/video/cpia.ko ldv_main0_plain_sorted_withcheck
  5. drivers/media/video/cx231xx/cx231xx.ko ldv_main6_plain_sorted_withcheck

BLAST says safe, CPAchecker says unsafe:

  1. drivers/media/common/saa7146.ko ldv_main0_plain_sorted_withcheck
  2. drivers/media/common/saa7146_vv.ko ldv_main0_plain_sorted_withcheck
  3. drivers/media/dvb/dvb-usb/dvb-usb-af9015.ko ldv_main0_plain_sorted_withcheck
  4. drivers/media/dvb/dvb-usb/dvb-usb-cxusb.ko ldv_main0_plain_sorted_withcheck
  5. drivers/media/dvb/dvb-usb/dvb-usb-dib0700.ko ldv_main0_plain_sorted_withcheck
  6. drivers/media/dvb/dvb-usb/dvb-usb-gp8psk.ko ldv_main0_plain_sorted_withcheck
  7. drivers/media/dvb/dvb-usb/dvb-usb-gp8psk.ko ldv_main1_plain_sorted_withcheck
  8. drivers/media/dvb/dvb-usb/dvb-usb-vp7045.ko ldv_main0_plain_sorted_withcheck
  9. drivers/media/dvb/dvb-usb/dvb-usb-vp7045.ko ldv_main1_plain_sorted_withcheck
  10. drivers/media/dvb/firewire/firedtv.ko ldv_main1_plain_sorted_withcheck
  11. drivers/media/dvb/firewire/firedtv.ko ldv_main4_plain_sorted_withcheck
  12. drivers/media/dvb/frontends/bcm3510.ko ldv_main0_plain_sorted_withcheck
  13. drivers/media/dvb/ttusb-dec/ttusb_dec.ko ldv_main0_plain_sorted_withcheck
  14. drivers/media/video/au0828/au0828.ko ldv_main4_plain_sorted_withcheck
  15. drivers/media/video/s2255drv.ko ldv_main0_plain_sorted_withcheck
  16. drivers/media/video/zc0301/zc0301.ko ldv_main0_plain_sorted_withcheck
Actions
Copy link
 #5

Updated by Pavel Shved about 13 years ago

I analyzed drivers/media/dvb/dvb-usb/dvb-usb-cxusb.ko, and found out that CPAchecker's positive is false (see bug #1019). I guess, it is the reason of most of the CPAchecker's unsafes listed, so the investigation should be postponed.

Actions
Copy link
 #6

Updated by Evgeny Novikov about 11 years ago

  • Assignee changed from Pavel Shved to Mikhail Mandrykin

Mikhail, can you please update status of the current issue as well as #1019?

Actions
Copy link

Also available in: Atom PDF