Skip to content

Commit

Permalink
Upgrade toolchain to nightly-2022-09-13 (#1737)
Browse files Browse the repository at this point in the history
Fixes #1615

Relevant changes to rustc:
  - rust-lang/rust#101483: Change to intrinsics.
  - rust-lang/rust#94075: Change to niche opt.
  - rust-lang/rust#101101: Method rename.

Co-authored-by: Adrian Palacios <[email protected]>
  • Loading branch information
celinval and adpaco-aws authored Oct 3, 2022
1 parent 78761bd commit 07092de
Show file tree
Hide file tree
Showing 14 changed files with 163 additions and 111 deletions.
4 changes: 4 additions & 0 deletions .cargo/config.toml
Original file line number Diff line number Diff line change
Expand Up @@ -28,4 +28,8 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
"-Aclippy::expect_fun_call",
"-Aclippy::or_fun_call",
"-Aclippy::new_without_default",

# New lints that we are not compliant yet
"-Aclippy::needless-borrow",
"-Aclippy::bool-to-int-with-if",
]
30 changes: 21 additions & 9 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -313,13 +313,6 @@ impl<'tcx> GotocCtx<'tcx> {
($f:ident) => {{ codegen_intrinsic_binop!($f) }};
}

// Intrinsics which encode a pointer comparison (e.g., `ptr_guaranteed_eq`).
// These behave as regular pointer comparison at runtime:
// https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq
macro_rules! codegen_ptr_guaranteed_cmp {
($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b).cast_to(Type::c_bool())) }};
}

// Intrinsics which encode a simple binary operation
macro_rules! codegen_intrinsic_binop {
($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b)) }};
Expand Down Expand Up @@ -596,8 +589,7 @@ impl<'tcx> GotocCtx<'tcx> {
"powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
"powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
"pref_align_of" => codegen_intrinsic_const!(),
"ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq),
"ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq),
"ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, p),
"ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
"ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, p, loc),
"raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
Expand Down Expand Up @@ -1012,6 +1004,26 @@ impl<'tcx> GotocCtx<'tcx> {
Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc)
}

// In some contexts (e.g., compilation-time evaluation),
// `ptr_guaranteed_cmp` compares two pointers and returns:
// * 2 if the result is unknown.
// * 1 if they are guaranteed to be equal.
// * 0 if they are guaranteed to be not equal.
// But at runtime, this intrinsic behaves as a regular pointer comparison.
// Therefore, we return 1 if the pointers are equal and 0 otherwise.
//
// This intrinsic replaces `ptr_guaranteed_eq` and `ptr_guaranteed_ne`:
// https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq
fn codegen_ptr_guaranteed_cmp(&mut self, mut fargs: Vec<Expr>, p: &Place<'tcx>) -> Stmt {
let a = fargs.remove(0);
let b = fargs.remove(0);
let place_type = self.place_ty(p);
let res_type = self.codegen_ty(place_type);
let eq_expr = a.eq(b);
let cmp_expr = eq_expr.ternary(res_type.one(), res_type.zero());
self.codegen_expr_to_place(p, cmp_expr)
}

/// Computes the offset from a pointer.
///
/// Note that this function handles code generation for:
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -466,12 +466,12 @@ impl<'tcx> GotocCtx<'tcx> {
}

