Error tracing

[michkot]

What should the interaction of user and the analysis look like when an error has been found?

We can assume it should like like some kind of back-trace explaining the origin of such erroneous state.
Could be:

• dumping analysis specific graphic/text (SMG plots) for deduced or manually specified points of program
• print compiler-message-like line-of-code back-trace for every line that participated in origin of error-triggering value
• dumping SVCOMP-like XML error trace for the user
• dumping executable (debugging possible) error trace for the user

This issue is about

1. coming up with other user interaction patterns
2. discussing those patterns, theirs pros, cons and whether their implementation is feasible ATM
3. which patterns should we implement framework-wide / we should at least provide support for them in Angie and which patterns are suitable only for analysis-specific implementation

Keep in mind that Angie is meant to be an analysis framework.

[michkot]

From meeting 14.03.2017:

• @peringer used "last modified" flag (in Predator ADT?)
• @vojnar asks how should we work around joins? Joins introduce parallel history in the life of values/variables -> @michkot: how to solve this (pick one, merge them, list them, interactive graph?)
• @michkot asks whether analysis should create some kind of "modifications list" during regular execution OR produce these information on demand via back-tracing.
• @vojnar, @michkot: about the abstract nature of SVCOMP XML trace and how we could retrieve a concrete counter example with guided run of SMG analysis without abstractions.
• @michkot's main concerns are summarized in the first comment

[peringer]

"last modified field" is active only if previous instruction writes to field (each State.clone() cleans it). In the case of Join there should be no problem -- all but one previous instructions are JUMP (i.e. "nothing modified").

[peringer]

Our "Backtrace" should be independent on presentation form (it is in Predator). Then we can transform it to anything by some filter algorithm.

[vojnar]

Indeed, we could again get inspired by Predator and its error traces. These traces are, in fact, graphs, right? They include all branches created via joining between the entry node and the error node. This can even include loops and abstraction.

Of course, given such a graph, the user may have to do a lot of exploration to find the actual bug unless she is happy and is by chance given a trace without branching (can be enforced when prohibiting joins and abstraction as in Predator hunters).

Later, one could think of supporting some better error reporting based on some automated tool that would try to traverse the graph, following different paths in it without abstraction and trying to reach a bug.