diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 5fa9ede910ee..7aae03f1538a 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/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, 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(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index b64725f9324d..d657de37c601 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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,11 +783,13 @@ 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"), @@ -795,7 +797,8 @@ impl<'tcx> GotocCtx<'tcx> { ); } - 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, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 280448bd88e1..f33a454ee79d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/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()), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 72440401275a..dc6938f780f1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/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()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index fb217e747371..6520b330af03 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/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(); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index aeae6f8d56ca..621fdb226fe7 100644 --- a/rust-toolchain.toml +++ b/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"]