From 7031b9314de7313c4067aedaa7eff094b37c0106 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 10 Dec 2024 15:54:15 -0500 Subject: [PATCH 1/5] Improve PR approval script logging (#219) Improve the logging in our PR approvals workflow. This is a good thing to do generally, but we're specifically trying to debug why the script is failing in #107. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Michael Tautschnig --- .github/workflows/pr_approval.yml | 32 ++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/.github/workflows/pr_approval.yml b/.github/workflows/pr_approval.yml index 06dbb1599d93f..3094f4b6baf66 100644 --- a/.github/workflows/pr_approval.yml +++ b/.github/workflows/pr_approval.yml @@ -52,8 +52,11 @@ jobs: pull_number = context.issue.number; } + console.log(`owner is ${owner}`); + console.log(`pull_number is ${pull_number}`); // Get parsed data + let requiredApprovers; try { const tomlContent = fs.readFileSync('.github/pull_requests.toml', 'utf8'); console.log('TOML content:', tomlContent); @@ -85,23 +88,22 @@ jobs: ); const requiredApprovals = 2; - const currentCountfromCommittee = 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:', requiredApprovals); + 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 checkName = 'PR Approval Status'; - const conclusion = (approvers.size >= requiredApprovals && currentCountfromCommittee >= 2) ? 'success' : 'failure'; - const output = { - title: checkName, - summary: `PR has ${approvers.size} total approvals and ${requiredApprovals} required approvals.`, - text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}` - }; + const conclusion = (currentCountfromCommittee >= 2) ? 'success' : 'failure'; + console.log('PR Approval Status'); + 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 at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`); + core.setFailed(`PR needs 2 approvals from committee members, but it has ${currentCountfromCommittee}`); + } else { + core.info('PR approval check passed successfully.'); } From 19eaf6adcb11fb89e1d3297e6c6fdf717a24321c Mon Sep 17 00:00:00 2001 From: Reinier Maas Date: Tue, 10 Dec 2024 21:54:36 +0100 Subject: [PATCH 2/5] Update 0005-linked-list.md (#216) Fixing typos. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig --- doc/src/challenges/0005-linked-list.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index b10d6e743cf14..3bfcb87cc73a3 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -11,7 +11,7 @@ ## 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. +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 over its internal inductive-defined data type. ### Details From bc9c9f9765d0c23761ffbc8c29e96a765d06f900 Mon Sep 17 00:00:00 2001 From: Reinier Maas Date: Tue, 10 Dec 2024 21:55:53 +0100 Subject: [PATCH 3/5] Update 0002-intrinsics-memory.md (#208) Fixing some typos. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Carolyn Zech --- doc/src/challenges/0002-intrinsics-memory.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index adb4176254804..933d76b808190 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -1,4 +1,4 @@ -# Challenge 2: Verify the memory safery of core intrinsics using raw pointers +# Challenge 2: Verify the memory safety of core intrinsics using raw pointers - **Status:** Open - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16) From cb94f9cf82b66c9a3f3ae214a3f4efe3e37d804e Mon Sep 17 00:00:00 2001 From: Reinier Maas Date: Tue, 10 Dec 2024 21:56:02 +0100 Subject: [PATCH 4/5] Update 0002-intrinsics-memory.md (#209) Fixing typos. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Carolyn Zech --- doc/src/challenges/0002-intrinsics-memory.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index 933d76b808190..23aef0d36f50a 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -61,7 +61,7 @@ All the following usages of intrinsics were proven safe: -Annotate and verify all the functions that below that expose intrinsics with safety contracts +Annotate and verify all the functions below that expose intrinsics with safety contracts | Function | Location | |---------|---------| From 002c7c036805f06e45c7a73f53db5e7981738ec2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 Dec 2024 21:56:15 +0100 Subject: [PATCH 5/5] Cleanup stray comment (#218) With https://github.com/model-checking/kani/issues/3670 having been addressed we re-enabled harnesses in #211. Yet the comment explaining previously-commented-out-harnesses stayed in place. Removing it for it no longer applies. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/slice/iter.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 5ea9204a28fd0..fcf901e3c9f43 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3607,10 +3607,6 @@ mod verify { check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); - // FIXME: The functions that are commented out are currently failing verification. - // Debugging the issue is currently blocked by: - // https://github.com/model-checking/kani/issues/3670 - // // Public functions that call safe abstraction `make_slice`. check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| { iter.as_slice();