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

Support crate-type=bin and --tests with dependencies #1260

Merged
merged 6 commits into from
Jun 8, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 38 additions & 0 deletions Cargo.lock
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,12 @@ version = "1.0.56"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4361135be9122e0870de935d7c439aef945b9f9ddd4199a553b5270b49c82a27"

[[package]]
name = "ar"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "450575f58f7bee32816abbff470cbc47797397c2a81e0eaced4b98436daf52e1"

[[package]]
name = "arrayvec"
version = "0.7.2"
Expand Down Expand Up @@ -184,6 +190,15 @@ dependencies = [
"tracing",
]

[[package]]
name = "crc32fast"
version = "1.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b540bd8bc810d3885c6ea91e2018302f68baba2129ab3e88f32389ee9370880d"
dependencies = [
"cfg-if",
]

[[package]]
name = "crossbeam-channel"
version = "0.5.4"
Expand Down Expand Up @@ -322,6 +337,16 @@ dependencies = [
"winapi",
]

[[package]]
name = "indexmap"
version = "1.8.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e6012d540c5baa3589337a98ce73408de9b5a25ec9fc2c6fd6be8f0d39e0ca5a"
dependencies = [
"autocfg",
"hashbrown",
]

[[package]]
name = "instant"
version = "0.1.12"
Expand Down Expand Up @@ -357,6 +382,7 @@ dependencies = [
name = "kani-compiler"
version = "0.3.0"
dependencies = [
"ar",
"atty",
"bitflags",
"clap",
Expand All @@ -366,6 +392,7 @@ dependencies = [
"kani_queries",
"libc",
"num",
"object",
"rustc-demangle",
"serde",
"serde_json",
Expand Down Expand Up @@ -632,6 +659,17 @@ dependencies = [
"libc",
]

[[package]]
name = "object"
version = "0.27.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "67ac1d3f9a1d3616fd9a60c8d74296f22406a238b6a72f5cc1e6f314df4ffbf9"
dependencies = [
"crc32fast",
"indexmap",
"memchr",
]

[[package]]
name = "once_cell"
version = "1.10.0"
Expand Down
4 changes: 3 additions & 1 deletion kani-compiler/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ edition = "2021"
license = "MIT OR Apache-2.0"

[dependencies]
ar = { version = "0.8.0", optional = true }
atty = "0.2.14"
bitflags = { version = "1.0", optional = true }
cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
Expand All @@ -17,6 +18,7 @@ kani_queries = {path = "kani_queries"}
kani_metadata = { path = "../kani_metadata", optional = true }
libc = { version = "0.2", optional = true }
num = { version = "0.4.0", optional = true }
object = { version = "0.27.0", default-features = false, features = ["std", "read_core", "write", "archive", "coff", "elf", "macho", "pe"], optional = true }
rustc-demangle = { version = "0.1.21", optional = true }
serde = { version = "1", optional = true }
serde_json = { version = "1", optional = true }
Expand All @@ -28,7 +30,7 @@ tracing-tree = "0.2.0"
# Future proofing: enable backend dependencies using feature.
[features]
default = ['cprover']
cprover = ['bitflags', 'cbmc', 'kani_metadata', 'libc', 'num', 'rustc-demangle', 'serde', 'serde_json']
cprover = ['ar', 'bitflags', 'cbmc', 'kani_metadata', 'libc', 'num', 'object', 'rustc-demangle', 'serde', 'serde_json']

[package.metadata.rust-analyzer]
# This package uses rustc crates.
Expand Down
191 changes: 191 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/archive.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,191 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// Modifications Copyright Kani Contributors
// See GitHub history for details.
// This file is a lightly modified version of upstream rustc:
// compiler/rustc_codegen_cranelift/src/archive.rs

// Along with lifting the deps:
// object = { version = "0.27.0", default-features = false, features = ["std", "read_core", "write", "archive", "coff", "elf", "macho", "pe"] }
// ar = "0.8.0"

// Also: I removed all mentions of 'ranlib' which caused issues on macos.
// We don't actually need these to be passed to a real linker anyway.
// 'ranlib' is about building a global symbol table out of all the object
// files in the archive, and we just don't put object files in our archives.

//! Creation of ar archives like for the lib and staticlib crate type

use std::fs::File;
use std::io::{self, Read, Seek};
use std::path::{Path, PathBuf};

use rustc_codegen_ssa::back::archive::ArchiveBuilder;
use rustc_session::Session;

use object::read::archive::ArchiveFile;
use object::ReadCache;

#[derive(Debug)]
enum ArchiveEntry {
FromArchive { archive_index: usize, file_range: (u64, u64) },
File(PathBuf),
}

pub(crate) struct ArArchiveBuilder<'a> {
sess: &'a Session,
dst: PathBuf,
use_gnu_style_archive: bool,

src_archives: Vec<File>,
// Don't use `HashMap` here, as the order is important. `rust.metadata.bin` must always be at
// the end of an archive for linkers to not get confused.
entries: Vec<(Vec<u8>, ArchiveEntry)>,
}

impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
fn new(sess: &'a Session, output: &Path, input: Option<&Path>) -> Self {
let (src_archives, entries) = if let Some(input) = input {
let read_cache = ReadCache::new(File::open(input).unwrap());
let archive = ArchiveFile::parse(&read_cache).unwrap();
let mut entries = Vec::new();

for entry in archive.members() {
let entry = entry.unwrap();
entries.push((
entry.name().to_vec(),
ArchiveEntry::FromArchive { archive_index: 0, file_range: entry.file_range() },
));
}

(vec![read_cache.into_inner()], entries)
} else {
(vec![], Vec::new())
};

ArArchiveBuilder {
sess,
dst: output.to_path_buf(),
use_gnu_style_archive: sess.target.archive_format == "gnu",
src_archives,
entries,
}
}

fn src_files(&mut self) -> Vec<String> {
self.entries.iter().map(|(name, _)| String::from_utf8(name.clone()).unwrap()).collect()
}

fn remove_file(&mut self, name: &str) {
let index = self
.entries
.iter()
.position(|(entry_name, _)| entry_name == name.as_bytes())
.expect("Tried to remove file not existing in src archive");
self.entries.remove(index);
}

fn add_file(&mut self, file: &Path) {
self.entries.push((
file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(),
ArchiveEntry::File(file.to_owned()),
));
}

fn add_archive<F>(&mut self, archive_path: &Path, mut skip: F) -> std::io::Result<()>
where
F: FnMut(&str) -> bool + 'static,
{
let read_cache = ReadCache::new(std::fs::File::open(&archive_path)?);
let archive = ArchiveFile::parse(&read_cache).unwrap();
let archive_index = self.src_archives.len();

for entry in archive.members() {
let entry = entry.map_err(|err| io::Error::new(io::ErrorKind::InvalidData, err))?;
let file_name = String::from_utf8(entry.name().to_vec())
.map_err(|err| io::Error::new(io::ErrorKind::InvalidData, err))?;
if !skip(&file_name) {
self.entries.push((
file_name.into_bytes(),
ArchiveEntry::FromArchive { archive_index, file_range: entry.file_range() },
));
}
}

self.src_archives.push(read_cache.into_inner());
Ok(())
}

fn build(mut self) {
enum BuilderKind {
Bsd(ar::Builder<File>),
Gnu(ar::GnuBuilder<File>),
}

let sess = self.sess;

let mut entries = Vec::new();

for (entry_name, entry) in self.entries {
// FIXME only read the symbol table of the object files to avoid having to keep all
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we want a tracking issue for the "FIXMEs" here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not our fixme, it's from the upstream file. I didn't remove it because I wanted to modify the file as minimally as possible.

// object files in memory at once, or read them twice.
let data = match entry {
ArchiveEntry::FromArchive { archive_index, file_range } => {
// FIXME read symbols from symtab
let src_read_cache = &mut self.src_archives[archive_index];

src_read_cache.seek(io::SeekFrom::Start(file_range.0)).unwrap();
let mut data = std::vec::from_elem(0, usize::try_from(file_range.1).unwrap());
src_read_cache.read_exact(&mut data).unwrap();

data
}
ArchiveEntry::File(file) => std::fs::read(file).unwrap_or_else(|err| {
sess.fatal(&format!(
"error while reading object file during archive building: {}",
err
));
}),
};

entries.push((entry_name, data));
}

let mut builder = if self.use_gnu_style_archive {
BuilderKind::Gnu(ar::GnuBuilder::new(
File::create(&self.dst).unwrap_or_else(|err| {
sess.fatal(&format!(
"error opening destination during archive building: {}",
err
));
}),
entries.iter().map(|(name, _)| name.clone()).collect(),
))
} else {
BuilderKind::Bsd(ar::Builder::new(File::create(&self.dst).unwrap_or_else(|err| {
sess.fatal(&format!("error opening destination during archive building: {}", err));
})))
};

// Add all files
for (entry_name, data) in entries.into_iter() {
let header = ar::Header::new(entry_name, data.len() as u64);
match builder {
BuilderKind::Bsd(ref mut builder) => builder.append(&header, &mut &*data).unwrap(),
BuilderKind::Gnu(ref mut builder) => builder.append(&header, &mut &*data).unwrap(),
}
}

// Finalize archive
std::mem::drop(builder);
}

fn inject_dll_import_lib(
&mut self,
_lib_name: &str,
_dll_imports: &[rustc_session::cstore::DllImport],
_tmpdir: &rustc_data_structures::temp_dir::MaybeTempDir,
) {
unimplemented!("injecting dll imports is not supported");
}
}
32 changes: 28 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -189,11 +189,35 @@ impl CodegenBackend for GotocCodegenBackend {

fn link(
&self,
_sess: &Session,
_codegen_results: CodegenResults,
_outputs: &OutputFilenames,
sess: &Session,
codegen_results: CodegenResults,
outputs: &OutputFilenames,
) -> Result<(), ErrorGuaranteed> {
Ok(())
// In `link`, we need to do two things:
// 1. We need to emit `rlib` files normally. Cargo expects these in some circumstances and sends
// them to subsequent builds with `-L`.
// 2. We MUST NOT try to invoke the native linker, because that will fail. We don't have real objects.
// This is normally not a problem: usually we only get one requested `crate-type`.
// But let's be careful and fail loudly if we get conflicting requests:
let requested_crate_types = sess.crate_types();
// Quit successfully if we don't need an `rlib`:
if !requested_crate_types.contains(&rustc_session::config::CrateType::Rlib) {
return Ok(());
}
// Fail loudly if we need an `rlib` (above!) and *also* an executable, which
// we can't produce, and can't easily suppress in `link_binary`:
if requested_crate_types.contains(&rustc_session::config::CrateType::Executable) {
sess.err("Build crate-type requested both rlib and executable, and Kani cannot handle this situation");
sess.abort_if_errors();
}

// All this ultimately boils down to is emitting an `rlib` that contains just one file: `lib.rmeta`
use rustc_codegen_ssa::back::link::link_binary;
link_binary::<crate::codegen_cprover_gotoc::archive::ArArchiveBuilder<'_>>(
sess,
&codegen_results,
outputs,
)
}
}

Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/codegen_cprover_gotoc/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
mod archive;
mod codegen;
mod compiler_interface;
mod context;
Expand Down
4 changes: 3 additions & 1 deletion kani-driver/src/call_single_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::path::{Path, PathBuf};
use std::process::Command;

