ntdriver benchmarks are not memory safe

[mchalupa]

Hi,

I was just going through this ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c benchmark again (#290) and found out that it is still not memory safe at all. There is a bunch of places where an invalid memory dereference can occur.

1. here is an out-of-bound access https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c#L1681
2. here the DriverExtension is not allocated https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c#L1688 (actually, it is usage of uninitialized automatic value)
3. here the DeviceExtension is not allocated https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c#L1709
4. here (and on many other places) a uninitialized pointer is loaded https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c#L1744 and dereferenced later (e.g. https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c#L1746)

The question is what to do with it? Should I try fix all these errors or should we drop the benchmark (we already have the false-valid-deref version)?

Thanks, Marek

[dbeyer]

Fixing would be great, and unfold, i.e., one true-valid-memsafety, and one _false for each of the cases above would be awesome.

[mchalupa]

Exactly the same issues (and some more), can be found in these benchmarks:

• https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/diskperf_true-unreach-call_true-valid-memsafety.i.cil.c
• https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/floppy2_true-unreach-call_true-valid-memsafety.i.cil.c
• https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/parport_false-unreach-call_true-valid-memsafety.i.cil.c.

I tried to fix them, but I haven't succeeded. And I'm not sure if I'm not changing the semantics of the benchmarks in the first place. I guess the memory bugs in ntdriver benchmarks should be fixed the same way as in the DeviceDriver64 benchmarks (@mutilin suggested this https://github.com/sosy-lab/sv-benchmarks/issues/230#issuecomment-263296566), since they are of the same essence.

EDIT: added links to other files from ntdrivers. All of the ntdriver benchmarks that I checked contain these invalid dereferences (even the simplified versions).

EDIT 2: removed the claim that some of the invalid dereferences are also in the simplified versions in ntdrivers-simplified. I checked it again and I probably have mistaken the files with some of the non-simplified (I should give myself some limit on the number of opened files at once :)

[mikhailramalho]

Any progress on this?

We just found some property violation in the following benchmarks:

ntdrivers/diskperf_true-unreach-call_true-valid-memsafety.i.cil.c              false(valid-deref)
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c                false(valid-deref)
ntdrivers/parport_true-unreach-call_true-valid-memsafety.i.cil.c               false(valid-deref)

[zvonimir]

We find bugs in all of these

ntdrivers/diskperf_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref)
ntdrivers/diskperf_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref)
ntdrivers/floppy2_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref)
ntdrivers/floppy_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-memtrack)
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-memtrack)
ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref)
ntdrivers/parport_false-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref)
ntdrivers/parport_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref)

I am having trouble keeping track of all pull requests and all issues, but benchmarks above are likely mislabeled.

[mikhailramalho]

Should we remove them from this year's competition? @dbeyer suggested:

Non-fixable programs are to be moved to a directory -todo.

I believe these qualify to be removed.

[zvonimir]

Wait, why shouldn't we just change the labels? It is not like we have to fix them so that they don't contain bugs. We just have to update their labels. No?

[mikhailramalho]

I was actually taking under consideration that two tools (we and @versokova) reported memory leak in ntdrivers/cdaudio_false-unreach-call_true-valid-memsafety.i.cil.c, which @mchalupa reported another memory violation (deref).

My assumption is that all benchmarks in this category have at least two memory violations (leak and deref), that's why I suggested remove them.

[zvonimir]

Ah, got it. Sure, in that case I don't think it is feasible we fix them before the deadline. These are I think very tricky to fix. So I am fine if we remove them.

[dbeyer]

Is the conclusion that these should be fixed later? So I added milestone SV-COMP 2018.