From c5ec3062c5844a238fde1a21e8c9087f3b90c1c1 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Fri, 22 Jul 2022 15:29:05 -0500 Subject: [PATCH] Comment and Refactor a few files (#1398) --- .../codegen_cprover_gotoc/codegen/assert.rs | 55 ++- .../codegen_cprover_gotoc/codegen/block.rs | 8 +- .../codegen_cprover_gotoc/codegen/operand.rs | 2 +- .../codegen/statement.rs | 461 +++++++++--------- .../codegen/static_var.rs | 3 + .../src/codegen_cprover_gotoc/codegen/typ.rs | 13 +- 6 files changed, 301 insertions(+), 241 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 3f97e688944c1..c86c4a50b0303 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -1,9 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This file contains the code that acts as a wrapper to create the new assert and related statements +//! This module is the central location for handling assertions and assumptions in Kani. + +use crate::codegen_cprover_gotoc::utils; use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{Expr, Location, Stmt}; +use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt}; +use rustc_span::Span; use std::convert::AsRef; use strum_macros::{AsRefStr, EnumString}; @@ -39,6 +42,7 @@ impl PropertyClass { } impl<'tcx> GotocCtx<'tcx> { + /// Generates a CBMC assertion. Note: Does _NOT_ assume. pub fn codegen_assert( &self, cond: Expr, @@ -51,6 +55,7 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::assert(cond, property_name, message, loc) } + /// Generates a CBMC assertion, followed by an assumption of the same condition. pub fn codegen_assert_assume( &self, cond: Expr, @@ -66,6 +71,7 @@ impl<'tcx> GotocCtx<'tcx> { ) } + /// A shorthand for generating a CBMC assert-false. TODO: This should probably be eliminated! pub fn codegen_assert_false( &self, property_class: PropertyClass, @@ -76,4 +82,49 @@ impl<'tcx> GotocCtx<'tcx> { let property_name = property_class.as_str(); Stmt::assert_false(property_name, message, loc) } + + /// Kani hooks function calls to `panic` and calls this intead. + pub fn codegen_panic(&self, span: Option, fargs: Vec) -> Stmt { + // CBMC requires that the argument to the assertion must be a string constant. + // If there is one in the MIR, use it; otherwise, explain that we can't. + assert!(!fargs.is_empty(), "Panic requires a string message"); + let msg = utils::extract_const_message(&fargs[0]).unwrap_or(String::from( + "This is a placeholder message; Kani doesn't support message formatted at runtime", + )); + + self.codegen_fatal_error(PropertyClass::Assertion, &msg, span) + } + + /// Generate code for fatal error which should trigger an assertion failure and abort the + /// execution. + pub fn codegen_fatal_error( + &self, + property_class: PropertyClass, + msg: &str, + span: Option, + ) -> Stmt { + let loc = self.codegen_caller_span(&span); + Stmt::block( + vec![ + self.codegen_assert_false(property_class, msg, loc), + BuiltinFn::Abort.call(vec![], loc).as_stmt(loc), + ], + loc, + ) + } + + /// Generate code to cover the given condition at the current location + pub fn codegen_cover(&self, cond: Expr, msg: &str, span: Option) -> Stmt { + let loc = self.codegen_caller_span(&span); + // Should use Stmt::cover, but currently this doesn't work with CBMC + // unless it is run with '--cover cover' (see + // https://github.com/diffblue/cbmc/issues/6613). So for now use + // assert(!cond). + self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc) + } + + /// Generate code to cover the current location + pub fn codegen_cover_loc(&self, msg: &str, span: Option) -> Stmt { + self.codegen_cover(Expr::bool_true(), msg, span) + } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index f6bdd2725df4f..9298c8851eea2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -1,12 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This file contains functions related to codegenning MIR blocks into gotoc - use crate::codegen_cprover_gotoc::GotocCtx; use rustc_middle::mir::{BasicBlock, BasicBlockData}; impl<'tcx> GotocCtx<'tcx> { + /// Generates Goto-C for a basic block. + /// + /// A MIR basic block consists of 0 or more statements followed by a terminator. + /// + /// This function does not return a value, but mutates state with + /// `self.current_fn_mut().push_onto_block(...)` pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) { self.current_fn_mut().set_current_bb(bb); let label: String = self.current_fn().find_label(&bb); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 4f8e8a11c8b4f..db299e97f5494 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -26,7 +26,7 @@ impl<'tcx> GotocCtx<'tcx> { trace!(operand=?o, "codegen_operand"); match o { Operand::Copy(d) | Operand::Move(d) => - // TODO: move shouldn't be the same as copy + // TODO: move is an opportunity to poison/nondet the original memory. { let projection = unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(d)); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index d68f9481b31e0..f13eb0243a432 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -4,10 +4,9 @@ use super::typ::TypeExt; use super::typ::FN_RETURN_VOID_VAR_NAME; use super::PropertyClass; use crate::codegen_cprover_gotoc::codegen::typ::pointee_type; -use crate::codegen_cprover_gotoc::utils; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; -use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; +use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::utils::BUG_REPORT_URL; use kani_queries::UserInput; use rustc_hir::def_id::DefId; @@ -24,19 +23,166 @@ use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; use tracing::{debug, info_span, trace, warn}; impl<'tcx> GotocCtx<'tcx> { - fn codegen_ret_unit(&mut self) -> Stmt { - let is_file_local = false; - let ty = self.codegen_ty_unit(); - let var = self.ensure_global_var( - FN_RETURN_VOID_VAR_NAME, - is_file_local, - ty, - Location::none(), - |_, _| None, - ); - Stmt::ret(Some(var), Location::none()) + /// Generate Goto-C for MIR [Statement]s. + /// This does not cover all possible "statements" because MIR distinguishes between ordinary + /// statements and [Terminator]s, which can exclusively appear at the end of a basic block. + /// + /// See [GotocCtx::codegen_terminator] for those. + pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { + let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered(); + debug!(?stmt, kind=?stmt.kind, "handling_statement"); + let location = self.codegen_span(&stmt.source_info.span); + match &stmt.kind { + StatementKind::Assign(box (l, r)) => { + let lty = self.place_ty(l); + let rty = self.rvalue_ty(r); + let llayout = self.layout_of(lty); + // we ignore assignment for all zero size types + if llayout.is_zst() { + Stmt::skip(Location::none()) + } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { + // implicit address of a function pointer, e.g. + // let fp: fn() -> i32 = foo; + // where the reference is implicit. + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) + .goto_expr + .assign(self.codegen_rvalue(r, location).address_of(), location) + } else if rty.is_bool() { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) + .goto_expr + .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location) + } else { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) + .goto_expr + .assign(self.codegen_rvalue(r, location), location) + } + } + StatementKind::Deinit(place) => { + // From rustc doc: "This writes `uninit` bytes to the entire place." + // Thus, we assign nondet() value to the entire place. + let dst_mir_ty = self.place_ty(place); + let dst_type = self.codegen_ty(dst_mir_ty); + let layout = self.layout_of(dst_mir_ty); + if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 { + // We ignore assignment for all zero size types + // Ignore generators too for now: + // https://github.com/model-checking/kani/issues/416 + Stmt::skip(location) + } else { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) + .goto_expr + .assign(dst_type.nondet(), location) + } + } + StatementKind::SetDiscriminant { place, variant_index } => { + // this requires place points to an enum type. + let pt = self.place_ty(place); + let (def, _) = match pt.kind() { + ty::Adt(def, substs) => (def, substs), + ty::Generator(..) => { + return self + .codegen_unimplemented( + "ty::Generator", + Type::code(vec![], Type::empty()), + location, + "https://github.com/model-checking/kani/issues/416", + ) + .as_stmt(location); + } + _ => unreachable!(), + }; + 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 = def.discriminant_for_variant(self.tcx, *variant_index); + 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)); + unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place(place) + ) + .goto_expr + .member("case", &self.symbol_table) + .assign(discr, location) + } + TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { + if dataful_variant != variant_index { + let offset = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => { + offsets[0].bytes_usize() + } + _ => 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 && 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) + } + } + }, + } + } + 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, + }) => { + // Pack the operands and their types, then call `codegen_copy` + let fargs = vec![ + self.codegen_operand(src), + self.codegen_operand(dst), + self.codegen_operand(count), + ]; + let farg_types = + &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)]; + self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location) + } + StatementKind::FakeRead(_) + | StatementKind::Retag(_, _) + | StatementKind::AscribeUserType(_, _) + | StatementKind::Nop + | StatementKind::Coverage { .. } => Stmt::skip(location), + } + .with_location(self.codegen_span(&stmt.source_info.span)) } + /// Generate Goto-c for MIR [Terminator] statements. + /// Many kinds of seemingly ordinary statements in Rust are "terminators" (i.e. the sort of statement that _ends_ a basic block) + /// because of the need for unwinding/drop. For instance, function calls. + /// + /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s. pub fn codegen_terminator(&mut self, term: &Terminator<'tcx>) -> Stmt { let loc = self.codegen_span(&term.source_info.span); let _trace_span = info_span!("CodegenTerminator", statement = ?term.kind).entered(); @@ -83,9 +229,6 @@ impl<'tcx> GotocCtx<'tcx> { loc, ), TerminatorKind::Drop { place, target, unwind: _ } => self.codegen_drop(place, target), - TerminatorKind::DropAndReplace { .. } => { - unreachable!("this instruction is unreachable") - } TerminatorKind::Call { func, args, destination, target, .. } => { self.codegen_funcall(func, args, destination, target, term.source_info.span) } @@ -130,10 +273,14 @@ impl<'tcx> GotocCtx<'tcx> { loc, ) } - TerminatorKind::Yield { .. } - | TerminatorKind::GeneratorDrop + TerminatorKind::DropAndReplace { .. } | TerminatorKind::FalseEdge { .. } - | TerminatorKind::FalseUnwind { .. } => unreachable!("we should not hit these cases"), + | TerminatorKind::FalseUnwind { .. } => { + unreachable!("drop elaboration removes these TerminatorKind") + } + TerminatorKind::Yield { .. } | TerminatorKind::GeneratorDrop => { + unreachable!("we should not hit these cases") // why? + } TerminatorKind::InlineAsm { .. } => self .codegen_unimplemented( "InlineAsm", @@ -145,25 +292,43 @@ impl<'tcx> GotocCtx<'tcx> { } } - // TODO: this function doesn't handle unwinding which begins if the destructor panics - // https://github.com/model-checking/kani/issues/221 - fn codegen_drop(&mut self, location: &Place<'tcx>, target: &BasicBlock) -> Stmt { - let loc_ty = self.place_ty(location); - debug!(?loc_ty, "codegen_drop"); - let drop_instance = Instance::resolve_drop_in_place(self.tcx, loc_ty); + /// A special case handler to codegen `return ();` + fn codegen_ret_unit(&mut self) -> Stmt { + let is_file_local = false; + let ty = self.codegen_ty_unit(); + let var = self.ensure_global_var( + FN_RETURN_VOID_VAR_NAME, + is_file_local, + ty, + Location::none(), + |_, _| None, + ); + Stmt::ret(Some(var), Location::none()) + } + + /// Generates Goto-C for MIR [TerminatorKind::Drop] calls. We only handle code _after_ Rust's "drop elaboration" + /// transformation, so these have a simpler semantics. + /// + /// The generated code should invoke the appropriate `drop` function on `place`, then goto `target`. + fn codegen_drop(&mut self, place: &Place<'tcx>, target: &BasicBlock) -> Stmt { + // TODO: this function doesn't handle unwinding which begins if the destructor panics + // https://github.com/model-checking/kani/issues/221 + let place_ty = self.place_ty(place); + debug!(?place_ty, "codegen_drop"); + let drop_instance = Instance::resolve_drop_in_place(self.tcx, place_ty); // Once upon a time we did a `hook_applies` check here, but we no longer seem to hook drops let drop_implementation = match drop_instance.def { InstanceDef::DropGlue(_, None) => { // We can skip empty DropGlue functions Stmt::skip(Location::none()) } - _ => { - match loc_ty.kind() { + InstanceDef::DropGlue(_def_id, Some(_)) => { + match place_ty.kind() { ty::Dynamic(..) => { // Virtual drop via a vtable lookup let trait_fat_ptr = unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place(location) + self.codegen_place(place) ) .fat_ptr_goto_expr .unwrap(); @@ -177,7 +342,7 @@ impl<'tcx> GotocCtx<'tcx> { let fn_ptr = vtable.member("drop", &self.symbol_table); // Pull the self argument off of the fat pointer's data pointer - if let Some(typ) = pointee_type(self.local_ty(location.local)) { + if let Some(typ) = pointee_type(self.local_ty(place.local)) { if !(typ.is_trait() || typ.is_box()) { warn!(self_type=?typ, "Unsupported drop of unsized"); return self @@ -213,7 +378,7 @@ impl<'tcx> GotocCtx<'tcx> { let func = self.codegen_func_expr(drop_instance, None); let place = unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place(location) + self.codegen_place(place) ); let arg = if let Some(fat_ptr) = place.fat_ptr_goto_expr { // Drop takes the fat pointer if it exists @@ -245,15 +410,18 @@ impl<'tcx> GotocCtx<'tcx> { } } } + _ => unreachable!( + "TerminatorKind::Drop but not InstanceDef::DropGlue should be impossible" + ), }; let goto_target = Stmt::goto(self.current_fn().find_label(target), Location::none()); let block = vec![drop_implementation, goto_target]; Stmt::block(block, Location::none()) } - /// + /// Generates Goto-C for MIR [TerminatorKind::SwitchInt]. /// Operand evaluates to an integer; - /// jump depending on its value to one of the targets, and otherwise fallback to otherwise. + /// jump depending on its value to one of the targets, and otherwise fallback to `targets.otherwise()`. /// The otherwise value is stores as the last value of targets. fn codegen_switch_int( &mut self, @@ -302,6 +470,9 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// As part of **calling** a function (closure actually), we may need to un-tuple arguments. + /// + /// See [GotocCtx::ty_needs_closure_untupled] fn codegen_untuple_closure_args( &mut self, instance: Instance<'tcx>, @@ -343,6 +514,8 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Because function calls terminate basic blocks, to "end" a function call, we + /// must jump to the next basic block. fn codegen_end_call(&self, target: Option<&BasicBlock>, loc: Location) -> Stmt { if let Some(next_bb) = target { Stmt::goto(self.current_fn().find_label(next_bb), loc) @@ -356,7 +529,10 @@ impl<'tcx> GotocCtx<'tcx> { } } - pub fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec { + /// Generate Goto-C for each argument to a function call. + /// + /// N.B. public only because instrinsics use this directly, too. + pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec { args.iter() .filter_map(|o| { let ot = self.operand_ty(o); @@ -372,6 +548,18 @@ impl<'tcx> GotocCtx<'tcx> { .collect() } + /// Generates Goto-C for a MIR [TerminatorKind::Call] statement. + /// + /// This calls either: + /// + /// 1. A statically-known function definition. + /// 2. A statically-known trait function, which gets a pointer out of a vtable. + /// 2. A direct function pointer. + /// + /// Kani also performs a few alterations: + /// + /// 1. Do nothing for "empty drop glue" + /// 2. If a Kani hook applies, do that instead. fn codegen_funcall( &mut self, func: &Operand<'tcx>, @@ -462,8 +650,8 @@ impl<'tcx> GotocCtx<'tcx> { } /// Extract a reference to self for virtual method calls. - /// See [codegen_dynamic_function_sig](GotocCtx::codegen_dynamic_function_sig) for more - /// details. + /// + /// See [GotocCtx::codegen_dynamic_function_sig] for more details. fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty<'tcx>) -> Expr { // Generate an expression that indexes the pointer. let expr = self @@ -560,10 +748,11 @@ impl<'tcx> GotocCtx<'tcx> { ret_stmts } - /// A place is similar to the C idea of a LHS. For example, the returned value of a function call is stored to a place. - /// If the place is unit (i.e. the statement value is not stored anywhere), then we can just turn it directly to a statement. - /// Otherwise, we assign the value of the expression to the place. - pub fn codegen_expr_to_place(&mut self, p: &Place<'tcx>, e: Expr) -> Stmt { + /// Generates Goto-C to assign a value to a [Place]. + /// A MIR [Place] is an L-value (i.e. the LHS of an assignment). + /// + /// In Kani, we slightly optimize the special case for Unit and don't assign anything. + pub(crate) fn codegen_expr_to_place(&mut self, p: &Place<'tcx>, e: Expr) -> Stmt { if self.place_ty(p).is_unit() { e.as_stmt(Location::none()) } else { @@ -572,198 +761,4 @@ impl<'tcx> GotocCtx<'tcx> { .assign(e, Location::none()) } } - - pub fn codegen_panic(&self, span: Option, fargs: Vec) -> Stmt { - // CBMC requires that the argument to the assertion must be a string constant. - // If there is one in the MIR, use it; otherwise, explain that we can't. - assert!(!fargs.is_empty(), "Panic requires a string message"); - let msg = utils::extract_const_message(&fargs[0]).unwrap_or(String::from( - "This is a placeholder message; Kani doesn't support message formatted at runtime", - )); - - self.codegen_fatal_error(PropertyClass::Assertion, &msg, span) - } - - // Generate code for fatal error which should trigger an assertion failure and abort the - // execution. - pub fn codegen_fatal_error( - &self, - property_class: PropertyClass, - msg: &str, - span: Option, - ) -> Stmt { - let loc = self.codegen_caller_span(&span); - Stmt::block( - vec![ - self.codegen_assert_false(property_class, msg, loc), - BuiltinFn::Abort.call(vec![], loc).as_stmt(loc), - ], - loc, - ) - } - - /// Generate code to cover the given condition at the current location - pub fn codegen_cover(&self, cond: Expr, msg: &str, span: Option) -> Stmt { - let loc = self.codegen_caller_span(&span); - // Should use Stmt::cover, but currently this doesn't work with CBMC - // unless it is run with '--cover cover' (see - // https://github.com/diffblue/cbmc/issues/6613). So for now use - // assert(!cond). - self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc) - } - - /// Generate code to cover the current location - pub fn codegen_cover_loc(&self, msg: &str, span: Option) -> Stmt { - self.codegen_cover(Expr::bool_true(), msg, span) - } - - pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { - let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered(); - debug!(?stmt, kind=?stmt.kind, "handling_statement"); - let location = self.codegen_span(&stmt.source_info.span); - match &stmt.kind { - StatementKind::Assign(box (l, r)) => { - let lty = self.place_ty(l); - let rty = self.rvalue_ty(r); - let llayout = self.layout_of(lty); - // we ignore assignment for all zero size types - if llayout.is_zst() { - Stmt::skip(Location::none()) - } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { - // implicit address of a function pointer, e.g. - // let fp: fn() -> i32 = foo; - // where the reference is implicit. - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location).address_of(), location) - } else if rty.is_bool() { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location) - } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location), location) - } - } - StatementKind::Deinit(place) => { - // From rustc doc: "This writes `uninit` bytes to the entire place." - // Thus, we assign nondet() value to the entire place. - let dst_mir_ty = self.place_ty(place); - let dst_type = self.codegen_ty(dst_mir_ty); - let layout = self.layout_of(dst_mir_ty); - if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 { - // We ignore assignment for all zero size types - // Ignore generators too for now: - // https://github.com/model-checking/kani/issues/416 - Stmt::skip(location) - } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) - .goto_expr - .assign(dst_type.nondet(), location) - } - } - StatementKind::SetDiscriminant { place, variant_index } => { - // this requires place points to an enum type. - let pt = self.place_ty(place); - let (def, _) = match pt.kind() { - ty::Adt(def, substs) => (def, substs), - ty::Generator(..) => { - return self - .codegen_unimplemented( - "ty::Generator", - Type::code(vec![], Type::empty()), - location, - "https://github.com/model-checking/kani/issues/416", - ) - .as_stmt(location); - } - _ => unreachable!(), - }; - 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 = def.discriminant_for_variant(self.tcx, *variant_index); - 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)); - unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(place) - ) - .goto_expr - .member("case", &self.symbol_table) - .assign(discr, location) - } - TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { - if dataful_variant != variant_index { - let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => { - offsets[0].bytes_usize() - } - _ => 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 && 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) - } - } - }, - } - } - 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, - }) => { - // Pack the operands and their types, then call `codegen_copy` - let fargs = vec![ - self.codegen_operand(src), - self.codegen_operand(dst), - self.codegen_operand(count), - ]; - let farg_types = - &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)]; - self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location) - } - StatementKind::FakeRead(_) - | StatementKind::Retag(_, _) - | StatementKind::AscribeUserType(_, _) - | StatementKind::Nop - | StatementKind::Coverage { .. } => Stmt::skip(location), - } - .with_location(self.codegen_span(&stmt.source_info.span)) - } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index a1e414119e1cb..dfea9d31858d3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -11,13 +11,16 @@ use rustc_middle::ty::{subst::InternalSubsts, Instance}; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { + /// Ensures a static variable is initialized. pub fn codegen_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) { debug!("codegen_static"); let alloc = self.tcx.eval_static_initializer(def_id).unwrap(); let symbol_name = item.symbol_name(self.tcx).to_string(); + // This is an `Expr` constructing function, but it mutates the symbol table to ensure initialization. self.codegen_allocation(alloc.inner(), |_| symbol_name.clone(), Some(symbol_name.clone())); } + /// Mutates the Goto-C symbol table to add a forward-declaration of the static variable. pub fn declare_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) { // Unique mangled monomorphized name. let symbol_name = item.symbol_name(self.tcx).to_string(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 768d2958fc739..2641a90df6c36 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -770,6 +770,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// A closure in Rust MIR takes two arguments: + /// /// 0. a struct representing the environment /// 1. a tuple containing the parameters /// @@ -779,16 +780,22 @@ impl<'tcx> GotocCtx<'tcx> { /// Checking whether the type's kind is a closure is insufficient, because /// a virtual method call through a vtable can have the trait's non-closure /// type. For example: + /// + /// ``` /// let p: &dyn Fn(i32) = &|x| assert!(x == 1); /// p(1); + /// ``` /// - /// Here, the call p(1) desugars to an MIR trait call Fn::call(&p, (1,)), + /// Here, the call `p(1)` desugars to an MIR trait call `Fn::call(&p, (1,))`, /// where the second argument is a tuple. The instance type kind for - /// Fn::call is not a closure, because dynamically, the pointer may be to + /// `Fn::call` is not a closure, because dynamically, the pointer may be to /// a function definition instead. We still need to untuple in this case, /// so we follow the example elsewhere in Rust to use the ABI call type. - /// See `make_call_args` in kani/compiler/rustc_mir/src/transform/inline.rs + /// + /// See `make_call_args` in `rustc_mir_transform/src/inline.rs` pub fn ty_needs_closure_untupled(&self, ty: Ty<'tcx>) -> bool { + // Note that [Abi::RustCall] is not [Abi::Rust]. + // Documentation is sparse, but it does seem to correspond to the need for untupling. match ty.kind() { ty::FnDef(..) | ty::FnPtr(..) => ty.fn_sig(self.tcx).abi() == Abi::RustCall, _ => unreachable!("Can't treat type as a function: {:?}", ty),