Skip to content

Commit

Permalink
Cleanup a few internal compiler deps (#3739)
Browse files Browse the repository at this point in the history
Some of this code was broken by the toolchain update. Instead of
changing it, replace it by StableMIR APIs.

Related to #3731 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
celinval authored Nov 27, 2024
1 parent 0ebf089 commit 17f4ff1
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 89 deletions.
8 changes: 5 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,9 @@
//! `typ.rs`.

use crate::codegen_cprover_gotoc::GotocCtx;
use crate::kani_middle::abi::LayoutOf;
use cbmc::goto_program::Type;
use rustc_middle::ty::layout::{LayoutOf, TyAndLayout};
use rustc_middle::ty::layout::{LayoutOf as _, TyAndLayout};
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{Local, Operand, Place, Rvalue};
Expand Down Expand Up @@ -36,7 +37,7 @@ impl<'tcx> GotocCtx<'tcx> {
}

pub fn is_zst_stable(&self, ty: Ty) -> bool {
self.is_zst(rustc_internal::internal(self.tcx, ty))
LayoutOf::new(ty).is_zst()
}

pub fn layout_of_stable(&self, ty: Ty) -> TyAndLayout<'tcx> {
Expand Down Expand Up @@ -113,14 +114,15 @@ impl<'tcx> GotocCtx<'tcx> {
/// This should be replaced by StableMIR `pretty_ty()` after
/// <https://github.com/rust-lang/rust/pull/118364> is merged.
pub fn pretty_ty(&self, ty: Ty) -> String {
rustc_internal::internal(self.tcx, ty).to_string()
ty.to_string()
}

pub fn requires_caller_location(&self, instance: Instance) -> bool {
let instance_internal = rustc_internal::internal(self.tcx, instance);
instance_internal.def.requires_caller_location(self.tcx)
}
}

/// If given type is a Ref / Raw ref, return the pointee type.
pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
match mir_type.kind() {
Expand Down
5 changes: 5 additions & 0 deletions kani-compiler/src/kani_middle/abi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,11 @@ impl LayoutOf {
self.layout.is_sized()
}

/// Return whether this is a zero-sized type
pub fn is_zst(&self) -> bool {
self.is_sized() && self.layout.size.bytes() == 0
}

/// Return whether the type is unsized and its tail is a foreign item.
///
/// This will also return `true` if the type is foreign.
Expand Down
5 changes: 3 additions & 2 deletions kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -622,8 +622,9 @@ impl<'tcx> KaniAttributes<'tcx> {
),
);
} else {
let instance = Instance::mono(tcx, self.item);
if !super::fn_abi(tcx, instance).args.is_empty() {
let instance = rustc_internal::stable(Instance::mono(tcx, self.item));
let fn_abi = instance.fn_abi().unwrap();
if !fn_abi.args.is_empty() {
tcx.dcx().span_err(span, "functions used as harnesses cannot have any arguments");
}
}
Expand Down
85 changes: 1 addition & 84 deletions kani-compiler/src/kani_middle/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,17 +7,8 @@ use std::collections::HashSet;

use crate::kani_queries::QueryDb;
use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE};
use rustc_middle::span_bug;
use rustc_middle::ty::layout::{
FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError,
LayoutOfHelpers, TyAndLayout,
};
use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt};
use rustc_middle::ty::TyCtxt;
use rustc_smir::rustc_internal;
use rustc_span::Span;
use rustc_span::source_map::respan;
use rustc_target::abi::call::FnAbi;
use rustc_target::abi::{HasDataLayout, TargetDataLayout};
use stable_mir::CrateDef;
use stable_mir::mir::mono::MonoItem;
use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
Expand Down Expand Up @@ -155,80 +146,6 @@ impl SourceLocation {
}
}

/// Get the FnAbi of a given instance with no extra variadic arguments.
/// TODO: Get rid of this. Use instance.fn_abi() instead.
/// <https://github.com/model-checking/kani/issues/1365>
pub fn fn_abi<'tcx>(
tcx: TyCtxt<'tcx>,
instance: InstanceInternal<'tcx>,
) -> &'tcx FnAbi<'tcx, TyInternal<'tcx>> {
let helper = CompilerHelpers { tcx };
helper.fn_abi_of_instance(instance, ty::List::empty())
}

struct CompilerHelpers<'tcx> {
tcx: TyCtxt<'tcx>,
}

impl<'tcx> HasParamEnv<'tcx> for CompilerHelpers<'tcx> {
fn param_env(&self) -> ty::ParamEnv<'tcx> {
ty::ParamEnv::reveal_all()
}
}

impl<'tcx> HasTyCtxt<'tcx> for CompilerHelpers<'tcx> {
fn tcx(&self) -> TyCtxt<'tcx> {
self.tcx
}
}

impl HasDataLayout for CompilerHelpers<'_> {
fn data_layout(&self) -> &TargetDataLayout {
self.tcx.data_layout()
}
}

impl<'tcx> LayoutOfHelpers<'tcx> for CompilerHelpers<'tcx> {
type LayoutOfResult = TyAndLayout<'tcx>;

#[inline]
fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: TyInternal<'tcx>) -> ! {
span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
}
}

/// Implement error handling for extracting function ABI information.
impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> {
type FnAbiOfResult = &'tcx FnAbi<'tcx, TyInternal<'tcx>>;

#[inline]
fn handle_fn_abi_err(
&self,
err: FnAbiError<'tcx>,
span: Span,
fn_abi_request: FnAbiRequest<'tcx>,
) -> ! {
if let FnAbiError::Layout(LayoutError::SizeOverflow(_)) = err {
self.tcx.dcx().emit_fatal(respan(span, err))
} else {
match fn_abi_request {
FnAbiRequest::OfFnPtr { sig, extra_args } => {
span_bug!(
span,
"Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`",
);
}
FnAbiRequest::OfInstance { instance, extra_args } => {
span_bug!(
span,
"Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`",
);
}
}
}
}
}

/// Try to convert an internal `DefId` to a `FnDef`.
pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option<FnDef> {
if let TyKind::RigidTy(RigidTy::FnDef(def, _)) =
Expand Down

0 comments on commit 17f4ff1

Please sign in to comment.