Try to move to 2024-06-05

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<Span>) -> Expr {
+    pub fn codegen_const(&mut self, constant: &MirConst, span: Option<Span>) -> 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<Span>) -> 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!()
+            }
         }
     }
 

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())

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);
     }

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 })
     }
 

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,

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,
                 }));

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"]