Merge pull request #272 from moka-rs/fix-overflow-in-freq-sketch

Fix occasional panic in `FrequencySketch` in debug build

.github/workflows/Kani.yml

@@ -0,0 +1,33 @@
+name: Kani CI
+
+on:
+  pull_request:
+    paths-ignore:
+      - '.devcontainer/**'
+      - '.gitpod.yml'
+      - '.vscode/**'
+      - CHANGELOG.md
+      - README.md
+  push:
+    paths-ignore:
+      - '.devcontainer/**'
+      - '.gitpod.yml'
+      - '.vscode/**'
+      - CHANGELOG.md
+      - README.md
+
+jobs:
+  run-kani:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Moka
+        uses: actions/checkout@v3
+
+      - name: Show CPU into
+        run: |
+          nproc
+          lscpu
+          free -m
+
+      - name: Run Kani
+        uses: model-checking/kani-github-action@v0.28

CHANGELOG.md

@@ -2,6 +2,11 @@
 
 ## Version 0.11.1
 
+### Fixed
+
+-  Fixed occasional panic in internal `FrequencySketch` in debug build.
+   ([#272][gh-pull-0272])
+
 ### Added
 
 - Added some example programs to the `examples` directory. ([#268][gh-pull-0268], by
@@ -655,6 +660,7 @@ The minimum supported Rust version (MSRV) is now 1.51.0 (2021-03-25).
 [gh-issue-0034]: https://github.com/moka-rs/moka/issues/34/
 [gh-issue-0031]: https://github.com/moka-rs/moka/issues/31/
 
+[gh-pull-0272]: https://github.com/moka-rs/moka/pull/272/
 [gh-pull-0268]: https://github.com/moka-rs/moka/pull/268/
 [gh-pull-0259]: https://github.com/moka-rs/moka/pull/259/
 [gh-pull-0251]: https://github.com/moka-rs/moka/pull/251/

src/common/frequency_sketch.rs

@@ -180,7 +180,7 @@ impl FrequencySketch {
     fn index_of(&self, hash: u64, depth: u8) -> usize {
         let i = depth as usize;
         let mut hash = hash.wrapping_add(SEED[i]).wrapping_mul(SEED[i]);
-        hash += hash >> 32;
+        hash = hash.wrapping_add(hash >> 32);
         (hash & self.table_mask) as usize
     }
 
@@ -328,3 +328,73 @@ mod tests {
         }
     }
 }
+
+// Verify that some properties hold such as no panic occurs on any possible inputs.
+#[cfg(kani)]
+mod kani {
+    use super::FrequencySketch;
+
+    const CAPACITIES: &[u32] = &[
+        0,
+        1,
+        1024,
+        1025,
+        2u32.pow(24),
+        2u32.pow(24) + 1,
+        2u32.pow(30),
+        2u32.pow(30) + 1,
+        u32::MAX,
+    ];
+
+    #[kani::proof]
+    fn verify_ensure_capacity() {
+        // Check for arbitrary capacities.
+        let capacity = kani::any();
+        let mut sketch = FrequencySketch::default();
+        sketch.ensure_capacity(capacity);
+    }
+
+    #[kani::proof]
+    fn verify_frequency() {
+        // Check for some selected capacities.
+        for capacity in CAPACITIES {
+            let mut sketch = FrequencySketch::default();
+            sketch.ensure_capacity(*capacity);
+
+            // Check for arbitrary hashes.
+            let hash = kani::any();
+            let frequency = sketch.frequency(hash);
+            assert!(frequency <= 15);
+        }
+    }
+
+    #[kani::proof]
+    fn verify_increment() {
+        // Only check for small capacities. Because Kani Rust Verifier is a model
+        // checking tool, it will take much longer time (exponential) to check larger
+        // capacities here.
+        for capacity in &[0, 1, 128] {
+            let mut sketch = FrequencySketch::default();
+            sketch.ensure_capacity(*capacity);
+
+            // Check for arbitrary hashes.
+            let hash = kani::any();
+            sketch.increment(hash);
+        }
+    }
+
+    #[kani::proof]
+    fn verify_index_of() {
+        // Check for arbitrary capacities.
+        let capacity = kani::any();
+        let mut sketch = FrequencySketch::default();
+        sketch.ensure_capacity(capacity);
+
+        // Check for arbitrary hashes.
+        let hash = kani::any();
+        for i in 0..4 {
+            let index = sketch.index_of(hash, i);
+            assert!(index < sketch.table.len());
+        }
+    }
+}