Skip to content

Commit

Permalink
Update Rust Toolchain to 2022-06-09 (#1272)
Browse files Browse the repository at this point in the history
* Update Rust Toolchain to 2022-06-09

* minor fixes. layout.might_permit_raw_init

* Rust made Call have an unconditional return Place. Remove unused codegen_drop hook

* New subcategories of pointer casts
  • Loading branch information
tedinski authored Jun 13, 2022
1 parent 51d2be9 commit 887c2e3
Show file tree
Hide file tree
Showing 29 changed files with 523 additions and 702 deletions.
16 changes: 11 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{self, Ty};
use rustc_middle::ty::{Instance, InstanceDef};
use rustc_span::Span;
use rustc_target::abi::InitKind;
use tracing::{debug, warn};

macro_rules! emit_concurrency_warning {
Expand Down Expand Up @@ -47,17 +48,18 @@ impl<'tcx> GotocCtx<'tcx> {
&mut self,
func: &Operand<'tcx>,
args: &[Operand<'tcx>],
destination: &Option<(Place<'tcx>, BasicBlock)>,
destination: &Place<'tcx>,
target: &Option<BasicBlock>,
span: Span,
) -> Stmt {
let instance = self.get_intrinsic_instance(func).unwrap();

if let Some((assign_to, target)) = destination {
if let Some(target) = target {
let loc = self.codegen_span(&span);
let fargs = self.codegen_funcall_args(args);
Stmt::block(
vec![
self.codegen_intrinsic(instance, fargs, &assign_to, Some(span)),
self.codegen_intrinsic(instance, fargs, &destination, Some(span)),
Stmt::goto(self.current_fn().find_label(&target), loc),
],
loc,
Expand Down Expand Up @@ -785,15 +787,19 @@ impl<'tcx> GotocCtx<'tcx> {

// 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" && !layout.might_permit_raw_init(self, true) {
if intrinsic == "assert_zero_valid"
&& !layout.might_permit_raw_init(self, InitKind::Zero, false)
{
return self.codegen_fatal_error(
PropertyClass::DefaultAssertion,
&format!("attempted to zero-initialize type `{}`, which is invalid", ty),
span,
);
}

if intrinsic == "assert_uninit_valid" && !layout.might_permit_raw_init(self, false) {
if intrinsic == "assert_uninit_valid"
&& !layout.might_permit_raw_init(self, InitKind::Uninit, false)
{
return self.codegen_fatal_error(
PropertyClass::DefaultAssertion,
&format!("attempted to leave type `{}` uninitialized, which is invalid", ty),
Expand Down
20 changes: 17 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use num::bigint::BigInt;
use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
use rustc_middle::ty::adjustment::PointerCast;
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{self, Instance, IntTy, Ty, UintTy, VtblEntry, COMMON_VTABLE_ENTRIES};
use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
use tracing::{debug, warn};

Expand Down Expand Up @@ -424,7 +424,15 @@ impl<'tcx> GotocCtx<'tcx> {
Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, res_ty),
Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => self.codegen_rvalue_ref(p, res_ty),
Rvalue::Len(p) => self.codegen_rvalue_len(p),
Rvalue::Cast(CastKind::Misc, e, t) => {
// Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet:
// Should we? Tracking ticket: https://github.com/model-checking/kani/issues/1274
Rvalue::Cast(
CastKind::Misc
| CastKind::PointerExposeAddress
| CastKind::PointerFromExposedAddress,
e,
t,
) => {
let t = self.monomorphize(*t);
self.codegen_misc_cast(e, t)
}
Expand Down Expand Up @@ -602,6 +610,8 @@ impl<'tcx> GotocCtx<'tcx> {
src_goto_expr.member("data", &self.symbol_table).cast_to(dst_goto_typ)
}

/// This handles all kinds of casts, except a limited subset that are instead
/// handled by [`codegen_pointer_cast`].
fn codegen_misc_cast(&mut self, src: &Operand<'tcx>, dst_t: Ty<'tcx>) -> Expr {
let src_t = self.operand_ty(src);
debug!(
Expand Down Expand Up @@ -678,6 +688,10 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// "Pointer casts" are particular kinds of pointer-to-pointer casts.
/// See the [`PointerCast`] type for specifics.
/// Note that this does not include all casts involving pointers,
/// many of which are instead handled by [`codegen_misc_cast`] instead.
pub fn codegen_pointer_cast(
&mut self,
k: &PointerCast,
Expand Down Expand Up @@ -950,7 +964,7 @@ impl<'tcx> GotocCtx<'tcx> {

ctx.tcx.vtable_entries(trait_ref_binder)
} else {
COMMON_VTABLE_ENTRIES
TyCtxt::COMMON_VTABLE_ENTRIES
};

let (vt_size, vt_align) = ctx.codegen_vtable_size_and_align(src_mir_type);
Expand Down
Loading

0 comments on commit 887c2e3

Please sign in to comment.