From 7dad84740cb34d3b2dd79487f1b810abf0bbe231 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:35:11 +0200 Subject: [PATCH] Remove further uses of Location::none (#3253) We now only have 12 uses of `Location::none` left, all of which have no reasonable location to use. Resolves: #136 --- cprover_bindings/src/goto_program/expr.rs | 5 +- cprover_bindings/src/irep/to_irep.rs | 4 +- .../codegen_cprover_gotoc/codegen/assert.rs | 4 +- .../codegen_cprover_gotoc/codegen/contract.rs | 13 +- .../codegen/foreign_function.rs | 8 +- .../codegen/intrinsic.rs | 19 +-- .../codegen_cprover_gotoc/codegen/operand.rs | 113 ++++++++++-------- .../codegen_cprover_gotoc/codegen/place.rs | 30 ++--- .../codegen_cprover_gotoc/codegen/rvalue.rs | 65 +++++----- .../src/codegen_cprover_gotoc/codegen/span.rs | 4 - .../codegen/statement.rs | 38 +++--- .../codegen/static_var.rs | 2 +- .../codegen_cprover_gotoc/context/goto_ctx.rs | 15 ++- .../codegen_cprover_gotoc/overrides/hooks.rs | 35 +++--- kani-driver/src/cbmc_property_renderer.rs | 5 +- tests/cargo-kani/simple-extern/src/lib.rs | 3 + 16 files changed, 204 insertions(+), 159 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index c76b580237841..75eb18df0abbd 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -140,6 +140,7 @@ pub enum ExprValue { /// `({ op1; op2; ...})` StatementExpression { statements: Vec, + location: Location, }, /// A raw string constant. Note that you normally actually want a pointer to the first element. /// `"s"` @@ -739,10 +740,10 @@ impl Expr { /// /// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })` /// `({ op1; op2; ...})` - pub fn statement_expression(ops: Vec, typ: Type) -> Self { + pub fn statement_expression(ops: Vec, typ: Type, loc: Location) -> Self { assert!(!ops.is_empty()); assert_eq!(ops.last().unwrap().get_expression().unwrap().typ, typ); - expr!(StatementExpression { statements: ops }, typ) + expr!(StatementExpression { statements: ops, location: loc }, typ).with_location(loc) } /// Internal helper function for Struct initalizer diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 9ec8c49e80bf9..8716c16d88e00 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -299,9 +299,9 @@ impl ToIrep for ExprValue { named_sub: linear_map![], }, ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]), - ExprValue::StatementExpression { statements: ops } => side_effect_irep( + ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep( IrepId::StatementExpression, - vec![Stmt::block(ops.to_vec(), Location::none()).to_irep(mm)], + vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)], ), ExprValue::StringConstant { s } => Irep { id: IrepId::StringConstant, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 70a65ad6ebcae..f78cf3eba707b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -252,7 +252,7 @@ impl<'tcx> GotocCtx<'tcx> { t.nondet().as_stmt(loc), ]; - Expr::statement_expression(body, t).with_location(loc) + Expr::statement_expression(body, t, loc) } /// Kani does not currently support all MIR constructs. @@ -356,7 +356,7 @@ impl<'tcx> GotocCtx<'tcx> { // Encode __CPROVER_r_ok(ptr, size). // First, generate a CBMC expression representing the pointer. let ptr = { - let ptr_projection = self.codegen_place_stable(&ptr_place).unwrap(); + let ptr_projection = self.codegen_place_stable(&ptr_place, *loc).unwrap(); let place_ty = self.place_ty_stable(place); if self.use_thin_pointer_stable(place_ty) { ptr_projection.goto_expr().clone() diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 7edd64438728b..5494a3a666bd2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -3,7 +3,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::attributes::KaniAttributes; use cbmc::goto_program::FunctionContract; -use cbmc::goto_program::Lambda; +use cbmc::goto_program::{Lambda, Location}; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; @@ -105,7 +105,11 @@ impl<'tcx> GotocCtx<'tcx> { /// Convert the Kani level contract into a CBMC level contract by creating a /// CBMC lambda. - fn codegen_modifies_contract(&mut self, modified_places: Vec) -> FunctionContract { + fn codegen_modifies_contract( + &mut self, + modified_places: Vec, + loc: Location, + ) -> FunctionContract { let goto_annotated_fn_name = self.current_fn().name(); let goto_annotated_fn_typ = self .symbol_table @@ -120,7 +124,7 @@ impl<'tcx> GotocCtx<'tcx> { Lambda::as_contract_for( &goto_annotated_fn_typ, None, - self.codegen_place_stable(&local.into()).unwrap().goto_expr.dereference(), + self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(), ) }) .collect(); @@ -138,7 +142,8 @@ impl<'tcx> GotocCtx<'tcx> { assert!(self.current_fn.is_none()); let body = instance.body().unwrap(); self.set_current_fn(instance, &body); - let goto_contract = self.codegen_modifies_contract(modified_places); + let goto_contract = + self.codegen_modifies_contract(modified_places, self.codegen_span_stable(body.span)); let name = self.current_fn().name(); self.symbol_table.attach_contract(name, goto_contract); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 4ab72eb3a705d..9d5374ca22a83 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -50,6 +50,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol { debug!(?instance, "codegen_foreign_function"); let fn_name = self.symbol_name_stable(instance).intern(); + let loc = self.codegen_span_stable(instance.def.span()); if self.symbol_table.contains(fn_name) { // Symbol has been added (either a built-in CBMC function or a Rust allocation function). self.symbol_table.lookup(fn_name).unwrap() @@ -63,8 +64,7 @@ impl<'tcx> GotocCtx<'tcx> { // https://github.com/model-checking/kani/issues/2426 self.ensure(fn_name, |gcx, _| { let typ = gcx.codegen_ffi_type(instance); - Symbol::function(fn_name, typ, None, instance.name(), Location::none()) - .with_is_extern(true) + Symbol::function(fn_name, typ, None, instance.name(), loc).with_is_extern(true) }) } else { let shim_name = format!("{fn_name}_ffi_shim"); @@ -77,7 +77,7 @@ impl<'tcx> GotocCtx<'tcx> { typ, Some(gcx.codegen_ffi_shim(shim_name.as_str().into(), instance)), instance.name(), - Location::none(), + loc, ) }) } @@ -109,7 +109,7 @@ impl<'tcx> GotocCtx<'tcx> { } else { let ret_expr = unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place_stable(ret_place) + self.codegen_place_stable(ret_place, loc) ) .goto_expr; let ret_type = ret_expr.typ().clone(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 942c392030839..29ea69eeb39b5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -33,11 +33,12 @@ impl<'tcx> GotocCtx<'tcx> { place: &Place, mut fargs: Vec, f: F, + loc: Location, ) -> Stmt { let arg1 = fargs.remove(0); let arg2 = fargs.remove(0); let expr = f(arg1, arg2); - self.codegen_expr_to_place_stable(place, expr, Location::none()) + self.codegen_expr_to_place_stable(place, expr, loc) } /// Given a call to an compiler intrinsic, generate the call and the `goto` terminator @@ -178,7 +179,7 @@ impl<'tcx> GotocCtx<'tcx> { // Intrinsics which encode a simple binary operation macro_rules! codegen_intrinsic_binop { - ($f:ident) => {{ self.binop(place, fargs, |a, b| a.$f(b)) }}; + ($f:ident) => {{ self.binop(place, fargs, |a, b| a.$f(b), loc) }}; } // Intrinsics which encode a simple binary operation which need a machine model @@ -208,7 +209,7 @@ impl<'tcx> GotocCtx<'tcx> { let alloc = stable_instance.try_const_eval(place_ty).unwrap(); // We assume that the intrinsic has type checked at this point, so // we can use the place type as the expression type. - let expr = self.codegen_allocation(&alloc, place_ty, Some(span)); + let expr = self.codegen_allocation(&alloc, place_ty, loc); self.codegen_expr_to_place_stable(&place, expr, loc) }}; } @@ -727,7 +728,7 @@ impl<'tcx> GotocCtx<'tcx> { let res = self.codegen_binop_with_overflow(binop, left, right, result_type.clone(), loc); self.codegen_expr_to_place_stable( place, - Expr::statement_expression(vec![res.as_stmt(loc)], result_type), + Expr::statement_expression(vec![res.as_stmt(loc)], result_type, loc), loc, ) } @@ -1042,9 +1043,11 @@ impl<'tcx> GotocCtx<'tcx> { let is_lhs_ok = lhs_var.clone().is_nonnull(); let is_rhs_ok = rhs_var.clone().is_nonnull(); let should_skip_pointer_checks = is_len_zero.and(is_lhs_ok).and(is_rhs_ok); - let place_expr = - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place)) - .goto_expr; + let place_expr = unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(place, loc) + ) + .goto_expr; let res = should_skip_pointer_checks.ternary( Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned) BuiltinFn::Memcmp @@ -1634,7 +1637,7 @@ impl<'tcx> GotocCtx<'tcx> { loc, ) } else { - self.binop(p, fargs, op_fun) + self.binop(p, fargs, op_fun, loc) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 3b71cfec91c2e..4c45b475a3a77 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -11,8 +11,8 @@ use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; use stable_mir::mir::mono::{Instance, StaticDef}; use stable_mir::mir::Operand; use stable_mir::ty::{ - Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Span, - Ty, TyConst, TyConstKind, TyKind, UintTy, + Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty, + TyConst, TyConstKind, TyKind, UintTy, }; use stable_mir::{CrateDef, CrateItem}; use tracing::{debug, trace}; @@ -38,8 +38,10 @@ impl<'tcx> GotocCtx<'tcx> { Operand::Copy(place) | Operand::Move(place) => // TODO: move is an opportunity to poison/nondet the original memory. { - let projection = - unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place)); + let projection = unwrap_or_return_codegen_unimplemented!( + self, + self.codegen_place_stable(place, Location::none()) + ); // 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. @@ -51,7 +53,7 @@ impl<'tcx> GotocCtx<'tcx> { } } Operand::Constant(constant) => { - self.codegen_const(&constant.literal, Some(constant.span)) + self.codegen_const(&constant.literal, self.codegen_span_stable(constant.span)) } } } @@ -62,8 +64,11 @@ impl<'tcx> GotocCtx<'tcx> { span: Option, ) -> Expr { let stable_const = rustc_internal::stable(constant); - let stable_span = rustc_internal::stable(span); - self.codegen_const_ty(&stable_const, stable_span) + if let Some(stable_span) = rustc_internal::stable(span) { + self.codegen_const_ty(&stable_const, self.codegen_span_stable(stable_span)) + } else { + self.codegen_const_ty(&stable_const, Location::none()) + } } /// Generate a goto expression that represents a MIR-level constant. @@ -73,16 +78,16 @@ impl<'tcx> GotocCtx<'tcx> { /// generate code for it as simple literals or constants if possible. Otherwise, we create /// a memory allocation for them and access them indirectly. /// - ZeroSized: These are ZST constants and they just need to match the right type. - pub fn codegen_const(&mut self, constant: &MirConst, span: Option) -> Expr { + pub fn codegen_const(&mut self, constant: &MirConst, loc: Location) -> Expr { trace!(?constant, "codegen_constant"); match constant.kind() { - ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), span), + ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), loc), ConstantKind::ZeroSized => { let lit_ty = constant.ty(); match lit_ty.kind() { // Rust "function items" (not closures, not function pointers, see `codegen_fndef`) TyKind::RigidTy(RigidTy::FnDef(def, args)) => { - self.codegen_fndef(def, &args, span) + self.codegen_fndef(def, &args, loc) } _ => Expr::init_unit(self.codegen_ty_stable(lit_ty), &self.symbol_table), } @@ -90,7 +95,7 @@ impl<'tcx> GotocCtx<'tcx> { ConstantKind::Param(..) | ConstantKind::Unevaluated(..) => { unreachable!() } - ConstantKind::Ty(t) => self.codegen_const_ty(t, span), + ConstantKind::Ty(t) => self.codegen_const_ty(t, loc), } } @@ -101,19 +106,19 @@ impl<'tcx> GotocCtx<'tcx> { /// generate code for it as simple literals or constants if possible. Otherwise, we create /// a memory allocation for them and access them indirectly. /// - ZeroSized: These are ZST constants and they just need to match the right type. - pub fn codegen_const_ty(&mut self, constant: &TyConst, span: Option) -> Expr { + pub fn codegen_const_ty(&mut self, constant: &TyConst, loc: Location) -> Expr { trace!(?constant, "codegen_constant"); match constant.kind() { TyConstKind::ZSTValue(lit_ty) => { match lit_ty.kind() { // Rust "function items" (not closures, not function pointers, see `codegen_fndef`) TyKind::RigidTy(RigidTy::FnDef(def, args)) => { - self.codegen_fndef(def, &args, span) + self.codegen_fndef(def, &args, loc) } _ => Expr::init_unit(self.codegen_ty_stable(*lit_ty), &self.symbol_table), } } - TyConstKind::Value(ty, alloc) => self.codegen_allocation(alloc, *ty, span), + TyConstKind::Value(ty, alloc) => self.codegen_allocation(alloc, *ty, loc), TyConstKind::Bound(..) => unreachable!(), TyConstKind::Param(..) | TyConstKind::Unevaluated(..) => { unreachable!() @@ -121,11 +126,11 @@ impl<'tcx> GotocCtx<'tcx> { } } - pub fn codegen_allocation(&mut self, alloc: &Allocation, ty: Ty, span: Option) -> Expr { + pub fn codegen_allocation(&mut self, alloc: &Allocation, ty: Ty, loc: Location) -> Expr { // First try to generate the constant without allocating memory. - let expr = self.try_codegen_constant(alloc, ty, span).unwrap_or_else(|| { + let expr = self.try_codegen_constant(alloc, ty, loc).unwrap_or_else(|| { debug!("codegen_allocation try_fail"); - let mem_var = self.codegen_const_allocation(alloc, None); + let mem_var = self.codegen_const_allocation(alloc, None, loc); mem_var .cast_to(Type::unsigned_int(8).to_pointer()) .cast_to(self.codegen_ty_stable(ty).to_pointer()) @@ -143,12 +148,7 @@ impl<'tcx> GotocCtx<'tcx> { /// 3. enums that don't carry data /// 4. unit, tuples (may be multi-ary!), or size-0 arrays /// 5. pointers to an allocation - fn try_codegen_constant( - &mut self, - alloc: &Allocation, - ty: Ty, - span: Option, - ) -> Option { + fn try_codegen_constant(&mut self, alloc: &Allocation, ty: Ty, loc: Location) -> Option { debug!(?alloc, ?ty, "try_codegen_constant"); match ty.kind() { TyKind::RigidTy(RigidTy::Int(it)) => { @@ -194,7 +194,7 @@ impl<'tcx> GotocCtx<'tcx> { } TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) | TyKind::RigidTy(RigidTy::Ref(_, inner_ty, _)) => { - Some(self.codegen_const_ptr(alloc, ty, inner_ty, span)) + Some(self.codegen_const_ptr(alloc, ty, inner_ty, loc)) } TyKind::RigidTy(RigidTy::Adt(adt, args)) if adt.kind().is_struct() => { // Structs only have one variant. @@ -221,7 +221,7 @@ impl<'tcx> GotocCtx<'tcx> { &self.symbol_table, )) } else { - self.try_codegen_constant(alloc, *t, span) + self.try_codegen_constant(alloc, *t, loc) } }) .collect::>>()?; @@ -238,7 +238,7 @@ impl<'tcx> GotocCtx<'tcx> { } TyKind::RigidTy(RigidTy::Tuple(tys)) if tys.len() == 1 => { let overall_t = self.codegen_ty_stable(ty); - let inner_expr = self.try_codegen_constant(alloc, tys[0], span)?; + let inner_expr = self.try_codegen_constant(alloc, tys[0], loc)?; Some(inner_expr.transmute_to(overall_t, &self.symbol_table)) } // Everything else we encode as an allocation. @@ -251,7 +251,7 @@ impl<'tcx> GotocCtx<'tcx> { alloc: &Allocation, ty: Ty, inner_ty: Ty, - span: Option, + loc: Location, ) -> Expr { debug!(?ty, ?alloc, "codegen_const_ptr"); if self.use_fat_pointer_stable(inner_ty) { @@ -268,7 +268,7 @@ impl<'tcx> GotocCtx<'tcx> { let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else { unreachable!() }; - let mem_var = self.codegen_const_allocation(&data, None); + let mem_var = self.codegen_const_allocation(&data, None, loc); // Extract identifier for static variable. // codegen_allocation_auto_imm_name returns the *address* of @@ -309,7 +309,7 @@ impl<'tcx> GotocCtx<'tcx> { let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else { unreachable!() }; - let mem_var = self.codegen_const_allocation(&data, None); + let mem_var = self.codegen_const_allocation(&data, None, loc); let inner_typ = self.codegen_ty_stable(inner_ty); let len = data.bytes.len() / inner_typ.sizeof(&self.symbol_table) as usize; let data_expr = mem_var.cast_to(inner_typ.to_pointer()); @@ -325,7 +325,6 @@ impl<'tcx> GotocCtx<'tcx> { TyKind::RigidTy(RigidTy::Adt(def, _)) if def.name().ends_with("::CStr") => { // TODO: Handle CString // - let loc = self.codegen_span_option_stable(span); let typ = self.codegen_ty_stable(ty); let operation_name = "C string literal"; self.codegen_unimplemented_expr( @@ -343,7 +342,7 @@ impl<'tcx> GotocCtx<'tcx> { let ptr = alloc.provenance.ptrs[0]; let alloc_id = ptr.1.0; let typ = self.codegen_ty_stable(ty); - self.codegen_alloc_pointer(typ, alloc_id, ptr.0, span) + self.codegen_alloc_pointer(typ, alloc_id, ptr.0, loc) } else { // If there's no provenance, just codegen the pointer address. trace!("codegen_const_ptr no_prov"); @@ -359,13 +358,13 @@ impl<'tcx> GotocCtx<'tcx> { res_t: Type, alloc_id: AllocId, offset: Size, - span: Option, + loc: Location, ) -> Expr { debug!(?res_t, ?alloc_id, "codegen_alloc_pointer"); let base_addr = match GlobalAlloc::from(alloc_id) { GlobalAlloc::Function(instance) => { // We want to return the function pointer (not to be confused with function item) - self.codegen_func_expr(instance, span).address_of() + self.codegen_func_expr(instance, loc).address_of() } GlobalAlloc::Static(def) => self.codegen_static_pointer(def), GlobalAlloc::Memory(alloc) => { @@ -373,7 +372,7 @@ impl<'tcx> GotocCtx<'tcx> { // crates do not conflict. The name alone is insufficient because Rust // allows different versions of the same crate to be used. let name = format!("{}::{alloc_id:?}", self.full_crate_name()); - self.codegen_const_allocation(&alloc, Some(name)) + self.codegen_const_allocation(&alloc, Some(name), loc) } alloc @ GlobalAlloc::VTable(..) => { // This is similar to GlobalAlloc::Memory but the type is opaque to rust and it @@ -383,7 +382,7 @@ impl<'tcx> GotocCtx<'tcx> { unreachable!() }; let name = format!("{}::{alloc_id:?}", self.full_crate_name()); - self.codegen_const_allocation(&alloc, Some(name)) + self.codegen_const_allocation(&alloc, Some(name), loc) } }; assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table)); @@ -459,12 +458,17 @@ impl<'tcx> GotocCtx<'tcx> { /// /// These constants can be named constants which are declared by the user, or constant values /// used scattered throughout the source - fn codegen_const_allocation(&mut self, alloc: &Allocation, name: Option) -> Expr { + fn codegen_const_allocation( + &mut self, + alloc: &Allocation, + name: Option, + loc: Location, + ) -> Expr { debug!(?name, "codegen_const_allocation"); let alloc_name = match self.alloc_map.get(alloc) { None => { let alloc_name = if let Some(name) = name { name } else { self.next_global_name() }; - self.codegen_alloc_in_memory(alloc.clone(), alloc_name.clone()); + self.codegen_alloc_in_memory(alloc.clone(), alloc_name.clone(), loc); alloc_name } Some(name) => name.clone(), @@ -479,7 +483,7 @@ impl<'tcx> GotocCtx<'tcx> { /// /// This function is ultimately responsible for creating new statically initialized global variables /// in our goto binaries. - pub fn codegen_alloc_in_memory(&mut self, alloc: Allocation, name: String) { + pub fn codegen_alloc_in_memory(&mut self, alloc: Allocation, name: String, loc: Location) { debug!(?alloc, ?name, "codegen_alloc_in_memory"); let struct_name = &format!("{name}::struct"); @@ -488,7 +492,7 @@ impl<'tcx> GotocCtx<'tcx> { // initializers. For example, for a boolean static variable, the variable will have type // CBool and the initializer will be a single byte (a one-character array) representing the // bit pattern for the boolean value. - let alloc_data = self.codegen_allocation_data(&alloc); + let alloc_data = self.codegen_allocation_data(&alloc, loc); let alloc_typ_ref = self.ensure_struct(struct_name, struct_name, |_, _| { alloc_data .iter() @@ -511,7 +515,7 @@ impl<'tcx> GotocCtx<'tcx> { &name, false, //TODO is this correct? alloc_typ_ref.clone(), - Location::none(), + loc, |_, _| None, ); let var_typ = var.typ().clone(); @@ -538,13 +542,13 @@ impl<'tcx> GotocCtx<'tcx> { &self.symbol_table, ); let fn_name = Self::initializer_fn_name(&name); - let temp_var = self.gen_function_local_variable(0, &fn_name, alloc_typ_ref).to_expr(); + let temp_var = self.gen_function_local_variable(0, &fn_name, alloc_typ_ref, loc).to_expr(); let body = Stmt::block( vec![ - Stmt::decl(temp_var.clone(), Some(val), Location::none()), - var.assign(temp_var.transmute_to(var_typ, &self.symbol_table), Location::none()), + Stmt::decl(temp_var.clone(), Some(val), loc), + var.assign(temp_var.transmute_to(var_typ, &self.symbol_table), loc), ], - Location::none(), + loc, ); self.register_initializer(&name, body); @@ -556,7 +560,11 @@ impl<'tcx> GotocCtx<'tcx> { /// We codegen global statics as their own unique struct types, and this creates a field-by-field /// representation of what those fields should be initialized with. /// (A field is either bytes, or initialized with an expression.) - fn codegen_allocation_data<'a>(&mut self, alloc: &'a Allocation) -> Vec> { + fn codegen_allocation_data<'a>( + &mut self, + alloc: &'a Allocation, + loc: Location, + ) -> Vec> { let mut alloc_vals = Vec::with_capacity(alloc.provenance.ptrs.len() + 1); let pointer_size = self.symbol_table.machine_model().pointer_width_in_bytes(); @@ -571,7 +579,7 @@ impl<'tcx> GotocCtx<'tcx> { Type::signed_int(8).to_pointer(), prov.0, ptr_offset.try_into().unwrap(), - None, + loc, ))); next_offset = offset + pointer_size; @@ -607,9 +615,9 @@ impl<'tcx> GotocCtx<'tcx> { /// function types. /// /// See - pub fn codegen_fndef(&mut self, def: FnDef, args: &GenericArgs, span: Option) -> Expr { + pub fn codegen_fndef(&mut self, def: FnDef, args: &GenericArgs, loc: Location) -> Expr { let instance = Instance::resolve(def, args).unwrap(); - self.codegen_fn_item(instance, span) + self.codegen_fn_item(instance, loc) } /// Ensure that the given instance is in the symbol table, returning the symbol. @@ -633,10 +641,9 @@ impl<'tcx> GotocCtx<'tcx> { /// Note: In general with this `Expr` you should immediately either `.address_of()` or `.call(...)`. /// /// This should not be used where Rust expects a "function item" (See `codegen_fn_item`) - pub fn codegen_func_expr(&mut self, instance: Instance, span: Option) -> Expr { + pub fn codegen_func_expr(&mut self, instance: Instance, loc: Location) -> Expr { let func_symbol = self.codegen_func_symbol(instance); - Expr::symbol_expression(func_symbol.name, func_symbol.typ.clone()) - .with_location(self.codegen_span_option_stable(span)) + Expr::symbol_expression(func_symbol.name, func_symbol.typ.clone()).with_location(loc) } /// Generate a goto expression referencing the singleton value for a MIR "function item". @@ -644,7 +651,7 @@ impl<'tcx> GotocCtx<'tcx> { /// For a given function instance, generate a ZST struct and return a singleton reference to that. /// This is the Rust "function item". See /// This is not the function pointer, for that use `codegen_func_expr`. - fn codegen_fn_item(&mut self, instance: Instance, span: Option) -> Expr { + fn codegen_fn_item(&mut self, instance: Instance, loc: Location) -> Expr { let func_symbol = self.codegen_func_symbol(instance); let mangled_name = func_symbol.name; let fn_item_struct_ty = self.codegen_fndef_type_stable(instance); @@ -654,7 +661,7 @@ impl<'tcx> GotocCtx<'tcx> { &fn_singleton_name, false, fn_item_struct_ty, - self.codegen_span_option_stable(span), + loc, |_, _| None, // zero-sized, so no initialization necessary ) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 771a38ac922de..d0e3fc3f442fb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -364,22 +364,20 @@ impl<'tcx> GotocCtx<'tcx> { /// a named variable. /// /// Recursively finds the actual FnDef from a pointer or box. - fn codegen_local_fndef(&mut self, ty: Ty) -> Option { + fn codegen_local_fndef(&mut self, ty: Ty, loc: Location) -> Option { match ty.kind() { // A local that is itself a FnDef, like Fn::call_once - TyKind::RigidTy(RigidTy::FnDef(def, args)) => { - Some(self.codegen_fndef(def, &args, None)) - } + TyKind::RigidTy(RigidTy::FnDef(def, args)) => Some(self.codegen_fndef(def, &args, loc)), // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut TyKind::RigidTy(RigidTy::RawPtr(inner, _)) => self - .codegen_local_fndef(inner) + .codegen_local_fndef(inner, loc) .map(|f| if f.can_take_address_of() { f.address_of() } else { f }), // A local can be a boxed function pointer TyKind::RigidTy(RigidTy::Adt(def, args)) if def.is_box() => { let boxed_ty = self.codegen_ty_stable(ty); // The type of `T` for `Box` can be derived from the first definition args. let inner_ty = args.0[0].ty().unwrap(); - self.codegen_local_fndef(*inner_ty) + self.codegen_local_fndef(*inner_ty, loc) .map(|f| self.box_value(f.address_of(), boxed_ty)) } _ => None, @@ -387,10 +385,10 @@ impl<'tcx> GotocCtx<'tcx> { } /// Codegen for a local - pub fn codegen_local(&mut self, l: Local) -> Expr { + pub fn codegen_local(&mut self, l: Local, loc: Location) -> Expr { let local_ty = self.local_ty_stable(l); // Check if the local is a function definition (see comment above) - if let Some(fn_def) = self.codegen_local_fndef(local_ty) { + if let Some(fn_def) = self.codegen_local_fndef(local_ty, loc) { return fn_def; } @@ -408,6 +406,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, before: Result, proj: &ProjectionElem, + loc: Location, ) -> Result { let before = before?; trace!(?before, ?proj, "codegen_projection"); @@ -500,7 +499,7 @@ impl<'tcx> GotocCtx<'tcx> { } ProjectionElem::Index(i) => { let base_type = before.mir_typ(); - let idxe = self.codegen_local(*i); + let idxe = self.codegen_local(*i, loc); let typ = match base_type.kind() { TyKind::RigidTy(RigidTy::Array(elemt, _)) | TyKind::RigidTy(RigidTy::Slice(elemt)) => TypeOrVariant::Type(elemt), @@ -651,10 +650,10 @@ impl<'tcx> GotocCtx<'tcx> { /// build the fat pointer from there. /// - For `*(Wrapper)` where `T: Unsized`, the projection's `goto_expr` returns an object, /// and we need to take it's address and build the fat pointer. - pub fn codegen_place_ref_stable(&mut self, place: &Place) -> Expr { + pub fn codegen_place_ref_stable(&mut self, place: &Place, loc: Location) -> Expr { let place_ty = self.place_ty_stable(place); let projection = - unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place)); + unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place, loc)); if self.use_thin_pointer_stable(place_ty) { // For ZST objects rustc does not necessarily generate any actual objects. let need_not_be_an_object = self.is_zst_object(&projection.goto_expr); @@ -678,6 +677,7 @@ impl<'tcx> GotocCtx<'tcx> { Expr::statement_expression( vec![decl, assume_non_zero, assume_aligned, cast_to_pointer_type], address_of.typ().clone(), + *loc, ) } else { // Just return the address of the place dereferenced. @@ -711,9 +711,10 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_place_stable( &mut self, place: &Place, + loc: Location, ) -> Result { debug!(?place, "codegen_place"); - let initial_expr = self.codegen_local(place.local); + let initial_expr = self.codegen_local(place.local, loc); let initial_typ = TypeOrVariant::Type(self.local_ty_stable(place.local)); debug!(?initial_typ, ?initial_expr, "codegen_place"); let initial_projection = @@ -721,7 +722,7 @@ impl<'tcx> GotocCtx<'tcx> { let result = place .projection .iter() - .fold(initial_projection, |accum, proj| self.codegen_projection(accum, proj)); + .fold(initial_projection, |accum, proj| self.codegen_projection(accum, proj, loc)); match result { Err(data) => Err(UnimplementedData::new( &data.operation, @@ -738,10 +739,11 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, initial_projection: ProjectedPlace, variant_idx: VariantIdx, + loc: Location, ) -> ProjectedPlace { debug!(?initial_projection, ?variant_idx, "codegen_variant_lvalue"); let downcast = ProjectionElem::Downcast(variant_idx); - self.codegen_projection(Ok(initial_projection), &downcast).unwrap() + self.codegen_projection(Ok(initial_projection), &downcast, loc).unwrap() } // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 21185624942c7..31590266a7b80 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -73,7 +73,7 @@ impl<'tcx> GotocCtx<'tcx> { ret_type.nondet().as_stmt(loc).with_location(loc), ]; - Expr::statement_expression(body, ret_type).with_location(loc) + Expr::statement_expression(body, ret_type, loc) } else { // Compare data pointer. let res_ty = op.ty(left_typ, right_typ); @@ -167,12 +167,12 @@ impl<'tcx> GotocCtx<'tcx> { op_expr.array_constant(width).with_location(loc) } - fn codegen_rvalue_len(&mut self, p: &Place) -> Expr { + fn codegen_rvalue_len(&mut self, p: &Place, loc: Location) -> Expr { let pt = self.place_ty_stable(p); match pt.kind() { - TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const_ty(&sz, None), + TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const_ty(&sz, loc), TyKind::RigidTy(RigidTy::Slice(_)) => { - unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(p)) + unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(p, loc)) .fat_ptr_goto_expr .unwrap() .member("len", &self.symbol_table) @@ -224,6 +224,7 @@ impl<'tcx> GotocCtx<'tcx> { var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table).as_stmt(loc), ], ret_type, + loc, ) } @@ -254,7 +255,7 @@ impl<'tcx> GotocCtx<'tcx> { ], &self.symbol_table, ); - Expr::statement_expression(vec![decl, cast.as_stmt(loc)], expected_typ) + Expr::statement_expression(vec![decl, cast.as_stmt(loc)], expected_typ, loc) } /// Generate code for a binary arithmetic operation with UB / overflow checks in place. @@ -371,6 +372,7 @@ impl<'tcx> GotocCtx<'tcx> { Expr::statement_expression( vec![check, result.clone().as_stmt(loc)], result.typ().clone(), + loc, ) } BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => { @@ -384,6 +386,7 @@ impl<'tcx> GotocCtx<'tcx> { Expr::statement_expression( vec![check, result.clone().as_stmt(loc)], result.typ().clone(), + loc, ) } else { result @@ -429,6 +432,7 @@ impl<'tcx> GotocCtx<'tcx> { Expr::statement_expression( vec![bytes_overflow_check, overflow_check, res.as_stmt(loc)], ce1.typ().clone(), + loc, ) } } @@ -566,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> { // 2- Initialize the members of the temporary variant. let initial_projection = ProjectedPlace::try_from_ty(temp_var.clone(), res_ty, self).unwrap(); - let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index); + let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index, loc); let variant_expr = variant_proj.goto_expr.clone(); let layout = self.layout_of_stable(res_ty); let fields = match &layout.variants { @@ -603,7 +607,7 @@ impl<'tcx> GotocCtx<'tcx> { stmts.push(set_discriminant); // 4- Return temporary variable. stmts.push(temp_var.as_stmt(loc)); - Expr::statement_expression(stmts, typ) + Expr::statement_expression(stmts, typ, loc) } fn codegen_rvalue_aggregate( @@ -723,13 +727,14 @@ impl<'tcx> GotocCtx<'tcx> { Rvalue::Use(p) => self.codegen_operand_stable(p), Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc), Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => { - let place_ref = self.codegen_place_ref_stable(&p); + let place_ref = self.codegen_place_ref_stable(&p, loc); if self.queries.args().ub_check.contains(&ExtraChecks::PtrToRefCast) { let place_ref_type = place_ref.typ().clone(); match self.codegen_raw_ptr_deref_validity_check(&p, &loc) { Some(ptr_validity_check_expr) => Expr::statement_expression( vec![ptr_validity_check_expr, place_ref.as_stmt(loc)], place_ref_type, + loc, ), None => place_ref, } @@ -737,7 +742,7 @@ impl<'tcx> GotocCtx<'tcx> { place_ref } } - Rvalue::Len(p) => self.codegen_rvalue_len(p), + Rvalue::Len(p) => self.codegen_rvalue_len(p, loc), // Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet: // Should we? Tracking ticket: https://github.com/model-checking/kani/issues/1274 Rvalue::Cast( @@ -862,9 +867,11 @@ impl<'tcx> GotocCtx<'tcx> { } }, Rvalue::Discriminant(p) => { - let place = - unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(p)) - .goto_expr; + let place = unwrap_or_return_codegen_unimplemented!( + self, + self.codegen_place_stable(p, loc) + ) + .goto_expr; let pt = self.place_ty_stable(p); self.codegen_get_discriminant(place, pt, res_ty) } @@ -879,7 +886,7 @@ impl<'tcx> GotocCtx<'tcx> { // A CopyForDeref is equivalent to a read from a place at the codegen level. // https://github.com/rust-lang/rust/blob/1673f1450eeaf4a5452e086db0fe2ae274a0144f/compiler/rustc_middle/src/mir/syntax.rs#L1055 Rvalue::CopyForDeref(place) => { - unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place)) + unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place, loc)) .goto_expr } } @@ -1130,7 +1137,7 @@ impl<'tcx> GotocCtx<'tcx> { let instance = Instance::resolve(def, &args).unwrap(); // We need to handle this case in a special way because `codegen_operand_stable` compiles FnDefs to dummy structs. // (cf. the function documentation) - self.codegen_func_expr(instance, None).address_of() + self.codegen_func_expr(instance, loc).address_of() } _ => unreachable!(), }, @@ -1141,7 +1148,7 @@ impl<'tcx> GotocCtx<'tcx> { { let instance = Instance::resolve_closure(def, &args, ClosureKind::FnOnce) .expect("failed to normalize and resolve closure during codegen"); - self.codegen_func_expr(instance, None).address_of() + self.codegen_func_expr(instance, loc).address_of() } else { unreachable!("{:?} cannot be cast to a fn ptr", operand) } @@ -1173,7 +1180,7 @@ impl<'tcx> GotocCtx<'tcx> { let src_goto_expr = self.codegen_operand_stable(operand); let src_mir_type = self.operand_ty_stable(operand); let dst_mir_type = t; - self.codegen_unsized_cast(src_goto_expr, src_mir_type, dst_mir_type) + self.codegen_unsized_cast(src_goto_expr, src_mir_type, dst_mir_type, loc) } } } @@ -1191,6 +1198,7 @@ impl<'tcx> GotocCtx<'tcx> { src_goto_expr: Expr, src_mir_type: Ty, dst_mir_type: Ty, + loc: Location, ) -> Expr { // The MIR may include casting that isn't necessary. Detect this early on and return the // expression for the RHS. @@ -1204,7 +1212,7 @@ impl<'tcx> GotocCtx<'tcx> { // Handle the leaf which should always be a pointer. let (ptr_cast_info, ptr_src_expr) = path.pop().unwrap(); - let initial_expr = self.codegen_cast_to_fat_pointer(ptr_src_expr, ptr_cast_info); + let initial_expr = self.codegen_cast_to_fat_pointer(ptr_src_expr, ptr_cast_info, loc); // Iterate from the back of the path initializing each struct that requires the coercion. // This code is required for handling smart pointers. @@ -1370,7 +1378,7 @@ impl<'tcx> GotocCtx<'tcx> { // Check the size are inserting in to the vtable against two sources of // truth: (1) the compile-time rustc sizeof functions, and (2) the CBMC // __CPROVER_OBJECT_SIZE function. - fn check_vtable_size(&mut self, operand_type: Ty, vt_size: Expr) -> Stmt { + fn check_vtable_size(&mut self, operand_type: Ty, vt_size: Expr, loc: Location) -> Stmt { // Check against the size we get from the layout from the what we // get constructing a value of that type let ty = self.codegen_ty_stable(operand_type); @@ -1380,7 +1388,7 @@ impl<'tcx> GotocCtx<'tcx> { // Insert a CBMC-time size check, roughly: // local_temp = nondet(); // assert(__CPROVER_OBJECT_SIZE(&local_temp) == vt_size); - let (temp_var, decl) = self.decl_temp_variable(ty.clone(), None, Location::none()); + let (temp_var, decl) = self.decl_temp_variable(ty.clone(), None, loc); let cbmc_size = if ty.is_empty() { // CBMC errors on passing a pointer to void to __CPROVER_OBJECT_SIZE. // In practice, we have seen this with the Never type, which has size 0: @@ -1396,11 +1404,11 @@ impl<'tcx> GotocCtx<'tcx> { let check = Expr::eq(cbmc_size, vt_size); let assert_msg = format!("Correct CBMC vtable size for {ty:?} (MIR type {:?})", operand_type.kind()); - let size_assert = self.codegen_sanity(check, &assert_msg, Location::none()); - Stmt::block(vec![decl, size_assert], Location::none()) + let size_assert = self.codegen_sanity(check, &assert_msg, loc); + Stmt::block(vec![decl, size_assert], loc) } - fn codegen_vtable(&mut self, src_mir_type: Ty, dst_mir_type: Ty) -> Expr { + fn codegen_vtable(&mut self, src_mir_type: Ty, dst_mir_type: Ty, loc: Location) -> Expr { let trait_type = match dst_mir_type.kind() { // DST is pointer type TyKind::RigidTy(RigidTy::Ref(_, pointee_type, ..)) => pointee_type, @@ -1422,7 +1430,7 @@ impl<'tcx> GotocCtx<'tcx> { vtable_impl_name, true, Type::struct_tag(vtable_name), - Location::none(), + loc, |ctx, var| { // Build the vtable, using Rust's vtable_entries to determine field order let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() { @@ -1433,7 +1441,7 @@ impl<'tcx> GotocCtx<'tcx> { }; let (vt_size, vt_align) = ctx.codegen_vtable_size_and_align(src_mir_type); - let size_assert = ctx.check_vtable_size(src_mir_type, vt_size.clone()); + let size_assert = ctx.check_vtable_size(src_mir_type, vt_size.clone(), loc); let vtable_fields: Vec = vtable_entries .iter() @@ -1461,8 +1469,8 @@ impl<'tcx> GotocCtx<'tcx> { vtable_fields, &ctx.symbol_table, ); - let body = var.assign(vtable, Location::none()); - let block = Stmt::block(vec![size_assert, body], Location::none()); + let body = var.assign(vtable, loc); + let block = Stmt::block(vec![size_assert, body], loc); Some(block) }, ) @@ -1476,6 +1484,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, src_goto_expr: Expr, coerce_info: CoerceUnsizedInfo, + loc: Location, ) -> Expr { assert_ne!(coerce_info.src_ty.kind(), coerce_info.dst_ty.kind()); @@ -1499,7 +1508,7 @@ impl<'tcx> GotocCtx<'tcx> { ) => { // Cast to a slice fat pointer. assert_eq!(src_elt_type, dst_elt_type); - let dst_goto_len = self.codegen_const_ty(&src_elt_count, None); + let dst_goto_len = self.codegen_const_ty(&src_elt_count, loc); let src_pointee_ty = pointee_type_stable(coerce_info.src_ty).unwrap(); let dst_data_expr = if src_pointee_ty.kind().is_array() { src_goto_expr.cast_to(self.codegen_ty_stable(src_elt_type).to_pointer()) @@ -1527,7 +1536,7 @@ impl<'tcx> GotocCtx<'tcx> { (_, TyKind::RigidTy(RigidTy::Dynamic(..))) => { // Generate the data and vtable pointer that will be stored in the fat pointer. let dst_data_expr = src_goto_expr.cast_to(dst_data_type); - let vtable = self.codegen_vtable(metadata_src_type, metadata_dst_type); + let vtable = self.codegen_vtable(metadata_src_type, metadata_dst_type, loc); let vtable_expr = vtable.address_of(); dynamic_fat_ptr(fat_ptr_type, dst_data_expr, vtable_expr, &self.symbol_table) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index d068298222743..aadb4fbebed91 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -26,10 +26,6 @@ impl<'tcx> GotocCtx<'tcx> { ) } - pub fn codegen_span_option_stable(&self, sp: Option) -> Location { - sp.map_or(Location::none(), |span| self.codegen_span_stable(span)) - } - pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location { self.codegen_caller_span(&rustc_internal::internal(self.tcx, sp)) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 1e81cccd0c070..c606ae13d0958 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -42,14 +42,14 @@ impl<'tcx> GotocCtx<'tcx> { // where the reference is implicit. unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place_stable(lhs) + self.codegen_place_stable(lhs, location) ) .goto_expr .assign(self.codegen_rvalue_stable(rhs, location).address_of(), location) } else if rty.kind().is_bool() { unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place_stable(lhs) + self.codegen_place_stable(lhs, location) ) .goto_expr .assign( @@ -59,7 +59,7 @@ impl<'tcx> GotocCtx<'tcx> { } else { unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place_stable(lhs) + self.codegen_place_stable(lhs, location) ) .goto_expr .assign(self.codegen_rvalue_stable(rhs, location), location) @@ -70,7 +70,7 @@ impl<'tcx> GotocCtx<'tcx> { let dest_ty = self.place_ty_stable(place); let dest_expr = unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place_stable(place) + self.codegen_place_stable(place, location) ) .goto_expr; self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) @@ -79,14 +79,14 @@ impl<'tcx> GotocCtx<'tcx> { if self.queries.args().ignore_storage_markers { Stmt::skip(location) } else { - Stmt::decl(self.codegen_local(*var_id), None, location) + Stmt::decl(self.codegen_local(*var_id, location), None, location) } } StatementKind::StorageDead(var_id) => { if self.queries.args().ignore_storage_markers { Stmt::skip(location) } else { - Stmt::dead(self.codegen_local(*var_id), location) + Stmt::dead(self.codegen_local(*var_id, location), location) } } StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( @@ -156,7 +156,7 @@ impl<'tcx> GotocCtx<'tcx> { let place = Place::from(RETURN_LOCAL); let place_expr = unwrap_or_return_codegen_unimplemented_stmt!( self, - self.codegen_place_stable(&place) + self.codegen_place_stable(&place, loc) ) .goto_expr; assert_eq!(rty, self.place_ty_stable(&place), "Unexpected return type"); @@ -304,9 +304,12 @@ impl<'tcx> GotocCtx<'tcx> { // We ignore assignment for all zero size types Stmt::skip(loc) } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place)) - .goto_expr - .deinit(loc) + unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(place, loc) + ) + .goto_expr + .deinit(loc) } } @@ -338,7 +341,7 @@ impl<'tcx> GotocCtx<'tcx> { } InstanceKind::Shim => { // Since the reference is used right away here, no need to inject a check for pointer validity. - let place_ref = self.codegen_place_ref_stable(place); + let place_ref = self.codegen_place_ref_stable(place, loc); match place_ty.kind() { TyKind::RigidTy(RigidTy::Dynamic(..)) => { // Virtual drop via a vtable lookup. @@ -364,7 +367,7 @@ impl<'tcx> GotocCtx<'tcx> { // Non-virtual, direct drop_in_place call assert!(!matches!(drop_instance.kind, InstanceKind::Virtual { .. })); - let func = self.codegen_func_expr(drop_instance, None); + let func = self.codegen_func_expr(drop_instance, loc); // The only argument should be a self reference let args = vec![place_ref]; @@ -572,7 +575,7 @@ impl<'tcx> GotocCtx<'tcx> { InstanceKind::Item | InstanceKind::Intrinsic | InstanceKind::Shim => { // We need to handle FnDef items in a special way because `codegen_operand` compiles them to dummy structs. // (cf. the function documentation) - let func_exp = self.codegen_func_expr(instance, None); + let func_exp = self.codegen_func_expr(instance, loc); if instance.is_foreign_item() { vec![self.codegen_foreign_call(func_exp, fargs, destination, loc)] } else { @@ -723,9 +726,12 @@ impl<'tcx> GotocCtx<'tcx> { if self.place_ty_stable(place).kind().is_unit() { expr.as_stmt(loc) } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place)) - .goto_expr - .assign(expr, loc) + unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(place, loc) + ) + .goto_expr + .assign(expr, loc) } } } 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 0a0a55ad3dd4c..e05da3f7f6224 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -19,7 +19,7 @@ impl<'tcx> GotocCtx<'tcx> { debug!("codegen_static"); let alloc = def.eval_initializer().unwrap(); let symbol_name = Instance::from(def).mangled_name(); - self.codegen_alloc_in_memory(alloc, symbol_name); + self.codegen_alloc_in_memory(alloc, symbol_name, self.codegen_span_stable(def.span())); } /// Mutates the Goto-C symbol table to add a forward-declaration of the static variable. diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 9a81838b7fc2b..7d51cff037c63 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -137,8 +137,14 @@ impl<'tcx> GotocCtx<'tcx> { } // Generate a Symbol Expression representing a function variable from the MIR - pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol { - self.gen_stack_variable(c, fname, "var", t, Location::none()) + pub fn gen_function_local_variable( + &mut self, + c: u64, + fname: &str, + t: Type, + loc: Location, + ) -> Symbol { + self.gen_stack_variable(c, fname, "var", t, loc) } /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable @@ -283,13 +289,14 @@ impl<'tcx> GotocCtx<'tcx> { pub fn register_initializer(&mut self, var_name: &str, body: Stmt) -> &Symbol { let fn_name = Self::initializer_fn_name(var_name); let pretty_name = format!("{var_name}::init"); + let loc = *body.location(); self.ensure(&fn_name, |_tcx, _| { Symbol::function( &fn_name, Type::code(vec![], Type::constructor()), - Some(Stmt::block(vec![body], Location::none())), //TODO is this block needed? + Some(Stmt::block(vec![body], loc)), //TODO is this block needed? &pretty_name, - Location::none(), + loc, ) .with_is_file_local(true) }) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index d66e16b6ce59b..fc245fc6f4c9d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -168,7 +168,7 @@ impl GotocHook for Nondet { } else { let pe = unwrap_or_return_codegen_unimplemented_stmt!( gcx, - gcx.codegen_place_stable(assign_to) + gcx.codegen_place_stable(assign_to, loc) ) .goto_expr; Stmt::block( @@ -228,8 +228,10 @@ impl GotocHook for IsAllocated { let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer()); let target = target.unwrap(); let loc = gcx.codegen_caller_span_stable(span); - let ret_place = - unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to)); + let ret_place = unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ); let ret_type = ret_place.goto_expr.typ().clone(); Stmt::block( @@ -262,8 +264,10 @@ impl GotocHook for PointerObject { let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer()); let target = target.unwrap(); let loc = gcx.codegen_caller_span_stable(span); - let ret_place = - unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to)); + let ret_place = unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ); let ret_type = ret_place.goto_expr.typ().clone(); Stmt::block( @@ -296,8 +300,10 @@ impl GotocHook for PointerOffset { let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer()); let target = target.unwrap(); let loc = gcx.codegen_caller_span_stable(span); - let ret_place = - unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to)); + let ret_place = unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ); let ret_type = ret_place.goto_expr.typ().clone(); Stmt::block( @@ -336,7 +342,7 @@ impl GotocHook for RustAlloc { vec![ unwrap_or_return_codegen_unimplemented_stmt!( gcx, - gcx.codegen_place_stable(assign_to) + gcx.codegen_place_stable(assign_to, loc) ) .goto_expr .assign( @@ -396,13 +402,14 @@ impl GotocHook for MemCmp { let is_first_ok = first_var.clone().is_nonnull(); let is_second_ok = second_var.clone().is_nonnull(); let should_skip_pointer_checks = is_count_zero.and(is_first_ok).and(is_second_ok); - let place_expr = - unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to)) - .goto_expr; + let place_expr = unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ) + .goto_expr; let rhs = should_skip_pointer_checks.ternary( Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned) - gcx.codegen_func_expr(instance, Some(span)) - .call(vec![first_var, second_var, count_var]), + gcx.codegen_func_expr(instance, loc).call(vec![first_var, second_var, count_var]), ); let code = place_expr.assign(rhs, loc).with_location(loc); Stmt::block( @@ -447,7 +454,7 @@ impl GotocHook for UntrackedDeref { vec![Stmt::assign( unwrap_or_return_codegen_unimplemented_stmt!( gcx, - gcx.codegen_place_stable(assign_to) + gcx.codegen_place_stable(assign_to, loc) ) .goto_expr, fargs.pop().unwrap().dereference(), diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 7e4fffe428124..4f32028b58661 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -162,7 +162,7 @@ enum CoverageStatus { const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani"; const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop"; const UNWINDING_ASSERT_REC_DESC: &str = "recursion unwinding assertion"; -const DEFAULT_ASSERTION: &str = "assertion"; +const UNDEFINED_FUNCTION_DESC: &str = "undefined function should be unreachable"; impl ParserItem { /// Determines if an item must be skipped or not. @@ -618,8 +618,7 @@ fn modify_undefined_function_checks(mut properties: Vec) -> (Vec