Skip to content

Commit

Permalink
Merge pull request #350 from pq-code-package/update-bitwuzla
Browse files Browse the repository at this point in the history 
Update bitwuzla -> 0.6.0 &  Z3 -> 4.13.3
  • Loading branch information
@hanno-becker
hanno-becker authored Nov 8, 2024
2 parents 8001044 + 9072d07 commit 761a7ca
Show file tree
Hide file tree
Showing 5 changed files with 186 additions and 118 deletions.
53 changes: 32 additions & 21 deletions cbmc/default.nix
View file
Original file line number Diff line number Diff line change
@@ -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
};
}
8 changes: 7 additions & 1 deletion cbmc/litani.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

{ stdenvNoCC
, fetchFromGitHub
, python3Packages
}:

stdenvNoCC.mkDerivation {
Expand All @@ -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";
Expand Down
45 changes: 45 additions & 0 deletions cbmc/z3.nix
View file
Original file line number Diff line number Diff line change
@@ -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" ];
}
19 changes: 18 additions & 1 deletion flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

179 changes: 84 additions & 95 deletions flake.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand All @@ -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 = ''
Expand All @@ -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-
Expand Down

0 comments on commit 761a7ca

Please sign in to comment.