Wrong c line number in generated bpl file

[octopus-yun]

Hallo,

I am working with Hernan @hernanponcedeleon and developing the Dartagnan to generate a graph with failed c program. And I need to select the useful information from transformed bpl file (with cmd smack -t path-for-cfile -bpl bpl-file-name --clang-options=-DCUSTOM_VERIFIER_ASSERT), then I have found that some events were shown in generated bpl file with a wrong line number from c file. For example: in attachment are a c file and a corresponding generated bpl file, and the events in c file with line number 27 and 28 are assigned in bpl file with line number 30, I think here is a bug for the selecting line from c file. bug.zip

[zvonimir]

Hi! Thanks for reporting this! We are busy with SVCOMP :), but I'll try to take a look this coming week. Note that in general line numbers in SMACK are only as good as debug info that clang generates. Typically, clang generates pretty good debug info, but we've certainly seen programs where debug info is off. We'll get back to you.

[hernanponcedeleon]

Thanks @zvonimir for the pointer. Assuming you get the debug Information via -g flag, it seems clang is providing the correct one (see sample.ll.zip).

The $i4, $i5, $i6 instructions are coming from

  store i32 %12, i32* %4, align 4, !dbg !64
  store i32 0, i32* %6, align 4, !dbg !65
  store i32 0, i32* %5, align 4, !dbg !66

and the following debugging info

!64 = !DILocation(line: 26, column: 7, scope: !43)
!65 = !DILocation(line: 27, column: 7, scope: !43)
!66 = !DILocation(line: 28, column: 7, scope: !43)

[shaobo-he]

Hi @hernanponcedeleon I assume the code fragment you attached is before the optimization passes applied by SMACK, some of which cannot preserve debug information. For example, we use the mem2reg pass which converts stack allocations into registers. Therefore, load/store instructions involving stack allocations will be removed as well as their debug info.

[hernanponcedeleon]

@shaobo-he the code I gave above was obtained using directly clang (with no optimisations).

However I would assume that if some debug information is lost during the optimisation passes, the SMACK would not create the corresponding :sourceloctag for those instructions. For instructions $i4, $i5, $i6 (which are stores involving stack allocations), I would not expect to see the line assume {:sourceloc "output/bresenham_unwindbound2_tmp.c", 30, 5} true;