Linux Driver Verification

shvedsky-current--X--drivers--X--octrunlinux-2.6.31.6--X--32_7.pax
Bug 465 fixed

linux-2.6.31.6 with lattice on seq_one env model
BLAST_EXP_NOALIAS=1 RCV_MEMLIMIT=2000000

1. drivers/input/input.c (drivers/input/misc/ati_remote2.ko:ldv_main0_seq_one) = unsafe
2. drivers/media/radio/radio-gemtek-pci.c (drivers/media/radio/radio-gemtek-pci.ko:ldv_main0_seq_one) = unsafe

1. drivers/char/nozomi.c unsafe -- (model) builtin_expect: in ntty_write the result of mutex_trylock is checked with __builtin_expect
2. drivers/input/misc/cm109.c unsafe (preconditions) in cm109_usb_post_reset: unlock without lock. Precondition violated: usb_post_reset is always called with usb_pre_reset
3. drivers/media/video/gspca/sq905c.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
4. drivers/media/video/gspca/sq905.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
5. drivers/media/video/gspca/finepix.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
6. drivers/usb/class/cdc-wdm.c unsafe -- (preconditions) struct usb_driver: wdm_pre_reset and wdm_post_reset should be always unconditionally called

1. drivers/media/video/cafe_ccic.c (drivers/media/video/cafe_ccic.ko:ldv_main0_seq_one) = Out_of_memory
2. drivers/media/video/hdpvr/hdpvr-core.c (drivers/media/video/hdpvr/hdpvr.ko:ldv_main1_seq_one,ldv_main2_seq_one) = Out_of_memory
3. drivers/media/video/hdpvr/hdpvr-video.c (drivers/media/video/hdpvr/hdpvr.ko:ldv_main1_seq_one,ldv_main2_seq_one) = Out_of_memory
4. drivers/net/wireless/wl12xx/main.c (drivers/net/wireless/wl12xx/wl12xx.ko:ldv_main0_seq_one) = Out_of_memory
5. drivers/hid/hidraw.c (drivers/hid/hid.ko:ldv_main3_seq_one) = Out_of_memory

iceberg-current--X--drivers---X--defaultlinux-2.6.31.6--X--32_7.pax

Solver= yices, env model is plain_sorted_withcheck, mem=1500000

1. hidraw drivers/hid/hid.ko ldv_main3_plain_sorted_withcheck
2. drivers/media/radio/radio-gemtek-pci.ko ldv_main0_plain_sorted_withcheck
3. drivers/media/video/cafe_ccic.ko ldv_main0_plain_sorted_withcheck
4. core drivers/media/video/hdpvr/hdpvr.ko ldv_main1_plain_sorted_withcheck
5. video drivers/media/video/hdpvr/hdpvr.ko ldv_main2_plain_sorted_withcheck

1. drivers/input/misc/ati_remote2.ko ldv_main0_plain_sorted_withcheck safe
2. drivers/net/wireless/wl12xx/wl12xx.ko ldv_main0_plain_sorted_withcheck Exception: Failure("sanity check: mem_temp recycled? ((mem_conf@wl1251_mem_cfg).header).len")

1. drivers/serial/serial_core.c unsafe -- (model) &state->mutex: in uart_get IS_ERR check after mutex_lock_interruptible uses __builtin_expect which is undefined in the model
2. drivers/media/video/gspca/sq905c.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
3. drivers/media/video/gspca/sq905.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
4. drivers/media/video/gspca/finepix.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
5. drivers/net/cassini.c unsafe -- (preconditions) double lock of &cp->pm_mutex: first cas_open with ret<0, second cas_close. Check return value of .ndo_open before calling .ndo_stop in the structure type net_device_ops.
6. drivers/usb/core/inode.c unsafe -- (lock2) in remount,update_sb first lock &root->d_inode->i_mutex, then we iterate list_for_each_entry(bus, &root->d_subdirs, d_u.d_child) and call update_bus: second lock &bus->d_inode->i_mutex

1. drivers/media/video/cx231xx/cx231xx-cards.c unsafe -- (error???) mutex &dev->ctrl_urb_lock is not unlocked on fail path usb_control_msg<0. Where: cx231xx_read_ctrl_reg in cx231xx_usb_probe, cx231xx_init_dev: first &dev->ctrl_urb_lock in itialize_cx231xx, cx231xx_read_ctrl_reg and second &dev->ctrl_urb_lock in: cx231xx_pre_card_setup, cx231xx_set_gpio_direction, cx231xx_set_gpio_bit, cx231xx_send_gpio_cmd, cx231xx_send_vendor_cmd
2. drivers/net/wireless/iwlwifi/iwl3945-base.c == unsafe -- (error???) unlock without lock in iwl3945_pci_probe,iwl3945_hw_set_hw_params: &priv->mutex is unlock on pci_alloc_consistent!=0, but pci_alloc_consistent don't always lock it

