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.

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

Add option to override --crate-name from kani #3054

Merged
merged 9 commits into from
Mar 8, 2024

Conversation

adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Mar 1, 2024

Adds a hidden --crate-name option to standalone Kani (i.e., kani) only. This option allows users to override the crate name used during the compilation of single-file Rust programs, making it easier to apply Kani to non-Cargo projects (see #3046 for more details).

Resolves #3046

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

@adpaco-aws adpaco-aws changed the title Add option to override --crate-name from kani [DRAFT] Add option to override --crate-name from kani Mar 1, 2024
@adpaco-aws adpaco-aws changed the title [DRAFT] Add option to override --crate-name from kani [Draft] Add option to override --crate-name from kani Mar 1, 2024
kani-driver/src/project.rs Outdated Show resolved Hide resolved
@adpaco-aws
Copy link
Contributor Author

I'm stuck with the test because the last step throws the error:

error[E0463]: can't find crate for `a` which `b` depends on
 --> c/src/lib.rs:3:1
  |
3 | extern crate b;
  | ^^^^^^^^^^^^^^^ can't find crate

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0463`.

The tree for the test project looks like:

test_project/
├── a/
│   ├── src/
│   │   └── lib.rs
├── b/
│   ├── src/
│   │   └── lib.rs
├── c/
│   ├── src/
│   │   └── lib.rs

In the project, c depends on b, which in turn depends on a. I'm getting the error in the last step when I attempt to run kani on c/src/lib.rs with

RUSTFLAGS="--edition 2021 --extern b=b/src/libb.rlib --extern a=a/src/liba.rlib" kani c/src/lib.rs

Unfortunately, the --extern a=a/src/liba.rlib doesn't seem to make any difference here. That said, I'm also getting the same error if I follow similar compilation steps with rustc:

rustc --crate-type=lib --crate-name=a a/src/lib.rs
rustc --crate-type=lib --extern a=liba.rlib b/src/lib.rs --crate-name=b
rustc --crate-type=lib --extern b=libb.rlib --extern a=liba.rlib c/src/lib.rs --crate-name=c

These steps also result in the error posted above. Therefore, it's not clear to me how to communicate this transitive dependency to rustc. It's not even clear to me if it should be needed since the dependency was already declared when we compiled b... Thoughts? @celinval @rodionov

@adpaco-aws
Copy link
Contributor Author

Just after writing that long comment, I tried adding extern crate a; to c/src/lib.rs and that works 😆

@adpaco-aws adpaco-aws marked this pull request as ready for review March 8, 2024 16:30
@adpaco-aws adpaco-aws requested a review from a team as a code owner March 8, 2024 16:30
@adpaco-aws adpaco-aws changed the title [Draft] Add option to override --crate-name from kani Add option to override --crate-name from kani Mar 8, 2024
@adpaco-aws adpaco-aws enabled auto-merge (squash) March 8, 2024 21:14
@adpaco-aws adpaco-aws merged commit ea710b3 into model-checking:main Mar 8, 2024
20 checks passed
@rodionov
Copy link

rodionov commented Mar 8, 2024

Many thanks for investigating this @adpaco-aws @celinval! Glad it has been resolved :)

Some additional thoughts on it. According to https://doc.rust-lang.org/rustc/command-line-arguments.html#--extern-specify-where-an-external-library-is-located

"
...
Specifying --extern has one behavior difference from extern crate: --extern merely makes the crate a candidate for being linked; it does not actually link it unless it's actively used. In rare occasions you may wish to ensure a crate is linked even if you don't actively use it from your code: for example, if it changes the global allocator or if it contains #[no_mangle] symbols for use by other programming languages. In such cases you'll need to use extern crate.
...
"

Since crate c doesn't actually use crate a, then crate a isn't being linked to crate c even though --extern a=liba.rlib is provided. Additionally, --extern flag is used to specify direct dependencies. Thus, this possibly explains why rustc cannot find crate a which is an indirect dependency of c.

In my experiments, I used additional rustc flag -L (https://doc.rust-lang.org/rustc/command-line-arguments.html#option-l-search-path) to provide directory path where both liba.rlib and libb.rlib are located. As a result, your change worked fine for me even without including extern crate a; -- rustc was able to figure out the transitive dependency on a.

Thanks again for fixing this!

zhassan-aws added a commit that referenced this pull request Mar 13, 2024
These are the original release notes for the reference:

## What's Changed
* Automatic cargo update to 2024-02-26 by @github-actions in
#3043
* Upgrade rust toolchain to 2024-02-17 by @celinval in
#3040
* Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in
#3049
* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in
#3047
* Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in
#3048
* Update s2n-quic submodule by @zhassan-aws in
#3050
* Update s2n-quic submodule weekly through dependabot by @zhassan-aws in
#3053
* Retrieve info for recursion tracker reliably by @feliperodri in
#3045
* Automatic cargo update to 2024-03-04 by @github-actions in
#3055
* Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in
#3052
* Add `--use-local-toolchain` to Kani setup by @jaisnan in
#3056
* Replace internal reverse_postorder by a stable one by @celinval in
#3064
* Add option to override `--crate-name` from `kani` by @adpaco-aws in
#3054
* cargo update and fix macos CI by @zhassan-aws in
#3067
* Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in
#3066
* Upgrade toolchain to 2024-03-11 by @zhassan-aws in
#3071
* Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in
#3063


**Full Changelog**:
kani-0.47.0...kani-0.48.0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Advise on using Kani for non-cargo projects
3 participants