Unsoundness on svcomp22 reachsafety test

[MartinWehking]

The following test becomes true but should actually be false:

• [ ] sv-benchmarks/c/ldv-validator-v0.8/linux-stable-8817633-1-144_2a-drivers--staging--media--easycap--easycap.ko-entry_point_ldv-val-v0.8.cil.out.c

I've used the following settings:

{
  "ana": {
    "sv-comp": {
      "enabled": true,
      "functions": true
    },
    "int": {
      "def_exc": true,
      "enums": false,
      "interval": true
    },
    "activated": [
      "base",
      "threadid",
      "threadflag",
      "mallocWrapper",
      "mutex",
      "mutexEvents",
      "access",
      "escape",
      "expRelation",
      "symb_locks",
      "region",
      "thread"
    ],
    "context": {
      "widen": false
    },
    "malloc": {
      "wrappers": [
        "kmalloc",
        "__kmalloc",
        "usb_alloc_urb",
        "__builtin_alloca",
        "kzalloc",

        "ldv_malloc",

        "kzalloc_node",
        "ldv_zalloc",
        "kmalloc_array",
        "kcalloc"
      ]
    },
    "base": {
      "arrays": {
        "domain": "partitioned"
      }
    }
  },
  "exp": {
    "region-offsets": true
  },
  "solver": "td3",
  "sem": {
    "unknown_function": {
      "spawn": false
    },
    "int": {
      "signed_overflow": "assume_none"
    }
  },
  "witness": {
    "id": "enumerate",
    "unknown": false
  }
}

[sim642]

In SV-COMP 2022 we timed out on this task after 960s, by the way.

[michael-schwarz]

Thank you for filing this issue, we'll look into it!

[sim642]

I believe this benchmark has UB. usb_altnum_to_altsetting mallocs some memory into alt and then reads from it without initializing anything. At ep = & (alt->endpoint + (unsigned long )j)->desc; due to the bottom in the blob, we somehow get that ep is an empty address set (which we might want to change as well), so in the following ep == 0 condition both branches end up dead (#826 would be useful for these situations). The following dead code might be the reason why we consider reach_error unreachable.

I'll make a MR to sv-benchmarks.

EDIT: sv-benchmarks MR for task exclusion: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1367.

[michael-schwarz]

Still the case with most recent version of Goblint

[sim642]

The sv-benchmarks MR for excluding this program has been merged.