Update the rust toolchain to nightly-2024-06-11 (#3225)

Changes required due to: - rust-lang/rust@a34c26e7ec Make body_owned_by return the body directly. - rust-lang/rust@333458c2cb Uplift TypeRelation and Relate - rust-lang/rust@459ce3f6bb Add an intrinsic for `ptr::metadata` - rust-lang/rust@7e08f80b34 Split smir `Const` into `TyConst` and `MirConst` - rust-lang/rust@eb584a23bf offset_of: allow (unstably) taking the offset of slice tail fields - rust-lang/rust@16e8803579 Update cargo Resolves: #3218
model-checking · Jun 11, 2024 · e922d73 · e922d73
1 parent eeb5fe7
commit e922d73
Show file tree

Hide file tree

Showing 17 changed files with 150 additions and 46 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -390,9 +390,9 @@ checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800"
 
 [[package]]
 name = "itertools"
-version = "0.12.1"
+version = "0.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ba291022dbbd398a455acf126c1e341954079855bc60dfdda641363bd6922569"
+checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186"
 dependencies = [
  "either",
 ]
@@ -999,9 +999,9 @@ dependencies = [
 
 [[package]]
 name = "string-interner"
-version = "0.15.0"
+version = "0.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "07f9fdfdd31a0ff38b59deb401be81b73913d76c9cc5b1aed4e1330a223420b9"
+checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e"
 dependencies = [
  "cfg-if",
  "hashbrown",

diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
@@ -17,7 +17,7 @@ lazy_static = "1.4.0"
 num = "0.4.0"
 num-traits = "0.2"
 serde = {version = "1", features = ["derive"]}
-string-interner = "0.15.0"
+string-interner = "0.17.0"
 tracing = "0.1"
 linear-map = {version = "1.2", features = ["serde_impl"]}
 

diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
@@ -12,7 +12,7 @@ publish = false
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = { version = "4.4.11", features = ["derive", "cargo"] }
 home = "0.5"
-itertools = "0.12"
+itertools = "0.13"
 kani_metadata = {path = "../kani_metadata"}
 lazy_static = "1.4.0"
 num = { version = "0.4.0", optional = true }

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -11,8 +11,8 @@ use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, StaticDef};
 use stable_mir::mir::Operand;
 use stable_mir::ty::{
-    Allocation, Const, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, RigidTy, Size, Span, Ty,
-    TyKind, UintTy,
+    Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Span,
+    Ty, TyConst, TyConstKind, TyKind, UintTy,
 };
 use stable_mir::{CrateDef, CrateItem};
 use tracing::{debug, trace};
@@ -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,34 @@ 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::Value(ty, alloc) => self.codegen_allocation(alloc, *ty, span),
+            TyConstKind::Bound(..) => 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
@@ -18,15 +18,15 @@ use cbmc::goto_program::{
 use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
 use num::bigint::BigInt;
-use rustc_middle::ty::{TyCtxt, VtblEntry};
+use rustc_middle::ty::{ParamEnv, TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
 use stable_mir::abi::{Primitive, Scalar, ValueAbi};
 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, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy, VariantIdx};
 use std::collections::BTreeMap;
 use tracing::{debug, trace, warn};
 
@@ -161,7 +161,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)
@@ -170,7 +170,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
@@ -779,9 +779,10 @@ impl<'tcx> GotocCtx<'tcx> {
                         .with_size_of_annotation(self.codegen_ty_stable(*t)),
                     NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
                     NullOp::OffsetOf(fields) => Expr::int_constant(
-                        layout
+                        self.tcx
                             .offset_of_subfield(
-                                self,
+                                ParamEnv::reveal_all(),
+                                layout,
                                 fields.iter().map(|(var_idx, field_idx)| {
                                     (
                                         rustc_internal::internal(self.tcx, var_idx),
@@ -814,6 +815,51 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                 }
                 UnOp::Neg => self.codegen_operand_stable(e).neg(),
+                UnOp::PtrMetadata => {
+                    let src_goto_expr = self.codegen_operand_stable(e);
+                    let dst_goto_typ = self.codegen_ty_stable(res_ty);
+                    debug!(
+                        "PtrMetadata |{:?}| with result type |{:?}|",
+                        src_goto_expr, dst_goto_typ
+                    );
+                    if let Some(_vtable_typ) =
+                        src_goto_expr.typ().lookup_field_type("vtable", &self.symbol_table)
+                    {
+                        let vtable_expr = src_goto_expr.member("vtable", &self.symbol_table);
+                        let dst_components =
+                            dst_goto_typ.lookup_components(&self.symbol_table).unwrap();
+                        assert_eq!(dst_components.len(), 2);
+                        assert_eq!(dst_components[0].name(), "_vtable_ptr");
+                        assert!(dst_components[0].typ().is_pointer());
+                        assert_eq!(dst_components[1].name(), "_phantom");
+                        self.assert_is_rust_phantom_data_like(&dst_components[1].typ());
+                        Expr::struct_expr(
+                            dst_goto_typ,
+                            btree_string_map![
+                                ("_vtable_ptr", vtable_expr.cast_to(dst_components[0].typ())),
+                                (
+                                    "_phantom",
+                                    Expr::struct_expr(
+                                        dst_components[1].typ(),
+                                        [].into(),
+                                        &self.symbol_table
+                                    )
+                                )
+                            ],
+                            &self.symbol_table,
+                        )
+                    } else if let Some(len_typ) =
+                        src_goto_expr.typ().lookup_field_type("len", &self.symbol_table)
+                    {
+                        assert_eq!(len_typ, dst_goto_typ);
+                        src_goto_expr.member("len", &self.symbol_table)
+                    } else {
+                        unreachable!(
+                            "fat pointer with neither vtable nor len: {:?}",
+                            src_goto_expr
+                        );
+                    }
+                }
             },
             Rvalue::Discriminant(p) => {
                 let place =
@@ -1453,7 +1499,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/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -11,8 +11,8 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::print::FmtPrinter;
 use rustc_middle::ty::GenericArgsRef;
 use rustc_middle::ty::{
-    self, AdtDef, Const, CoroutineArgs, FloatTy, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
-    UintTy, VariantDef, VtblEntry,
+    self, AdtDef, Const, CoroutineArgs, CoroutineArgsExt, FloatTy, Instance, IntTy, PolyFnSig, Ty,
+    TyCtxt, TyKind, UintTy, VariantDef, VtblEntry,
 };
 use rustc_middle::ty::{List, TypeFoldable};
 use rustc_smir::rustc_internal;

diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -125,7 +125,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Best effort check if the struct represents a rust `std::marker::PhantomData`
-    fn assert_is_rust_phantom_data_like(&self, t: &Type) {
+    pub fn assert_is_rust_phantom_data_like(&self, t: &Type) {
         // TODO: A `std::marker::PhantomData` appears to be an empty struct, in the cases we've seen.
         // Is there something smarter we can do here?
         assert!(t.is_struct_like());

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -633,7 +633,7 @@ fn parse_modify_values<'a>(
             TokenTree::Token(token, _) => {
                 if let TokenKind::Ident(id, _) = &token.kind {
                     let hir = tcx.hir();
-                    let bid = hir.body_owned_by(local_def_id);
+                    let bid = hir.body_owned_by(local_def_id).id();
                     Some(
                         hir.body_param_names(bid)
                             .zip(mir.args_iter())

diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -376,6 +376,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
@@ -7,7 +7,7 @@ use crate::kani_middle::find_fn_def;
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::*;
-use stable_mir::ty::{Const, GenericArgs, Span, Ty, UintTy};
+use stable_mir::ty::{GenericArgs, MirConst, Span, Ty, UintTy};
 use std::fmt::Debug;
 use std::mem;
 
@@ -80,12 +80,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
@@ -18,7 +18,8 @@ use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruct
 use crate::kani_middle::transform::check_values::SourceOp::UnsupportedCheck;
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
-use rustc_middle::ty::TyCtxt;
+use rustc_middle::ty::{Const, TyCtxt};
+use rustc_smir::rustc_internal;
 use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange};
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
@@ -28,7 +29,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, IndexedVal, MirConst, RigidTy, Ty, TyKind, UintTy};
 use stable_mir::CrateDef;
 use std::fmt::Debug;
 use strum_macros::AsRefStr;
@@ -65,7 +66,7 @@ impl TransformPass for ValidValuePass {
         // Do not cache body.blocks().len() since it will change as we add new checks.
         for bb_idx in 0..new_body.blocks().len() {
             let Some(candidate) =
-                CheckValueVisitor::find_next(&new_body, bb_idx, bb_idx >= orig_len)
+                CheckValueVisitor::find_next(tcx, &new_body, bb_idx, bb_idx >= orig_len)
             else {
                 continue;
             };
@@ -118,7 +119,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,
         }));
@@ -262,7 +263,8 @@ struct UnsafeInstruction {
 ///   - Transmute
 ///   - MemCopy
 ///   - Cast
-struct CheckValueVisitor<'a> {
+struct CheckValueVisitor<'a, 'b> {
+    tcx: TyCtxt<'b>,
     locals: &'a [LocalDecl],
     /// Whether we should skip the next instruction, since it might've been instrumented already.
     /// When we instrument an instruction, we partition the basic block, and the instruction that
@@ -279,13 +281,15 @@ struct CheckValueVisitor<'a> {
     machine: MachineInfo,
 }
 
-impl<'a> CheckValueVisitor<'a> {
+impl<'a, 'b> CheckValueVisitor<'a, 'b> {
     fn find_next(
+        tcx: TyCtxt<'b>,
         body: &'a MutableBody,
         bb: BasicBlockIdx,
         skip_first: bool,
     ) -> Option<UnsafeInstruction> {
         let mut visitor = CheckValueVisitor {
+            tcx,
             locals: body.locals(),
             skip_next: skip_first,
             current: SourceInstruction::Statement { idx: 0, bb },
@@ -305,7 +309,7 @@ impl<'a> CheckValueVisitor<'a> {
     }
 }
 
-impl<'a> MirVisitor for CheckValueVisitor<'a> {
+impl<'a, 'b> MirVisitor for CheckValueVisitor<'a, 'b> {
     fn visit_statement(&mut self, stmt: &Statement, location: Location) {
         if self.skip_next {
             self.skip_next = false;
@@ -388,12 +392,10 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
                                 match validity {
                                     Ok(ranges) if ranges.is_empty() => {}
                                     Ok(ranges) => {
-                                        let sz = Const::try_from_uint(
-                                            target_ty.layout().unwrap().shape().size.bytes()
-                                                as u128,
-                                            UintTy::Usize,
-                                        )
-                                        .unwrap();
+                                        let sz = rustc_internal::stable(Const::from_target_usize(
+                                            self.tcx,
+                                            target_ty.layout().unwrap().shape().size.bytes() as u64,
+                                        ));
                                         self.push_target(SourceOp::BytesValidity {
                                             target_ty,
                                             rvalue: Rvalue::Repeat(args[1].clone(), sz),

diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -11,7 +11,7 @@ use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, Constant, Operand, TerminatorKind};
-use stable_mir::ty::{Const as MirConst, FnDef, RigidTy, TyKind};
+use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
 use stable_mir::{CrateDef, DefId};
 use std::collections::HashSet;
 use std::fmt::Debug;