From 7a46da336fc791bc2aca8fa1f92cf805e1890d39 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 30 Jun 2021 10:04:35 -0400 Subject: [PATCH 1/5] Support boxed closures --- .../rustc_codegen_llvm/src/gotoc/operand.rs | 6 +- .../rustc_codegen_llvm/src/gotoc/place.rs | 23 ++- .../rustc_codegen_llvm/src/gotoc/statement.rs | 141 +++++++++++------- compiler/rustc_codegen_llvm/src/gotoc/typ.rs | 3 +- src/test/cbmc/DynTrait/boxed_closure.rs | 8 + 5 files changed, 113 insertions(+), 68 deletions(-) create mode 100644 src/test/cbmc/DynTrait/boxed_closure.rs diff --git a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs index 17143dbaf9dc..947ae66dd698 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs @@ -28,7 +28,11 @@ 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); + 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..5b5cc5011bbe 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. @@ -102,12 +102,13 @@ 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 - // ); + 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 +253,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..e5038ace2353 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -2,7 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use super::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; use super::metadata::*; -use super::typ::FN_RETURN_VOID_VAR_NAME; +use super::typ::{is_dyn_trait_fat_pointer, 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,103 @@ 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, size) => { + // We must have at least one argument, and the first one + // should be a fat pointer for the trait + let mut 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, + &target, + &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>, + target: &BasicBlock, + 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 8d4805f264cf..f64b8562d9b9 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..1c6b31042c87 --- /dev/null +++ b/src/test/cbmc/DynTrait/boxed_closure.rs @@ -0,0 +1,8 @@ +fn main() { + // Create a boxed once-callable closure + let f: Box = Box::new(|| { + }); + + // Call it + f(); +} \ No newline at end of file From ff2a43a1a2ca93a21867ddc69fb79d47338745fe Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 30 Jun 2021 10:16:58 -0400 Subject: [PATCH 2/5] More comments --- compiler/rustc_codegen_llvm/src/gotoc/operand.rs | 3 +++ compiler/rustc_codegen_llvm/src/gotoc/place.rs | 1 + 2 files changed, 4 insertions(+) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs index 947ae66dd698..bc7f024d3600 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs @@ -29,6 +29,9 @@ impl<'tcx> GotocCtx<'tcx> { // TODO: move shouldn't be the same as copy { 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. match self.operand_ty(o).kind() { ty::Dynamic(..) => projection.fat_ptr_goto_expr.unwrap(), _ => projection.goto_expr, diff --git a/compiler/rustc_codegen_llvm/src/gotoc/place.rs b/compiler/rustc_codegen_llvm/src/gotoc/place.rs index 5b5cc5011bbe..814f05d09265 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/place.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/place.rs @@ -102,6 +102,7 @@ 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. + // 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{:?}", From 5903d12e4564e736af3d3e4060a31e4a84a0dcb0 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 30 Jun 2021 14:25:24 -0400 Subject: [PATCH 3/5] Review comments --- .../rustc_codegen_llvm/src/gotoc/operand.rs | 6 ++++-- compiler/rustc_codegen_llvm/src/gotoc/place.rs | 4 ++-- src/test/cbmc/DynTrait/boxed_closure.rs | 10 ++++++++-- .../cbmc/DynTrait/boxed_closure_fail_fixme.rs | 18 ++++++++++++++++++ 4 files changed, 32 insertions(+), 6 deletions(-) create mode 100644 src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs diff --git a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs index bc7f024d3600..c79cae548b3d 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs @@ -29,9 +29,11 @@ impl<'tcx> GotocCtx<'tcx> { // TODO: move shouldn't be the same as copy { 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 + // 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, diff --git a/compiler/rustc_codegen_llvm/src/gotoc/place.rs b/compiler/rustc_codegen_llvm/src/gotoc/place.rs index 814f05d09265..af31c24b9c7f 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/place.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/place.rs @@ -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? @@ -103,7 +103,7 @@ 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. // https://github.com/model-checking/rmc/issues/277 - if !Self::_check_expr_typ(&goto_expr, &mir_typ_or_variant, ctx) { + 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 diff --git a/src/test/cbmc/DynTrait/boxed_closure.rs b/src/test/cbmc/DynTrait/boxed_closure.rs index 1c6b31042c87..6cfd4120746e 100644 --- a/src/test/cbmc/DynTrait/boxed_closure.rs +++ b/src/test/cbmc/DynTrait/boxed_closure.rs @@ -1,8 +1,14 @@ +// 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(|| { + let f: Box = Box::new(|x| { + assert!(x == 1) }); // Call it - f(); + f(1); } \ No newline at end of file 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..bfcdaa3f9acd --- /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); +} \ No newline at end of file From 96b7e541811307dd9b8fd1420cba4ead6db1e39e Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 30 Jun 2021 15:12:54 -0400 Subject: [PATCH 4/5] Whitespace and test typo --- src/test/cbmc/DynTrait/boxed_closure.rs | 6 ++---- src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs | 2 +- src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs | 2 +- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/test/cbmc/DynTrait/boxed_closure.rs b/src/test/cbmc/DynTrait/boxed_closure.rs index 6cfd4120746e..6f2e6042fbfd 100644 --- a/src/test/cbmc/DynTrait/boxed_closure.rs +++ b/src/test/cbmc/DynTrait/boxed_closure.rs @@ -5,10 +5,8 @@ fn main() { // Create a boxed once-callable closure - let f: Box = Box::new(|x| { - assert!(x == 1) - }); + let f: Box = Box::new(|x| assert!(x == 1)); // Call it f(1); -} \ No newline at end of file +} diff --git a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs index bfcdaa3f9acd..f638d11568db 100644 --- a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs +++ b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs @@ -15,4 +15,4 @@ fn main() { // Call it f(1); -} \ No newline at end of file +} 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() { From 93c251f0304a779e473ae5e60e9dcac40ed870f5 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 30 Jun 2021 20:23:37 +0000 Subject: [PATCH 5/5] Cleanup --- compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs | 1 - compiler/rustc_codegen_llvm/src/gotoc/mod.rs | 6 ------ compiler/rustc_codegen_llvm/src/gotoc/statement.rs | 8 +++----- 3 files changed, 3 insertions(+), 12 deletions(-) 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/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index e5038ace2353..82347dbaa34f 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use super::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; use super::metadata::*; -use super::typ::{is_dyn_trait_fat_pointer, FN_RETURN_VOID_VAR_NAME}; +use super::typ::FN_RETURN_VOID_VAR_NAME; use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ @@ -283,10 +283,10 @@ impl<'tcx> GotocCtx<'tcx> { return Stmt::goto(self.current_fn().find_label(&target), Location::none()); } // Handle a virtual function call via a vtable lookup - InstanceDef::Virtual(def_id, size) => { + InstanceDef::Virtual(def_id, _) => { // We must have at least one argument, and the first one // should be a fat pointer for the trait - let mut trait_fat_ptr = fargs[0].to_owned(); + let trait_fat_ptr = fargs[0].to_owned(); //Check the Gotoc-level fat pointer type assert!(trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)); @@ -295,7 +295,6 @@ impl<'tcx> GotocCtx<'tcx> { trait_fat_ptr, def_id, &p, - &target, &mut fargs, loc.clone(), ) @@ -342,7 +341,6 @@ impl<'tcx> GotocCtx<'tcx> { trait_fat_ptr: Expr, def_id: DefId, place: &Place<'tcx>, - target: &BasicBlock, fargs: &mut Vec, loc: Location, ) -> Vec {