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 https://github.com/goblint/gobview/issues/7.

[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! https://github.com/goblint/analyzer/blob/5e55c1d964b018bb0831f04e9adc2776e09a760c/src/solvers/td3.ml#L480-L505

[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: bcb4de29e22885570ba82f7ec9cee2e661854b7a. 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.