analyzer
analyzer copied to clipboard
Type-safe global query system
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
- [x] Convert
InvariantGlobalquery. - [ ] Add documentation.
- [ ] Use this for #1394.
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?
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.
True, maybe give it ask and getg then?
This also looks like it's 95% done?