WIP: investigating changing genv::no_panic return type from bool --> Expr

Author: ninehusky

crates/flux-fhir-analysis/src/conv/mod.rs

@@ -665,6 +665,9 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
         fn_id: MaybeExternId,
         fn_sig: &fhir::FnSig,
     ) -> QueryResult<rty::PolyFnSig> {
+        let fn_name = self.tcx().def_path_str(fn_id.resolved_id());
+        eprintln!("trying to conv fn sig for `{fn_name}` with id `{fn_id:?}`");
+
         let decl = &fn_sig.decl;
         let header = fn_sig.header;
 
@@ -680,9 +683,12 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
         let no_panic = if let Some(e) = fn_sig.no_panic_if {
             self.conv_expr(&mut env, &e)?
         } else {
-            if self.genv().no_panic(fn_id) { Expr::tt() } else { Expr::ff() }
+            // if self.genv().no_panic(fn_id) { Expr::tt() } else { Expr::ff() }
+            self.genv().no_panic(fn_id)
         };
 
+        let fn_name = self.tcx().def_path_str(fn_id.resolved_id());
+
         let fn_sig =
             self.conv_fn_decl(&mut env, header.safety(), header.abi, decl, body_id, no_panic)?;
 

crates/flux-metadata/src/lib.rs

@@ -177,7 +177,7 @@ pub struct Tables<K: Eq + Hash> {
     func_sort: UnordMap<FluxId<K>, rty::PolyFuncSort>,
     func_span: UnordMap<FluxId<K>, Span>,
     sort_decl_param_count: UnordMap<FluxId<K>, usize>,
-    no_panic: UnordMap<K, bool>,
+    no_panic: UnordMap<K, rty::Expr>,
 }
 
 impl CStore {
@@ -256,7 +256,7 @@ impl CrateStore for CStore {
         get!(self, adt_sort_def, def_id)
     }
 
-    fn no_panic(&self, def_id: DefId) -> Option<bool> {
+    fn no_panic(&self, def_id: DefId) -> Option<rty::Expr> {
         get!(self, no_panic, def_id)
     }
 

crates/flux-middle/src/builtin_assoc_refts.rs

@@ -117,13 +117,7 @@ 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()
-                    }
-                }
+                BaseTy::Closure(_, _, _, no_panic) => no_panic.clone(),
                 _ => rty::Expr::ff(),
             };
             rty::Lambda::bind_with_vars(body, List::empty(), rty::Sort::Bool)

crates/flux-middle/src/cstore.rs

@@ -36,7 +36,7 @@ pub trait CrateStore {
     fn func_sort(&self, def_id: FluxDefId) -> Option<rty::PolyFuncSort>;
     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(&self, def_id: DefId) -> Option<rty::Expr>;
 }
 
 pub type CrateStoreDyn = dyn CrateStore;

crates/flux-middle/src/global_env.rs

@@ -457,7 +457,7 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> {
     }
 
     /// Whether the function is marked with `#[flux::no_panic]`
-    pub fn no_panic(self, def_id: impl IntoQueryParam<DefId>) -> bool {
+    pub fn no_panic(self, def_id: impl IntoQueryParam<DefId>) -> rty::Expr {
         self.inner.queries.no_panic(self, def_id.into_query_param())
     }
 

crates/flux-middle/src/queries.rs

@@ -286,7 +286,7 @@ pub struct Queries<'genv, 'tcx> {
     fn_sig: Cache<DefId, QueryResult<rty::EarlyBinder<rty::PolyFnSig>>>,
     lower_late_bound_vars: Cache<LocalDefId, QueryResult<List<ty::BoundVariableKind>>>,
     sort_decl_param_count: Cache<FluxDefId, usize>,
-    no_panic: Cache<DefId, bool>,
+    no_panic: Cache<DefId, rty::Expr>,
 }
 
 impl<'genv, 'tcx> Queries<'genv, 'tcx> {
@@ -629,7 +629,7 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
         })
     }
 
