[QUESTION] Variables for Control Flow Trace Debugging

[lks9]

This winter, I had a student project for interactive visualization of these traces, which you can try out here. But what is currently not displayed are the values of variables or left-hand-sides. In general, it might be impossible to deterministically reconstruct them. But for us the values from a smt solver model are sufficicient, as long as the model follows the same control flow and ends with the violated assertion—this was basically the goal of "better bugreporting with better privacy" [2], so I think my approach might be worth it.

I found out that cbmc/jbmc's --json-ui or --xml-ui trace include all the lhs-assignment values we want to display in our interactive tool (it took me some time until I noticed that I need javac -g, otherwise I got a lot of anonlocal lhs-names). And I also noticed there is the cbmc-viewer.

So my question before we start to extent [1] with the lhs-values from jbmc is: Is there anything to consider? Was there already the idea to implement something similar?

Thank you in advance!

[1] https://github.com/ProRunVis/ProRunVis-examples
[2] https://doi.org/10.1145/1346281.1346322

Further Background

Some time ago, I talked with @tautschnig about following a recorded control flow trace with cbmc (I call this "retracing"). The tool is here [3].

Note that retracing is only as hard as NP-complete. Thanks to modern SAT/SMT solvers, this is good news and much better than the typical bmc complexity, which is (if I am not mistaken) PSPACE-complete. And theoretically, it is be possible to generate a retracing-SSA of polynomial size, so cbmc might be just the right tool.

But currently, we don't make use of the good complexity: For experiments with our recent implementation based on CProver.assume(...), I sometimes use trial-and-error to find a --unwind value together with --unwinding-assertions. We still plan to replace our CProver.assume(...) retracing appraoch in [3] with a direct cbmc integration in goto_symext::symex_goto() to optimize it. But this is another story (we already have similar rules for KeY [4], but sadly, the "simplification"-stuff in KeY is still by far less efficient).

[3] https://github.com/lks9/src-tracer
[4] KeYProject/key#3504

[lks9]

closed because of no response

[peterschrammel]

Hi Lukas, sorry, I missed the initial notification of this issue.
There used to exist a trace navigation tool for JBMC, which wasn't great, but proved that it is not impossible to implement a (mostly) working tool based on the existing JSON traces. I remember that quite some hacks were necessary to perform a sort of dataflow analysis to join the lhs values together. The lhs objects are essentially those that we get after translating bytecode to GOTO - so, they certainly exhibit all the artifacts introduced in the translation.

[lks9]

Hi Peter,
Thank you very much for the information, and yes, this is quite useful to know! I was hoping that there were no hacks needed, but this seems still within reason.
I would also be very interested in a copy of a tool, if you could share it with me.
Kind regards
Lukas