Extract bitcode for KLEE klee

4 files changed, 62 insertions, 9 deletions

diff --git a/cppcheck/default.nix b/cppcheck/default.nix
index 60991a7..4c7276b 100644
--- a/cppcheck/default.nix
+++ b/cppcheck/default.nix
@@ -16,8 +16,10 @@
 # SPDX-FileCopyrightText: 2023 Nguyễn Gia Phong
 # SPDX-License-Identifier: AGPL-3.0-or-later
 
-{ lib, stdenv, fetchFromGitHub, fetchpatch, version, commit, hash, binRenameHook
-, docbook_xsl, docbook_xml_dtd_45, libxslt, python3, which, pcre }:
+{ lib, stdenv, fetchFromGitHub, fetchpatch, version, commit, hash
+, bcExtractHook, binRenameHook
+, docbook_xsl, docbook_xml_dtd_45, libxslt
+, python3, which, pcre }:
 
 stdenv.mkDerivation rec {
   pname = "cppcheck";
@@ -40,7 +42,9 @@ stdenv.mkDerivation rec {
 
   # strictDeps = true;
   nativeBuildInputs = [
-    binRenameHook docbook_xsl docbook_xml_dtd_45 libxslt python3 which
+    bcExtractHook binRenameHook
+    docbook_xsl docbook_xml_dtd_45 libxslt
+    python3 which
   ];
   buildInputs = [ pcre ];
 
diff --git a/grep/default.nix b/grep/default.nix
index ae1e9d3..5585c10 100644
--- a/grep/default.nix
+++ b/grep/default.nix
@@ -9,12 +9,13 @@
 # SPDX-FileCopyrightText: 2023 Nguyễn Gia Phong
 # SPDX-License-Identifier: AGPL-3.0-or-later
 
-{ lib, stdenv, version, base, snapshot, binRenameHook, pcre, libiconv }:
+{ lib, stdenv, version, base, snapshot
+, bcExtractHook, binRenameHook, pcre, libiconv }:
 stdenv.mkDerivation rec {
   pname = "grep";
   inherit version;
 
-  nativeBuildInputs = [ binRenameHook ];
+  nativeBuildInputs = [ bcExtractHook binRenameHook ];
   buildInputs = [ pcre libiconv ];
   hardeningDisable = [ "all" ];
 
@@ -23,10 +24,12 @@ stdenv.mkDerivation rec {
     tar xf ${snapshot} --strip-components=1
   '';
 
-  # On macOS, force use of mkdir -p, since grep's fallback
-  # (./install-sh) is broken.
   preConfigure = ''
+    # On macOS, force use of mkdir -p,
+    # since grep's fallback (./install-sh) is broken.
     export MKDIR_P="mkdir -p"
+    # Skip extra initialization and optimizations
+    configureFlagsArray+=(--disable-nls)
   '';
   doCheck = false;
 
diff --git a/md4c/default.nix b/md4c/default.nix
index d5fb39e..aa51e1d 100644
--- a/md4c/default.nix
+++ b/md4c/default.nix
@@ -9,7 +9,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 
 { lib, stdenv, version, fetchFromGitHub, commit, hash
-, binRenameHook, cmake, pkg-config }:
+, bcExtractHook, binRenameHook, cmake, pkg-config }:
 
 stdenv.mkDerivation rec {
   pname = "md4c";
@@ -29,7 +29,7 @@ stdenv.mkDerivation rec {
     ./fix-pkgconfig.patch
   ];
 
-  nativeBuildInputs = [ binRenameHook cmake pkg-config ];
+  nativeBuildInputs = [ bcExtractHook binRenameHook cmake pkg-config ];
 
   meta = with lib; {
     description = "Markdown parser made in C";
diff --git a/shell.nix b/shell.nix
index 8ec7eb8..b1372d0 100644
--- a/shell.nix
+++ b/shell.nix
@@ -5,6 +5,22 @@
 
 with import <nixpkgs> { };
 let
+  bcExtractHook = writeTextFile {
+    name = "bc-extract-hook";
+    text = ''
+      #!${runtimeShell}
+      extractBitcodes() {
+        mkdir -p $out/share/klee
+        for i in $out/bin/*
+        do
+          ${wllvm}/bin/extract-bc -o $out/share/klee/$(basename $i).bc $i
+        done
+      }
+      preDistPhases+=(extractBitcodes)
+    '';
+    executable = true;
+    destination = "/nix-support/setup-hook";
+  };
   binRenameHook = version: writeTextFile {
     name = "bin-rename-hook";
     text = ''
@@ -20,9 +36,11 @@ let
     destination = "/nix-support/setup-hook";
   };
   cppcheck = version: commit: hash: callPackage ./cppcheck {
+    stdenv = wllvmStdenv;
     inherit version;
     inherit commit;
     inherit hash;
+    inherit bcExtractHook;
     binRenameHook = binRenameHook version;
   };
   grep-2_6 = fetchurl {
@@ -34,20 +52,47 @@ let
     hash = "sha256-Tc4KT7g93QEg31HgC1L6dg8u2GddTUwLCuZCumkurWQ=";
   };
   grep = version: base: commit: hash: callPackage ./grep {
+    stdenv = wllvmStdenv;
     inherit version;
     inherit base;
     snapshot = fetchurl {
       url = "http://git.savannah.gnu.org/cgit/grep.git/snapshot/grep-${commit}.tar.gz";
       inherit hash;
     };
+    inherit bcExtractHook;
     binRenameHook = binRenameHook version;
   };
   md4c = version: commit: hash: callPackage ./md4c {
+    stdenv = wllvmStdenv;
     inherit version;
     inherit commit;
     inherit hash;
+    inherit bcExtractHook;
     binRenameHook = binRenameHook version;
   };
+  wllvmStdenv = let
+    inherit (llvmPackages_12) clang libllvm stdenv;
+    cflags = lib.concatStringsSep " " [
+      # Recommended by https://github.com/klee/klee/issues/902
+      "-g" "-O1" "-Xclang" "-disable-llvm-passes"
+      # Prevent clang from emitting safe version of certain library functions
+      # KLEE has yet to model
+      "-D__NO_STRING_INLINES" "-D_FORTIFY_SOURCE=0" "-U__OPTIMIZE__"
+    ];
+    wllvmEnv = writeText "wllvm.env" ''
+      CC=wllvm
+      CXX=wllvm++
+      export CFLAGS="${cflags}"
+      export CXXFLAGS="${cflags}"
+      export LLVM_COMPILER=clang
+      export PATH=${lib.makeBinPath [ clang libllvm wllvm ]}:$PATH
+    '';
+  in overrideCC stdenv (wrapCCWith {
+    cc = wllvm;
+    extraBuildCommands = ''
+      cat ${wllvmEnv} >> $out/nix-support/setup-hook
+    '';
+  });
 in mkShell {
   packages = [
     (cppcheck "9261.buggy"
@@ -74,5 +119,6 @@ in mkShell {
     (md4c "107.fixed"
       "5d7c35973e5d06b46ca21b5b6e292c56dba7ca23"
       "sha256-N/vIRhXuU948z0O4NXKMSKOZGAEE6UjGDT5oqrGpUy8=")
+    klee
   ];
 }