Skip to content

Commit ce5c061

Browse files
authored
Stop building legacy-lib/ (#2173)
We no longer need to bundle the kani libraries for the legacy linker since its no longer supported. This won't affect the std script which is the last place we still use the legacy reachability mode
1 parent 5d265c7 commit ce5c061

File tree

3 files changed

+4
-61
lines changed

3 files changed

+4
-61
lines changed

kani-compiler/src/main.rs

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -173,11 +173,7 @@ fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
173173
let mut rustc_args = vec![String::from("rustc")];
174174
if args.get_flag(parser::GOTO_C) {
175175
let mut default_path = kani_root();
176-
if args.reachability_type() == ReachabilityType::Legacy {
177-
default_path.push("legacy-lib")
178-
} else {
179-
default_path.push("lib");
180-
}
176+
default_path.push("lib");
181177
let gotoc_args = rustc_gotoc_flags(
182178
args.get_one::<String>(parser::KANI_LIB)
183179
.unwrap_or(&default_path.to_str().unwrap().to_string()),
@@ -262,8 +258,7 @@ fn sysroot_path(args: &ArgMatches) -> PathBuf {
262258
let sysroot_arg = args.get_one::<String>(parser::SYSROOT);
263259
let path = if let Some(s) = sysroot_arg {
264260
PathBuf::from(s)
265-
} else if args.reachability_type() == ReachabilityType::Legacy || !args.get_flag(parser::GOTO_C)
266-
{
261+
} else if !args.get_flag(parser::GOTO_C) {
267262
toolchain_sysroot_path()
268263
} else {
269264
kani_root()

tools/build-kani/src/main.rs

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@
1010
mod parser;
1111
mod sysroot;
1212

13-
use crate::sysroot::{
14-
build_bin, build_lib, build_lib_legacy, kani_sysroot_legacy_lib, kani_sysroot_lib,
15-
};
13+
use crate::sysroot::{build_bin, build_lib, kani_sysroot_lib};
1614
use anyhow::{bail, Result};
1715
use clap::Parser;
1816
use std::{ffi::OsString, path::Path, process::Command};
@@ -23,7 +21,6 @@ fn main() -> Result<()> {
2321
match args.subcommand {
2422
parser::Commands::BuildDev(build_parser) => {
2523
build_lib();
26-
build_lib_legacy();
2724
build_bin(&build_parser.args);
2825
}
2926
parser::Commands::Bundle(bundle_parser) => {
@@ -76,7 +73,6 @@ fn prebundle(dir: &Path) -> Result<()> {
7673
build_bin(&["--release"]);
7774
// And that libraries have been built too.
7875
build_lib();
79-
build_lib_legacy();
8076
Ok(())
8177
}
8278

@@ -104,7 +100,6 @@ fn bundle_kani(dir: &Path) -> Result<()> {
104100

105101
// 4. Pre-compiled library files
106102
cp_dir(&kani_sysroot_lib(), dir)?;
107-
cp_dir(&kani_sysroot_legacy_lib(), dir)?;
108103

109104
// 5. Record the exact toolchain we use
110105
std::fs::write(dir.join("rust-toolchain-version"), env!("RUSTUP_TOOLCHAIN"))?;
@@ -114,6 +109,7 @@ fn bundle_kani(dir: &Path) -> Result<()> {
114109

115110
Ok(())
116111
}
112+
117113
/// Copy CBMC files into `dir`
118114
fn bundle_cbmc(dir: &Path) -> Result<()> {
119115
// In an effort to avoid creating new places where we must specify the exact version

tools/build-kani/src/sysroot.rs

Lines changed: 0 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@
55
//! In this folder, you can find the following folders:
66
//! - `bin/`: Where all Kani binaries will be located.
77
//! - `lib/`: Kani libraries as well as rust standard libraries.
8-
//! - `legacy-lib/`: Kani libraries built based on the the toolchain standard libraries.
98
//!
109
//! Rustc expects the sysroot to have a specific folder layout:
1110
//! `{SYSROOT}/rustlib/<target-triplet>/lib/<libraries>`
@@ -50,15 +49,6 @@ pub fn kani_sysroot_lib() -> PathBuf {
5049
path_buf!(kani_sysroot(), "lib")
5150
}
5251

53-
/// Returns the path to where Kani pre-compiled library are stored.
54-
///
55-
/// The legacy libraries are compiled on the top of rustup sysroot. Using it results in missing
56-
/// symbols. This is still needed though because when we use the rust monomorphizer as our
57-
/// reachability algorithm, the resulting boundaries are different than the new sysroot.
58-
pub fn kani_sysroot_legacy_lib() -> PathBuf {
59-
path_buf!(kani_sysroot(), "legacy-lib")
60-
}
61-
6252
/// Returns the path to where Kani's pre-compiled binaries are stored.
6353
pub fn kani_sysroot_bin() -> PathBuf {
6454
path_buf!(kani_sysroot(), "bin")
@@ -197,44 +187,6 @@ fn build_artifacts(cargo_cmd: &mut Child) -> Vec<Artifact> {
197187
.collect()
198188
}
199189

200-
/// Build Kani libraries using the regular rust toolchain standard libraries.
201-
/// We should be able to remove this once the MIR linker is stable.
202-
pub fn build_lib_legacy() {
203-
// Run cargo build with -Z build-std
204-
let target_dir = env!("KANI_LEGACY_LIBS");
205-
let args = [
206-
"build",
207-
"-p",
208-
"std",
209-
"-p",
210-
"kani",
211-
"-p",
212-
"kani_macros",
213-
"--target-dir",
214-
target_dir,
215-
"--message-format",
216-
"json-diagnostic-rendered-ansi",
217-
];
218-
let mut child = Command::new("cargo")
219-
.env("CARGO_ENCODED_RUSTFLAGS", ["--cfg=kani"].join("\x1f"))
220-
.args(args)
221-
.stdout(Stdio::piped())
222-
.spawn()
223-
.expect("Failed to build Kani libraries.");
224-
225-
// Collect the build artifacts.
226-
let artifacts = build_artifacts(&mut child);
227-
let _ = child.wait().expect("Couldn't get cargo's exit status");
228-
229-
// Create sysroot folder.
230-
let legacy_lib = kani_sysroot_legacy_lib();
231-
legacy_lib.exists().then(|| fs::remove_dir_all(&legacy_lib));
232-
fs::create_dir_all(&legacy_lib).expect(&format!("Failed to create {legacy_lib:?}"));
233-
234-
// Copy Kani libraries to inside the legacy-lib folder.
235-
copy_libs(&artifacts, &legacy_lib, &is_kani_lib);
236-
}
237-
238190
/// Extra arguments to be given to `cargo build` while building Kani's binaries.
239191
/// Note that the following arguments are always provided:
240192
/// ```bash

0 commit comments

Comments
 (0)