search

goblint / analyzer

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

Structs sets domain causes many incomparable comparisons on zstd #699

Open sim642 opened 2 years ago

sim642 commented 2 years ago

Out of curiosity I wanted to try the sets domain for base structs (from #419) on zstd, because with simple structs we lose the relationship between its thread pool functions and their arguments: image Therefore we end up calling all the job functions with all the opaque arguments, so calling the functions with arguments of completely wrong types, which cannot possibly be good for precision.

Unfortunately it generates an insane amount of incomparable warnings like:

warn_type leq: incomparable abstr. values Int and Address at lib/common/fse_decompress.c:267:14-267:54: (0) and {}

It's so bad that in a minute it produces more output than the entire ~45 minute analysis with simple structs on zstd.

sim642 commented 2 years ago

On a minimized example in our regression tests, in #716 it turned out that these relational struct domains wouldn't even help, because they are still joined together before evaluating offsets on them.