Track written lvalues per function and use this information in Base.combine

[jerhard]

Problem: Precision loss in combine with partial contexts

When analyzing functions with partial contexts, the final state of a function f thus can contain abstract values joined over multiple calls sites with different states. At a call site of f, the combine will take the abstract values of shared memory locations, e.g. globals, from the final state of f, which may be imprecise due to partial contexts. This causes an unnecessary lose in precision when it is clear that f does not write to these memory locations.

Proposed Solution

Introduce an analysis that should track for each function (with its context) an overapproximation of the lvalues it may write to or modify via passing them to other functions. When encountering a function call, the Base analysis should query this analysis about the written lvalues. Only for these, the abstract values of the callee need to be used.

Remarks

This is probably will bring a higher benefit in a setting without earlyglobs compared to a setting with earlyglobs, as more shared memory locations (in particular globals) are kept in the local state.

[michael-schwarz]

@FelixKrayer is working on this for his Bachelor's thesis, I just forgot we had an issue for this.

Some details from the internal topic tracker:

[BA] Combatting Precision Loss From Partial Contexts in the Static Analyzer Goblint
Taint Analysis & More precise partical contexts:

• for each function keep track of the set of variables it may have written
• Use this in other analyses (in particular in the Base analysis) to only use the values of the callee for those lvals that are possible written