Unreach-call verdict of ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml

[sim642]

In our own testing Goblint gave the result true for ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml but its expected verdict is false. Obviously we want to fix our unsoundness so I've been desperately trying to understand this program and how it can reach the error. Unfortunately I haven't been successful so I'm asking about it here to avoid going truly insane: is there really a violation or could the expected verdict be itself wrong?

Below are a few things which have made me suspect the latter.

Previous SV-COMPs

I looked through the results of previous SV-COMPs which included this benchmark and I couldn't find any tool to have solved this correctly, so no violation witness to inspect either. There were only two cases ever where a tool gave a non-timeout non-error result:

• SymDIVINE in SV-COMP 2017 with true, no (useful) witness;
• SeaHorn-F16 in SV-COMP 2016 with true, no (useful) witness.

Goblint's result

Goblint's true output also comes with a correctness witness witness.txt (renamed to .txt for GitHub). Unfortunately I haven't been able to validate it. I tried both CPAchecker and Ultimate (without time limit and 20GB of memory) and both eventually ran out of that memory.

What Goblint's own output says more directly is that supposedly large parts of this program are dead code.

Manual analysis

Finally I turned myself into a verifier in order to try to understand the program and its supposed violation. Working backwards from error locations I managed to convince myself of the same thing: all the ways I could see for reaching the error are dead code due to how some state variables are initialized and manipulated.

For reference, below is a rough dump of my internal state that lead me to that conclusion.

My manual backwards analysis notes

• reach_error called by:

  • ldv_error called by:
    • ldv_module_put called by:
      • ldv_module_put_11 called by:
        • dvb_device_open if dvbdev from dvb_minors is not NULL (dead, see below)
      • ldv_module_put_81 called by:
        • dvb_ca_en50221_io_open (dead, see below)
      • ldv_module_put_82 called by:
        • dvb_ca_en50221_io_release (dead, see below)
      • ldv_module_put_118 called by:
        • dvb_net_do_ioctl (dead, see below)
      • ldv_module_put_119 called by:
        • dvb_net_do_ioctl (dead, see below)
      • ldv_module_put_121 called by:
        • dvb_net_do_ioctl (dead, see below)
      • ldv_module_put_and_exit (dead)
    • ldv_check_final_state if ldv_module_refcounter is not 1 (dead, see below), called by:
      • main (end)

• dvb_minors written by:

  • zero initialized
  • dvb_register_device called by:
    • dvb_dmxdev_init (dead)
    • dvb_ca_en50221_init (dead)
    • dvb_register_frontend (dead)
    • dvb_net_init (dead)
  • dvb_unregister_device to zero (dead, irrelevant)

• ldv_module_refcounter written by:

  • initialized to 1
  • ldv_module_get (dead)
  • ldv_try_module_get called by:
    • ldv_try_module_get_10 called by:
      • dvb_device_open if dvbdev from dvb_minors is not NULL (dead, see above)
    • ldv_try_module_get_80 called by:
      • dvb_ca_en50221_io_open (dead, see below)
    • ldv_try_module_get_117 called by:
      • dvb_net_do_ioctl (dead, see below)
    • ldv_try_module_get_120 called by:
      • dvb_net_do_ioctl (dead, see below)
  • ldv_module_put (dead, see above)

• dvb_ca_en50221_io_open called by:

  • main if ldv_state_variable_8 is 1 (dead)
  • pointer in dvb_ca_fops
    • pointer in dvbdev_ca
      • used in dvb_ca_en50221_init (dead)

• dvb_ca_en50221_io_release called by:

  • ldv_main_exported_8 if ldv_state_variable_8 is 2 (dead), called by:
    • main if ldv_state_variable_8 is not 0 (dead)
  • pointer in dvb_ca_fops
    • pointer in dvbdev_ca
      • used in dvb_ca_en50221_init (dead)

• ldv_state_variable_8 written by:

  • main (begin), initialized to 0
  • ldv_main_exported_8 called by:
    • main if ldv_state_variable_8 is not 0 (dead)

• dvb_net_do_ioctl called by:

  • dvb_net_ioctl via dvb_usercopy, called by:
    • ldv_main_exported_4 if ldv_state_variable_4 is 2 (dead), called by:
      • main if ldv_state_variable_4 is not 0 (dead)

• ldv_state_variable_4 written by:

  • main (begin), initialized to 0
  • ldv_main_exported_4 called by:
    • main if ldv_state_variable_4 is not 0 (dead)

[PhilippWendler]

@mutilin?

[mutilin]

@sim642 Simmo, the intention of the benchmark was to demonstrate a violation of Module get/put rule. In this example there is a mismatch between try_module_get expanded from fops_get and module_put from fops_replace in dvb_device_open.

As you correctly wrote, current example misses some initialization of dvb_minors, which should be done by dvb_register_device from dvb_dmxdev_init. Alternatively, it may be initialized by arbitrary values.

[sim642]

@mutilin Since you know the structure of these benchmarks better than I do, could you open a PR to put the missing initialization to some appropriate place which would restore the original intent of the benchmark?

I assume that would be preferable to changing the expected verdict to true, which would match the existing benchmark code but misses the original intent.

[mutilin]

I think it is better to move it to some TODO directory or remove, because now I do not have time to fix it.