search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

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 #1245

Open zvonimir opened 3 years ago

zvonimir commented 3 years ago

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 commented 3 years ago

@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 commented 3 years ago

@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 commented 3 years ago

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 commented 3 years ago

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