Add support for installing on NixOS #1298

tedinski · 2022-06-22T19:58:21Z

Description of changes:

Add a setup hack that detects installation on NixOS and applies the patchelf hacks necessary to make the downloaded binaries work on that platform.
I added 3 new Docker files for testing releases, none of which I've added to CI at this time. These are: NixOS, Ubuntu 22.04, Amazon Linux 2.

Resolved issues:

Resolves #1179

Call-outs:

Testing:

How is this change tested? With the included docker file.
Is this a refactor change? no

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval

Thanks for figuring this out. Are you planning to add tests for these platforms in our regression as a follow up PR?

scripts/ci/Dockerfile.bundle-test-22-04

celinval · 2022-06-22T20:37:12Z

src/setup.rs

@@ -114,7 +117,7 @@ fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> {
    if os.os_type() == os_info::Type::Ubuntu
        && *os.version() == os_info::Version::Semantic(18, 4, 0)
    {
-        crate::os_hacks::setup_python_deps_on_ubuntu_18_04(&pyroot, pkg_versions)?;
+        os_hacks::setup_python_deps_on_ubuntu_18_04(&pyroot, pkg_versions)?;


Can you move this to be called inside setup_os_hacks() instead?

Nope. This hack is "do this step in a different way entirely" not "do an extra thing afterwards"

Oh. I would expect an else case then. From reading this code it does look like do this extra thing for ubuntu 18.4.0.

celinval · 2022-06-22T20:38:29Z

src/os_hacks.rs

+}
+
+/// On NixOS, the dynamic linker does not live at the standard path, and so our downloaded
+/// pre-built binaries need patching.


Is it possible to fix that while pre-building them to NixOS instead of patching here or do you mean that there is standard path and it is only available at runtime?

We don't pre-build anything specifically for NixOS (well, except that the kani-verifier is downloaded and built locally), so this is taking the generic linux binaries and making them link properly on NixOS.

There are no standard paths, it has to be discovered at runtime. Nix seems to hack things into sorta working by injecting flags so that the linker would add rpaths to binaries. This basically replicates the effect for downloaded binaries built elsewhere.

Oh, that's great. :(

src/os_hacks.rs

celinval · 2022-06-22T20:50:25Z

src/os_hacks.rs

+/// pre-built binaries need patching.
+/// In addition, the C++ standard library (needed by the CBMC binaries we ship) also does not
+/// have a standard path, and so we need to inject an rpath into those binaries to get them
+/// to successfully link at runtime.


I'm assuming LD_LIBRARY_PATH didn't do the trick, right?

An LD_LIBRARY_PATH would do the trick I think. But (1) that has to be done in a different place and it seems nicer to concentrate "os hacks" to install time things. (2) Hacking up binaries to add rpath seems to be the way this problem is fixed in the nix community's answers, and they built the patchelf tool specifically for it.

And I guess (3) this means users can add it to PATH and run cbmc manually successfully, I suppose.

yeah patchelf is nice since it makes it "just work" every time you invoke the command, rather than having to remember to correctly set up the LD_LIBRARY_PATH

If the path never changes, I agree that this is a more permanent solution, although a bit invasive.

Well the problem is it does change whenever the hash of the contents of the package changes. So this will work initially for when kani is set up, but if the hash of stdenv changes and the old version is garbage collected, then that path will point to a non-existent directory 😃. I think the most permanent solution is to publish kani to nixpkgs and that'll "just work" by automatically rebuilding kani anytime dependent packages change.

cargo-bolero was actually recently added (not even by me which is cool) so it's pretty easy to get packages in there: https://github.com/NixOs/nixpkgs/blob/master/pkgs/development/tools/rust/cargo-bolero/default.nix

Ah I see now what the question was.

Yeah, the path can change as the system updates, but we're using basically the same solution for finding the libraries as would be done for normally built binaries (for instance, for ANY binary that was cargo install'd would suffer the same fate.)

So I think when a base system update like that happens, users of things cargo install'd on NixOS are probably already familiar with needing to reinstall them?

That's cool!

