Skip to content

Commit fb30e98

Browse files
committed
Merge remote-tracking branch 'origin/main' into unchecked_mull_add
2 parents 4f945c8 + 5cf80a8 commit fb30e98

File tree

1,054 files changed

+60866
-27397
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,054 files changed

+60866
-27397
lines changed
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
---
2+
name: Tool Application
3+
about: Submit a new tool application
4+
title: "[Tool Application] "
5+
labels: Tool Application
6+
---
7+
8+
<!--
9+
Please see https://model-checking.github.io/verify-rust-std/tool_template.html for the application template.
10+
-->

.github/pull_requests.toml

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,15 @@ members = [
99
"remi-delmas-3000",
1010
"qinheping",
1111
"tautschnig",
12-
"jaisnan",
1312
"patricklam",
1413
"ranjitjhala",
1514
"carolynzech",
1615
"robdockins",
1716
"HuStmpHrrr",
1817
"Eh2406",
19-
"jswrenn"
18+
"jswrenn",
19+
"havelund",
20+
"jorajeev",
21+
"rajath-mk",
22+
"thanhnguyen-aws"
2023
]

.github/workflows/book.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
name: Build Book
44
on:
55
workflow_dispatch:
6+
merge_group:
67
pull_request:
78
branches: [ main ]
89
push:
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# This workflow executes the supported contracts in goto-transcoder
2+
3+
name: Run GOTO Transcoder (ESBMC)
4+
on:
5+
workflow_dispatch:
6+
merge_group:
7+
pull_request:
8+
branches: [ main ]
9+
push:
10+
paths:
11+
- 'library/**'
12+
- '.github/workflows/goto-transcoder.yml'
13+
- 'scripts/run-kani.sh'
14+
- 'scripts/run-goto-transcoder.sh'
15+
16+
defaults:
17+
run:
18+
shell: bash
19+
20+
jobs:
21+
verify-rust-std:
22+
name: Verify contracts with goto-transcoder
23+
runs-on: ubuntu-latest
24+
steps:
25+
# Step 1: Check out the repository
26+
- name: Checkout Repository
27+
uses: actions/checkout@v4
28+
with:
29+
submodules: true
30+
31+
# Step 2: Generate contracts programs
32+
- name: Generate contracts
33+
run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts
34+
35+
# Step 3: Run goto-transcoder
36+
- name: Run goto-transcoder
37+
run: ./scripts/run-goto-transcoder.sh kani/contracts checked_unchecked.*.out

.github/workflows/kani-metrics.yml

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
name: Kani Metrics Update
2+
3+
on:
4+
schedule:
5+
- cron: '0 0 * * 0' # Run at 00:00 UTC every Sunday
6+
workflow_dispatch:
7+
8+
defaults:
9+
run:
10+
shell: bash
11+
12+
jobs:
13+
update-kani-metrics:
14+
runs-on: ubuntu-latest
15+
16+
steps:
17+
- name: Checkout Repository
18+
uses: actions/checkout@v4
19+
with:
20+
submodules: true
21+
22+
# The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
23+
- name: Set up Python
24+
uses: actions/setup-python@v4
25+
with:
26+
python-version: '3.x'
27+
28+
- name: Compute Kani Metrics
29+
run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
30+
31+
- name: Create Pull Request
32+
uses: peter-evans/create-pull-request@v7
33+
with:
34+
commit-message: Update Kani metrics
35+
title: 'Update Kani Metrics'
36+
body: |
37+
This is an automated PR to update Kani metrics.
38+
39+
The metrics have been updated by running `./scripts/run-kani.sh --run metrics`.
40+
branch: update-kani-metrics
41+
delete-branch: true
42+
base: main

.github/workflows/kani.yml

Lines changed: 29 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ name: Kani
22

33
on:
44
workflow_dispatch:
5+
merge_group:
56
pull_request:
67
branches: [ main ]
78
push:
@@ -16,39 +17,45 @@ defaults:
1617

