Add explicit W set to base protection privatization

[sim642]

Regarding #1636 (comment).

Surprisingly, there was even a TODO about it:

analyzer/src/analyses/basePriv.ml

Lines 940 to 943 in a935456

	let unlock ask getg sideg (st: BaseComponents (D).t) m =
	let sideg = Wrapper.sideg ask sideg in
	let atomic = Param.handle_atomic && LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
	(* TODO: what about G_m globals in cpa that weren't actually written? *)

[michael-schwarz]

This looks reasonable! Could you maybe add a regression test where this make a difference?

I will try if this also behaves the intended way in the context of #1636. If it does and after adding a test, we should be good to go!

[michael-schwarz]

It falls short of what the snippet in #1636 achieves, likely because that one encodes a cheap path-sensitivity like behavior.

I pushed the merged verison to https://github.com/goblint/analyzer/tree/tmp_dn_1693 so we can play around with it.

[sim642]

Hmm, I suppose keeping separate CPA maps for written and refined values could be more precise indeed.
Although that doesn't seem like it should to be specific to Protection-Based Reading, but potentially all/many privatizations?

[michael-schwarz]

Although that doesn't seem like it should to be specific to Protection-Based Reading, but potentially all/many privatizations?

Sure! I think for base we know that it pays off. Not sure whether it's worth adding it to all privatizations?

[sim642]

To each one individually, probably not. I was thinking more along the lines of some kind of generic lifting with the dual CPAs or something. I don't have a specific idea though, so it might not really be possible so generally.