cbmc: 6.0.1 -> 6.4.0

pkgs/by-name/cb/cbmc/0001-Do-not-download-sources-in-cmake.patch

@@ -1,41 +1,26 @@
-From 714f5ebe9ade721abdccf58edfcddba52465cb8d Mon Sep 17 00:00:00 2001
+From 7b49a436bd5cc903b86b01f1a0f046ab8ec99fdb Mon Sep 17 00:00:00 2001
-From: Jiajie Chen <c@jia.je>
+From: wxt <3264117476@qq.com>
-Date: Sun, 2 Jul 2023 22:43:27 +0800
+Date: Mon, 11 Nov 2024 11:07:37 +0800
 Subject: [PATCH] Do not download sources in cmake
 
 ---
- src/solvers/CMakeLists.txt | 11 +----------
+ CMakeLists.txt | 3 +--
- 1 file changed, 1 insertion(+), 10 deletions(-)
+ 1 file changed, 1 insertion(+), 2 deletions(-)
 
-diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
+diff --git a/CMakeLists.txt b/CMakeLists.txt
-index daa0853a57..4bcbbdaa47 100644
+index 2c1289a..8128362 100644
---- a/src/solvers/CMakeLists.txt
+--- a/CMakeLists.txt
-+++ b/src/solvers/CMakeLists.txt
++++ b/CMakeLists.txt
-@@ -123,16 +123,6 @@ foreach(SOLVER ${sat_impl})
+@@ -116,8 +116,7 @@ if(DEFINED CMAKE_USE_CUDD)
-     elseif("${SOLVER}" STREQUAL "cadical")
+     include("${CMAKE_CURRENT_SOURCE_DIR}/cmake/DownloadProject.cmake")
-         message(STATUS "Building solvers with cadical")
+     message(STATUS "Downloading Cudd-3.0.0")
+     download_project(PROJ cudd
+-            URL https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download
+-            URL_MD5 4fdafe4924b81648b908881c81fe6c30
++            SOURCE_DIR @cudd.src@
+             )
  
--        download_project(PROJ cadical
+     if(NOT EXISTS ${cudd_SOURCE_DIR}/Makefile)
--            URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz
--            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch
--            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt
--            COMMAND ./configure
--            URL_MD5 be646831a017f81b300664e58deba1b5
--        )
--
--        add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
--
-         target_compile_definitions(solvers PUBLIC
-             SATCHECK_CADICAL HAVE_CADICAL
-         )
-@@ -140,6 +130,7 @@ foreach(SOLVER ${sat_impl})
-         target_include_directories(solvers
-             PUBLIC
-             ${cadical_SOURCE_DIR}/src
-+            ${cadical_INCLUDE_DIR}
-         )
- 
-         target_link_libraries(solvers cadical)
 -- 
-2.42.0
+2.47.0
 

pkgs/by-name/cb/cbmc/0002-Do-not-download-sources-in-cmake.patch

@@ -0,0 +1,53 @@
+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-2.0.0.tar.gz
++            SOURCE_DIR @srccadical@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+             COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
+             COMMAND ./configure
+-            URL_MD5 9fc2a66196b86adceb822a583318cc35
+         )
+ 
+         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-2.0.0.tar.gz
++            SOURCE_DIR @srccadical@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+             COMMAND ./configure
+-            URL_MD5 9fc2a66196b86adceb822a583318cc35
+         )
+ 
+         message(STATUS "Building CaDiCaL")
+-- 
+2.47.0
+

pkgs/by-name/cb/cbmc/package.nix

@@ -10,19 +10,39 @@
   flex,
   makeWrapper,
   perl,
