Comments (3)
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
whose unknown function pointer also ends up being called
which is a bigger problem anyway.
from sv-benchmarks.
Related Issues (20)
- Tasks in seq-mthreaded wrongly marked as non-terminating HOT 2
- Task ntdrivers/floppy2 is not memory safe
- Task ntdrivers/diskperf.i.cil-1.c is not memory safe HOT 2
- ntdrivers/parport.i.cil-2 is not memory safe
- LDV tasks with undefined behaviour and/or wrong verdicts HOT 3
- cut-2 and od-1 from busy-box are not memory safe HOT 1
- Undefined behavior in two AWS benchmarks
- MemSafety - unset subproperty for false verdict
- Incorrect Verification Task
- geo1-ll.c can overflow HOT 3
- Implementation-defined behaviour HOT 3
- SV-COMP concurrency benchmarks with data races HOT 3
- "Repeated" benchmarks in pthread-wmm
- why can echo-2.i overflow? HOT 2
- Benchmarks for weak memory models HOT 3
- Reachable error in pthread-ext/41_FreeBSD_abd_kbd_sliced
- Use of `__VERIFIER_nondet_*` functions that aren't specified in SV-COMP rules HOT 1
- Info on SV-COMP 2022? HOT 2
- Repository moved to GitLab HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from sv-benchmarks.