analyzer
analyzer copied to clipboard
Limit YAML witness invariants to to-be-read and just-written variables
As discussed in GobCon, this would be something to somewhat limit the large number of invariants we generate. Since accesses are to lvalues, not just variables, this also has lvalue granularity, because accessing a field in a large struct will the only emit one invariant about that field instead of all the fields of the struct.
Changes
- Add access event set to access analysis local state and
MayAccessed
query to use it in YAML witness generation. - Split access analysis by extracting race analysis from it. Now access analysis is only concerned with collecting all accessed lvalues from all expressions in all transfer functions, while race analysis uses that to construct its race tables in the global invariant.
- Generalize
Access
event andInvariant
query from optionalvarinfo
to lvalue set. Still uses a separateInvariant.context1
within the base analysis because the existing logic is per-lvalue. - Fix
Invariant
query offset handling in base analysis. - Add
query
tracing.