Incremental analysis: Eagerly analyze functions in force-reanalyze, even when reluctant is on
#600
Conversation
Goblint fails to prove the assertion in the incremental run. See issue #508.
…reached problem is exhibited.
… incremental.reluctant.on is activated. Force-reanalyze is intended to be used when functions are to be reanalyzed with different precision, e.g. differnt int-domains activated. Reluctant analysis (as-is) does not work for this kind of re-analysis, as the entry transfer function is not re-evaluated in the reluctant mode. Thus, this commit disables reluctant analysis for functions that are contained in the list of force analyzed functions.
… points, avoid explicitely solving their return nodes. The reluctant analysis stores the old abstract values at the return nodes of changed functions; it omits the eager destabilization of these changed functions. Instead it calls solve on the return nodes of changed functions and checks whether the abstract state changed. For functions in force-reanalyze, a reluctant analysis should not be performed (see issue #508). This commit adapts the reluctant analysis such that the entry nodes of functions in force-reanalyze are eagerly destabilized. The call of solve on the return node of these functions can therefore be omitted.
…ation. This test shows that the changing the precision annotation already works, even when incremental.reluctant.on is activated; This is (probably) because the functions calling a function with changed annotations are considered changed themselves.
src/solvers/td3.ml
Outdated
| eager || StringSet.mem f.svar.vname force_reanalyze | ||
| in |
There was a problem hiding this comment.
There might be a better way to do this than with a string set in the solver.
There was a problem hiding this comment.
I guess that could be covered by #596, but I'm a bit hesitant on doing that since it will make the master vs interactive branch TD3s significantly more different and thereby complicating merges (either way) between the branches.
But for now, a possibility might be an extra field in change_info about force reanalyze functions and the current logic inside the solver could look that up instead of dealing with the option. The incremental preprocessing would then be in charge of populating the list appropriately.
There was a problem hiding this comment.
As mentioned below, a set of varinfos belonging to functions with a name listed in force-reanalyze is now collected within CompareCIL.
|
An alternative approach to fix #508 would be to mark functions that call functions in |
…luctant is off. The set `obsolete_prim` is eagerly destablized; it does not need to be collected when reluctant is on. When reluctant is on and at the same time, some function is in force-reanalyze, this function will be considered a completely changed function, and not as partially changed. Therefore the unknowns belonging to its function entry node are collected in `obsolete_entry` beforehand; which will be eagerly destablized as required.
…lly called function
…ions are partially changed.
…nfo. Functions are still listed in .changed, as they should be treated as changed.
Problem
For functions for which the precision setting was changed for the incremental run, the analysis cannot be done reluctantly, as the
enterneeds to be redone for the precision adjustment to take effect, which does not happen in an reluctant incremental analysis. See issue #508.Functions for which the precision was adjusted are listed in
incremental.force-reanalyze.funs. Thus, a reluctant analysis should not be performed for functions contained in this set.Note that functions for which the precision was changed through an in-code annotation there is no problem with the reluctant analysis: This is because the call-sites of such functions are detected as changed; thus all functions calling such a function with a new in-code precision annotation are reanalyzed. So no further changes are required for the in-code annotation case.
Background on reluctant incremental analysis
The reluctant analysis stores the old abstract values at the return nodes of changed functions; it omits the eager destabilization of these changed functions. Instead it calls solve on the return nodes of changed functions and checks whether the abstract state changed.
Description of changes
This PR adapts the reluctant analysis such that the entry nodes of functions in force-reanalyze are eagerly destabilized. This is done by collecting the function entry nodes of such functions, and performing the destabilization of such function entry unknowns (in
obsolete_entry) even whenreluctantis on.The call to
solveon the return node of these functions is therefore omitted. This is achieved by not collecting unknowns belonging to return nodes of functions inincremental.force-reanalyze.funsinobsolete_ret.Closes #508.