search

goblint / analyzer

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

Meet of string pointers in address domain imprecise #1467

Open michael-schwarz opened 1 month ago

michael-schwarz commented 1 month ago

Currently the meet of an unknown string pointer and a known string pointer is the unknown string pointer.

{"string"} \sqcap {(unknown string)} = {(unknown string)}

The problem seems to be in the address domain, as the actual meet in the string domain which is defined to return the known pointer

https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/cdomain/value/cdomains/stringDomain.ml#L99-L108

is never actually called.

michael-schwarz commented 1 month ago

The call propagates until ProjectiveSetPairwiseMeet

https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/domain/disjointDomain.ml#L190-L205

where B.may_be_equal delegates to

https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/cdomain/value/cdomains/addressDomain.ml#L180

Addr.semantic_equal given by

https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/cdomain/value/cdomains/addressDomain.ml#L102-L111

which calls SD.sematic_equal

https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/cdomain/value/cdomains/stringDomain.ml#L77-L81