iceberg2-current--X--drivers---X--defaultlinux-2.6.31.6--X--32_7.pax

Solver= yices, env model is seq_one, mem=1500000

1. drivers/hid/hidraw.c == unsafe -- (error) http://linuxtesting.org/results/report?num=L0014 loop in function hidraw_read(), that may not terminate
2. drivers/media/radio/radio-gemtek-pci.c == unsafe -- (error) http://linuxtesting.org/results/report?num=L0013 double lock: first time in gemtek_pci_unmute(). It calls gemtek_pci_setfrequency(),which immediately and unconditionally locks card->lock again.
3. drivers/media/video/cafe_ccic.c == unsafe -- (error) http://linuxtesting.org/results/report?num=L0001 When doing goto in cafe_pci_probe(), mutex is not unlocked.
4. drivers/media/video/hdpvr/hdpvr-core.c == unsafe -- (error) http://linuxtesting.ru/results/report?num=L0003
5. drivers/media/video/hdpvr/hdpvr-video.c == unsafe -- (error) http://linuxtesting.ru/results/report?num=L0003 in hdpvr_open() funciton mutex is unlocked after err:, while the logic suggests that it should be unlocked before it.

1. drivers/char/nozomi.c unsafe -- (model) builtin_expect: in ntty_write the result of mutex_trylock is checked with __builtin_expect
2. drivers/input/misc/cm109.c unsafe (preconditions) in cm109_usb_post_reset: unlock without lock. Precondition violated: usb_post_reset is always called with usb_pre_reset
3. drivers/media/video/gspca/sq905c.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
4. drivers/media/video/gspca/sq905.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
5. drivers/media/video/gspca/finepix.c unsafe -- (preconditions) in sd_stop0: the mutex &gspca_dev->usb_lock is immediately unlocked. Precondition of sd_stop0: mutex &gspca_dev->usb_lock must be held (called from gspca.c:gspca_stream_off)
6. drivers/net/cassini.c unsafe -- (preconditions) double lock of &cp->pm_mutex: first cas_open with ret&lt;0, second cas_close. Check return value of .ndo_open before calling .ndo_stop in the structure type net_device_ops.
7. drivers/serial/serial_core.c unsafe -- (model) &state->mutex: in uart_get IS_ERR check after mutex_lock_interruptible uses __builtin_expect which is undefined in the model
8. drivers/usb/class/cdc-wdm.c unsafe -- (32_7:preconditions) struct usb_driver: wdm_pre_reset and wdm_post_reset should be always unconditionally called (32_1:lock2) in wdm_release: &wdm_mutex, &desc->plock. Old result in kb is safe because of possible confusion: wdm_read calls mutex_lock_interruptible, compares result with zero, CBE format fails on it
9. drivers/hwmon/abituguru3.c unsafe -- {drivers/hwmon/abituguru3.ko;ldv_main0} (preconditions) unlock &data->update_lock in abituguru3_resume without lock in abituguru3_suspend. Before .resume there must be .suspend in struct platform_driver
10. drivers/media/dvb/dvb-core/dmxdev.c unsafe -- {drivers/media/dvb/dvb-core/dvb-core.ko;ldv_main1} (lock2) in dvb_demux_release, dvb_dmxdev_filter_free: first &dmxdev->mutex, second &dmxdevfilter->mutex
11. drivers/media/video/saa7134/saa7134-video.c unsafe -- {drivers/media/video/saa7134/saa7134.ko;ldv_main6} (path conditions???) in video_poll: double mutex_unlock(&fh->cap.vb_lock): if function fh->cap.ops->buf_prepare(&fh->cap,fh->cap.read_buf,fh->cap.field)) returns 0 then fh->cap.read_buf!=NULL???
12. drivers/usb/storage/usb.c unsafe -- {drivers/usb/storage/usb-storage.ko;ldv_main3} (preconditions) unlock &us->dev_mutex without lock in usb_stor_post_reset. Order: .pre_reset should be before .post_reset in struct usb_driver
13. drivers/video/aty/atyfb_base.c unsafe -- {drivers/video/aty/atyfb.ko;ldv_main0} (link:no function!) in atyfb_reboot_notify, unlock_fb_info: unlock &info->lock without lock. Function lock_fb_info which locks the mutex is implemented in drivers/video/fbmem.c while unlock_fb_info is inlined.
14. drivers/usb/core/inode.c == unsafe -- {drivers/usb/core/usbcore.ko;ldv_main17} (lock2) in remount,update_sb first lock &root->d_inode->i_mutex, then we iterate list_for_each_entry(bus, &root->d_subdirs, d_u.d_child) and call update_bus: second lock &bus->d_inode->i_mutex
15. drivers/input/misc/ati_remote2.ko -- Preconditions usb_driver

