Fix handling of labels in unrolling & add possibility to run CIL checks on CFGs

[michael-schwarz]

Our handling of labels when unrolling loops was still slightly off:

• We did not populate the labelAlphaTable, so there were collisions possible with labels defined outside the loop that is being unrolled, as we started from a fresh alpha table.
• We were excessively copying statements (not leaving the original statement in the CFG as well (at the very end), causing gotos from outside the CFG to point to statements that were not included in the current CFG anymore.

To catch such issues early from now on, I added the option dbg.run_cil_check that causes CIL integrity checks to run and enabled them for our loop unrolling tests.

TODO:

• Wait for merge of Expose populateLabelAlphaTable cil#121 and update pins

Closes #895

[michael-schwarz]

It has an overwhelmingly positive impact if we do this and enable the loop autotuning. The instances in which we are unsound remain to be investigated, they may already be fixed upstream in SV-Comp.

For overflows, we succeed with an additional 14 tasks, for no-data-race it makes no difference.

[sim642]

The instances in which we are unsound remain to be investigated, they may already be fixed upstream in SV-Comp.

Do you have a list of these new unsound cases? Would be good to look into at least some of them to determine what's at fault and whether we will be able to do something about them any more after the tasks are frozen.

The improvement is nice, but an additional 66 points won't move us up in the category rankings, but any unsound case will compromise our 1st place in the correctness ranking, which is not worth giving up.

[michael-schwarz]

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

• 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
• 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
• 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
• 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
• 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)
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point.cil.out.yml
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--comedi--comedi.ko-entry_point.cil.out.yml
• 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)
• 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

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

[michael-schwarz]

Would be good to look into at least some of them to determine what's at fault and whether we will be able to do something about them any more after the tasks are frozen.

Iirc, if we find UB, we can still move to exclude those tasks, right?

[sim642]

I looked up if any of those have been modified/have open MRs in sv-benchmarks and added links for those.

It is possible to exclude tasks after freezing by proposing changes, but getting those merged is more difficult since "pull requests after deadline only merged after jury approval".
But either way, since loop unrolling is currently disabled, we can keep it disabled until all of those tasks have been handled.

[michael-schwarz]

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)

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

[sim642]

I opened a new issue about these unsound cases to not block this PR.