[Backport release-24.11] 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: Jiajie Chen <[email protected]>
-Date: Sun, 2 Jul 2023 22:43:27 +0800
+From 7b49a436bd5cc903b86b01f1a0f046ab8ec99fdb Mon Sep 17 00:00:00 2001
+From: wxt <[email protected]>
+Date: Mon, 11 Nov 2024 11:07:37 +0800
 Subject: [PATCH] Do not download sources in cmake
 
 ---
- src/solvers/CMakeLists.txt | 11 +----------
- 1 file changed, 1 insertion(+), 10 deletions(-)
+ CMakeLists.txt | 3 +--
+ 1 file changed, 1 insertion(+), 2 deletions(-)
 
-diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
-index daa0853a57..4bcbbdaa47 100644
---- a/src/solvers/CMakeLists.txt
-+++ b/src/solvers/CMakeLists.txt
-@@ -123,16 +123,6 @@ foreach(SOLVER ${sat_impl})
-     elseif("${SOLVER}" STREQUAL "cadical")
-         message(STATUS "Building solvers with cadical")
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 2c1289a..8128362 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -116,8 +116,7 @@ if(DEFINED CMAKE_USE_CUDD)
+     include("${CMAKE_CURRENT_SOURCE_DIR}/cmake/DownloadProject.cmake")
+     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
--            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)
+     if(NOT EXISTS ${cudd_SOURCE_DIR}/Makefile)
 -- 
-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 <[email protected]>
+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

@@ -1,27 +1,48 @@
-{ lib
-, stdenv
-, fetchFromGitHub
-, testers
-, bison
-, cadical
-, cbmc
-, cmake
-, flex
-, makeWrapper
-, perl
+{
+  lib,
+  stdenv,
+  fetchFromGitHub,
+  testers,
+  bison,
+  cadical,
+  cbmc,
+  cmake,
+  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;
-    rev = "${pname}-${version}";
-    sha256 = "sha256-7syRpCNL7TRZoJaNrmAdahNy7IyovyniYyOwD/lzhuw=";
+    repo = "cbmc";
+    rev = "refs/tags/cbmc-${finalAttrs.version}";
+    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
@@ -30,26 +51,46 @@ 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 .
-  '' + lib.optionalString (!stdenv.cc.isGNU) ''
-    # goto-gcc rely on gcc
-    substituteInPlace "regression/CMakeLists.txt" \
-      --replace "add_subdirectory(goto-gcc)" ""
-  '';
+  postPatch =
+    ''
+      # 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-fail "add_subdirectory(goto-gcc)" ""
+    '';
 
   postInstall = ''
     # goto-cc expects ls_parse.py in PATH
@@ -60,29 +101,36 @@ stdenv.mkDerivation rec {
       --prefix PATH : "$out/share/cbmc" \
   '';
 
-  env.NIX_CFLAGS_COMPILE = toString (lib.optionals stdenv.cc.isGNU [
-    # Needed with GCC 12 but breaks on darwin (with clang)
-    "-Wno-error=maybe-uninitialized"
-  ] ++ lib.optionals stdenv.cc.isClang [
-    # fix "argument unused during compilation"
-    "-Wno-unused-command-line-argument"
-  ]);
+  env.NIX_CFLAGS_COMPILE = toString (
+    lib.optionals stdenv.cc.isGNU [
+      # Needed with GCC 12 but breaks on darwin (with clang)
+      "-Wno-error=maybe-uninitialized"
+    ]
+    ++ lib.optionals stdenv.cc.isClang [
+      # fix "argument unused during compilation"
+      "-Wno-unused-command-line-argument"
+    ]
+  );
 
   # TODO: add jbmc support
-  cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ];
+  cmakeFlags = [
+    "-DWITH_JBMC=OFF"
+    "-Dsat_impl=cadical"
+    "-Dcadical_INCLUDE_DIR=${cadical.dev}/include"
+  ];
 
   passthru.tests.version = testers.testVersion {
     package = cbmc;
     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;
-    maintainers = with maintainers; [ jiegec ];
-    platforms = platforms.unix;
-    # error: no member named 'aligned_alloc' in the global namespace
-    broken = stdenv.hostPlatform.isDarwin && stdenv.hostPlatform.isx86_64;
+    license = lib.licenses.bsdOriginal;
+    maintainers = with lib.maintainers; [ jiegec ];
+    platforms = lib.platforms.unix;
   };
-}
+})