search

goblint / analyzer

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

Type-based incremental restarting #617

Open sim642 opened 2 years ago

sim642 commented 2 years ago

In some cases it might be necessary to do manual incremental restarting not by a global variable name, but a type name. In particular, the access analysis has some type-based unknowns which cannot be manually restarted otherwise.

jerhard commented 1 year ago

In particular, the access analysis has some type-based unknowns which cannot be manually restarted otherwise.

Can you elaborate on this? Which typed-based unknowns cannot be manually restarted in the access analysis?

sim642 commented 1 year ago

If there's an access to a struct field on an unknown pointer, then that's collected under the memory location (struct foo).bar. To restart those, you need to restart the type struct foo.

jerhard commented 1 year ago

@just-max Ok, so I guess the general steps to implement this would be as follows:

  1. Extend the type VarQuery.t with a variant for C-types.
  2. Allow for types as input for the restarting mechanism This would enable the general mechanism requested by this issue, i.e. that analyses can provide some iteration by type
  3. Adapt the AccessAnalysis, to implement an answer to the IterSysVars query, that in particular implements the case that the query is about a type.

Regarding 3: Currently, the globals in the AccessAnalysis are program Nodes, which are mapped to a set of accesses. Since we want to be able iterate over program variables / types in these sets, one would have to iterate over all unknowns (i.e. nodes) and check the sets that are associated with them to see whether the set contains one of the variables / types of interest.

sim642 commented 1 year ago

Actually now that race analysis is split off from access analysis, IterSysVars should be in RaceAnalysis instead.