Merge remote-tracking branch 'origin/main' into from_mut_unchecked

Author: tautschnig

.github/workflows/kani-metrics.yml

@@ -14,6 +14,13 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
+    - name: Remove unnecessary software to free up disk space
+      run: |
+        # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+        df -h
+        sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+        df -h
+
     - name: Checkout Repository
       uses: actions/checkout@v4
       with:
@@ -26,7 +33,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

@@ -37,6 +37,14 @@ jobs:
       WORKER_TOTAL: 4
 
     steps:
+      - name: Remove unnecessary software to free up disk space
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
@@ -53,7 +61,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:
@@ -67,6 +75,14 @@ jobs:
       fail-fast: false
 
     steps:
+      - name: Remove unnecessary software to free up disk space
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
@@ -78,9 +94,16 @@ jobs:
       # possible functions as that may take a lot longer than expected. Instead,
       # 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
       - 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 \
@@ -122,14 +145,143 @@ jobs:
             --exclude-pattern time::Duration::from_secs_f \
             --include-pattern unicode::unicode_data::conversions::to_ \
             --exclude-pattern ::precondition_check \
-            --harness-timeout 5m \
+            --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:
+      - name: Remove unnecessary software to free up disk space
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
+      # 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
     runs-on: ubuntu-latest
     steps:
+      - name: Remove unnecessary software to free up disk space
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
@@ -176,12 +328,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

.github/workflows/pr_approval.yml

@@ -73,6 +73,21 @@ jobs:
               return;
             }
 
+            // Get the list of changed files
+            const { data: changedFiles } = await github.rest.pulls.listFiles({
+              owner,
+              repo,
+              pull_number,
+            });
+
+            // Check if any files in doc/, library/ or verifast-proofs/ are modified
+            const affectsDocs = changedFiles.some(file => file.filename.startsWith('doc/'));
+            const affectsLibrary = changedFiles.some(file => file.filename.startsWith('library/'));
+            const affectsVerifast = changedFiles.some(file => file.filename.startsWith('verifast-proofs/'));
+            // Require two approvals iff one of the above folders are modified; otherwise, one is sufficient.
+            const requiresTwoApprovals = affectsDocs || affectsLibrary || affectsVerifast;
+            const requiredApprovals = requiresTwoApprovals ? 2 : 1;
+
             // Get all reviews with pagination
             async function getAllReviews() {
               let allReviews = [];
@@ -113,23 +128,27 @@ jobs:
                 .map(review => review.user.login)
             );
 
-            const requiredApprovals = 2;
             const committeeApprovers = Array.from(approvers)
               .filter(approver => requiredApprovers.includes(approver));
             const currentCountfromCommittee = committeeApprovers.length;
 
-            // Core logic that checks if the approvers are in the committee
-            const conclusion = (currentCountfromCommittee >= 2) ? 'success' : 'failure';
+            // Check if we have enough approvals
+            const conclusion = (currentCountfromCommittee >= requiredApprovals) ? 'success' : 'failure';
 
             console.log('PR Approval Status');
+            console.log('Modified folders:');
+            console.log(`- doc/: ${affectsDocs ? 'yes' : 'no'}`);
+            console.log(`- library/: ${affectsLibrary ? 'yes' : 'no'}`);
+            console.log(`- verifast-proofs/: ${affectsVerifast ? 'yes' : 'no'}`);
+            console.log(`Required approvals from committee: ${requiredApprovals}`);
             console.log(`PR has ${approvers.size} total approvals and ${currentCountfromCommittee} required approvals from the committee.`);
             
             console.log(`Committee Members: [${requiredApprovers.join(', ')}]`);
             console.log(`Committee Approvers: ${committeeApprovers.length === 0 ? 'NONE' : `[${committeeApprovers.join(', ')}]`}`);
             console.log(`All Approvers: ${approvers.size === 0 ? 'NONE' : `[${Array.from(approvers).join(', ')}]`}`);
             
             if (conclusion === 'failure') {
-              core.setFailed(`PR needs 2 approvals from committee members, but it has ${currentCountfromCommittee}`);
+              core.setFailed(`PR needs ${requiredApprovals} approval${requiredApprovals > 1 ? 's' : ''} from committee members, but it has ${currentCountfromCommittee}`);
             } else {
               core.info('PR approval check passed successfully.');
             }

