search

goblint / analyzer

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

ExpRelation analysis ignores overflows #776

Open sim642 opened 2 years ago

sim642 commented 2 years ago

As pointed out in https://github.com/goblint/analyzer/pull/770#discussion_r912977915, the expRelation analysis makes some claims about expressions containing arithmetic which may overflow. Depending on the configuration, we might not want it to make definite claims about expressions that become unsound due to overflows. This doesn't concern just signed overflow (for which we have an option), but also unsigned overflow.

As I found out in #770, most of those seem completely untested beforehand, so instead of fixing maybe they could largely just be removed. Unless there are some non-regression test programs where these expRelations matter.

michael-schwarz commented 2 years ago

ExpRelation is crucial to the partitioned array domains working, and I think we should actually keep some such analysis that infers the relationship between variables symbolically. (I agree that we need to think about overflows here though - maybe it is possible to do overflow checks or in the worst case only enable this domain when we assume no overflows)

Note that it is an analysis only by name, I formulated it as an analysis mostly to be able to conveniently query it.

sim642 commented 2 years ago

ExpRelation is crucial to the partitioned array domains working

I'm not sure how crucial it really is though. In https://github.com/goblint/analyzer/pull/770/commits/16c70bcc8d4846352d54e06395ee275892b23402 I managed to remove most of these cases without any regression test failing.