Merge branch 'main' into core_arch_x86-arbitrary

Author: tautschnig

.github/workflows/kani-metrics.yml

@@ -28,7 +28,9 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
+      run: |
+        ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
+        rm kani-list.json
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7

.github/workflows/kani.yml

@@ -55,7 +55,7 @@ jobs:
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
-  kani-autoharness:
+  kani_autoharness:
     name: Verify std library using autoharness
     runs-on: ${{ matrix.os }}
     strategy:
@@ -83,11 +83,17 @@ jobs:
       # explicitly list all functions (or prefixes thereof) the proofs of which
       # are known to pass.
       # Notes:
+      # - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
+      #   as whitespace is not supported, cf.
+      #   https://github.com/model-checking/kani/issues/4046
       # - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
       #   core_arch::x86:: functions that are known to verify successfully.
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern ">::disjoint_bitor" \
+            --include-pattern ">::unchecked_disjoint_bitor" \
+            --include-pattern alloc::__default_lib_allocator:: \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
@@ -132,7 +138,121 @@ jobs:
             --exclude-pattern ::precondition_check \
             --harness-timeout 10m \
             --default-unwind 1000 \
-            --jobs=3 --output-format=terse
+            --jobs=3 --output-format=terse | tee autoharness-verification.log
+          gzip autoharness-verification.log
+
+      - name: Upload Autoharness Verification Log
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-autoharness-verification.log.gz
+          path: autoharness-verification.log.gz
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+  run_kani_metrics:
+    name: Kani Metrics
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: true
+
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.x'
+
+      # Step 2: Run list on the std library
+      - name: Run Kani Metrics
+        run: |
+          scripts/run-kani.sh --run metrics --with-autoharness
+          pushd /tmp/std_lib_analysis
+          tar czf results.tar.gz results
+          popd
+
+      - name: Upload kani-list.json
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-kani-list.json
+          path: kani-list.json
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+      - name: Upload scanner results
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.tar.gz
+          path: /tmp/std_lib_analysis/results.tar.gz
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+  run-log-analysis:
+    name: Build JSON from logs
+    needs: [run_kani_metrics, kani_autoharness]
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: false
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: false
+
+      - name: Download log
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-autoharness-verification.log.gz
+
+      - name: Download kani-list.json
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-kani-list.json
+
+      - name: Download scanner results
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.tar.gz
+
+      - name: Run log parser
+        run: |
+          gunzip autoharness-verification.log.gz
+          tar xzf results.tar.gz
+          python3 scripts/kani-std-analysis/log_parser.py \
+            --kani-list-file kani-list.json \
+            --analysis-results-dir results/ \
+            autoharness-verification.log \
+            -o results.json
+
+      - name: Upload JSON
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.json
+          path: results.json
+          if-no-files-found: error
 
   run-kani-list:
     name: Kani List
@@ -188,12 +308,14 @@ jobs:
       # Step 3: Add output to job summary
       - name: Add Autoharness Analyzer output to job summary
         run: |
+          pushd scripts/autoharness_analyzer
           echo "# Autoharness Failure Summary" >> "$GITHUB_STEP_SUMMARY"
           echo "## Crate core, all functions" >> "$GITHUB_STEP_SUMMARY"
-          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          cat core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
           echo "## Crate core, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
-          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          cat core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
           echo "## Crate std, all functions" >> "$GITHUB_STEP_SUMMARY"
-          cat autoharness_analyzer/std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          cat std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
           echo "## Crate std, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
-          cat autoharness_analyzer/std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          cat std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          popd

.gitignore

@@ -22,6 +22,7 @@ Session.vim
 /kani_build/
 /target
 library/target
+scripts/autoharness_analyzer/target/
 *.rlib
 *.rmeta
 *.mir

doc/mdbook-metrics/Cargo.toml

@@ -5,4 +5,5 @@ edition = "2021"
 
 [dependencies]
 mdbook = { version = "^0.4" }
+mdbook-linkcheck = "0.7.7"
 serde_json = "1.0.132"

doc/src/SUMMARY.md

@@ -32,3 +32,8 @@
   - [16: Verify the safety of Iterator functions](./challenges/0016-iter.md)
   - [17: Verify the safety of slice functions](./challenges/0017-slice.md)
   - [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter.md)
+  - [19: Safety of `RawVec`](./challenges/0019-rawvec.md)
+  - [20: Verify the safety of char-related functions in str::pattern](./challenges/0020-str-pattern-pt1.md)
+  - [21: Verify the safety of substring-related functions in str::pattern](./challenges/0021-str-pattern-pt2.md)
+  - [22: Verify the safety of str iter functions](./challenges/0022-str-iter.md)
+  - [25: Verify the safety of `VecDeque` functions](./challenges/0025-vecdeque.md)

doc/src/challenges/0007-atomic-types.md

@@ -87,14 +87,18 @@ Write and verify safety contracts for the unsafe functions:
 - `atomic_umax`
 - `atomic_umin`
 
+##### Panicking (Optional)
 Then, for each of the safe abstractions that invoke the unsafe functions listed above, write contracts that ensure that they are not invoked with `order`s that would cause panics.
 
 For example, `atomic_store` panics if invoked with `Acquire` or `AcqRel` ordering.
 In this case, you would write contracts on the safe `store` methods that enforce that they are not called with either of those `order`s.
 
+This section is not required to complete the challenge, since panicking is not undefined behavior.
+However, it would be incorrect for someone to call these functions with the wrong arguments, so we encourage providing these specifications.
+
 #### Part 3: Atomic Intrinsics
 
-Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`):
+Write safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`):
 
 | Operations            |  Functions |
 |-----------------------|-------------|

doc/src/challenges/0019-rawvec.md

@@ -0,0 +1,67 @@
+# Challenge 25: Verify the safety of `RawVec` functions
+
+- **Status:** Open
+- **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283)
+- **Start date:** *2025-03-07*
+- **End date:** *2025-10-17*
+- **Reward:** *10000 USD*
+
+-------------------
+
+
+## Goal
+
+Verify the safety of `RawVec` functions in (library/alloc/src/raw_vec/mod.rs).
+
+## Motivation 
+
+`RawVec` is the type of the main component of both `Vec` and `VecDeque`: the buffer. Therefore, the safety of the functions of `Vec` and `VecDeque` depend on the safety of `RawVec`.
+
+### Success Criteria
+
+Verify the safety of the following functions in (library/alloc/src/raw_vec/mod.rs):
+
+Write and prove the contract for the safety of the following unsafe functions:
+
+| Function |
+|---------|
+|new_cap|
+|into_box|
+|from_raw_parts_in|
+|from_nonnull_in|
+|set_ptr_and_cap|
+|shrink_unchecked|
+|deallocate|
+
+Prove the absence of undefined behavior for following safe abstractions:
+
+| Function |
+|---------|
+|drop|
+|new_in|
+|with_capacity_in|
+|try_allocate_in|
+|current_memory|
+|try_reserve|
+|try_reserve_exact|
+|grow_amortized|
+|grow_exact|
+|shrink|
+|finish_grow|
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must hold for generic type `T` (no monomorphization).
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory except for padding or unions.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

doc/src/challenges/0020-str-pattern-pt1.md

@@ -0,0 +1,103 @@
+# Challenge 20: Verify the safety of char-related functions in str::pattern
+
+- **Status:** Open
+- **Tracking Issue:** [#277](https://github.com/model-checking/verify-rust-std/issues/277)
+- **Start date:** *2025-03-07*
+- **End date:** *2025-10-17*
+- **Reward:** *25000 USD*
+
+-------------------
+## Goal
+Verify the safety of char-related `Searcher` methods in `str::pattern`.
+
+## Motivation
+
+String and `str` types are widely used in Rust programs, so it is important that their associated functions do not cause undefined behavior.
+
+## Description
+
+The following str library functions are generic over the `Pattern` trait (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html): 
+- `contains`
+- `starts_with`
+- `ends_with`
+- `find` 
+- `rfind`
+- `split`
+- `split_inclusive`
+- `rsplit`
+- `split_terminator`
+- `rsplit_terminator`
+- `splitn`
+- `rsplitn`
+- `split_once`
+- `rsplit_once`
+- `rmatches`
+- `match_indices`
+- `rmatch_indices`
+- `trim_matches`
+- `trim_start_matches`
+- `strip_prefix`
+- `strip_suffix`
+- `trim_end_matches`
+These functions accept a pattern as input, then call [into_searcher](https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html#tymethod.into_searcher) to create a [Searcher](https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html#associatedtype.Searcher) for the pattern. They use this `Searcher` to perform their desired operations (split, find, etc.).
+Those functions are implemented in (library/core/src/str/mod.rs), but the core of them are the searching algorithms which are implemented in (library/core/src/str/pattern.rs).
+
+### Assumptions
+
+**Important note:** for this challenge, you can assume: 
+1. The safety and functional correctness of all functions in `slice` module.
+2. That all functions in (library/core/src/str/validations.rs) are functionally correct (consistent with the UTF-8 encoding description in https://en.wikipedia.org/wiki/UTF-8). 
+3. That all the Searchers in (library/core/src/str/iter.rs) are created by the into_searcher(_, haystack) with haystack being a valid UTF-8 string (str). You can assume any UTF-8 string property of haystack.
+
+Verify the safety of the functions in (library/core/src/str/pattern.rs) listed in the next section.
+
+The safety properties we are targeting are: 
+1. No undefined behavior occurs after the Searcher is created.
+2. The impls of unsafe traits `Searcher` and `ReverseSearcher` satisfy the SAFETY condition stated in the file: 
+```
+/// The trait is marked unsafe because the indices returned by the
+/// [`next()`][Searcher::next] methods are required to lie on valid utf8
+/// boundaries in the haystack. This enables consumers of this trait to
+/// slice the haystack without additional runtime checks.
+```
+This property should hold for next_back() of `ReverseSearcher` too.
+
+
+### Success Criteria
+
+Verify the safety of the following functions in (library/core/src/str/pattern.rs) : 
+- `next`
+- `next_match`
+- `next_back`
+- `next_match_back`
+- `next_reject`
+- `next_back_reject`
+for the following `Searcher`s: 
+- `CharSearcher`
+- `MultiCharEqSearcher`
+- `CharArraySearcher`
+- `CharArrayRefSearcher`
+- `CharSliceSearcher`
+- `CharPredicateSearcher`
+
+The verification is considered successful if for each `Searcher` above, you can specify a condition (a "type invariant") `C` and prove that:
+1. If the `Searcher` is created from any valid UTF-8 haystack, it satisfies `C`.
+2. If the `Searcher` satisfies `C`, it ensures the two safety properties mentioned in the previous section.
+3. If the `Searcher` satisfies `C`, after it calls any function above and gets modified, it still satisfies `C`.
+
+Furthermore, you must prove the absence of undefined behaviors listed in the next section.
+
+The verification must be unbounded---it must hold for inputs of arbitrary size.
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory except for padding or unions.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.