In the meantime, if the path changes, we should probably use LD_LIBRARY_PATH or re-patch the binaries if the value has changed. We don't expect users to invoke kani-driver or kani-compiler directly, so we might as well ensure that they always work.

I could be wrong, but the annoying part is that our users will have to re-install kani-verifier crate, but that won't fix the problem since the bundle we downloaded will still be on the disk. So when they run kani, they will get another crash now because kani-driver is broken, right? At that point, they will have to run kani setup to force everything to be reinstalled.

Not a blocker since nothing works today, but we should at least document that.

Yep that's correct. But what's here is definitely an improvement. Like I said, I think for the best user experience is to get into nixpkgs.

camshaft · 2022-06-22T21:37:33Z

scripts/ci/Dockerfile.bundle-test-nixos

+# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
+COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
+RUN cargo install --path ./kani-verifier
+RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz


Do you plan on running a quick smoke test to make sure everything was correctly patched as well?

I hope we'll eventually have exactly that: cargo-kani self-test #1246

Right now the "smoke tests" we do can be seen here: https://github.com/model-checking/kani/blob/main/.github/workflows/kani.yml#L126-L132

I have not added Nix to our CI, so the above are what I tested manually. Once 1 is resolved, I expect all these docker files to add cargo kani self-test to the end of them. Then the test would be complete just by successfully building the container with no extra steps.

sounds good

Can we add a test for standalone kani in the CI?

camshaft · 2022-06-22T21:39:29Z

src/os_hacks.rs

+/// pre-built binaries need patching.
+/// In addition, the C++ standard library (needed by the CBMC binaries we ship) also does not
+/// have a standard path, and so we need to inject an rpath into those binaries to get them
+/// to successfully link at runtime.


yeah patchelf is nice since it makes it "just work" every time you invoke the command, rather than having to remember to correctly set up the LD_LIBRARY_PATH

celinval

As we talked offline, please add a CI job to run NixOS at least as part of a push to main. Thanks!

celinval

Thanks for adding CI coverage!

tedinski added 5 commits June 21, 2022 21:21

Add nixos support

1a31f85

tweak nixos, add al2

06e9a0f

fix nixos detection, setup, patchelf

90cca88

add ubuntu 22.04

ae06fac

add rpath patching for c++ libs

caaecec

tedinski requested a review from a team as a code owner June 22, 2022 19:58

tedinski changed the title ~~Nixos~~ Add support for installing on NixOS Jun 22, 2022

celinval reviewed Jun 22, 2022

View reviewed changes

camshaft reviewed Jun 22, 2022

View reviewed changes

name ubuntu dockerfiles with 'ubuntu'

2148a6e

celinval approved these changes Jun 24, 2022

View reviewed changes

tedinski added 2 commits June 24, 2022 20:02

Test the nixos install procedure in CI

ab326cd

Merge remote-tracking branch 'origin/main' into nixos

a8f4d05

tedinski force-pushed the nixos branch from 779b064 to a8f4d05 Compare June 24, 2022 20:03

celinval approved these changes Jun 24, 2022

View reviewed changes

tedinski merged commit 6cfd1b4 into model-checking:main Jun 24, 2022

tedinski deleted the nixos branch June 24, 2022 20:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for installing on NixOS #1298

Add support for installing on NixOS #1298

tedinski commented Jun 22, 2022

celinval left a comment

celinval Jun 22, 2022

tedinski Jun 22, 2022

celinval Jun 22, 2022

celinval Jun 22, 2022

tedinski Jun 22, 2022

celinval Jun 22, 2022

celinval Jun 22, 2022

tedinski Jun 22, 2022

camshaft Jun 22, 2022

celinval Jun 22, 2022

camshaft Jun 22, 2022

camshaft Jun 22, 2022

tedinski Jun 22, 2022

celinval Jun 22, 2022

celinval Jun 23, 2022

camshaft Jun 23, 2022

camshaft Jun 22, 2022

tedinski Jun 22, 2022

camshaft Jun 22, 2022

celinval Jun 22, 2022

camshaft Jun 22, 2022

celinval left a comment

celinval left a comment

Add support for installing on NixOS #1298

Add support for installing on NixOS #1298

Conversation

tedinski commented Jun 22, 2022

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment