search

marek-trtik / cbmc

C Bounded Model Checker
http://www.cprover.org/cbmc
Other
0 stars 0 forks source link

Incorrect FALSE detected in function strcpy (module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i) #36

Open lucasccordeiro opened 6 years ago

lucasccordeiro commented 6 years ago

./cbmc --graphml-witness witness.graphml --64 --propertyfile ../../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i

Violated property:
  file <builtin-library-strcpy> line 23 function strcpy
  strcpy src/dst overlap
  POINTER_OBJECT(dst) != POINTER_OBJECT(src) || (unsigned long int)POINTER_OFFSET(src) + n < (unsigned long int)POINTER_OFFSET(dst) || (unsigned long int)POINTER_OFFSET(dst) + n < (unsigned long int)POINTER_OFFSET(src)

VERIFICATION FAILED
EC=10
FALSE
marek-trtik commented 6 years ago 
State 72 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6800 function main thread 0
----------------------------------------------------
  var_set_param_timeout_0_p0=((char *)0) + 1l (0000000000000000000000000000000000000000000000000000000000000001)

State 73 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6801 function main thread 0
----------------------------------------------------
  var_set_param_timeout_0_p1=((struct kernel_param *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 74 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6802 function main thread 0
----------------------------------------------------
  var_set_param_wdog_ifnum_3_p0=((char *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 75 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6803 function main thread 0
----------------------------------------------------
  var_set_param_wdog_ifnum_3_p1=((struct kernel_param *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 76 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6804 function main thread 0
----------------------------------------------------
  var_set_param_str_1_p0=valcp!0@35 (1101001100100000000000000000000000000000000000000000000000000000)

State 77 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6805 function main thread 0
----------------------------------------------------
  var_set_param_str_1_p1=((struct kernel_param *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 78 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6806 function main thread 0
----------------------------------------------------
  var_get_param_str_2_p0=((char *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 79 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6807 function main thread 0
----------------------------------------------------
  var_get_param_str_2_p1=((struct kernel_param *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 80 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6808 function main thread 0
----------------------------------------------------
  var_group1=((struct ipmi_smi_msg *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 81 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6809 function main thread 0
----------------------------------------------------
  var_group2=((struct ipmi_recv_msg *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 82 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6810 function main thread 0
----------------------------------------------------
  var_group3=((struct file *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 83 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6811 function main thread 0
----------------------------------------------------
  var_ipmi_read_18_p1=((char *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 84 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6812 function main thread 0
----------------------------------------------------
  var_ipmi_read_18_p2=9223372036854775808ul (1000000000000000000000000000000000000000000000000000000000000000)

State 85 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6813 function main thread 0
----------------------------------------------------
  var_ipmi_read_18_p3=((signed long int *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 86 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6814 function main thread 0
----------------------------------------------------
  res_ipmi_read_18=1l (0000000000000000000000000000000000000000000000000000000000000001)

State 87 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6815 function main thread 0
----------------------------------------------------
  var_ipmi_poll_20_p1=data!0@452 (1000000000000000000000000000000000000000000000000000000000000000)

State 88 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6816 function main thread 0
----------------------------------------------------
  var_ipmi_write_17_p1=((char *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 89 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6817 function main thread 0
----------------------------------------------------
  var_ipmi_write_17_p2=1ul (0000000000000000000000000000000000000000000000000000000000000001)

State 90 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6818 function main thread 0
----------------------------------------------------
  var_ipmi_write_17_p3=((signed long int *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 91 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6819 function main thread 0
----------------------------------------------------
  res_ipmi_write_17=0l (0000000000000000000000000000000000000000000000000000000000000000)

State 92 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6820 function main thread 0
----------------------------------------------------
  var_ipmi_unlocked_ioctl_16_p1=2147768068u (10000000000001000101011100000100)

State 93 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6821 function main thread 0
----------------------------------------------------
  var_ipmi_unlocked_ioctl_16_p2=0ul (0000000000000000000000000000000000000000000000000000000000000000)

State 94 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6822 function main thread 0
----------------------------------------------------
  var_group4=((struct inode *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 95 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6823 function main thread 0
----------------------------------------------------
  res_ipmi_open_19=2147353061 (01111111111111100000000111100101)

State 96 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6824 function main thread 0
----------------------------------------------------
  var_ipmi_fasync_21_p0=0 (00000000000000000000000000000000)

State 97 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6825 function main thread 0
----------------------------------------------------
  var_ipmi_fasync_21_p2=0 (00000000000000000000000000000000)

State 98 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6826 function main thread 0
----------------------------------------------------
  var_ipmi_wdog_msg_handler_23_p1=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 99 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6827 function main thread 0
----------------------------------------------------
  var_ipmi_wdog_pretimeout_handler_24_p0=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 100 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6828 function main thread 0
----------------------------------------------------
  var_group5=((struct notifier_block *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 101 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6829 function main thread 0
----------------------------------------------------
  var_ipmi_nmi_27_p1=9223372036854775820ul (1000000000000000000000000000000000000000000000000000000000001100)

State 102 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6830 function main thread 0
----------------------------------------------------
  var_ipmi_nmi_27_p2=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 103 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6831 function main thread 0
----------------------------------------------------
  var_wdog_reboot_handler_28_p1=0ul (0000000000000000000000000000000000000000000000000000000000000000)

State 104 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6832 function main thread 0
----------------------------------------------------
  var_wdog_reboot_handler_28_p2=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 105 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6833 function main thread 0
----------------------------------------------------
  var_wdog_panic_handler_29_p1=0ul (0000000000000000000000000000000000000000000000000000000000000000)

State 106 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6834 function main thread 0
----------------------------------------------------
  var_wdog_panic_handler_29_p2=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 107 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6835 function main thread 0
----------------------------------------------------
  var_ipmi_new_smi_30_p0=0 (00000000000000000000000000000000)

State 108 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6836 function main thread 0
----------------------------------------------------
  var_group6=((struct device *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 109 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6837 function main thread 0
----------------------------------------------------
  var_ipmi_smi_gone_31_p0=0 (00000000000000000000000000000000)

State 110 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6838 function main thread 0
----------------------------------------------------
  ldv_s_ipmi_wdog_fops_file_operations=0 (00000000000000000000000000000000)

State 111 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6839 function main thread 0
----------------------------------------------------
  tmp=0 (00000000000000000000000000000000)

State 112 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6840 function main thread 0
----------------------------------------------------
  tmp___0=17 (00000000000000000000000000010001)

State 113 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6841 function main thread 0
----------------------------------------------------
  tmp___1=0 (00000000000000000000000000000000)

State 114 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6845 function main thread 0
----------------------------------------------------
  ldv_s_ipmi_wdog_fops_file_operations=0 (00000000000000000000000000000000)

State 115 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6846 function main thread 0
----------------------------------------------------
  LDV_IN_INTERRUPT=1 (00000000000000000000000000000001)

State 121 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6704 function ipmi_wdog_init thread 0
----------------------------------------------------
  rv=0 (00000000000000000000000000000000)

State 122 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6705 function ipmi_wdog_init thread 0
----------------------------------------------------
  tmp=0 (00000000000000000000000000000000)

State 123 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6706 function ipmi_wdog_init thread 0
----------------------------------------------------
  tmp___0=0 (00000000000000000000000000000000)

State 124 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6707 function ipmi_wdog_init thread 0
----------------------------------------------------
  tmp___1=0 (00000000000000000000000000000000)

State 127 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6711 function ipmi_wdog_init thread 0
----------------------------------------------------
  inval=action (0000010101000000000000000000000000000000000000000000000000000000)

State 128 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6711 function ipmi_wdog_init thread 0
----------------------------------------------------
  outval=((char *)0) (0000000000000000000000000000000000000000000000000000000000000000)

State 129 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6497 function action_op thread 0
----------------------------------------------------
  tmp=0 (00000000000000000000000000000000)

State 130 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6498 function action_op thread 0
----------------------------------------------------
  tmp___0=0 (00000000000000000000000000000000)

State 131 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6499 function action_op thread 0
----------------------------------------------------
  tmp___1=0 (00000000000000000000000000000000)

State 132 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6500 function action_op thread 0
----------------------------------------------------
  tmp___2=0 (00000000000000000000000000000000)

State 137 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6516 function action_op thread 0
----------------------------------------------------
  s1=action (0000010101000000000000000000000000000000000000000000000000000000)

State 138 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6516 function action_op thread 0
----------------------------------------------------
  s2="reset" (0000010101100000000000000000000000000000000000000000000000000000)

State 176 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6516 function action_op thread 0
----------------------------------------------------
  tmp___2=0 (00000000000000000000000000000000)

State 178 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6519 function action_op thread 0
----------------------------------------------------
  action_val=1 (00000001)

State 182 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6545 function action_op thread 0
----------------------------------------------------
  dst=action (0000010101000000000000000000000000000000000000000000000000000000)

State 183 file ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i line 6545 function action_op thread 0
----------------------------------------------------
  src=action (0000010101000000000000000000000000000000000000000000000000000000)

Violated property:
  file <builtin-library-strcpy> line 23 function strcpy
  strcpy src/dst overlap
  POINTER_OBJECT(dst) != POINTER_OBJECT(src) || (unsigned long int)POINTER_OFFSET(src) + n < (unsigned long int)POINTER_OFFSET(dst) || (unsigned long int)POINTER_OFFSET(dst) + n < (unsigned long int)POINTER_OFFSET(src)

VERIFICATION FAILED
EC=10
FALSE
marek-trtik commented 6 years ago

Each execution trace (starting in the main function) reaches the line 6847 where is called a function ldv_initialize. Two things apply here:

  1. The function ldv_initialize is only declared external in the benchmark, it is not defined.

  2. There is no assumption about calling undefined function in rules of SV-COMP (https://sv-comp.sosy-lab.org/2018/rules.php).

    So, the function pointer ldv_initialize is udefined and the call ldv_initialize() at line 6847 leads to an undefined behaviour.

tautschnig commented 6 years ago

Yes, there is a problem of undefined functions, but that would imply we would have to get rid of all LDV benchmarks on the spot. If ldv_initialize were assumed to be a just a trivial function doing nothing, would there still be undefined behaviour? (The trace suggests such.)

marek-trtik commented 6 years ago

Another way how to prove the presence of undefined behaviour in the benchmark (assuming ldv_initialize is defined as identity) is to follow the error trace generated by CBMC above. Let me point out the key information of the trace:

  1. In the main function at line 6848 is called the function ipmi_wdog_init.
  2. In function ipmi_wdog_init at line 6711 we call the function action_op. Important is that the first argument is the pointer to the global array action. This array was initialsed (before entering main) to the string reset. The second argument is NULL pointer.
  3. When entering the function action_op the fist parameter inval points to the global array action and the second parameter outval is NULL.
  4. The execution takes the else branch at line 6503.
  5. The execution takes the else branch at line 6510.
  6. The result from the call to strcmp at line 6516 returns 0, because it compares the string pointed to be inval (i.e. the string reset in action global variable) with the string constant reset.
  7. The execution takes the true branch at line 6518.
  8. At line 6545 there is called function strcpy with address of action global array with inval pointer which contains address of the same array action. Therefore, we reach an undefined behaviour.
tautschnig commented 6 years ago

Thank you very much for this analysis! Can you please copy the above description into an issue at sosy-labs/sv-benchmarks?

lucasccordeiro commented 6 years ago

We have just created the issue in https://github.com/sosy-lab/sv-benchmarks/issues/551.