Assignment line number in trace wrong in a special case

[AdamZsofi]

In the case of expressions similar to this:
if (p2 != 0) {
lk2 = 1;
} else {}
the line number in trace will be the line number of the condition instead of the assignment.

[Deleted user]

What flags did you use?
I think it can help if you add --show-final-cfg and add here the resulting files (.main.dot I think). (Maybe an optimization kicks in that transforms this into lk2 = (p2 != 0 ? 1 : lk2) (more precisely LLVM::SelectInst).
If you add --no-optimize, does the result change?

[sallaigy]

This is exactly what happens - sadly this optimization is the consequence of the mem2reg pass itself, however the location of the computation p2 != 0 is still set to the line of the if, therefore we report that location in the trace (both locations point to the line of the if):

%tmp53 = icmp ne i32 %tmp35, 0, !dbg !69
%.04 = select i1 %tmp53, i32 1, i32 0, !dbg !71
call void @llvm.dbg.value(metadata i32 %.04, metadata !18, metadata !DIExpression()), !dbg !47

Fun fact: as this is basically metadata for debuggers, you can get a similar issue if you compile the final module and run it with gdb:

57	        if (cond == 0) {
(gdb) 
94	        if (p2 != 0) {
(gdb) 
98	        if (p3 != 0) {
(gdb) 

I have started working on a PR to add extra instrumentation so we can follow assignments to local variables better (@RL555 this might be interesting to you as well): #18

[AdamZsofi]

I have locally merged the branches svcomp-witness-output and trace-locations-after-mem2reg, the fix already solves the issue with the witnesses.

[hajduakos]

What's up with this issue? Seems like a wontfix to me. @AdamZsofi please close if we don't plan to work on this anymore

[AdamZsofi]

You're right, we'll probably won't work on this for a while or we'll just find some workarounds, if needed.