search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Use ppx_deriving_hash 0.1.2 #1395

Closed sim642 closed 3 months ago

sim642 commented 3 months ago

This gets rid of some ppx_deriving_hash related TODOs by using a version of it which includes their support.

michael-schwarz commented 3 months ago

LGTM!

Side remark: Have you discussed with @stilscher the issues that ppx_deriving_hash breaking the invariants ensured by the Stdlib.hash (hashes being portable between 32 and 64 bit machines) causes for gobview? The search being broken seems to, e.g., be a consequence of this.

sim642 commented 3 months ago

Side remark: Have you discussed with @stilscher the issues that ppx_deriving_hash breaking the invariants ensured by the Stdlib.hash (hashes being portable between 32 and 64 bit machines) causes for gobview? The search being broken seems to, e.g., be a consequence of this.

Briefly, yes. ppx_deriving_hash is hardly the culprit here: Goblint still contains many manual hash implementations that also don't guarantee this. Also hashes from dependencies might not, so it's hard to guarantee that.

I vaguely remember this point coming up before but I don't know where and why. Our Printable.relift exists precisely to fix this by rehashing marshaled data. Maybe the issue at the time was just fixed by properly recursing relift into all the necessary places.

What search is broken right now? During some recent changes I actually tested GobView's syntactic/semantic search and it seemed to work. GobView CI also tests this.

michael-schwarz commented 3 months ago

GobView's semantic search

Last I heard from Sarah that was still broken.

sim642 commented 3 months ago

Odd, because in #1372 I broke the GobView CI and also fixed it, so it seems to still work there.

michael-schwarz commented 3 months ago

Ah, nevermind, I wasn't up-to-date it seems.