fn codegen_allocation_data(&mut self, alloc: &'tcx Allocation) -> Vec<AllocData<'tcx>> {
let mut alloc_vals = Vec::with_capacity(alloc.relocations().len() + 1);
let mut alloc_vals = Vec::with_capacity(alloc.provenance().len() + 1);
let pointer_size =
Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes());

let mut next_offset = Size::ZERO;
for &(offset, alloc_id) in alloc.relocations().iter() {
for &(offset, alloc_id) in alloc.provenance().iter() {
if offset > next_offset {
let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
next_offset.bytes_usize()..offset.bytes_usize(),
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -504,7 +504,7 @@ impl<'tcx> GotocCtx<'tcx> {
TagEncoding::Direct => {
self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty))
}
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
// This code follows the logic in the ssa codegen backend:
// https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
// See also the cranelift backend:
Expand Down Expand Up @@ -550,7 +550,7 @@ impl<'tcx> GotocCtx<'tcx> {
};
is_niche.ternary(
niche_discr,
Expr::int_constant(dataful_variant.as_u32(), result_type),
Expr::int_constant(untagged_variant.as_u32(), result_type),
)
}
},
Expand Down
25 changes: 16 additions & 9 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@ use kani_queries::UserInput;
use rustc_hir::def_id::DefId;
use rustc_middle::mir;
use rustc_middle::mir::{
AssertKind, BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator,
TerminatorKind,
AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind,
SwitchTargets, Terminator, TerminatorKind,
};
use rustc_middle::ty;
use rustc_middle::ty::layout::LayoutOf;
Expand Down Expand Up @@ -89,8 +89,8 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_discriminant_field(place_goto_expr, pt)
.assign(discr, location)
}
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
if dataful_variant != variant_index {
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
if untagged_variant != variant_index {
let offset = match &layout.fields {
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
_ => unreachable!("niche encoding must have arbitrary fields"),
Expand Down Expand Up @@ -122,11 +122,9 @@ impl<'tcx> GotocCtx<'tcx> {
}
StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping {
ref src,
ref dst,
ref count,
}) => {
StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping(
mir::CopyNonOverlapping { ref src, ref dst, ref count },
)) => {
// Pack the operands and their types, then call `codegen_copy`
let fargs = vec![
self.codegen_operand(src),
Expand All @@ -137,6 +135,15 @@ impl<'tcx> GotocCtx<'tcx> {
&[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)];
self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location)
}
StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => {
let cond = self.codegen_operand(op).cast_to(Type::bool());
self.codegen_assert_assume(
cond,
PropertyClass::Assume,
"assumption failed",
location,
)
}
StatementKind::FakeRead(_)
| StatementKind::Retag(_, _)
| StatementKind::AscribeUserType(_, _)
Expand Down
131 changes: 72 additions & 59 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1418,32 +1418,34 @@ impl<'tcx> GotocCtx<'tcx> {
subst: &'tcx InternalSubsts<'tcx>,
) -> Type {
let pretty_name = self.ty_pretty_name(ty);
self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |ctx, name| {
// variants appearing in source code (in source code order)
let source_variants = &adtdef.variants();
let layout = ctx.layout_of(ty);
// variants appearing in mir code
match &layout.variants {
Variants::Single { index } => {
// variants appearing in source code (in source code order)
let source_variants = &adtdef.variants();
let layout = self.layout_of(ty);
// variants appearing in mir code
match &layout.variants {
Variants::Single { index } => {
self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, _| {
match source_variants.get(*index) {
None => {
// an empty enum with no variants (its value cannot be instantiated)
vec![]
}
Some(variant) => {
// a single enum is pretty much like a struct
let layout = ctx.layout_of(ty).layout;
ctx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO)
let layout = gcx.layout_of(ty).layout;
gcx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO)
}
}
}
Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
// Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
assert!(layout.fields.count() <= 1);
// Contrary to generators, the discriminant is the first (and only) field for enums:
assert_eq!(*tag_field, 0);
match tag_encoding {
TagEncoding::Direct => {
})
}
Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
// Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
assert!(layout.fields.count() <= 1);
// Contrary to generators, the discriminant is the first (and only) field for enums:
assert_eq!(*tag_field, 0);
match tag_encoding {
TagEncoding::Direct => {
self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, name| {
// For direct encoding of tags, we generate a type with two fields:
// ```
// struct tag-<> { // enum type
Expand All @@ -1455,22 +1457,22 @@ impl<'tcx> GotocCtx<'tcx> {
// (`#[repr]`) and it represents which variant is being used.
// The `cases` field is a union of all variant types where the name
// of each union field is the name of the corresponding discriminant.
let discr_t = ctx.codegen_enum_discr_typ(ty);
let int = ctx.codegen_ty(discr_t);
let discr_offset = ctx.layout_of(discr_t).size;
let discr_t = gcx.codegen_enum_discr_typ(ty);
let int = gcx.codegen_ty(discr_t);
let discr_offset = gcx.layout_of(discr_t).size;
let initial_offset =
ctx.variant_min_offset(variants).unwrap_or(discr_offset);
gcx.variant_min_offset(variants).unwrap_or(discr_offset);
let mut fields = vec![DatatypeComponent::field("case", int)];
if let Some(padding) =
ctx.codegen_struct_padding(discr_offset, initial_offset, 0)
gcx.codegen_struct_padding(discr_offset, initial_offset, 0)
{
fields.push(padding);
}
let union_name = format!("{}-union", name);
let union_pretty_name = format!("{}-union", pretty_name);
fields.push(DatatypeComponent::field(
"cases",
ctx.ensure_union(&union_name, &union_pretty_name, |ctx, name| {
gcx.ensure_union(&union_name, &union_pretty_name, |ctx, name| {
ctx.codegen_enum_cases(
name,
pretty_name,
Expand All @@ -1482,45 +1484,56 @@ impl<'tcx> GotocCtx<'tcx> {
}),
));
fields
}
TagEncoding::Niche { dataful_variant, .. } => {
// Enumerations with multiple variants and niche encoding have a
// specific format that can be used to optimize its layout and reduce
// memory consumption.
//
// These enumerations have one and only one variant with non-ZST
// fields which is referred to by the `dataful_variant` index. Their
// final size and alignment is equal to the one from the
// `dataful_variant`. All other variants either don't have any field
// or all fields types are ZST.
//
// Because of that, we can represent these enums as simple structures
// where each field represent one variant. This allows them to be
// referred to correctly.
//
// Note: I tried using a union instead but it had a significant runtime
// penalty.
tracing::trace!(
?name,
?variants,
?dataful_variant,
?tag_encoding,
?subst,
"codegen_enum: Niche"
);
ctx.codegen_enum_cases(
name,
pretty_name,
adtdef,
subst,
variants,
Size::ZERO,
)
}
})
}
TagEncoding::Niche { .. } => {
self.codegen_enum_niche(ty, adtdef, subst, variants)
}
}
}
})
}
}

/// Codegen an enumeration that is encoded using niche optimization.
///
/// Enumerations with multiple variants and niche encoding have a
/// specific format that can be used to optimize its layout and reduce
/// memory consumption.
///
/// The niche is a location in the entire type where some bit pattern
/// isn't valid. The compiler uses the `untagged_variant` index to
/// access this field.
/// The final size and alignment is also equal to the one from the
/// `untagged_variant`. All other variants either don't have any field,
/// or their size is smaller than the `untagged_variant`.
/// See <https://github.com/rust-lang/rust/issues/46213> for more details.
///
/// Because of that, we usually represent these enums as simple unions
/// where each field represent one variant. This allows them to be
/// referred to correctly.
///
/// The one exception is the case where only one variant has data.
/// We use a struct instead because it is more performant.
fn codegen_enum_niche(
&mut self,
ty: Ty<'tcx>,
adtdef: &'tcx AdtDef,
subst: &'tcx InternalSubsts<'tcx>,
variants: &IndexVec<VariantIdx, Layout>,
) -> Type {
let non_zst_count = variants.iter().filter(|layout| layout.size().bytes() > 0).count();
let mangled_name = self.ty_mangled_name(ty);
let pretty_name = self.ty_pretty_name(ty);
tracing::trace!(?pretty_name, ?variants, ?subst, ?non_zst_count, "codegen_enum: Niche");
if non_zst_count > 1 {
self.ensure_union(mangled_name, pretty_name, |gcx, name| {
gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO)
})
} else {
self.ensure_struct(mangled_name, pretty_name, |gcx, name| {
gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO)
})
}
}

pub(crate) fn variant_min_offset(
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {

// Collect initialization.
let alloc = self.tcx.eval_static_initializer(def_id).unwrap();
for &id in alloc.inner().relocations().values() {
for &id in alloc.inner().provenance().values() {
self.queue.extend(collect_alloc_items(self.tcx, id).iter());
}
}
Expand Down Expand Up @@ -202,7 +202,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
}
ConstValue::Slice { data: alloc, start: _, end: _ }
| ConstValue::ByRef { alloc, .. } => {
for &id in alloc.inner().relocations().values() {
for &id in alloc.inner().provenance().values() {
self.collected.extend(collect_alloc_items(self.tcx, id).iter())
}
}
Expand Down Expand Up @@ -542,7 +542,7 @@ fn collect_alloc_items<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec<MonoIt
GlobalAlloc::Memory(alloc) => {
trace!(?alloc_id, "global_alloc memory");
items.extend(
alloc.inner().relocations().values().flat_map(|id| collect_alloc_items(tcx, *id)),
alloc.inner().provenance().values().flat_map(|id| collect_alloc_items(tcx, *id)),
);
}
GlobalAlloc::VTable(ty, trait_ref) => {
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
#![feature(box_patterns)]
#![feature(once_cell)]
#![feature(rustc_private)]
#![feature(more_qualified_paths)]
extern crate rustc_ast;
extern crate rustc_codegen_ssa;
extern crate rustc_data_structures;
Expand Down
1 change: 1 addition & 0 deletions kani-driver/src/main.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
#![feature(let_chains)]

use anyhow::Result;
use args_toml::join_args;
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
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-08-30"
channel = "nightly-2022-09-13"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 0 additions & 2 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,6 @@
//! binaries will download the appropriate Kani release bundle and invoke
//! the "real" `kani` and `cargo-kani` binaries.
#![warn(clippy::all, clippy::cargo)]

mod cmd;
mod os_hacks;
mod setup;
Expand Down
Loading

0 comments on commit 07092de

Please sign in to comment.