Skip to content

Commit e310ede

Browse files
authored
Merge branch 'main' into layout-contracts
2 parents 2e9f3f6 + bbfbb19 commit e310ede

File tree

3 files changed

+207
-0
lines changed

3 files changed

+207
-0
lines changed

.github/workflows/pr_approval.yml

+156
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
name: Check PR Approvals
2+
3+
# For now, the workflow gets triggered only when a review is submitted
4+
# This technically means, a PR with zero approvals can be merged by the rules of this workflow alone
5+
# To protect against that scenario, we can turn on number of approvals required to 2 in the github settings
6+
# of the repository
7+
on:
8+
pull_request_review:
9+
types: [submitted]
10+
workflow_dispatch:
11+
12+
jobs:
13+
check-approvals:
14+
if: github.event.review.state == 'APPROVED' || github.event_name == 'workflow_dispatch'
15+
runs-on: ubuntu-latest
16+
steps:
17+
- name: Checkout repository
18+
uses: actions/checkout@v2
19+
20+
- name: Install TOML parser
21+
run: npm install @iarna/toml
22+
23+
- name: Check PR Relevance and Approvals
24+
uses: actions/github-script@v6
25+
with:
26+
script: |
27+
const fs = require('fs');
28+
const toml = require('@iarna/toml');
29+
const { owner, repo } = context.repo;
30+
let pull_number;
31+
32+
if (github.event_name === 'workflow_dispatch') {
33+
const branch = github.ref.replace('refs/heads/', '');
34+
const prs = await github.rest.pulls.list({
35+
owner,
36+
repo,
37+
head: `${owner}:${branch}`,
38+
state: 'open'
39+
});
40+
if (prs.data.length === 0) {
41+
console.log('No open PR found for this branch.');
42+
return;
43+
}
44+
pull_number = prs.data[0].number;
45+
} else {
46+
pull_number = context.issue.number;
47+
}
48+
49+
// Get PR files
50+
const files = await github.rest.pulls.listFiles({
51+
owner,
52+
repo,
53+
pull_number
54+
});
55+
56+
const relevantPaths = ['library/', 'doc/src/challenges/'];
57+
const isRelevantPR = files.data.some(file =>
58+
relevantPaths.some(path => file.filename.startsWith(path))
59+
);
60+
61+
if (!isRelevantPR) {
62+
console.log('PR does not touch relevant paths. Exiting workflow.');
63+
return;
64+
}
65+
66+
// Get parsed data
67+
try {
68+
const tomlContent = fs.readFileSync('.github/pull_requests.toml', 'utf8');
69+
console.log('TOML content:', tomlContent);
70+
const tomlData = toml.parse(tomlContent);
71+
console.log('Parsed TOML data:', JSON.stringify(tomlData, null, 2));
72+
73+
if (!tomlData.committee || !Array.isArray(tomlData.committee.members)) {
74+
throw new Error('committee.members is not an array in the TOML file');
75+
}
76+
requiredApprovers = tomlData.committee.members;
77+
} catch (error) {
78+
console.error('Error reading or parsing TOML file:', error);
79+
core.setFailed('Failed to read required approvers list');
80+
return;
81+
}
82+
83+
// Get all reviews
84+
const reviews = await github.rest.pulls.listReviews({
85+
owner,
86+
repo,
87+
pull_number
88+
});
89+
90+
// Example: approvers = ["celina", "zyad"]
91+
const approvers = new Set(
92+
reviews.data
93+
.filter(review => review.state === 'APPROVED')
94+
.map(review => review.user.login)
95+
);
96+
97+
const requiredApprovals = 2;
98+
const requiredApproversCount = Array.from(approvers)
99+
.filter(approver => requiredApprovers.includes(approver))
100+
.length;
101+
102+
// TODO: Improve logging and messaging to the user
103+
console.log('PR Approvers:', Array.from(approvers));
104+
console.log('Required Approvers:', requiredApproversCount);
105+
106+
// Core logic that checks if the approvers are in the committee
107+
const checkName = 'PR Approval Status';
108+
const conclusion = (approvers.size >= requiredApprovals && requiredApproversCount >= 2) ? 'success' : 'failure';
109+
const output = {
110+
title: checkName,
111+
summary: `PR has ${approvers.size} total approvals and ${requiredApproversCount} required approvals.`,
112+
text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
113+
};
114+
115+
// Get PR details
116+
const pr = await github.rest.pulls.get({
117+
owner,
118+
repo,
119+
pull_number
120+
});
121+
122+
// Create or update check run
123+
const checkRuns = await github.rest.checks.listForRef({
124+
owner,
125+
repo,
126+
ref: pr.data.head.sha,
127+
check_name: checkName
128+
});
129+
130+
// Reuse the same workflow everytime there's a new review submitted
131+
// instead of creating new workflows. Better efficiency and readability
132+
// as the number of workflows is kept to a minimal number
133+
if (checkRuns.data.total_count > 0) {
134+
await github.rest.checks.update({
135+
owner,
136+
repo,
137+
check_run_id: checkRuns.data.check_runs[0].id,
138+
status: 'completed',
139+
conclusion,
140+
output
141+
});
142+
} else {
143+
await github.rest.checks.create({
144+
owner,
145+
repo,
146+
name: checkName,
147+
head_sha: pr.data.head.sha,
148+
status: 'completed',
149+
conclusion,
150+
output
151+
});
152+
}
153+
154+
if (conclusion === 'failure') {
155+
core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApproversCount}`);
156+
}

doc/src/SUMMARY.md

+1
Original file line numberDiff line numberDiff line change
@@ -16,3 +16,4 @@
1616
- [Core Transmutation](./challenges/0001-core-transmutation.md)
1717
- [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
1818
- [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
19+
- [Inductive data type](./challenges/0005-linked-list.md)
+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# Challenge 5: Verify functions iterating over inductive data type: `linked_list`
2+
3+
- **Status:** Open
4+
- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29)
5+
- **Start date:** *24/07/01*
6+
- **End date:** *24/12/10*
7+
8+
-------------------
9+
10+
11+
## Goal
12+
13+
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.
14+
15+
### Details
16+
17+
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.
18+
19+
20+
### Success Criteria
21+
22+
The memory safety of the following public functions that iterating over the internal inductive data type must be verified:
23+
24+
| Function | Location |
25+
|---------|---------|
26+
|clearn | alloc::collections::linked_list |
27+
|contains| alloc::collections::linked_list |
28+
|split_off| alloc::collections::linked_list |
29+
|remove| alloc::collections::linked_list |
30+
|retain| alloc::collections::linked_list |
31+
|retain_mut| alloc::collections::linked_list |
32+
|extract_if| alloc::collections::linked_list |
33+
34+
35+
The verification must be unbounded---it must hold for linked lists of arbitrary shape.
36+
37+
It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc.
38+
39+
### List of UBs
40+
41+
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):
42+
43+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
44+
* Reading from uninitialized memory except for padding or unions.
45+
* Mutating immutable bytes.
46+
* Producing an invalid value
47+
48+
49+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
50+
in addition to the ones listed above.

0 commit comments

Comments
 (0)