diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 7fc82bc50642..be8d91874a5d 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs @@ -453,7 +453,6 @@ impl<'tcx> GotocCtx<'tcx> { "prefetch_read_instruction" => unimplemented!(), "prefetch_write_data" => unimplemented!(), "prefetch_write_instruction" => unimplemented!(), - "try" => unimplemented!(), "unaligned_volatile_store" => unimplemented!(), "va_arg" => unimplemented!(), "va_copy" => unimplemented!(), diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs index 00e0608b6fd0..ea395ca0e395 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs @@ -105,14 +105,8 @@ impl<'tcx> GotocCtx<'tcx> { x if x.ends_with("__getit") => true, // https://github.com/model-checking/rmc/issues/205 "panic::Location::<'a>::caller" => true, - // https://github.com/model-checking/rmc/issues/206 - "core::sync::atomic::atomic_swap" => true, // https://github.com/model-checking/rmc/issues/207 "core::slice::::split_first" => true, - // https://github.com/model-checking/rmc/issues/208 - "panicking::take_hook" => true, - // https://github.com/model-checking/rmc/issues/209 - "panicking::r#try" => true, _ => false, } } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs index 17143dbaf9dc..c79cae548b3d 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs @@ -28,7 +28,16 @@ impl<'tcx> GotocCtx<'tcx> { Operand::Copy(d) | Operand::Move(d) => // TODO: move shouldn't be the same as copy { - self.codegen_place(d).goto_expr + let projection = self.codegen_place(d); + // If the operand itself is a Dynamic (like when passing a boxed closure), + // we need to pull off the fat pointer. In that case, the rustc kind() on + // both the operand and the inner type are Dynamic. + // Consider moving this check elsewhere in: + // https://github.com/model-checking/rmc/issues/277 + match self.operand_ty(o).kind() { + ty::Dynamic(..) => projection.fat_ptr_goto_expr.unwrap(), + _ => projection.goto_expr, + } } Operand::Constant(c) => self.codegen_constant(&c), } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/place.rs b/compiler/rustc_codegen_llvm/src/gotoc/place.rs index 5a2c028e53c1..af31c24b9c7f 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/place.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/place.rs @@ -13,7 +13,7 @@ use rustc_middle::{ ty::{self, Ty, TyS, VariantDef}, }; use rustc_target::abi::{LayoutOf, TagEncoding, Variants}; -use tracing::debug; +use tracing::{debug, warn}; /// A projection in RMC can either be to a type (the normal case), /// or a variant in the case of a downcast. @@ -63,7 +63,7 @@ impl<'tcx> ProjectedPlace<'tcx> { /// Constructor impl<'tcx> ProjectedPlace<'tcx> { - fn _check_expr_typ(expr: &Expr, typ: &TypeOrVariant<'tcx>, ctx: &mut GotocCtx<'tcx>) -> bool { + fn check_expr_typ(expr: &Expr, typ: &TypeOrVariant<'tcx>, ctx: &mut GotocCtx<'tcx>) -> bool { match typ { TypeOrVariant::Type(t) => &ctx.codegen_ty(t) == expr.typ(), TypeOrVariant::Variant(_) => true, //TODO, what to do here? @@ -102,12 +102,14 @@ impl<'tcx> ProjectedPlace<'tcx> { } // TODO: these assertions fail on a few regressions. Figure out why. // I think it may have to do with boxed fat pointers. - // assert!( - // Self::check_expr_typ(&goto_expr, &mir_typ_or_variant, ctx), - // "\n{:?}\n{:?}", - // &goto_expr, - // &mir_typ_or_variant - // ); + // https://github.com/model-checking/rmc/issues/277 + if !Self::check_expr_typ(&goto_expr, &mir_typ_or_variant, ctx) { + warn!( + "Unexpected type mismatch in projection: \n{:?}\n{:?}", + &goto_expr, &mir_typ_or_variant + ); + }; + assert!( Self::check_fat_ptr_typ(&fat_ptr_goto_expr, &fat_ptr_mir_typ, ctx), "\n{:?}\n{:?}", @@ -252,6 +254,14 @@ impl<'tcx> GotocCtx<'tcx> { before.fat_ptr_goto_expr }; + // Check that we have a valid trait or slice fat pointer + if let Some(fat_ptr) = fat_ptr_goto_expr.clone() { + assert!( + fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table) + || fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table) + ); + }; + let inner_mir_typ = inner_mir_typ_and_mut.ty; let expr = match inner_mir_typ.kind() { ty::Slice(_) | ty::Str | ty::Dynamic(..) => { diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index ea27f951f67a..82347dbaa34f 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -3,6 +3,7 @@ use super::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; use super::metadata::*; use super::typ::FN_RETURN_VOID_VAR_NAME; +use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, @@ -276,79 +277,101 @@ impl<'tcx> GotocCtx<'tcx> { let (p, target) = destination.unwrap(); - if let ty::InstanceDef::DropGlue(_, None) = instance.def { - // here an empty drop glue is invoked. we just ignore it. - return Stmt::goto(self.current_fn().find_label(&target), Location::none()); - } - - // Handle the case of a virtual function call via vtable lookup. - let mut stmts = if let InstanceDef::Virtual(def_id, size) = instance.def { - debug!( - "Codegen a call through a virtual function. def_id: {:?} size: {:?}", - def_id, size - ); - - // The first argument to a virtual function is a fat pointer for the trait - let trait_fat_ptr = fargs[0].to_owned(); - let vtable_field_name = self.vtable_field_name(def_id); - - // Now that we have all the stuff we need, we can actually build the dynamic call - // If the original call was of the form - // f(arg0, arg1); - // The new call should be of the form - // arg0.vtable->f(arg0.data,arg1); - let vtable_ref = trait_fat_ptr.to_owned().member("vtable", &self.symbol_table); - let vtable = vtable_ref.dereference(); - let fn_ptr = vtable.member(&vtable_field_name, &self.symbol_table); - - // Update the argument from arg0 to arg0.data - fargs[0] = trait_fat_ptr.to_owned().member("data", &self.symbol_table); + let mut stmts: Vec = match instance.def { + // Here an empty drop glue is invoked; we just ignore it. + InstanceDef::DropGlue(_, None) => { + return Stmt::goto(self.current_fn().find_label(&target), Location::none()); + } + // Handle a virtual function call via a vtable lookup + InstanceDef::Virtual(def_id, _) => { + // We must have at least one argument, and the first one + // should be a fat pointer for the trait + let trait_fat_ptr = fargs[0].to_owned(); - // For soundness, add an assertion that the vtable function call is not null. - // Otherwise, CBMC might treat this as an assert(0) and later user-added assertions - // could be vacuously true. - let call_is_nonnull = fn_ptr.clone().is_nonnull(); - let assert_msg = - format!("Non-null virtual function call for {:?}", vtable_field_name); - let assert_nonnull = Stmt::assert(call_is_nonnull, &assert_msg, loc.clone()); + //Check the Gotoc-level fat pointer type + assert!(trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)); - // Virtual function call and corresponding nonnull assertion. - let func_exp: Expr = fn_ptr.dereference(); - vec![ - assert_nonnull, - self.codegen_expr_to_place(&p, func_exp.call(fargs)) - .with_location(loc.clone()), - ] - } else { - // Non-virtual function call. - let func_exp = self.codegen_operand(func); - vec![ - self.codegen_expr_to_place(&p, func_exp.call(fargs)) - .with_location(loc.clone()), - ] + self.codegen_virtual_funcall( + trait_fat_ptr, + def_id, + &p, + &mut fargs, + loc.clone(), + ) + } + // Normal, non-virtual function calls + InstanceDef::Item(..) + | InstanceDef::DropGlue(_, Some(_)) + | InstanceDef::Intrinsic(..) + | InstanceDef::FnPtrShim(.., _) + | InstanceDef::VtableShim(..) + | InstanceDef::ReifyShim(..) + | InstanceDef::ClosureOnceShim { call_once: _ } + | InstanceDef::CloneShim(..) => { + let func_exp = self.codegen_operand(func); + vec![ + self.codegen_expr_to_place(&p, func_exp.call(fargs)) + .with_location(loc.clone()), + ] + } }; - - // Add return jump. stmts.push(Stmt::goto(self.current_fn().find_label(&target), loc.clone())); - - // Produce the full function call block. - Stmt::block(stmts, loc) + return Stmt::block(stmts, loc); } + // Function call through a pointer ty::FnPtr(_) => { let (p, target) = destination.unwrap(); let func_expr = self.codegen_operand(func).dereference(); - // Actually generate the function call, and store the return value, if any. - Stmt::block( + // Actually generate the function call and return. + return Stmt::block( vec![ self.codegen_expr_to_place(&p, func_expr.call(fargs)) .with_location(loc.clone()), Stmt::goto(self.current_fn().find_label(&target), loc.clone()), ], loc, - ) + ); } x => unreachable!("Function call where the function was of unexpected type: {:?}", x), - } + }; + } + + fn codegen_virtual_funcall( + &mut self, + trait_fat_ptr: Expr, + def_id: DefId, + place: &Place<'tcx>, + fargs: &mut Vec, + loc: Location, + ) -> Vec { + let vtable_field_name = self.vtable_field_name(def_id); + + // Now that we have all the stuff we need, we can actually build the dynamic call + // If the original call was of the form + // f(arg0, arg1); + // The new call should be of the form + // arg0.vtable->f(arg0.data,arg1); + let vtable_ref = trait_fat_ptr.to_owned().member("vtable", &self.symbol_table); + let vtable = vtable_ref.dereference(); + let fn_ptr = vtable.member(&vtable_field_name, &self.symbol_table); + + // Update the argument from arg0 to arg0.data + fargs[0] = trait_fat_ptr.to_owned().member("data", &self.symbol_table); + + // For soundness, add an assertion that the vtable function call is not null. + // Otherwise, CBMC might treat this as an assert(0) and later user-added assertions + // could be vacuously true. + let call_is_nonnull = fn_ptr.clone().is_nonnull(); + let assert_msg = format!("Non-null virtual function call for {:?}", vtable_field_name); + let assert_nonnull = Stmt::assert(call_is_nonnull, &assert_msg, loc.clone()); + + // Virtual function call and corresponding nonnull assertion. + let func_exp: Expr = fn_ptr.dereference(); + vec![ + assert_nonnull, + self.codegen_expr_to_place(place, func_exp.call(fargs.to_vec())) + .with_location(loc.clone()), + ] } /// 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. diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index 9cb59caa9824..0b78a51320dc 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs @@ -970,12 +970,11 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// whether a variable of type ty should be ignored + /// Whether a variable of type ty should be ignored as a parameter to a function pub fn ignore_var_ty(&self, ty: Ty<'tcx>) -> bool { match ty.kind() { ty::Tuple(substs) if substs.is_empty() => true, ty::FnDef(_, _) => true, - ty::Dynamic(_, _) => true, //DSN understand why _ => false, } } diff --git a/src/test/cbmc/DynTrait/boxed_closure.rs b/src/test/cbmc/DynTrait/boxed_closure.rs new file mode 100644 index 000000000000..6f2e6042fbfd --- /dev/null +++ b/src/test/cbmc/DynTrait/boxed_closure.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can codegen a boxed dyn closure + +fn main() { + // Create a boxed once-callable closure + let f: Box = Box::new(|x| assert!(x == 1)); + + // Call it + f(1); +} diff --git a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs new file mode 100644 index 000000000000..f638d11568db --- /dev/null +++ b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs @@ -0,0 +1,18 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can codegen a boxed dyn closure and fail an inner assertion + +// This current verifies "successfully" because the closure is not actually +// called in the resulting CotoC code. +// https://github.com/model-checking/rmc/issues/240 + +fn main() { + // Create a boxed once-callable closure + let f: Box = Box::new(|x| { + __VERIFIER_expect_fail(x == 2, "Wrong int"); + }); + + // Call it + f(1); +} diff --git a/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs b/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs index ddfaf9358df1..bc235663a756 100644 --- a/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs +++ b/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs @@ -13,7 +13,7 @@ fn takes_dyn_fun(fun: &dyn Fn() -> i32) { let x = fun(); __VERIFIER_expect_fail(x != 5, "Wrong return"); /* The closure captures `a` and thus is sized */ - __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) == 8, "Wrong size"); + __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 8, "Wrong size"); } fn main() {