hernanponcedeleon/Dat3M

Feature: Improved source tracing and visualization of static analysis results

ThomasHaas opened this issue · 0 comments

SImilar to #534, we should have better ways to visualize (and hence understand) our own internal analyses results.
By internal analysis results, I mean things like aliasing relationships, call/control-flow graphs, data-dependency graphs etc.
To make these results easily accessible/readable, we should relate them to the source code instead of our own internal representation. This would also allow us to easily see if there are obvious imprecisions in the analyses.

To do this, we need to keep more LLVM metadata in addition to just the source location. For example, we should keep source-language types, names of local variables, field access expressions (e.g., r = load(ptr) might have been a int r = struct->x), etc.

I think just having the expression for all loads/stores in the source language would already be tremendeously useful to compactly visualize the alias analysis results. Say we find load(ptr1) and load(ptr2) to be possibly aliasing, but in the source language we see that the corresponding expressions are struct->X and struct->Y, then we immediately know that we were imprecise.