Skip to content

Add CBMC target platform support #1200

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
tob-joe wants to merge 2 commits into from
Closed

Add CBMC target platform support #1200

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3cdab5c
Add CBMC target platform support
tob-joe Jun 26, 2026
6f25dae
Drop unsupported riscv32 CBMC target
tob-joe Jun 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions flake.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Copyright (c) The mlkem-native project authors

Check failure on line 1 in flake.nix

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-latest)

Format error 

/home/runner/work/mldsa-native/mldsa-native/flake.nix require to be formatted

Check failure on line 1 in flake.nix

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-24.04-arm)

Format error 

/home/runner/work/mldsa-native/mldsa-native/flake.nix require to be formatted
# Copyright (c) The mldsa-native project authors
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -116,6 +117,17 @@
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; };
};
Expand Down
8 changes: 7 additions & 1 deletion nix/util.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.
Expand Down Expand Up @@ -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) ];
Expand Down
108 changes: 97 additions & 11 deletions proofs/cbmc/Makefile.common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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)
Expand Down Expand Up @@ -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 \
Expand All @@ -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 \
Expand All @@ -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 \
Expand All @@ -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 \
Expand All @@ -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 \
Expand All @@ -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 \
Expand All @@ -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 \
Expand All @@ -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 \
Expand All @@ -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 \
Expand Down
21 changes: 21 additions & 0 deletions proofs/cbmc/cbmc_target_model/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
19 changes: 19 additions & 0 deletions proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// Copyright (c) The mldsa-native project authors
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT

#include <stddef.h>
#include <stdint.h>

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");
}
4 changes: 4 additions & 0 deletions proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
2 changes: 1 addition & 1 deletion proofs/cbmc/ntt_butterfly_block/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/rej_eta_native/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 2 additions & 0 deletions proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#!/usr/bin/env sh

Check failure on line 1 in proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-latest)

Missing license header error 

proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc is missing SPDX License header

Check failure on line 1 in proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-24.04-arm)

Missing license header error 

proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc is missing SPDX License header
exec aarch64-unknown-linux-gnu-gcc "$@"
2 changes: 2 additions & 0 deletions proofs/cbmc/tools/i686-gcc-as-gcc/gcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#!/usr/bin/env sh

Check failure on line 1 in proofs/cbmc/tools/i686-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-latest)

Missing license header error 

proofs/cbmc/tools/i686-gcc-as-gcc/gcc is missing SPDX License header

Check failure on line 1 in proofs/cbmc/tools/i686-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-24.04-arm)

Missing license header error 

proofs/cbmc/tools/i686-gcc-as-gcc/gcc is missing SPDX License header
exec i686-unknown-linux-gnu-gcc "$@"
2 changes: 2 additions & 0 deletions proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#!/usr/bin/env sh

Check failure on line 1 in proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-latest)

Missing license header error 

proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc is missing SPDX License header

Check failure on line 1 in proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-24.04-arm)

Missing license header error 

proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc is missing SPDX License header
exec powerpc64le-unknown-linux-gnu-gcc "$@"
2 changes: 2 additions & 0 deletions proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#!/usr/bin/env sh

Check failure on line 1 in proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-latest)

Missing license header error 

proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc is missing SPDX License header

Check failure on line 1 in proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-24.04-arm)

Missing license header error 

proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc is missing SPDX License header
exec riscv64-unknown-linux-gnu-gcc "$@"
2 changes: 2 additions & 0 deletions proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#!/usr/bin/env sh

Check failure on line 1 in proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-latest)

Missing license header error 

proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc is missing SPDX License header

Check failure on line 1 in proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc

View workflow job for this annotation

GitHub Actions / Base / Linting (ubuntu-24.04-arm)

Missing license header error 

proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc is missing SPDX License header
exec x86_64-unknown-linux-gnu-gcc "$@"
25 changes: 22 additions & 3 deletions scripts/tests
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}"]

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 = (
Expand Down Expand Up @@ -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",
Expand Down
Loading