Skip to content

Commit

Permalink
Replace TyKind utility methods with StableMIR ones
Browse files Browse the repository at this point in the history
  • Loading branch information
@celinval
celinval committed Dec 12, 2023
1 parent 10af130 commit 9969ec1
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 71 deletions.
8 changes: 3 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,7 @@
//! in [GotocCtx::codegen_place] below.

use super::typ::TypeExt;
use crate::codegen_cprover_gotoc::codegen::ty_stable::{
is_box, is_coroutine, pointee_type, StableConverter,
};
use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type, StableConverter};
use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
use crate::codegen_cprover_gotoc::GotocCtx;
Expand Down Expand Up @@ -411,7 +409,7 @@ impl<'tcx> GotocCtx<'tcx> {
match proj {
ProjectionElem::Deref => {
let base_type = before.mir_typ();
let inner_goto_expr = if is_box(&base_type.kind()) {
let inner_goto_expr = if base_type.kind().is_box() {
self.deref_box(before.goto_expr)
} else {
before.goto_expr
Expand Down Expand Up @@ -601,7 +599,7 @@ impl<'tcx> GotocCtx<'tcx> {
Variants::Single { .. } => before.goto_expr,
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let cases = if is_coroutine(&ty_kind) {
let cases = if ty_kind.is_coroutine() {
before.goto_expr
} else {
before.goto_expr.member("cases", &self.symbol_table)
Expand Down
33 changes: 15 additions & 18 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
use crate::codegen_cprover_gotoc::codegen::ty_stable::{
is_adt, is_array, is_char, is_coroutine, is_integral, is_numeric, is_signed, is_simd,
pointee_type_stable, StableConverter,
};
use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, StableConverter};
use crate::codegen_cprover_gotoc::codegen::PropertyClass;
use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
Expand Down Expand Up @@ -119,7 +116,7 @@ impl<'tcx> GotocCtx<'tcx> {
BinOp::Rem => ce1.rem(ce2),
BinOp::ShlUnchecked => ce1.shl(ce2),
BinOp::ShrUnchecked => {
if is_signed(&self.operand_ty_stable(e1).kind()) {
if self.operand_ty_stable(e1).kind().is_signed() {
ce1.ashr(ce2)
} else {
ce1.lshr(ce2)
Expand All @@ -138,7 +135,7 @@ impl<'tcx> GotocCtx<'tcx> {
BinOp::Mul => ce1.mul(ce2),
BinOp::Shl => ce1.shl(ce2),
BinOp::Shr => {
if is_signed(&self.operand_ty_stable(e1).kind()) {
if self.operand_ty_stable(e1).kind().is_signed() {
ce1.ashr(ce2)
} else {
ce1.lshr(ce2)
Expand Down Expand Up @@ -327,7 +324,7 @@ impl<'tcx> GotocCtx<'tcx> {
Expr::struct_expr_from_values(
self.codegen_ty_stable(res_ty),
vec![
if is_signed(&t1.kind()) {
if t1.kind().is_signed() {
ce1.ashr(ce2.clone())
} else {
ce1.lshr(ce2.clone())
Expand Down Expand Up @@ -366,7 +363,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
BinOp::Div | BinOp::Rem => {
let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
if is_integral(&self.operand_ty_stable(e1).kind()) {
if self.operand_ty_stable(e1).kind().is_integral() {
let is_rem = matches!(op, BinOp::Rem);
let check = self.check_div_overflow(e1, e2, is_rem, loc);
Expr::statement_expression(
Expand Down Expand Up @@ -446,7 +443,7 @@ impl<'tcx> GotocCtx<'tcx> {
msg,
loc,
);
if is_signed(&self.operand_ty_stable(dividend).kind()) {
if self.operand_ty_stable(dividend).kind().is_signed() {
let dividend_expr = self.codegen_operand_stable(dividend);
let overflow_msg = if is_remainder {
"attempt to calculate the remainder with overflow"
Expand Down Expand Up @@ -625,7 +622,7 @@ impl<'tcx> GotocCtx<'tcx> {
&self.symbol_table,
)
}
AggregateKind::Adt(_, _, _, _, _) if is_simd(&res_ty.kind()) => {
AggregateKind::Adt(_, _, _, _, _) if res_ty.kind().is_simd() => {
let typ = self.codegen_ty_stable(res_ty);
let layout = self.layout_of_stable(res_ty);
trace!(shape=?layout.fields, "codegen_rvalue_aggregate");
Expand Down Expand Up @@ -789,7 +786,7 @@ impl<'tcx> GotocCtx<'tcx> {
),
"discriminant field (`case`) only exists for multiple variants and direct encoding"
);
let expr = if is_coroutine(&ty.kind()) {
let expr = if ty.kind().is_coroutine() {
// Coroutines are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_coroutine`]).
// As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`.
place.member("direct_fields", &self.symbol_table)
Expand Down Expand Up @@ -930,19 +927,19 @@ impl<'tcx> GotocCtx<'tcx> {
let dst_ty_kind = dst_ty.kind();

// number casting
if is_numeric(&src_ty_kind) && is_numeric(&dst_ty_kind) {
if src_ty_kind.is_numeric() && dst_ty_kind.is_numeric() {
return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty));
}

// Behind the scenes, char is just a 32bit integer
if (is_integral(&src_ty_kind) && is_char(&dst_ty_kind))
|| (is_char(&src_ty_kind) && is_integral(&dst_ty_kind))
if (src_ty_kind.is_integral() && dst_ty_kind.is_char())
|| (src_ty_kind.is_char() && dst_ty_kind.is_integral())
{
return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty));
}

// Cast an enum to its discriminant
if src_ty_kind.is_enum() && is_integral(&dst_ty_kind) {
if src_ty_kind.is_enum() && dst_ty_kind.is_integral() {
let operand = self.codegen_operand_stable(src);
return self.codegen_get_discriminant(operand, src_ty, dst_ty);
}
Expand Down Expand Up @@ -1143,8 +1140,8 @@ impl<'tcx> GotocCtx<'tcx> {
info: CoerceUnsizedInfo,
member_coercion: Expr,
) -> Expr {
assert!(is_adt(&info.src_ty.kind()), "Expected struct. Found {:?}", info.src_ty);
assert!(is_adt(&info.dst_ty.kind()), "Expected struct. Found {:?}", info.dst_ty);
assert!(info.src_ty.kind().is_adt(), "Expected struct. Found {:?}", info.src_ty);
assert!(info.dst_ty.kind().is_adt(), "Expected struct. Found {:?}", info.dst_ty);
let dst_goto_type = self.codegen_ty_stable(info.dst_ty);
let src_field_exprs = src_expr.struct_field_exprs(&self.symbol_table);
let dst_field_exprs = src_field_exprs
Expand Down Expand Up @@ -1394,7 +1391,7 @@ impl<'tcx> GotocCtx<'tcx> {
assert_eq!(src_elt_type, dst_elt_type);
let dst_goto_len = self.codegen_const(&src_elt_count, None);
let src_pointee_ty = pointee_type_stable(coerce_info.src_ty).unwrap();
let dst_data_expr = if is_array(&src_pointee_ty.kind()) {
let dst_data_expr = if src_pointee_ty.kind().is_array() {
src_goto_expr.cast_to(self.codegen_ty_stable(src_elt_type).to_pointer())
} else {
// A struct that contains the type being coerced to a slice.
Expand Down
48 changes: 0 additions & 48 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,6 @@ use stable_mir::mir::mono::Instance;
use stable_mir::mir::{Local, Operand, Place, Rvalue};
use stable_mir::ty::{Const, RigidTy, Ty, TyKind};

pub use self::ty_utils::*;

impl<'tcx> GotocCtx<'tcx> {
pub fn place_ty_stable(&self, place: &Place) -> Ty {
place.ty(self.current_fn().body().locals()).unwrap()
Expand Down Expand Up @@ -181,49 +179,3 @@ impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
self.super_constant(constant, location);
}
}

/// Utility methods for types that we expect to be incorporated into StableMIR.
pub mod ty_utils {
use rustc_smir::rustc_internal;
use stable_mir::ty::{RigidTy, TyKind};

pub fn is_signed(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Int(..)))
}

pub fn is_integral(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Int(..) | RigidTy::Uint(..)))
}

pub fn is_array(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Array(..)))
}

pub fn is_adt(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Adt(..)))
}

pub fn is_char(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Char))
}

pub fn is_float(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Float(..)))
}

pub fn is_numeric(kind: &TyKind) -> bool {
is_integral(kind) || is_float(kind)
}

pub fn is_coroutine(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Coroutine(..)))
}

pub fn is_simd(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Adt(def, ..)) if rustc_internal::internal(def).repr().simd() )
}

pub fn is_box(kind: &TyKind) -> bool {
matches!(kind, TyKind::RigidTy(RigidTy::Adt(def, _)) if def.is_box())
}
}

0 comments on commit 9969ec1

Please sign in to comment.