Change verdict for 'adutux' module

[mutilin]

Verdict false was incorrect, because it was obtained on the old environment model where kzalloc was not modeled with calloc. The correct verdict is true

[dbeyer]

Thanks for the correction by the contributor of the verification tasks.

[zvonimir]

SMACK actually reports a bug for ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--misc--adutux despite properly modeling calloc. So this should not be merged just like that. How should we proceed?

[dbeyer]

Thanks for letting us know. Let's discuss before merging.

[dbeyer]

@zvonimir Can you please put in a review with "changes required"?
This way you have the control over when it is ready to be merged.

[zvonimir]

I am not sure why this label should be changed. It seems that several tools do report a bug on this benchmark. I think I am reading this right:
https://www.sosy-lab.org/research/witness-based-debugging/inspect.php?programSHA=87f2d6c2dad7df4170b8a425e697c69fd1a57a2e&programName=..%2Fsv-benchmarks%2Fc%2Fldv-linux-4.0-rc1-mav%2Flinux-4.0-rc1---drivers--usb--misc--adutux.ko_false-unreach-call.cil.c&witnessSHA=25f4cee875d44871d0e2b41c20e1c42af92f4951&witnessName=..%2Fresults-verified%2Fsmack.2016-12-25_1714.logfiles%2Fsv-comp17.linux-4.0-rc1---drivers--usb--misc--adutux.ko_false-unreach-call.cil.c.files%2Fwitness.graphml

[mutilin]

Thanks @zvonimir, @dbeyer,
Yes, we have to investigate the case before merging.
By the way, do we have any tools for inspecting witnesses manually?

[zvonimir]

We (team SMACK) unfortunately don't have any fancy tools (yet :)) for inspecting our witnesses, and so we do it manually using out txt error trace output (not witness automata). Others maybe have better tools, not sure about that.

[mutilin]

First of all, I want to note that the page with list of witnesses is misleading, because it does not tell correctness witnesses from violation witnesses. To find violation witnesses you have to open each witness and look to witness-type key. Dirk (@dbeyer), is it possible to separate witnesses by type?

Anyway the information was very helpful. I have inspected SMACK 1.7.1 witness. It looks like many steps are missing in the witness, but I was able to understand it.

First of all, adu_open is called which checks that device is not null and plugged in.
see line 4945:
if ((unsigned long )dev == (unsigned long )((struct adu_device *)0) || (unsigned long )dev->udev == (unsigned long )((struct usb_device *)0)) {
I assume that this check is passed, because witness contains an edge
<edge source="A58" target="A59"><data key="assumption">tmp == 0;</data><data key="startline">6763</data><data key="assumption.scope">ldv_file_operations_instance_probe_0_12</data></edge>

which means that adu_open returns 0
6763: tmp = adu_open(arg1, arg2);

The device is stored in parameter file which equals to ldv_0_resource_file from ldv_file_operations_file_operations_instance_0
4976: file->private_data = (void *)dev;

After that the witness contains a call to adu_release where dev is extrated from the parameter file which equals to ldv_0_resource_file from ldv_file_operations_file_operations_instance_0 (the same as in adu_open)

The function adu_delete which deallocates resources and causes violation is called only if the device was unplugged, i.e. dev->udev becomes zero (lines 5086-5089).

  if ((unsigned long )dev->udev == (unsigned long )((struct usb_device *)0)) {
    if (dev->open_count == 0) {
      {
      adu_delete(dev);

As I can see nobody unplugged the device, which can be done by adu_disconnect.
So adu_delete should not be called, and the VERIFIER_error should not be reachable.

[mutilin]

The Travis CI has failed, but it seems that it should be just restarted

apt-get install failed


The command "sudo -E apt-get -yq --no-install-suggests --no-install-recommends --force-yes install libc6-dev-i386 gcc-5 clang-3.8 python-yaml libwww-perl g++-5 bison flex" failed and exited with 100 during .

[dbeyer]

@mutilin Thanks for your suggested improvement to the witness table.
I added a column that shows the witness type.

[dbeyer]

@zvonimir The explanation by @mutilin sounds reasonable to me. Would you be willing to let this PR go through?

[zvonimir]

Usually what happens in device driver benchmarks is that there is a write to unallocated memory somewhere, that can then overwrite anything, causing a a bug to be reachable. Please give us until Monday night to study this problem in more detail.
@Guoanshisb : please take a look at our error trace for this benchmark and see if you can figure out why it is happening.

[shaobo-he]

@mutilin @zvonimir @dbeyer

I did some study on this benchmark and here is what I found:

First of all, dev in adu_open got its value from usb_get_intfdata(interface), which is an arbitrary pointer since interface is the return value of an external function without a body.

Then in line 4980, function usb_fill_int_urb is called with dev->interrupt_in_urb as its first argument urb. There is a write to unallocated memory happening in line 4613 (urb->interval = 1 << (interval + -1);) inside usb_fill_int_urb.

Since usb->interval is (should be) treated as a pointer of arbitrary value, it can alias with &file->private_data. Therefore, pointer dev in function adu_delete can be of any value and so is dev->udev.

Please let me know if it makes sense. I think we should not change the label of this benchmark to true unless unallocated memory accesses are fixed.

[mutilin]

Of course, in Linux usb_find_interface could not return pointer where usb->interval is aliased with file->private_data (See implementation). That is why we need assumptions on pointers for undefined functions introduced by RAM (or on-demand memory) in #230.
As a workaround we may allocate memory for interface and interface->dev->driver_data.
@Guoanshisb, would you be able to prepare a pull request for it?

[tautschnig]

@mutilin If you want this pull request to go through, you might have to include the fix for the benchmark that you are requesting in this pull request.

[shaobo-he]

Hi @mutilin, I have spent some time to try to fix this benchmark. However, it is not easy as I thought it to be because of nested structure objects. So I was wondering if it is possible to keep the current label and relabel it once we adopt a systematic way to deal with such issue (e.g., RAM proposed in #230).

[dbeyer]

If the verification task does not correctly implement the submitter's intention, and
a fix is not possible, then the program should be moved to the -todo folder.

[mutilin]

@dbeyer, I have moved benchmark into -todo directory.
@tautschnig, I could not solve all the memory issues in the benchmark, because every undefined function causes such problems. That is why tool developers may suggest a workaround fixing problems on the way to error.

[dbeyer]

@zvonimir Please unblock.