Project

General

Profile

Actions
Copy link

Bug #405

open

Unsafe drivers reported as safe on kb0032

Added by Vadim Mutilin about 14 years ago. Updated over 13 years ago.

Status:
Open
Priority:
Normal
Assignee:
-
Category:
-
Start date:
08/30/2010
Due date:
% Done:

0%

Estimated time:
Detected in build:
d58d8ff201c57c50da2c88bbf790c43c550565fc
Platform:
Published in build:

Description

Analysing the results of kbdrivers(toolset/experimenter_new/lib/kb/kb0032.txt) run in general test-set(ldv-tools/ldv-tests/regr-tests/test-sets/general/regr-task-general) I found the following:

The unsafes reported as safes in kbdrivers which descriptions are clear to me
1. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--hid--hidraw.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--hid--hidraw.c/hidraw.ko ldv_main0 safe
2. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--infiniband--core--user_mad.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--infiniband--core--user_mad.c/user_mad.ko ldv_main0 safe
3. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--s2255drv.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--s2255drv.c/s2255drv.ko ldv_main0 safe
4. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--usb--class--cdc-acm.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--usb--class--cdc-acm.c/cdc-acm.ko ldv_main0 safe
5. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--usb--serial--usb-serial.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--usb--serial--usb-serial.c/usb-serial.ko ldv_main0 safe

The unsafes which are not clear (if it really still exists) but which is now safe:
1. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--block--loop.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--block--loop.c/loop.ko ldv_main0 safe
2. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--dvb--dvb-usb--opera1.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--dvb--dvb-usb--opera1.c/opera1.ko ldv_main0 safe
3. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--au0828--au0828-video.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--au0828--au0828-video.c/au0828-video.ko ldv_main0 safe
4. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--mmc--card--sdio_uart.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--mmc--card--sdio_uart.c/sdio_uart.ko ldv_main0 safe
5. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--usb--misc--legousbtower.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--usb--misc--legousbtower.c/legousbtower.ko ldv_main0 safe

Files

Download all files
regr-task-new-general-0032 (171 KB) regr-task-new-general-0032 results of run without lattice on 8 env models and 32_1 rule model Vadim Mutilin, 09/10/2010 02:37 PM
diff_file (121 KB) diff_file results of the experiment (diff file from tests) Pavel Shved, 10/18/2010 05:47 PM

Related issues 1 (0 open — 1 closed)

Blocked by BLAST - Bug #330: Coverage check is flawed for lattice-based regions!ClosedVadim Mutilin08/03/201012/02/2010

Actions
Actions
Copy link
 #1

Updated by Pavel Shved about 14 years ago

What environment models were the drivers checked with? KB was created when an only model (sequential calls without return code checking) was implemented. Were the functions, in which there were errors, such as double locking, called at all? Haven't they been cut off by return code checking? Weren't they discarded? Did reordering of functions happen (it could affect whether double lock happened)?

Do you have answers to these questions?

