Narrowing of globals in TD

[Red-Panda64]

Description

Adds the capability of narrowing globals (and function entry unknowns) to TD. Contributions to each global unknown are tracked per source unknown. When an unknown x triggers a side-effect to y, this side-effect is applied to x's contribution to y by warrowing. The overall value of a global unknown is computed as the join over all contributions to said unknown.

Configuration Options

• ana.base.priv.protection.changes-only: protection-based privatization won't produce spurious side-effects to protected unknowns. Otherwise, abstract values for globals that are refined by a guard edge may be written back to said global without a true write-access ("pseudo-writes"). This should have no benefit when narrowing of globals is disabled, as the pseudo-writes are already subsumed by the respective global. Implemented for base privatization only.
• solvers.td3.narrow-globs.enabled: enables the global narrowing scheme.
• solvers.td3.narrow-globs.conservative-widen: side-effects are only applied to contributions by widening if applying them with a join would affect the overall value of a global.
• solvers.td3.narrow-globs.immediate-growth: irrespective of this option, side-effects from x to y are accumulated throughout an evaluation of x to ensure soundness. This guarantees that the final side-effect will subsume all prior ones from this evaluation. This option permits the immediate application of accumulated values during constraint evaluation, provided they are not subsumed by the current contribution of x to y. Otherwise, the accumulated value is applied after x is fully evaluated.
• solvers.td3.narrow-globs.narrow-gas: limit the number of switches between widening and narrowing per contribution. This is necessary to enforce termination.
• solvers.td3.narrow-globs.eliminate-dead: if an unknown x triggers no side-effect to y but did so previously, its contribution is narrowed with bottom. Should y become bottom and be a function entry unknown, the exit unknown will be queried, propagating bottom throughout the function body.

Modifications to td3.ml

• new structure divided_side_effects: to track current values of contributions, last combination mode (widen or narrow), and counter for remaining mode switches
• new structure narrow_globs_start_values: explicitly track initial values for unknowns to ensure they are accounted for when the join over all contributions is computed
• new structure prev_sides maps unknowns to side-effected targets on the last evaluation

Modifications to basePriv.ml

Optionally track "true writes" for protection based privatizations: in addition to CPA tracking the most precise available value per global variable, the new data structure tracks only values that were written. In particular, this excludes refined values that were obtained via guard edges (e.g. inside an if (g < 10) block), which are also stored in CPA for increased precision but do not correspond to real writes.

Modifications to constraint system

Constraint system can provide a hint in the form of the "postmortem" function, that returns for some side-effect target unknown that has become bottom, which local unknowns might now be worth re-evaluating. The purpose of this is to allow the re-evaluation of function exit nodes, when their entry becomes bottom, in order to propagate this bottom value and remove superfluous side effects along the way.

[Red-Panda64]

For now, this is only a draft because I will see if I can't extract the changes to td3.ml and put them behind a reusable module.

[Red-Panda64]

Although it should be possible to extract this into a module, doing so is a bit of a hassle because of the way td3's current side-effect widening strategies are very closely tied to the internals of td3. In any case, it makes no sense to try and do this until #1442 has been accepted or rejected.

[sim642]

This has similar connotations to #365: calling solve like this on an x which is influenced by the current y turns it into a forward-propagating solver (in part), as opposed to remaining fully demand-driven.
Like with #365, this seems like it could ask to solve things which maybe nothing depends on any more, just doing extra work.

[michael-schwarz]

This is precisely why that is there! I'll share the draft paper with you that explains this once we have a little more time next week.

[michael-schwarz]

This is closely tied to the remark above: The idea is that for those unknowns in postmortem we are willing to pay this additional penalty in order to collect dead side-effects and potentially improve the values at globals. Dead code will be pruned at the end by reach but that doesn't shrink side-effects.

For those with access to our drafts at https://github.com/tum-cit-pl, this is discussed in https://github.com/tum-cit-pl/combatting-precision-loss Section 4.3, where we also have the remark that forward propagating solvers exhibit this behavior out of the box.

[sim642]

It might be worth revisiting #349 in light of all this abstract garbage collection and Ali's findings about the inefficiency of large solver hashtables.
At the time, #349 probably wasn't as useful as it now would be because unreachable contexts wouldn't be bottomed. But if the abstract garbage collection now performs recomputations that propagate bottoms, then we might end up with a bunch of bottoms in the hashtables with no benefit. They would just keep the hashtables large, which slows down their usage.

[michael-schwarz]

The failing CI is due to the CI not being able to download ocamlfind from http://download.camlcity.org/download/findlib-1.9.6.tar.gz.

[sim642]

I don't really like how this is going against our long-term goal of not having an uncomprehensively massive td3.ml. It was a big reason for reverting the aborting feature (#364), even though it had significant benefit.
Or if we want to allow td3.ml as a dumping ground for all sorts of new things without regard to modularization, then this is something we should re-decide collectively, because it will make it increasingly difficult to add new features if everything is super-coupled.

[michael-schwarz]

@sim642: I have now pulled things out into a separate module. Let me know if you prefer this version!

[michael-schwarz]

@sim642: Any further comments here? Otherwise I suggest merging now that the paper is accepted at PLDI.

[sim642]

Thanks for putting in the effort to extract things into a separate module. I haven't had the time to look at this yet, but hopefully can soon.

[sim642]

Other than one comment in a test (#1636 (comment)), I think this is now in good enough shape.