Skip to content

Commit

Permalink
Upgrade rust toolchain to 2024-02-17 (model-checking#3040)
Browse files Browse the repository at this point in the history
Upgrade toolchain to 2024-02-17. Relevant PR:

- rust-lang/rust#120500
- rust-lang/rust#100603

Fixes model-checking#87
Fixes model-checking#3034
Fixes model-checking#3037
  • Loading branch information
celinval authored Feb 26, 2024
1 parent b3110ee commit c2dc489
Show file tree
Hide file tree
Showing 12 changed files with 227 additions and 148 deletions.
25 changes: 3 additions & 22 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use cbmc::goto_program::{
use rustc_middle::ty::layout::ValidityRequirement;
use rustc_middle::ty::ParamEnv;
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::{Instance, InstanceKind};
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{BasicBlockIdx, Operand, Place};
use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
use tracing::debug;
Expand Down Expand Up @@ -45,17 +45,15 @@ impl<'tcx> GotocCtx<'tcx> {
/// there is no terminator.
pub fn codegen_funcall_of_intrinsic(
&mut self,
func: &Operand,
instance: Instance,
args: &[Operand],
destination: &Place,
target: Option<BasicBlockIdx>,
span: Span,
) -> Stmt {
let instance = self.get_intrinsic_instance(func).unwrap();

if let Some(target) = target {
let loc = self.codegen_span_stable(span);
let fargs = self.codegen_funcall_args(args, false);
let fargs = args.iter().map(|arg| self.codegen_operand_stable(arg)).collect::<Vec<_>>();
Stmt::block(
vec![
self.codegen_intrinsic(instance, fargs, destination, span),
Expand All @@ -68,23 +66,6 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Returns `Some(instance)` if the function is an intrinsic; `None` otherwise
fn get_intrinsic_instance(&self, func: &Operand) -> Option<Instance> {
let funct = self.operand_ty_stable(func);
match funct.kind() {
TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
let instance = Instance::resolve(def, &args).unwrap();
if matches!(instance.kind, InstanceKind::Intrinsic) { Some(instance) } else { None }
}
_ => None,
}
}

/// Returns true if the `func` is a call to a compiler intrinsic; false otherwise.
pub fn is_intrinsic(&self, func: &Operand) -> bool {
self.get_intrinsic_instance(func).is_some()
}

/// Handles codegen for non returning intrinsics
/// Non returning intrinsics are not associated with a destination
pub fn codegen_never_return_intrinsic(&mut self, instance: Instance, span: Span) -> Stmt {
Expand Down
11 changes: 11 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -557,6 +557,17 @@ impl<'tcx> GotocCtx<'tcx> {
alloc_vals
}

/// Returns `Some(instance)` if the function is an intrinsic; `None` otherwise
pub fn get_instance(&self, func: &Operand) -> Option<Instance> {
let funct = self.operand_ty_stable(func);
match funct.kind() {
TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
Some(Instance::resolve(def, &args).unwrap())
}
_ => None,
}
}

/// Generate a goto expression for a MIR "function item" reference.
///
/// A "function item" is a ZST that corresponds to a specific single function.
Expand Down
110 changes: 60 additions & 50 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,16 @@ use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
use crate::unwrap_or_return_codegen_unimplemented_stmt;
use cbmc::goto_program::{Expr, Location, Stmt, Type};
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{List, ParamEnv};
use rustc_smir::rustc_internal;
use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
use stable_mir::mir::mono::{Instance, InstanceKind};
use stable_mir::mir::{
AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL,
};
use stable_mir::ty::{RigidTy, Span, Ty, TyKind, VariantIdx};
use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
use tracing::{debug, debug_span, trace};

impl<'tcx> GotocCtx<'tcx> {
Expand Down Expand Up @@ -432,31 +434,21 @@ impl<'tcx> GotocCtx<'tcx> {
/// as subsequent parameters.
///
/// See [GotocCtx::ty_needs_untupled_args] for more details.
fn codegen_untupled_args(
&mut self,
instance: Instance,
fargs: &mut Vec<Expr>,
last_mir_arg: Option<&Operand>,
) {
debug!("codegen_untuple_closure_args instance: {:?}, fargs {:?}", instance.name(), fargs);
if !fargs.is_empty() {
let tuple_ty = self.operand_ty_stable(last_mir_arg.unwrap());
if self.is_zst_stable(tuple_ty) {
// Don't pass anything if all tuple elements are ZST.
// ZST arguments are ignored.
return;
}
let tupe = fargs.remove(fargs.len() - 1);
if let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() {
for (idx, arg_ty) in tupled_args.iter().enumerate() {
if !self.is_zst_stable(*arg_ty) {
// Access the tupled parameters through the `member` operation
let idx_expr = tupe.clone().member(&idx.to_string(), &self.symbol_table);
fargs.push(idx_expr);
}
}
}
}
fn codegen_untupled_args(&mut self, op: &Operand, args_abi: &[ArgAbi]) -> Vec<Expr> {
let tuple_ty = self.operand_ty_stable(op);
let tuple_expr = self.codegen_operand_stable(op);
let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() else { unreachable!() };
tupled_args
.iter()
.enumerate()
.filter_map(|(idx, _)| {
let arg_abi = &args_abi[idx];
(arg_abi.mode != PassMode::Ignore).then(|| {
// Access the tupled parameters through the `member` operation
tuple_expr.clone().member(idx.to_string(), &self.symbol_table)
})
})
.collect()
}

/// Because function calls terminate basic blocks, to "end" a function call, we
Expand All @@ -472,25 +464,24 @@ impl<'tcx> GotocCtx<'tcx> {
/// Generate Goto-C for each argument to a function call.
///
/// N.B. public only because instrinsics use this directly, too.
/// When `skip_zst` is set to `true`, the return value will not include any argument that is ZST.
/// This is used because we ignore ZST arguments, except for intrinsics.
pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand], skip_zst: bool) -> Vec<Expr> {
let fargs = args
pub(crate) fn codegen_funcall_args(&mut self, fn_abi: &FnAbi, args: &[Operand]) -> Vec<Expr> {
let fargs: Vec<Expr> = args
.iter()
.filter_map(|op| {
let op_ty = self.operand_ty_stable(op);
if op_ty.kind().is_bool() {
.enumerate()
.filter_map(|(i, op)| {
// Functions that require caller info will have an extra parameter.
let arg_abi = &fn_abi.args.get(i);
let ty = self.operand_ty_stable(op);
if 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 {
} else if arg_abi.map_or(true, |abi| abi.mode != PassMode::Ignore) {
Some(self.codegen_operand_stable(op))
} else {
// We ignore ZST types.
debug!(arg=?op, "codegen_funcall_args ignore");
None
}
})
.collect();
debug!(?fargs, "codegen_funcall_args");
debug!(?fargs, args_abi=?fn_abi.args, "codegen_funcall_args");
fargs
}

Expand All @@ -515,9 +506,12 @@ impl<'tcx> GotocCtx<'tcx> {
span: Span,
) -> Stmt {
debug!(?func, ?args, ?destination, ?span, "codegen_funcall");
if self.is_intrinsic(&func) {
let instance_opt = self.get_instance(func);
if let Some(instance) = instance_opt
&& matches!(instance.kind, InstanceKind::Intrinsic)
{
return self.codegen_funcall_of_intrinsic(
&func,
instance,
&args,
&destination,
target.map(|bb| bb),
Expand All @@ -526,16 +520,23 @@ impl<'tcx> GotocCtx<'tcx> {
}

let loc = self.codegen_span_stable(span);
let funct = self.operand_ty_stable(func);
let mut fargs = self.codegen_funcall_args(&args, true);
match funct.kind() {
TyKind::RigidTy(RigidTy::FnDef(def, subst)) => {
let instance = Instance::resolve(def, &subst).unwrap();

// TODO(celina): Move this check to be inside codegen_funcall_args.
if self.ty_needs_untupled_args(rustc_internal::internal(self.tcx, funct)) {
self.codegen_untupled_args(instance, &mut fargs, args.last());
}
let fn_ty = self.operand_ty_stable(func);
match fn_ty.kind() {
fn_def @ TyKind::RigidTy(RigidTy::FnDef(..)) => {
let instance = instance_opt.unwrap();
let fn_abi = instance.fn_abi().unwrap();
let mut fargs = if args.is_empty()
|| fn_def.fn_sig().unwrap().value.abi != Abi::RustCall
{
self.codegen_funcall_args(&fn_abi, &args)
} else {
let (untupled, first_args) = args.split_last().unwrap();
let mut fargs = self.codegen_funcall_args(&fn_abi, &first_args);
fargs.append(
&mut self.codegen_untupled_args(untupled, &fn_abi.args[first_args.len()..]),
);
fargs
};

if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) {
return hk.handle(self, instance, fargs, destination, *target, span);
Expand Down Expand Up @@ -573,7 +574,16 @@ impl<'tcx> GotocCtx<'tcx> {
Stmt::block(stmts, loc)
}
// Function call through a pointer
TyKind::RigidTy(RigidTy::FnPtr(_)) => {
TyKind::RigidTy(RigidTy::FnPtr(fn_sig)) => {
let fn_sig_internal = rustc_internal::internal(self.tcx, fn_sig);
let fn_ptr_abi = rustc_internal::stable(
self.tcx
.fn_abi_of_fn_ptr(
ParamEnv::reveal_all().and((fn_sig_internal, &List::empty())),
)
.unwrap(),
);
let fargs = self.codegen_funcall_args(&fn_ptr_abi, &args);
let func_expr = self.codegen_operand_stable(func).dereference();
// Actually generate the function call and return.
Stmt::block(
Expand Down
5 changes: 5 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,11 @@ impl<'tcx> GotocCtx<'tcx> {
pub fn pretty_ty(&self, ty: Ty) -> String {
rustc_internal::internal(self.tcx, 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> {
Expand Down
39 changes: 2 additions & 37 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ use rustc_target::abi::{
Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
TyAndLayout, VariantIdx, Variants,
};
use rustc_target::spec::abi::Abi;
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
use stable_mir::mir::mono::Instance as InstanceStable;
use stable_mir::mir::Body;
Expand Down Expand Up @@ -731,39 +730,6 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_struct_fields(flds, &layout.layout.0, Size::ZERO)
}

/// A closure / some shims in Rust MIR takes two arguments:
///
/// 0. a struct representing the environment
/// 1. a tuple containing the parameters
///
/// However, during codegen/lowering from MIR, the 2nd tuple of parameters
/// is flattened into subsequent parameters.
///
/// Checking whether the type's kind is a closure is insufficient, because
/// a virtual method call through a vtable can have the trait's non-closure
/// type. For example:
///
/// ```
/// let p: &dyn Fn(i32) = &|x| assert!(x == 1);
/// p(1);
/// ```
///
/// Here, the call `p(1)` desugars to an MIR trait call `Fn::call(&p, (1,))`,
/// where the second argument is a tuple. The instance type kind for
/// `Fn::call` is not a closure, because dynamically, the pointer may be to
/// a function definition instead. We still need to untuple in this case,
/// so we follow the example elsewhere in Rust to use the ABI call type.
///
/// See `make_call_args` in `rustc_mir_transform/src/inline.rs`
pub fn ty_needs_untupled_args(&self, ty: Ty<'tcx>) -> bool {
// Note that [Abi::RustCall] is not [Abi::Rust].
// Documentation is sparse, but it does seem to correspond to the need for untupling.
match ty.kind() {
ty::FnDef(..) | ty::FnPtr(..) => ty.fn_sig(self.tcx).abi() == Abi::RustCall,
_ => unreachable!("Can't treat type as a function: {:?}", ty),
}
}

/// A closure is a struct of all its environments. That is, a closure is
/// just a tuple with a unique type identifier, so that Fn related traits
/// can find its impl.
Expand Down Expand Up @@ -1647,13 +1613,12 @@ impl<'tcx> GotocCtx<'tcx> {
/// 1. In some cases, an argument can be ignored (e.g.: ZST arguments in regular Rust calls).
/// 2. We currently don't support `track_caller`, so we ignore the extra argument that is added to support that.
/// Tracked here: <https://github.com/model-checking/kani/issues/374>
fn codegen_args<'a>(
pub fn codegen_args<'a>(
&self,
instance: InstanceStable,
fn_abi: &'a FnAbi,
) -> impl Iterator<Item = (usize, &'a ArgAbi)> {
let instance_internal = rustc_internal::internal(self.tcx, instance);
let requires_caller_location = instance_internal.def.requires_caller_location(self.tcx);
let requires_caller_location = self.requires_caller_location(instance);
let num_args = fn_abi.args.len();
fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| {
arg_abi.mode != PassMode::Ignore && !(requires_caller_location && idx + 1 == num_args)
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,8 @@ fn resolve_rust_intrinsic<'tcx>(
func_ty: Ty<'tcx>,
) -> Option<(Symbol, GenericArgsRef<'tcx>)> {
if let ty::FnDef(def_id, args) = *func_ty.kind() {
if tcx.is_intrinsic(def_id) {
return Some((tcx.item_name(def_id), args));
if let Some(symbol) = tcx.intrinsic(def_id) {
return Some((symbol, args));
}
}
None
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
#![feature(lazy_cell)]
#![feature(more_qualified_paths)]
#![feature(iter_intersperse)]
#![feature(let_chains)]
extern crate rustc_abi;
extern crate rustc_ast;
extern crate rustc_ast_pretty;
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-02-14"
channel = "nightly-2024-02-17"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
16 changes: 16 additions & 0 deletions tests/kani/Closure/zst_unwrap.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Test that Kani can properly handle closure to fn ptr when an argument type is Never (`!`).
//! See <https://github.com/model-checking/kani/issues/3034> for more details.
#![feature(never_type)]

pub struct Foo {
_x: i32,
_never: !,
}

#[kani::proof]
fn check_unwrap_never() {
let res = Result::<i32, Foo>::Ok(3);
let _x = res.unwrap_or_else(|_f| 5);
}
Loading

0 comments on commit c2dc489

Please sign in to comment.