diff --git a/cbmc/default.nix b/cbmc/default.nix index 29b787b5a..95c087d3f 100644 --- a/cbmc/default.nix +++ b/cbmc/default.nix @@ -1,29 +1,40 @@ # SPDX-License-Identifier: Apache-2.0 -{ cbmc +{ buildEnv +, cbmc , fetchFromGitHub , callPackage -, z3_4_12 , bitwuzla , ninja +, cadical }: -builtins.attrValues { - cbmc = cbmc.overrideAttrs (old: rec { - version = "6.3.1"; # remember to adjust this in ../flake.nix too - src = fetchFromGitHub { - owner = "diffblue"; - repo = old.pname; - rev = "${old.pname}-${version}"; - hash = "sha256-y3avPsVxtxSV+WB8TBbvnaNZ4WZltGRTcD+GPwTlp2E="; - }; - patches = [ - ./0001-Do-not-download-sources-in-cmake.patch - ]; - }); - litani = callPackage ./litani.nix { }; # 1.29.0 - cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.9 - inherit - ninja# 1.11.1 - z3_4_12# 4.12.5 - bitwuzla; # 0.4.0 +buildEnv { + name = "pqcp-cbmc"; + paths = + builtins.attrValues { + cbmc = cbmc.overrideAttrs (old: rec { + version = "6.3.1"; # remember to adjust this in ../flake.nix too + src = fetchFromGitHub { + owner = "diffblue"; + repo = old.pname; + rev = "${old.pname}-${version}"; + hash = "sha256-y3avPsVxtxSV+WB8TBbvnaNZ4WZltGRTcD+GPwTlp2E="; + }; + patches = [ + ./0001-Do-not-download-sources-in-cmake.patch + ]; + }); + litani = callPackage ./litani.nix { }; # 1.29.0 + cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.9 + + z3 = callPackage ./z3.nix { + version = "4.13.3"; + sha256 = "sha256-odwalnF00SI+sJGHdIIv4KapFcfVVKiQ22HFhXYtSvA="; + }; + + inherit + cadical#1.9.5 + bitwuzla# 0.6.0 + ninja; # 1.11.1 + }; } diff --git a/cbmc/litani.nix b/cbmc/litani.nix index 7cacd4048..9676110f2 100644 --- a/cbmc/litani.nix +++ b/cbmc/litani.nix @@ -2,6 +2,7 @@ { stdenvNoCC , fetchFromGitHub +, python3Packages }: stdenvNoCC.mkDerivation { @@ -16,12 +17,17 @@ stdenvNoCC.mkDerivation { dontConfigure = true; installPhase = '' mkdir -p $out/bin - cp litani $out/bin + install -Dm755 litani $out/bin/litani cp -r lib $out/bin cp -r templates $out/bin ''; dontStrip = true; noAuditTmpdir = true; + propagatedBuildInputs = [ + (python3Packages.python.withPackages + (pythonPackages: [ pythonPackages.jinja2 ]) + ) + ]; meta = { description = "Litani metabuild system"; diff --git a/cbmc/z3.nix b/cbmc/z3.nix new file mode 100644 index 000000000..af1a7dddf --- /dev/null +++ b/cbmc/z3.nix @@ -0,0 +1,45 @@ +# SPDX-License-Identifier: MIT + +{ version +, sha256 +, fetchFromGitHub +, fixDarwinDylibNames +, lib +, stdenv +, python3Packages +, llvmPackages +}: +stdenv.mkDerivation rec { + inherit version sha256; + pname = "z3"; + src = fetchFromGitHub { + inherit sha256; + owner = "Z3Prover"; + repo = "z3"; + rev = "z3-${version}"; + }; + + nativeBuildInputs = [ python3Packages.python ] + ++ lib.optional stdenv.hostPlatform.isLinux llvmPackages.libcxxClang + ++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames; + + enableParallelBuilding = true; + + configurePhase = '' + python scripts/mk_make.py --prefix=$out + cd build + ''; + + checkPhase = '' + make test + ./test-z3 -a + ''; + + postInstall = '' + mkdir -p $dev $lib + mv $out/lib $lib/lib + mv $out/include $dev/include + ''; + + outputs = [ "out" "lib" "dev" ]; +} diff --git a/flake.lock b/flake.lock index 842a27a27..021d41212 100644 --- a/flake.lock +++ b/flake.lock @@ -36,10 +36,27 @@ "type": "github" } }, + "nixpkgs-unstable": { + "locked": { + "lastModified": 1730785428, + "narHash": "sha256-Zwl8YgTVJTEum+L+0zVAWvXAGbWAuXHax3KzuejaDyo=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "4aa36568d413aca0ea84a1684d2d46f55dbabad7", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, "root": { "inputs": { "flake-parts": "flake-parts", - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs", + "nixpkgs-unstable": "nixpkgs-unstable" } } }, diff --git a/flake.nix b/flake.nix index a4b4b2ad9..534a09292 100644 --- a/flake.nix +++ b/flake.nix @@ -5,6 +5,7 @@ inputs = { nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.05"; + nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable"; flake-parts = { url = "github:hercules-ci/flake-parts"; @@ -16,98 +17,45 @@ flake-parts.lib.mkFlake { inherit inputs; } { imports = [ ]; systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ]; - perSystem = { pkgs, ... }: + perSystem = { config, pkgs, system, inputs', ... }: let - cbmcpkg = pkgs.callPackage ./cbmc { }; # 6.3.1 - - linters = builtins.attrValues { - clang-tools = pkgs.clang-tools.overrideAttrs { - unwrapped = pkgs.llvmPackages_17.clang-unwrapped; - }; - - inherit (pkgs) - nixpkgs-fmt - shfmt; - - inherit (pkgs.python3Packages) - black; - }; - - glibc-join = p: p.buildPackages.symlinkJoin { - name = "glibc-join"; - paths = [ p.glibc p.glibc.static ]; - }; - - wrap-gcc = p: p.buildPackages.wrapCCWith { - cc = p.buildPackages.gcc13.cc; - bintools = p.buildPackages.wrapBintoolsWith { - bintools = p.buildPackages.binutils-unwrapped; - libc = glibc-join p; - }; - }; - - x86_64-gcc = wrap-gcc pkgs.pkgsCross.gnu64; - aarch64-gcc = wrap-gcc pkgs.pkgsCross.aarch64-multiplatform; - default_gcc = { cross ? true }: let - gcc = - if pkgs.stdenv.isDarwin - then [ ] - else - if cross - then - if pkgs.stdenv.isAarch64 - then [ x86_64-gcc aarch64-gcc ] - else [ aarch64-gcc x86_64-gcc ] - else - if pkgs.stdenv.isAarch64 - then [ aarch64-gcc ] - else [ x86_64-gcc ]; - in - gcc; + glibc-join = p: p.buildPackages.symlinkJoin { + name = "glibc-join"; + paths = [ p.glibc p.glibc.static ]; + }; - base = - builtins.attrValues { - inherit (pkgs.python3Packages) - pyyaml - python - click; - }; + wrap-gcc = p: p.buildPackages.wrapCCWith { + cc = p.buildPackages.gcc13.cc; + bintools = p.buildPackages.wrapBintoolsWith { + bintools = p.buildPackages.binutils-unwrapped; + libc = glibc-join p; + }; + }; - # cross is for determining whether to install the cross toolchain or not + x86_64-gcc = wrap-gcc pkgs.pkgsCross.gnu64; + aarch64-gcc = wrap-gcc pkgs.pkgsCross.aarch64-multiplatform; + in + if pkgs.stdenv.isDarwin + then [ ] + else if cross + then if pkgs.stdenv.isAarch64 + then [ x86_64-gcc aarch64-gcc ] + else [ aarch64-gcc x86_64-gcc ] + else if pkgs.stdenv.isAarch64 + then [ aarch64-gcc ] + else [ x86_64-gcc ]; + + # cross is for determining whether to install the cross toolchain or not core = { cross ? true }: - default_gcc { cross = cross; } ++ base ++ + [ (default_gcc { cross = cross; }) ] ++ builtins.attrValues { + inherit (config.packages) base; inherit (pkgs) qemu; # 8.2.4 }; - core_gcc48 = base ++ builtins.attrValues { - inherit (pkgs) - gcc48; #4.8 - }; - - core_gcc49 = base ++ builtins.attrValues { - inherit (pkgs) - gcc49; #4.9 - }; - - core_gcc7 = base ++ builtins.attrValues { - inherit (pkgs) - gcc7; #7 - }; - - core_gcc11 = base ++ builtins.attrValues { - inherit (pkgs) - gcc11; #11 - }; - - core_clang18 = base ++ builtins.attrValues { - inherit (pkgs) - clang_18; #18 - }; - wrapShell = mkShell: attrs: mkShell (attrs // { shellHook = '' @@ -116,26 +64,67 @@ }); in { - devShells.default = wrapShell pkgs.mkShellNoCC { - packages = core { } ++ linters ++ cbmcpkg ++ - builtins.attrValues { + # NOTE: hack for replacing bitwuzla in nixos-24.05 (0.4.0) to the one in nixos-unstable (0.6.0) by nix overlays + _module.args.pkgs = import inputs.nixpkgs { + inherit system; + overlays = [ + (_: _: { bitwuzla = inputs'.nixpkgs-unstable.legacyPackages.bitwuzla; }) + ]; + }; + + packages.linters = pkgs.buildEnv + { + name = "pqcp-linters"; + paths = builtins.attrValues { + clang-tools = pkgs.clang-tools.overrideAttrs { + unwrapped = pkgs.llvmPackages_17.clang-unwrapped; + }; + inherit (pkgs) - direnv - nix-direnv; + nixpkgs-fmt + shfmt; + + inherit (pkgs.python3Packages) + black; }; + }; + + packages.cbmc = pkgs.callPackage ./cbmc { }; # 6.3.1 + + packages.base = pkgs.buildEnv { + name = "pqcp-base"; + paths = builtins.attrValues { + inherit (pkgs.python3Packages) + pyyaml + python + click; + }; + }; + + + devShells.default = wrapShell pkgs.mkShellNoCC { + packages = + core { } ++ + builtins.attrValues + { + inherit (config.packages) linters cbmc; + inherit (pkgs) + direnv + nix-direnv; + }; }; devShells.ci = wrapShell pkgs.mkShellNoCC { packages = core { cross = false; }; }; devShells.ci-cross = wrapShell pkgs.mkShellNoCC { packages = core { }; }; - devShells.ci-cbmc = wrapShell pkgs.mkShellNoCC { packages = core { cross = false; } ++ cbmcpkg; }; - devShells.ci-cbmc-cross = wrapShell pkgs.mkShellNoCC { packages = core { } ++ cbmcpkg; }; - devShells.ci-linter = wrapShell pkgs.mkShellNoCC { packages = linters; }; - - devShells.ci_clang18 = wrapShell pkgs.mkShellNoCC { packages = core_clang18; }; - devShells.ci_gcc48 = wrapShell pkgs.mkShellNoCC { packages = core_gcc48; }; - devShells.ci_gcc49 = wrapShell pkgs.mkShellNoCC { packages = core_gcc49; }; - devShells.ci_gcc7 = wrapShell pkgs.mkShellNoCC { packages = core_gcc7; }; - devShells.ci_gcc11 = wrapShell pkgs.mkShellNoCC { packages = core_gcc11; }; + devShells.ci-cbmc = wrapShell pkgs.mkShellNoCC { packages = core { cross = false; } ++ [ config.packages.cbmc ]; }; + devShells.ci-cbmc-cross = wrapShell pkgs.mkShellNoCC { packages = core { } ++ [ config.packages.cbmc ]; }; + devShells.ci-linter = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.linters ]; }; + + devShells.ci_clang18 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.clang_18 ]; }; + devShells.ci_gcc48 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc48 ]; }; + devShells.ci_gcc49 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc49 ]; }; + devShells.ci_gcc7 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc7 ]; }; + devShells.ci_gcc11 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc11 ]; }; }; flake = { # The usual flake attributes can be defined here, including system-