Skip to content

Commit 85e538b

Browse files
vzalivavzaliva
authored
CN: Mucore program export to Coq (#847)
* ignore cerb_times.csv * `with-coq` flag for cn.opam * CN coq build and package infrastructure * CerbTypes module * cn-with-coq target * top level _CoqProject for vscode * More MuCore and relted Cerberus types * workaround for build problem * better cn-dev-watch target * using sym type * iop, binop types * Id_t -> Symbol.identifier * simplified BaseTypes * Terms.v * indexTerms.v * index terms used * mem_iv_constraint * more types from OCaml * Symbol handling * initial work on Coq export. * location printing * pp_basetype * expr, body * memop printing * garbage printing supressed in PrefFunArg * remaining pexpr cases * renamed type_placeholder * more types definitions * pp_sctype * ctype * basetype printing fix * pp_annot_t * re-ident * pp_return_type * more types and printing * more types * undefined behaviours * pmap printing * correct pmap printing * message * CN types, pretty-printing to Coq * sctypes * struct_layout * linux memory order * pp_identifier * memory model simple module type * types for memory values * preptty printer for coq for memory model types * Request.Owned printing * pp_symbol debugged * Cnprog types and placeholders for printing * Cnprog.t pretty printing * ProcDecl handling * added missing Request.name constructor * type parametricity in BaseTypes.t_get * add --coq-export-file option to cn verify * imports in generated coq * typechecking output * string imports * balancing brackets * qualified field names for [q]predicate * core_base_types, constructors * Z literals * location_info printing * Request printing * Reques.t typechecks * fixing term printing shortcomings * painful type param propagation and constructor name disambiguation * constructor disambiguation, arguments tupling * handling negative literals * adding type parameters * type parameter in pp_value * more typing fixes * wip on typechecking * arguments types fix * pp_unit_type fix * coq typecheck pass for slf_quadruple_mem.c! * refactoring (pp_record) * pp_constructor used in pp_undefined * correction to pp_constructor * refactoring * number and string printing cleanup * option printing cleanup * more base types printing * more refactoring * more refactoring * more refactoring and base types printing fixes * more refactoring * refactored pp_cn_expr * refactoring pass done * pp_comment * line breaks and indentation * script to run cn coq tests * temp workaround for vip/concrete model mismatch * debugging coq extraction * print numbers * all tests pass * inlined Impl_mem.pp_pointer_value_for_coq * enabled warnings * pp_constructor0 * refactoring * generating .v in-place * fixed more tests after rebase. all pass now * CI tests for CN-coq (untested) * Enable CI on cn-logging branch * cache creation * opam init * missing dependency * test script name * update docs [skip ci] * reverting some accidental changes * aligning Coq constructor names with OCaml version * Refactor workflows to create cache keys based on matrix variables. - ci.cn builds CN without Coq - ci-cn-coq builds CN with Coq - ci-cheri builds CHERI-enabled CN - ci-cn-spec-testing runs CN-runtime tests (Cerberus and CN tutorial) and CN-Test-Gen - ci-cn-bench runs performance benchmarks - ci-docker - remains unchanged. * avoid duplicate switch creation * debuging caching * removed debug checks * formatting fixes * missing opam repo dependency * renamed some workflows to be more descriptive * adding missing pretty printers for CHERI memory model.
1 parent c935516 commit 85e538b

Some content is hidden

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

50 files changed

+5247
-47
lines changed

‎.github/workflows/ci-cheri.yml

+30-10
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,12 @@
1-
name: CHERI
1+
# Builds cerberus-cheri and runs CHERI tests
2+
3+
name: Cerberus-CHERI
24

35
on:
46
pull_request:
57
push:
68
branches:
79
- master
8-
- cheri-tests
910

1011
env:
1112
CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release
@@ -26,33 +27,52 @@ jobs:
2627
runs-on: ubuntu-22.04
2728

2829
steps:
29-
- uses: actions/checkout@v3
30+
31+
- name: Checkout Cerberus
32+
uses: actions/checkout@v4
3033

3134
- name: System dependencies (ubuntu)
3235
run: |
3336
sudo apt-get install build-essential libgmp-dev opam
3437
35-
- name: Restore cached opam
38+
- name: Restore OPAM cache
3639
id: cache-opam-restore
3740
uses: actions/cache/restore@v4
3841
with:
3942
path: ~/.opam
40-
key: ${{ matrix.version }}
41-
fail-on-cache-miss: true
43+
key: ${{ matrix.version }}-cheri
4244

45+
- name: Setup OPAM
46+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
47+
run: |
48+
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
49+
eval $(opam env --switch=${{ matrix.version }}-cheri)
50+
opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
51+
opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
52+
opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
53+
opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
54+
opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git#2f02c44ad061d4da30136dc9dbc06c142c94fdaf
55+
56+
- name: Save OPAM cache
57+
uses: actions/cache/save@v4
58+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
59+
with:
60+
path: ~/.opam
61+
key: ${{ matrix.version }}-cheri
62+
4363
- name: Install Cerberus-CHERI
4464
if: ${{ matrix.version == '4.14.1' }}
4565
run: |
46-
opam switch with_coq
47-
eval $(opam env --switch=with_coq)
66+
opam switch ${{ matrix.version }}-cheri
67+
eval $(opam env --switch=${{ matrix.version }}-cheri )
4868
opam pin --yes --no-action add cerberus-lib .
4969
opam pin --yes --no-action add cerberus-cheri .
5070
opam install --yes cerberus-cheri
5171
5272
- name: Run Cerberus-CHERI CI tests
5373
if: ${{ matrix.version == '4.14.1' }}
5474
run: |
55-
opam switch with_coq
56-
eval $(opam env --switch=with_coq)
75+
opam switch ${{ matrix.version }}-cheri
76+
eval $(opam env --switch=${{ matrix.version }}-cheri )
5777
cd tests; USE_OPAM='' ./run-cheri.sh
5878
cd ..

‎.github/workflows/ci-cn-bench.yml

+20-5
Original file line numberDiff line numberDiff line change
@@ -31,20 +31,35 @@ jobs:
3131
runs-on: ubuntu-22.04
3232

3333
steps:
34-
- uses: actions/checkout@v3
3534

36-
- name: System dependencies (ubuntu)
35+
- name: Checkout Cerberus
36+
uses: actions/checkout@v4
37+
38+
- name: System dependencies (Ubuntu)
3739
run: |
3840
sudo apt-get install build-essential libgmp-dev z3 opam jq
3941
40-
- name: Restore cached opam
42+
- name: Restore OPAM cache
4143
id: cache-opam-restore
4244
uses: actions/cache/restore@v4
4345
with:
4446
path: ~/.opam
4547
key: ${{ matrix.version }}
46-
fail-on-cache-miss: true
47-
48+
49+
- name: Setup OPAM
50+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
51+
run: |
52+
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
53+
eval $(opam env --switch=${{ matrix.version }})
54+
opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
55+
56+
- name: Save OPAM cache
57+
uses: actions/cache/save@v4
58+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
59+
with:
60+
path: ~/.opam
61+
key: ${{ matrix.version }}
62+
4863
- name: Install Cerberus
4964
run: |
5065
opam switch ${{ matrix.version }}

‎.github/workflows/ci-cn-coq.yml

+80
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
# Builds CN with Coq and runs Coq tests
2+
name: CN-Coq
3+
4+
on:
5+
pull_request:
6+
push:
7+
branches:
8+
- master
9+
- cn-logging
10+
- cn-resource-logging
11+
12+
env:
13+
CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release
14+
15+
# cancel in-progress job when a new push is performed
16+
concurrency:
17+
group: ci-${{ github.workflow }}-${{ github.ref }}
18+
cancel-in-progress: true
19+
20+
jobs:
21+
build:
22+
strategy:
23+
matrix:
24+
version: [5.2.0]
25+
26+
runs-on: ubuntu-22.04
27+
28+
steps:
29+
30+
- name: Checkout Cerberus
31+
uses: actions/checkout@v4
32+
33+
- name: System dependencies (Ubuntu)
34+
run: |
35+
sudo apt-get install build-essential libgmp-dev z3 opam
36+
37+
- name: Restore OPAM cache
38+
id: cache-opam-restore
39+
uses: actions/cache/restore@v4
40+
with:
41+
path: ~/.opam
42+
key: ${{ matrix.version }}-with-coq
43+
44+
- name: Setup OPAM
45+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
46+
run: |
47+
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
48+
opam switch create ${{ matrix.version }}-with-coq ${{ matrix.version }}
49+
eval $(opam env --switch=${{ matrix.version }}-with-coq)
50+
opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
51+
opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
52+
53+
- name: Save OPAM cache
54+
uses: actions/cache/save@v4
55+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
56+
with:
57+
path: ~/.opam
58+
key: ${{ matrix.version }}-with-coq
59+
60+
- name: Install Cerberus
61+
run: |
62+
opam switch ${{ matrix.version }}-with-coq
63+
eval $(opam env --switch=${{ matrix.version }}-with-coq )
64+
opam pin --yes --no-action add cerberus-lib .
65+
opam pin --yes --no-action add cerberus .
66+
opam install --yes cerberus
67+
68+
- name: Install CN (with Coq)
69+
run: |
70+
opam switch ${{ matrix.version }}-with-coq
71+
eval $(opam env --switch=${{ matrix.version }}-with-coq )
72+
opam pin --yes --no-action add cn .
73+
opam pin --yes --no-action add cn-coq .
74+
opam install --yes cn cn-coq ocamlformat.0.26.2
75+
76+
- name: Run CN-Coq tests
77+
run: |
78+
opam switch ${{ matrix.version }}-with-coq
79+
eval $(opam env --switch=${{ matrix.version }}-with-coq )
80+
./tests/run-cn-coq.sh

‎.github/workflows/ci-cn-spec-testing.yml

+16-3
Original file line numberDiff line numberDiff line change
@@ -26,20 +26,33 @@ jobs:
2626

2727
steps:
2828

29-
- name: Checkout cerberus
29+
- name: Checkout Cerberus
3030
uses: actions/checkout@v4
3131

3232
- name: System dependencies (ubuntu)
3333
run: |
3434
sudo apt-get install build-essential libgmp-dev z3 opam cmake lcov
3535
36-
- name: Restore cached opam
36+
- name: Restore OPAM cache
3737
id: cache-opam-restore
3838
uses: actions/cache/restore@v4
3939
with:
4040
path: ~/.opam
4141
key: ${{ matrix.version }}
42-
fail-on-cache-miss: true
42+
43+
- name: Setup OPAM
44+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
45+
run: |
46+
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
47+
eval $(opam env --switch=${{ matrix.version }})
48+
opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
49+
50+
- name: Save OPAM cache
51+
uses: actions/cache/save@v4
52+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
53+
with:
54+
path: ~/.opam
55+
key: ${{ matrix.version }}
4356

4457
- name: Install Cerberus
4558
run: |

‎.github/workflows/ci-cn.yml

+20-5
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
# Installs CN (without Coq) and runs tests
12
name: CN Proof
23

34
on:
@@ -21,23 +22,37 @@ jobs:
2122
# version: [4.12.0, 4.14.1]
2223
version: [4.14.1]
2324

24-
2525
runs-on: ubuntu-22.04
2626

2727
steps:
28-
- uses: actions/checkout@v3
2928

30-
- name: System dependencies (ubuntu)
29+
- name: Checkout Cerberus
30+
uses: actions/checkout@v4
31+
32+
- name: System dependencies (Ubuntu)
3133
run: |
3234
sudo apt-get install build-essential libgmp-dev z3 opam
3335
34-
- name: Restore cached opam
36+
- name: Restore OPAM cache
3537
id: cache-opam-restore
3638
uses: actions/cache/restore@v4
3739
with:
3840
path: ~/.opam
3941
key: ${{ matrix.version }}
40-
fail-on-cache-miss: true
42+
43+
- name: Setup OPAM
44+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
45+
run: |
46+
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
47+
eval $(opam env --switch=${{ matrix.version }})
48+
opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
49+
50+
- name: Save OPAM cache
51+
uses: actions/cache/save@v4
52+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
53+
with:
54+
path: ~/.opam
55+
key: ${{ matrix.version }}
4156

4257
- name: Install Cerberus
4358
run: |

‎.github/workflows/ci.yml

+24-13
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
name: CI
1+
# Install Cerberus (without Coq or CHERI) and run tests
2+
name: Cerberus
23

34
on:
45
pull_request:
@@ -26,40 +27,50 @@ jobs:
2627
runs-on: ubuntu-22.04
2728

2829
steps:
29-
- uses: actions/checkout@v3
30+
31+
- name: Checkout Cerberus
32+
uses: actions/checkout@v4
3033

3134
- name: System dependencies (ubuntu)
3235
run: |
3336
sudo apt-get install build-essential libgmp-dev z3 opam cmake
3437
35-
- name: Restore cached opam
38+
- name: Restore OPAM cache
3639
id: cache-opam-restore
3740
uses: actions/cache/restore@v4
3841
with:
3942
path: ~/.opam
4043
key: ${{ matrix.version }}
41-
44+
45+
- name: Setup OPAM
46+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
47+
run: |
48+
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
49+
opam switch create ${{ matrix.version }} ${{ matrix.version }}
50+
eval $(opam env --switch=${{ matrix.version }})
51+
opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
52+
53+
- name: Save OPAM cache
54+
uses: actions/cache/save@v4
55+
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
56+
with:
57+
path: ~/.opam
58+
key: ${{ matrix.version }}
59+
4260
- name: Setup opam
4361
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
4462
run: |
4563
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
46-
opam install --deps-only --yes ./cerberus-lib.opam
47-
opam switch create with_coq ${{ matrix.version }}
48-
eval $(opam env --switch=with_coq)
64+
eval $(opam env --switch=${{ matrix.version }})
4965
opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
50-
opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
51-
opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
52-
opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
53-
opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git#2f02c44ad061d4da30136dc9dbc06c142c94fdaf
54-
opam install --deps-only --yes ./cerberus-lib.opam ./cerberus-cheri.opam
5566
5667
- name: Save cached opam
5768
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
5869
id: cache-opam-save
5970
uses: actions/cache/save@v4
6071
with:
6172
path: ~/.opam
62-
key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
73+
key: ${{ matrix.version }}
6374

6475
- name: Install Cerberus
6576
run: |

‎.gitignore

+18
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
# Dune build directory
22
_build
33

4+
# Dune temporary files
5+
*.install
6+
47
# Merlin files are generated by Dune
58
.merlin
69

@@ -36,6 +39,21 @@ public/package-lock.json
3639
/backend/cheri/cerb.prof
3740
/cerb.prof
3841

42+
# Coq generated files
43+
*.vo
44+
*.vok
45+
*.vos
46+
*.glob
47+
*.aux
48+
*.log
49+
*.html
50+
*.vty
51+
*.vti
52+
3953
# debug stuff
4054
log*.txt
4155
*.cache
56+
cerberus.code-workspace
57+
.vscode/tasks.json
58+
.cursorignore
59+
cerb_times.csv

0 commit comments

Comments
 (0)