From 3cdab5c670b0c6b74b32302f8df62e3b339f7568 Mon Sep 17 00:00:00 2001 From: Joe Doyle Date: Thu, 25 Jun 2026 21:26:59 -0400 Subject: [PATCH 1/2] Add CBMC target platform support Add explicit CBMC target platform selection for the proof infrastructure, including i386 Linux support with an i686 preprocessor and matching target-model flags. Add target compiler shims for goto-instrument, a target ABI canary proof, and the solver/proof configuration tweaks needed by the 32-bit ML-DSA suite. Verification: git diff --check; python3 -B -m py_compile scripts/tests proofs/cbmc/run-cbmc-proofs.py; ./scripts/tests cbmc --help target list; canary dry-runs for i386-linux, x86_64-linux, aarch64-linux, riscv64-linux, riscv32-linux, and ppc64le-linux; nix eval --raw .#devShells.aarch64-linux.cbmc32.drvPath. Signed-off-by: Joe Doyle Co-authored-by: Codex --- flake.nix | 13 ++ nix/util.nix | 8 +- proofs/cbmc/Makefile.common | 120 ++++++++++++++++-- proofs/cbmc/cbmc_target_model/Makefile | 21 +++ .../cbmc_target_model_harness.c | 19 +++ .../cbmc_target_model_project.c | 4 + proofs/cbmc/ntt_butterfly_block/Makefile | 2 +- proofs/cbmc/rej_eta_native/Makefile | 2 +- proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc | 2 + proofs/cbmc/tools/i686-gcc-as-gcc/gcc | 2 + proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc | 2 + proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc | 2 + proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc | 2 + proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc | 2 + scripts/tests | 26 +++- 15 files changed, 210 insertions(+), 17 deletions(-) create mode 100644 proofs/cbmc/cbmc_target_model/Makefile create mode 100644 proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c create mode 100644 proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c create mode 100755 proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc create mode 100755 proofs/cbmc/tools/i686-gcc-as-gcc/gcc create mode 100755 proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc create mode 100755 proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc create mode 100755 proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc create mode 100755 proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc diff --git a/flake.nix b/flake.nix index bdf72ebf2..f75362b72 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_riscv32 + 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..49f99b89e 100644 --- a/proofs/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -329,9 +329,103 @@ 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),riscv32-linux) + ifeq ($(strip $(CBMC_TARGET_CC)),) + CBMC_TARGET_CC = riscv32-unknown-linux-gnu-gcc + endif + CBMC_TARGET_CBMC_FLAGS = --arch riscv32 --os linux --ILP32 + ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),) + CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/riscv32-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),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, riscv32-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 +679,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 +689,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 +840,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 +863,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 +885,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 +899,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 +922,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 +932,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 +954,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 +966,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 +978,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..122df37cb --- /dev/null +++ b/proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +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..758ec4ca4 --- /dev/null +++ b/proofs/cbmc/tools/i686-gcc-as-gcc/gcc @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +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..dc900ad17 --- /dev/null +++ b/proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +exec powerpc64le-unknown-linux-gnu-gcc "$@" diff --git a/proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc b/proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc new file mode 100755 index 000000000..00be2eef8 --- /dev/null +++ b/proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +exec riscv32-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..caf1b650b --- /dev/null +++ b/proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +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..cddc4a90c --- /dev/null +++ b/proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +exec x86_64-unknown-linux-gnu-gcc "$@" diff --git a/scripts/tests b/scripts/tests index c6f1cad32..1ee9371dd 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,20 @@ 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", + "riscv32-linux", + "ppc64le-linux", + ], + default=None, + ) + cbmc_parser.add_argument( "--reduce-ram", help="Run CBMC proofs with MLD_CONFIG_REDUCE_RAM enabled", From 6f25dae5e4ec282d5b67ecb1c7680376c59be74c Mon Sep 17 00:00:00 2001 From: Joe Doyle Date: Thu, 25 Jun 2026 21:38:01 -0400 Subject: [PATCH 2/2] Drop unsupported riscv32 CBMC target Remove riscv32-linux from the CBMC target platform list because this CBMC toolchain does not support that architecture model. Keep the regular repository cross-riscv32 shell untouched; only the CBMC target interface and cbmc32 proof shell are narrowed. Verification: git diff --check; python3 -B -m py_compile scripts/tests proofs/cbmc/run-cbmc-proofs.py; ./scripts/tests cbmc --help target list; canary dry-runs for i386-linux, x86_64-linux, aarch64-linux, riscv64-linux, and ppc64le-linux; nix eval --raw .#devShells.aarch64-linux.cbmc32.drvPath. Signed-off-by: Joe Doyle Co-authored-by: Codex --- flake.nix | 1 - proofs/cbmc/Makefile.common | 14 +------------- proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc | 2 -- scripts/tests | 1 - 4 files changed, 1 insertion(+), 17 deletions(-) delete mode 100755 proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc diff --git a/flake.nix b/flake.nix index f75362b72..6c6245f60 100644 --- a/flake.nix +++ b/flake.nix @@ -125,7 +125,6 @@ toolchain_x86_64 toolchain_aarch64 toolchain_riscv64 - toolchain_riscv32 toolchain_ppc64le; } ++ [ pkgs.gh ]; }; diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common index 49f99b89e..68adccfc7 100644 --- a/proofs/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -395,18 +395,6 @@ else ifeq ($(CBMC_TARGET),riscv64-linux) CBMC_TARGET_POINTER_BYTES = 8 CBMC_TARGET_SIZE_T_BYTES = 8 CBMC_TARGET_LONG_BYTES = 8 -else ifeq ($(CBMC_TARGET),riscv32-linux) - ifeq ($(strip $(CBMC_TARGET_CC)),) - CBMC_TARGET_CC = riscv32-unknown-linux-gnu-gcc - endif - CBMC_TARGET_CBMC_FLAGS = --arch riscv32 --os linux --ILP32 - ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),) - CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/riscv32-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),ppc64le-linux) ifeq ($(strip $(CBMC_TARGET_CC)),) CBMC_TARGET_CC = powerpc64le-unknown-linux-gnu-gcc @@ -420,7 +408,7 @@ else ifeq ($(CBMC_TARGET),ppc64le-linux) 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, riscv32-linux, ppc64le-linux, or unset) + $(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 diff --git a/proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc b/proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc deleted file mode 100755 index 00be2eef8..000000000 --- a/proofs/cbmc/tools/riscv32-gcc-as-gcc/gcc +++ /dev/null @@ -1,2 +0,0 @@ -#!/usr/bin/env sh -exec riscv32-unknown-linux-gnu-gcc "$@" diff --git a/scripts/tests b/scripts/tests index 1ee9371dd..b354f18bf 100755 --- a/scripts/tests +++ b/scripts/tests @@ -1485,7 +1485,6 @@ def cli(): "x86_64-linux", "aarch64-linux", "riscv64-linux", - "riscv32-linux", "ppc64le-linux", ], default=None,