Make precision refinement compatible with reluctant destabilization

[stilscher]

Reluctant destabilization takes the abstract value of the entry point of a changed function from the previous run to re-evaluate the changed function. With the precision refinement the new (increased) precision is projected at the entry edges. With reluctant destabilization this entry edge to a changed function will however never be reevaluated if there are no actual code changes in the changed function that affect the abstract value at its return point. This results in the fixpoint not being reached at the entry state of the changed function.

As a test case for this issue one can refer to incremental/01-force-reanalyze/00-int with additionally activated reluctant destabilization.

[jerhard]

With reluctant destabilization this entry edge to a changed function will however never be reevaluated if there are no actual code changes in the changed function that affect the abstract value at its return point. This results in the fixpoint not being reached at the entry state of the changed function.

To elaborate, the verifier complains about an unreached fixed-point, when the verifier itself is not incremental. Then the verifier does re-evaluate the enter and thus obtains a state with a different set of active domains.

[jerhard]

The idea to fix would be to also re-evaluate the call edges for calls to changed functions in the reluctant analysis.
One would utilize the side_dep set and now additionally remove the unknowns from stable that depend on any unknown relating to the return node of the changed functions. The solve would then be called on these unknowns.

This will lead to some more evaluations in the reluctant setting, especially if there are many calls to the changed function. This leads to the question whether re-doing the enter/combine should be an option, or whether we can get around re-doing the enter/combine for all changed functions -- it really should only be needed for functions for which the activated int-domains or the context-information that is tracked has changed.

[jerhard]

it really should only be needed for functions for which the activated int-domains or the context-information that is tracked has changed.

That would mean introducing a separate list of functions, similar to force-reanalyze, for which the enter/combine would be re-evaluated.

[sim642]

Why not just exclude force-reanalyze functions from reluctant destabilization?

[jerhard]

That actually seems like a good idea: When a function is re-analyzed with different int-domains, the resulting end state should never be leq compared to the old state. (Unless there are no ints in the abstract states of the function, in which case activating different int-domains would be meaningless.)

Edit: although one would not check the state and the return node of the function, but rather the state after the calls to the function. This could still yield some benefits for a reluctant version.

[jerhard]

Closing this as #600 is merged into incremental.