Skip to content

Commit c2dc489

Browse files
authored
Upgrade rust toolchain to 2024-02-17 (#3040)
Upgrade toolchain to 2024-02-17. Relevant PR: - rust-lang/rust#120500 - rust-lang/rust#100603 Fixes #87 Fixes #3034 Fixes #3037
1 parent b3110ee commit c2dc489

File tree

12 files changed

+227
-148
lines changed

12 files changed

+227
-148
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 3 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ use cbmc::goto_program::{
1212
use rustc_middle::ty::layout::ValidityRequirement;
1313
use rustc_middle::ty::ParamEnv;
1414
use rustc_smir::rustc_internal;
15-
use stable_mir::mir::mono::{Instance, InstanceKind};
15+
use stable_mir::mir::mono::Instance;
1616
use stable_mir::mir::{BasicBlockIdx, Operand, Place};
1717
use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
1818
use tracing::debug;
@@ -45,17 +45,15 @@ impl<'tcx> GotocCtx<'tcx> {
4545
/// there is no terminator.
4646
pub fn codegen_funcall_of_intrinsic(
4747
&mut self,
48-
func: &Operand,
48+
instance: Instance,
4949
args: &[Operand],
5050
destination: &Place,
5151
target: Option<BasicBlockIdx>,
5252
span: Span,
5353
) -> Stmt {
54-
let instance = self.get_intrinsic_instance(func).unwrap();
55-
5654
if let Some(target) = target {
5755
let loc = self.codegen_span_stable(span);
58-
let fargs = self.codegen_funcall_args(args, false);
56+
let fargs = args.iter().map(|arg| self.codegen_operand_stable(arg)).collect::<Vec<_>>();
5957
Stmt::block(
6058
vec![
6159
self.codegen_intrinsic(instance, fargs, destination, span),
@@ -68,23 +66,6 @@ impl<'tcx> GotocCtx<'tcx> {
6866
}
6967
}
7068

71-
/// Returns `Some(instance)` if the function is an intrinsic; `None` otherwise
72-
fn get_intrinsic_instance(&self, func: &Operand) -> Option<Instance> {
73-
let funct = self.operand_ty_stable(func);
74-
match funct.kind() {
75-
TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
76-
let instance = Instance::resolve(def, &args).unwrap();
77-
if matches!(instance.kind, InstanceKind::Intrinsic) { Some(instance) } else { None }
78-
}
79-
_ => None,
80-
}
81-
}
82-
83-
/// Returns true if the `func` is a call to a compiler intrinsic; false otherwise.
84-
pub fn is_intrinsic(&self, func: &Operand) -> bool {
85-
self.get_intrinsic_instance(func).is_some()
86-
}
87-
8869
/// Handles codegen for non returning intrinsics
8970
/// Non returning intrinsics are not associated with a destination
9071
pub fn codegen_never_return_intrinsic(&mut self, instance: Instance, span: Span) -> Stmt {

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -557,6 +557,17 @@ impl<'tcx> GotocCtx<'tcx> {
557557
alloc_vals
558558
}
559559

560+
/// Returns `Some(instance)` if the function is an intrinsic; `None` otherwise
561+
pub fn get_instance(&self, func: &Operand) -> Option<Instance> {
562+
let funct = self.operand_ty_stable(func);
563+
match funct.kind() {
564+
TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
565+
Some(Instance::resolve(def, &args).unwrap())
566+
}
567+
_ => None,
568+
}
569+
}
570+
560571
/// Generate a goto expression for a MIR "function item" reference.
561572
///
562573
/// A "function item" is a ZST that corresponds to a specific single function.

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

Lines changed: 60 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,16 @@ use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
77
use crate::unwrap_or_return_codegen_unimplemented_stmt;
88
use cbmc::goto_program::{Expr, Location, Stmt, Type};
99
use rustc_middle::ty::layout::LayoutOf;
10+
use rustc_middle::ty::{List, ParamEnv};
1011
use rustc_smir::rustc_internal;
1112
use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
13+
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
1214
use stable_mir::mir::mono::{Instance, InstanceKind};
1315
use stable_mir::mir::{
1416
AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
1517
Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL,
1618
};
17-
use stable_mir::ty::{RigidTy, Span, Ty, TyKind, VariantIdx};
19+
use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
1820
use tracing::{debug, debug_span, trace};
1921

2022
impl<'tcx> GotocCtx<'tcx> {
@@ -432,31 +434,21 @@ impl<'tcx> GotocCtx<'tcx> {
432434
/// as subsequent parameters.
433435
///
434436
/// See [GotocCtx::ty_needs_untupled_args] for more details.
435-
fn codegen_untupled_args(
436-
&mut self,
437-
instance: Instance,
438-
fargs: &mut Vec<Expr>,
439-
last_mir_arg: Option<&Operand>,
440-
) {
441-
debug!("codegen_untuple_closure_args instance: {:?}, fargs {:?}", instance.name(), fargs);
442-
if !fargs.is_empty() {
443-
let tuple_ty = self.operand_ty_stable(last_mir_arg.unwrap());
444-
if self.is_zst_stable(tuple_ty) {
445-
// Don't pass anything if all tuple elements are ZST.
446-
// ZST arguments are ignored.
447-
return;
448-
}
449-
let tupe = fargs.remove(fargs.len() - 1);
450-
if let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() {
451-
for (idx, arg_ty) in tupled_args.iter().enumerate() {
452-
if !self.is_zst_stable(*arg_ty) {
453-
// Access the tupled parameters through the `member` operation
454-
let idx_expr = tupe.clone().member(&idx.to_string(), &self.symbol_table);
455-
fargs.push(idx_expr);
456-
}
457-
}
458-
}
459-
}
437+
fn codegen_untupled_args(&mut self, op: &Operand, args_abi: &[ArgAbi]) -> Vec<Expr> {
438+
let tuple_ty = self.operand_ty_stable(op);
439+
let tuple_expr = self.codegen_operand_stable(op);
440+
let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() else { unreachable!() };
441+
tupled_args
442+
.iter()
443+
.enumerate()
444+
.filter_map(|(idx, _)| {
445+
let arg_abi = &args_abi[idx];
446+
(arg_abi.mode != PassMode::Ignore).then(|| {
447+
// Access the tupled parameters through the `member` operation
448+
tuple_expr.clone().member(idx.to_string(), &self.symbol_table)
449+
})
450+
})
451+
.collect()
460452
}
461453

462454
/// Because function calls terminate basic blocks, to "end" a function call, we
@@ -472,25 +464,24 @@ impl<'tcx> GotocCtx<'tcx> {
472464
/// Generate Goto-C for each argument to a function call.
473465
///
474466
/// N.B. public only because instrinsics use this directly, too.
475-
/// When `skip_zst` is set to `true`, the return value will not include any argument that is ZST.
476-
/// This is used because we ignore ZST arguments, except for intrinsics.
477-
pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand], skip_zst: bool) -> Vec<Expr> {
478-
let fargs = args
467+
pub(crate) fn codegen_funcall_args(&mut self, fn_abi: &FnAbi, args: &[Operand]) -> Vec<Expr> {
468+
let fargs: Vec<Expr> = args
479469
.iter()
480-
.filter_map(|op| {
481-
let op_ty = self.operand_ty_stable(op);
482-
if op_ty.kind().is_bool() {
470+
.enumerate()
471+
.filter_map(|(i, op)| {
472+
// Functions that require caller info will have an extra parameter.
473+
let arg_abi = &fn_abi.args.get(i);
474+
let ty = self.operand_ty_stable(op);
475+
if ty.kind().is_bool() {
483476
Some(self.codegen_operand_stable(op).cast_to(Type::c_bool()))
484-
} else if !self.is_zst_stable(op_ty) || !skip_zst {
477+
} else if arg_abi.map_or(true, |abi| abi.mode != PassMode::Ignore) {
485478
Some(self.codegen_operand_stable(op))
486479
} else {
487-
// We ignore ZST types.
488-
debug!(arg=?op, "codegen_funcall_args ignore");
489480
None
490481
}
491482
})
492483
.collect();
493-
debug!(?fargs, "codegen_funcall_args");
484+
debug!(?fargs, args_abi=?fn_abi.args, "codegen_funcall_args");
494485
fargs
495486
}
496487

@@ -515,9 +506,12 @@ impl<'tcx> GotocCtx<'tcx> {
515506
span: Span,
516507
) -> Stmt {
517508
debug!(?func, ?args, ?destination, ?span, "codegen_funcall");
518-
if self.is_intrinsic(&func) {
509+
let instance_opt = self.get_instance(func);
510+
if let Some(instance) = instance_opt
511+
&& matches!(instance.kind, InstanceKind::Intrinsic)
512+
{
519513
return self.codegen_funcall_of_intrinsic(
520-
&func,
514+
instance,
521515
&args,
522516
&destination,
523517
target.map(|bb| bb),
@@ -526,16 +520,23 @@ impl<'tcx> GotocCtx<'tcx> {
526520
}
527521

528522
let loc = self.codegen_span_stable(span);
529-
let funct = self.operand_ty_stable(func);
530-
let mut fargs = self.codegen_funcall_args(&args, true);
531-
match funct.kind() {
532-
TyKind::RigidTy(RigidTy::FnDef(def, subst)) => {
533-
let instance = Instance::resolve(def, &subst).unwrap();
534-
535-
// TODO(celina): Move this check to be inside codegen_funcall_args.
536-
if self.ty_needs_untupled_args(rustc_internal::internal(self.tcx, funct)) {
537-
self.codegen_untupled_args(instance, &mut fargs, args.last());
538-
}
523+
let fn_ty = self.operand_ty_stable(func);
524+
match fn_ty.kind() {
525+
fn_def @ TyKind::RigidTy(RigidTy::FnDef(..)) => {
526+
let instance = instance_opt.unwrap();
527+
let fn_abi = instance.fn_abi().unwrap();
528+
let mut fargs = if args.is_empty()
529+
|| fn_def.fn_sig().unwrap().value.abi != Abi::RustCall
530+
{
531+
self.codegen_funcall_args(&fn_abi, &args)
532+
} else {
533+
let (untupled, first_args) = args.split_last().unwrap();
534+
let mut fargs = self.codegen_funcall_args(&fn_abi, &first_args);
535+
fargs.append(
536+
&mut self.codegen_untupled_args(untupled, &fn_abi.args[first_args.len()..]),
537+
);
538+
fargs
539+
};
539540

540541
if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) {
541542
return hk.handle(self, instance, fargs, destination, *target, span);
@@ -573,7 +574,16 @@ impl<'tcx> GotocCtx<'tcx> {
573574
Stmt::block(stmts, loc)
574575
}
575576
// Function call through a pointer
576-
TyKind::RigidTy(RigidTy::FnPtr(_)) => {
577+
TyKind::RigidTy(RigidTy::FnPtr(fn_sig)) => {
578+
let fn_sig_internal = rustc_internal::internal(self.tcx, fn_sig);
579+
let fn_ptr_abi = rustc_internal::stable(
580+
self.tcx
581+
.fn_abi_of_fn_ptr(
582+
ParamEnv::reveal_all().and((fn_sig_internal, &List::empty())),
583+
)
584+
.unwrap(),
585+
);
586+
let fargs = self.codegen_funcall_args(&fn_ptr_abi, &args);
577587
let func_expr = self.codegen_operand_stable(func).dereference();
578588
// Actually generate the function call and return.
579589
Stmt::block(

kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,11 @@ impl<'tcx> GotocCtx<'tcx> {
115115
pub fn pretty_ty(&self, ty: Ty) -> String {
116116
rustc_internal::internal(self.tcx, ty).to_string()
117117
}
118+
119+
pub fn requires_caller_location(&self, instance: Instance) -> bool {
120+
let instance_internal = rustc_internal::internal(self.tcx, instance);
121+
instance_internal.def.requires_caller_location(self.tcx)
122+
}
118123
}
119124
/// If given type is a Ref / Raw ref, return the pointee type.
120125
pub fn pointee_type(mir_type: Ty) -> Option<Ty> {

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Lines changed: 2 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ use rustc_target::abi::{
2121
Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
2222
TyAndLayout, VariantIdx, Variants,
2323
};
24-
use rustc_target::spec::abi::Abi;
2524
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
2625
use stable_mir::mir::mono::Instance as InstanceStable;
2726
use stable_mir::mir::Body;
@@ -731,39 +730,6 @@ impl<'tcx> GotocCtx<'tcx> {
731730
self.codegen_struct_fields(flds, &layout.layout.0, Size::ZERO)
732731
}
733732

734-
/// A closure / some shims in Rust MIR takes two arguments:
735-
///
736-
/// 0. a struct representing the environment
737-
/// 1. a tuple containing the parameters
738-
///
739-
/// However, during codegen/lowering from MIR, the 2nd tuple of parameters
740-
/// is flattened into subsequent parameters.
741-
///
742-
/// Checking whether the type's kind is a closure is insufficient, because
743-
/// a virtual method call through a vtable can have the trait's non-closure
744-
/// type. For example:
745-
///
746-
/// ```
747-
/// let p: &dyn Fn(i32) = &|x| assert!(x == 1);
748-
/// p(1);
749-
/// ```
750-
///
751-
/// Here, the call `p(1)` desugars to an MIR trait call `Fn::call(&p, (1,))`,
752-
/// where the second argument is a tuple. The instance type kind for
753-
/// `Fn::call` is not a closure, because dynamically, the pointer may be to
754-
/// a function definition instead. We still need to untuple in this case,
755-
/// so we follow the example elsewhere in Rust to use the ABI call type.
756-
///
757-
/// See `make_call_args` in `rustc_mir_transform/src/inline.rs`
758-
pub fn ty_needs_untupled_args(&self, ty: Ty<'tcx>) -> bool {
759-
// Note that [Abi::RustCall] is not [Abi::Rust].
760-
// Documentation is sparse, but it does seem to correspond to the need for untupling.
761-
match ty.kind() {
762-
ty::FnDef(..) | ty::FnPtr(..) => ty.fn_sig(self.tcx).abi() == Abi::RustCall,
763-
_ => unreachable!("Can't treat type as a function: {:?}", ty),
764-
}
765-
}
766-
767733
/// A closure is a struct of all its environments. That is, a closure is
768734
/// just a tuple with a unique type identifier, so that Fn related traits
769735
/// can find its impl.
@@ -1647,13 +1613,12 @@ impl<'tcx> GotocCtx<'tcx> {
16471613
/// 1. In some cases, an argument can be ignored (e.g.: ZST arguments in regular Rust calls).
16481614
/// 2. We currently don't support `track_caller`, so we ignore the extra argument that is added to support that.
16491615
/// Tracked here: <https://github.com/model-checking/kani/issues/374>
1650-
fn codegen_args<'a>(
1616+
pub fn codegen_args<'a>(
16511617
&self,
16521618
instance: InstanceStable,
16531619
fn_abi: &'a FnAbi,
16541620
) -> impl Iterator<Item = (usize, &'a ArgAbi)> {
1655-
let instance_internal = rustc_internal::internal(self.tcx, instance);
1656-
let requires_caller_location = instance_internal.def.requires_caller_location(self.tcx);
1621+
let requires_caller_location = self.requires_caller_location(instance);
16571622
let num_args = fn_abi.args.len();
16581623
fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| {
16591624
arg_abi.mode != PassMode::Ignore && !(requires_caller_location && idx + 1 == num_args)

kani-compiler/src/kani_middle/intrinsics.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,8 +101,8 @@ fn resolve_rust_intrinsic<'tcx>(
101101
func_ty: Ty<'tcx>,
102102
) -> Option<(Symbol, GenericArgsRef<'tcx>)> {
103103
if let ty::FnDef(def_id, args) = *func_ty.kind() {
104-
if tcx.is_intrinsic(def_id) {
105-
return Some((tcx.item_name(def_id), args));
104+
if let Some(symbol) = tcx.intrinsic(def_id) {
105+
return Some((symbol, args));
106106
}
107107
}
108108
None

kani-compiler/src/main.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
#![feature(lazy_cell)]
1414
#![feature(more_qualified_paths)]
1515
#![feature(iter_intersperse)]
16+
#![feature(let_chains)]
1617
extern crate rustc_abi;
1718
extern crate rustc_ast;
1819
extern crate rustc_ast_pretty;

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2024-02-14"
5+
channel = "nightly-2024-02-17"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/Closure/zst_unwrap.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//! Test that Kani can properly handle closure to fn ptr when an argument type is Never (`!`).
4+
//! See <https://github.com/model-checking/kani/issues/3034> for more details.
5+
#![feature(never_type)]
6+
7+
pub struct Foo {
8+
_x: i32,
9+
_never: !,
10+
}
11+
12+
#[kani::proof]
13+
fn check_unwrap_never() {
14+
let res = Result::<i32, Foo>::Ok(3);
15+
let _x = res.unwrap_or_else(|_f| 5);
16+
}

0 commit comments

Comments
 (0)