diff --git a/crates/flux-metadata/src/lib.rs b/crates/flux-metadata/src/lib.rs index 23f773eeeb..a54d346840 100644 --- a/crates/flux-metadata/src/lib.rs +++ b/crates/flux-metadata/src/lib.rs @@ -178,6 +178,7 @@ pub struct Tables { func_span: UnordMap, Span>, sort_decl_param_count: UnordMap, usize>, no_panic: UnordMap, + no_panic_if: UnordMap, } impl CStore { @@ -260,6 +261,10 @@ impl CrateStore for CStore { get!(self, no_panic, def_id) } + fn no_panic_if(&self, def_id: DefId) -> Option { + get!(self, no_panic_if, def_id) + } + fn variants_of( &self, def_id: DefId, diff --git a/crates/flux-middle/src/builtin_assoc_refts.rs b/crates/flux-middle/src/builtin_assoc_refts.rs index 82052ff4c6..85f5db0607 100644 --- a/crates/flux-middle/src/builtin_assoc_refts.rs +++ b/crates/flux-middle/src/builtin_assoc_refts.rs @@ -118,11 +118,12 @@ impl<'tcx> GlobalEnv<'_, 'tcx> { let self_ty = alias_reft.self_ty(); let body = match self_ty.as_bty_skipping_binder() { BaseTy::Closure(_, _, _, no_panic) => { - if *no_panic { - rty::Expr::tt() - } else { - rty::Expr::ff() - } + no_panic.clone() + // if *no_panic { + // rty::Expr::tt() + // } else { + // rty::Expr::ff() + // } } _ => rty::Expr::ff(), }; diff --git a/crates/flux-middle/src/cstore.rs b/crates/flux-middle/src/cstore.rs index 2bb4ef572a..5e9bfc8ecc 100644 --- a/crates/flux-middle/src/cstore.rs +++ b/crates/flux-middle/src/cstore.rs @@ -3,7 +3,11 @@ use std::rc::Rc; use rustc_hir::def_id::CrateNum; use rustc_span::def_id::DefId; -use crate::{def_id::FluxDefId, queries::QueryResult, rty}; +use crate::{ + def_id::FluxDefId, + queries::QueryResult, + rty::{self, Expr}, +}; pub type OptResult = Option>; @@ -37,6 +41,7 @@ pub trait CrateStore { fn func_span(&self, def_id: FluxDefId) -> Option; fn sort_decl_param_count(&self, def_id: FluxDefId) -> Option; fn no_panic(&self, def_id: DefId) -> Option; + fn no_panic_if(&self, def_id: DefId) -> Option; } pub type CrateStoreDyn = dyn CrateStore; diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs index 90b1c04145..5246b959a3 100644 --- a/crates/flux-middle/src/global_env.rs +++ b/crates/flux-middle/src/global_env.rs @@ -27,7 +27,7 @@ use crate::{ queries::{DispatchKey, Providers, Queries, QueryErr, QueryResult}, query_bug, rty::{ - self, QualifierKind, + self, Expr, QualifierKind, refining::{Refine as _, Refiner}, }, }; @@ -461,6 +461,12 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { self.inner.queries.no_panic(self, def_id.into_query_param()) } + pub fn no_panic_if(self, def_id: impl IntoQueryParam) -> Expr { + self.inner + .queries + .no_panic_if(self, def_id.into_query_param()) + } + pub fn is_box(&self, res: fhir::Res) -> bool { res.is_box(self.tcx()) } diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index 5a6633cde6..bcd25215ee 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -287,6 +287,7 @@ pub struct Queries<'genv, 'tcx> { lower_late_bound_vars: Cache>>, sort_decl_param_count: Cache, no_panic: Cache, + no_panic_if: Cache, } impl<'genv, 'tcx> Queries<'genv, 'tcx> { @@ -328,6 +329,7 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { lower_late_bound_vars: Default::default(), sort_decl_param_count: Default::default(), no_panic: Default::default(), + no_panic_if: Default::default(), } } @@ -670,6 +672,50 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { }) } + pub(crate) fn no_panic_if(&self, genv: GlobalEnv, def_id: DefId) -> Expr { + run_with_cache(&self.no_panic_if, def_id, || { + def_id.dispatch_query( + genv, + self, + |def_id| { + let mut current_id = def_id.local_id(); + + // Walk up the entire parent chain within this closure + loop { + // Skip dummy items and closures. + if genv.is_dummy(current_id) + || genv.tcx().is_closure_like(current_id.into()) + { + if let Some(parent) = genv.tcx().opt_local_parent(current_id) { + current_id = parent; + continue; + } else { + return Expr::ff(); // Reached top without finding non-dummy + } + } + + if let Ok(sig) = genv.fn_sig(current_id.to_def_id()) { + return sig.skip_binder().skip_binder().no_panic(); + } + + // Move to the next parent + if let Some(parent) = genv.tcx().opt_local_parent(current_id) { + current_id = parent; + } else { + break; // Reached the top + } + } + + // Be default, try to inherit the `no_panic` status from the raw annotations if + // `no_panic_if` is not present. + if genv.no_panic(def_id) { Expr::tt() } else { Expr::ff() } + }, + |def_id| genv.cstore().no_panic_if(def_id), + |_| Expr::ff(), + ) + }) + } + pub(crate) fn adt_def(&self, genv: GlobalEnv, def_id: DefId) -> QueryResult { run_with_cache(&self.adt_def, def_id, || { def_id.dispatch_query( diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 2472e79e32..473982a556 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -938,7 +938,12 @@ impl TypeSuperFoldable for BaseTy { BaseTy::Array(ty.try_fold_with(folder)?, c.try_fold_with(folder)?) } BaseTy::Closure(did, args, gen_args, no_panic) => { - BaseTy::Closure(*did, args.try_fold_with(folder)?, gen_args.clone(), *no_panic) + BaseTy::Closure( + *did, + args.try_fold_with(folder)?, + gen_args.clone(), + no_panic.clone(), + ) } BaseTy::Coroutine(did, resume_ty, args, gen_args) => { BaseTy::Coroutine( diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 20274b047a..2a86b4ed33 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -713,7 +713,7 @@ pub fn to_closure_sig( tys: &[Ty], args: &flux_rustc_bridge::ty::GenericArgs, poly_sig: &PolyFnSig, - no_panic: bool, + no_panic: Expr, ) -> PolyFnSig { let closure_args = args.as_closure(); let kind_ty = closure_args.kind_ty().to_rustc(tcx); @@ -723,7 +723,7 @@ pub fn to_closure_sig( let mut vars = poly_sig.vars().clone().to_vec(); let fn_sig = poly_sig.clone().skip_binder(); - let closure_ty = Ty::closure(closure_id.into(), tys, args, no_panic); + let closure_ty = Ty::closure(closure_id.into(), tys, args, no_panic.clone()); let env_ty = match kind { ClosureKind::Fn => { vars.push(BoundVariableKind::Region(BoundRegionKind::ClosureEnv)); @@ -755,7 +755,8 @@ pub fn to_closure_sig( fn_sig.requires.clone(), inputs.into(), output, - if no_panic { crate::rty::Expr::tt() } else { crate::rty::Expr::ff() }, + // if no_panic { crate::rty::Expr::tt() } else { crate::rty::Expr::ff() }, + no_panic, false, ); @@ -1616,7 +1617,7 @@ impl Ty { did: DefId, tys: impl Into>, args: &flux_rustc_bridge::ty::GenericArgs, - no_panic: bool, + no_panic: Expr, ) -> Ty { BaseTy::Closure(did, tys.into(), args.clone(), no_panic).to_ty() } @@ -1830,7 +1831,7 @@ pub enum BaseTy { Alias(AliasKind, AliasTy), Array(Ty, Const), Never, - Closure(DefId, /* upvar_tys */ List, flux_rustc_bridge::ty::GenericArgs, bool), + Closure(DefId, /* upvar_tys */ List, flux_rustc_bridge::ty::GenericArgs, Expr), Coroutine( DefId, /*resume_ty: */ Ty, diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 244468eb8d..0e78c456ba 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -213,7 +213,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { pub fn refine_ty_or_base(&self, ty: &ty::Ty) -> QueryResult { let bty = match ty.kind() { ty::TyKind::Closure(did, args) => { - let no_panic = self.genv.no_panic(did); + let no_panic = self.genv.no_panic_if(*did); let closure_args = args.as_closure(); let upvar_tys = closure_args .upvar_tys() diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 7a0524e9df..58e6e9da23 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1335,7 +1335,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { let closure_id = did.expect_local(); let span = tcx.def_span(closure_id); let body = genv.mir(closure_id).with_span(span)?; - let no_panic = self.genv.no_panic(*did); + let mut no_panic = self.genv.no_panic_if(self.checker_id.root_id()); + let closure_sig = rty::to_closure_sig(tcx, closure_id, upvar_tys, args, poly_sig, no_panic); Checker::run( infcx.change_item(closure_id, &body.infcx), @@ -1345,6 +1346,13 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { ) } + // TODO: this function should ensure that the EarlyBinder matches that of the closure, and that + // the inner binder of the FnSig can't mention EarlyBinder variables. + // For now, this is a nothing burger. + fn no_panic_if_ok(parent_sig: PolyFnSig, closure_sig: PolyFnSig) -> () { + // 1. The EarlyBinder matches that of the closure. + } + fn check_rvalue_closure( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, @@ -1363,7 +1371,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { // (3) "Save" the closure type in the `closures` map self.inherited.closures.insert(*did, poly_sig); // (4) Return the closure type - let no_panic = self.genv.no_panic(*did); + let no_panic = self.genv.no_panic_if(self.checker_id.root_id()); + Ok(Ty::closure(*did, upvar_tys, args, no_panic)) } diff --git a/crates/flux-refineck/src/type_env/place_ty.rs b/crates/flux-refineck/src/type_env/place_ty.rs index 123a8e61ad..b93d5381bd 100644 --- a/crates/flux-refineck/src/type_env/place_ty.rs +++ b/crates/flux-refineck/src/type_env/place_ty.rs @@ -525,7 +525,7 @@ impl<'a, 'infcx, 'genv, 'tcx> Unfolder<'a, 'infcx, 'genv, 'tcx> { let mut upvar_tys = upvar_tys.to_vec(); upvar_tys[f.as_usize()] = upvar_tys[f.as_usize()].try_fold_with(self)?; Ty::indexed( - BaseTy::Closure(*def_id, upvar_tys.into(), args.clone(), *no_panic), + BaseTy::Closure(*def_id, upvar_tys.into(), args.clone(), no_panic.clone()), idx.clone(), ) } @@ -677,7 +677,7 @@ where TyKind::Indexed(BaseTy::Closure(def_id, upvar_tys, args, no_panic), idx) => { let upvar_tys = self.fold_field_at(upvar_tys, f); Ty::indexed( - BaseTy::Closure(*def_id, upvar_tys, args.clone(), *no_panic), + BaseTy::Closure(*def_id, upvar_tys, args.clone(), no_panic.clone()), idx.clone(), ) } diff --git a/tests/tests/neg/surface/no_panic07.rs b/tests/tests/neg/surface/no_panic07.rs new file mode 100644 index 0000000000..542a5a421d --- /dev/null +++ b/tests/tests/neg/surface/no_panic07.rs @@ -0,0 +1,27 @@ +#[flux::assoc(fn foo_no_panic() -> bool)] +trait Ticks { + #[flux::sig(fn (&Self) -> Self)] + #[flux::no_panic_if(Self::foo_no_panic())] + fn foo(&self) -> Self; +} + +// `call_ticks_0` and `call_ticks_1` should have identical behavior, but +// right now, they don't because of the way we handle closures: closures +// only inherit their `no_panic` status from the first parent who is annotated +// with `no_panic`, effectively ignoring the `no_panic_if` annotation on `call_ticks_0`. +// Boo! +#[flux::sig(fn (_) -> ())] +#[flux::no_panic_if(true)] +fn call_ticks_0(a: T) { + let x = || { + a.foo(); //~ ERROR may panic + }; +} + +#[flux::sig(fn (_) -> ())] +#[flux::no_panic] +fn call_ticks_1(a: T) { + let x = || { + a.foo(); //~ ERROR may panic + }; +} diff --git a/tests/tests/neg/surface/no_panic08.rs b/tests/tests/neg/surface/no_panic08.rs new file mode 100644 index 0000000000..1a9f454bd3 --- /dev/null +++ b/tests/tests/neg/surface/no_panic08.rs @@ -0,0 +1,30 @@ +#[flux::assoc(fn foo_no_panic() -> bool)] +trait Ticks { + #[flux::sig(fn (&Self) -> Self)] + #[flux::no_panic_if(Self::foo_no_panic())] + fn foo(&self) -> Self; +} + +#[flux::sig(fn (_) -> ())] +#[flux::no_panic_if(true)] +fn call_ticks_0(a: T) { + let x = || { + let y = || { + let z = || { + a.foo(); //~ ERROR may panic + }; + }; + }; +} + +#[flux::sig(fn (_) -> ())] +#[flux::no_panic] +fn call_ticks_1(a: T) { + let x = || { + let y = || { + let z = || { + a.foo(); //~ ERROR may panic + }; + }; + }; +} diff --git a/tests/tests/neg/surface/no_panic09.rs b/tests/tests/neg/surface/no_panic09.rs new file mode 100644 index 0000000000..50b29ea8cd --- /dev/null +++ b/tests/tests/neg/surface/no_panic09.rs @@ -0,0 +1,19 @@ +#[flux_rs::no_panic_if(true)] +fn foo1() { + evil(); //~ ERROR may panic + let x = || { + evil(); //~ ERROR may panic + }; +} + +#[flux_rs::no_panic] +fn foo2() { + evil(); //~ ERROR may panic + let x = || { + evil(); //~ ERROR may panic + }; +} + +fn evil() { + panic!("yoohoo!"); +}