Skip to content

Commit 50921df

Browse files
tob-joecodex
tob-joe
and
codex
committed
Test CBMC target models in CI
Add CBMC workflow inputs for selecting a target platform, proof subset, single-step execution, timeout, report mode, and Nix shell. Use those inputs to run the cbmc_target_model canary across every supported explicit CBMC target in the cbmc32 shell, while leaving the existing full-suite CBMC jobs unchanged. Also format flake.nix with nixpkgs-fmt and add the SPDX/copyright headers required by lint to the target compiler shims. Verification: - nix develop .#ci -c lint - python3 -B -m py_compile scripts/tests proofs/cbmc/run-cbmc-proofs.py - ./scripts/tests cbmc --help - cbmc_target_model passed locally for i386-linux, x86_64-linux, aarch64-linux, riscv64-linux, and ppc64le-linux under .#cbmc32 Signed-off-by: Joe Doyle <joseph.doyle@trailofbits.com> Co-authored-by: Codex <codex@openai.com>
1 parent 7290e5c commit 50921df

9 files changed

Lines changed: 147 additions & 19 deletions

File tree

‎.github/actions/cbmc/action.yml‎

Lines changed: 57 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,24 @@ inputs:
2020
mlkem_k:
2121
description: "Security level for ML-KEM (2,3,4)"
2222
default: "2"
23+
cbmc-target:
24+
description: "CBMC target platform; empty uses the default host model"
25+
default: ""
26+
proofs:
27+
description: "Space-separated proof patterns to run; empty runs all proofs"
28+
default: ""
29+
single-step:
30+
description: "Run proofs one at a time"
31+
default: "false"
32+
timeout:
33+
description: "Timeout for individual CBMC proofs, in seconds"
34+
default: "3600"
35+
per-proof-timeout:
36+
description: "Timeout passed to run-cbmc-proofs.py for each proof"
37+
default: "1800"
38+
report:
39+
description: "Publish CBMC runtime regression report"
40+
default: "true"
2341
gh_token:
2442
description: Github access token to use
2543
required: true
@@ -53,14 +71,44 @@ runs:
5371
env:
5472
GH_TOKEN: ${{ inputs.gh_token }}
5573
run: |
56-
echo "::group::cbmc_${{ inputs.mlkem_k }}"
57-
tests cbmc --mlkem-parameter-set ${{ inputs.mlkem_k }} --per-proof-timeout 1800 --output-result-json ${{ github.workspace }}/cbmc_result_k${{ inputs.mlkem_k }}.json || cbmc_failed=true
74+
cbmc_failed=false
75+
cbmc_target="${{ inputs.cbmc-target }}"
76+
group_name="cbmc_${{ inputs.mlkem_k }}"
77+
result_suffix=""
78+
if [ -n "$cbmc_target" ]; then
79+
group_name="${group_name}_${cbmc_target}"
80+
result_suffix="_${cbmc_target//[^A-Za-z0-9_.-]/_}"
81+
fi
82+
result_json="${{ github.workspace }}/cbmc_result_k${{ inputs.mlkem_k }}${result_suffix}.json"
83+
cbmc_args=(
84+
--mlkem-parameter-set "${{ inputs.mlkem_k }}"
85+
--timeout "${{ inputs.timeout }}"
86+
--per-proof-timeout "${{ inputs.per-proof-timeout }}"
87+
)
88+
if [ -n "$cbmc_target" ]; then
89+
cbmc_args+=(--cbmc-target "$cbmc_target")
90+
fi
91+
proofs="${{ inputs.proofs }}"
92+
if [ -n "$proofs" ]; then
93+
read -r -a proof_args <<< "$proofs"
94+
cbmc_args+=(-p "${proof_args[@]}")
95+
fi
96+
if [ "${{ inputs.single-step }}" = "true" ]; then
97+
cbmc_args+=(--single-step --fail-upon-error)
98+
fi
99+
if [ "${{ inputs.report }}" = "true" ]; then
100+
cbmc_args+=(--output-result-json "$result_json")
101+
fi
102+
echo "::group::$group_name"
103+
tests cbmc "${cbmc_args[@]}" || cbmc_failed=true
58104
echo "::endgroup::"
59-
python3 ${{ github.action_path }}/report.py \
60-
--results-json "${{ github.workspace }}/cbmc_result_k${{ inputs.mlkem_k }}.json" \
61-
--mlkem-k "${{ inputs.mlkem_k }}" \
62-
--min-runtime 20 \
63-
--regression-threshold 1.5 \
64-
--gh-pages-branch gh-pages \
65-
--data-dir dev/cbmc
105+
if [ "${{ inputs.report }}" = "true" ]; then
106+
python3 ${{ github.action_path }}/report.py \
107+
--results-json "$result_json" \
108+
--mlkem-k "${{ inputs.mlkem_k }}" \
109+
--min-runtime 20 \
110+
--regression-threshold 1.5 \
111+
--gh-pages-branch gh-pages \
112+
--data-dir dev/cbmc
113+
fi
66114
if [ "$cbmc_failed" = "true" ]; then exit 1; fi

