Skip to content

Investigate failures to link in standard libraries #109

Description

@adpaco
No description provided.

Activity

  1. nchong-at-aws commented on May 4, 2021

    @nchong-at-aws
    Contributor
    cargo new SizeAndAlignOfDstTest #< this test needs mutex and cell (which aren't linked)
    cd SizeAndAlignOfDstTest
    cp ~/rmc/rust-tests/cbmc-reg/SizeAndAlignOfDst/main_fail.rs src/main.rs 
    rustup component add rust-src --toolchain nightly
    cargo +nightly run -Z build-std --target x86_64-unknown-linux-gnu #< succeeds (just compiling)
    RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo +nightly build -Z build-std --target x86_64-unknown-linux-gnu #< fails trying to compile libc
    
  2. avanhatt commented on Jun 28, 2021

    @avanhatt
    Contributor

    cp ~/rmc/rust-tests/cbmc-reg/SizeAndAlignOfDst/main_fail.rs src/main.rs

    Is now (after tests moved):

    cp ../rmc/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs src/main.rs
    
  3. avanhatt commented on Jul 12, 2021

    @avanhatt
    Contributor

    We can now successfully codegen all of the crates in the standard library (!) (with some specific functions skipped, in the linked issues).

    However, we now fail with an actual linker error when attempting to compile the local crate, presumably because our backend does not build .rlib files:

     Compiling core v0.0.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/core)
       Compiling rustc-std-workspace-core v1.99.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/rustc-std-workspace-core)
       Compiling compiler_builtins v0.1.45
       Compiling libc v0.2.93
       Compiling alloc v0.0.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/alloc)
       Compiling cfg-if v0.1.10
       Compiling adler v0.2.3
       Compiling rustc-demangle v0.1.18
       Compiling unwind v0.0.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/unwind)
       Compiling rustc-std-workspace-alloc v1.99.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/rustc-std-workspace-alloc)
       Compiling panic_abort v0.0.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/panic_abort)
       Compiling panic_unwind v0.0.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/panic_unwind)
       Compiling gimli v0.23.0
       Compiling std_detect v0.1.5 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/stdarch/crates/std_detect)
       Compiling miniz_oxide v0.4.0
       Compiling object v0.22.0
       Compiling hashbrown v0.11.0
       Compiling addr2line v0.14.0
       Compiling std v0.0.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/std)
       Compiling proc_macro v0.0.0 (/home/ubuntu/rmc/build/x86_64-unknown-linux-gnu/stage1/lib/rustlib/src/rust/library/proc_macro)
       Compiling SizeAndAlignOfDstTest v0.1.0 (/home/ubuntu/SizeAndAlignOfDstTest)
    error: extern location for std does not exist: /home/ubuntu/SizeAndAlignOfDstTest/target/x86_64-unknown-linux-gnu/debug/deps/libstd-b5c5f6c5c49f492a.rlib
    error: aborting due to previous error
    error: could not compile `SizeAndAlignOfDstTest`
    To learn more, run the command again with --verbose.
  4. avanhatt commented on Sep 9, 2021

    @avanhatt
    Contributor

    The final linking error seems to be the same root issue as here: RMC fails to build when the final target is a main.rs cargo target instead of a lib.rs one: #473

  5. self-assigned this
    on Oct 27, 2021
  6. added a commit that references this issue on Jan 12, 2022
    ddb015a
  7. celinval commented on Jan 13, 2022

    @celinval
    Contributor

    It looks like this got closed by mistake after the last merge. That said, this issue is fairly open ended, and we have already fixed the regression script. So let's close it and open more specific issues for each failure we find.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Labels

[F] SoundnessKani failed to detect an issue

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions