From 5f2798ea25521dc74b3d8c0cbe495f03832259d5 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 10 Jul 2024 11:23:14 -0500 Subject: [PATCH 1/2] Add a challenge for `linked_list` (#30) > Please add a description of your PR. > If this is a solution to an open challenge, please explain your solution. > > Don't forget to check our book to ensure your solution satisfy the overall > requirements as well as the challenge success criteria. > By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0005-linked-list.md | 50 ++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 doc/src/challenges/0005-linked-list.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 992ca46a7c818..21713571824ce 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -16,3 +16,4 @@ - [Core Transmutation](./challenges/0001-core-transmutation.md) - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) + - [Inductive data type](./challenges/0005-linked-list.md) diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md new file mode 100644 index 0000000000000..5701acb7b82d2 --- /dev/null +++ b/doc/src/challenges/0005-linked-list.md @@ -0,0 +1,50 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *24/07/01* +- **End date:** *24/12/10* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate the its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clearn | alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### 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. From bbfbb19c4a4ade172b0a165eb56c262670c3b031 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Wed, 10 Jul 2024 12:37:20 -0400 Subject: [PATCH 2/2] Add PR approval check for specific directories (#31) Adds process/CI workflow to check that the approvers for every PR are in a committee of recognized approvers. This is a much simplified version of the r?bot that rust-lang uses. ## Testing Scenarios ### Happy path What happens when 2 of the approvers are in the committee Run: https://github.com/jaisnan/rust-dev/pull/16/checks?check_run_id=26914353663 ## What if someone not in the list approves, and 1 from the committee approves? In this scenario, we have a committee that consists of someone called "jaisu-1". But if the approvals came from one ID that's recognized, and another called "Jaisu-1" (Note to the reader: "jaisu-1" != "Jaisu-1"), then the workflow fails and the PR merge is (rightfully) blocked. Run: https://github.com/jaisnan/rust-dev/pull/15/checks?check_run_id=26914179444 ## Call-Outs 1. We need to add a requirement through settings that at least 2 approvers are required before merging, and allow anyone to approve (if it's not already the setting). 2. Once the first iteration of a committee is finalized, we can merge this workflow to begin the approval checking. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/workflows/pr_approval.yml | 156 ++++++++++++++++++++++++++++++ 1 file changed, 156 insertions(+) create mode 100644 .github/workflows/pr_approval.yml diff --git a/.github/workflows/pr_approval.yml b/.github/workflows/pr_approval.yml new file mode 100644 index 0000000000000..316be83fc0e62 --- /dev/null +++ b/.github/workflows/pr_approval.yml @@ -0,0 +1,156 @@ +name: Check PR Approvals + +# For now, the workflow gets triggered only when a review is submitted +# This technically means, a PR with zero approvals can be merged by the rules of this workflow alone +# To protect against that scenario, we can turn on number of approvals required to 2 in the github settings +# of the repository +on: + pull_request_review: + types: [submitted] + workflow_dispatch: + +jobs: + check-approvals: + if: github.event.review.state == 'APPROVED' || github.event_name == 'workflow_dispatch' + runs-on: ubuntu-latest + steps: + - name: Checkout repository + uses: actions/checkout@v2 + + - name: Install TOML parser + run: npm install @iarna/toml + + - name: Check PR Relevance and Approvals + uses: actions/github-script@v6 + with: + script: | + const fs = require('fs'); + const toml = require('@iarna/toml'); + const { owner, repo } = context.repo; + let pull_number; + + if (github.event_name === 'workflow_dispatch') { + const branch = github.ref.replace('refs/heads/', ''); + const prs = await github.rest.pulls.list({ + owner, + repo, + head: `${owner}:${branch}`, + state: 'open' + }); + if (prs.data.length === 0) { + console.log('No open PR found for this branch.'); + return; + } + pull_number = prs.data[0].number; + } else { + pull_number = context.issue.number; + } + + // Get PR files + const files = await github.rest.pulls.listFiles({ + owner, + repo, + pull_number + }); + + const relevantPaths = ['library/', 'doc/src/challenges/']; + const isRelevantPR = files.data.some(file => + relevantPaths.some(path => file.filename.startsWith(path)) + ); + + if (!isRelevantPR) { + console.log('PR does not touch relevant paths. Exiting workflow.'); + return; + } + + // Get parsed data + try { + const tomlContent = fs.readFileSync('.github/pull_requests.toml', 'utf8'); + console.log('TOML content:', tomlContent); + const tomlData = toml.parse(tomlContent); + console.log('Parsed TOML data:', JSON.stringify(tomlData, null, 2)); + + if (!tomlData.committee || !Array.isArray(tomlData.committee.members)) { + throw new Error('committee.members is not an array in the TOML file'); + } + requiredApprovers = tomlData.committee.members; + } catch (error) { + console.error('Error reading or parsing TOML file:', error); + core.setFailed('Failed to read required approvers list'); + return; + } + + // Get all reviews + const reviews = await github.rest.pulls.listReviews({ + owner, + repo, + pull_number + }); + + // Example: approvers = ["celina", "zyad"] + const approvers = new Set( + reviews.data + .filter(review => review.state === 'APPROVED') + .map(review => review.user.login) + ); + + const requiredApprovals = 2; + const requiredApproversCount = Array.from(approvers) + .filter(approver => requiredApprovers.includes(approver)) + .length; + + // TODO: Improve logging and messaging to the user + console.log('PR Approvers:', Array.from(approvers)); + console.log('Required Approvers:', requiredApproversCount); + + // Core logic that checks if the approvers are in the committee + const checkName = 'PR Approval Status'; + const conclusion = (approvers.size >= requiredApprovals && requiredApproversCount >= 2) ? 'success' : 'failure'; + const output = { + title: checkName, + summary: `PR has ${approvers.size} total approvals and ${requiredApproversCount} required approvals.`, + text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}` + }; + + // Get PR details + const pr = await github.rest.pulls.get({ + owner, + repo, + pull_number + }); + + // Create or update check run + const checkRuns = await github.rest.checks.listForRef({ + owner, + repo, + ref: pr.data.head.sha, + check_name: checkName + }); + + // Reuse the same workflow everytime there's a new review submitted + // instead of creating new workflows. Better efficiency and readability + // as the number of workflows is kept to a minimal number + if (checkRuns.data.total_count > 0) { + await github.rest.checks.update({ + owner, + repo, + check_run_id: checkRuns.data.check_runs[0].id, + status: 'completed', + conclusion, + output + }); + } else { + await github.rest.checks.create({ + owner, + repo, + name: checkName, + head_sha: pr.data.head.sha, + status: 'completed', + conclusion, + output + }); + } + + if (conclusion === 'failure') { + core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApproversCount}`); + }