More descriptive error traces

[lzaoral]

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:

  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
  

  It would be definitely useful to extend this with location info pointing to the original sources as well.
• freeing stack memory is reported as free of alloca which suggests that the memory was explicitly allocated by alloca(3) which is generally not true. I suggest something like memory error: free of address on stack if the alloca(3) wasn't involved.
• freeing invalid memory is reported as memory error: invalid pointer: free which suggests that there's something wrong with an invalid pointer named free. memory error: invalid pointer passed to free would be better.
• memory error: out of bound pointer -> something like memory 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
  

[lzaoral]

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]

@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.

[lzaoral]

The unfinished work for allocation origins in a form of a patch is here: https://gist.github.com/lzaoral/b2d90972e651d14286c10b744b12e912