1718
jobs:
1819
check-kani-on-std:
19-
name: Verify std library
20+
name: Verify std library (partition ${{ matrix.partition }})
2021
runs-on: ${{ matrix.os }}
2122
strategy:
2223
matrix:
2324
os: [ubuntu-latest, macos-latest]
25+
partition: [1, 2, 3, 4]
2426
include:
2527
- os: ubuntu-latest
2628
base: ubuntu
2729
- os: macos-latest
2830
base: macos
31+
fail-fast: false
32+
33+
env:
34+
# Define the index of this particular worker [1-WORKER_TOTAL]
35+
WORKER_INDEX: ${{ matrix.partition }}
36+
# Total number of workers running this step
37+
WORKER_TOTAL: 4
38+
2939
steps:
3040
# Step 1: Check out the repository
3141
- name: Checkout Repository
3242
uses: actions/checkout@v4
3343
with:
3444
path: head
3545
submodules: true
36-
37-
# Step 2: Run Kani on the std library (default configuration)
46+
47+
# Step 2: Install jq
48+
- name: Install jq
49+
if: matrix.os == 'ubuntu-latest'
50+
run: sudo apt-get install -y jq
51+
52+
# Step 3: Run Kani on the std library (default configuration)
3853
- name: Run Kani Verification
3954
run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
40-
41-
test-kani-script:
42-
name: Test Kani script
43-
runs-on: ${{ matrix.os }}
44-
strategy:
45-
matrix:
46-
os: [ubuntu-latest, macos-latest]
47-
include:
48-
- os: ubuntu-latest
49-
base: ubuntu
50-
- os: macos-latest
51-
base: macos
55+
56+
run-kani-list:
57+
name: Kani List
58+
runs-on: ubuntu-latest
5259
steps:
5360
# Step 1: Check out the repository
5461
- name: Checkout Repository
@@ -57,25 +64,18 @@ jobs:
5764
path: head
5865
submodules: true
5966

60-
# Step 2: Test Kani verification script with specific arguments
61-
- name: Test Kani script (Custom Args)
62-
run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse
63-
64-
# Step 3: Test Kani verification script in the repository directory
65-
- name: Test Kani script (In Repo Directory)
66-
working-directory: ${{github.workspace}}/head
67-
run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
68-
69-
# Step 4: Run list on the std library and add output to job summary
67+
# Step 2: Run list on the std library
7068
- name: Run Kani List
7169
run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
72-
70+
71+
# Step 3: Add output to job summary
7372
- name: Add Kani List output to job summary
7473
uses: actions/github-script@v6
7574
with:
7675
script: |
7776
const fs = require('fs');
78-
const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
77+
const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani-list.md', 'utf8');
7978
await core.summary
80-
.addRaw(kaniOutput)
81-
.write();
79+
.addHeading('Kani List Output', 2)
80+
.addRaw(kaniOutput, false)
81+
.write();

.github/workflows/pr_approval.yml

Lines changed: 64 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,33 @@
1+
# This workflow checks that the PR has been approved by 2+ members of the committee listed in `pull_requests.toml`.
2+
#
3+
# Run this action when a pull request review is submitted / dismissed.
4+
# Note that an approval can be dismissed, and this can affect the job status.
5+
# We currently trust that contributors won't make significant changes to their PRs after approval, so we accept
6+
# changes after approval.
7+
#
8+
# We still need to run this in the case of a merge group, since it is a required step. In that case, the workflow
9+
# is a NOP.
110
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
711
on:
12+
merge_group:
813
pull_request_review:
9-
types: [submitted]
14+
types: [submitted, dismissed]
1015

1116
jobs:
1217
check-approvals:
1318
runs-on: ubuntu-latest
1419
steps:
1520
- name: Checkout repository
1621
uses: actions/checkout@v2
22+
if: ${{ github.event_name != 'merge_group' }}
1723

1824
- name: Install TOML parser
1925
run: npm install @iarna/toml
26+
if: ${{ github.event_name != 'merge_group' }}
2027

