Skip to content

Commit

Permalink
Migrate intrinsics module to use StableMIR
Browse files Browse the repository at this point in the history
  • Loading branch information
celinval committed Dec 13, 2023
1 parent a7c239e commit 6804592
Show file tree
Hide file tree
Showing 8 changed files with 393 additions and 363 deletions.
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ impl<'tcx> GotocCtx<'tcx> {

/// Generate a cover statement for code coverage reports.
pub fn codegen_coverage(&self, span: Span) -> Stmt {
let loc = self.codegen_caller_span(&Some(span));
let loc = self.codegen_caller_span(&span);
// Should use Stmt::cover, but currently this doesn't work with CBMC
// unless it is run with '--cover cover' (see
// https://github.com/diffblue/cbmc/issues/6613). So for now use
Expand Down Expand Up @@ -214,9 +214,9 @@ impl<'tcx> GotocCtx<'tcx> {
&self,
property_class: PropertyClass,
msg: &str,
span: Option<Span>,
span: SpanStable,
) -> Stmt {
let loc = self.codegen_caller_span(&span);
let loc = self.codegen_caller_span_stable(span);
self.codegen_assert_assume_false(property_class, msg, loc)
}

Expand Down
633 changes: 333 additions & 300 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -393,7 +393,7 @@ impl<'tcx> GotocCtx<'tcx> {
// Check that computing `offset` in bytes would not overflow
let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
ce2.clone().cast_to(Type::ssize_t()),
rustc_internal::internal(ty),
ty,
Type::ssize_t(),
"offset",
loc,
Expand Down
12 changes: 4 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,20 +33,16 @@ impl<'tcx> GotocCtx<'tcx> {
}

pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location {
self.codegen_caller_span(&Some(rustc_internal::internal(sp)))
self.codegen_caller_span(&rustc_internal::internal(sp))
}

/// Get the location of the caller. This will attempt to reach the macro caller.
/// This function uses rustc_span methods designed to returns span for the macro which
/// originally caused the expansion to happen.
/// Note: The API stops backtracing at include! boundary.
pub fn codegen_caller_span(&self, sp: &Option<Span>) -> Location {
if let Some(span) = sp {
let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span);
self.codegen_span(&topmost)
} else {
Location::none()
}
pub fn codegen_caller_span(&self, span: &Span) -> Location {
let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span);
self.codegen_span(&topmost)
}

pub fn codegen_span_option(&self, sp: Option<Span>) -> Location {
Expand Down
62 changes: 37 additions & 25 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
use super::typ::TypeExt;
use super::typ::FN_RETURN_VOID_VAR_NAME;
use super::PropertyClass;
use crate::codegen_cprover_gotoc::codegen::ty_stable::StableConverter;
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
use crate::unwrap_or_return_codegen_unimplemented_stmt;
use cbmc::goto_program::{Expr, Location, Stmt, Type};
Expand All @@ -18,7 +19,7 @@ use rustc_smir::rustc_internal;
use rustc_span::Span;
use rustc_target::abi::VariantIdx;
use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
use stable_mir::mir::Place as PlaceStable;
use stable_mir::mir::{Operand as OperandStable, Place as PlaceStable};
use tracing::{debug, debug_span, trace};

impl<'tcx> GotocCtx<'tcx> {
Expand Down Expand Up @@ -68,15 +69,13 @@ impl<'tcx> GotocCtx<'tcx> {
StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping(
mir::CopyNonOverlapping { ref src, ref dst, ref count },
)) => {
let operands =
[src, dst, count].map(|op| StableConverter::convert_operand(self, op.clone()));
// Pack the operands and their types, then call `codegen_copy`
let fargs = vec![
self.codegen_operand(src),
self.codegen_operand(dst),
self.codegen_operand(count),
];
let farg_types =
&[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)];
self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location)
let fargs =
operands.iter().map(|op| self.codegen_operand_stable(op)).collect::<Vec<_>>();
let farg_types = operands.map(|op| self.operand_ty_stable(&op));
self.codegen_copy("copy_nonoverlapping", true, fargs, &farg_types, None, location)
}
StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => {
let cond = self.codegen_operand(op).cast_to(Type::bool());
Expand Down Expand Up @@ -474,20 +473,20 @@ impl<'tcx> GotocCtx<'tcx> {
/// This is used because we ignore ZST arguments, except for intrinsics.
pub(crate) fn codegen_funcall_args(
&mut self,
args: &[Operand<'tcx>],
args: &[OperandStable],
skip_zst: bool,
) -> Vec<Expr> {
let fargs = args
.iter()
.filter_map(|o| {
let op_ty = self.operand_ty(o);
if op_ty.is_bool() {
Some(self.codegen_operand(o).cast_to(Type::c_bool()))
} else if !self.is_zst(op_ty) || !skip_zst {
Some(self.codegen_operand(o))
.filter_map(|op| {
let op_ty = self.operand_ty_stable(op);
if op_ty.kind().is_bool() {
Some(self.codegen_operand_stable(op).cast_to(Type::c_bool()))
} else if !self.is_zst_stable(op_ty) || !skip_zst {
Some(self.codegen_operand_stable(op))
} else {
// We ignore ZST types.
debug!(arg=?o, "codegen_funcall_args ignore");
debug!(arg=?op, "codegen_funcall_args ignore");
None
}
})
Expand Down Expand Up @@ -517,13 +516,26 @@ impl<'tcx> GotocCtx<'tcx> {
span: Span,
) -> Stmt {
debug!(?func, ?args, ?destination, ?span, "codegen_funcall");
if self.is_intrinsic(func) {
return self.codegen_funcall_of_intrinsic(func, args, destination, target, span);
let func_stable = StableConverter::convert_operand(self, func.clone());
let args_stable = args
.iter()
.map(|arg| StableConverter::convert_operand(self, arg.clone()))
.collect::<Vec<_>>();
let destination_stable = StableConverter::convert_place(self, *destination);

if self.is_intrinsic(&func_stable) {
return self.codegen_funcall_of_intrinsic(
&func_stable,
&args_stable,
&destination_stable,
target.map(|bb| bb.index()),
rustc_internal::stable(span),
);
}

let loc = self.codegen_span(&span);
let funct = self.operand_ty(func);
let mut fargs = self.codegen_funcall_args(args, true);
let mut fargs = self.codegen_funcall_args(&args_stable, true);
match &funct.kind() {
ty::FnDef(defid, subst) => {
let instance =
Expand Down Expand Up @@ -700,13 +712,13 @@ impl<'tcx> GotocCtx<'tcx> {
/// A MIR [Place] is an L-value (i.e. the LHS of an assignment).
///
/// In Kani, we slightly optimize the special case for Unit and don't assign anything.
pub(crate) fn codegen_expr_to_place_stable(&mut self, p: &PlaceStable, e: Expr) -> Stmt {
if e.typ().is_unit() {
e.as_stmt(Location::none())
pub(crate) fn codegen_expr_to_place_stable(&mut self, place: &PlaceStable, expr: Expr) -> Stmt {
if self.place_ty_stable(place).kind().is_unit() {
expr.as_stmt(Location::none())
} else {
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(p))
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place))
.goto_expr
.assign(e, Location::none())
.assign(expr, Location::none())
}
}

Expand Down
17 changes: 15 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,11 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_ty_ref(rustc_internal::internal(ty))
}

pub fn local_ty_stable(&mut self, local: Local) -> Ty {
pub fn local_ty_stable(&self, local: Local) -> Ty {
self.current_fn().body().local_decl(local).unwrap().ty
}

pub fn operand_ty_stable(&mut self, operand: &Operand) -> Ty {
pub fn operand_ty_stable(&self, operand: &Operand) -> Ty {
operand.ty(self.current_fn().body().locals()).unwrap()
}

Expand Down Expand Up @@ -89,6 +89,11 @@ impl<'tcx> GotocCtx<'tcx> {
pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty {
rvalue.ty(self.current_fn().body().locals()).unwrap()
}

pub fn simd_size_and_type(&self, ty: Ty) -> (u64, Ty) {
let (sz, ty) = rustc_internal::internal(ty).simd_size_and_type(self.tcx);
(sz, rustc_internal::stable(ty))
}
}
/// If given type is a Ref / Raw ref, return the pointee type.
pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
Expand All @@ -99,6 +104,14 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
}
}

/// Convert a type into a user readable type representation.
///
/// This should be replaced by StableMIR `pretty_ty()` after
/// <https://github.com/rust-lang/rust/pull/118364> is merged.
pub fn pretty_ty(ty: Ty) -> String {
rustc_internal::internal(ty).to_string()
}

/// Convert internal rustc's structs into StableMIR ones.
///
/// The body of a StableMIR instance already comes monomorphized, which is different from rustc's
Expand Down
6 changes: 0 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1898,12 +1898,6 @@ fn common_vtable_fields(drop_in_place: Type) -> Vec<DatatypeComponent> {
fields
}

/// The mir type is a mir pointer type (Ref or RawPtr).
/// This will return false for all smart pointers. See is_std_pointer for a more complete check.
pub fn is_pointer(mir_type: Ty) -> bool {
return pointee_type(mir_type).is_some();
}

/// 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
18 changes: 0 additions & 18 deletions kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,9 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
use super::super::codegen::TypeExt;
use crate::codegen_cprover_gotoc::codegen::typ::{is_pointer, pointee_type};
use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type};
use cbmc::{btree_string_map, InternedString};
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::Ty;
use tracing::debug;

// Should move into rvalue
Expand All @@ -20,21 +17,6 @@ pub fn dynamic_fat_ptr(typ: Type, data: Expr, vtable: Expr, symbol_table: &Symbo
}

impl<'tcx> GotocCtx<'tcx> {
/// Generates an expression `(ptr as usize) % align_of(T) == 0`
/// to determine if a pointer `ptr` with pointee type `T` is aligned.
pub fn is_ptr_aligned(&mut self, typ: Ty<'tcx>, ptr: Expr) -> Expr {
// Ensure `typ` is a pointer, then extract the pointee type
assert!(is_pointer(typ));
let pointee_type = pointee_type(typ).unwrap();
// Obtain the alignment for the pointee type `T`
let layout = self.layout_of(pointee_type);
let align = Expr::int_constant(layout.align.abi.bytes(), Type::size_t());
// Cast the pointer to `usize` and return the alignment expression
let cast_ptr = ptr.cast_to(Type::size_t());
let zero = Type::size_t().zero();
cast_ptr.rem(align).eq(zero)
}

pub fn unsupported_msg(item: &str, url: Option<&str>) -> String {
let mut s = format!("{item} is not currently supported by Kani");
if let Some(url) = url {
Expand Down

0 comments on commit 6804592

Please sign in to comment.