diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index c8aba08ba5ed..f8271f5c0d4f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -11,7 +11,7 @@ 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, + Allocation, MirConst, TyConst, ConstantKind, TyConstKind, FloatTy, FnDef, GenericArgs, IntTy, RigidTy, Size, Span, Ty, TyKind, UintTy, }; use stable_mir::{CrateDef, CrateItem}; @@ -63,17 +63,17 @@ impl<'tcx> GotocCtx<'tcx> { ) -> Expr { let stable_const = rustc_internal::stable(constant); let stable_span = rustc_internal::stable(span); - self.codegen_const(&stable_const, stable_span) + self.codegen_const_ty(&stable_const, stable_span) } - /// Generate a goto expression that represents a constant. + /// Generate a goto expression that represents a MIR-level constant. /// /// 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. - pub fn codegen_const(&mut self, constant: &Const, span: Option) -> Expr { + pub fn codegen_const(&mut self, constant: &MirConst, span: Option) -> Expr { trace!(?constant, "codegen_constant"); match constant.kind() { ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), span), @@ -90,6 +90,37 @@ impl<'tcx> GotocCtx<'tcx> { ConstantKind::Param(..) | ConstantKind::Unevaluated(..) => { unreachable!() } + ConstantKind::Ty(t) => { + self.codegen_const_ty(t, span) + } + } + } + + /// Generate a goto expression that represents a type-level constant. + /// + /// 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. + pub fn codegen_const_ty(&mut self, constant: &TyConst, span: Option) -> Expr { + trace!(?constant, "codegen_constant"); + match constant.kind() { + TyConstKind::ZSTValue(lit_ty) => { + match lit_ty.kind() { + // Rust "function items" (not closures, not function pointers, see `codegen_fndef`) + TyKind::RigidTy(RigidTy::FnDef(def, args)) => { + self.codegen_fndef(def, &args, span) + } + _ => Expr::init_unit(self.codegen_ty_stable(*lit_ty), &self.symbol_table), + } + } + TyConstKind::Bound(..) | TyConstKind::Value(..) => { + unreachable!() + } + TyConstKind::Param(..) | TyConstKind::Unevaluated(..) => { + unreachable!() + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 395bf0892da2..64b928fa0c69 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -25,7 +25,7 @@ use stable_mir::mir::mono::Instance; use stable_mir::mir::{ AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp, }; -use stable_mir::ty::{ClosureKind, Const, IntTy, RigidTy, Size, Ty, TyKind, UintTy, VariantIdx}; +use stable_mir::ty::{ClosureKind, TyConst, IntTy, RigidTy, Size, Ty, TyKind, UintTy, VariantIdx}; use std::collections::BTreeMap; use tracing::{debug, trace, warn}; @@ -160,7 +160,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Codegens expressions of the type `let a = [4u8; 6];` - fn codegen_rvalue_repeat(&mut self, op: &Operand, sz: &Const, loc: Location) -> Expr { + fn codegen_rvalue_repeat(&mut self, op: &Operand, sz: &TyConst, loc: Location) -> Expr { let op_expr = self.codegen_operand_stable(op); let width = sz.eval_target_usize().unwrap(); op_expr.array_constant(width).with_location(loc) @@ -169,7 +169,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_rvalue_len(&mut self, p: &Place) -> Expr { let pt = self.place_ty_stable(p); match pt.kind() { - TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const(&sz, None), + TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const_ty(&sz, None), TyKind::RigidTy(RigidTy::Slice(_)) => { unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(p)) .fat_ptr_goto_expr @@ -1483,7 +1483,7 @@ impl<'tcx> GotocCtx<'tcx> { ) => { // Cast to a slice fat pointer. assert_eq!(src_elt_type, dst_elt_type); - let dst_goto_len = self.codegen_const(&src_elt_count, None); + let dst_goto_len = self.codegen_const_ty(&src_elt_count, None); let src_pointee_ty = pointee_type_stable(coerce_info.src_ty).unwrap(); let dst_data_expr = if src_pointee_ty.kind().is_array() { src_goto_expr.cast_to(self.codegen_ty_stable(src_elt_type).to_pointer()) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 71eb4931aad4..0d80caeb88f5 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -391,6 +391,10 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { // Nothing to do here. return; } + ConstantKind::Ty(_) => { + // Nothing to do here. + return; + } }; self.collect_allocation(&allocation); } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 9402835c2ff2..7d4a75ecdf73 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -11,7 +11,7 @@ use stable_mir::mir::{ Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, VarDebugInfo, }; -use stable_mir::ty::{Const, GenericArgs, Span, Ty, UintTy}; +use stable_mir::ty::{MirConst, GenericArgs, Span, Ty, UintTy}; use std::fmt::Debug; use std::mem; @@ -84,12 +84,12 @@ impl MutableBody { } pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand { - let literal = Const::from_str(msg); + let literal = MirConst::from_str(msg); Operand::Constant(Constant { span, user_ty: None, literal }) } pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand { - let literal = Const::try_from_uint(val, uint_ty).unwrap(); + let literal = MirConst::try_from_uint(val, uint_ty).unwrap(); Operand::Constant(Constant { span, user_ty: None, literal }) } diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 2c05c07be7f2..14ed4f52789b 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -28,7 +28,7 @@ use stable_mir::mir::{ Statement, StatementKind, Terminator, TerminatorKind, }; use stable_mir::target::{MachineInfo, MachineSize}; -use stable_mir::ty::{AdtKind, Const, IndexedVal, RigidTy, Ty, TyKind, UintTy}; +use stable_mir::ty::{AdtKind, MirConst, TyConst, IndexedVal, RigidTy, Ty, TyKind, UintTy}; use stable_mir::CrateDef; use std::fmt::Debug; use strum_macros::AsRefStr; @@ -118,7 +118,7 @@ impl ValidValuePass { ) { let span = source.span(body.blocks()); let rvalue = Rvalue::Use(Operand::Constant(Constant { - literal: Const::from_bool(false), + literal: MirConst::from_bool(false), span, user_ty: None, })); @@ -388,7 +388,10 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> { match validity { Ok(ranges) if ranges.is_empty() => {} Ok(ranges) => { - let sz = Const::try_from_uint( + // TODO: try_new_ty_const_uint isn't public, and there is + // no TyConst equivalent to try_from_uint. It's not at all + // clear how to create a TyConst at all. + let sz = TyConst::try_new_ty_const_uint( target_ty.layout().unwrap().shape().size.bytes() as u128, UintTy::Usize, diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 6354e3777aca..053b210babb0 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -18,7 +18,7 @@ use stable_mir::mir::{ BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, }; use stable_mir::target::MachineInfo; -use stable_mir::ty::{Const, RigidTy, TyKind}; +use stable_mir::ty::{MirConst, RigidTy, TyKind}; use std::fmt::Debug; use strum_macros::AsRefStr; use tracing::trace; @@ -82,7 +82,7 @@ impl IntrinsicGeneratorPass { Rvalue::Use(Operand::Constant(Constant { span, user_ty: None, - literal: Const::from_bool(true), + literal: MirConst::from_bool(true), })), ); let stmt = Statement { kind: assign, span }; @@ -116,7 +116,7 @@ impl IntrinsicGeneratorPass { Err(msg) => { // We failed to retrieve all the valid ranges. let rvalue = Rvalue::Use(Operand::Constant(Constant { - literal: Const::from_bool(false), + literal: MirConst::from_bool(false), span, user_ty: None, })); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 3f54963cc97b..47a37754b70d 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-06-04" +channel = "nightly-2024-06-05" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]