symbiotic
symbiotic copied to clipboard
More descriptive error traces
I've following suggestions for rewording of current error traces emitted by klee
.
- All error traces that contain info about the origin of the allocated memory are only pointing to the executed LLVM IR:
It would be definitely useful to extend this with location info pointing to the original sources as well.Info: address: 82:0 pointing to: object at Segment: [82] of size 16 MO71[16] allocated at main(): %9 = call noalias i8* @malloc(i64 16) #3, !dbg !18
-
free
ing stack memory is reported asfree of alloca
which suggests that the memory was explicitly allocated byalloca(3)
which is generally not true. I suggest something likememory error: free of address on stack
if thealloca(3)
wasn't involved. -
free
ing invalid memory is reported asmemory error: invalid pointer: free
which suggests that there's something wrong with an invalid pointer namedfree
.memory error: invalid pointer passed to free
would be better. -
memory error: out of bound pointer
-> something likememory error: dereference of out-of-bound pointer
as "just" having a pointer to invalid memory is not generally UB. - Integer overflow bugs are reported as follows:
- location in input sources is missing
- the message itself does not mention overflow at all
Error: ASSERTION FAIL: __VERIFIER_error called Stack: #000000042 in __INSTR_check_add_i32 (=2147483647, =10) #100000024 in main (=1, =0) at /home/lukas/rpm-symbiotic/tests/overflows/4/main.c:5
- Generally traces that fail on
__VERIFIER_error
could say what was the actual assertion that failed (the integer overflow above is just one example) as the current trace itself is not sufficient:Error: ASSERTION FAIL: verifier assertion failed File: /opt/symbiotic/lib/verifier/klee/__VERIFIER_error.c Line: 9 assembly.ll line: 13 Stack: #000000013 in __VERIFIER_error () at /opt/symbiotic/lib/verifier/klee/__VERIFIER_error.c:9 #100000081 in main (=1, =0) at /home/lukas/rpm-symbiotic/tests/undefined/2/main.c:4
I started to look into the first issue so that we use the linked location info in the traces:
MO71[16] allocated at main(): %9 = call noalias i8* @malloc(i64 16) #3, !dbg !18
and there is a problem if the instruction is an alloca
because sbt-slicer
removes the corresponding llvm.dbg.declare
so the link between the instruction and debug info is lost. @mchalupa is there any way to convince the slicer to preserve the llvm.dbg.*
instructions?
@mchalupa is there any way to convince the slicer to preserve the llvm.dbg.* instructions?
Not a one that is implemented, but there is a way: we may set llvm.dbg.*
instructions as dependencies of the instructions to which they are related. That is actually something that I was contemplating to do in the past, because we have already ran into some issues caused by missing dbg instructions.
The unfinished work for allocation origins in a form of a patch is here: https://gist.github.com/lzaoral/b2d90972e651d14286c10b744b12e912