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

Fix occasional panic in FrequencySketch in debug build #272

Merged
merged 4 commits into from
May 28, 2023

Conversation

tatsuya6502
Copy link
Member

@tatsuya6502 tatsuya6502 commented May 27, 2023

Fixes #267.
Fixes #113.

This PR prevents an internal index_of method of FrequencySketch from panicking by arithmetic overflow.

  • Only debug build was affected by this issue.
  • Release build was not affected unless overflow checks were explicitly enabled at the build time.

Changes

  • Replace an u64 addition (+) operator in FrequencySketch::index_of method with wrapping_add method.
    • Wrapping (modular) addition is the desired behavior for index_of method.
    • The + operator will behave the same to wrapping _add method in release build (where overflow checks are disabled).
  • Add test harnesses (test cases) for Kani Verifier to ensure there is no chance for arithmetic overflows and other panics to occur in FrequencySketch (not only for index_of method but also other methods).
    • Enable a CI job to run Kani test on every git pushes.

Verification

  • Ran cargo kani before fixing the issue, and arithmetic overflow was detected.
  • Ran cargo kani after fixing, and no issue was detected.

…ccurs

Using the harnesses, Kani Verifier should detect panics in
`FrequencySketch::index_of` method with some `u64` hash input.
…g build

- Replace `u64` `+` with `wrapping_add` to avoid overflow panic.
- Kani Verifier reports no panic in the `FrequencySketch::index_of` and other
  methods.
@tatsuya6502 tatsuya6502 self-assigned this May 27, 2023
@tatsuya6502 tatsuya6502 added the bug Something isn't working label May 27, 2023
@tatsuya6502 tatsuya6502 added this to the v0.11.1 milestone May 27, 2023
Copy link
Member Author

@tatsuya6502 tatsuya6502 left a comment

Choose a reason for hiding this comment

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

Merging.

@tatsuya6502 tatsuya6502 added this pull request to the merge queue May 28, 2023
Merged via the queue into master with commit a0d3342 May 28, 2023
@tatsuya6502 tatsuya6502 deleted the fix-overflow-in-freq-sketch branch May 28, 2023 04:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
1 participant