symbiotic
symbiotic copied to clipboard
`argv` out-of-bound access is silently ignored
Might be related to #103.
Input:
#include <assert.h>
int main(int argc, char * argv[])
{
assert(argc == 1);
const char *ptr = argv[10]; /* error */
}
Output:
$ symbiotic --prp=memsafety argv-oob.c
8.0.0-pre-llvm-12.0.0-symbiotic:66916f64-dg:06c8ca8c-sbt-slicer:b0864a5b-sbt-instrumentation:ad1d134f-klee:10e5fae9
INFO: Looking for invalid dereferences, invalid free, memory leaks, etc.
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1
INFO: Instrumentation time: 0.05532646179199219
INFO: Optimizations time: 0.02613091468811035
INFO: Starting slicing
INFO: Total slicing time: 0.020180940628051758
INFO: Optimizations time: 0.026351213455200195
INFO: After-slicing optimizations and transformations time: 3.0517578125e-05
INFO: Starting verification
KLEE: WARNING: undefined reference to function: klee_make_nondet
No error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv-comp switch
RESULT: true
INFO: Total time elapsed: 0.5680685043334961
Yep, solving this should probably solve also #103 .
We need to:
- [ ] enable symbolic argv in
KLEE
(and other verification backends). KLEE allows only a bounded argv, so we must pick a good bound (and make sure to catch the cases where the bound is not enough to avoid incorrect answers). - [ ] check that slicer works in this scenario. I think that slicer should work well, but is imprecise with argv (https://github.com/mchalupa/dg/issues/280.)