analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Type-safe global query system

Open sim642 opened this issue 1 year ago • 3 comments

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 InvariantGlobal query.
  • [ ] Add documentation.
  • [ ] Use this for #1394.

sim642 avatar Apr 22 '24 09:04 sim642

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?

michael-schwarz avatar May 08 '24 07:05 michael-schwarz

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.

sim642 avatar May 08 '24 07:05 sim642

True, maybe give it ask and getg then?

michael-schwarz avatar May 08 '24 07:05 michael-schwarz

This also looks like it's 95% done?

michael-schwarz avatar Feb 28 '25 17:02 michael-schwarz