Invalid memory access in DeviceDriversLinux64

[sosy-lab]

Invalid memory access in DeviceDriversLinux64

[mutilin]

All benchmarks in ldv-consumption directory are using parameters var_groupN which are not initialized. Why only these 3 benchmarks are causing problems?

[shaobo-he]

Hi @mutilin,

Based on my observation, it is because dereferencing some uninitialized function pointers that are reachable from these parameters results in calling functions that lead to assertion failure (let's call them buggy functions). In some benchmarks, buggy functions do not match the signature of these uninitialized function pointers while others do as those that I pointed out in my previous comment. I can show you the location where such function pointer deference happens.

[zvonimir]

@mutilin It could as well be that other benchmarks contain similar problems. It is hard to say why SMACK is not discovering these problems in other benchmarks. Maybe they are in the parts of the code that is irrelevant for a particular property being checked. Maybe SMACK times out on other benchmarks that have this problem. We can certainly not guarantee that SMACK can find all such problems.

Having said that, I think we should certainly try to fix the ones that SMACK does find, such as the ones that @Guoanshisb reported. I hope you agree with that.

Finally, if folks who submitted these benchmarks don't have time to fix them, they we can give it a try. Just let us know ASAP and we will try to propose a patch.

[mutilin]

See #227, #228, #229 for examples N1, N2, N3

[PavelAndrianov]

@Guoanshisb In the benchmark ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call.cil.out.c (the fourth one) rtl8150_probe could not be called before rtl8150_driver_init, which correctly allocates memory for rtl8150_driver_group1

[tautschnig]

@Guoanshisb With @Andrianovpavel's further comment, are all issues covered by either a pull request or that final comment? If so, this issue should be closed.

[shaobo-he]

Hi @mutilin @Andrianovpavel ,

Sorry for the late reply.

SMACK still reports bugs for these benchmarks. For example, in N1, var_group_4 is calloced, so __cil_tmp23 at line 8285 is equal to the return value of calloc + 1600. __cil_tmp24 at line 8286 is the deference of __cil_tmp23 which equals to 0 (calloced memory). __cil_tmp26 at line 8288 will be 360, which is not initialized. __cil_tmp27 at line 8289 is the deference of __cil_tmp26 which can be any value. In line 8295, a function pointer is called which is the deference of __cil_tmp27 . So a function that results in the assertion failure will be called since *__cil_tmp27 could alias with any function.

It seems that you may have to initialize the structure in a complete way.

Please let know if it makes sense.

[shaobo-he]

@Andrianovpavel With respect to the fourth benchmark, rtl8150_driver_group1 got the return value of ldv_zalloc, which can return a NULL pointer.

[PavelAndrianov]

@Guoanshisb Could you check the fix of the fourth issue?

[shaobo-he]

@Andrianovpavel I'm afraid your changes does not fix the issue. Please take a look at the error witness attached.
witness.txt

[shaobo-he]

@Andrianovpavel @mutilin May I ask what is your assumption on uninitialized function pointer dispatch?

[mutilin]

CPAchecker witness validator could not confirm the witness.txt in 90 sec.
Is there any confirmation from the other validators?

[zvonimir]

Why don't you run it without this 90 seconds time out?
This is not the competition, but rather an attempt to fix bugs in SV-COMP benchmarks, and so enforcing this time out makes no sense to me.
Also, if CPAChecker cannot find this bug in the first place, then why do you think it would be able to discharge our witness?

[mutilin]

@zvonimir, of course, CPAchecker may fail as any other tool. I just try to understand what is the confedence in correctness of the witness.
@Guoanshisb, did commenting of function pointer calls help SMACK to prove true?

[shaobo-he]

@mutilin Yes, it seems so for some benchmarks. For other benchmarks that SMACK reported a false bug, commenting out function pointers does not help. We will look into them.

[PhilippWendler]

@shaobo-he Is this fixed?

[PhilippWendler]

@shaobo-he @mutilin @Andrianovpavel Is this fixed?