Fix load_run pruning entire solution in Gobview

[sofamaniac]

Fixed the issue that prevented gobiew semantic search from working. It was due to the results of the analysis being pruned again by gobview.

Closes goblint/gobview#7.

[sim642]

Should have indeed, but pruning a pruned solution shouldn't delete everything either, so this might be indicative of a deeper issue. If a solution is loaded, then the postsolver should be doing complete reverification anyway to check its validity and emit the warnings (by corresponding postsolvers), so it should still be reaching all the nodes and not pruning them.

[sim642]

Just a thought, maybe the postsolver runs correctly on the loaded solution to check it and prints its warnings. While doing that it also collects a reachable set, which should prevent everything from being pruned. But maybe due to some hashconsing relifting problem, the reachable set lookups all fail, despite the values being in there or something.

[sofamaniac]

The issue is caused by the fact that in that reachable set, the node's id are not the same as in the one that are unmarshalled, which cause the pruning to remove everything.

[sim642]

That's unusual because the postsolver should add to the reachable set the same nodes that it handles when iterating the loaded solution.
Maybe something related to this Gobview change? goblint/gobview@f8c509d

[sofamaniac]

Okay so commenting out the code of goblint/gobview@f8c509d does indeed restore the correct node id, but it does not solve the problem that the pruning remove everything.
So the way gobview load a solution must differ from the way of goblint

[sim642]

Oh damn! I automatically thought you were already testing with that change.
Turns out that commit was on the master branch in Gobview's repository, but the gobview submodule in this Goblint's repository hadn't yet been updated to include that commenting out. I now did that though.

I suppose one thing to try would be disabling ana.opt.hashcons to see if it might have anything to do with hashconsing and relifting.

[sofamaniac]

Disabling ana.opt.hashcons does indeed solve the issue, but I don't think the issue comes directly from it, as one can execute a query with ana.opt.hashcons enabled and the load_run option set to some directory containing the results from goblint, and it works as expected.

My best guess is that there is something different between goblint's initialization and gobview's one, which I cannot find.

[jerhard]

Does GobView already perform relift on the loaded data, so that the hashcons tables are populated again?
Similar to what Goblint already does for the compare_runs option:

analyzer/src/framework/control.ml

Lines 440 to 442 in fe5c98d

	VH.iter (fun k v ->
	VH.replace vh' (S2.Var.relift k) (S2.Dom.relift v)
	) vh;

[sofamaniac]

The code you linked is for the case the compare_runs option is set. For the load_run option in both Goblint and Gobview the relifting is done with the same code :

analyzer/src/solvers/generic.ml

Lines 20 to 26 in fe5c98d

	let vh' = VH.create (VH.length vh) in
	VH.iter (fun x d ->
	let x' = S.Var.relift x in
	let d' = S.Dom.relift d in
	VH.replace vh' x' d'
	) vh;
	vh'

[michael-schwarz]

I decided to take a look at it today as well. Even when I disable hash consing, the issue is still there.

What is fascinating is that the key is not found when checking for membership of reachable, but when I iterate over reachable checking with S.Key.equal a corresponding entry is found. This points at some potentially deep issue with the hashtables after marshalling (hopefully only in the Javascript world).

I then try to replace the lazy computation in HashCashed with fresh computation ignoring the potentially cached value, it works as expected in that case. The question is if we can perform some sort of relifting automatically or whether that will break invariants of those hash tables that are not fresh (as reachable is).

[sim642]

The question is if we can perform some sort of relifting automatically or whether that will break invariants of those hash tables that are not fresh (as reachable is).

My first thought would be to implement relift in the different HashCached functors to perform that forceful recomputation. Currently they're either missing or identity (for the specialized case actually used). And to also ensure that the relift calls are delegated through all the Spec lifting layers up to base's CPA, which is the one to use HashCached.

This of course means that relifting doesn't only need to be done with ana.opt.hashcons, but also when hashcaching is used. Maybe it makes sense to also have an option for that? Otherwise we'd always have to do relifting.

This points at some potentially deep issue with the hashtables after marshalling (hopefully only in the Javascript world).

I guess this could be related to the 64bit vs 32bit nature of int overflow and how it affects hash implementations. If relifting recomputes all the hashes in JS, it hopefully should ensure that consistency still.

[michael-schwarz]

Yes, those things I will have to do for sure. What I am a bit worried about is what happens to a hashtable if the underlying hash changes (because it is now a 54 bit integer instead of a 63 bit one)? I fear one might have to clean the hashtable and repopulate it or some such nonsense to restore the invariants a hashtable relies upon.

But I guess we'll have to see

[sim642]

I fear one might have to clean the hashtable and repopulate it or some such nonsense to restore the invariants a hashtable relies upon.

That's exactly what the relifting for load_run or TD3 does though. There's also Hashtbl.rebuild in recent OCaml versions, although that's no use to us since we want our relift to also change the objects (e.g. in hashconsing or hashcaching).

[michael-schwarz]

That's exactly what the relifting for load_run or TD3 does though.

Not really though: it mostly ensures that the things are added back to the hash-consing table (empty after marshall), but do not modify the underlying hash-table in that the computed hashes should stay the same regardless of hash-consing or not. This is not the case here, the freshly computed hash might (and will likely) be different form the previous one.

But I'll just try to implement it (maybe on the train today), and we'll see!

[sim642]

but do not modify the underlying hash-table in that the computed hashes should stay the same regardless of hash-consing or not.

They create a new hashtable and add all the relifted things to that. Adding the keys to a new hashtable recomputes their hashes. Except for HashCached, which just return the stored hash currently.
It's what Hashtbl.rebuild would also do (although maybe slightly more cleverly).

[michael-schwarz]

Ah, I see what you mean now!

analyzer/src/solvers/td3.ml

Lines 480 to 505 in 5e55c1d

	if loaded && GobConfig.get_bool "ana.opt.hashcons" then (
	let rho' = HM.create (HM.length data.rho) in
	HM.iter (fun k v ->
	(* call hashcons on contexts and abstract values; results in new tags *)
	let k' = S.Var.relift k in
	let v' = S.Dom.relift v in
	HM.replace rho' k' v';
	) data.rho;
	data.rho <- rho';
	let stable' = HM.create (HM.length data.stable) in
	HM.iter (fun k v ->
	HM.replace stable' (S.Var.relift k) v
	) data.stable;
	data.stable <- stable';
	let wpoint' = HM.create (HM.length data.wpoint) in
	HM.iter (fun k v ->
	HM.replace wpoint' (S.Var.relift k) v
	) data.wpoint;
	data.wpoint <- wpoint';
	let infl' = HM.create (HM.length data.infl) in
	HM.iter (fun k v ->
	HM.replace infl' (S.Var.relift k) (VS.map S.Var.relift v)
	) data.infl;
	data.infl <- infl';
	data.st <- List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st;
	);

[michael-schwarz]

Could this issue be related to the issue you uncovered with List.mem @sim642?

[sim642]

Could this issue be related to the issue you uncovered with List.mem @sim642?

I don't believe so. I directly fixed remaining instances directly on master: bcb4de2. None of those seem in related places though.

This issue would have to be looked at again, so much has changed in the meanwhile. And I think the discussion in last comments here was never tested in implementation.

[michael-schwarz]

Thank you again! This does not seem to be the solution we want, so I am closing this for now.