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

Update toolchain to 2022-07-05 #1340

Merged
merged 6 commits into from
Jul 6, 2022
Merged

Update toolchain to 2022-07-05 #1340

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
4a4539b
Update toolchain to 2022-07-05
celinval Jul 6, 2022
71b1188
Codegen unimplemented for unsupported constant slices
celinval Jul 6, 2022
9f17da9
Fix copyright check
celinval Jul 6, 2022
6134f1d
Use codegen_option_span instead
celinval Jul 6, 2022
5821f87
Merge branch 'main' into issue-1336-toolchain
celinval Jul 6, 2022
519ed87
Merge branch 'main' into issue-1336-toolchain
celinval Jul 6, 2022
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
41 changes: 6 additions & 35 deletions kani-compiler/src/codegen_cprover_gotoc/archive.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,47 +44,16 @@ pub(crate) struct ArArchiveBuilder<'a> {
}

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())
};

fn new(sess: &'a Session, output: &Path) -> Self {
Copy link
Contributor

Choose a reason for hiding this comment

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

Idle comment: I copied this file (with minor changes) from cranelift. After I did so, I heard that it got updated/simplified.

It's been on my todo list to look into whether I should re-copy it.

I notice that rust-lang/rust#97485 exists though, and that might ultimately let us just delete this file. I'll track that instead?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

That would be great!

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

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(),
Expand Down Expand Up @@ -116,7 +85,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
Ok(())
}

