Skip to content

Commit 997a54c

Browse files
zhassan-awskarkhaztautschnig
authored
Upgrade toolchain to 2024-04-22 (rust-lang#3171)
Addresses the new `AggregateKind::RawPtr` added in rust-lang#123840. Resolves rust-lang#3161 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Kareem Khazem <[email protected]> Co-authored-by: Michael Tautschnig <[email protected]>
1 parent b34d117 commit 997a54c

File tree

3 files changed

+39
-1
lines changed

3 files changed

+39
-1
lines changed

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

+37
Original file line numberDiff line numberDiff line change
@@ -674,6 +674,43 @@ impl<'tcx> GotocCtx<'tcx> {
674674
&self.symbol_table,
675675
)
676676
}
677+
AggregateKind::RawPtr(pointee_ty, _) => {
678+
// We expect two operands: "data" and "meta"
679+
assert!(operands.len() == 2);
680+
let typ = self.codegen_ty_stable(res_ty);
681+
let layout = self.layout_of_stable(res_ty);
682+
assert!(layout.ty.is_unsafe_ptr());
683+
let data = self.codegen_operand_stable(&operands[0]);
684+
match pointee_ty.kind() {
685+
TyKind::RigidTy(RigidTy::Slice(inner_ty)) => {
686+
let pointee_goto_typ = self.codegen_ty_stable(inner_ty);
687+
// cast data to pointer with specified type
688+
let data_cast =
689+
data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
690+
let meta = self.codegen_operand_stable(&operands[1]);
691+
slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
692+
}
693+
TyKind::RigidTy(RigidTy::Adt(..)) => {
694+
let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
695+
let data_cast =
696+
data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
697+
let meta = self.codegen_operand_stable(&operands[1]);
698+
if meta.typ().sizeof(&self.symbol_table) == 0 {
699+
data_cast
700+
} else {
701+
let vtable_expr =
702+
meta.member("vtable_ptr", &self.symbol_table).cast_to(
703+
typ.lookup_field_type("vtable", &self.symbol_table).unwrap(),
704+
);
705+
dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
706+
}
707+
}
708+
_ => {
709+
let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
710+
data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) })
711+
}
712+
}
713+
}
677714
AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty),
678715
}
679716
}

kani-compiler/src/kani_middle/transform/check_values.rs

+1
Original file line numberDiff line numberDiff line change
@@ -678,6 +678,7 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
678678
AggregateKind::Array(_)
679679
| AggregateKind::Closure(_, _)
680680
| AggregateKind::Coroutine(_, _, _)
681+
| AggregateKind::RawPtr(_, _)
681682
| AggregateKind::Tuple => {}
682683
},
683684
Rvalue::AddressOf(_, _)

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-2024-04-21"
5+
channel = "nightly-2024-04-22"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)