Add CBMC target platform support

.github/actions/cbmc/action.yml

@@ -24,6 +24,24 @@ inputs:
   reduce_ram:
     description: "Run CBMC proofs with MLD_CONFIG_REDUCE_RAM enabled"
     default: "false"
+  cbmc-target:
+    description: "CBMC target platform; empty uses the default host model"
+    default: ""
+  proofs:
+    description: "Space-separated proof patterns to run; empty runs all proofs"
+    default: ""
+  single-step:
+    description: "Run proofs one at a time"
+    default: "false"
+  timeout:
+    description: "Timeout for individual CBMC proofs, in seconds"
+    default: "3600"
+  per-proof-timeout:
+    description: "Timeout passed to run-cbmc-proofs.py for each proof"
+    default: "1800"
+  report:
+    description: "Publish CBMC runtime regression report"
+    default: "true"
   gh_token:
     description: Github access token to use
     required: true
@@ -57,23 +75,52 @@ runs:
         env:
           GH_TOKEN: ${{ inputs.gh_token }}
         run: |
-          echo "::group::cbmc_${{ inputs.mldsa_parameter_set }}"
-          reduce_ram_flag=""
+          cbmc_failed=false
+          cbmc_target="${{ inputs.cbmc-target }}"
+          group_name="cbmc_${{ inputs.mldsa_parameter_set }}"
+          result_suffix=""
+          if [ -n "$cbmc_target" ]; then
+            group_name="${group_name}_${cbmc_target}"
+            result_suffix="_${cbmc_target//[^A-Za-z0-9_.-]/_}"
+          fi
+          result_json="${{ github.workspace }}/cbmc_result_${{ inputs.mldsa_parameter_set }}${result_suffix}.json"
+          cbmc_args=(
+            --mldsa-parameter-set "${{ inputs.mldsa_parameter_set }}"
+            --timeout "${{ inputs.timeout }}"
+            --per-proof-timeout "${{ inputs.per-proof-timeout }}"
+          )
           data_dir="dev/cbmc"
           variant=""
           if [ "${{ inputs.reduce_ram }}" = "true" ]; then
-            reduce_ram_flag="--reduce-ram"
+            cbmc_args+=(--reduce-ram)
             data_dir="dev/cbmc-reduce-ram"
             variant="reduce-ram"
           fi
-          tests cbmc --mldsa-parameter-set ${{ inputs.mldsa_parameter_set }} --per-proof-timeout 1800 --output-result-json ${{ github.workspace }}/cbmc_result_${{ inputs.mldsa_parameter_set }}.json $reduce_ram_flag || cbmc_failed=true
+          if [ -n "$cbmc_target" ]; then
+            cbmc_args+=(--cbmc-target "$cbmc_target")
+          fi
+          proofs="${{ inputs.proofs }}"
+          if [ -n "$proofs" ]; then
+            read -r -a proof_args <<< "$proofs"
+            cbmc_args+=(-p "${proof_args[@]}")
+          fi
+          if [ "${{ inputs.single-step }}" = "true" ]; then
+            cbmc_args+=(--single-step --fail-upon-error)
+          fi
+          if [ "${{ inputs.report }}" = "true" ]; then
+            cbmc_args+=(--output-result-json "$result_json")
+          fi
+          echo "::group::$group_name"
+          tests cbmc "${cbmc_args[@]}" || cbmc_failed=true
           echo "::endgroup::"
-          python3 ${{ github.action_path }}/report.py \
-            --results-json "${{ github.workspace }}/cbmc_result_${{ inputs.mldsa_parameter_set }}.json" \
-            --mldsa-parameter-set "${{ inputs.mldsa_parameter_set }}" \
-            --min-runtime 20 \
-            --regression-threshold 1.5 \
-            --gh-pages-branch gh-pages \
-            --data-dir "$data_dir" \
-            --variant "$variant"
+          if [ "${{ inputs.report }}" = "true" ]; then
+            python3 ${{ github.action_path }}/report.py \
+              --results-json "$result_json" \
+              --mldsa-parameter-set "${{ inputs.mldsa_parameter_set }}" \
+              --min-runtime 20 \
+              --regression-threshold 1.5 \
+              --gh-pages-branch gh-pages \
+              --data-dir "$data_dir" \
+              --variant "$variant"
+          fi
           if [ "$cbmc_failed" = "true" ]; then exit 1; fi

.github/workflows/cbmc.yml

@@ -38,3 +38,43 @@ jobs:
       cbmc_mldsa_parameter_set: ${{ matrix.parameter_set }}
       cbmc_reduce_ram: ${{ matrix.reduce_ram }}
     secrets: inherit
+  cbmc_target_model:
+    name: CBMC target model (${{ matrix.cbmc_target }})
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+      pull-requests: 'write'
+    strategy:
+      fail-fast: false
+      matrix:
+        cbmc_target:
+          - i386-linux
+          - x86_64-linux
+          - aarch64-linux
+          - riscv64-linux
+          - ppc64le-linux
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC target model (${{ matrix.cbmc_target }})
+      ec2_instance_type: c7g.4xlarge
+      ec2_ami: ubuntu-latest (aarch64)
+      ec2_volume_size: 20
+      compile_mode: native
+      opt: no_opt
+      lint: false
+      verbose: true
+      functest: false
+      kattest: false
+      acvptest: false
+      cbmc: true
+      cbmc_nix_shell: cbmc32
+      cbmc_mldsa_parameter_set: 44
+      cbmc_reduce_ram: false
+      cbmc_target: ${{ matrix.cbmc_target }}
+      cbmc_proofs: cbmc_target_model
+      cbmc_single_step: true
+      cbmc_report: false
+      cbmc_timeout: 300
+      cbmc_per_proof_timeout: 300
+    secrets: inherit

