Upgrade Rust toolchain to nightly-2023-02-17

cprover_bindings/src/goto_program/expr.rs

@@ -498,8 +498,8 @@ impl Expr {
     }
 
     /// Casts value to new_typ, only when the current type of value
-    /// is equivalent to new_typ on the given machine (e.g. i32 -> c_int)
-    pub fn cast_to_machine_equivalent_type(self, new_typ: &Type, mm: &MachineModel) -> Expr {
+    /// is equivalent to new_typ on the given target (e.g. i32 -> c_int)
+    pub fn cast_to_target_equivalent_type(self, new_typ: &Type, mm: &MachineModel) -> Expr {
         if self.typ() == new_typ {
             self
         } else {
@@ -509,8 +509,8 @@ impl Expr {
     }
 
     /// Casts arguments to type of function parameters when the corresponding types
-    /// are equivalent on the given machine (e.g. i32 -> c_int)
-    pub fn cast_arguments_to_machine_equivalent_function_parameter_types(
+    /// are equivalent on the given target (e.g. i32 -> c_int)
+    pub fn cast_arguments_to_target_equivalent_function_parameter_types(
         function: &Expr,
         mut arguments: Vec<Expr>,
         mm: &MachineModel,
@@ -520,7 +520,7 @@ impl Expr {
         let mut rval: Vec<_> = parameters
             .iter()
             .map(|parameter| {
-                arguments.remove(0).cast_to_machine_equivalent_type(parameter.typ(), mm)
+                arguments.remove(0).cast_to_target_equivalent_type(parameter.typ(), mm)
             })
             .collect();
 

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -162,7 +162,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ($f:ident) => {{
                 let mm = self.symbol_table.machine_model();
                 let casted_fargs =
-                    Expr::cast_arguments_to_machine_equivalent_function_parameter_types(
+                    Expr::cast_arguments_to_target_equivalent_function_parameter_types(
                         &BuiltinFn::$f.as_expr(),
                         fargs,
                         mm,
@@ -783,19 +783,22 @@ impl<'tcx> GotocCtx<'tcx> {
             );
         }
 
-        let param_env_and_layout = ty::ParamEnv::reveal_all().and(layout);
+        let param_env_and_type = ty::ParamEnv::reveal_all().and(ty);
 
         // Then we check if the type allows "raw" initialization for the cases
         // where memory is zero-initialized or entirely uninitialized
-        if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(param_env_and_layout) {
+        if intrinsic == "assert_zero_valid"
+            && !self.tcx.permits_zero_init(param_env_and_type).ok().unwrap()
+        {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
                 &format!("attempted to zero-initialize type `{ty}`, which is invalid"),
                 span,
             );
         }
 
-        if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(param_env_and_layout)
+        if intrinsic == "assert_uninit_valid"
+            && !self.tcx.permits_uninit_init(param_env_and_type).ok().unwrap()
         {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -253,7 +253,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 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_machine_isize(self).unwrap(), Type::ssize_t())
+                    Expr::int_constant(s.to_target_isize(self).unwrap(), Type::ssize_t())
                 }
             },
             (Scalar::Int(_), ty::Uint(it)) => match it {
@@ -263,7 +263,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 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_machine_usize(self).unwrap(), Type::size_t())
+                    Expr::int_constant(s.to_target_usize(self).unwrap(), Type::size_t())
                 }
             },
             (Scalar::Int(_), ty::Bool) => Expr::c_bool_constant(s.to_bool().unwrap()),

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -462,7 +462,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
                 match before.mir_typ().kind() {
                     ty::Array(ty, len) => {
-                        let len = len.kind().try_to_machine_usize(self.tcx).unwrap();
+                        let len = len.kind().try_to_target_usize(self.tcx).unwrap();
                         let subarray_len = if from_end {
                             // `to` counts from the end of the array
                             len - to - from
@@ -653,7 +653,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match before.mir_typ().kind() {
             //TODO, ask on zulip if we can ever have from_end here?
             ty::Array(elemt, length) => {
-                let length = length.kind().try_to_machine_usize(self.tcx).unwrap();
+                let length = length.kind().try_to_target_usize(self.tcx).unwrap();
                 assert!(length >= min_length);
                 let idx = if from_end { length - offset } else { offset };
                 let idxe = Expr::int_constant(idx, Type::ssize_t());

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -304,7 +304,7 @@ impl<'tcx> GotocCtx<'tcx> {
             var: ty::BoundVar::from_usize(bound_vars.len() - 1),
             kind: ty::BoundRegionKind::BrEnv,
         };
-        let env_region = ty::ReLateBound(ty::INNERMOST, br);
+        let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br);
         let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();
 
         let sig = sig.skip_binder();

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-02-16"
+channel = "nightly-2023-02-17"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]