use crate::session::KaniSession;
use crate::util::alter_extension;
use crate::util::{alter_extension, guess_rlib_name};

/// The outputs of kani-compiler operating on a single Rust source file.
pub struct SingleOutputs {
Expand All @@ -31,9 +31,11 @@ impl KaniSession {
let typemap_filename = alter_extension(file, "type_map.json");
let metadata_filename = alter_extension(file, "kani-metadata.json");
let restrictions_filename = alter_extension(file, "restrictions.json");
let rlib_filename = guess_rlib_name(file);

{
let mut temps = self.temporaries.borrow_mut();
temps.push(rlib_filename);
temps.push(output_filename.clone());
temps.push(typemap_filename);
temps.push(metadata_filename.clone());
Expand Down
21 changes: 21 additions & 0 deletions kani-driver/src/util.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,19 @@ pub fn alter_extension(path: &Path, ext: &str) -> PathBuf {
path.with_extension(ext)
}

/// Attempt to guess the rlib name for rust source file.
/// This is only used by 'kani', never 'cargo-kani', so we hopefully don't have too many corner
/// cases to deal with.
/// In rustc, you can find some code dealing this this naming in:
/// compiler/rustc_codegen_ssa/src/back/link.rs
pub fn guess_rlib_name(path: &Path) -> PathBuf {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a more reliable way to get the rlib name?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not as far as I can tell, will at least add a quick ref to rustc sources...

let basedir = path.parent().unwrap_or(Path::new("."));
let stem = path.file_stem().expect("has filename").to_str().expect("utf-8 filename");
let rlib_name = format!("lib{}.rlib", stem.replace('-', "_"));

basedir.join(rlib_name)
}

/// Add an extension to an existing file path (amazingly Rust doesn't support this well)
pub fn append_path(path: &Path, ext: &str) -> PathBuf {
let mut str = path.to_owned().into_os_string();
Expand Down Expand Up @@ -90,6 +103,14 @@ mod tests {
assert_eq!(alter_extension(&q, "symtab.json"), PathBuf::from("file.more.symtab.json"));
}

#[test]
fn check_guess_rlib_name() {
assert_eq!(guess_rlib_name(Path::new("mycrate.rs")), PathBuf::from("libmycrate.rlib"));
assert_eq!(guess_rlib_name(Path::new("my-crate.rs")), PathBuf::from("libmy_crate.rlib"));
assert_eq!(guess_rlib_name(Path::new("./foo.rs")), PathBuf::from("./libfoo.rlib"));
assert_eq!(guess_rlib_name(Path::new("a/b/foo.rs")), PathBuf::from("a/b/libfoo.rlib"));
}

#[test]
fn check_append_path() {
assert_eq!(append_path(&PathBuf::from("./file"), "tar"), PathBuf::from("./file.tar"));
Expand Down
Loading