AeneasVerif / aeneas

A verification toolchain for Rust programs
Apache License 2.0
123 stars 12 forks source link

Easy installation recipes #144

Open RaitoBezarius opened 2 weeks ago

RaitoBezarius commented 2 weeks ago

We discussed earlier the creation of an easy installation recipe to work using Aeneas.

cc @Nadrieril @sonmarcho

Re: discussion on static binaries, currently, here are the results:

❯ ldd result/bin/aeneas 
    linux-vdso.so.1 (0x00007ffc46deb000)
    libpthread.so.0 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libpthread.so.0 (0x00007f9812a07000)
    libgmp.so.10 => /nix/store/s3s7gv33p88kzbgki2bprg2a1nc7jnf8-gmp-with-cxx-6.3.0/lib/libgmp.so.10 (0x00007f9812964000)
    libm.so.6 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libm.so.6 (0x00007f9812884000)
    libc.so.6 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libc.so.6 (0x00007f981269c000)
    /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/ld-linux-x86-64.so.2 => /nix/store/ddwyrxif62r8n6xclvskjyy6szdhvj60-glibc-2.39-5/lib64/ld-linux-x86-64.so.2 (0x00007f9812a0e000)
❯ ldd result/bin/charon
    linux-vdso.so.1 (0x00007fffddee1000)
    libgcc_s.so.1 => /nix/store/myw67gkgayf3s2mniij7zwd79lxy8v0k-gcc-12.3.0-lib/lib/libgcc_s.so.1 (0x00007f223c27f000)
    libc.so.6 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libc.so.6 (0x00007f223c097000)
    /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/ld-linux-x86-64.so.2 => /nix/store/ddwyrxif62r8n6xclvskjyy6szdhvj60-glibc-2.39-5/lib64/ld-linux-x86-64.so.2 (0x00007f223c545000)
Nadrieril commented 2 weeks ago

The fun one is charon-driver:

> ldd ../bin/charon-driver
        linux-vdso.so.1 (0x00007ffcb57f0000)
        librustc_driver-796e47691512e4e9.so => /nix/store/6gjabmhh7kjcpz1s9dk6mqv1plmsn035-rust-default-1.72.0-nightly-2023-06-02/lib/rustlib/x86_64-unknown-linux-gnu/lib/librustc_driver-796e47691512e4e9.so (0x00007f768c000000)
        libstd-fe004512c8383174.so => /nix/store/6gjabmhh7kjcpz1s9dk6mqv1plmsn035-rust-default-1.72.0-nightly-2023-06-02/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-fe004512c8383174.so (0x00007f768be26000)
        libgcc_s.so.1 => /nix/store/myw67gkgayf3s2mniij7zwd79lxy8v0k-gcc-12.3.0-lib/lib/libgcc_s.so.1 (0x00007f769122e000)
        libc.so.6 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libc.so.6 (0x00007f768bc3e000)
        /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/ld-linux-x86-64.so.2 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib64/ld-linux-x86-64.so.2 (0x00007f7691251000)
        libLLVM-16-rust-1.72.0-nightly.so => /nix/store/a8n8c8v6ayx6ychgmhvq8j98irxslnln-rustc-1.72.0-nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/libLLVM-16-rust-1.72.0-nightly.so (0x00007f7682800000)
        libdl.so.2 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libdl.so.2 (0x00007f7691227000)
        libpthread.so.0 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libpthread.so.0 (0x00007f7691222000)
        libm.so.6 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/libm.so.6 (0x00007f768bb5e000)
        librt.so.1 => /nix/store/qn3ggz5sf3hkjs2c797xf7nan3amdxmp-glibc-2.38-27/lib/librt.so.1 (0x00007f769121b000)
        libz.so.1 => /nix/store/8xgb8phqmfn9h971q7dg369h647i1aa0-zlib-1.3/lib/libz.so.1 (0x00007f76911fd000)
Nadrieril commented 2 weeks ago

Found here:

rustc_driver is only available as dylib.

Nadrieril commented 2 weeks ago

The various .so files we need are provided by rustup when we ask for the rustc-dev and llvm-tools-preview components. So cargo aeneas should call to rustup to install the pinned toolchain + components we need, then provide charon-driver with the path to the .sos inside ~/.rustup. In fact, rustup run nightly-2023-06-02-x86_64-unknown-linux-gnu <command> runs the command with the appropriate LD_LIBRARY_PATH, that's nice.

Of course for nix users we don't need to do any of that.