Skip to content

Commit 91bf0ad

Browse files
committed
Upgrade toolchain to nightly-2022-09-13
Fixes model-checking#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.
1 parent 35b4b10 commit 91bf0ad

File tree

14 files changed

+170
-109
lines changed

14 files changed

+170
-109
lines changed

.cargo/config.toml

+4
Original file line numberDiff line numberDiff line change
@@ -28,4 +28,8 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
2828
"-Aclippy::expect_fun_call",
2929
"-Aclippy::or_fun_call",
3030
"-Aclippy::new_without_default",
31+
32+
# New lints that we are not compliant yet
33+
"-Aclippy::needless-borrow",
34+
"-Aclippy::bool-to-int-with-if",
3135
]

cprover_bindings/src/goto_program/expr.rs

+7
Original file line numberDiff line numberDiff line change
@@ -544,6 +544,13 @@ impl Expr {
544544
Self::double_constant(c)
545545
}
546546

547+
/// `if (c) { t } else { e }`
548+
pub fn if_then_else_expr(c: Expr, t: Expr, e: Expr) -> Self {
549+
assert!(c.typ().is_bool());
550+
assert!(t.typ() == e.typ());
551+
expr!(If { c, t, e }, t.typ().clone())
552+
}
553+
547554
pub fn empty_union(typ: Type, st: &SymbolTable) -> Self {
548555
assert!(typ.is_union() || typ.is_union_tag());
549556
assert!(typ.lookup_components(st).unwrap().is_empty());

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

+21-9
Original file line numberDiff line numberDiff line change
@@ -313,13 +313,6 @@ impl<'tcx> GotocCtx<'tcx> {
313313
($f:ident) => {{ codegen_intrinsic_binop!($f) }};
314314
}
315315

316-
// Intrinsics which encode a pointer comparison (e.g., `ptr_guaranteed_eq`).
317-
// These behave as regular pointer comparison at runtime:
318-
// https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq
319-
macro_rules! codegen_ptr_guaranteed_cmp {
320-
($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b).cast_to(Type::c_bool())) }};
321-
}
322-
323316
// Intrinsics which encode a simple binary operation
324317
macro_rules! codegen_intrinsic_binop {
325318
($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b)) }};
@@ -596,8 +589,7 @@ impl<'tcx> GotocCtx<'tcx> {
596589
"powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
597590
"powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
598591
"pref_align_of" => codegen_intrinsic_const!(),
599-
"ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq),
600-
"ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq),
592+
"ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, p),
601593
"ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
602594
"ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, p, loc),
603595
"raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
@@ -1012,6 +1004,26 @@ impl<'tcx> GotocCtx<'tcx> {
10121004
Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc)
10131005
}
10141006

1007+
// In some contexts (e.g., compilation-time evaluation),
1008+
// `ptr_guaranteed_cmp` compares two pointers and returns:
1009+
// * 2 if the result is unknown.
1010+
// * 1 if they are guaranteed to be equal.
1011+
// * 0 if they are guaranteed to be not equal.
1012+
// But at runtime, this intrinsic behaves as a regular pointer comparison.
1013+
// Therefore, we return 1 if the pointers are equal and 0 otherwise.
1014+
//
1015+
// This intrinsic replaces `ptr_guaranteed_eq` and `ptr_guaranteed_ne`:
1016+
// https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq
1017+
fn codegen_ptr_guaranteed_cmp(&mut self, mut fargs: Vec<Expr>, p: &Place<'tcx>) -> Stmt {
1018+
let a = fargs.remove(0);
1019+
let b = fargs.remove(0);
1020+
let place_type = self.place_ty(p);
1021+
let res_type = self.codegen_ty(place_type);
1022+
let eq_expr = a.eq(b);
1023+
let cmp_expr = Expr::if_then_else_expr(eq_expr, res_type.one(), res_type.zero());
1024+
self.codegen_expr_to_place(p, cmp_expr)
1025+
}
1026+
10151027
/// Computes the offset from a pointer.
10161028
///
10171029
/// Note that this function handles code generation for:

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -466,12 +466,12 @@ impl<'tcx> GotocCtx<'tcx> {
466466
}
467467

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

473473
let mut next_offset = Size::ZERO;
474-
for &(offset, alloc_id) in alloc.relocations().iter() {
474+
for &(offset, alloc_id) in alloc.provenance().iter() {
475475
if offset > next_offset {
476476
let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
477477
next_offset.bytes_usize()..offset.bytes_usize(),

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -504,7 +504,7 @@ impl<'tcx> GotocCtx<'tcx> {
504504
TagEncoding::Direct => {
505505
self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty))
506506
}
507-
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
507+
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
508508
// This code follows the logic in the ssa codegen backend:
509509
// https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
510510
// See also the cranelift backend:
@@ -550,7 +550,7 @@ impl<'tcx> GotocCtx<'tcx> {
550550
};
551551
is_niche.ternary(
552552
niche_discr,
553-
Expr::int_constant(dataful_variant.as_u32(), result_type),
553+
Expr::int_constant(untagged_variant.as_u32(), result_type),
554554
)
555555
}
556556
},

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

+16-9
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ use kani_queries::UserInput;
1111
use rustc_hir::def_id::DefId;
1212
use rustc_middle::mir;
1313
use rustc_middle::mir::{
14-
AssertKind, BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator,
15-
TerminatorKind,
14+
AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind,
15+
SwitchTargets, Terminator, TerminatorKind,
1616
};
1717
use rustc_middle::ty;
1818
use rustc_middle::ty::layout::LayoutOf;
@@ -89,8 +89,8 @@ impl<'tcx> GotocCtx<'tcx> {
8989
self.codegen_discriminant_field(place_goto_expr, pt)
9090
.assign(discr, location)
9191
}
92-
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
93-
if dataful_variant != variant_index {
92+
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
93+
if untagged_variant != variant_index {
9494
let offset = match &layout.fields {
9595
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
9696
_ => unreachable!("niche encoding must have arbitrary fields"),
@@ -122,11 +122,9 @@ impl<'tcx> GotocCtx<'tcx> {
122122
}
123123
StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
124124
StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
125-
StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping {
126-
ref src,
127-
ref dst,
128-
ref count,
129-
}) => {
125+
mir::StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping(
126+
mir::CopyNonOverlapping { ref src, ref dst, ref count },
127+
)) => {
130128
// Pack the operands and their types, then call `codegen_copy`
131129
let fargs = vec![
132130
self.codegen_operand(src),
@@ -137,6 +135,15 @@ impl<'tcx> GotocCtx<'tcx> {
137135
&[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)];
138136
self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location)
139137
}
138+
StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => {
139+
let cond = self.codegen_operand(op).cast_to(Type::bool());
140+
self.codegen_assert_assume(
141+
cond,
142+
PropertyClass::Assume,
143+
"assumption failed",
144+
location,
145+
)
146+
}
140147
StatementKind::FakeRead(_)
141148
| StatementKind::Retag(_, _)
142149
| StatementKind::AscribeUserType(_, _)

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

+72-59
Original file line numberDiff line numberDiff line change
@@ -1418,32 +1418,34 @@ impl<'tcx> GotocCtx<'tcx> {
14181418
subst: &'tcx InternalSubsts<'tcx>,
14191419
) -> Type {
14201420
let pretty_name = self.ty_pretty_name(ty);
1421-
self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |ctx, name| {
1422-
// variants appearing in source code (in source code order)
1423-
let source_variants = &adtdef.variants();
1424-
let layout = ctx.layout_of(ty);
1425-
// variants appearing in mir code
1426-
match &layout.variants {
1427-
Variants::Single { index } => {
1421+
// variants appearing in source code (in source code order)
1422+
let source_variants = &adtdef.variants();
1423+
let layout = self.layout_of(ty);
1424+
// variants appearing in mir code
1425+
match &layout.variants {
1426+
Variants::Single { index } => {
1427+
self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, _| {
14281428
match source_variants.get(*index) {
14291429
None => {
14301430
// an empty enum with no variants (its value cannot be instantiated)
14311431
vec![]
14321432
}
14331433
Some(variant) => {
14341434
// a single enum is pretty much like a struct
1435-
let layout = ctx.layout_of(ty).layout;
1436-
ctx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO)
1435+
let layout = gcx.layout_of(ty).layout;
1436+
gcx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO)
14371437
}
14381438
}
1439-
}
1440-
Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
1441-
// Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
1442-
assert!(layout.fields.count() <= 1);
1443-
// Contrary to generators, the discriminant is the first (and only) field for enums:
1444-
assert_eq!(*tag_field, 0);
1445-
match tag_encoding {
1446-
TagEncoding::Direct => {
1439+
})
1440+
}
1441+
Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
1442+
// Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
1443+
assert!(layout.fields.count() <= 1);
1444+
// Contrary to generators, the discriminant is the first (and only) field for enums:
1445+
assert_eq!(*tag_field, 0);
1446+
match tag_encoding {
1447+
TagEncoding::Direct => {
1448+
self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, name| {
14471449
// For direct encoding of tags, we generate a type with two fields:
14481450
// ```
14491451
// struct tag-<> { // enum type
@@ -1455,22 +1457,22 @@ impl<'tcx> GotocCtx<'tcx> {
14551457
// (`#[repr]`) and it represents which variant is being used.
14561458
// The `cases` field is a union of all variant types where the name
14571459
// of each union field is the name of the corresponding discriminant.
1458-
let discr_t = ctx.codegen_enum_discr_typ(ty);
1459-
let int = ctx.codegen_ty(discr_t);
1460-
let discr_offset = ctx.layout_of(discr_t).size;
1460+
let discr_t = gcx.codegen_enum_discr_typ(ty);
1461+
let int = gcx.codegen_ty(discr_t);
1462+
let discr_offset = gcx.layout_of(discr_t).size;
14611463
let initial_offset =
1462-
ctx.variant_min_offset(variants).unwrap_or(discr_offset);
1464+
gcx.variant_min_offset(variants).unwrap_or(discr_offset);
14631465
let mut fields = vec![DatatypeComponent::field("case", int)];
14641466
if let Some(padding) =
1465-
ctx.codegen_struct_padding(discr_offset, initial_offset, 0)
1467+
gcx.codegen_struct_padding(discr_offset, initial_offset, 0)
14661468
{
14671469
fields.push(padding);
14681470
}
14691471
let union_name = format!("{}-union", name);
14701472
let union_pretty_name = format!("{}-union", pretty_name);
14711473
fields.push(DatatypeComponent::field(
14721474
"cases",
1473-
ctx.ensure_union(&union_name, &union_pretty_name, |ctx, name| {
1475+
gcx.ensure_union(&union_name, &union_pretty_name, |ctx, name| {
14741476
ctx.codegen_enum_cases(
14751477
name,
14761478
pretty_name,
@@ -1482,45 +1484,56 @@ impl<'tcx> GotocCtx<'tcx> {
14821484
}),
14831485
));
14841486
fields
1485-
}
1486-
TagEncoding::Niche { dataful_variant, .. } => {
1487-
// Enumerations with multiple variants and niche encoding have a
1488-
// specific format that can be used to optimize its layout and reduce
1489-
// memory consumption.
1490-
//
1491-
// These enumerations have one and only one variant with non-ZST
1492-
// fields which is referred to by the `dataful_variant` index. Their
1493-
// final size and alignment is equal to the one from the
1494-
// `dataful_variant`. All other variants either don't have any field
1495-
// or all fields types are ZST.
1496-
//
1497-
// Because of that, we can represent these enums as simple structures
1498-
// where each field represent one variant. This allows them to be
1499-
// referred to correctly.
1500-
//
1501-
// Note: I tried using a union instead but it had a significant runtime
1502-
// penalty.
1503-
tracing::trace!(
1504-
?name,
1505-
?variants,
1506-
?dataful_variant,
1507-
?tag_encoding,
1508-
?subst,
1509-
"codegen_enum: Niche"
1510-
);
1511-
ctx.codegen_enum_cases(
1512-
name,
1513-
pretty_name,
1514-
adtdef,
1515-
subst,
1516-
variants,
1517-
Size::ZERO,
1518-
)
1519-
}
1487+
})
1488+
}
1489+
TagEncoding::Niche { .. } => {
1490+
self.codegen_enum_niche(ty, adtdef, subst, variants)
15201491
}
15211492
}
15221493
}
1523-
})
1494+
}
1495+
}
1496+
1497+
/// Codegen an enumeration that is encoded using niche optimization.
1498+
///
1499+
/// Enumerations with multiple variants and niche encoding have a
1500+
/// specific format that can be used to optimize its layout and reduce
1501+
/// memory consumption.
1502+
///
1503+
/// The niche is a location in the entire type where some bit pattern
1504+
/// isn't valid. The compiler uses the `untagged_variant` index to
1505+
/// access this field.
1506+
/// The final size and alignment is also equal to the one from the
1507+
/// `untagged_variant`. All other variants either don't have any field,
1508+
/// or their size is smaller than the `untagged_variant`.
1509+
/// See <https://github.com/rust-lang/rust/issues/46213> for more details.
1510+
///
1511+
/// Because of that, we usually represent these enums as simple unions
1512+
/// where each field represent one variant. This allows them to be
1513+
/// referred to correctly.
1514+
///
1515+
/// The one exception is the case where only one variant has data.
1516+
/// We use a struct instead because it is more performant.
1517+
fn codegen_enum_niche(
1518+
&mut self,
1519+
ty: Ty<'tcx>,
1520+
adtdef: &'tcx AdtDef,
1521+
subst: &'tcx InternalSubsts<'tcx>,
1522+
variants: &IndexVec<VariantIdx, Layout>,
1523+
) -> Type {
1524+
let non_zst_count = variants.iter().filter(|layout| layout.size().bytes() > 0).count();
1525+
let mangled_name = self.ty_mangled_name(ty);
1526+
let pretty_name = self.ty_pretty_name(ty);
1527+
tracing::trace!(?pretty_name, ?variants, ?subst, ?non_zst_count, "codegen_enum: Niche");
1528+
if non_zst_count > 1 {
1529+
self.ensure_union(mangled_name, pretty_name, |gcx, name| {
1530+
gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO)
1531+
})
1532+
} else {
1533+
self.ensure_struct(mangled_name, pretty_name, |gcx, name| {
1534+
gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO)
1535+
})
1536+
}
15241537
}
15251538

15261539
pub(crate) fn variant_min_offset(

kani-compiler/src/codegen_cprover_gotoc/reachability.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
9696

9797
// Collect initialization.
9898
let alloc = self.tcx.eval_static_initializer(def_id).unwrap();
99-
for &id in alloc.inner().relocations().values() {
99+
for &id in alloc.inner().provenance().values() {
100100
self.queue.extend(collect_alloc_items(self.tcx, id).iter());
101101
}
102102
}
@@ -202,7 +202,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
202202
}
203203
ConstValue::Slice { data: alloc, start: _, end: _ }
204204
| ConstValue::ByRef { alloc, .. } => {
205-
for &id in alloc.inner().relocations().values() {
205+
for &id in alloc.inner().provenance().values() {
206206
self.collected.extend(collect_alloc_items(self.tcx, id).iter())
207207
}
208208
}
@@ -542,7 +542,7 @@ fn collect_alloc_items<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec<MonoIt
542542
GlobalAlloc::Memory(alloc) => {
543543
trace!(?alloc_id, "global_alloc memory");
544544
items.extend(
545-
alloc.inner().relocations().values().flat_map(|id| collect_alloc_items(tcx, *id)),
545+
alloc.inner().provenance().values().flat_map(|id| collect_alloc_items(tcx, *id)),
546546
);
547547
}
548548
GlobalAlloc::VTable(ty, trait_ref) => {

kani-compiler/src/main.rs

+1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
#![feature(box_patterns)]
1313
#![feature(once_cell)]
1414
#![feature(rustc_private)]
15+
#![feature(more_qualified_paths)]
1516
extern crate rustc_ast;
1617
extern crate rustc_codegen_ssa;
1718
extern crate rustc_data_structures;

kani-driver/src/main.rs

+1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
#![feature(let_chains)]
34

45
use anyhow::Result;
56
use args_toml::join_args;

rust-toolchain.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2022-08-30"
5+
channel = "nightly-2022-09-13"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)