this is needed to handle all sorts of different offsets that may be semantically equal, i.e., evaluate to the same physical address. In this case it keeps both elements.
After some discussion with @jerhard and @hseidl, we reached the following insights:
This behavior is overly conservative, as the mess of the address lattice contains some sub-lattices where the meet operation is semantically correct.
This now checks via a new predicate amenable_to_meet whether for the two addresses a and b this relationship between values and the meet holds. If this is the case, a meet is performed and the element added to the resulting set only if it is distinct from bot.
Currently, we answer amenable_to_meetby true whenever both arguments are strings, or when the both are addresses that differ in the numeric(!) offsets only.
This PR also adds two tests where this yields additional precision.
Currently, in the address domain inside the buckets, for the meets we use
ProjectiveSetPairwiseMeethttps://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/domain/disjointDomain.ml#L190-L205
where
B.may_be_equaldelegates tohttps://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/cdomain/value/cdomains/addressDomain.ml#L180
Addr.semantic_equalgiven byhttps://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/cdomain/value/cdomains/addressDomain.ml#L102-L111
which calls
SD.sematic_equalhttps://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/cdomain/value/cdomains/stringDomain.ml#L77-L81
this is needed to handle all sorts of different offsets that may be semantically equal, i.e., evaluate to the same physical address. In this case it keeps both elements.
After some discussion with @jerhard and @hseidl, we reached the following insights:
This behavior is overly conservative, as the mess of the address lattice contains some sub-lattices where the
meetoperation is semantically correct.This now checks via a new predicate
amenable_to_meetwhether for the two addressesaandbthis relationship between values and the meet holds. If this is the case, a meet is performed and the element added to the resulting set only if it is distinct frombot.Currently, we answer
amenable_to_meetby true whenever both arguments are strings, or when the both are addresses that differ in the numeric(!) offsets only.This PR also adds two tests where this yields additional precision.
Closes #1467