From 22b14f400edf6cd0e70f464e7aa31c667ce6c244 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 15 Apr 2023 00:43:15 +0200 Subject: [PATCH] Upgrade toolchain to 2023-02-05 (#2347) Co-authored-by: Celina G. Val --- .../codegen_cprover_gotoc/codegen/place.rs | 11 ++ .../codegen_cprover_gotoc/codegen/rvalue.rs | 153 ++++++++++++++++-- .../codegen/statement.rs | 126 ++++++++------- rust-toolchain.toml | 2 +- tests/kani/Enum/multiple_never.rs | 39 +++++ tests/kani/Enum/one_two.rs | 23 +++ 6 files changed, 282 insertions(+), 72 deletions(-) create mode 100644 tests/kani/Enum/multiple_never.rs create mode 100644 tests/kani/Enum/one_two.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 67801f747acc..72440401275a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -624,6 +624,17 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Given a projection, generate an lvalue that represents the given variant index. + pub fn codegen_variant_lvalue( + &mut self, + initial_projection: ProjectedPlace<'tcx>, + variant_idx: VariantIdx, + ) -> ProjectedPlace<'tcx> { + debug!(?initial_projection, ?variant_idx, "codegen_variant_lvalue"); + let downcast = ProjectionElem::Downcast(None, variant_idx); + self.codegen_projection(Ok(initial_projection), downcast).unwrap() + } + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html // ConstantIndex // [−] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index fc6d87bf440a..e17cd7f3031a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use super::typ::pointee_type; +use crate::codegen_cprover_gotoc::codegen::place::{ProjectedPlace, TypeOrVariant}; use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; @@ -17,9 +18,9 @@ use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; -use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants}; +use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants}; use std::collections::BTreeMap; -use tracing::{debug, warn}; +use tracing::{debug, trace, warn}; impl<'tcx> GotocCtx<'tcx> { fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand<'tcx>, e2: &Operand<'tcx>) -> Expr { @@ -279,13 +280,112 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Create an initializer for a generator struct. + fn codegen_rvalue_generator(&mut self, operands: &[Operand<'tcx>], ty: Ty<'tcx>) -> Expr { + let layout = self.layout_of(ty); + let discriminant_field = match &layout.variants { + Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field, + _ => unreachable!( + "Expected generators to have multiple variants and direct encoding, but found: {layout:?}" + ), + }; + let overall_t = self.codegen_ty(ty); + let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap(); + let mut operands_iter = operands.iter(); + let direct_fields_expr = Expr::struct_expr_from_values( + direct_fields.typ(), + layout + .fields + .index_by_increasing_offset() + .map(|idx| { + let field_ty = layout.field(self, idx).ty; + if idx == *discriminant_field { + Expr::int_constant(0, self.codegen_ty(field_ty)) + } else { + self.codegen_operand(operands_iter.next().unwrap()) + } + }) + .collect(), + &self.symbol_table, + ); + assert!(operands_iter.next().is_none()); + Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table) + } + + /// This code will generate an expression that initializes an enumeration. + /// + /// It will first create a temporary variant with the same enum type. + /// Initialize the case structure and set its discriminant. + /// Finally, it will return the temporary value. + fn codegen_rvalue_enum_aggregate( + &mut self, + variant_index: VariantIdx, + operands: &[Operand<'tcx>], + res_ty: Ty<'tcx>, + loc: Location, + ) -> Expr { + let mut stmts = vec![]; + let typ = self.codegen_ty(res_ty); + // 1- Create a temporary value of the enum type. + tracing::debug!(?typ, ?res_ty, "aggregate_enum"); + let (temp_var, decl) = self.decl_temp_variable(typ.clone(), None, loc); + stmts.push(decl); + if !operands.is_empty() { + // 2- Initialize the members of the temporary variant. + let initial_projection = ProjectedPlace::try_new( + temp_var.clone(), + TypeOrVariant::Type(res_ty), + None, + None, + self, + ) + .unwrap(); + let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index); + let variant_expr = variant_proj.goto_expr.clone(); + let layout = self.layout_of(res_ty); + let fields = match &layout.variants { + Variants::Single { index } => { + if *index != variant_index { + // This may occur if all variants except for the one pointed by + // index can never be constructed. Generic code might still try + // to initialize the non-existing invariant. + trace!(?res_ty, ?variant_index, "Unreachable invariant"); + return Expr::nondet(typ); + } + &layout.fields + } + Variants::Multiple { variants, .. } => &variants[variant_index].fields, + }; + + trace!(?variant_expr, ?fields, ?operands, "codegen_aggregate enum"); + let init_struct = Expr::struct_expr_from_values( + variant_expr.typ().clone(), + fields + .index_by_increasing_offset() + .map(|idx| self.codegen_operand(&operands[idx])) + .collect(), + &self.symbol_table, + ); + let assign_case = variant_proj.goto_expr.assign(init_struct, loc); + stmts.push(assign_case); + } + // 3- Set discriminant. + let set_discriminant = + self.codegen_set_discriminant(res_ty, temp_var.clone(), variant_index, loc); + stmts.push(set_discriminant); + // 4- Return temporary variable. + stmts.push(temp_var.as_stmt(loc)); + Expr::statement_expression(stmts, typ) + } + fn codegen_rvalue_aggregate( &mut self, - k: &AggregateKind<'tcx>, + aggregate: &AggregateKind<'tcx>, operands: &[Operand<'tcx>], res_ty: Ty<'tcx>, + loc: Location, ) -> Expr { - match *k { + match *aggregate { AggregateKind::Array(et) => { if et.is_unit() { Expr::struct_expr_from_values( @@ -304,7 +404,44 @@ impl<'tcx> GotocCtx<'tcx> { ) } } - AggregateKind::Tuple => { + AggregateKind::Adt(_, _, _, _, Some(active_field_index)) => { + assert!(res_ty.is_union()); + assert_eq!(operands.len(), 1); + let typ = self.codegen_ty(res_ty); + let components = typ.lookup_components(&self.symbol_table).unwrap(); + Expr::union_expr( + typ, + components[active_field_index].name(), + self.codegen_operand(&operands[0]), + &self.symbol_table, + ) + } + AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => { + let typ = self.codegen_ty(res_ty); + let layout = self.layout_of(res_ty); + let vector_element_type = typ.base_type().unwrap().clone(); + Expr::vector_expr( + typ, + layout + .fields + .index_by_increasing_offset() + .map(|idx| { + let cgo = self.codegen_operand(&operands[idx]); + // The input operand might actually be a one-element array, as seen + // when running assess on firecracker. + if *cgo.typ() == vector_element_type { + cgo + } else { + cgo.transmute_to(vector_element_type.clone(), &self.symbol_table) + } + }) + .collect(), + ) + } + AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => { + self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc) + } + AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => { let typ = self.codegen_ty(res_ty); let layout = self.layout_of(res_ty); Expr::struct_expr_from_values( @@ -317,9 +454,7 @@ impl<'tcx> GotocCtx<'tcx> { &self.symbol_table, ) } - AggregateKind::Adt(_, _, _, _, _) => unimplemented!(), - AggregateKind::Closure(_, _) => unimplemented!(), - AggregateKind::Generator(_, _, _) => unimplemented!(), + AggregateKind::Generator(_, _, _) => self.codegen_rvalue_generator(&operands, res_ty), } } @@ -406,7 +541,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_get_discriminant(place, pt, res_ty) } Rvalue::Aggregate(ref k, operands) => { - self.codegen_rvalue_aggregate(k, operands, res_ty) + self.codegen_rvalue_aggregate(k, operands, res_ty, loc) } Rvalue::ThreadLocalRef(def_id) => { // Since Kani is single-threaded, we treat a thread local like a static variable: diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 60e817f77670..4892ed988e39 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -16,6 +16,7 @@ use rustc_middle::ty; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{Instance, InstanceDef, Ty}; use rustc_span::Span; +use rustc_target::abi::VariantIdx; use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; use tracing::{debug, debug_span, trace}; @@ -55,68 +56,11 @@ impl<'tcx> GotocCtx<'tcx> { } StatementKind::Deinit(place) => self.codegen_deinit(place, location), StatementKind::SetDiscriminant { place, variant_index } => { - // this requires place points to an enum type. - let pt = self.place_ty(place); - let layout = self.layout_of(pt); - match &layout.variants { - Variants::Single { .. } => Stmt::skip(location), - Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { - TagEncoding::Direct => { - let discr = - pt.discriminant_for_variant(self.tcx, *variant_index).unwrap(); - let discr_t = self.codegen_enum_discr_typ(pt); - // The constant created below may not fit into the type. - // https://github.com/model-checking/kani/issues/996 - // - // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)` - // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant` - // because when it tries to codegen `std::cmp::Ordering` (which should produce - // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types: - // - // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty); - // DISCRIMINANT - val:255 ty:i8 - // DISCRIMINANT - val:0 ty:i8 - // DISCRIMINANT - val:1 ty:i8 - let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); - let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(place) - ) - .goto_expr; - self.codegen_discriminant_field(place_goto_expr, pt) - .assign(discr, location) - } - 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"), - }; - let discr_ty = self.codegen_enum_discr_typ(pt); - let discr_ty = self.codegen_ty(discr_ty); - let niche_value = - variant_index.as_u32() - niche_variants.start().as_u32(); - let niche_value = (niche_value as u128).wrapping_add(*niche_start); - let value = if niche_value == 0 - && matches!(tag.primitive(), Primitive::Pointer(_)) - { - discr_ty.null() - } else { - Expr::int_constant(niche_value, discr_ty.clone()) - }; - let place = unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(place) - ) - .goto_expr; - self.codegen_get_niche(place, offset, discr_ty) - .assign(value, location) - } else { - Stmt::skip(location) - } - } - }, - } + let dest_ty = self.place_ty(place); + let dest_expr = + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) + .goto_expr; + self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me @@ -259,6 +203,64 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Create a statement that sets the variable discriminant to the value that corresponds to the + /// variant index. + pub fn codegen_set_discriminant( + &mut self, + dest_ty: Ty<'tcx>, + dest_expr: Expr, + variant_index: VariantIdx, + location: Location, + ) -> Stmt { + // this requires place points to an enum type. + let layout = self.layout_of(dest_ty); + match &layout.variants { + Variants::Single { .. } => Stmt::skip(location), + Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { + TagEncoding::Direct => { + let discr = dest_ty.discriminant_for_variant(self.tcx, variant_index).unwrap(); + let discr_t = self.codegen_enum_discr_typ(dest_ty); + // The constant created below may not fit into the type. + // https://github.com/model-checking/kani/issues/996 + // + // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)` + // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant` + // because when it tries to codegen `std::cmp::Ordering` (which should produce + // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types: + // + // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty); + // DISCRIMINANT - val:255 ty:i8 + // DISCRIMINANT - val:0 ty:i8 + // DISCRIMINANT - val:1 ty:i8 + let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); + self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr, location) + } + 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"), + }; + let discr_ty = self.codegen_enum_discr_typ(dest_ty); + let discr_ty = self.codegen_ty(discr_ty); + let niche_value = variant_index.as_u32() - niche_variants.start().as_u32(); + let niche_value = (niche_value as u128).wrapping_add(*niche_start); + let value = if niche_value == 0 + && matches!(tag.primitive(), Primitive::Pointer(_)) + { + discr_ty.null() + } else { + Expr::int_constant(niche_value, discr_ty.clone()) + }; + self.codegen_get_niche(dest_expr, offset, discr_ty).assign(value, location) + } else { + Stmt::skip(location) + } + } + }, + } + } + /// From rustc doc: "This writes `uninit` bytes to the entire place." /// Our model of GotoC has a similar statement, which is later lowered /// to assigning a Nondet in CBMC, with a comment specifying that it diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 7844043def0b..4747ffef5d2d 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-02-04" +channel = "nightly-2023-02-05" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Enum/multiple_never.rs b/tests/kani/Enum/multiple_never.rs new file mode 100644 index 000000000000..4dc3f54d1b44 --- /dev/null +++ b/tests/kani/Enum/multiple_never.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test is to check how Kani handle enums where only one variant is valid. +#![feature(never_type)] + +enum MyResult { + Yes(Y), + No(N), + Maybe(M), +} + +fn change_maybe(orig: MyResult, val: O) -> MyResult { + match orig { + MyResult::Yes(y) => MyResult::Yes(y), + MyResult::No(n) => MyResult::No(n), + MyResult::Maybe(m) => MyResult::Maybe(val), + } +} + +fn check() -> Result { + let val = Result::::Ok(10)?; + Ok(val) +} + +fn checkErr() -> Result { + let val = Result::::Err(10)?; +} + +fn checkMaybe() -> MyResult { + change_maybe(MyResult::::Maybe(10), 0) +} + +#[kani::proof] +pub fn harness_residual() { + let _ = checkMaybe(); + let _ = checkErr(); + let _ = check(); +} diff --git a/tests/kani/Enum/one_two.rs b/tests/kani/Enum/one_two.rs new file mode 100644 index 000000000000..54b2dc8bbc0b --- /dev/null +++ b/tests/kani/Enum/one_two.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +enum Niche_Enum { + One(bool), + Two(bool, bool), +} + +enum Enum { + One(u32), + Two(u32, u32), +} + +#[kani::proof] +fn check() { + // This will have one operand. + let _var = Niche_Enum::One(false); + // This will have two operands -- true and false + let _var = Niche_Enum::Two(true, false); + // This will have one operand. + let _var = Enum::One(1); + // This will have two operands -- 2 and 3 + let _var = Enum::Two(2, 3); +}