From cb94f600feecb160629cd97c8447b9b694c9c104 Mon Sep 17 00:00:00 2001 From: wxt <3264117476@qq.com> Date: Mon, 11 Nov 2024 10:49:37 +0800 Subject: [PATCH 1/2] cbmc: nixfmt (cherry picked from commit 1d2443c3d7b13c4eb47b29edf0a3dbf5934b7f39) --- pkgs/by-name/cb/cbmc/package.nix | 72 ++++++++++++++++++-------------- 1 file changed, 41 insertions(+), 31 deletions(-) diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index 0bfb512737582..fdee35e98ec58 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/pkgs/by-name/cb/cbmc/package.nix @@ -1,14 +1,15 @@ -{ lib -, stdenv -, fetchFromGitHub -, testers -, bison -, cadical -, cbmc -, cmake -, flex -, makeWrapper -, perl +{ + lib, + stdenv, + fetchFromGitHub, + testers, + bison, + cadical, + cbmc, + cmake, + flex, + makeWrapper, + perl, }: stdenv.mkDerivation rec { @@ -38,18 +39,20 @@ stdenv.mkDerivation rec { ./0001-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 = + '' + # 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)" "" + ''; postInstall = '' # goto-cc expects ls_parse.py in PATH @@ -60,16 +63,23 @@ 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; From 2c0156fe93599450e8bf44505efaaf4528d61ed1 Mon Sep 17 00:00:00 2001 From: wxt <3264117476@qq.com> Date: Mon, 11 Nov 2024 11:46:21 +0800 Subject: [PATCH 2/2] cbmc: 6.0.1 -> 6.4.0 (cherry picked from commit 0d71320797007c58d408dfc991e21ef236843de6) --- ...001-Do-not-download-sources-in-cmake.patch | 53 +++++-------- ...002-Do-not-download-sources-in-cmake.patch | 53 +++++++++++++ pkgs/by-name/cb/cbmc/package.nix | 76 ++++++++++++++----- 3 files changed, 129 insertions(+), 53 deletions(-) create mode 100644 pkgs/by-name/cb/cbmc/0002-Do-not-download-sources-in-cmake.patch diff --git a/pkgs/by-name/cb/cbmc/0001-Do-not-download-sources-in-cmake.patch b/pkgs/by-name/cb/cbmc/0001-Do-not-download-sources-in-cmake.patch index c209ed059e44f..324fd2adc04aa 100644 --- a/pkgs/by-name/cb/cbmc/0001-Do-not-download-sources-in-cmake.patch +++ b/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 -Date: Sun, 2 Jul 2023 22:43:27 +0800 +From 7b49a436bd5cc903b86b01f1a0f046ab8ec99fdb Mon Sep 17 00:00:00 2001 +From: wxt <3264117476@qq.com> +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 diff --git a/pkgs/by-name/cb/cbmc/0002-Do-not-download-sources-in-cmake.patch b/pkgs/by-name/cb/cbmc/0002-Do-not-download-sources-in-cmake.patch new file mode 100644 index 0000000000000..c45b65e80f6ef --- /dev/null +++ b/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 + diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index fdee35e98ec58..fb360095c7bc9 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/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; - 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 @@ -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; - 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; }; -} +})