.github/workflows/update-subtree.yml

@@ -11,6 +11,7 @@ defaults:
 
 jobs:
   update-subtree-library:
+    if: github.repository == 'model-checking/verify-rust-std'
     # Changing the host platform may alter the libgit2 version as used by
     # splitsh-lite, which will require changing the version of git2go.
     # See https://github.com/jeffWelling/git2go?tab=readme-ov-file#which-go-version-to-use
@@ -85,6 +86,7 @@ jobs:
       if: ${{ env.SUBTREE_PR_EXISTS == 'no' }}
       run: |
         cd splitsh-lite
+        sudo apt-get update
         sudo apt-get install -y golang libgit2-dev
         # git2go upstream hasn't been updated to more recent versions of
         # libgit2, so using a fork that does stay up to date
@@ -110,6 +112,10 @@ jobs:
         fi
 
         git checkout ${NEXT_COMMIT_HASH}
+        # Collect submodule commits; note that submodules (intentionally!)
+        # aren't initialized, hence lines will be prefixed with "-" (see git
+        # submodule --help).
+        git submodule status  -- library/ | sed 's/^-//' > ../submodule-heads
         /usr/bin/time -v ../splitsh-lite/splitsh-lite --progress --prefix=library --target subtree/library
         git checkout -b subtree/library subtree/library
 
@@ -165,6 +171,7 @@ jobs:
           fi
         fi
         git checkout main
+        git submodule foreach 'git fetch'
 
         # Tell git about the correct merge base to use, which is the subtree
         # head that we last merged from.
@@ -178,6 +185,8 @@ jobs:
             -c user.name=gitbot -c user.email=git@bot \
             merge -Xsubtree=library subtree/library; then
           echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV
+          # Ignore submodule conflicts, those are dealt with below.
+          for d in $(cat ../submodule-heads | cut -f2 -d" ") ; do git reset HEAD $d ; done
           git -c user.name=gitbot -c user.email=git@bot commit -a -m "Merge from $NEXT_COMMIT_HASH with conflicts"
         else
           echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV
@@ -187,6 +196,14 @@ jobs:
         NEW_SUBTREE_HEAD=$(git rev-parse subtree/library)
         echo "NEW_SUBTREE_HEAD=${NEW_SUBTREE_HEAD}" >> $GITHUB_ENV
 
+        # Set submodules to upstream versions
+        git submodule update --init
+        git submodule foreach 'grep $sm_path $toplevel/../submodule-heads | cut -f1 -d" " | xargs git checkout'
+        if ! git diff --quiet; then
+          git -c user.name=gitbot -c user.email=git@bot \
+            commit -m "Update submodules" library/
+        fi
+
         sed -i "s/^channel = \"nightly-.*\"/channel = \"nightly-${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update toolchain to ${NEXT_TOOLCHAIN_DATE}" rust-toolchain.toml
@@ -195,6 +212,22 @@ jobs:
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update Kani version to ${KANI_COMMIT_HASH}" tool_config/kani-version.toml
 
+        # Try to automatically patch the VeriFast proofs
+        pushd verifast-proofs
+        if bash ./patch-verifast-proofs.sh; then
+          if ! git diff --quiet; then
+            git -c user.name=gitbot -c user.email=git@bot \
+              commit . -m "Update VeriFast proofs"
+          else
+            # The original files have not changed; no updates to the VeriFast proofs are necessary.
+            true
+          fi
+        else
+          # Patching the VeriFast proofs failed; requires manual intervention.
+          true
+        fi
+        popd
+
     - name: Create Pull Request without conflicts
       if: ${{ env.MERGE_CONFLICTS == 'no' && env.MERGE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7

.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"