Merge no_panic_if(true), no_panic behavior

crates/flux-metadata/src/lib.rs

@@ -178,6 +178,7 @@ pub struct Tables<K: Eq + Hash> {
     func_span: UnordMap<FluxId<K>, Span>,
     sort_decl_param_count: UnordMap<FluxId<K>, usize>,
     no_panic: UnordMap<K, bool>,
+    no_panic_if: UnordMap<K, rty::Expr>,
 }
 
 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<rty::Expr> {
+        get!(self, no_panic_if, def_id)
+    }
+
     fn variants_of(
         &self,
         def_id: DefId,

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(),
             };

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<T> = Option<QueryResult<T>>;
 
@@ -37,6 +41,7 @@ pub trait CrateStore {
     fn func_span(&self, def_id: FluxDefId) -> Option<rustc_span::Span>;
     fn sort_decl_param_count(&self, def_id: FluxDefId) -> Option<usize>;
     fn no_panic(&self, def_id: DefId) -> Option<bool>;
+    fn no_panic_if(&self, def_id: DefId) -> Option<Expr>;
 }
 
 pub type CrateStoreDyn = dyn CrateStore;

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<DefId>) -> 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())
     }

crates/flux-middle/src/queries.rs

@@ -287,6 +287,7 @@ pub struct Queries<'genv, 'tcx> {
     lower_late_bound_vars: Cache<LocalDefId, QueryResult<List<ty::BoundVariableKind>>>,
     sort_decl_param_count: Cache<FluxDefId, usize>,
     no_panic: Cache<DefId, bool>,
+    no_panic_if: Cache<DefId, Expr>,
 }
 
 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<rty::AdtDef> {
         run_with_cache(&self.adt_def, def_id, || {
             def_id.dispatch_query(

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(

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<List<Ty>>,
         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<Ty>, flux_rustc_bridge::ty::GenericArgs, bool),
+    Closure(DefId, /* upvar_tys */ List<Ty>, flux_rustc_bridge::ty::GenericArgs, Expr),
     Coroutine(
         DefId,
         /*resume_ty: */ Ty,

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<rty::TyOrBase> {
         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()

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))
     }
 

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(),
                 )
             }

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<T: Ticks>(a: T) {
+    let x = || {
+        a.foo(); //~ ERROR may panic
+    };
+}
+
+#[flux::sig(fn (_) -> ())]
+#[flux::no_panic]
+fn call_ticks_1<T: Ticks>(a: T) {
+    let x = || {
+        a.foo(); //~ ERROR may panic
+    };
+}

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<T: Ticks>(a: T) {
+    let x = || {
+        let y = || {
+            let z = || {
+                a.foo(); //~ ERROR may panic
+            };
+        };
+    };
+}
+
+#[flux::sig(fn (_) -> ())]
+#[flux::no_panic]
+fn call_ticks_1<T: Ticks>(a: T) {
+    let x = || {
+        let y = || {
+            let z = || {
+                a.foo(); //~ ERROR may panic
+            };
+        };
+    };
+}

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!");
+}