Suspected Unsoundness in SV-COMP SoftwareSystems

[sim642]

In my own run of Goblint on SV-COMP SoftwareSystems category, Goblint was unsound (reach_error() being unreachable: expected false, actual true) on the following benchmarks:

• ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--lustre--lustre--llite--llite_lloop.ko-entry_point.cil.out.i

[sim642]

I looked at SV-COMP 2020 results to see if any other verifier has given a violation witness for this benchmark but all of them either timed out or gave an unknown result.

Oddly, the correctness witness Goblint produces is just a single entry node. Somehow region analysis manages to break witness generation because disabling region makes the witness be outputted in whole. While it's something I need to look into, it's not the real issue because in HTML output, ldv_error is dead code either way.

[sim642]

After hunting around that benchmark I found the following:

https://github.com/sosy-lab/sv-benchmarks/blob/ac7cce1b1da7546521309eb9bb417ee994fe9439/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--lustre--lustre--llite--llite_lloop.ko-entry_point.cil.out.i#L9645-L9655:

__inline static void *kmalloc_array(size_t n , size_t size , gfp_t flags )
{
  void *tmp ;
  {
  if (size != 0UL && 0xffffffffffffffffUL / size < n) {
    return ((void *)0);
  } else {
  }
  tmp = __kmalloc(n * size, flags);
  return (tmp);
}

This gets called with n = 16, size = 4912 and according to Goblint, this always returns 0:

But with these values, the condition should actually be false. This benchmark should follow the LP64 data model and the typedefs in it say size_t is unsigned long.

The following regression test should model this issue:

// PARAM: --enable ana.int.interval --enable ana.int.def_exc
#include <assert.h>

int main() {
    // should be LP64
    unsigned long n = 16;
    unsigned long size = 4912;

    assert(!(0xffffffffffffffffUL / size < n));
}

[sim642]

Oddly enough, if the constant 0xffffffffffffffffUL is stored into a variable, which is used instead, then it works correctly.

[vogler]

analyzer/src/analyses/base.ml

Line 615 in 3164939

`Int (ID.of_int num)

Haven't tried it, but maybe we should cast constants there: Int (ID.cast_to typ (ID.of_int num)).

[michael-schwarz]

Haven't tried it, but maybe we should cast constants there: Int (ID.cast_to typ (ID.of_int num))

Would definitely not hurt.

However, I think the root cause is these issues from #98 once again.

[sim642]

Over the weekend I made a new run with 15 minute timeout on SV-COMP SoftwareSystems category (using 16 CPU cores helps) because SV-COMP preruns still haven't happened yet. This revealed unsoundness (reach_error() being unreachable: expected false, actual true) on the following benchmarks:

• ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--media--platform--timblogiw.ko-entry_point.cil.out.i (186 seconds)
• ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.i (78 seconds)

[sim642]

The former of the two is caused by our special handling of kzalloc in which the benchmark actually has the possible error call. See #123.

[sim642]

ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.i

I've now spent way too many hours trying to understand why we are wrong but haven't found anything. Most of the program is dead code according to Goblint and it seems right to me. I tried to manually find every possible way that ldv_error could end up being called and it's all functions that are never even called syntactically or happen under conditions which depend on variable values that aren't initially satisfied and there's no way they could change either.

I made some notes to myself while backtracking this program:

• 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)