__builtin_unreachable() in LDV benchmarks

[sim642]

The function __builtin_unreachable() is called in many LDV benchmarks: https://github.com/sosy-lab/sv-benchmarks/search?p=17&q=__builtin_unreachable. However, the function is nowhere defined or even declared.

Clearly this is supposed to be a GCC builtin: https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index-_005f_005fbuiltin_005funreachable. Unfortunately this by definition invokes undefined behavior directly:

If control flow reaches the point of the __builtin_unreachable, the program is undefined.

I suppose the most reasonable well-defined behavior for its analysis would be to assume execution doesn't continue at that point. I think it would be better to make it explicit in the programs themselves. In the spirit of what's already there, assume_abort_if_not(0); should be a good replacement.

[PhilippWendler]

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.

[sim642]

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.

[sim642]

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: https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i#L5875-L5888

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: https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i#L5821

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 https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i#L6022 whose unknown function pointer also ends up being called https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i#L6139-L6146 which is a bigger problem anyway.