Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Aug 10, 2022

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. Simplify base analysis invariant logic to use a single lvalue instead of invariant context.
  4. Fix Invariant query offset handling in base analysis.
  5. Add query tracing.

@sim642 sim642 added feature usability performance Analysis time, memory usage labels Aug 10, 2022
@sim642 sim642 self-assigned this Aug 10, 2022
@sim642 sim642 marked this pull request as ready for review August 25, 2022 13:27
@sim642 sim642 added the sv-comp SV-COMP (analyses, results), witnesses label Aug 25, 2022
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As soon as the comment about the unitAnalysis is addressed, I think this is good to merge!

@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Sep 27, 2022
@sim642
Copy link
Member Author

sim642 commented Sep 27, 2022

This will conflict with #833 and I think it'll be easier to have that merged first.

@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Oct 4, 2022
@sim642 sim642 merged commit 06c4a92 into master Oct 4, 2022
@sim642 sim642 deleted the access-local branch October 4, 2022 07:57
sim642 added a commit that referenced this pull request Oct 4, 2022
@sim642 sim642 added this to the v2.1.0 milestone Nov 21, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

feature performance Analysis time, memory usage sv-comp SV-COMP (analyses, results), witnesses usability

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants