Skip to content

Commit 31a8d89

Browse files
AlexLB99AlexLB99
authored
Merge branch 'model-checking:main' into check_align_to
2 parents 9e62272 + c176f19 commit 31a8d89

File tree

522 files changed

+735867
-3916
lines changed

Some content is hidden

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

522 files changed

+735867
-3916
lines changed

‎.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: "844e2fc0caa6aa96d72f2fcb627a27bf2495d82e"
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: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,6 @@ jobs:
2727
uses: actions/checkout@v4
2828
with:
2929
submodules: true
30-
- name: Apply stdarch patch
31-
run: cd library/stdarch && patch -p1 < ../../stdarch.patch
3230

3331
# Step 2: Generate contracts programs
3432
- name: Generate contracts

‎.github/workflows/kani-metrics.yml‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,7 @@ jobs:
2525
uses: actions/checkout@v4
2626
with:
2727
submodules: true
28-
- name: Apply stdarch patch
29-
run: cd library/stdarch && patch -p1 < ../../stdarch.patch
30-
28+
3129
# The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
3230
- name: Set up Python
3331
uses: actions/setup-python@v4

‎.github/workflows/kani.yml‎

Lines changed: 60 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,7 @@ jobs:
5151
with:
5252
path: head
5353
submodules: true
54-
- name: Apply stdarch patch
55-
run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
56-
54+
5755
# Step 2: Install jq
5856
- name: Install jq
5957
if: matrix.os == 'ubuntu-latest'
@@ -90,30 +88,82 @@ jobs:
9088
uses: actions/checkout@v4
9189
with:
9290
submodules: true
93-
- name: Apply stdarch patch
94-
run: cd library/stdarch && patch -p1 < ../../stdarch.patch
9591

