diff --git a/.github/actions/cbmc/action.yml b/.github/actions/cbmc/action.yml index f8cc38b64..d4652f48b 100644 --- a/.github/actions/cbmc/action.yml +++ b/.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 diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml index bb791f036..ff14479b1 100644 --- a/.github/workflows/cbmc.yml +++ b/.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 diff --git a/.github/workflows/ci_ec2_reusable.yml b/.github/workflows/ci_ec2_reusable.yml index 81767dcf1..2c7f9f029 100644 --- a/.github/workflows/ci_ec2_reusable.yml +++ b/.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 }} diff --git a/flake.nix b/flake.nix index bdf72ebf2..0e3b273fb 100644 --- a/flake.nix +++ b/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; }; }; diff --git a/nix/util.nix b/nix/util.nix index 1d7c74980..b992573a3 100644 --- a/nix/util.nix +++ b/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) ]; diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common index a8acb5bf4..68adccfc7 100644 --- a/proofs/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -329,9 +329,91 @@ CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK) # initialized with unconstrained values. NONDET_STATIC ?= +# Target platform for CBMC/goto-cc. Leave unset to preserve the historic +# host-default model. +CBMC_TARGET ?= +CBMC_TARGET_CC ?= +CBMC_TARGET_GOTO_FLAGS ?= +CBMC_TARGET_CBMC_FLAGS ?= +CBMC_TARGET_INSTRUMENT_ENV ?= +CBMC_TARGET_GCC_AS_GCC_DIR ?= +CBMC_TARGET_HOST_PATH ?= $(shell printf '%s' "$$PATH") +CBMC_TARGET_POINTER_BYTES ?= 8 +CBMC_TARGET_SIZE_T_BYTES ?= 8 +CBMC_TARGET_LONG_BYTES ?= 8 + +ifeq ($(strip $(CBMC_TARGET)),) + ifeq ($(strip $(CBMC_TARGET_CC)),) + CBMC_TARGET_CC = $(CC) + endif +else ifeq ($(CBMC_TARGET),i386-linux) + ifeq ($(strip $(CBMC_TARGET_CC)),) + CBMC_TARGET_CC = i686-unknown-linux-gnu-gcc + endif + CBMC_TARGET_GOTO_FLAGS = --i386-linux + CBMC_TARGET_CBMC_FLAGS = --i386-linux + ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),) + CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/i686-gcc-as-gcc + endif + CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC) + CBMC_TARGET_POINTER_BYTES = 4 + CBMC_TARGET_SIZE_T_BYTES = 4 + CBMC_TARGET_LONG_BYTES = 4 +else ifeq ($(CBMC_TARGET),x86_64-linux) + ifeq ($(strip $(CBMC_TARGET_CC)),) + CBMC_TARGET_CC = x86_64-unknown-linux-gnu-gcc + endif + CBMC_TARGET_CBMC_FLAGS = --arch x86_64 --os linux --LP64 + ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),) + CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/x86_64-gcc-as-gcc + endif + CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC) + CBMC_TARGET_POINTER_BYTES = 8 + CBMC_TARGET_SIZE_T_BYTES = 8 + CBMC_TARGET_LONG_BYTES = 8 +else ifeq ($(CBMC_TARGET),aarch64-linux) + ifeq ($(strip $(CBMC_TARGET_CC)),) + CBMC_TARGET_CC = aarch64-unknown-linux-gnu-gcc + endif + CBMC_TARGET_CBMC_FLAGS = --arch arm64 --os linux --LP64 + ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),) + CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/aarch64-gcc-as-gcc + endif + CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC) + CBMC_TARGET_POINTER_BYTES = 8 + CBMC_TARGET_SIZE_T_BYTES = 8 + CBMC_TARGET_LONG_BYTES = 8 +else ifeq ($(CBMC_TARGET),riscv64-linux) + ifeq ($(strip $(CBMC_TARGET_CC)),) + CBMC_TARGET_CC = riscv64-unknown-linux-gnu-gcc + endif + CBMC_TARGET_CBMC_FLAGS = --arch riscv64 --os linux --LP64 + ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),) + CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/riscv64-gcc-as-gcc + endif + CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC) + CBMC_TARGET_POINTER_BYTES = 8 + CBMC_TARGET_SIZE_T_BYTES = 8 + CBMC_TARGET_LONG_BYTES = 8 +else ifeq ($(CBMC_TARGET),ppc64le-linux) + ifeq ($(strip $(CBMC_TARGET_CC)),) + CBMC_TARGET_CC = powerpc64le-unknown-linux-gnu-gcc + endif + CBMC_TARGET_CBMC_FLAGS = --arch ppc64le --os linux --LP64 + ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),) + CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/ppc64le-gcc-as-gcc + endif + CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC) + CBMC_TARGET_POINTER_BYTES = 8 + CBMC_TARGET_SIZE_T_BYTES = 8 + CBMC_TARGET_LONG_BYTES = 8 +else + $(error Unsupported CBMC_TARGET '$(CBMC_TARGET)'; expected i386-linux, x86_64-linux, aarch64-linux, riscv64-linux, ppc64le-linux, or unset) +endif + # Flags to pass to goto-cc for compilation and linking -COMPILE_FLAGS ?= -Wall -Werror --native-compiler $(CC) -LINK_FLAGS ?= -Wall -Werror +COMPILE_FLAGS ?= -Wall -Werror $(CBMC_TARGET_GOTO_FLAGS) --native-compiler $(CBMC_TARGET_CC) +LINK_FLAGS ?= -Wall -Werror $(CBMC_TARGET_GOTO_FLAGS) EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols # During instrumentation, it adds models of C library functions @@ -585,6 +667,7 @@ endif ################################################################ # CBMC flags common to all proofs CBMCFLAGS += $(CBMC_FLAG_FLUSH) +CBMCFLAGS += $(CBMC_TARGET_CBMC_FLAGS) CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS) CBMCFLAGS += --slice-formula @@ -594,6 +677,9 @@ CBMCFLAGS += --slice-formula DEFINES += -DCBMC=1 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS) DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))" +DEFINES += -DCBMC_TARGET_POINTER_BYTES=$(CBMC_TARGET_POINTER_BYTES) +DEFINES += -DCBMC_TARGET_SIZE_T_BYTES=$(CBMC_TARGET_SIZE_T_BYTES) +DEFINES += -DCBMC_TARGET_LONG_BYTES=$(CBMC_TARGET_LONG_BYTES) ifndef MLD_CONFIG_PARAMETER_SET $(error MLD_CONFIG_PARAMETER_SET not set) @@ -742,7 +828,7 @@ $(PROOF_GOTO)0100.goto: $(PROOF_SOURCES) $(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/remove_function_body-log.txt \ @@ -765,7 +851,7 @@ $(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto $(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \ @@ -787,7 +873,7 @@ ifneq ($(strip $(CODE_CONTRACTS)),) else $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/nondet_static-log.txt \ @@ -801,7 +887,7 @@ $(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/linking-library-models-log.txt \ @@ -824,7 +910,7 @@ $(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/unwind_loops-log.txt \ @@ -834,7 +920,7 @@ ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) else ifneq ($(strip $(CODE_CONTRACTS)),) $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/unwind_loops-log.txt \ @@ -856,7 +942,7 @@ endif $(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ @@ -868,7 +954,7 @@ $(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto $(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/slice_global_inits-log.txt \ @@ -880,7 +966,7 @@ $(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto $(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ + '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \ diff --git a/proofs/cbmc/cbmc_target_model/Makefile b/proofs/cbmc/cbmc_target_model/Makefile new file mode 100644 index 000000000..bf63bfed2 --- /dev/null +++ b/proofs/cbmc/cbmc_target_model/Makefile @@ -0,0 +1,21 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = cbmc_target_model_harness + +PROOF_UID = mld_cbmc_target_model + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(PROOFDIR)/cbmc_target_model_project.c + +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = harness + +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c b/proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c new file mode 100644 index 000000000..1bd11706a --- /dev/null +++ b/proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include + +void __CPROVER_assert(_Bool, const char *); + +void harness(void) +{ + __CPROVER_assert(sizeof(void *) == CBMC_TARGET_POINTER_BYTES, + "CBMC target pointer width matches selected model"); + __CPROVER_assert(sizeof(size_t) == CBMC_TARGET_SIZE_T_BYTES, + "CBMC target size_t width matches selected model"); + __CPROVER_assert(sizeof(long) == CBMC_TARGET_LONG_BYTES, + "CBMC target long width matches selected model"); + __CPROVER_assert(sizeof(uint64_t) == 8, + "CBMC target uint64_t width is 8 bytes"); +} diff --git a/proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c b/proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c new file mode 100644 index 000000000..86360d0d2 --- /dev/null +++ b/proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c @@ -0,0 +1,4 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +int cbmc_target_model_project_anchor; diff --git a/proofs/cbmc/ntt_butterfly_block/Makefile b/proofs/cbmc/ntt_butterfly_block/Makefile index ae4b238e9..385e97bee 100644 --- a/proofs/cbmc/ntt_butterfly_block/Makefile +++ b/proofs/cbmc/ntt_butterfly_block/Makefile @@ -26,7 +26,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--smt2 FUNCTION_NAME = mld_ntt_butterfly_block diff --git a/proofs/cbmc/rej_eta_native/Makefile b/proofs/cbmc/rej_eta_native/Makefile index 76fb0b117..627ecfd24 100644 --- a/proofs/cbmc/rej_eta_native/Makefile +++ b/proofs/cbmc/rej_eta_native/Makefile @@ -33,7 +33,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--smt2 FUNCTION_NAME = mld_rej_eta_native diff --git a/proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc b/proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc new file mode 100755 index 000000000..98c6946f7 --- /dev/null +++ b/proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc @@ -0,0 +1,5 @@ +#!/usr/bin/env sh +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +exec aarch64-unknown-linux-gnu-gcc "$@" diff --git a/proofs/cbmc/tools/i686-gcc-as-gcc/gcc b/proofs/cbmc/tools/i686-gcc-as-gcc/gcc new file mode 100755 index 000000000..1cda83e21 --- /dev/null +++ b/proofs/cbmc/tools/i686-gcc-as-gcc/gcc @@ -0,0 +1,5 @@ +#!/usr/bin/env sh +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +exec i686-unknown-linux-gnu-gcc "$@" diff --git a/proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc b/proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc new file mode 100755 index 000000000..182606cf1 --- /dev/null +++ b/proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc @@ -0,0 +1,5 @@ +#!/usr/bin/env sh +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +exec powerpc64le-unknown-linux-gnu-gcc "$@" diff --git a/proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc b/proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc new file mode 100755 index 000000000..5e18ae185 --- /dev/null +++ b/proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc @@ -0,0 +1,5 @@ +#!/usr/bin/env sh +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +exec riscv64-unknown-linux-gnu-gcc "$@" diff --git a/proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc b/proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc new file mode 100755 index 000000000..18264ef19 --- /dev/null +++ b/proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc @@ -0,0 +1,5 @@ +#!/usr/bin/env sh +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +exec x86_64-unknown-linux-gnu-gcc "$@" diff --git a/scripts/tests b/scripts/tests index c6f1cad32..b354f18bf 100755 --- a/scripts/tests +++ b/scripts/tests @@ -418,7 +418,7 @@ class Tests: return res def make_j(self): - if self.args.j is None or int(self.args.j) == 1: + if self.args.j is None: return [] return [f"-j{self.args.j}"] @@ -918,8 +918,14 @@ class Tests: print(p) exit(0) - def run_cbmc_single_step(mldsa_parameter_set, proofs): + def cbmc_envvars(mldsa_parameter_set): envvars = {"MLD_CONFIG_PARAMETER_SET": mldsa_parameter_set} + if self.args.cbmc_target is not None: + envvars["CBMC_TARGET"] = self.args.cbmc_target + return envvars + + def run_cbmc_single_step(mldsa_parameter_set, proofs): + envvars = cbmc_envvars(mldsa_parameter_set) if self.args.reduce_ram: envvars["MLD_CONFIG_REDUCE_RAM"] = "1" scheme = SCHEME.from_mode(mldsa_parameter_set) @@ -990,7 +996,7 @@ class Tests: if self.args.single_step: run_cbmc_single_step(mldsa_parameter_set, proofs) return - envvars = {"MLD_CONFIG_PARAMETER_SET": mldsa_parameter_set} + envvars = cbmc_envvars(mldsa_parameter_set) if self.args.reduce_ram: envvars["MLD_CONFIG_REDUCE_RAM"] = "1" cmd = ( @@ -1471,6 +1477,19 @@ def cli(): default=None, ) + cbmc_parser.add_argument( + "--cbmc-target", + help="CBMC target platform; omit to use the default host model", + choices=[ + "i386-linux", + "x86_64-linux", + "aarch64-linux", + "riscv64-linux", + "ppc64le-linux", + ], + default=None, + ) + cbmc_parser.add_argument( "--reduce-ram", help="Run CBMC proofs with MLD_CONFIG_REDUCE_RAM enabled",