Comments (3)
Here are witnesses for memsafety violation for 181 of these benchmarks that I was able to confirm with CPAchecker: https://www.fi.muni.cz/~xchalup4/sv-comp/1270_witnesses_memsafety/
from sv-benchmarks.
Surprisingly most of the provided witnesses are quite short.
CPAchecker can also be executed to directly verify those files:
scripts/cpa.sh -smg -spec test/programs/benchmarks/properties/valid-memsafety.prp -64 SOURCEFILE
As CPAchecker might in theory overapproximate the state space and sometimes reports false alarms,
a detailed investigation for those files is required.
I took a look at ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--acpi--apei--einj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
.
There seems to be an invalid pointer dereference in line 4394.
The minified counterexample trace is as follows:
static struct acpi_table_einj *einj_tab = 0; CALL main() int tmp___7; ldv_initialize(); // does nothing tmp___7 = einj_init_2(); CALL einj_init() __cil_tmp10 = (acpi_string )"EINJ"; __cil_tmp11 = 0U; __cil_tmp12 = (struct acpi_table_header **)(&einj_tab); status = acpi_get_table(__cil_tmp10, __cil_tmp11, __cil_tmp12); // does nothing? __cil_tmp13 = &einj_tab; __cil_tmp14 = *__cil_tmp13; rc = einj_check_table_4(__cil_tmp14); CALL einj_check_table(struct acpi_table_einj *einj_tab___0) __cil_tmp3 = (unsigned long)einj_tab___0; __cil_tmp4 = __cil_tmp3 + 36; __cil_tmp5 = *((u32 *)__cil_tmp4); // dereference of pointer
Can someone confirm this? Maybe I have overlooked something.
Should the method acpi_get_table
initialize the table somehow?
from sv-benchmarks.
@kfriedberger I'm not as surprised that you are finding counterexamples to be short - the issues will really just be a lack of necessary initialisation, often resulting in an invalid pointer dereference as soon as such a pointer dereference occurs.
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
- 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
- __builtin_unreachable() in LDV benchmarks HOT 3
- 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.