9692
# Step 2: Run Kani autoharness on the std library for selected functions.
9793
# Uses "--include-pattern" to make sure we do not try to run across all
9894
# possible functions as that may take a lot longer than expected. Instead,
9995
# explicitly list all functions (or prefixes thereof) the proofs of which
10096
# are known to pass.
10197
# Notes:
102-
# - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
103-
# as whitespace is not supported, cf.
104-
# https://github.com/model-checking/kani/issues/4046
10598
# - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
10699
# core_arch::x86:: functions that are known to verify successfully.
107100
- name: Run Kani Verification
108101
run: |
109102
scripts/run-kani.sh --run autoharness --kani-args \
110-
--include-pattern ">::disjoint_bitor" \
111-
--include-pattern ">::unchecked_disjoint_bitor" \
103+
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
104+
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \
105+
--include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::backward_unchecked" \
106+
--include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::forward_unchecked" \
112107
--include-pattern alloc::__default_lib_allocator:: \
113108
--include-pattern alloc::layout::Layout::from_size_align \
114109
--include-pattern ascii::ascii_char::AsciiChar::from_u8 \
115110
--include-pattern char::convert::from_u32_unchecked \
116111
--include-pattern core_arch::x86::__m128d::as_f64x2 \
112+
--include-pattern "convert::num::<impl.convert::From<num::nonzero::NonZero<" \
113+
--include-pattern "num::<impl.i8>::unchecked_add" \
114+
--include-pattern "num::<impl.i16>::unchecked_add" \
115+
--include-pattern "num::<impl.i32>::unchecked_add" \
116+
--include-pattern "num::<impl.i64>::unchecked_add" \
117+
--include-pattern "num::<impl.i128>::unchecked_add" \
118+
--include-pattern "num::<impl.isize>::unchecked_add" \
119+
--include-pattern "num::<impl.u8>::unchecked_add" \
120+
--include-pattern "num::<impl.u16>::unchecked_add" \
121+
--include-pattern "num::<impl.u32>::unchecked_add" \
122+
--include-pattern "num::<impl.u64>::unchecked_add" \
123+
--include-pattern "num::<impl.u128>::unchecked_add" \
124+
--include-pattern "num::<impl.usize>::unchecked_add" \
125+
--include-pattern "num::<impl.i8>::unchecked_neg" \
126+
--include-pattern "num::<impl.i16>::unchecked_neg" \
127+
--include-pattern "num::<impl.i32>::unchecked_neg" \
128+
--include-pattern "num::<impl.i64>::unchecked_neg" \
129+
--include-pattern "num::<impl.i128>::unchecked_neg" \
130+
--include-pattern "num::<impl.isize>::unchecked_neg" \
131+
--include-pattern "num::<impl.i8>::unchecked_sh" \
132+
--include-pattern "num::<impl.i16>::unchecked_sh" \
133+
--include-pattern "num::<impl.i32>::unchecked_sh" \
134+
--include-pattern "num::<impl.i64>::unchecked_sh" \
135+
--include-pattern "num::<impl.i128>::unchecked_sh" \
136+
--include-pattern "num::<impl.isize>::unchecked_sh" \
137+
--include-pattern "num::<impl.u8>::unchecked_sh" \
138+
--include-pattern "num::<impl.u16>::unchecked_sh" \
139+
--include-pattern "num::<impl.u32>::unchecked_sh" \
140+
--include-pattern "num::<impl.u64>::unchecked_sh" \
141+
--include-pattern "num::<impl.u128>::unchecked_sh" \
142+
--include-pattern "num::<impl.usize>::unchecked_sh" \
143+
--include-pattern "num::<impl.i8>::unchecked_sub" \
144+
--include-pattern "num::<impl.i16>::unchecked_sub" \
145+
--include-pattern "num::<impl.i32>::unchecked_sub" \
146+
--include-pattern "num::<impl.i64>::unchecked_sub" \
147+
--include-pattern "num::<impl.i128>::unchecked_sub" \
148+
--include-pattern "num::<impl.isize>::unchecked_sub" \
149+
--include-pattern "num::<impl.u8>::unchecked_sub" \
150+
--include-pattern "num::<impl.u16>::unchecked_sub" \
151+
--include-pattern "num::<impl.u32>::unchecked_sub" \
152+
--include-pattern "num::<impl.u64>::unchecked_sub" \
153+
--include-pattern "num::<impl.u128>::unchecked_sub" \
154+
--include-pattern "num::<impl.usize>::unchecked_sub" \
155+
--include-pattern "num::<impl.i8>::wrapping_sh" \
156+
--include-pattern "num::<impl.i16>::wrapping_sh" \
157+
--include-pattern "num::<impl.i32>::wrapping_sh" \
158+
--include-pattern "num::<impl.i64>::wrapping_sh" \
159+
--include-pattern "num::<impl.i128>::wrapping_sh" \
160+
--include-pattern "num::<impl.isize>::wrapping_sh" \
161+
--include-pattern "num::<impl.u8>::wrapping_sh" \
162+
--include-pattern "num::<impl.u16>::wrapping_sh" \
163+
--include-pattern "num::<impl.u32>::wrapping_sh" \
164+
--include-pattern "num::<impl.u64>::wrapping_sh" \
165+
--include-pattern "num::<impl.u128>::wrapping_sh" \
166+
--include-pattern "num::<impl.usize>::wrapping_sh" \
117167
--include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
118168
--include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
119169
--include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
@@ -295,8 +345,6 @@ jobs:
295345
with:
296346
path: head
297347
submodules: true
298-
- name: Apply stdarch patch
299-
run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
300348

301349
# Step 2: Run list on the std library
302350
- name: Run Kani List
@@ -329,8 +377,6 @@ jobs:
329377
uses: actions/checkout@v4
330378
with:
331379
submodules: true
332-
- name: Apply stdarch patch
333-
run: cd library/stdarch && patch -p1 < ../../stdarch.patch
334380

335381
# Step 2: Run autoharness analyzer on the std library
336382
- name: Run Autoharness Analyzer

‎doc/src/SUMMARY.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
- [Kani](./tools/kani.md)
1111
- [GOTO Transcoder](./tools/goto-transcoder.md)
1212
- [VeriFast](./tools/verifast.md)
13+
- [Flux](./tools/flux.md)
1314

1415
---
1516

0 commit comments

Comments
 (0)