+  substituteAll,
+  substitute,
+  cudd,
+  fetchurl,
+  nix-update-script,
+  apple-sdk,
+  apple-sdk_10_15,
+  darwinMinVersionHook,
 }:
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation (finalAttrs: {
   pname = "cbmc";
-  version = "6.0.1";
+  version = "6.4.0";
 
   src = fetchFromGitHub {
     owner = "diffblue";
-    repo = pname;
+    repo = "cbmc";
-    rev = "${pname}-${version}";
+    rev = "refs/tags/cbmc-${finalAttrs.version}";
-    sha256 = "sha256-7syRpCNL7TRZoJaNrmAdahNy7IyovyniYyOwD/lzhuw=";
+    hash = "sha256-PZZnseOE3nodE0zwyG+82gm55BO4rsCcP4T+fZq7L6I=";
   };
 
+  srcglucose = fetchFromGitHub {
+    owner = "brunodutertre";
+    repo = "glucose-syrup";
+    rev = "0bb2afd3b9baace6981cbb8b4a1c7683c44968b7";
+    hash = "sha256-+KrnXEJe7ApSuj936T615DaXOV+C2LlRxc213fQI+Q4=";
+  };
+
+  srccadical =
+    (cadical.override {
+      version = "2.0.0";
+    }).src;
+
   nativeBuildInputs = [
     bison
     cmake
@@ -31,27 +51,45 @@ stdenv.mkDerivation rec {
     makeWrapper
   ];
 
-  buildInputs = [ cadical ];
+  buildInputs =
+    [ cadical ]
+    ++ lib.optionals stdenv.hostPlatform.isDarwin [
+      (darwinMinVersionHook "10.15")
+    ]
+    ++ lib.optionals (stdenv.hostPlatform.isDarwin && lib.versionOlder apple-sdk.version "10.15") [
+      apple-sdk_10_15
+    ];
 
   # do not download sources
   # link existing cadical instead
   patches = [
-    ./0001-Do-not-download-sources-in-cmake.patch
+    (substituteAll {
+      src = ./0001-Do-not-download-sources-in-cmake.patch;
+      inherit cudd;
+    })
+    ./0002-Do-not-download-sources-in-cmake.patch
   ];
 
   postPatch =
     ''
-      # do not hardcode gcc
-      substituteInPlace "scripts/bash-autocomplete/extract_switches.sh" \
-        --replace "gcc" "$CC" \
-        --replace "g++" "$CXX"
       # fix library_check.sh interpreter error
       patchShebangs .
+
+      mkdir -p srccadical
+      cp -r ${finalAttrs.srccadical}/* srccadical
+
+      mkdir -p srcglucose
+      cp -r ${finalAttrs.srcglucose}/* srcglucose
+      find -exec chmod +w {} \;
+
+      substituteInPlace src/solvers/CMakeLists.txt \
+       --replace-fail "@srccadical@" "$PWD/srccadical" \
+       --replace-fail "@srcglucose@" "$PWD/srcglucose"
     ''
     + lib.optionalString (!stdenv.cc.isGNU) ''
       # goto-gcc rely on gcc
       substituteInPlace "regression/CMakeLists.txt" \
-        --replace "add_subdirectory(goto-gcc)" ""
+        --replace-fail "add_subdirectory(goto-gcc)" ""
     '';
 
   postInstall = ''
@@ -86,13 +124,13 @@ stdenv.mkDerivation rec {
     command = "cbmc --version";
   };
 
-  meta = with lib; {
+  passthru.updateScript = nix-update-script { };
+
+  meta = {
     description = "CBMC is a Bounded Model Checker for C and C++ programs";
     homepage = "http://www.cprover.org/cbmc/";
-    license = licenses.bsdOriginal;
+    license = lib.licenses.bsdOriginal;
-    maintainers = with maintainers; [ jiegec ];
+    maintainers = with lib.maintainers; [ jiegec ];
-    platforms = platforms.unix;
+    platforms = lib.platforms.unix;
-    # error: no member named 'aligned_alloc' in the global namespace
-    broken = stdenv.hostPlatform.isDarwin && stdenv.hostPlatform.isx86_64;
   };
-}
+})