Nix: Update CBCM to experimental branch

See diffblue/cbmc#8830

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

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;
           };
@@ -219,7 +220,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;
             };

nix/cbmc/0002-Do-not-download-sources-in-cmake.patch

@@ -0,0 +1,52 @@
+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

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
     };

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";
@@ -94,7 +94,7 @@ rec {
     };
   };
 
-  cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc bitwuzla z3; };
+  cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc cadical bitwuzla z3; };
 
   valgrind_varlat = pkgs.callPackage ./valgrind { };
   hol_light' = pkgs.callPackage ./hol_light { };