analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

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

Open jerhard opened this issue 2 years ago • 0 comments

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.

jerhard avatar Jan 20 '22 17:01 jerhard