Skip to content

Commit 108c2a6

Browse files
tautschnigqinheping
andcommitted
Upgrade Rust toolchain to nightly-2023-02-17
Upstream PRs that require local changes: - Don't ICE in might_permit_raw_init if reference is polymorphic rust-lang/rust#108012 - Use target instead of machine for mir interpreter integer handling rust-lang/rust#108047 - Optimize mk_region rust-lang/rust#108020 Co-authored-by: Qinheping Hu <[email protected]>
1 parent 5490a80 commit 108c2a6

File tree

6 files changed

+18
-15
lines changed

6 files changed

+18
-15
lines changed

cprover_bindings/src/goto_program/expr.rs

+5-5
Original file line numberDiff line numberDiff line change
@@ -498,8 +498,8 @@ impl Expr {
498498
}
499499

500500
/// Casts value to new_typ, only when the current type of value
501-
/// is equivalent to new_typ on the given machine (e.g. i32 -> c_int)
502-
pub fn cast_to_machine_equivalent_type(self, new_typ: &Type, mm: &MachineModel) -> Expr {
501+
/// is equivalent to new_typ on the given target (e.g. i32 -> c_int)
502+
pub fn cast_to_target_equivalent_type(self, new_typ: &Type, mm: &MachineModel) -> Expr {
503503
if self.typ() == new_typ {
504504
self
505505
} else {
@@ -509,8 +509,8 @@ impl Expr {
509509
}
510510

511511
/// Casts arguments to type of function parameters when the corresponding types
512-
/// are equivalent on the given machine (e.g. i32 -> c_int)
513-
pub fn cast_arguments_to_machine_equivalent_function_parameter_types(
512+
/// are equivalent on the given target (e.g. i32 -> c_int)
513+
pub fn cast_arguments_to_target_equivalent_function_parameter_types(
514514
function: &Expr,
515515
mut arguments: Vec<Expr>,
516516
mm: &MachineModel,
@@ -520,7 +520,7 @@ impl Expr {
520520
let mut rval: Vec<_> = parameters
521521
.iter()
522522
.map(|parameter| {
523-
arguments.remove(0).cast_to_machine_equivalent_type(parameter.typ(), mm)
523+
arguments.remove(0).cast_to_target_equivalent_type(parameter.typ(), mm)
524524
})
525525
.collect();
526526

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

+7-4
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ impl<'tcx> GotocCtx<'tcx> {
162162
($f:ident) => {{
163163
let mm = self.symbol_table.machine_model();
164164
let casted_fargs =
165-
Expr::cast_arguments_to_machine_equivalent_function_parameter_types(
165+
Expr::cast_arguments_to_target_equivalent_function_parameter_types(
166166
&BuiltinFn::$f.as_expr(),
167167
fargs,
168168
mm,
@@ -783,19 +783,22 @@ impl<'tcx> GotocCtx<'tcx> {
783783
);
784784
}
785785

786-
let param_env_and_layout = ty::ParamEnv::reveal_all().and(layout);
786+
let param_env_and_type = ty::ParamEnv::reveal_all().and(ty);
787787

788788
// Then we check if the type allows "raw" initialization for the cases
789789
// where memory is zero-initialized or entirely uninitialized
790-
if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(param_env_and_layout) {
790+
if intrinsic == "assert_zero_valid"
791+
&& !self.tcx.permits_zero_init(param_env_and_type).ok().unwrap()
792+
{
791793
return self.codegen_fatal_error(
792794
PropertyClass::SafetyCheck,
793795
&format!("attempted to zero-initialize type `{ty}`, which is invalid"),
794796
span,
795797
);
796798
}
797799

798-
if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(param_env_and_layout)
800+
if intrinsic == "assert_uninit_valid"
801+
&& !self.tcx.permits_uninit_init(param_env_and_type).ok().unwrap()
799802
{
800803
return self.codegen_fatal_error(
801804
PropertyClass::SafetyCheck,

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,7 @@ impl<'tcx> GotocCtx<'tcx> {
253253
IntTy::I64 => Expr::int_constant(s.to_i64().unwrap(), Type::signed_int(64)),
254254
IntTy::I128 => Expr::int_constant(s.to_i128().unwrap(), Type::signed_int(128)),
255255
IntTy::Isize => {
256-
Expr::int_constant(s.to_machine_isize(self).unwrap(), Type::ssize_t())
256+
Expr::int_constant(s.to_target_isize(self).unwrap(), Type::ssize_t())
257257
}
258258
},
259259
(Scalar::Int(_), ty::Uint(it)) => match it {
@@ -263,7 +263,7 @@ impl<'tcx> GotocCtx<'tcx> {
263263
UintTy::U64 => Expr::int_constant(s.to_u64().unwrap(), Type::unsigned_int(64)),
264264
UintTy::U128 => Expr::int_constant(s.to_u128().unwrap(), Type::unsigned_int(128)),
265265
UintTy::Usize => {
266-
Expr::int_constant(s.to_machine_usize(self).unwrap(), Type::size_t())
266+
Expr::int_constant(s.to_target_usize(self).unwrap(), Type::size_t())
267267
}
268268
},
269269
(Scalar::Int(_), ty::Bool) => Expr::c_bool_constant(s.to_bool().unwrap()),

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -462,7 +462,7 @@ impl<'tcx> GotocCtx<'tcx> {
462462
// https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
463463
match before.mir_typ().kind() {
464464
ty::Array(ty, len) => {
465-
let len = len.kind().try_to_machine_usize(self.tcx).unwrap();
465+
let len = len.kind().try_to_target_usize(self.tcx).unwrap();
466466
let subarray_len = if from_end {
467467
// `to` counts from the end of the array
468468
len - to - from
@@ -653,7 +653,7 @@ impl<'tcx> GotocCtx<'tcx> {
653653
match before.mir_typ().kind() {
654654
//TODO, ask on zulip if we can ever have from_end here?
655655
ty::Array(elemt, length) => {
656-
let length = length.kind().try_to_machine_usize(self.tcx).unwrap();
656+
let length = length.kind().try_to_target_usize(self.tcx).unwrap();
657657
assert!(length >= min_length);
658658
let idx = if from_end { length - offset } else { offset };
659659
let idxe = Expr::int_constant(idx, Type::ssize_t());

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -304,7 +304,7 @@ impl<'tcx> GotocCtx<'tcx> {
304304
var: ty::BoundVar::from_usize(bound_vars.len() - 1),
305305
kind: ty::BoundRegionKind::BrEnv,
306306
};
307-
let env_region = ty::ReLateBound(ty::INNERMOST, br);
307+
let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br);
308308
let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();
309309

310310
let sig = sig.skip_binder();

rust-toolchain.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2023-02-16"
5+
channel = "nightly-2023-02-17"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)