Merge branch 'model-checking:main' into morechallenges

model-checking · Feb 28, 2025 · 7437d1e · 7437d1e
2 parents 4a3a0e6 + eef04d8
commit 7437d1e
Show file tree

Hide file tree

Showing 23 changed files with 9,940 additions and 0 deletions.
diff --git a/.github/workflows/update-subtree.yml b/.github/workflows/update-subtree.yml
@@ -0,0 +1,155 @@
+name: Subtree Update
+
+on:
+  schedule:
+    - cron: '0 14 * * *'  # Run at 14:00 UTC every day
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  update-subtree-library:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout Repository
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        path: verify-rust-std
+        submodules: true
+
+    - name: Checkout Kani
+      uses: actions/checkout@v4
+      with:
+        repository: model-checking/kani
+        path: kani-tmp
+
+    - name: Checkout Rust
+      uses: actions/checkout@v4
+      with:
+        repository: rust-lang/rust
+        fetch-depth: 0
+        path: rust-tmp
+
+    - name: Checkout git-filter-repo
+      uses: actions/checkout@v4
+      with:
+        repository: newren/git-filter-repo
+        path: git-filter-repo
+
+    - name: Fetch toolchain versions
+      run: |
+        CURRENT_TOOLCHAIN_DATE=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' verify-rust-std/rust-toolchain.toml)
+        NEXT_TOOLCHAIN_DATE=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' kani-tmp/rust-toolchain.toml)
+        CURRENT_COMMIT_HASH=$(curl https://static.rust-lang.org/dist/$CURRENT_TOOLCHAIN_DATE/channel-rust-nightly-git-commit-hash.txt)
+        NEXT_COMMIT_HASH=$(curl https://static.rust-lang.org/dist/$NEXT_TOOLCHAIN_DATE/channel-rust-nightly-git-commit-hash.txt)
+        if [ -z "$CURRENT_COMMIT_HASH" ]; then
+          echo "Could not find current commit hash on static.rust-lang.org"
+          exit 1
+        fi
+        if [ -z "$NEXT_COMMIT_HASH" ]; then
+          echo "Could not find next commit hash on static.rust-lang.org"
+          exit 1
+        fi
+        echo "CURRENT_TOOLCHAIN_DATE=${CURRENT_TOOLCHAIN_DATE}" >> $GITHUB_ENV
+        echo "NEXT_TOOLCHAIN_DATE=${NEXT_TOOLCHAIN_DATE}" >> $GITHUB_ENV
+        echo "CURRENT_COMMIT_HASH=${CURRENT_COMMIT_HASH}" >> $GITHUB_ENV
+        echo "NEXT_COMMIT_HASH=${NEXT_COMMIT_HASH}" >> $GITHUB_ENV
+
+    - name: Update subtree/library locally
+      run: |
+        cd rust-tmp
+
+        # Ensure "upstream/master" branch contains the target commit
+        if ! git show ${NEXT_COMMIT_HASH} --oneline --no-patch; then
+          echo "Rust commit ${NEXT_COMMIT_HASH} cannot be found."
+          exit 1
+        fi
+
+        git checkout ${NEXT_COMMIT_HASH}
+        ../git-filter-repo/git-filter-repo --subdirectory-filter library --force
+        git checkout -b subtree/library
+
+        cd ../verify-rust-std
+        git remote add rust-filtered ../rust-tmp/
+        git fetch rust-filtered
+        git checkout -b subtree/library rust-filtered/subtree/library
+        SUBTREE_HEAD_MSG=$(git log --format=%s -n 1 origin/subtree/library)
+        UPSTREAM_FROM=$(git log --grep="${SUBTREE_HEAD_MSG}" -n 1 --format=%H rust-filtered/subtree/library)
+        UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)
+        if [ "${UPSTREAM_HEAD}" = "${UPSTREAM_FROM}" ]; then
+          echo "Nothing to do, ${UPSTREAM_FROM} matches ${UPSTREAM_HEAD} (${SUBTREE_HEAD_MSG})"
+          echo "MERGE_CONFLICTS=noop" >> $GITHUB_ENV
+        else
+          git branch --set-upstream-to=origin/subtree/library
+          git -c user.name=gitbot -c user.email=git@bot rebase
+          echo "MERGE_CONFLICTS=maybe" >> $GITHUB_ENV
+        fi
+
+    - name: Create Pull Request
+      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: 'Update subtree/library to ${{ env.NEXT_TOOLCHAIN_DATE }}'
+        body: |
+          This is an automated PR to update the subtree/library branch to the changes
+          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
+          to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
+        branch: update-subtree/library
+        delete-branch: true
+        base: subtree/library
+        path: verify-rust-std
+
+    - name: Merge subtree/library changes
+      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+      run: |
+        cd verify-rust-std
+        git checkout main
+
+        # This command may fail, which will require human intervention.
+        if ! git \
+            -c user.name=gitbot -c user.email=git@bot \
+            subtree merge --prefix=library update-subtree/library --squash; then
+          echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV
+          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
+        fi
+
+        sed -i "s/^channel = \"nightly-.*\"/channel = \"${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
+
+    - name: Create Pull Request without conflicts
+      if: ${{ env.MERGE_CONFLICTS == 'no' }}
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
+        body: |
+          This is an automated PR to merge library subtree updates
+          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
+          to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
+          This is a clean merge, no conflicts were detected.
+        branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
+        delete-branch: true
+        base: main
+        path: verify-rust-std
+
+    - name: Create Pull Request with conflicts
+      if: ${{ env.MERGE_CONFLICTS == 'yes' }}
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
+        body: |
+          This is an automated PR to merge library subtree updates
+          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
+          to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}) (inclusive)
+          into main. `git merge` resulted in conflicts, which require manual resolution.
+          Files were commited with merge conflict markers.
+        branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
+        delete-branch: true
+        base: main
+        path: verify-rust-std
diff --git a/.github/workflows/verifast-negative.yml b/.github/workflows/verifast-negative.yml
@@ -0,0 +1,45 @@
+# This workflow runs some negative VeriFast test cases, to ensure
+# that VeriFast actually catches bugs.
+
+name: VeriFast (negative)
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/verifast.yml'
+      - 'verifast-proofs/**'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  check-verifast-on-std:
+    name: Verify std library
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+
+      - name: Install VeriFast
+        run: |
+          cd ~
+          curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/4911733
+          echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8  verifast-25.02-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.02-linux.tar.gz
+
+      - name: Install the Rust toolchain used by VeriFast
+        run: rustup toolchain install nightly-2024-11-23
+
+      - name: Run VeriFast Verification
+        run: |
+          export PATH=~/verifast-25.02/bin:$PATH
+          cd verifast-proofs
+          mysh check-verifast-proofs-negative.mysh
diff --git a/.github/workflows/verifast.yml b/.github/workflows/verifast.yml
@@ -0,0 +1,42 @@
+name: VeriFast
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/verifast.yml'
+      - 'verifast-proofs/**'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  check-verifast-on-std:
+    name: Verify std library
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+
+      - name: Install VeriFast
+        run: |
+          cd ~
+          curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/4911733
+          echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8  verifast-25.02-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.02-linux.tar.gz
+
+      - name: Install the Rust toolchain used by VeriFast
+        run: rustup toolchain install nightly-2024-11-23
+
+      - name: Run VeriFast Verification
+        run: |
+          export PATH=~/verifast-25.02/bin:$PATH
+          cd verifast-proofs
+          mysh check-verifast-proofs.mysh
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
@@ -9,6 +9,7 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
   - [GOTO Transcoder](./tools/goto-transcoder.md)
+  - [VeriFast](./tools/verifast.md)
 
 ---
 

diff --git a/doc/src/tools.md b/doc/src/tools.md
@@ -13,6 +13,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
 |---------------------|-------|
  | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |
  | GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml)      |
+ | VeriFast for Rust   | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml)      |