__builtin_unreachable() in LDV benchmarks about sv-benchmarks HOT 3 OPEN

Is this actually reachable in the code? If not, there is no problem, right?

I had a look at a few calls of those calls, and all where cases where in the original Linux code the macro BUG_ON was used. So if any calls are reachable, this would be worth investigating as it could highlight a bug in Linux. And actually the BUG_ON macro ensures (via assembly code) that the code to __builtin_unreachable is unreachable.

from sv-benchmarks.

It might very well be true that all such locations are unreachable, but as is, nothing about the benchmarks is requiring a verifier to prove that they are actually unreachable. Interpreting abstractly, such location might be reachable, but since it's not necessarily a violation of the reachability property being checked, it's not an abstract counterexample that needs to be refined. Rather, one might just want to soundly and abstractly interpret it. On the other hand, if the checked property were proving the lack of undefined behavior, it would require a verifier to prove unreachability.

To ensure that all these locations are unreachable, one would have to construct alternate version of these benchmarks where __builtin_unreachable have been replaced with reach_error (and original error locations/assertions removed) and verify them for unreachability. And then it still would make sense for the original benchmarks to not invoke __builtin_unreachable because the validity of doing that depends on the verification result of the alternate program. Replacing them would decouple the two programs.

from sv-benchmarks.

Actually in ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i seems reachable as well, although likely only due to LDV modelling. There __builtin_unreachable is reachable (at least when inline ASM isn't to be analyzed) in the following snippet:

The discriminating value pv_irq_ops.save_fl.func may very well be NULL since the pv_irq_ops struct is extern and nowhere written to:

Arguably the problem in this benchmark might be the extern, but at least there's a clear sound way to handle that: possibly read any value, including NULL.

Ok, there's another extern struct

from sv-benchmarks.