Invalid memory access in DeviceDriversLinux64
Created by: shaobo-he
Hi guys,
I found several problematic benchmarks that contain invalid memory access in DeviceDriversLinux64 category. For each benchmark, I will briefly describe the problem and its witness file can be found in a github repo (https://github.com/Guoanshisb/BenchmarksWithInvalidDerefs).
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
main
calls az6007_tuner_attach
with an local uninitialized pointer var_group4
as the argument. At line 8295, __cil_tmp27
is dereferenced which is var_group4
plus an offset.
ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c
main
calls ttm_bo_vm_fault
with two local uninitialized pointer var_group1
and var_group2
. The first argument is derefenced multiple times in this function. For example, at line 9887, an uninitialized function pointer is dereferenced which can alias to any function with identical signature.
ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--pcmcia--pcmcia.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c
pccard_show_cis
is called by main
with two local uninitialized pointers var_group1
and var_group2
as arugments. pccard_validate_cis
is called by pccard_show_cis
with a argument which is essentially var_group2
plus an offset. This argument is passed around and dereferenced directly or indirectly.
ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call.cil.out.c
main
calls rtl8150_probe
with global pointer rtl8150_driver_group1
as an argument, which is not assigned to any memory location. rtl8150_probe
then calls interface_to_usbdev
which dereferences rtl8150_driver_group1
.