‎.github/workflows/cbmc.yml‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,3 +72,40 @@ jobs:
7272
cbmc: true
7373
cbmc_mlkem_k: 4
7474
secrets: inherit
75+
cbmc_target_model:
76+
name: CBMC target model (${{ matrix.cbmc_target }})
77+
if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
78+
permissions:
79+
contents: 'read'
80+
id-token: 'write'
81+
pull-requests: 'write'
82+
strategy:
83+
fail-fast: false
84+
matrix:
85+
cbmc_target:
86+
- i386-linux
87+
- x86_64-linux
88+
- aarch64-linux
89+
- riscv64-linux
90+
- ppc64le-linux
91+
uses: ./.github/workflows/ci_ec2_reusable.yml
92+
with:
93+
name: CBMC target model (${{ matrix.cbmc_target }})
94+
ec2_instance_type: r8g.xlarge
95+
ec2_ami: ubuntu-latest (aarch64)
96+
ec2_volume_size: 20
97+
compile_mode: native
98+
opt: no_opt
99+
lint: false
100+
verbose: true
101+
test: false
102+
cbmc: true
103+
cbmc_nix_shell: cbmc32
104+
cbmc_mlkem_k: 2
105+
cbmc_target: ${{ matrix.cbmc_target }}
106+
cbmc_proofs: cbmc_target_model
107+
cbmc_single_step: true
108+
cbmc_report: false
109+
cbmc_timeout: 300
110+
cbmc_per_proof_timeout: 300
111+
secrets: inherit

‎.github/workflows/ci_ec2_reusable.yml‎

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,9 +67,30 @@ on:
6767
slothy:
6868
type: boolean
6969
default: false
70+
cbmc_nix_shell:
71+
type: string
72+
default: cbmc
7073
cbmc_mlkem_k:
7174
type: string
7275
default: 2
76+
cbmc_target:
77+
type: string
78+
default: ''
79+
cbmc_proofs:
80+
type: string
81+
default: ''
82+
cbmc_single_step:
83+
type: boolean
84+
default: false
85+
cbmc_report:
86+
type: boolean
87+
default: true
88+
cbmc_timeout:
89+
type: string
90+
default: '3600'
91+
cbmc_per_proof_timeout:
92+
type: string
93+
default: '1800'
7394
env:
7495
AWS_ROLE: arn:aws:iam::559050233797:role/mlkem-c-aarch64-gh-action
7596
AWS_REGION: us-east-1
@@ -194,9 +215,15 @@ jobs:
194215
if: ${{ inputs.cbmc && (success() || failure()) }}
195216
uses: ./.github/actions/cbmc
196217
with:
197-
nix-shell: cbmc
218+
nix-shell: ${{ inputs.cbmc_nix_shell }}
198219
nix-verbose: ${{ inputs.verbose }}
199220
mlkem_k: ${{ inputs.cbmc_mlkem_k }}
221+
cbmc-target: ${{ inputs.cbmc_target }}
222+
proofs: ${{ inputs.cbmc_proofs }}
223+
single-step: ${{ inputs.cbmc_single_step }}
224+
report: ${{ inputs.cbmc_report }}
225+
timeout: ${{ inputs.cbmc_timeout }}
226+
per-proof-timeout: ${{ inputs.cbmc_per_proof_timeout }}
200227
gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
201228
- name: SLOTHY
202229
if: ${{ inputs.slothy }}

‎flake.nix‎

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -132,15 +132,16 @@
132132
packages = builtins.attrValues { inherit (config.packages) cbmc toolchains_native; } ++ [ pkgs.gh ];
133133
};
134134
devShells.cbmc32 = util.mkShell {
135-
packages = builtins.attrValues {
136-
inherit (config.packages)
137-
cbmc
138-
toolchain_i686
139-
toolchain_x86_64
140-
toolchain_aarch64
141-
toolchain_riscv64
142-
toolchain_ppc64le;
143-
} ++ [ pkgs.gh ];
135+
packages = builtins.attrValues
136+
{
137+
inherit (config.packages)
138+
cbmc
139+
toolchain_i686
140+
toolchain_x86_64
141+
toolchain_aarch64
142+
toolchain_riscv64
143+
toolchain_ppc64le;
144+
} ++ [ pkgs.gh ];
144145
};
145146
devShells.slothy = util.mkShell {
146147
packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; };

‎proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,5 @@
11
#!/usr/bin/env sh
2+
# Copyright (c) The mlkem-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
25
exec aarch64-unknown-linux-gnu-gcc "$@"

‎proofs/cbmc/tools/i686-gcc-as-gcc/gcc‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,5 @@
11
#!/usr/bin/env sh
2+
# Copyright (c) The mlkem-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
25
exec i686-unknown-linux-gnu-gcc "$@"

‎proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,5 @@
11
#!/usr/bin/env sh
2+
# Copyright (c) The mlkem-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
25
exec powerpc64le-unknown-linux-gnu-gcc "$@"

‎proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,5 @@
11
#!/usr/bin/env sh
2+
# Copyright (c) The mlkem-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
25
exec riscv64-unknown-linux-gnu-gcc "$@"

‎proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,5 @@
11
#!/usr/bin/env sh
2+
# Copyright (c) The mlkem-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
25
exec x86_64-unknown-linux-gnu-gcc "$@"

0 commit comments

Comments
 (0)