2128
- name: Check PR Relevance and Approvals
2229
uses: actions/github-script@v6
30+
if: ${{ github.event_name != 'merge_group' }}
2331
with:
2432
script: |
2533
const fs = require('fs');
@@ -44,8 +52,11 @@ jobs:
4452
pull_number = context.issue.number;
4553
}
4654
55+
console.log(`owner is ${owner}`);
56+
console.log(`pull_number is ${pull_number}`);
4757
4858
// Get parsed data
59+
let requiredApprovers;
4960
try {
5061
const tomlContent = fs.readFileSync('.github/pull_requests.toml', 'utf8');
5162
console.log('TOML content:', tomlContent);
@@ -62,38 +73,63 @@ jobs:
6273
return;
6374
}
6475
65-
// Get all reviews
66-
const reviews = await github.rest.pulls.listReviews({
67-
owner,
68-
repo,
69-
pull_number
70-
});
76+
// Get all reviews with pagination
77+
async function getAllReviews() {
78+
let allReviews = [];
79+
let page = 1;
80+
let page_limit = 100;
81+
82+
while (page < page_limit) {
83+
const response = await github.rest.pulls.listReviews({
84+
owner,
85+
repo,
86+
pull_number,
87+
per_page: 100,
88+
page
89+
});
90+
91+
allReviews = allReviews.concat(response.data);
92+
93+
if (response.data.length < 100) {
94+
break;
95+
}
96+
97+
page++;
98+
}
99+
100+
if (page == page_limit) {
101+
console.log(`WARNING: Reached page limit of ${page_limit} while fetching reviews data; approvals count may be less than the real total.`)
102+
}
103+
104+
return allReviews;
105+
}
106+
107+
const reviews = await getAllReviews();
71108
72109
// Example: approvers = ["celina", "zyad"]
73110
const approvers = new Set(
74-
reviews.data
111+
reviews
75112
.filter(review => review.state === 'APPROVED')
76113
.map(review => review.user.login)
77114
);
78115
79116
const requiredApprovals = 2;
80-
const currentCountfromCommittee = Array.from(approvers)
81-
.filter(approver => requiredApprovers.includes(approver))
82-
.length;
83-
84-
// TODO: Improve logging and messaging to the user
85-
console.log('PR Approvers:', Array.from(approvers));
86-
console.log('Required Approvers:', requiredApprovals);
117+
const committeeApprovers = Array.from(approvers)
118+
.filter(approver => requiredApprovers.includes(approver));
119+
const currentCountfromCommittee = committeeApprovers.length;
87120
88121
// Core logic that checks if the approvers are in the committee
89-
const checkName = 'PR Approval Status';
90-
const conclusion = (approvers.size >= requiredApprovals && currentCountfromCommittee >= 2) ? 'success' : 'failure';
91-
const output = {
92-
title: checkName,
93-
summary: `PR has ${approvers.size} total approvals and ${requiredApprovals} required approvals.`,
94-
text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
95-
};
122+
const conclusion = (currentCountfromCommittee >= 2) ? 'success' : 'failure';
96123
124+
console.log('PR Approval Status');
125+
console.log(`PR has ${approvers.size} total approvals and ${currentCountfromCommittee} required approvals from the committee.`);
126+
127+
console.log(`Committee Members: [${requiredApprovers.join(', ')}]`);
128+
console.log(`Committee Approvers: ${committeeApprovers.length === 0 ? 'NONE' : `[${committeeApprovers.join(', ')}]`}`);
129+
console.log(`All Approvers: ${approvers.size === 0 ? 'NONE' : `[${Array.from(approvers).join(', ')}]`}`);
130+
97131
if (conclusion === 'failure') {
98-
core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);
132+
core.setFailed(`PR needs 2 approvals from committee members, but it has ${currentCountfromCommittee}`);
133+
} else {
134+
core.info('PR approval check passed successfully.');
99135
}

.github/workflows/rustc.yml

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
name: Rust Tests
55
on:
66
workflow_dispatch:
7+
merge_group:
78
pull_request:
89
branches: [ main ]
910
push:
@@ -18,7 +19,7 @@ defaults:
1819
shell: bash
1920

2021
jobs:
21-
build:
22+
upstream_test:
2223
runs-on: ${{ matrix.os }}
2324
strategy:
2425
matrix:
@@ -27,8 +28,8 @@ jobs:
2728
steps:
2829
- name: Checkout Library
2930
uses: actions/checkout@v4
30-
with:
31-
path: head
3231

3332
- name: Run rustc script
34-
run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head
33+
env:
34+
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
35+
run: ./scripts/check_rustc.sh

0 commit comments

Comments
 (0)