diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 4031d08fa9aa..b6ad7a041d11 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -627,6 +627,34 @@ impl Expr { expr!(IntConstant(i), typ) } + pub fn ssize_constant(i: i128, symbol_table: &SymbolTable) -> Self { + match symbol_table.machine_model().pointer_width { + 32 => { + let val = BigInt::from(i as i32); + expr!(IntConstant(val), Type::ssize_t()) + } + 64 => { + let val = BigInt::from(i as i64); + expr!(IntConstant(val), Type::ssize_t()) + } + i => unreachable!("Expected 32 or 64 bits pointer width, but got `{i}`"), + } + } + + pub fn size_constant(i: u128, symbol_table: &SymbolTable) -> Self { + match symbol_table.machine_model().pointer_width { + 32 => { + let val = BigInt::from(i as u32); + expr!(IntConstant(val), Type::size_t()) + } + 64 => { + let val = BigInt::from(i as u64); + expr!(IntConstant(val), Type::size_t()) + } + i => unreachable!("Expected 32 or 64 bits pointer width, but got `{i}`"), + } + } + pub fn typecheck_call(function: &Expr, arguments: &[Expr]) -> bool { // For variadic functions, all named arguments must match the type of their formal param. // Extra arguments (e.g the ... args) can have any type. 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 61ab4f97bfe8..617eeb8af506 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -16,7 +16,9 @@ use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; use cbmc::{InternString, InternedString}; use lazy_static::lazy_static; use rustc_middle::ty::Instance; +use rustc_smir::rustc_internal; use rustc_target::abi::call::Conv; +use stable_mir::mir::mono::Instance as InstanceStable; use tracing::{debug, trace}; lazy_static! { @@ -44,8 +46,9 @@ impl<'tcx> GotocCtx<'tcx> { /// /// For other foreign items, we declare a shim and add to the list of foreign shims to be /// handled later. - pub fn codegen_foreign_fn(&mut self, instance: Instance<'tcx>) -> &Symbol { + pub fn codegen_foreign_fn(&mut self, instance: InstanceStable) -> &Symbol { debug!(?instance, "codegen_foreign_function"); + let instance = rustc_internal::internal(instance); let fn_name = self.symbol_name(instance).intern(); if self.symbol_table.contains(fn_name) { // Symbol has been added (either a built-in CBMC function or a Rust allocation function). diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 11e4721dfb31..88aecf947975 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -12,6 +12,7 @@ use rustc_middle::mir::{BasicBlock, Operand, Place}; use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement}; use rustc_middle::ty::{self, Ty}; use rustc_middle::ty::{Instance, InstanceDef}; +use rustc_smir::rustc_internal; use rustc_span::Span; use tracing::debug; @@ -233,14 +234,14 @@ impl<'tcx> GotocCtx<'tcx> { // Intrinsics which encode a value known during compilation macro_rules! codegen_intrinsic_const { () => {{ - let value = self - .tcx - .const_eval_instance(ty::ParamEnv::reveal_all(), instance, span) - .unwrap(); + let place = rustc_internal::stable(p); + let place_ty = self.place_ty_stable(&place); + let stable_instance = rustc_internal::stable(instance); + 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 e = self.codegen_const_value(value, self.place_ty(p), span.as_ref()); - self.codegen_expr_to_place(p, e) + let e = self.codegen_allocation(&alloc, place_ty, rustc_internal::stable(span)); + self.codegen_expr_to_place_stable(&place, e) }}; } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 3339a1419f4a..0f2e0ad609f4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -1,26 +1,31 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::codegen_cprover_gotoc::codegen::ty_stable::StableConverter; use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented; -use cbmc::btree_string_map; use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type}; -use rustc_ast::ast::Mutability; -use rustc_middle::mir::interpret::{read_target_uint, AllocId, Allocation, GlobalAlloc, Scalar}; -use rustc_middle::mir::{Const as mirConst, ConstOperand, ConstValue, Operand, UnevaluatedConst}; -use rustc_middle::ty::layout::LayoutOf; -use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy}; +use rustc_middle::mir::Operand as OperandInternal; +use rustc_middle::ty::{Const as ConstInternal, Instance as InstanceInternal}; use rustc_smir::rustc_internal; use rustc_span::def_id::DefId; -use rustc_span::Span; -use rustc_target::abi::{Size, TagEncoding, Variants}; -use stable_mir::mir::mono::Instance as InstanceStable; -use stable_mir::ty::{FnDef, GenericArgs, Span as SpanStable}; +use rustc_span::Span as SpanInternal; +use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; +use stable_mir::mir::mono::{Instance, StaticDef}; +use stable_mir::mir::Operand; +use stable_mir::ty::{ + Allocation, Const, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, RigidTy, Size, Span, Ty, + TyKind, UintTy, +}; use stable_mir::CrateDef; use tracing::{debug, trace}; +#[derive(Clone, Debug)] enum AllocData<'a> { - Bytes(&'a [u8]), + /// The data is represented as a slice of optional bytes, where None represents uninitialized + /// bytes. + Bytes(&'a [Option]), + /// The allocation has been translated to an expression. Expr(Expr), } @@ -30,141 +35,219 @@ impl<'tcx> GotocCtx<'tcx> { /// A MIR operand is either a constant (literal or `const` declaration) or a place /// (being moved or copied for this operation). /// An "operand" in MIR is the argument to an "Rvalue" (and is also used by some statements.) - pub fn codegen_operand(&mut self, o: &Operand<'tcx>) -> Expr { - trace!(operand=?o, "codegen_operand"); - match o { - Operand::Copy(d) | Operand::Move(d) => + pub fn codegen_operand(&mut self, operand: &OperandInternal<'tcx>) -> Expr { + self.codegen_operand_stable(&StableConverter::convert_operand(self, operand.clone())) + } + + pub fn codegen_operand_stable(&mut self, operand: &Operand) -> Expr { + trace!(?operand, "codegen_operand"); + match operand { + 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(d)); + unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place)); // 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/kani/issues/277 - match self.operand_ty(o).kind() { - ty::Dynamic(..) => projection.fat_ptr_goto_expr.unwrap(), + match self.operand_ty_stable(operand).kind() { + TyKind::RigidTy(RigidTy::Dynamic(..)) => projection.fat_ptr_goto_expr.unwrap(), _ => projection.goto_expr, } } - Operand::Constant(c) => self.codegen_constant(c), - } - } - - /// Generate a goto expression from a MIR constant operand. - /// - /// There are three possibile constants: - /// 1. `Ty` means e.g. that it's a const generic parameter. (See `codegen_const`) - /// 2. `Val` means it's a constant value of various kinds. (See `codegen_const_value`) - /// 3. `Unevaluated` means we need to run the interpreter, to get a `ConstValue`. (See `codegen_const_unevaluated`) - fn codegen_constant(&mut self, c: &ConstOperand<'tcx>) -> Expr { - trace!(constant=?c, "codegen_constant"); - let span = Some(&c.span); - match self.monomorphize(c.const_) { - mirConst::Ty(ct) => self.codegen_const(ct, span), - mirConst::Val(val, ty) => self.codegen_const_value(val, ty, span), - mirConst::Unevaluated(unevaluated, ty) => { - self.codegen_const_unevaluated(unevaluated, ty, span) + Operand::Constant(constant) => { + self.codegen_const(&constant.literal, Some(constant.span)) } } } - /// Runs the interpreter to get a `ConstValue`, then call `codegen_const_value` - fn codegen_const_unevaluated( + pub fn codegen_const_internal( &mut self, - unevaluated: UnevaluatedConst<'tcx>, - ty: Ty<'tcx>, - span: Option<&Span>, + constant: ConstInternal<'tcx>, + span: Option, ) -> Expr { - debug!(?unevaluated, "codegen_const_unevaluated"); - let const_val = - self.tcx.const_eval_resolve(ty::ParamEnv::reveal_all(), unevaluated, None).unwrap(); - self.codegen_const_value(const_val, ty, span) + let stable_const = StableConverter::convert_constant(self, constant); + let stable_span = rustc_internal::stable(span); + self.codegen_const(&stable_const, stable_span) } - /// Generate a goto expression from a MIR `Const`. - /// - /// `Const` are special constant values that (only?) come from the type system, - /// and consequently only need monomorphization to produce a value. + /// Generate a goto expression that represents a constant. /// - /// Not to be confused with the more general MIR `Constant` which may need interpretation. - pub fn codegen_const(&mut self, lit: Const<'tcx>, span: Option<&Span>) -> Expr { - debug!("found literal: {:?}", lit); - let lit = self.monomorphize(lit); - - match lit.kind() { - // A `ConstantKind::Ty(ConstKind::Unevaluated)` should no longer show up - // and should be a `ConstantKind::Unevaluated` instead (and thus handled - // at the level of `codegen_constant` instead of `codegen_const`.) - ConstKind::Unevaluated(_) => unreachable!(), - - ConstKind::Value(valtree) => { - let value = self.tcx.valtree_to_const_val((lit.ty(), valtree)); - debug!("The literal was a ConstValue {:?}", value); - self.codegen_const_value(value, lit.ty(), span) + /// There are two possible constants included in the body of an instance: + /// - Allocated: It will have its byte representation already defined. We try to eagerly + /// 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. + fn codegen_const(&mut self, constant: &Const, span: Option) -> Expr { + trace!(?constant, "codegen_constant"); + match constant.kind() { + ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), span), + 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) + } + _ => Expr::init_unit(self.codegen_ty_stable(lit_ty), &self.symbol_table), + } } - _ => { - unreachable!( - "monomorphized item shouldn't have this constant value: {:?}", - lit.kind() - ) + ConstantKind::Param(..) | ConstantKind::Unevaluated(..) => { + unreachable!() } } } - /// Generate a goto expression from a MIR `ConstValue`. + pub fn codegen_allocation(&mut self, alloc: &Allocation, ty: Ty, span: Option) -> Expr { + // First try to generate the constant without allocating memory. + let expr = self.try_codegen_constant(alloc, ty, span).unwrap_or_else(|| { + debug!("codegen_allocation try_fail"); + let mem_var = self.codegen_const_allocation(alloc, None); + mem_var + .cast_to(Type::unsigned_int(8).to_pointer()) + .cast_to(self.codegen_ty_stable(ty).to_pointer()) + .dereference() + }); + debug!(?expr, ?alloc, ?ty, "codegen_allocation"); + expr + } + + /// Before allocating space for a constant, try to generate a simple expression. /// - /// A `ConstValue` is the result of evaluation of a constant (of various original forms). - /// All forms of constant code generation ultimately land here, where we have an actual value - /// that we now just need to translate based on its kind. - pub fn codegen_const_value( + /// Generate an expression for a constant too small/simple to require an `Allocation` such as: + /// 1. integers + /// 2. ZST, or transparent structs of one (scalar) value + /// 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, - v: ConstValue<'tcx>, - lit_ty: Ty<'tcx>, - span: Option<&Span>, - ) -> Expr { - trace!(val=?v, ?lit_ty, "codegen_const_value"); - match v { - ConstValue::Scalar(s) => self.codegen_scalar(s, lit_ty, span), - ConstValue::Slice { data, meta } => { - self.codegen_slice_value(v, lit_ty, span, data.inner(), meta.try_into().unwrap()) + alloc: &Allocation, + ty: Ty, + span: Option, + ) -> Option { + debug!(?alloc, ?ty, "try_codegen_constant"); + match ty.kind() { + TyKind::RigidTy(RigidTy::Int(it)) => { + let val = alloc.read_int().unwrap(); + Some(match it { + IntTy::Isize => Expr::ssize_constant(val, &self.symbol_table), + IntTy::I8 => Expr::int_constant(val as i8, Type::signed_int(8)), + IntTy::I16 => Expr::int_constant(val as i16, Type::signed_int(16)), + IntTy::I32 => Expr::int_constant(val as i32, Type::signed_int(32)), + IntTy::I64 => Expr::int_constant(val as i64, Type::signed_int(64)), + IntTy::I128 => Expr::int_constant(val, Type::signed_int(128)), + }) + } + TyKind::RigidTy(RigidTy::Uint(it)) => { + let val = alloc.read_uint().unwrap(); + Some(match it { + UintTy::Usize => Expr::size_constant(val, &self.symbol_table), + UintTy::U8 => Expr::int_constant(val as u8, Type::unsigned_int(8)), + UintTy::U16 => Expr::int_constant(val as u16, Type::unsigned_int(16)), + UintTy::U32 => Expr::int_constant(val as u32, Type::unsigned_int(32)), + UintTy::U64 => Expr::int_constant(val as u64, Type::unsigned_int(64)), + UintTy::U128 => Expr::int_constant(val, Type::unsigned_int(128)), + }) + } + TyKind::RigidTy(RigidTy::Bool) => { + Some(Expr::c_bool_constant(alloc.read_bool().unwrap())) + } + TyKind::RigidTy(RigidTy::Char) => { + Some(Expr::int_constant(alloc.read_int().unwrap(), Type::signed_int(32))) + } + TyKind::RigidTy(RigidTy::Float(k)) => + // rustc uses a sophisticated format for floating points that is hard to get f32/f64 from. + // Instead, we use integers with the right width to represent the bit pattern. + { + match k { + FloatTy::F32 => Some(Expr::float_constant_from_bitpattern( + alloc.read_uint().unwrap() as u32, + )), + FloatTy::F64 => Some(Expr::double_constant_from_bitpattern( + alloc.read_uint().unwrap() as u64, + )), + } + } + TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) + | TyKind::RigidTy(RigidTy::Ref(_, inner_ty, _)) => { + Some(self.codegen_const_ptr(alloc, ty, inner_ty, span)) + } + TyKind::RigidTy(RigidTy::Adt(adt, args)) if adt.kind().is_struct() => { + // Structs only have one variant. + let variant = adt.variants_iter().next().unwrap(); + // There must be at least one field associated with the scalar data. + // Any additional fields correspond to ZSTs. + let field_types: Vec<_> = + variant.fields().iter().map(|f| f.ty_with_args(&args)).collect(); + // Check that there is a single non-ZST field. + let non_zst_types: Vec<_> = + field_types.iter().filter(|t| !self.is_zst_stable(**t)).collect(); + debug!(len=?non_zst_types.len(), "non_zst_types"); + if non_zst_types.len() == 1 { + // Only try to directly expand the constant if only one field has data. + // We could eventually expand this, but keep it simple for now. See: + // https://github.com/model-checking/kani/issues/2936 + let overall_type = self.codegen_ty_stable(ty); + let field_values: Vec = field_types + .iter() + .map(|t| { + if self.is_zst_stable(*t) { + Some(Expr::init_unit( + self.codegen_ty_stable(*t), + &self.symbol_table, + )) + } else { + self.try_codegen_constant(alloc, *t, span) + } + }) + .collect::>>()?; + Some(Expr::struct_expr_from_values( + overall_type, + field_values, + &self.symbol_table, + )) + } else { + // Structures with more than one non-ZST element are handled with an extra + // allocation. + None + } } - ConstValue::Indirect { alloc_id, offset } => { - let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory(); - debug!("ConstValue by ref {:?} {:?}", alloc, offset); - let mem_var = self.codegen_const_allocation(alloc.inner(), None); - mem_var - .cast_to(Type::unsigned_int(8).to_pointer()) - .plus(Expr::int_constant(offset.bytes(), Type::unsigned_int(64))) - .cast_to(self.codegen_ty(lit_ty).to_pointer()) - .dereference() + 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)?; + Some(inner_expr.transmute_to(overall_t, &self.symbol_table)) } - ConstValue::ZeroSized => match lit_ty.kind() { - // Rust "function items" (not closures, not function pointers, see `codegen_fndef`) - ty::FnDef(d, args) => self.codegen_fndef(*d, args, span), - _ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table), - }, + // Everything else we encode as an allocation. + _ => None, } } - /// Generate a goto expression from a MIR `ConstValue::Slice`. - /// - /// A constant slice is an internal reference to another constant allocation. - fn codegen_slice_value( + fn codegen_const_ptr( &mut self, - v: ConstValue<'tcx>, - lit_ty: Ty<'tcx>, - span: Option<&Span>, - data: &'tcx Allocation, - size: usize, + alloc: &Allocation, + ty: Ty, + inner_ty: Ty, + span: Option, ) -> Expr { - if let ty::Ref(_, ref_ty, _) = lit_ty.kind() { - match ref_ty.kind() { - ty::Str => { + debug!(?ty, ?alloc, "codegen_const_ptr"); + if self.use_fat_pointer_stable(inner_ty) { + match inner_ty.kind() { + TyKind::RigidTy(RigidTy::Str) => { // a string literal // Create a static variable that holds its value - let mem_var = self.codegen_const_allocation(data, None); + assert_eq!( + alloc.provenance.ptrs.len(), + 1, + "Expected `&str` to point to a str buffer" + ); + let alloc_id = alloc.provenance.ptrs[0].1.0; + let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else { + unreachable!() + }; + let mem_var = self.codegen_const_allocation(&data, None); // Extract identifier for static variable. // codegen_allocation_auto_imm_name returns the *address* of @@ -178,279 +261,59 @@ impl<'tcx> GotocCtx<'tcx> { }; // Extract the actual string literal - let slice = data.inspect_with_uninit_and_ptr_outside_interpreter(0..size); - let s = ::std::str::from_utf8(slice).expect("non utf8 str from miri"); + let bytes = data.raw_bytes().unwrap(); + let s = ::std::str::from_utf8(&bytes).expect("non utf8 str from mir"); // Store the identifier to the string literal in the goto context self.str_literals.insert(*ident, s.into()); // Codegen as a fat pointer let data_expr = mem_var.cast_to(Type::unsigned_int(8).to_pointer()); - let len_expr = Expr::int_constant(size, Type::size_t()); - return slice_fat_ptr( - self.codegen_ty(lit_ty), + let len_expr = Expr::int_constant(bytes.len(), Type::size_t()); + slice_fat_ptr( + self.codegen_ty_stable(ty), data_expr, len_expr, &self.symbol_table, - ); - } - ty::Slice(slice_ty) => { - if let Uint(UintTy::U8) = slice_ty.kind() { - let mem_var = self.codegen_const_allocation(data, None); - let slice = data.inspect_with_uninit_and_ptr_outside_interpreter(0..size); - let len = slice.len(); - let data_expr = mem_var.cast_to(Type::unsigned_int(8).to_pointer()); - let len_expr = Expr::int_constant(len, Type::size_t()); - return slice_fat_ptr( - self.codegen_ty(lit_ty), - data_expr, - len_expr, - &self.symbol_table, - ); - } else { - // TODO: Handle cases with other types such as tuples and larger integers. - let loc = self.codegen_span_option(span.cloned()); - let typ = self.codegen_ty(lit_ty); - let operation_name = format!("Constant slice for type {slice_ty}"); - return self.codegen_unimplemented_expr( - &operation_name, - typ, - loc, - "https://github.com/model-checking/kani/issues/1339", - ); - } - } - ty::Adt(def, _) if Some(def.did()) == self.tcx.lang_items().c_str() => { - // TODO: Handle CString - // - let loc = self.codegen_span_option(span.cloned()); - let typ = self.codegen_ty(lit_ty); - let operation_name = "C string literal"; - return self.codegen_unimplemented_expr( - &operation_name, - typ, - loc, - "https://github.com/model-checking/kani/issues/2549", - ); - } - _ => {} - } - } - unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty.kind(), span); - } - - /// Generate a goto expression from a MIR `ConstValue::Scalar`. - /// - /// A `Scalar` is a constant too small/simple to require an `Allocation` such as: - /// 1. integers - /// 2. ZST, or transparent structs of one (scalar) value - /// 3. enums that don't carry data - /// 4. unit, tuples (may be multi-ary!), or size-0 arrays - /// 5. pointers to an allocation - fn codegen_scalar(&mut self, s: Scalar, ty: Ty<'tcx>, span: Option<&Span>) -> Expr { - debug!(scalar=?s, ?ty, kind=?ty.kind(), ?span, "codegen_scalar"); - match (s, &ty.kind()) { - (Scalar::Int(_), ty::Int(it)) => match it { - IntTy::I8 => Expr::int_constant(s.to_i8().unwrap(), Type::signed_int(8)), - IntTy::I16 => Expr::int_constant(s.to_i16().unwrap(), Type::signed_int(16)), - IntTy::I32 => Expr::int_constant(s.to_i32().unwrap(), Type::signed_int(32)), - IntTy::I64 => Expr::int_constant(s.to_i64().unwrap(), Type::signed_int(64)), - IntTy::I128 => Expr::int_constant(s.to_i128().unwrap(), Type::signed_int(128)), - IntTy::Isize => { - Expr::int_constant(s.to_target_isize(self).unwrap(), Type::ssize_t()) - } - }, - (Scalar::Int(_), ty::Uint(it)) => match it { - UintTy::U8 => Expr::int_constant(s.to_u8().unwrap(), Type::unsigned_int(8)), - UintTy::U16 => Expr::int_constant(s.to_u16().unwrap(), Type::unsigned_int(16)), - UintTy::U32 => Expr::int_constant(s.to_u32().unwrap(), Type::unsigned_int(32)), - UintTy::U64 => Expr::int_constant(s.to_u64().unwrap(), Type::unsigned_int(64)), - UintTy::U128 => Expr::int_constant(s.to_u128().unwrap(), Type::unsigned_int(128)), - UintTy::Usize => { - Expr::int_constant(s.to_target_usize(self).unwrap(), Type::size_t()) - } - }, - (Scalar::Int(_), ty::Bool) => Expr::c_bool_constant(s.to_bool().unwrap()), - (Scalar::Int(_), ty::Char) => { - Expr::int_constant(s.to_i32().unwrap(), Type::signed_int(32)) - } - (Scalar::Int(_), ty::Float(k)) => - // rustc uses a sophisticated format for floating points that is hard to get f32/f64 from. - // Instead, we use integers with the right width to represent the bit pattern. - { - match k { - FloatTy::F32 => Expr::float_constant_from_bitpattern(s.to_u32().unwrap()), - FloatTy::F64 => Expr::double_constant_from_bitpattern(s.to_u64().unwrap()), + ) } - } - (Scalar::Int(..), ty::FnDef(..)) => { - // This was removed here: https://github.com/rust-lang/rust/pull/98957. - unreachable!("ZST is no longer represented as a scalar") - } - (Scalar::Int(_), ty::RawPtr(tm)) => { - Expr::int_constant(s.to_u64().unwrap(), Type::unsigned_int(64)) - .cast_to(self.codegen_ty(tm.ty).to_pointer()) - } - // TODO: Removing this doesn't cause any regressions to fail. - // We need a regression for this case. - (Scalar::Int(int), ty::Ref(_, ty, _)) => { - if int.is_null() { - self.codegen_ty(*ty).to_pointer().null() - } else { - unreachable!() - } - } - (Scalar::Int(_), ty::Adt(adt, subst)) => { - if adt.is_struct() { - // In this case, we must have a one variant ADT. - let variant = adt.non_enum_variant(); - let overall_type = self.codegen_ty(ty); - // There must be at least one field associated with the scalar data. - // Any additional fields correspond to ZSTs. - let field_types: Vec> = - variant.fields.iter().map(|f| f.ty(self.tcx, subst)).collect(); - // Check that there is a single non-ZST field. - let non_zst_types: Vec<_> = - field_types.iter().filter(|t| !self.is_zst(**t)).collect(); - assert!( - non_zst_types.len() == 1, - "error: expected exactly one field whose type is not a ZST" + TyKind::RigidTy(RigidTy::Slice(inner_ty)) => { + // Create a static variable that holds its value + assert_eq!( + alloc.provenance.ptrs.len(), + 1, + "Expected `&[T]` to point to a single buffer" ); - let field_values: Vec = field_types - .iter() - .map(|t| { - if self.is_zst(*t) { - Expr::init_unit(self.codegen_ty(*t), &self.symbol_table) - } else { - self.codegen_scalar(s, *t, span) - } - }) - .collect(); - Expr::struct_expr_from_values(overall_type, field_values, &self.symbol_table) - } else if adt.is_enum() { - let layout = self.layout_of(ty); - let overall_t = self.codegen_ty(ty); - match &layout.variants { - Variants::Single { index } => { - // here we must have one variant - let variant = &adt.variants()[*index]; - match variant.fields.len() { - 0 => Expr::struct_expr_from_values( - overall_t, - vec![], - &self.symbol_table, - ), - 1 => { - let fty = variant.fields[0usize.into()].ty(self.tcx, subst); - self.codegen_single_variant_single_field( - s, span, overall_t, fty, - ) - } - _ => unreachable!(), - } - } - Variants::Multiple { tag_encoding, tag_field, .. } => match tag_encoding { - TagEncoding::Niche { .. } => { - let niche_offset = layout.fields.offset(*tag_field); - assert_eq!( - niche_offset, - Size::ZERO, - "nonzero offset for niche in scalar" - ); - let discr_ty = self.codegen_enum_discr_typ(ty); - let niche_val = self.codegen_scalar(s, discr_ty, span); - let result_type = self.codegen_ty(ty); - let niche_type = niche_val.typ().clone(); - assert_eq!( - niche_type.sizeof_in_bits(&self.symbol_table), - result_type.sizeof_in_bits(&self.symbol_table), - "niche type and enum have different size in scalar" - ); - niche_val.transmute_to(result_type, &self.symbol_table) - } - - TagEncoding::Direct => { - // then the scalar field stores the discriminant - let discr_ty = self.codegen_enum_discr_typ(ty); - let init = self.codegen_scalar(s, discr_ty, span); - let cgt = self.codegen_ty(ty); - let fields = - cgt.get_non_empty_components(&self.symbol_table).unwrap(); - // TagEncoding::Direct makes a constant with a tag but no data. - // Check our understanding that that the Enum must have one field, - // which is the tag, and no data field. - assert_eq!( - fields.len(), - 1, - "TagEncoding::Direct encountered for enum with non-empty variants" - ); - assert_eq!( - fields[0].name().to_string(), - "case", - "Unexpected field in enum/coroutine. Please report your failing case at https://github.com/model-checking/kani/issues/1465" - ); - Expr::struct_expr_with_nondet_fields( - cgt, - btree_string_map![("case", init)], - &self.symbol_table, - ) - } - }, - } - } else { - // if it's a union - unimplemented!() + let alloc_id = alloc.provenance.ptrs[0].1.0; + let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else { + unreachable!() + }; + let mem_var = self.codegen_const_allocation(&data, None); + 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()); + let len_expr = Expr::int_constant(len, Type::size_t()); + slice_fat_ptr( + self.codegen_ty_stable(ty), + data_expr, + len_expr, + &self.symbol_table, + ) } + _ => unreachable!("{inner_ty:?}"), } - (Scalar::Int(int), ty::Tuple(_)) => { - // A ScalarInt has a u128-typed data field, so the result can never be larger than - // that and the conversion to a uint (of an actual size that may be smaller than - // 128 bits) will succeed. - let int_u128 = int.try_to_uint(int.size()).ok().unwrap(); - let overall_t = self.codegen_ty(ty); - let expr_int = Expr::int_constant( - int_u128, - Type::unsigned_int(overall_t.sizeof_in_bits(&self.symbol_table)), - ); - expr_int.transmute_to(overall_t, &self.symbol_table) - } - (_, ty::Array(_, _)) => { - let typ = self.codegen_ty(ty); - // we must have zero size array here - Expr::struct_expr_from_values( - typ.clone(), - vec![Expr::array_expr(typ, vec![])], - &self.symbol_table, - ) - } - (Scalar::Ptr(ptr, _size), _) => { - let res_t = self.codegen_ty(ty); - let (prov, offset) = ptr.into_parts(); - let alloc_id = prov.alloc_id(); - self.codegen_alloc_pointer(res_t, alloc_id, offset, span) - } - _ => unimplemented!(), - } - } - - /// A private helper for `codegen_scalar`. Many "scalars" are more complex types, but get treated as scalars - /// because they only have one (small) field. We still translated them as struct types, however. - fn codegen_single_variant_single_field( - &mut self, - s: Scalar, - span: Option<&Span>, - overall_t: Type, - fty: Ty<'tcx>, - ) -> Expr { - if fty.is_unit() { - // TODO: It's not clear if this case is reachable. It's not covered by our test suite at least. - Expr::struct_expr_from_values(overall_t, vec![], &self.symbol_table) + } else if !alloc.provenance.ptrs.is_empty() { + // Codegen the provenance pointer. + trace!("codegen_const_ptr with_prov"); + 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) } else { - Expr::struct_expr_from_values( - overall_t, - vec![self.codegen_scalar(s, fty, span)], - &self.symbol_table, - ) + // If there's no provenance, just codegen the pointer address. + trace!("codegen_const_ptr no_prov"); + let expr = Expr::size_constant(alloc.read_uint().unwrap(), &self.symbol_table); + expr.cast_to(self.codegen_ty_stable(ty)) } } @@ -461,34 +324,37 @@ impl<'tcx> GotocCtx<'tcx> { res_t: Type, alloc_id: AllocId, offset: Size, - span: Option<&Span>, + span: Option, ) -> Expr { - let base_addr = match self.tcx.global_alloc(alloc_id) { + 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() } - GlobalAlloc::Static(def_id) => self.codegen_static_pointer(def_id, false), + GlobalAlloc::Static(def) => self.codegen_static_pointer(def), GlobalAlloc::Memory(alloc) => { // Full (mangled) crate name added so that allocations from different // 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.inner(), Some(name)) + self.codegen_const_allocation(&alloc, Some(name)) } - GlobalAlloc::VTable(ty, trait_ref) => { + alloc @ GlobalAlloc::VTable(..) => { // This is similar to GlobalAlloc::Memory but the type is opaque to rust and it // requires a bit more logic to get information about the allocation. - let alloc_id = self.tcx.vtable_allocation((ty, trait_ref)); - let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory(); + let vtable_alloc_id = alloc.vtable_allocation().unwrap(); + let GlobalAlloc::Memory(alloc) = GlobalAlloc::from(vtable_alloc_id) else { + unreachable!() + }; let name = format!("{}::{alloc_id:?}", self.full_crate_name()); - self.codegen_const_allocation(alloc.inner(), Some(name)) + self.codegen_const_allocation(&alloc, Some(name)) } }; assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table)); let offset_addr = base_addr .cast_to(Type::unsigned_int(8).to_pointer()) - .plus(Expr::int_constant(offset.bytes(), Type::unsigned_int(64))); + .plus(Expr::int_constant(offset, Type::unsigned_int(64))); // In some cases, Rust uses a transparent type here. Convert the pointer to an rvalue // of the type expected. https://github.com/model-checking/kani/issues/822 @@ -503,13 +369,24 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Generate a goto expression for a pointer to a static or thread-local variable. + /// Generate a goto expression for a pointer to a static. /// /// These are not initialized here, see `codegen_static`. - pub fn codegen_static_pointer(&mut self, def_id: DefId, is_thread_local: bool) -> Expr { - let instance = Instance::mono(self.tcx, def_id); + fn codegen_static_pointer(&mut self, def: StaticDef) -> Expr { + self.codegen_instance_pointer(Instance::from(def), false) + } - let sym = self.ensure(&self.symbol_name(instance), |ctx, name| { + /// Generate a goto expression for a pointer to a thread-local variable. + /// + /// These are not initialized here, see `codegen_static`. + pub fn codegen_thread_local_pointer(&mut self, def_id: DefId) -> Expr { + let instance = rustc_internal::stable(InstanceInternal::mono(self.tcx, def_id)); + self.codegen_instance_pointer(instance, true) + } + + /// Generate a goto expression for a pointer to a static or thread-local variable. + fn codegen_instance_pointer(&mut self, instance: Instance, is_thread_local: bool) -> Expr { + let sym = self.ensure(&instance.mangled_name(), |ctx, name| { // Rust has a notion of "extern static" variables. These are in an "extern" block, // and so aren't initialized in the current codegen unit. For example (from std): // extern "C" { @@ -525,14 +402,14 @@ impl<'tcx> GotocCtx<'tcx> { // 1. If they are `is_extern` they are nondet-initialized. // 2. If they are `!is_extern`, they are zero-initialized. // So we recognize a Rust "extern" declaration and pass that information along. - let is_extern = ctx.tcx.is_foreign_item(def_id); + let is_extern = instance.is_foreign_item(); - let span = ctx.tcx.def_span(def_id); + let span = instance.def.span(); Symbol::static_variable( name.to_string(), name.to_string(), - ctx.codegen_ty(instance.ty(ctx.tcx, ty::ParamEnv::reveal_all())), - ctx.codegen_span(&span), + ctx.codegen_ty_stable(instance.ty()), + ctx.codegen_span_stable(span), ) .with_is_extern(is_extern) .with_is_thread_local(is_thread_local) @@ -547,20 +424,18 @@ 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: &'tcx Allocation, name: Option) -> Expr { + fn codegen_const_allocation(&mut self, alloc: &Allocation, name: Option) -> Expr { debug!(?name, "codegen_const_allocation"); - assert_eq!( - alloc.mutability, - Mutability::Not, - "Expected constant allocation for `{name:?}`, but got a mutable instead" - ); - if !self.alloc_map.contains_key(&alloc) { - let name = if let Some(name) = name { name } else { self.next_global_name() }; - self.codegen_alloc_in_memory(alloc, name); - } + 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()); + alloc_name + } + Some(name) => name.clone(), + }; - let mem_place = - self.symbol_table.lookup(self.alloc_map.get(&alloc).unwrap()).unwrap().to_expr(); + let mem_place = self.symbol_table.lookup(alloc_name).unwrap().to_expr(); mem_place.address_of() } @@ -569,8 +444,8 @@ 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: &'tcx Allocation, name: String) { - debug!("codegen_alloc_in_memory name: {}", name); + pub fn codegen_alloc_in_memory(&mut self, alloc: Allocation, name: String) { + debug!(?alloc, ?name, "codegen_alloc_in_memory"); let struct_name = &format!("{name}::struct"); // The declaration of a static variable may have one type and the constant initializer for @@ -578,8 +453,9 @@ 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_typ_ref = self.ensure_struct(struct_name, struct_name, |ctx, _| { - ctx.codegen_allocation_data(alloc) + let alloc_data = self.codegen_allocation_data(&alloc); + let alloc_typ_ref = self.ensure_struct(struct_name, struct_name, |_, _| { + alloc_data .iter() .enumerate() .map(|(i, d)| match d { @@ -607,7 +483,6 @@ impl<'tcx> GotocCtx<'tcx> { // Assign the initial value `val` to `var` via an intermediate `temp_var` to allow for // transmuting the allocation type to the global static variable type. - let alloc_data = self.codegen_allocation_data(alloc); let val = Expr::struct_expr_from_values( alloc_typ_ref.clone(), alloc_data @@ -617,7 +492,9 @@ impl<'tcx> GotocCtx<'tcx> { Type::unsigned_int(8).array_of(bytes.len()), bytes .iter() - .map(|b| Expr::int_constant(*b, Type::unsigned_int(8))) + // We should consider adding a poison / undet where we have none + // This mimics the behaviour before StableMIR though. + .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8))) .collect(), ), AllocData::Expr(e) => e.clone(), @@ -639,45 +516,34 @@ impl<'tcx> GotocCtx<'tcx> { self.alloc_map.insert(alloc, name); } - /// This is an internal helper function for `codegen_alloc_in_memory` and you should understand - /// it by starting there. + /// This is an internal helper function for `codegen_alloc_in_memory`. /// /// 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(&mut self, alloc: &'tcx Allocation) -> Vec> { - let mut alloc_vals = Vec::with_capacity(alloc.provenance().ptrs().len() + 1); - let pointer_size = - Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); - - let mut next_offset = Size::ZERO; - for &(offset, prov) in alloc.provenance().ptrs().iter() { - let alloc_id = prov.alloc_id(); + fn codegen_allocation_data<'a>(&mut self, alloc: &'a Allocation) -> 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(); + + let mut next_offset = 0; + for &(offset, prov) in alloc.provenance.ptrs.iter() { if offset > next_offset { - let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( - next_offset.bytes_usize()..offset.bytes_usize(), - ); + let bytes = &alloc.bytes[next_offset..offset]; alloc_vals.push(AllocData::Bytes(bytes)); } - let ptr_offset = { - let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( - offset.bytes_usize()..(offset + pointer_size).bytes_usize(), - ); - read_target_uint(self.tcx.sess.target.options.endian, bytes) - } - .unwrap(); + let ptr_offset = { alloc.read_partial_uint(offset..(offset + pointer_size)).unwrap() }; alloc_vals.push(AllocData::Expr(self.codegen_alloc_pointer( Type::signed_int(8).to_pointer(), - alloc_id, - Size::from_bytes(ptr_offset), + prov.0, + ptr_offset.try_into().unwrap(), None, ))); next_offset = offset + pointer_size; } - if alloc.len() >= next_offset.bytes_usize() { - let range = next_offset.bytes_usize()..alloc.len(); - let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(range); + if alloc.bytes.len() >= next_offset { + let range = next_offset..alloc.bytes.len(); + let bytes = &alloc.bytes[range]; alloc_vals.push(AllocData::Bytes(bytes)); } @@ -695,46 +561,26 @@ impl<'tcx> GotocCtx<'tcx> { /// function types. /// /// See - pub fn codegen_fndef( - &mut self, - d: DefId, - args: ty::GenericArgsRef<'tcx>, - span: Option<&Span>, - ) -> Expr { - let instance = - Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, args).unwrap().unwrap(); + pub fn codegen_fndef(&mut self, def: FnDef, args: &GenericArgs, span: Option) -> Expr { + let instance = Instance::resolve(def, args).unwrap(); self.codegen_fn_item(instance, span) } - pub fn codegen_fndef_stable( - &mut self, - def: FnDef, - args: &GenericArgs, - span: Option, - ) -> Expr { - let instance = InstanceStable::resolve(def, args) - .expect(&format!("Failed to instantiate `{}` with `{args:?}`", def.name())); - self.codegen_fn_item( - rustc_internal::internal(instance), - rustc_internal::internal(span).as_ref(), - ) - } - /// Ensure that the given instance is in the symbol table, returning the symbol. /// /// FIXME: The function should not have to return the type of the function symbol as well /// because the symbol should have the type. The problem is that the type in the symbol table /// sometimes subtly differs from the type that codegen_function_sig returns. /// This is tracked in . - fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) { - let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance)); - let sym = if self.tcx.is_foreign_item(instance.def_id()) { + fn codegen_func_symbol(&mut self, instance: Instance) -> (&Symbol, Type) { + let funct = self.codegen_function_sig(self.fn_sig_of_instance_stable(instance)); + let sym = if instance.is_foreign_item() { // Get the symbol that represents a foreign instance. self.codegen_foreign_fn(instance) } else { // All non-foreign functions should've been declared beforehand. trace!(func=?instance, "codegen_func_symbol"); - let func = self.symbol_name(instance); + let func = self.symbol_name_stable(instance); self.symbol_table .lookup(&func) .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage")) @@ -747,16 +593,20 @@ 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<'tcx>, span: Option<&Span>) -> Expr { - let (func_symbol, func_typ) = self.codegen_func_symbol(instance); + pub fn codegen_func_expr_internal( + &mut self, + instance: InstanceInternal<'tcx>, + span: Option<&SpanInternal>, + ) -> Expr { + let (func_symbol, func_typ) = self.codegen_func_symbol(rustc_internal::stable(instance)); Expr::symbol_expression(func_symbol.name, func_typ) .with_location(self.codegen_span_option(span.cloned())) } - pub fn codegen_func_expr_stable(&mut self, instance: InstanceStable, span: SpanStable) -> Expr { - let (func_symbol, func_typ) = self.codegen_func_symbol(rustc_internal::internal(instance)); + pub fn codegen_func_expr(&mut self, instance: Instance, span: Option) -> Expr { + let (func_symbol, func_typ) = self.codegen_func_symbol(instance); Expr::symbol_expression(func_symbol.name, func_typ) - .with_location(self.codegen_span_stable(span)) + .with_location(self.codegen_span_option_stable(span)) } /// Generate a goto expression referencing the singleton value for a MIR "function item". @@ -764,19 +614,18 @@ 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<'tcx>, span: Option<&Span>) -> Expr { + fn codegen_fn_item(&mut self, instance: Instance, span: Option) -> Expr { let (func_symbol, _) = self.codegen_func_symbol(instance); let mangled_name = func_symbol.name; - let fn_item_struct_ty = self.codegen_fndef_type(instance); + let fn_item_struct_ty = self.codegen_fndef_type_stable(instance); // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object. let fn_singleton_name = format!("{mangled_name}::FnDefSingleton"); - let fn_singleton = self.ensure_global_var( + self.ensure_global_var( &fn_singleton_name, false, fn_item_struct_ty, - Location::none(), + self.codegen_span_option_stable(span), |_, _| None, // zero-sized, so no initialization necessary - ); - fn_singleton.with_location(self.codegen_span_option(span.cloned())) + ) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 5056d9d006ad..beb35d469391 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -369,7 +369,7 @@ impl<'tcx> GotocCtx<'tcx> { match ty.kind() { // A local that is itself a FnDef, like Fn::call_once TyKind::RigidTy(RigidTy::FnDef(def, args)) => { - Some(self.codegen_fndef_stable(def, &args, None)) + Some(self.codegen_fndef(def, &args, None)) } // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut TyKind::RigidTy(RigidTy::RawPtr(inner, _)) => self diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index e4b550c93591..697a7ba83d2d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -162,7 +162,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_rvalue_len(&mut self, p: &Place<'tcx>) -> Expr { let pt = self.place_ty(p); match pt.kind() { - ty::Array(_, sz) => self.codegen_const(*sz, None), + ty::Array(_, sz) => self.codegen_const_internal(*sz, None), ty::Slice(_) => unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p)) .fat_ptr_goto_expr .unwrap() @@ -761,7 +761,7 @@ impl<'tcx> GotocCtx<'tcx> { Rvalue::ThreadLocalRef(def_id) => { // Since Kani is single-threaded, we treat a thread local like a static variable: self.store_concurrent_construct("thread local (replaced by static variable)", loc); - self.codegen_static_pointer(*def_id, true) + self.codegen_thread_local_pointer(*def_id) } // 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 @@ -1006,7 +1006,7 @@ impl<'tcx> GotocCtx<'tcx> { .unwrap(); // We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs. // (cf. the function documentation) - self.codegen_func_expr(instance, None).address_of() + self.codegen_func_expr_internal(instance, None).address_of() } _ => unreachable!(), }, @@ -1017,7 +1017,7 @@ impl<'tcx> GotocCtx<'tcx> { Instance::resolve_closure(self.tcx, *def_id, args, ty::ClosureKind::FnOnce) .expect("failed to normalize and resolve closure during codegen") .polymorphize(self.tcx); - self.codegen_func_expr(instance, None).address_of() + self.codegen_func_expr_internal(instance, None).address_of() } else { unreachable!("{:?} cannot be cast to a fn ptr", operand) } @@ -1384,7 +1384,7 @@ impl<'tcx> GotocCtx<'tcx> { (ty::Array(src_elt_type, src_elt_count), ty::Slice(dst_elt_type)) => { // Cast to a slice fat pointer. assert_eq!(src_elt_type, dst_elt_type); - let dst_goto_len = self.codegen_const(*src_elt_count, None); + let dst_goto_len = self.codegen_const_internal(*src_elt_count, None); let src_pointee_ty = pointee_type(coerce_info.src_ty).unwrap(); let dst_data_expr = if src_pointee_ty.is_array() { src_goto_expr.cast_to(self.codegen_ty(*src_elt_type).to_pointer()) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 70b00357d264..ac312f1580a9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -27,6 +27,11 @@ impl<'tcx> GotocCtx<'tcx> { Some(loc.end_col), ) } + + 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(&Some(rustc_internal::internal(sp))) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 9ab0cbcc8d98..30a27f231d08 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -18,6 +18,7 @@ use rustc_smir::rustc_internal; use rustc_span::Span; use rustc_target::abi::VariantIdx; use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; +use stable_mir::mir::Place as PlaceStable; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -346,7 +347,7 @@ impl<'tcx> GotocCtx<'tcx> { // Non-virtual, direct drop_in_place call assert!(!matches!(drop_instance.def, InstanceDef::Virtual(_, _))); - let func = self.codegen_func_expr(drop_instance, None); + let func = self.codegen_func_expr_internal(drop_instance, None); // The only argument should be a self reference let args = vec![place_ref]; @@ -567,7 +568,7 @@ impl<'tcx> GotocCtx<'tcx> { | InstanceDef::CloneShim(..) => { // 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_internal(instance, None); vec![ self.codegen_expr_to_place(destination, func_exp.call(fargs)) .with_location(loc), @@ -697,6 +698,16 @@ impl<'tcx> GotocCtx<'tcx> { /// 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_stable(&mut self, p: &PlaceStable, e: Expr) -> Stmt { + if e.typ().is_unit() { + e.as_stmt(Location::none()) + } else { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(p)) + .goto_expr + .assign(e, Location::none()) + } + } + 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()) 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 13e4a5402e06..cf4c6173637b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -5,9 +5,8 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Symbol; -use rustc_hir::def_id::DefId; -use rustc_middle::mir::mono::MonoItem; -use rustc_middle::ty::{GenericArgs, Instance}; +use stable_mir::mir::mono::{Instance, StaticDef}; +use stable_mir::CrateDef; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { @@ -16,24 +15,24 @@ impl<'tcx> GotocCtx<'tcx> { /// Note that each static variable have their own location in memory. Per Rust documentation: /// "statics declare global variables. These represent a memory address." /// Source: - pub fn codegen_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) { + pub fn codegen_static(&mut self, def: StaticDef) { debug!("codegen_static"); - let alloc = self.tcx.eval_static_initializer(def_id).unwrap(); - let symbol_name = item.symbol_name(self.tcx).to_string(); - self.codegen_alloc_in_memory(alloc.inner(), symbol_name); + let alloc = def.eval_initializer().unwrap(); + let symbol_name = Instance::from(def).mangled_name(); + self.codegen_alloc_in_memory(alloc, symbol_name); } /// 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>) { + pub fn declare_static(&mut self, def: StaticDef) { + let instance = Instance::from(def); // Unique mangled monomorphized name. - let symbol_name = item.symbol_name(self.tcx).to_string(); + let symbol_name = instance.mangled_name(); // Pretty name which may include function name. - let pretty_name = Instance::new(def_id, GenericArgs::empty()).to_string(); - debug!(?symbol_name, ?pretty_name, "declare_static {}", item); + let pretty_name = instance.name(); + debug!(?def, ?symbol_name, ?pretty_name, "declare_static"); - let typ = self.codegen_ty(self.tcx.type_of(def_id).instantiate_identity()); - let span = self.tcx.def_span(def_id); - let location = self.codegen_span(&span); + let typ = self.codegen_ty_stable(instance.ty()); + let location = self.codegen_span_stable(def.span()); let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location) .with_is_hidden(false) // Static items are always user defined. .with_pretty_name(pretty_name); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs index 64222f15e091..5c9c235d3164 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs @@ -10,11 +10,12 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Type; use rustc_middle::mir; use rustc_middle::mir::visit::{MutVisitor, NonUseContext, PlaceContext}; -use rustc_middle::mir::Place as PlaceInternal; -use rustc_middle::ty::{Ty as TyInternal, TyCtxt}; +use rustc_middle::mir::{Operand as OperandInternal, Place as PlaceInternal}; +use rustc_middle::ty::{self, Const as ConstInternal, Ty as TyInternal, TyCtxt}; use rustc_smir::rustc_internal; -use stable_mir::mir::{Local, Place}; -use stable_mir::ty::{RigidTy, Ty, TyKind}; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{Local, Operand, Place}; +use stable_mir::ty::{Const, RigidTy, Ty, TyKind}; impl<'tcx> GotocCtx<'tcx> { pub fn place_ty_stable(&self, place: &Place) -> Ty { @@ -28,6 +29,31 @@ impl<'tcx> GotocCtx<'tcx> { pub fn local_ty_stable(&mut self, local: Local) -> Ty { self.current_fn().body().local_decl(local).unwrap().ty } + + pub fn operand_ty_stable(&mut self, operand: &Operand) -> Ty { + operand.ty(self.current_fn().body().locals()).unwrap() + } + + pub fn is_zst_stable(&self, ty: Ty) -> bool { + self.is_zst(rustc_internal::internal(ty)) + } + + pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type { + let func = self.symbol_name_stable(instance); + self.ensure_struct( + format!("{func}::FnDefStruct"), + format!("{}::FnDefStruct", instance.name()), + |_, _| vec![], + ) + } + + pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> ty::PolyFnSig<'tcx> { + self.fn_sig_of_instance(rustc_internal::internal(instance)) + } + + pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool { + self.use_fat_pointer(rustc_internal::internal(pointer_ty)) + } } /// If given type is a Ref / Raw ref, return the pointee type. pub fn pointee_type(mir_type: Ty) -> Option { @@ -59,6 +85,18 @@ impl<'a, 'tcx> StableConverter<'a, 'tcx> { ); rustc_internal::stable(place) } + + pub fn convert_operand(gcx: &'a GotocCtx<'tcx>, mut operand: OperandInternal<'tcx>) -> Operand { + let mut converter = StableConverter { gcx }; + converter.visit_operand(&mut operand, mir::Location::START); + rustc_internal::stable(operand) + } + + pub fn convert_constant(gcx: &'a GotocCtx<'tcx>, mut constant: ConstInternal<'tcx>) -> Const { + let mut converter = StableConverter { gcx }; + converter.visit_ty_const(&mut constant, mir::Location::START); + rustc_internal::stable(constant) + } } impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> { @@ -69,4 +107,22 @@ impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> { fn visit_ty(&mut self, ty: &mut TyInternal<'tcx>, _: mir::visit::TyContext) { *ty = self.gcx.monomorphize(*ty); } + + fn visit_ty_const(&mut self, ct: &mut ty::Const<'tcx>, _location: mir::Location) { + *ct = self.gcx.monomorphize(*ct); + } + + fn visit_constant(&mut self, constant: &mut mir::ConstOperand<'tcx>, location: mir::Location) { + let const_ = self.gcx.monomorphize(constant.const_); + let val = match const_.eval(self.gcx.tcx, ty::ParamEnv::reveal_all(), None) { + Ok(v) => v, + Err(mir::interpret::ErrorHandled::Reported(..)) => return, + Err(mir::interpret::ErrorHandled::TooGeneric(..)) => { + unreachable!("Failed to evaluate instance constant: {:?}", const_) + } + }; + let ty = constant.ty(); + constant.const_ = mir::Const::Val(val, ty); + self.super_constant(constant, location); + } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 9b875985b1ab..c8c0765a1fd8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -18,6 +18,7 @@ use rustc_middle::ty::{ UintTy, VariantDef, VtblEntry, }; use rustc_middle::ty::{List, TypeFoldable}; +use rustc_smir::rustc_internal; use rustc_span::def_id::DefId; use rustc_target::abi::{ Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding, @@ -680,7 +681,7 @@ impl<'tcx> GotocCtx<'tcx> { } fn codegen_ty_raw_array(&mut self, elem_ty: Ty<'tcx>, len: Const<'tcx>) -> Type { - let size = self.codegen_const(len, None).int_constant_value().unwrap(); + let size = self.codegen_const_internal(len, None).int_constant_value().unwrap(); let elemt = self.codegen_ty(elem_ty); elemt.array_of(size) } @@ -1323,12 +1324,7 @@ impl<'tcx> GotocCtx<'tcx> { /// /// For details, see pub fn codegen_fndef_type(&mut self, instance: Instance<'tcx>) -> Type { - let func = self.symbol_name(instance); - self.ensure_struct( - format!("{func}::FnDefStruct"), - format!("{}::FnDefStruct", self.readable_instance_name(instance)), - |_, _| vec![], - ) + self.codegen_fndef_type_stable(rustc_internal::stable(instance)) } /// codegen for struct diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 7b94dad06db4..5d27375de54f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -46,6 +46,7 @@ use rustc_session::Session; use rustc_smir::rustc_internal; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; +use stable_mir::mir::mono::MonoItem as MonoItemStable; use std::any::Any; use std::collections::BTreeMap; use std::collections::HashSet; @@ -111,8 +112,11 @@ impl GotocCodegenBackend { ); } MonoItem::Static(def_id) => { + let MonoItemStable::Static(def) = rustc_internal::stable(item) else { + unreachable!() + }; gcx.call_with_panic_debug_info( - |ctx| ctx.declare_static(def_id, *item), + |ctx| ctx.declare_static(def), format!("declare_static: {def_id:?}"), def_id, ); @@ -136,8 +140,11 @@ impl GotocCodegenBackend { ); } MonoItem::Static(def_id) => { + let MonoItemStable::Static(def) = rustc_internal::stable(item) else { + unreachable!() + }; gcx.call_with_panic_debug_info( - |ctx| ctx.codegen_static(def_id, *item), + |ctx| ctx.codegen_static(def), format!("codegen_static: {def_id:?}"), def_id, ); 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 d8901ae53803..61861827df96 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -24,7 +24,6 @@ use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; use kani_metadata::HarnessMetadata; use rustc_data_structures::fx::FxHashMap; -use rustc_middle::mir::interpret::Allocation; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, @@ -36,6 +35,7 @@ use rustc_span::source_map::respan; use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use stable_mir::ty::Allocation; pub struct GotocCtx<'tcx> { /// the typing context @@ -51,7 +51,7 @@ pub struct GotocCtx<'tcx> { /// a global counter for generating unique names for global variables pub global_var_count: u64, /// map a global allocation to a name in the symbol table - pub alloc_map: FxHashMap<&'tcx Allocation, String>, + pub alloc_map: FxHashMap, /// map (trait, method) pairs to possible implementations pub vtable_ctx: VtableCtx, pub current_fn: Option>, diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index e20ca5d41c60..b914c46c0f6c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -308,7 +308,7 @@ impl GotocHook for MemCmp { .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_stable(instance, span) + gcx.codegen_func_expr(instance, Some(span)) .call(vec![first_var, second_var, count_var]), ); let code = place_expr.assign(rhs, loc).with_location(loc); diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 2782f2cee47c..587eef72a645 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -10,6 +10,7 @@ use rustc_middle::mir::mono::CodegenUnitNameBuilder; use rustc_middle::mir::Local; use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::{Instance, TyCtxt}; +use stable_mir::mir::mono::Instance as InstanceStable; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { @@ -74,6 +75,15 @@ impl<'tcx> GotocCtx<'tcx> { if pretty == "main" { pretty } else { llvm_mangled } } + /// Return the mangled name to be used in the symbol table. + /// + /// We special case main function in order to support `--function main`. + // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 + pub fn symbol_name_stable(&self, instance: InstanceStable) -> String { + let pretty = instance.name(); + if pretty == "main" { pretty } else { instance.mangled_name() } + } + /// The name for a tuple field pub fn tuple_fld_name(n: usize) -> String { format!("{n}") diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 216feb66fb87..2a6bfbe8fc6b 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -631,8 +631,8 @@ mod debug { impl Display for Node { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { match &self.0 { - MonoItem::Fn(instance) => write!(f, "{}", instance.mangled_name()), - MonoItem::Static(def) => write!(f, "{}", CrateItem::from(*def).name()), + MonoItem::Fn(instance) => write!(f, "{}", instance.name()), + MonoItem::Static(def) => write!(f, "{}", def.name()), MonoItem::GlobalAsm(asm) => write!(f, "{asm:?}"), } } diff --git a/tests/kani/ConstEval/slices.rs b/tests/kani/ConstEval/slices.rs new file mode 100644 index 000000000000..16d422efe172 --- /dev/null +++ b/tests/kani/ConstEval/slices.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that we can properly handle tuple constants including the ones with some padding. +#[kani::proof] +fn point_slice() { + let point: &[(u8, u32)] = &[(0, u32::MAX), (u8::MAX, 0)]; + assert_eq!(point.len(), 2); + assert_eq!(point[0].0, 0); + assert_eq!(point[0].1, u32::MAX); +} + +#[kani::proof] +fn points() { + let point: &[(u8, u8)] = &[(0, u8::MAX), (10, 231)]; + assert_eq!(point.len(), 2); + assert_eq!(point[0].0, 0); + assert_eq!(point[0].1, u8::MAX); +}