.github/workflows/ci_ec2_reusable.yml

@@ -68,12 +68,33 @@ on:
       slothy:
         type: boolean
         default: false
+      cbmc_nix_shell:
+        type: string
+        default: cbmc
       cbmc_mldsa_parameter_set:
         type: string
         default: 44
       cbmc_reduce_ram:
         type: boolean
         default: false
+      cbmc_target:
+        type: string
+        default: ''
+      cbmc_proofs:
+        type: string
+        default: ''
+      cbmc_single_step:
+        type: boolean
+        default: false
+      cbmc_report:
+        type: boolean
+        default: true
+      cbmc_timeout:
+        type: string
+        default: '3600'
+      cbmc_per_proof_timeout:
+        type: string
+        default: '1800'
 env:
   AWS_ROLE: arn:aws:iam::904233116199:role/mldsa-native-ci
   AWS_REGION: us-east-1
@@ -200,10 +221,16 @@ jobs:
         if: ${{ inputs.cbmc && (success() || failure()) }}
         uses: ./.github/actions/cbmc
         with:
-          nix-shell: cbmc
+          nix-shell: ${{ inputs.cbmc_nix_shell }}
           nix-verbose: ${{ inputs.verbose }}
           mldsa_parameter_set: ${{ inputs.cbmc_mldsa_parameter_set }}
           reduce_ram: ${{ inputs.cbmc_reduce_ram }}
+          cbmc-target: ${{ inputs.cbmc_target }}
+          proofs: ${{ inputs.cbmc_proofs }}
+          single-step: ${{ inputs.cbmc_single_step }}
+          report: ${{ inputs.cbmc_report }}
+          timeout: ${{ inputs.cbmc_timeout }}
+          per-proof-timeout: ${{ inputs.cbmc_per_proof_timeout }}
           gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
       - name: SLOTHY
         if: ${{ inputs.slothy }}

flake.nix

@@ -79,6 +79,7 @@
           packages.toolchains = util.toolchains;
           packages.toolchains_native = util.toolchains_native;
           packages.toolchain_x86_64 = util.toolchain_x86_64;
+          packages.toolchain_i686 = util.toolchain_i686;
           packages.toolchain_aarch64 = util.toolchain_aarch64;
           packages.toolchain_riscv64 = util.toolchain_riscv64;
           packages.toolchain_riscv32 = util.toolchain_riscv32;
@@ -116,6 +117,18 @@
           devShells.cbmc = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) cbmc toolchains_native; } ++ [ pkgs.gh ];
           };
+          devShells.cbmc32 = util.mkShell {
+            packages = builtins.attrValues
+              {
+                inherit (config.packages)
+                  cbmc
+                  toolchain_i686
+                  toolchain_x86_64
+                  toolchain_aarch64
+                  toolchain_riscv64
+                  toolchain_ppc64le;
+              } ++ [ pkgs.gh ];
+          };
           devShells.slothy = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; };
           };

nix/util.nix

@@ -34,6 +34,7 @@ rec {
   _toolchains = { cross ? true }:
     let
       x86_64-gcc = wrap-gcc pkgs.pkgsCross.gnu64;
+      i686-gcc = wrap-gcc pkgs.pkgsCross.gnu32;
       aarch64-gcc = wrap-gcc pkgs.pkgsCross.aarch64-multiplatform;
       riscv64-gcc = wrap-gcc pkgs.pkgsCross.riscv64;
       riscv32-gcc = wrap-gcc pkgs.pkgsCross.riscv32;
@@ -47,7 +48,7 @@ rec {
       #   and won't just work for now
       # - equip all toolchains if cross is explicitly set to true
       # - On some machines, `native-gcc` needed to be evaluated lastly (placed as the last element of the toolchain list), or else would result in environment variables (CC, AR, ...) overriding issue.
-    pkgs.lib.optionals cross [ pkgs.qemu pkgs.gcc-arm-embedded x86_64-gcc aarch64-gcc riscv64-gcc riscv32-gcc ppc64le-gcc ]
+    pkgs.lib.optionals cross [ pkgs.qemu pkgs.gcc-arm-embedded x86_64-gcc i686-gcc aarch64-gcc riscv64-gcc riscv32-gcc ppc64le-gcc ]
     ++ pkgs.lib.optionals (cross && pkgs.stdenv.isLinux && pkgs.stdenv.isx86_64) [ aarch64_be-gcc ]
     ++ pkgs.lib.optionals cross [ native-gcc ]
     # git is not available in the nix shell on Darwin. As a workaround we add git as a dependency here.
@@ -133,6 +134,11 @@ rec {
     cross_compilers = [ (wrap-gcc pkgs.pkgsCross.gnu64) ];
   };
 
+  toolchain_i686 = _individual_toolchain {
+    name = "i686";
+    cross_compilers = [ (wrap-gcc pkgs.pkgsCross.gnu32) ];
+  };
+
   toolchain_aarch64 = _individual_toolchain {
     name = "aarch64";
     cross_compilers = [ (wrap-gcc pkgs.pkgsCross.aarch64-multiplatform) ];