From 25be4ece467a2bfa70b8115d44c01b8d5ff12176 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Thu, 12 Feb 2026 09:44:43 +0800 Subject: [PATCH 1/2] Nix: Update CBCM to experimental branch See https://github.com/diffblue/cbmc/pull/8830 Signed-off-by: Matthias J. Kannwischer --- flake.nix | 6 ++- ...002-Do-not-download-sources-in-cmake.patch | 53 +++++++++++++++++++ nix/cbmc/default.nix | 18 +++++-- nix/util.nix | 4 +- 4 files changed, 72 insertions(+), 9 deletions(-) create mode 100644 nix/cbmc/0002-Do-not-download-sources-in-cmake.patch diff --git a/flake.nix b/flake.nix index c89aee94e..56883e412 100644 --- a/flake.nix +++ b/flake.nix @@ -25,7 +25,8 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system}; pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system}; util = pkgs.callPackage ./nix/util.nix { - inherit (pkgs) cbmc bitwuzla z3; + inherit (pkgs-unstable) cbmc cadical; + inherit (pkgs) bitwuzla z3; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; }; @@ -222,7 +223,8 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux; util = pkgs.callPackage ./nix/util.nix { inherit pkgs; - inherit (pkgs) cbmc bitwuzla z3; + inherit (pkgs-unstable) cbmc cadical; + inherit (pkgs) bitwuzla z3; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; }; diff --git a/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch b/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch new file mode 100644 index 000000000..89456d8ae --- /dev/null +++ b/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch @@ -0,0 +1,53 @@ +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +From c6b6438d3c87ce000b4e80b2eda2389e9473d24c Mon Sep 17 00:00:00 2001 +From: wxt <3264117476@qq.com> +Date: Mon, 11 Nov 2024 11:35:03 +0800 +Subject: [PATCH] Do not download sources in cmake + +--- + src/solvers/CMakeLists.txt | 9 +++------ + 1 file changed, 3 insertions(+), 6 deletions(-) + +diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt +index ab8d111..d7165e2 100644 +--- a/src/solvers/CMakeLists.txt ++++ b/src/solvers/CMakeLists.txt +@@ -102,10 +102,9 @@ foreach(SOLVER ${sat_impl}) + message(STATUS "Building solvers with glucose") + + download_project(PROJ glucose +- URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz ++ SOURCE_DIR @srcglucose@ + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt +- URL_MD5 7c539c62c248b74210aef7414787323a + ) + + add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR}) +@@ -121,11 +120,10 @@ foreach(SOLVER ${sat_impl}) + message(STATUS "Building solvers with cadical") + + download_project(PROJ cadical +- URL https://github.com/arminbiere/cadical/archive/rel-3.0.0.tar.gz ++ SOURCE_DIR @srccadical@ + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-3.0.0-patch + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt + COMMAND ./configure +- URL_HASH SHA256=282b1c9422fde8631cb721b86450ae94df4e8de0545c17a69a301aaa4bf92fcf + ) + + add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) +@@ -144,10 +142,9 @@ foreach(SOLVER ${sat_impl}) + message(STATUS "Building with IPASIR solver linking against: CaDiCaL") + + download_project(PROJ cadical +- URL https://github.com/arminbiere/cadical/archive/rel-3.0.0.tar.gz ++ SOURCE_DIR @srccadical@ + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-3.0.0-patch + COMMAND ./configure +- URL_HASH SHA256=282b1c9422fde8631cb721b86450ae94df4e8de0545c17a69a301aaa4bf92fcf + ) + + message(STATUS "Building CaDiCaL") +-- +2.47.0 diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix index 4ff8db1a9..12fef4c43 100644 --- a/nix/cbmc/default.nix +++ b/nix/cbmc/default.nix @@ -19,12 +19,20 @@ buildEnv { paths = builtins.attrValues { cbmc = cbmc.overrideAttrs (old: rec { - version = "6.8.0"; + version = "6.8.0"; # tautschnig/smt2-output-stability src = fetchFromGitHub { - owner = "diffblue"; + owner = "tautschnig"; repo = "cbmc"; - hash = "sha256-PT6AYiwkplCeyMREZnGZA0BKl4ZESRC02/9ibKg7mYU="; - tag = "cbmc-6.8.0"; + rev = "37f2da4d6e2e2646fdd3190949bb68c28612e6d3"; + hash = "sha256-VV33r1owrA4T8oZBfhI8F95HCtl7UAP2gXH4PBrZoQA="; + }; + srccadical = cadical.src; # 3.0.0 from nixpkgs-unstable + patches = [ + (builtins.elemAt old.patches 0) # cudd patch from nixpkgs + ./0002-Do-not-download-sources-in-cmake.patch # cadical 3.0.0 + ]; + env = old.env // { + NIX_CFLAGS_COMPILE = (old.env.NIX_CFLAGS_COMPILE or "") + " -Wno-error=switch-enum"; }; }); litani = callPackage ./litani.nix { }; # 1.29.0 @@ -40,7 +48,7 @@ buildEnv { }); inherit - cadical# 2.2.0 + cadical# 3.0.0 bitwuzla# 0.8.2 ninja; # 1.13.2 }; diff --git a/nix/util.nix b/nix/util.nix index bdca99708..a0a595303 100644 --- a/nix/util.nix +++ b/nix/util.nix @@ -2,7 +2,7 @@ # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -{ pkgs, cbmc, bitwuzla, z3, python3-for-slothy }: +{ pkgs, cbmc, cadical, bitwuzla, z3, python3-for-slothy }: rec { glibc-join = p: p.buildPackages.symlinkJoin { name = "glibc-join"; @@ -95,7 +95,7 @@ rec { }; cbmc_pkgs = pkgs.callPackage ./cbmc { - inherit cbmc bitwuzla z3; + inherit cbmc cadical bitwuzla z3; }; valgrind_varlat = pkgs.callPackage ./valgrind { }; From cd2dff9e101059d9e4283b437b32c642d0319e8a Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Fri, 13 Feb 2026 14:54:49 +0000 Subject: [PATCH 2/2] Upgrade to cbmc-viewer 3.12 for compatibility with Python 3.13 Signed-off-by: Rod Chapman --- nix/cbmc/cbmc-viewer.nix | 4 ++-- nix/cbmc/default.nix | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/nix/cbmc/cbmc-viewer.nix b/nix/cbmc/cbmc-viewer.nix index 85cd0e83e..1370b8a7c 100644 --- a/nix/cbmc/cbmc-viewer.nix +++ b/nix/cbmc/cbmc-viewer.nix @@ -7,10 +7,10 @@ python3Packages.buildPythonApplication rec { pname = "cbmc-viewer"; - version = "3.11"; + version = "3.12"; src = fetchurl { url = "https://github.com/model-checking/${pname}/releases/download/viewer-${version}/cbmc_viewer-${version}-py3-none-any.whl"; - hash = "sha256-Oy51I64KMbtE8lG8xuFXdK4RvXFvWt4zYKBlcXqwILg="; + hash = "sha256-zlme9udeOyxGPC5YNyhP1e0/zX6kJwwx3vZwcQbILTM="; }; format = "wheel"; dontUseSetuptoolsCheck = true; diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix index 12fef4c43..b8961fc6b 100644 --- a/nix/cbmc/default.nix +++ b/nix/cbmc/default.nix @@ -36,7 +36,7 @@ buildEnv { }; }); litani = callPackage ./litani.nix { }; # 1.29.0 - cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.11 + cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.12 z3 = z3.overrideAttrs (old: rec { version = "4.15.3"; src = fetchFromGitHub {