fn build(mut self) {
fn build(mut self) -> bool {
enum BuilderKind {
Bsd(ar::Builder<File>),
Gnu(ar::GnuBuilder<File>),
Expand Down Expand Up @@ -168,6 +137,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
};

// Add all files
let any_members = !entries.is_empty();
for (entry_name, data) in entries.into_iter() {
let header = ar::Header::new(entry_name, data.len() as u64);
match builder {
Expand All @@ -178,6 +148,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {

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

fn inject_dll_import_lib(
Expand Down
86 changes: 43 additions & 43 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -396,79 +396,79 @@ impl<'tcx> GotocCtx<'tcx> {
"assumption failed",
loc,
),
"atomic_and" => codegen_atomic_binop!(bitand),
"atomic_and_acq" => codegen_atomic_binop!(bitand),
"atomic_and_seqcst" => codegen_atomic_binop!(bitand),
"atomic_and_acquire" => codegen_atomic_binop!(bitand),
"atomic_and_acqrel" => codegen_atomic_binop!(bitand),
"atomic_and_rel" => codegen_atomic_binop!(bitand),
"atomic_and_release" => codegen_atomic_binop!(bitand),
"atomic_and_relaxed" => codegen_atomic_binop!(bitand),
name if name.starts_with("atomic_cxchg") => {
self.codegen_atomic_cxchg(intrinsic, fargs, p, loc)
}
"atomic_fence" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_fence_acq" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_fence_seqcst" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_fence_acquire" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_fence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_fence_rel" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_load" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_load_acq" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_fence_release" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_load_seqcst" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_load_acquire" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_load_relaxed" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_load_unordered" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
"atomic_max" => codegen_atomic_binop!(max),
"atomic_max_acq" => codegen_atomic_binop!(max),
"atomic_max_seqcst" => codegen_atomic_binop!(max),
"atomic_max_acquire" => codegen_atomic_binop!(max),
"atomic_max_acqrel" => codegen_atomic_binop!(max),
"atomic_max_rel" => codegen_atomic_binop!(max),
"atomic_max_release" => codegen_atomic_binop!(max),
"atomic_max_relaxed" => codegen_atomic_binop!(max),
"atomic_min" => codegen_atomic_binop!(min),
"atomic_min_acq" => codegen_atomic_binop!(min),
"atomic_min_seqcst" => codegen_atomic_binop!(min),
"atomic_min_acquire" => codegen_atomic_binop!(min),
"atomic_min_acqrel" => codegen_atomic_binop!(min),
"atomic_min_rel" => codegen_atomic_binop!(min),
"atomic_min_release" => codegen_atomic_binop!(min),
"atomic_min_relaxed" => codegen_atomic_binop!(min),
"atomic_nand" => codegen_atomic_binop!(bitnand),
"atomic_nand_acq" => codegen_atomic_binop!(bitnand),
"atomic_nand_seqcst" => codegen_atomic_binop!(bitnand),
"atomic_nand_acquire" => codegen_atomic_binop!(bitnand),
"atomic_nand_acqrel" => codegen_atomic_binop!(bitnand),
"atomic_nand_rel" => codegen_atomic_binop!(bitnand),
"atomic_nand_release" => codegen_atomic_binop!(bitnand),
"atomic_nand_relaxed" => codegen_atomic_binop!(bitnand),
"atomic_or" => codegen_atomic_binop!(bitor),
"atomic_or_acq" => codegen_atomic_binop!(bitor),
"atomic_or_seqcst" => codegen_atomic_binop!(bitor),
"atomic_or_acquire" => codegen_atomic_binop!(bitor),
"atomic_or_acqrel" => codegen_atomic_binop!(bitor),
"atomic_or_rel" => codegen_atomic_binop!(bitor),
"atomic_or_release" => codegen_atomic_binop!(bitor),
"atomic_or_relaxed" => codegen_atomic_binop!(bitor),
"atomic_singlethreadfence" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_singlethreadfence_acq" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_singlethreadfence_seqcst" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_singlethreadfence_acquire" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_singlethreadfence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_singlethreadfence_rel" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_store" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_store_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_singlethreadfence_release" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_store_seqcst" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_store_release" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_store_unordered" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_umax" => codegen_atomic_binop!(max),
"atomic_umax_acq" => codegen_atomic_binop!(max),
"atomic_umax_seqcst" => codegen_atomic_binop!(max),
"atomic_umax_acquire" => codegen_atomic_binop!(max),
"atomic_umax_acqrel" => codegen_atomic_binop!(max),
"atomic_umax_rel" => codegen_atomic_binop!(max),
"atomic_umax_release" => codegen_atomic_binop!(max),
"atomic_umax_relaxed" => codegen_atomic_binop!(max),
"atomic_umin" => codegen_atomic_binop!(min),
"atomic_umin_acq" => codegen_atomic_binop!(min),
"atomic_umin_seqcst" => codegen_atomic_binop!(min),
"atomic_umin_acquire" => codegen_atomic_binop!(min),
"atomic_umin_acqrel" => codegen_atomic_binop!(min),
"atomic_umin_rel" => codegen_atomic_binop!(min),
"atomic_umin_release" => codegen_atomic_binop!(min),
"atomic_umin_relaxed" => codegen_atomic_binop!(min),
"atomic_xadd" => codegen_atomic_binop!(plus),
"atomic_xadd_acq" => codegen_atomic_binop!(plus),
"atomic_xadd_seqcst" => codegen_atomic_binop!(plus),
"atomic_xadd_acquire" => codegen_atomic_binop!(plus),
"atomic_xadd_acqrel" => codegen_atomic_binop!(plus),
"atomic_xadd_rel" => codegen_atomic_binop!(plus),
"atomic_xadd_release" => codegen_atomic_binop!(plus),
"atomic_xadd_relaxed" => codegen_atomic_binop!(plus),
"atomic_xchg" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xchg_acq" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xchg_seqcst" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xchg_acquire" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xchg_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xchg_release" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
"atomic_xor" => codegen_atomic_binop!(bitxor),
"atomic_xor_acq" => codegen_atomic_binop!(bitxor),
"atomic_xor_seqcst" => codegen_atomic_binop!(bitxor),
"atomic_xor_acquire" => codegen_atomic_binop!(bitxor),
"atomic_xor_acqrel" => codegen_atomic_binop!(bitxor),
"atomic_xor_rel" => codegen_atomic_binop!(bitxor),
"atomic_xor_release" => codegen_atomic_binop!(bitxor),
"atomic_xor_relaxed" => codegen_atomic_binop!(bitxor),
"atomic_xsub" => codegen_atomic_binop!(sub),
"atomic_xsub_acq" => codegen_atomic_binop!(sub),
"atomic_xsub_seqcst" => codegen_atomic_binop!(sub),
"atomic_xsub_acquire" => codegen_atomic_binop!(sub),
"atomic_xsub_acqrel" => codegen_atomic_binop!(sub),
"atomic_xsub_rel" => codegen_atomic_binop!(sub),
"atomic_xsub_release" => codegen_atomic_binop!(sub),
"atomic_xsub_relaxed" => codegen_atomic_binop!(sub),
"bitreverse" => self.codegen_expr_to_place(p, fargs.remove(0).bitreverse()),
// black_box is an identity function that hints to the compiler
Expand Down
25 changes: 17 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ impl<'tcx> GotocCtx<'tcx> {
debug!("found literal: {:?}", lit);
let lit = self.monomorphize(lit);

match lit.val() {
match lit.kind() {
// evaluate constant if it has no been evaluated yet
ConstKind::Unevaluated(unevaluated) => {
debug!("The literal was a Unevaluated");
Expand All @@ -68,14 +68,15 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_const_value(const_val, lit.ty(), span)
}

ConstKind::Value(v) => {
debug!("The literal was a ConstValue {:?}", v);
self.codegen_const_value(v, lit.ty(), span)
ConstKind::Value(valtree) => {
let value = self.tcx.valtree_to_const_val((lit.ty(), valtree));
debug!("The literal was a ConstValue {:?}", value);
self.codegen_const_value(value, lit.ty(), span)
}
_ => {
unreachable!(
"monomorphized item shouldn't have this constant value: {:?}",
lit.val()
lit.kind()
)
}
}
Expand Down Expand Up @@ -104,8 +105,6 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Slice(slice_ty) => {
if let Uint(UintTy::U8) = slice_ty.kind() {
// The case where we have a slice of u8 is easy enough: make an array of u8
// TODO: Handle cases with larger int types by making an array of bytes,
// then using byte-extract on it.
let slice =
data.inspect_with_uninit_and_ptr_outside_interpreter(start..end);
let vec_of_bytes: Vec<Expr> = slice
Expand All @@ -123,12 +122,22 @@ impl<'tcx> GotocCtx<'tcx> {
len_expr,
&self.symbol_table,
);
} else {
// TODO: Handle cases with other types such as tuples and larger integers.
let loc = self.codegen_span_option(span.cloned());
let typ = self.codegen_ty(lit_ty);
return self.codegen_unimplemented(
"Constant slice value with 2+ bytes",
typ,
loc,
"https://github.com/model-checking/kani/issues/1339",
);
}
}
_ => {}
Copy link
Contributor

Choose a reason for hiding this comment

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

What does this do?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I believe this is a no-op. In this case, the unimplemented!() macro will be invoked at the end.

}
}
unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty, span);
unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty.kind(), span);
}

pub fn codegen_const_value(
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -446,7 +446,7 @@ impl<'tcx> GotocCtx<'tcx> {
// https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
match before.mir_typ().kind() {
ty::Array(ty, len) => {
let len = len.val().try_to_machine_usize(self.tcx).unwrap();
let len = len.kind().try_to_machine_usize(self.tcx).unwrap();
let subarray_len = if from_end {
// `to` counts from the end of the array
len - to - from
Expand Down Expand Up @@ -578,7 +578,7 @@ impl<'tcx> GotocCtx<'tcx> {
match before.mir_typ().kind() {
//TODO, ask on zulip if we can ever have from_end here?
ty::Array(elemt, length) => {
let length = length.val().try_to_machine_usize(self.tcx).unwrap();
let length = length.kind().try_to_machine_usize(self.tcx).unwrap();
assert!(length >= min_length);
let idx = if from_end { length - offset } else { offset };
let idxe = Expr::int_constant(idx, Type::ssize_t());
Expand Down
8 changes: 4 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,8 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
use rustc_middle::ty::Instance;
use rustc_span::def_id::DefId;
use std::cell::RefCell;
use std::lazy::SyncLazy;
use std::panic;
use std::sync::LazyLock;
use tracing::debug;

// Use a thread-local global variable to track the current codegen item for debugging.
Expand All @@ -21,12 +21,12 @@ thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<String>, Option<Locat

pub fn init() {
// Install panic hook
SyncLazy::force(&DEFAULT_HOOK); // Install ice hook
LazyLock::force(&DEFAULT_HOOK); // Install ice hook
}

// Custom panic hook to add more information when panic occurs during goto-c codegen.
static DEFAULT_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
SyncLazy::new(|| {
static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
LazyLock::new(|| {
let hook = panic::take_hook();
panic::set_hook(Box::new(|info| {
// Invoke the default handler, which prints the actual panic message and
Expand Down
8 changes: 4 additions & 4 deletions kani-compiler/src/session.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@

use crate::parser;
use clap::ArgMatches;
use std::lazy::SyncLazy;
use std::panic;
use std::str::FromStr;
use std::sync::LazyLock;
use tracing_subscriber::{filter::Directive, layer::SubscriberExt, EnvFilter, Registry};
use tracing_tree::HierarchicalLayer;

Expand All @@ -19,8 +19,8 @@ const BUG_REPORT_URL: &str =
"https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md";

// Custom panic hook.
static PANIC_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
SyncLazy::new(|| {
static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
LazyLock::new(|| {
let hook = panic::take_hook();
panic::set_hook(Box::new(|info| {
// Print stack trace.
Expand Down Expand Up @@ -92,5 +92,5 @@ fn hier_logs(args: &ArgMatches, filter: EnvFilter) {

fn init_panic_hook() {
// Install panic hook
SyncLazy::force(&PANIC_HOOK); // Install ice hook
LazyLock::force(&PANIC_HOOK); // Install ice hook
}
2 changes: 1 addition & 1 deletion rust-toolchain.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2022-06-09"
channel = "nightly-2022-07-05"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
9 changes: 5 additions & 4 deletions tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@

#![feature(core_intrinsics)]
use std::intrinsics::{
atomic_xadd, atomic_xadd_acq, atomic_xadd_acqrel, atomic_xadd_rel, atomic_xadd_relaxed,
atomic_xadd_acqrel, atomic_xadd_acquire, atomic_xadd_relaxed, atomic_xadd_release,
atomic_xadd_seqcst,
};

#[kani::proof]
Expand All @@ -27,10 +28,10 @@ fn main() {
let c = 1 as u8;

unsafe {
let x1 = atomic_xadd(ptr_a1, b);
let x2 = atomic_xadd_acq(ptr_a2, b);
let x1 = atomic_xadd_seqcst(ptr_a1, b);
let x2 = atomic_xadd_acquire(ptr_a2, b);
let x3 = atomic_xadd_acqrel(ptr_a3, b);
let x4 = atomic_xadd_rel(ptr_a4, b);
let x4 = atomic_xadd_release(ptr_a4, b);
let x5 = atomic_xadd_relaxed(ptr_a5, b);

assert!(x1 == 0);
Expand Down
11 changes: 6 additions & 5 deletions tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,13 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Check that `atomic_and` and other variants (unstable version) return the
// Check that `atomic_and_seqcst` and other variants (unstable version) return the
// expected result.

#![feature(core_intrinsics)]
use std::intrinsics::{
atomic_and, atomic_and_acq, atomic_and_acqrel, atomic_and_rel, atomic_and_relaxed,
atomic_and_acqrel, atomic_and_acquire, atomic_and_relaxed, atomic_and_release,
atomic_and_seqcst,
};

#[kani::proof]
Expand All @@ -26,10 +27,10 @@ fn main() {
let b = 0 as u8;

unsafe {
let x1 = atomic_and(ptr_a1, b);
let x2 = atomic_and_acq(ptr_a2, b);
let x1 = atomic_and_seqcst(ptr_a1, b);
let x2 = atomic_and_acquire(ptr_a2, b);
let x3 = atomic_and_acqrel(ptr_a3, b);
let x4 = atomic_and_rel(ptr_a4, b);
let x4 = atomic_and_release(ptr_a4, b);
let x5 = atomic_and_relaxed(ptr_a5, b);

assert!(x1 == 1);
Expand Down
Loading