Questionable verdict of ldv-validator-v0.8/linux-stable-5934df9-1-111_1a-drivers--scsi--gdth.ko-entry_point_ldv-val-v0.8.cil.out.i

[zvonimir]

So SMACK fails to find a bug in this benchmark, despite reaching a large number of unrolls. I checked the results form last year, and none of the verifiers returned a meaningful result for this benchmark (just time outs and unknowns).
Does anyone have a witness for this benchmarks that we could confirm?
Or maybe a suggestion for there the bug should be?
Otherwise, I suggest we move it into TODO folder or something like that.

[zvonimir]

@mutilin Do you maybe have any clues on this one?
It seems that these are based on real bugs, and so maybe you know where this bug is hiding. That would be helpful to determine whether it is indeed reachable. Thanks!

[zvonimir]

@tautschnig What does CBMC report on this one this year? It timed out last year, but maybe not this year.
Basically, I can't really figure out where the bug is in this benchmark. Thanks!

[PavelAndrianov]

It seems that these are based on real bugs, and so maybe you know where this bug is hiding.

@zvonimir You may use a commit identifier in the file name as a hint, where to search a bug: 5934df9.

So, the error path is supposed to be something like ... -> gdth_unlocked_ioctl -> gdth_ioctl -> ioc_general -> ldv_copy_from_user_8 (line 10921) -> ldv_check_len -> ...
Not quite sure, but seems, you may get a negative number after casting a sum of two large unsigned longs to signed long: gen.data_len + gen.sense_len. Thus, the error should be feasible.

[tautschnig]

@zvonimir Unfortunately, CBMC still times out on this benchmark. But perhaps the problem for SMACK is the absence of a non-deterministic initialiser in https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-validator-v0.8/linux-stable-5934df9-1-111_1a-drivers--scsi--gdth.ko-entry_point_ldv-val-v0.8.cil.out.i#L10888? This matters, because https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-validator-v0.8/linux-stable-5934df9-1-111_1a-drivers--scsi--gdth.ko-entry_point_ldv-val-v0.8.cil.out.i#L10904 does not actually perform any copy as _copy_from_user does not actually touch the target memory.