Skip to content

Commit 1f4b817

Browse files
karthikbhargavankarthikbhargavan
authored
Merge branch 'main' into simd-models
2 parents 428fd3c + 099ad08 commit 1f4b817

File tree

1,962 files changed

+921446
-95281
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,962 files changed

+921446
-95281
lines changed

‎.github/ISSUE_TEMPLATE/tool_application.md‎

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: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,15 @@ members = [
99
"remi-delmas-3000",
1010
"qinheping",
1111
"tautschnig",
12-
"jaisnan",
1312
"patricklam",
1413
"ranjitjhala",
1514
"carolynzech",
1615
"robdockins",
1716
"HuStmpHrrr",
18-
"Eh2406"
17+
"Eh2406",
18+
"jswrenn",
19+
"havelund",
20+
"jorajeev",
21+
"rajath-mk",
22+
"thanhnguyen-aws"
1923
]

‎.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:

‎.github/workflows/flux.yml‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
name: Flux
2+
3+
on:
4+
workflow_dispatch:
5+
push:
6+
branches: [main]
7+
pull_request:
8+
branches: [main]
9+
10+
env:
11+
FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
12+
FLUX_VERSION: "f6bdf90c54ad6eed51b25c125f251cac01cfe170"
13+
14+
jobs:
15+
check-flux-on-core:
16+
runs-on: ubuntu-latest
17+
steps:
18+
- uses: actions/checkout@v4
19+
with:
20+
submodules: true
21+
22+
- name: Local Binaries
23+
run: |
24+
mkdir -p ~/.local/bin
25+
echo ~/.cargo/bin >> $GITHUB_PATH
26+
echo ~/.local/bin >> $GITHUB_PATH
27+
28+
- name: Cache fixpoint
29+
uses: actions/cache@v4
30+
id: cache-fixpoint
31+
with:
32+
path: ~/.local/bin/fixpoint
33+
key: fixpoint-bin-${{ runner.os }}-${{ env.FIXPOINT_VERSION }}
34+
35+
- name: Install Haskell
36+
if: steps.cache-fixpoint.outputs.cache-hit != 'true'
37+
uses: haskell-actions/[email protected]
38+
with:
39+
enable-stack: true
40+
stack-version: "2.15.7"
41+
42+
- name: Install fixpoint
43+
if: steps.cache-fixpoint.outputs.cache-hit != 'true'
44+
run: |
45+
git clone https://github.com/ucsd-progsys/liquid-fixpoint.git
46+
cd liquid-fixpoint
47+
git checkout $FIXPOINT_VERSION
48+
stack install --fast --flag liquid-fixpoint:-link-z3-as-a-library
49+
50+
- name: Install Z3
51+
uses: cda-tum/[email protected]
52+
with:
53+
version: 4.12.1
54+
platform: linux
55+
env:
56+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
57+
58+
- name: Clone Flux
59+
run: |
60+
git clone https://github.com/flux-rs/flux.git
61+
cd flux
62+
git checkout $FLUX_VERSION
63+
64+
- name: Rust Cache
65+
uses: Swatinem/[email protected]
66+
with:
67+
workspaces: flux
68+
69+
- name: Install Flux
70+
run: |
71+
cd flux
72+
cargo x install
73+
74+
- name: Verify Core
75+
run: |
76+
cd library
77+
FLUXFLAGS="-Ftimings" cargo flux -p core

‎.github/workflows/goto-transcoder.yml‎

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: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
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: Remove unnecessary software to free up disk space
18+
run: |
19+
# inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
20+
df -h
21+
sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
22+
df -h
23+
24+
- name: Checkout Repository
25+
uses: actions/checkout@v4
26+
with:
27+
submodules: true
28+
29+
# The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
30+
- name: Set up Python
31+
uses: actions/setup-python@v4
32+
with:
33+
python-version: '3.x'
34+
35+
- name: Compute Kani Metrics
36+
run: |
37+
./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
38+
rm kani-list.json
39+
40+
- name: Create Pull Request
41+
uses: peter-evans/create-pull-request@v7
42+
with:
43+
commit-message: Update Kani metrics
44+
title: 'Update Kani Metrics'
45+
body: |
46+
This is an automated PR to update Kani metrics.
47+
48+
The metrics have been updated by running `./scripts/run-kani.sh --run metrics`.
49+
branch: update-kani-metrics
50+
delete-branch: true
51+
base: main

0 commit comments

Comments
 (0)