Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Investigate failures to link in standard libraries #109

Closed
adpaco-aws opened this issue Apr 27, 2021 · 5 comments
Closed

Investigate failures to link in standard libraries #109

adpaco-aws opened this issue Apr 27, 2021 · 5 comments
Assignees
@danielsn @celinval
Labels
[F] Soundness Kani failed to detect an issue

Comments

@adpaco-aws
Copy link
Contributor

No description provided.

@adpaco-aws adpaco-aws added Area: compilation [F] Soundness Kani failed to detect an issue labels Apr 27, 2021
@nchong-at-aws
Copy link
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

This was referenced Jun 16, 2021
Closed
Closed
Open
Closed
Closed
Closed
Closed
Closed
Merged
Closed
Closed
Closed
@danielsn danielsn assigned danielsn and unassigned markrtuttle Jun 22, 2021
@avanhatt
Copy link
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

This was referenced Jul 1, 2021
Closed
Closed
Closed
Merged
@avanhatt
Copy link
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.

@avanhatt
Copy link
Contributor

avanhatt commented Sep 9, 2021

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

celinval added a commit to celinval/kani-dev that referenced this issue Oct 27, 2021
@celinval
Fix std lib regression script (model-checking#109 and model-checking#375
9482f89 
)

Create a target library instead of a binary.
@celinval celinval self-assigned this Oct 27, 2021
@celinval celinval mentioned this issue Oct 27, 2021
Merged
4 tasks
celinval added a commit to celinval/kani-dev that referenced this issue Nov 2, 2021
@celinval
Fix std lib regression script (model-checking#109 and model-checking#375
2b31725 
)

Create a target library instead of a binary.
celinval added a commit to celinval/kani-dev that referenced this issue Nov 3, 2021
@celinval
Fix std lib regression script (model-checking#109 and model-checking#375
57590b7 
)

Create a target library instead of a binary.
celinval added a commit to celinval/kani-dev that referenced this issue Nov 4, 2021
@celinval
Fix std lib regression script (model-checking#109 and model-checking#375
4d1a9a7 
)

Create a target library instead of a binary.
celinval added a commit that referenced this issue Nov 4, 2021
@celinval
Fix std lib regression script (#109 and #375) (#593)
e687b4c 
Create a target library instead of a binary.
@zhassan-aws zhassan-aws reopened this Jan 12, 2022
@celinval
Copy link
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.

tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 22, 2022
@celinval @tedinski
Fix std lib regression script (model-checking#109 and model-checking#375
8dffd35 
) (model-checking#593)

Create a target library instead of a binary.
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 25, 2022
@celinval @tedinski
Fix std lib regression script (model-checking#109 and model-checking#375
9286ec8 
) (model-checking#593)

Create a target library instead of a binary.
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 26, 2022
@celinval @tedinski
Fix std lib regression script (model-checking#109 and model-checking#375
7e27ec5 
) (model-checking#593)

Create a target library instead of a binary.
tedinski pushed a commit that referenced this issue Apr 27, 2022
@celinval @tedinski
Fix std lib regression script (#109 and #375) (#593)
b3f376d 
Create a target library instead of a binary.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@danielsn danielsn

@celinval celinval

Labels
[F] Soundness Kani failed to detect an issue
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
7 participants
@danielsn @markrtuttle @avanhatt @celinval @nchong-at-aws @adpaco-aws @zhassan-aws