sv-benchmarks unsoundness with loop unrolling

[sim642]

The unsound cases are all LDV-related, maybe you can have a look @sim642 since you looked into some similar ones as well.

• [x] c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_generic.ko-entry_point.cil.out.yml https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1405
• [x] c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_cisco.ko-entry_point.cil.out.yml https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1405
• [x] c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point.cil.out.yml https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1405
• [x] c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--mwifiex--mwifiex_sdio.ko-entry_point.cil.out.yml https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1405
• [x] c/ldv-validator-v0.6/linux-stable-431e8d4-1-102_1a-drivers--net--r8169.ko-entry_point.cil.out.yml (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1389)
• [x] c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point.cil.out.yml https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1406
• [x] c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--comedi--comedi.ko-entry_point.cil.out.yml https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1406
• [x] c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point.cil.out.yml (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1394)
• [x] c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--media--v4l2-core--videodev.ko-entry_point.cil.out.yml https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1406

At this point I am fairly convinced that the tasks are at fault, and would propose to merge this regardless (and in the worst case if we can not fix the benchmarks before keep the autotuner option for loop unrolling off for sv-comp).

Originally posted by @michael-schwarz in https://github.com/goblint/analyzer/issues/896#issuecomment-1309966941

[sim642]

c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_cisco.ko-entry_point.cil.out.i

• ldv_check_final_state() checks that ldv_set_is_empty() returns a non-zero value

• ldv_set_is_empty() is return (last_index == 0);

• last_index is a global initalized to zero

• It is modified from ldv_set_add and ldv_set_remove (which are both uncalled)

• ldv_set_add is uncalled and called

  • from ldv_skb_alloc (which is uncalled)

    • it is called from ldv_dev_alloc_skb_12 (which is uncalled)
      • which is called from cisco_keepalive_send (which is uncalled)
        • called from cisco_rx (where skb->len <= 3U is always true and the call to cisco_keepalive_send is never performed)
          • skb is a pointer to proto_group1 which is initialized to 0 in ldv_initialize_hdlc_proto_3 and never assigned any different value

  • and from ldv_netdev_alloc_skb (which is uncalled)

    • it is called from ldv_dev_alloc_skb (which is completely uncalled)

• ldv_set_remove only changes last_index if it is positive (and thus does not modify it here)

Originally posted by @michael-schwarz in https://github.com/goblint/analyzer/issues/896#issuecomment-1310160957

Same reasoning:

• c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_generic.ko-entry_point.cil.out.yml

[michael-schwarz]

• c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point.cil.out.yml

• ldv_set_add called from ldv_dev_alloc_skb_12 as above (uncalled)

  • from fr_lmi_send which is uncalled
    • called from fr_lmi_recv which is uncalled
      • called from fr_rx which checks if skb->len <= 4U
        • argument is ldvarg4
        • Pointer to freshly alloc'ed block from ldv_zalloc
    • called from fr_timer which is (statically) uncalled

[michael-schwarz]

• c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--mwifiex--mwifiex_sdio.ko-entry_point.cil.out.yml

• ldv_set_add called from ldv_dev_alloc_skb_14 as above (uncalled)

  • from mwifiex_process_int_status
    • aborts if adapter->int_status == 0
    • called from main with argument sdio_ops_group0
    • set to the result of a freshly calloced blob in ldv_initialize_mwifiex_if_ops_1

[michael-schwarz]

c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point.cil.out.yml

• reach_error is called from ldv_error

  • Called from ldv_module_put (uncalled)

    • Checks if ldv_module_refcounter > 1

  • Called from ldv_check_final_state

    • Checks if ldv_module_refcounter == 1

• ldv_module_refcounter is assigned to 1

• Incremented in:

  • ldv_module_get (statically uncalled)

  • ldv_try_module_get (uncalled)

    • called from ldv_try_module_get_44 (uncalled)

      • called from __get_policy_once (uncalled)

        • called from get_policy_once (uncalled)

          • called from get_policy (uncalled)

            • called from dm_cache_policy_create (uncalled)

              • called from create_cache_policy (uncalled)

                • called from cache_create (uncalled)

                  • called from cache_ctr if parse_cache_args(ca, (int )argc, argv, & ti->error); returns 0

                    • cache_ctr gets argc from its caller main as teh value of ldvarg16 which is set to 0

                    • parse_cache_args is passed along the argc value of 0

                      • puts argc into as.argc
                      • calls parse_metadata_dev
                        • calls at_least_one_arg with as
                          • at_least_one_arg returns 0 as as->arg is 0
                        • parse_metadata_dev returns -22

                    • parse_cache_args returns -22 and call does not happen

• Decremented in:

  • ldv_module_put (uncalled)

    • called from ldv_module_put_45 (uncalled)

      • called from put_policy (uncalled)

        • called from dm_cache_policy_create (uncalled)

          • called from create_cache_policy (uncalled) -called from cache_create (see above!)

        • called from dm_cache_policy_destroy (uncalled)

          • called from destroy (uncalled)
            • called from cache_dtr
              • called in main when ldv_state_variable_4 is not 0 or 1
                • ldv_state_variable_4 is only ever set to 0 or 1 as cache_ctr does not return 0
            • called from cache_create (see above!)
            • called from cache_ctr (after parse_cache_args that causes the early return as above)

Thus ldv_module_refcounter is never modified and the assert should hold due to always assuming argc is 0

[michael-schwarz]

c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--comedi--comedi.ko-entry_point.cil.out.yml

• reach_error is called from ldv_error

  • Called from ldv_module_put (uncalled)

    • Checks if ldv_module_refcounter > 1

  • Called from ldv_check_final_state

    • Checks if ldv_module_refcounter == 1

• ldv_module_refcounter is assigned to 1

• Incremented in:

  • ldv_module_get (statically uncalled)

  • ldv_try_module_get (uncalled)

    • called from ldv_try_module_get_7
      • called from comedi_open
        • only called if comedi_dev_get_from_minor(minor) does not return a null pointer
        • minor is computed by doing a logical and of inode->i_rdev and 1048575U. inode is comedi_fops_group1 which is allocated and set top zero in ldv_file_operations_2; Thus minor is 0
        • comedi_dev_get_from_board_minor(0) is called and the value returned
        • comedi_dev_get is called with the value of comedi_board_minor_table[0]
        • comedi_dev_get_from_minor(minor) returns a null pointer

  • comedi_board_minor_table is only assigned non-null-ptr values in comedi_alloc_board_minor (uncalled)

    • called from comedi_init

      • when i < comedi_num_legacy_minors
        • comedi_num_legacy_minors is never assigned and is constant 0
        • i is zero at this program point
          • call does not happen

    • called from comedi_auto_config (statically uncalled)

    • called from ldv_try_module_get_26 (uncalled)

      • called from comedi_device_attach (uncalled)
        • called from do_devconfig_ioctl (uncalled)
          • called from comedi_unlocked_ioctl (uncalled)
            • called from main when ldv_state_variable_2 is 2
            • is only set to 2 from a different value when comedi_open(comedi_fops_group1, comedi_fops_group2); does return 0
              • comedi_open returns -19 (see above)

    • called from ldv_try_module_get_28

      • called from comedi_device_attach (see above)

• Decremented in

  • ldv_module_put (but only if it is > 1)

Thus the issue is that comedi_board_minor_table is not properly intialized.

[michael-schwarz]

Corresponding upstream PR was merged.