1. drivers/net/wireless/wl12xx/wl12xx.ko ldv_main0_seq_one = Out_of_mem
2. drivers/input/input.c == unsafe -- (error) http://linuxtesting.ru/results/report?num=L0015 Preconditions:??? input_devices_seq_start mutex may not be locked (no error check) and be then unlocked at input_devices_seq_stop

1. drivers/media/video/cx231xx/cx231xx-cards.c unsafe -- (error???) mutex &dev->ctrl_urb_lock is not unlocked on fail path usb_control_msg&lt;0. Where: cx231xx_read_ctrl_reg in cx231xx_usb_probe, cx231xx_init_dev: first &dev-&gt;ctrl_urb_lock in itialize_cx231xx, cx231xx_read_ctrl_reg and second &dev->ctrl_urb_lock in: cx231xx_pre_card_setup, cx231xx_set_gpio_direction, cx231xx_set_gpio_bit, cx231xx_send_gpio_cmd, cx231xx_send_vendor_cmd
2. drivers/net/wireless/iwlwifi/iwl3945-base.c unsafe -- (error???) unlock without lock in iwl3945_pci_probe,iwl3945_hw_set_hw_params: &priv->mutex is unlock on pci_alloc_consistent!=0, but pci_alloc_consistent don't always lock it

iceberg3-current--X--drivers---X--defaultlinux-2.6.31.6--X--32_7.pax

yices, mem=1500000, time=900, model=plain_sorted_withcheck

With fixed preconditions.

1. drivers/hid/hid.ko ldv_main3_plain_sorted_withcheck
2. drivers/media/radio/radio-gemtek-pci.ko ldv_main0_plain_sorted_withcheck
3. drivers/media/video/cafe_ccic.ko ldv_main0_plain_sorted_withcheck
4. drivers/media/video/hdpvr/hdpvr.ko ldv_main1_plain_sorted_withcheck
5. drivers/media/video/hdpvr/hdpvr.ko ldv_main2_plain_sorted_withcheck
6. new:drivers/net/wireless/iwlwifi/iwl3945.ko ldv_main0_plain_sorted_withcheck
7. new:drivers/media/video/cx231xx/cx231xx.ko ldv_main2_plain_sorted_withcheck

1. drivers/serial/serial_core.ko ldv_main0_plain_sorted_withcheck
2. drivers/usb/core/usbcore.ko ldv_main17_plain_sorted_withcheck

1. drivers/input/input.c == unsafe -- (error) http://linuxtesting.ru/results/report?num=L0015 Preconditions:??? input_devices_seq_start mutex may not be locked (no error check) and be then unlocked at input_devices_seq_stop
2. drivers/net/wireless/wl12xx/wl12xx.ko ldv_main0_plain_sorted_withcheck = ZZZ: Exception: Failure("sanity check: mem_temp recycled? ((mem_conf@wl1251_mem_cfg).header).len")

Not found errors:

1. drivers/input/input.c http://linuxtesting.ru/results/report?num=L0015
The file drivers/input/input.c is not built as a part of any module in allmodconfig. By default it is built as a part of input-core.o which is a kernel built-in object.
I managed to switch it off in menuconfig (allnoconfig, EMBEDED=y, VT=n) but didn't find how to set it as M.
While Kconfig defines it as:

tristate "Generic input layer (needed for keyboard, mouse, ...)" if EMBEDDED

2. drivers/net/wireless/wl12xx/wl12xx.ko http://linuxtesting.ru/results/report?num=L0029
Two bugs #506 and #507 should be fixed

Note that bebbd33 introduced some performance improvements, as of bug #511.

Another its effect is conversion from "Time limit" to "Out of memory" with CVC3, because now BLAST spends less time to generate solver queries, but, at the same time, and has a chance to impose higher load on the solver, which it can't bear under the constraints.

A lot of changes were made for last months. May be status of this task is changed?