staticafi
Checking more properties at once
Hi,
Symbiotic now checks only property specified by the last --prp option or only assertions if this option is omitted. Would it be possible to modify Symbiotic so that it can check more properties and assertion violations in one run?
Thanks!
#include <assert.h>
int main(void)
{
char arr[1];
arr[1] = 0;
assert(0);
}
Run A - only invalid deref:
$ symbiotic --prp=memsafety assert-bounds.c
7.0.0-dev-llvm-9.0.1-symbiotic:d26ef236-dg:e89761ff-sbt-slicer:fff6245c-sbt-instrumentation:2f9
be629-klee:59f3e288
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1
INFO: Instrumentation time: 0.047057390213012695
INFO: Optimizations time: 0.02576899528503418
INFO: Starting slicing
INFO: Total slicing time: 0.011444807052612305
INFO: Optimizations time: 0.02638983726501465
INFO: After-slicing optimizations and transformations time: 3.600120544433594e-05
INFO: Starting verification
b'KLEE: WARNING: undefined reference to function: klee_make_nondet'
b'KLEE: ERROR: /home/lukas/tmp/assert-bounds.c:8: memory error: out of bound pointer'
b'KLEE: NOTE: now ignoring this error at this location'
INFO: Verification time: 0.041364192962646484
--- Error trace ---
Error: memory error: out of bound pointer
File: /home/lukas/tmp/assert-bounds.c
Line: 8
assembly.ll line: 16
Stack:
#000000016 in main () at /home/lukas/tmp/assert-bounds.c:8
Info:
address: 19:18172161
pointing to: object at 18172160 of size 1
MO8[1] allocated at main(): %1 = alloca [1 x i8], align 1
--- Sequence of non-deterministic values [function:file:line:col] ---
--- ----------- ---
Error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv
-comp switch
RESULT: false(valid-deref)
INFO: Total time elapsed: 0.5920290946960449
Run B - only assert(0) (no prp specified):
$ symbiotic assert-bounds.c
7.0.0-dev-llvm-9.0.1-symbiotic:d26ef236-dg:e89761ff-sbt-slicer:fff6245c-sbt-instrumentation:2f9be629-klee:59f3e288
INFO: Optimizations time: 0.023056507110595703
INFO: Starting slicing
INFO: Total slicing time: 0.0052034854888916016
INFO: Optimizations time: 0.023514270782470703
INFO: After-slicing optimizations and transformations time: 1.8358230590820312e-05
INFO: Starting verification
b'KLEE: ERROR: /home/lukas/tmp/assert-bounds.c:9: ASSERTION FAIL: 0'
b'KLEE: NOTE: now ignoring this error at this location'
INFO: Verification time: 0.04207634925842285
--- Error trace ---
Error: ASSERTION FAIL: 0
File: /home/lukas/tmp/assert-bounds.c
Line: 9
assembly.ll line: 12
Stack:
#000000012 in main () at /home/lukas/tmp/assert-bounds.c:9
--- Sequence of non-deterministic values [function:file:line:col] ---
--- ----------- ---
Error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv-comp switch
RESULT: false(unreach-call)
INFO: Total time elapsed: 0.4455740451812744
Hi, It would be possible and it is one of our long-term goals, but the change is not trivial (but should not be that hard either).
Btw. in the example program, I would actually expect Symbiotic to behave like it does right now since the program contains only one execution path that is terminated by the invalid dereference (which is sliced away when we look only for assertions). I guess that you would like to have something like:
1 #include <assert.h>
2
3 int main(void)
4 {
5 char arr[1];
6 if (*) {
7 arr[1] = 0;
8 }
9 assert(0);
10 }
With the result like:
file.c: 7: invalid pointer dereference
file.c: 9: assertion violation: assert(0);
Which does not work right now.
