search

goblint / analyzer

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

Type-safe global query system #1423

Open sim642 opened 2 months ago

sim642 commented 2 months ago

Queries like WarnGlobal and InvariantGlobal are only used globally in dummy ctx. Moreover, they have Obj.t arguments which are unsafe. Every analysis lifter which adds its own global unknowns must have special cases for converting such arguments for WarnGlobal and InvariantGlobal. If that is forgotten, then Goblint simply segfaults.

This PR introduces global queries using a separate global_query "transfer" function and gctx global "context" for the queries, which doesn't require all the dummy data.

TODO

michael-schwarz commented 2 months ago

Could we maybe think of better names for these things? I think ctx and query are things we are overusing already.

Also, WarnGlobal does not really fit into the category query anyway, as it returns unit. Maybe for it, a separate transfer function that does not get a ctx but only an ask and is called per analysis at the end of the analysis would be the more principled thing?

sim642 commented 2 months ago

Just ask isn't enough for these kinds of things though, they also need global. For example, the deadlock analysis needs to traverse the entire cycle starting from a global.

michael-schwarz commented 2 months ago

True, maybe give it ask and getg then?