Too much has changed since then. The verdicts should be reviewed now, and should be related to environment models (since we're implementing generation of multiple models).

And it seems, it's time to teach someone how to read reports...

Actions
Copy link
 #2

Updated by Vadim Mutilin about 14 years ago

Tested commit does not include new features of envgen (several models).
Detailed analysis of false safes was not done. So I could not say why we didn't found them.
But I looked at driver's code and I could definetely say that we SHOULD found them, because unsafes occur in callbacks which pretty well registered in the driver structures and double mutex lock is clear from the code. We must detect these unsafes.
The detailed analysis to be done!

Actions
Copy link
 #3

Updated by Pavel Shved about 14 years ago

What's the latest status with discrepancies in verification result of KB drivers? Is there a wiki page or something?

Actions
Copy link
 #4

Updated by Vadim Mutilin about 14 years ago

The unsafes in kbdrivers which descriptions are clear to me
1. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--hid--hidraw.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--hid--hidraw.c/hidraw.ko ldv_main0 safe
2. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--infiniband--core--user_mad.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--infiniband--core--user_mad.c/user_mad.ko ldv_main0 safe with lattice on plain_sorted_withcheck and Time limit on plain_sorted_withcheck, unsafe on the others
3. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--s2255drv.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--s2255drv.c/s2255drv.ko ldv_main0 safe with lattice and Out of memory without
4. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--usb--class--cdc-acm.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--usb--class--cdc-acm.c/cdc-acm.ko ldv_main0 unsafe (with lattice, without Out of memory)
5. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--usb--serial--usb-serial.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--usb--serial--usb-serial.c/usb-serial.ko ldv_main0 unsafe (with lattice, without Out of memory)

The unsafes which are not clear (if it really still exists):
1. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--block--loop.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--block--loop.c/loop.ko ldv_main0 unsafe
2. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--dvb--dvb-usb--opera1.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--dvb--dvb-usb--opera1.c/opera1.ko ldv_main0 safe with lattice and Time limit without lattice
3. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--au0828--au0828-video.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--au0828--au0828-video.c/au0828-video.ko ldv_main0 unsafe with lattice ant Out of mem without
4. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--mmc--card--sdio_uart.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--mmc--card--sdio_uart.c/sdio_uart.ko ldv_main0 unsafe
5. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--usb--misc--legousbtower.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--usb--misc--legousbtower.c/legousbtower.ko ldv_main0 unsafe

Actions
Copy link
 #6

Updated by Pavel Shved about 14 years ago

  • Status changed from New to Open
  • Priority changed from High to Urgent

Rising priority as decided at the planning meeting.

Actions
Copy link
 #7

Updated by Vadim Mutilin about 14 years ago

1. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--hid--hidraw.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--hid--hidraw.c/hidraw.ko ldv_main0 safe

fixed: bug in envgen: only signle space after = in structure initialization was allowed. Call to hidraw_read was not generated.

Actions
Copy link
 #8

Updated by Vadim Mutilin about 14 years ago

The drivers which are safe with lattice on plain_sorted_withcheck:
1. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--infiniband--core-- user_mad.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--infiniband--core--user_mad.c/user_mad.ko ldv_main0 safe with lattice and Time limit on plain_sorted_withcheck, unsafe on the others
2. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--video-- s2255drv.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--s2255drv.c/s2255drv.ko ldv_main0 safe with lattice and Out of memory without
3. linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--dvb--dvb-usb-- opera1.c.tar.bz2 drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--media--dvb--dvb-usb--opera1.c/opera1.ko ldv_main0 safe with lattice and Time limit without lattice

TODO: how it is related with bug #330?

Actions
Copy link
 #9

Updated by Pavel Shved about 14 years ago

In note 5 of bug #330 I describe the experiment with a modified lattice algorithm. And it seems to have worked! In most cases it just timed out, but those, which did not, yielded more correct results.

These unsafe drivers became safe.

unsafe anysee.c : Time limit -> unsafe
unsafe mtd_blkdevs : safe -> unsafe
safe mtd_blkdevs : safe -> unsafe (possible error in tests?)
unsafe hirraw : safe -> unsafe
unsafe hdpvr-video : safe -> unsafe
unsafe sdio_uart : safe -> unsafe
unsafe legousbtower : safe -> unsafe
unsafe ibmasm : OOM -> unsafe
unsafe cpia_usb : safe -> unsafe
unsafe 0077 core-message : safe -> unsafe

Note that not all drivers were verified, as I terminated the experiment.

So, perhaps, the issue is very related to bug #330. :-)

Actions
Copy link
 #10

Updated by Pavel Shved about 14 years ago

Since we know that failures in tests are mostly caused by incorrect lattice/regions implementation, I'll lower priority. We may address this bug closely after we resolve bug #330.

Actions
Copy link
 #11

Updated by Evgeny Novikov about 14 years ago

Was priority really decreased?

Actions
Copy link
 #12

Updated by Pavel Shved about 14 years ago

  • Priority changed from Urgent to Normal

:-D Thanks that you pointed it out. Fixed now.

Actions
Copy link
 #13

Updated by Vadim Mutilin almost 14 years ago

After fixing lattice there are three drivers which are safe. The description of first unsafe is clear, the others are not.
  • linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--s2255drv.c.tar.bz2
  • linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--dvb--dvb-usb--opera1.c.tar.bz2
  • linux-2.6.31.6 32_1 kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--media--video--au0828--au0828-video.c.tar.bz2
Actions
Copy link
 #14

Updated by Evgeny Novikov over 13 years ago

We have the similar task #466. But this is bug is "fresher".

Actions
Copy link

Also available in: Atom PDF