Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve memset analysis #696

Merged
merged 8 commits into from
Apr 27, 2022
Merged

Improve memset analysis #696

merged 8 commits into from
Apr 27, 2022

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Apr 25, 2022

This contains additional attempts to improve race detection precision on zstd after the soundness fixes.

I noticed that certain memset calls are accessing an unreasonably large number of memory locations and causing write races there. As a special function, the access analysis calculates the set of reachable addresses from its argument(s) and emits writes to all of them. Notably, if a memset struct contains a pointer to something else (another struct), then a write to the latter is also added. But this is unnecessarily imprecise, because memset only changes/writes what it immediately points to and doesn't dereference any pointers inside. In general special functions may do that, but memset (and probably many others) don't as generic functions, so instead of reachable addresses it suffices to just emit accesses to may point to addresses (i.e. not go transitive).

Additionally, I tried to fix #691, i.e. add explicit memset handling to base analysis as well. My hope is that this avoids introducing at least some unknown pointers whose calls later cause spurious races.

Changes

  1. Hack access analysis to not use reachability for memset. This is very ad-hoc for the time being. Ideally each invalidation argument would also specify whether it may access transitively or not.
  2. Cherry-pick access analysis type-partitioning unsoundness fix from Add option for ignoring races from free #695 because a similar (but not the same) issue appears here (no alloc variables in the failing test). Instead, the access analysis incorrectly calculates the type of the memset argument as void because it's implicitly cast to void* by CIL for memset. Considering how stupidly the type-partitioning fails, I have serious doubts about fixing it.
  3. Implement memset handling in base analysis to write a zero value of the corresponding type if memset argument is 0 (closes Zero-initialization using memset #691).
  4. Together with the previous, the special handling in other cases (non-zero argument), only writes top values to direct addresses, not all indirect ones via reachability (analogously to access analysis). Therefore it should also improve memset precision on non-zero arguments as well by avoiding all reachable invalidation.

TODO

@sim642
Copy link
Member Author

sim642 commented Apr 25, 2022

On top of #695 (comment), this doesn't seem to help much either:

 Summary for all memory locations:
-	safe:         2001
-	vulnerable:    181
-	unsafe:        863
-	-------------------
-	total:        3045
+	safe:         1736
+	vulnerable:    68
+	unsafe:        870
+	-------------------
+	total:        2674

Also, this seemed to increase the analysis time from ~40min to ~48min.

Still, the memset related write accesses are gone though, but the unknown function pointer call ones remain and are a frequent cause for races.

@michael-schwarz michael-schwarz self-requested a review April 26, 2022 14:34
…access partitioning

That partitioning was unsound for alloc variables (with void type in some cases), so had to be disabled to trade precision for soundness.
@sim642 sim642 merged commit 6b907fa into master Apr 27, 2022
@sim642 sim642 deleted the memset branch April 27, 2022 06:34
sim642 added a commit that referenced this pull request Apr 27, 2022
sim642 added a commit that referenced this pull request Apr 27, 2022
Should fix 04-mutex/70-memset_indirect_nr on MacOS CI.
sim642 added a commit that referenced this pull request Apr 27, 2022
Should fix 01-cpa/24-library_functions on MacOS CI.
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Zero-initialization using memset
2 participants