From 919083115f0d74b5d36cf7cf4341b331cb8a796a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 11 Dec 2023 22:09:24 -0800 Subject: [PATCH] Migrate static handling and most of the operand codegen code to StableMIR (#2931) Migrate most of the operand code generation to use StableMIR APIs, and static handling. This change is so far the one that required some re-work, since constants in StableMIR differ a bit from internal APIs. In the Rust compiler internal APIs, constant values can be using either: Scalar, Slice, Indirect (represented by an Allocation), and ZST. In the StableAPIs, a constant value is always represented with an Allocation. To avoid making changes to the final gotoc, we generate code for allocations in two steps, we first try to generate just a regular constant literal if the constant is small (similar logic to handling the Scalar internal type). For more complex cases, we create an allocation and read from it, similar to how Indirect / Slice internal handling used to work. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- cprover_bindings/src/goto_program/expr.rs | 28 + .../codegen/foreign_function.rs | 5 +- .../codegen/intrinsic.rs | 13 +- .../codegen_cprover_gotoc/codegen/operand.rs | 781 +++++++----------- .../codegen_cprover_gotoc/codegen/place.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 10 +- .../src/codegen_cprover_gotoc/codegen/span.rs | 5 + .../codegen/statement.rs | 15 +- .../codegen/static_var.rs | 27 +- .../codegen/ty_stable.rs | 64 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 10 +- .../compiler_interface.rs | 11 +- .../codegen_cprover_gotoc/context/goto_ctx.rs | 4 +- .../codegen_cprover_gotoc/overrides/hooks.rs | 2 +- .../src/codegen_cprover_gotoc/utils/names.rs | 10 + kani-compiler/src/kani_middle/reachability.rs | 4 +- tests/kani/ConstEval/slices.rs | 18 + 17 files changed, 496 insertions(+), 513 deletions(-) create mode 100644 tests/kani/ConstEval/slices.rs 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); +}