-    pub(crate) fn no_panic(&self, genv: GlobalEnv, def_id: DefId) -> bool {
+    pub(crate) fn no_panic(&self, genv: GlobalEnv, def_id: DefId) -> Expr {
         run_with_cache(&self.no_panic, def_id, || {
             def_id.dispatch_query(
                 genv,
@@ -645,13 +645,22 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                                 current_id = parent;
                                 continue;
                             } else {
-                                return false; // Reached top without finding non-dummy
+                                return Expr::ff();
                             }
                         }
 
-                        // Check if current non-dummy item has the `no_panic` attribute
+                        // Check if current non-dummy item has the `no_panic` attribute, or
+                        // a `no_panic_if` attribute.
                         if genv.fhir_attr_map(current_id).no_panic() {
-                            return true;
+                            return Expr::tt();
+                        } else if let Ok(fn_sig) = genv.fn_sig(current_id) {
+                            let fn_sig = fn_sig.skip_binder().skip_binder();
+                            eprintln!(
+                                "found fn_sig for {}, no_panic_if = {:?}",
+                                genv.tcx().def_path_str(current_id.to_def_id()),
+                                fn_sig.no_panic()
+                            );
+                            return fn_sig.no_panic();
                         }
 
                         // Move to the next parent
@@ -662,10 +671,10 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                         }
                     }
 
-                    config::no_panic()
+                    Expr::from_bool(config::no_panic())
                 },
                 |def_id| genv.cstore().no_panic(def_id),
-                |_| false,
+                |_| Expr::ff(),
             )
         })
     }

crates/flux-middle/src/rty/expr.rs

@@ -476,6 +476,13 @@ impl Expr {
         }
     }
 
+    pub fn from_bool(b: bool) -> Expr {
+        match b {
+            true => Expr::tt(),
+            false => Expr::ff(),
+        }
+    }
+
     fn const_op(op: &BinOp, c1: &Constant, c2: &Constant) -> Option<Constant> {
         match op {
             BinOp::Iff => c1.iff(c2),

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

@@ -68,7 +68,7 @@ use crate::{
     global_env::GlobalEnv,
     pretty::{Pretty, PrettyCx},
     queries::{QueryErr, QueryResult},
-    rty::subst::SortSubst,
+    rty::{self, subst::SortSubst},
 };
 
 /// The definition of the data sort automatically generated for a struct or enum.
@@ -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,7 @@ pub fn to_closure_sig(
         fn_sig.requires.clone(),
         inputs.into(),
         output,
-        if no_panic { crate::rty::Expr::tt() } else { crate::rty::Expr::ff() },
+        no_panic,
         false,
     );
 
@@ -1616,7 +1616,7 @@ impl Ty {
         did: DefId,
         tys: impl Into<List<Ty>>,
         args: &flux_rustc_bridge::ty::GenericArgs,
-        no_panic: bool,
+        no_panic: rty::Expr,
     ) -> Ty {
         BaseTy::Closure(did, tys.into(), args.clone(), no_panic).to_ty()
     }
@@ -1830,7 +1830,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, rty::Expr),
     Coroutine(
         DefId,
         /*resume_ty: */ Ty,

crates/flux-refineck/src/checker.rs

@@ -943,6 +943,16 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
             .deeply_normalize(&mut infcx.at(span))
             .with_span(span)?;
 
+        // let caller_fn_name = tcx.def_path_str(self.checker_id.root_id().to_def_id());
+        // let caller_no_panic = self.fn_sig.no_panic();
+
+        // println!("caller: no panic for {} is {caller_no_panic:?}", caller_fn_name);
+
+        // let callee_fn_name = tcx.def_path_str(callee_def_id.unwrap());
+        // let callee_no_panic = fn_sig.no_panic();
+
+        // println!("callee: no panic for {} is {callee_no_panic:?}", callee_fn_name);
+
         let mut at = infcx.at(span);
 
         if let Some(callee_def_id) = callee_def_id