Optimize TD3 to not unnecessarily store bottom for just eval-ed variables

[sim642]

This was revealed by #345. Simply get-ing/eval-ing global constraint variables added bottom to rho. This unnecessarily increases rho with default values.

This PR changes TD3 such that it doesn't store those bottoms eagerly when a constraint variable is just read and never receives a real value. Thus most HM.find rho are wrapped with catching Not_found to return bottom. Is there maybe some reason I'm not aware of why TD3 doesn't use implicit bottom values already?

There were a few places where HM.mem rho was used, for which it matters whether the bottom value has been added or not. From what I can tell, these are just for the space variant and actually correspond to HM.mem wpoint, which is how those checks are presented in the TD3 paper.

I added two static variables to tune the bottom insertion behavior of init such that the old behavior can easily be toggled as well.

[michael-schwarz]

To recap from Gobcon yesterday: The bottoms that are inserted are meaningful in that the hashtable for a partial (post-)solution should be closed, i.e. not depend on any implicit bottoms for any unknown. If this is the case, the domain of the hashtable actually contains the information that these are the only unknowns that were queried by the solver during the computation of the fixpoint.

From a purely practical standpoint, I guess the question is whether one wants to introduce an option that still makes this optimization, in case one is not interested in the domain. I think this something we should then only consider if it leads to improved performance of the solver, quicker marshaling, or some other measurable improvement.

[sim642]

To recap from Gobcon yesterday: The bottoms that are inserted are meaningful in that the hashtable for a partial (post-)solution should be closed, i.e. not depend on any implicit bottoms for any unknown. If this is the case, the domain of the hashtable actually contains the information that these are the only unknowns that were queried by the solver during the computation of the fixpoint.

In the space variant, the solution hashtable isn't closed anyway and missing keys might even correspond to non-bottom values. And the paper goes through all the trouble to define the closure of such solution to make it meaningful. Surely the reasoning for closing only bottoms is much simpler since it requires no transfer function evaluations (and resolving between wpoint). So I don't think it makes things any more sophisticated than it already is.

Moreover, we already make this assumption of implicit bottoms in the partial solution all over the place: Verify2, Reachability, Control, etc. They all wrap solution lookups in such a way, so this behavior has clearly been part of Goblint's design.

EDIT 1: Even TD3 itself, before these changes, follows this convention in some places: https://github.com/goblint/analyzer/blob/139734d19e999b5780397866a32d4f5566267359/src/solvers/td3.ml#L334-L338 https://github.com/goblint/analyzer/blob/139734d19e999b5780397866a32d4f5566267359/src/solvers/td3.ml#L390-L391 https://github.com/goblint/analyzer/blob/139734d19e999b5780397866a32d4f5566267359/src/solvers/td3.ml#L473-L475 So it's not even consistent within TD3 itself and that's why it seems like this was intended, but left uncompleted at some point.

EDIT 2: To drive this even further, the TD3 article doesn't even have init. In the published version, them being bottom is implicit, but in the unpublished extended version this defaulting is explicit: Map.create (fun () -> ⊥).

[michael-schwarz]

Do we want to do something with this or close it? I would vote for only merging this if we can show it to have significant performance impact.

[michael-schwarz]

@stilscher @jerhard @sim642 Opinions on whether we should mege (with a special option) or close this?

[sim642]

I think it's not worth complicating things by having another option for this feature, which probably made no performance difference. But I'll have a closer look before closing.

[sim642]

I cherry-picked 1f4bd6e9db07526c028aab14e4c3c6e0b59ba3b8 onto master because it's orthogonal cleanup, but let's leave the rest for now.