Skip to content

Commit

Permalink
Upgrade Rust toolchain to nightly-2023-02-17
Browse files Browse the repository at this point in the history
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 <qinhh@amazon.com>
  • Loading branch information
tautschnig and qinheping committed Apr 16, 2023
1 parent 49a256a commit 25a2ee4
Show file tree
Hide file tree
Showing 6 changed files with 18 additions and 15 deletions.
10 changes: 5 additions & 5 deletions cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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,
Expand All @@ -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();

Expand Down
11 changes: 7 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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()),
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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());
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]

0 comments on commit 25a2ee4

Please sign in to comment.