analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Limit YAML witness invariants to to-be-read and just-written variables

Open sim642 opened this issue 1 year ago • 0 comments

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

  1. Add access event set to access analysis local state and MayAccessed query to use it in YAML witness generation.
  2. 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.
  3. Generalize Access event and Invariant query from optional varinfo to lvalue set. Still uses a separate Invariant.context1 within the base analysis because the existing logic is per-lvalue.
  4. Fix Invariant query offset handling in base analysis.
  5. Add query tracing.

sim642 avatar Aug 10 '22 07:08 sim642