Found undefined behaviour in ldv programs (!1498) · Merge requests · SoSy-Lab / Benchmarking / SV-Benchmarks

Francesco Parolini requested to merge parof/sv-benchmarks:ldv-fix into main Nov 17, 2023

Me and @rmonat found some ldv benchmarks where there are undefined behaviours which might be mislabelled. In the file c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i there are two pointers that have offsets that are too huge to be correct:

✗ Check #427:
../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i: In function 'is_new_interface':
../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:6572.35-47: error: Invalid memory access
  
  6572:   __builtin_prefetch((void const *)e->link.next);
                                           ^^^^^^^^^^^^  
  accessing 8 bytes at offset 11363194349405083426456 of variable 'smi_infos:../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:4898.0-62' of size 16 bytes
  Callstack:
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:6589.8-33: is_new_interface
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:6034.12-25: add_smi
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:6054.4-24: try_init_dmi
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:6867.2-16: dmi_find_bmc
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:7820.21-35: init_ipmi_si
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i:7519.4-8: main

Indeed, e = (struct smi_info *)__mptr + 0xfffffffffffffda8UL;. Line 6572 is always reached from the beginnig of function is_new_interface because of the goto at line 6558. This behaviour happens in the following examples:

c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point.cil.out.i at line 6572
c/ldv-validator-v0.8/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point_ldv-val-v0.8.cil.out.i at line 6563

Furthermore, we found a null-pointer dereference in example c/ldv-validator-v0.6/linux-stable-1dfa93a-1-100_1a-drivers--usb--serial--kobil_sct.ko-entry_point.cil.out.i:

✗ Check #435:
../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-1dfa93a-1-100_1a-drivers--usb--serial--kobil_sct.ko-entry_point.cil.out.i: In function 'kobil_ioctl':
../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-1dfa93a-1-100_1a-drivers--usb--serial--kobil_sct.ko-entry_point.cil.out.i:5230.21-38: error: Invalid memory access
  
  5230:   if ((unsigned int )priv->device_type == 120U || (unsigned int )priv->device_type == 129U) {
                             ^^^^^^^^^^^^^^^^^                                                       
  pointer '&*(unsigned short *) ((signed char *) priv + 316)' may be null
  accessing 2 bytes at offset 316 of dynamically allocated block of size 0 bytes
  Callstack:
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-1dfa93a-1-100_1a-drivers--usb--serial--kobil_sct.ko-entry_point.cil.out.i:5501.6-77: kobil_ioctl
  	from ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-1dfa93a-1-100_1a-drivers--usb--serial--kobil_sct.ko-entry_point.cil.out.i:5323.4-8: main

At line 5230 priv points to a null pointer, as it is initialized to NULL at line 5227. This is because the function usb_get_serial_port_data returns the result of dev_get_drvdata, which is implemented as follows:

void *dev_get_drvdata(const struct device *arg0) {
  return ldv_malloc(0UL);
}

This problem is found in:

c/ldv-validator-v0.6/linux-stable-1dfa93a-1-100_1a-drivers--usb--serial--kobil_sct.ko-entry_point.cil.out.i at line 5230
c/ldv-validator-v0.8/linux-stable-1dfa93a-1-100_1a-drivers--usb--serial--kobil_sct.ko-entry_point_ldv-val-v0.8.cil.out.i at line 4201

We also found a problem in c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i. At line 6689 there is an index out of bounds:

✗ Check #282:
../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i: In function 'tlan_probe1':
../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:6689.2-15: error: Invalid memory access
  
  6689:   priv->pci_dev = pdev;
          ^^^^^^^^^^^^^        
  accessing 8 bytes at offset 3208 of dynamically allocated block of size 3200 bytes
  Callstack:
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:6637.8-42: tlan_probe1
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:10206.8-63: tlan_init_one
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:10307.24-10308.112: ldv_pci_instance_probe_2_17
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:9785.2-42: ldv_pci_pci_instance_2
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:9672.4-60: ldv_dispatch_register_13_2
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:10653.12-10654.60: ldv___pci_register_driver
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:6598.7-75: ldv___pci_register_driver_69
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:9654.8-20: tlan_probe
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:9907.23-88: ldv_EMGentry_init_tlan_probe_14_7
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:9935.2-34: ldv_entry_EMGentry_14
  	from ../sv-benchmarks/c/ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-ti-tlan.cil.i:9930.4-8: main

The reason is that priv points to dev + 3200, as netdev_priv is implemented as follows:

__inline static void *netdev_priv(struct net_device const *dev )
{
  {
  return ((void *)dev + 3200U);
}

But dev is assigned at line 6678 to a memory area of either 3200 bytes or a null pointer. One can see this by following the sequence of calls at lines 6678 -> 10680. The function ldv_alloc_etherdev_mqs at line 9648 returns either 3200 bytes or a null pointer. This shows that the dereference priv->pci_dev at line 6689 is always wrong.

We propose to move the five examples that always result in undefined behaviours in the respective todo directories.

Found undefined behaviour in ldv programs

Merge request reports