cbmc: init at 5.63.0

Cadical is used as sat solver backend.

https://github.com/diffblue/cbmc/releases/tag/cbmc-5.63.0

pkgs/applications/science/logic/cbmc/0001-Do-not-download-sources-in-cmake.patch

@@ -0,0 +1,49 @@
+From fbc1488e8da0175e9c9bdf5892f8a65c71f2a266 Mon Sep 17 00:00:00 2001
+From: Jiajie Chen <c@jia.je>
+Date: Fri, 15 Jul 2022 18:33:15 +0800
+Subject: [PATCH] Do not download sources in cmake
+
+---
+ src/solvers/CMakeLists.txt | 20 +-------------------
+ 1 file changed, 1 insertion(+), 19 deletions(-)
+
+diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
+index 744def486..5b719a78a 100644
+--- a/src/solvers/CMakeLists.txt
++++ b/src/solvers/CMakeLists.txt
+@@ -106,31 +106,13 @@ elseif("${sat_impl}" STREQUAL "glucose")
+ elseif("${sat_impl}" STREQUAL "cadical")
+     message(STATUS "Building solvers with cadical")
+ 
+-    download_project(PROJ cadical
+-        URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz
+-        PATCH_COMMAND true
+-        COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14
+-        URL_MD5 b44874501a175106424f4bd5de29aa59
+-    )
+-
+     message(STATUS "Building CaDiCaL")
+-    execute_process(COMMAND make -j WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+ 
+     target_compile_definitions(solvers PUBLIC
+         SATCHECK_CADICAL HAVE_CADICAL
+     )
+ 
+-    add_library(cadical STATIC IMPORTED)
+-
+-    set_target_properties(
+-        cadical
+-        PROPERTIES IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
+-    )
+-
+-    target_include_directories(solvers
+-      PUBLIC
+-      ${cadical_SOURCE_DIR}/src
+-    )
++    target_include_directories(solvers PUBLIC ${cadical_INCLUDE_DIR})
+ 
+     target_link_libraries(solvers cadical)
+ elseif("${sat_impl}" STREQUAL "ipasir-cadical")
+-- 
+2.35.1
+

pkgs/applications/science/logic/cbmc/default.nix

@@ -0,0 +1,82 @@
+{ lib
+, stdenv
+, fetchFromGitHub
+, testers
+, bison
+, cadical
+, cbmc
+, cmake
+, flex
+, makeWrapper
+, perl
+}:
+
+stdenv.mkDerivation rec {
+  pname = "cbmc";
+  version = "5.63.0";
+
+  src = fetchFromGitHub {
+    owner = "diffblue";
+    repo = pname;
+    rev = "${pname}-${version}";
+    sha256 = "sha256-4tn3wsmaYdo5/QaZc3MLxVGF0x8dmRKeygF/8A+Ww1o=";
+  };
+
+  nativeBuildInputs = [
+    bison
+    cmake
+    flex
+    perl
+    makeWrapper
+  ];
+
+  buildInputs = [ cadical ];
+
+  # do not download sources
+  # link existing cadical instead
+  patches = [
+    ./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)" ""
+  '';
+
+  postInstall = ''
+    # goto-cc expects ls_parse.py in PATH
+    mkdir -p $out/share/cbmc
+    mv $out/bin/ls_parse.py $out/share/cbmc/ls_parse.py
+    chmod +x $out/share/cbmc/ls_parse.py
+    wrapProgram $out/bin/goto-cc \
+      --prefix PATH : "$out/share/cbmc" \
+  '';
+
+  # fix "argument unused during compilation"
+  NIX_CFLAGS_COMPILE = lib.optionalString stdenv.cc.isClang
+    "-Wno-unused-command-line-argument";
+
+  # TODO: add jbmc support
+  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; {
+    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;
+  };
+}

pkgs/top-level/all-packages.nix

@@ -34247,6 +34247,8 @@ with pkgs;
 
   boogie = dotnetPackages.Boogie;
 
+  cbmc = callPackage ../applications/science/logic/cbmc { };
+
   cadical = callPackage ../applications/science/logic/cadical {};
 
   inherit (callPackage ./coq-packages.nix {