Merge main

Author: nilehmann

crates/flux-desugar/src/desugar.rs

@@ -481,7 +481,7 @@ impl<'a, 'genv, 'tcx: 'genv> RustItemCtxt<'a, 'genv, 'tcx> {
         fn_sig: Option<&surface::FnSig>,
     ) -> Result<(fhir::Generics<'genv>, fhir::FnSig<'genv>)> {
         let mut header = self.lift_fn_header();
-        let (generics, decl) = if let Some(fn_sig) = fn_sig {
+        let (generics, decl, expr) = if let Some(fn_sig) = fn_sig {
             self.fn_sig_scope = Some(fn_sig.node_id);
 
             let mut requires = vec![];
@@ -510,18 +510,20 @@ impl<'a, 'genv, 'tcx: 'genv> RustItemCtxt<'a, 'genv, 'tcx> {
                 span: fn_sig.span,
                 lifted: false,
             };
+
             // Fix up the span in asyncness
             if let surface::Async::Yes { span, .. } = fn_sig.asyncness {
                 header.asyncness = hir::IsAsync::Async(span);
             }
-            (generics, decl)
+            let expr = fn_sig.no_panic.as_ref().map(|e| self.desugar_expr(e));
+            (generics, decl, expr)
         } else {
-            (self.lift_generics(), self.lift_fn_decl())
+            (self.lift_generics(), self.lift_fn_decl(), None)
         };
         if config::dump_fhir() {
             dbg::dump_item_info(self.genv.tcx(), self.owner.local_id(), "fhir", decl).unwrap();
         }
-        Ok((generics, fhir::FnSig { header, decl: self.genv.alloc(decl) }))
+        Ok((generics, fhir::FnSig { header, decl: self.genv.alloc(decl), no_panic_if: expr }))
     }
 
     fn desugar_fn_sig_refine_params(

crates/flux-desugar/src/desugar/lift.rs

@@ -542,7 +542,7 @@ impl<'genv> RustItemCtxt<'_, 'genv, '_> {
 
     fn lift_fn_sig(&mut self, fn_sig: hir::FnSig) -> fhir::FnSig<'genv> {
         let decl = self.lift_fn_decl_inner(fn_sig.span, fn_sig.decl);
-        fhir::FnSig { header: fn_sig.header, decl: self.genv.alloc(decl) }
+        fhir::FnSig { header: fn_sig.header, decl: self.genv.alloc(decl), no_panic_if: None }
     }
 
     pub(crate) fn lift_foreign_item(

crates/flux-driver/src/collector/mod.rs

@@ -524,6 +524,9 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
             ("invariant", hir::AttrArgs::Delimited(dargs)) => {
                 self.parse(dargs, ParseSess::parse_expr, FluxAttrKind::Invariant)?
             }
+            ("no_panic_if", hir::AttrArgs::Delimited(dargs)) => {
+                self.parse(dargs, ParseSess::parse_expr, FluxAttrKind::NoPanicIf)?
+            }
             ("constant", hir::AttrArgs::Delimited(dargs)) => {
                 self.parse(dargs, ParseSess::parse_constant_info, FluxAttrKind::Constant)?
             }
@@ -587,6 +590,16 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
 
     fn report_dups(&mut self, attrs: &FluxAttrs) -> Result {
         let mut err = None;
+
+        // look for a NoPanic and a NoPanicIf
+        let has_no_panic_if = attrs.has_no_panic_if();
+        if has_no_panic_if && let Some(no_panic_attr_span) = attrs.has_no_panic() {
+            err.collect(self.errors.emit(errors::DuplicatedAttr {
+                span: no_panic_attr_span,
+                name: "NoPanic and NoPanicIf",
+            }));
+        }
+
         for (name, dups) in attrs.dups() {
             for attr in dups {
                 if attr.allow_dups() {
@@ -671,6 +684,7 @@ enum FluxAttrKind {
     ShouldFail,
     ExternSpec,
     NoPanic,
+    NoPanicIf(surface::Expr),
     /// See `detachXX.rs`
     DetachedSpecs(surface::DetachedSpecs),
 }
@@ -741,7 +755,13 @@ impl FluxAttrs {
     }
 
     fn fn_sig(&mut self) -> Option<surface::FnSig> {
-        read_attr!(self, FnSig)
+        let mut fn_sig = read_attr!(self, FnSig);
+        // FIXME(nilehmann) the `no_panic_if` annotation should work even if there's no `flux::spec`
+        // annotation or we should at least show an error.
+        if let Some(fn_sig) = &mut fn_sig {
+            fn_sig.no_panic = read_attr!(self, NoPanicIf);
+        }
+        fn_sig
     }
 
     fn ty_alias(&mut self) -> Option<Box<surface::TyAlias>> {
@@ -756,6 +776,17 @@ impl FluxAttrs {
         read_attr!(self, Generics)
     }
 
+    fn has_no_panic(&self) -> Option<Span> {
+        self.map
+            .get(attr_name!(NoPanic))
+            .and_then(|attrs| attrs.first())
+            .map(|attr| attr.span)
+    }
+
+    fn has_no_panic_if(&self) -> bool {
+        read_flag!(self, NoPanicIf)
+    }
+
     fn trait_assoc_refts(&mut self) -> Vec<surface::TraitAssocReft> {
         read_attrs!(self, TraitAssocReft)
             .into_iter()
@@ -821,7 +852,8 @@ impl FluxAttrs {
                 | FluxAttrKind::Variant(_)
                 | FluxAttrKind::Invariant(_)
                 | FluxAttrKind::ExternSpec
-                | FluxAttrKind::DetachedSpecs(_) => continue,
+                | FluxAttrKind::DetachedSpecs(_)
+                | FluxAttrKind::NoPanicIf(_) => continue,
             };
             attrs.push(attr);
         }
@@ -856,6 +888,7 @@ impl FluxAttrKind {
             FluxAttrKind::ExternSpec => attr_name!(ExternSpec),
             FluxAttrKind::DetachedSpecs(_) => attr_name!(DetachedSpecs),
             FluxAttrKind::NoPanic => attr_name!(NoPanic),
+            FluxAttrKind::NoPanicIf(_) => attr_name!(NoPanicIf),
         }
     }
 }

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

@@ -671,7 +671,12 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
         env.push_layer(Layer::list(self.results(), late_bound_regions.len() as u32, &[]));
 
         let body_id = self.tcx().hir_node_by_def_id(fn_id.local_id()).body_id();
-        let no_panic = self.genv().no_panic(fn_id);
+
+        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() }
+        };
 
         let fn_sig =
             self.conv_fn_decl(&mut env, header.safety(), header.abi, decl, body_id, no_panic)?;
@@ -986,7 +991,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
         abi: rustc_abi::ExternAbi,
         decl: &fhir::FnDecl,
         body_id: Option<BodyId>,
-        no_panic: bool,
+        no_panic: Expr,
     ) -> QueryResult<rty::FnSig> {
         let mut requires = vec![];
         for req in decl.requires {
@@ -1015,7 +1020,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
             requires.into(),
             inputs.into(),
             output,
-            if no_panic { Expr::tt() } else { Expr::ff() },
+            no_panic,
             decl.lifted,
         ))
     }
@@ -1260,7 +1265,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
                     bare_fn.abi,
                     bare_fn.decl,
                     None,
-                    false,
+                    Expr::ff(),
                 )?;
                 let vars = bare_fn
                     .generic_params

crates/flux-middle/src/fhir.rs

@@ -512,6 +512,7 @@ pub struct Requires<'fhir> {
 pub struct FnSig<'fhir> {
     pub header: FnHeader,
     pub decl: &'fhir FnDecl<'fhir>,
+    pub no_panic_if: Option<Expr<'fhir>>,
 }
 
 #[derive(Clone, Copy)]

crates/flux-refineck/src/checker.rs

@@ -312,6 +312,10 @@ fn check_fn_subtyping(
         for requires in super_sig.requires() {
             infcx.assume_pred(requires);
         }
+        infcx.check_pred(
+            Expr::implies(super_sig.no_panic(), sub_sig.no_panic()),
+            ConstrReason::Subtype(SubtypeReason::Input),
+        );
         for (actual, formal) in iter::zip(actuals, sub_sig.inputs()) {
             let reason = ConstrReason::Subtype(SubtypeReason::Input);
             infcx.subtyping_with_env(&mut env, &actual, formal, reason)?;

crates/flux-syntax/src/parser/mod.rs

@@ -53,6 +53,8 @@ enum SyntaxAttr {
     Hide,
     /// a `#[opaque]` attribute
     Opaque,
+    /// A `#[no_panic_if(...)]` attribute
+    NoPanicIf(Expr),
 }
 
 #[derive(Default)]
@@ -92,6 +94,14 @@ impl ParsedAttrs {
         }
     }
 
+    fn no_panic_if(&mut self) -> Option<Expr> {
+        let pos = self
+            .syntax
+            .iter()
+            .position(|x| matches!(x, SyntaxAttr::NoPanicIf(_)))?;
+        if let SyntaxAttr::NoPanicIf(expr) = self.syntax.remove(pos) { Some(expr) } else { None }
+    }
+
     fn invariant(&mut self) -> Option<Expr> {
         let pos = self
             .syntax
@@ -278,9 +288,10 @@ fn ident_path(cx: &mut ParseCtxt, ident: Ident) -> ExprPath {
 
 fn parse_detached_fn_sig(
     cx: &mut ParseCtxt,
-    attrs: ParsedAttrs,
+    mut attrs: ParsedAttrs,
 ) -> ParseResult<DetachedItem<FnSig>> {
-    let fn_sig = parse_fn_sig(cx, token::Semi)?;
+    let mut fn_sig = parse_fn_sig(cx, token::Semi)?;
+    fn_sig.no_panic = attrs.no_panic_if();
     let span = fn_sig.span;
     let ident = fn_sig
         .ident
@@ -411,6 +422,10 @@ fn parse_attr(cx: &mut ParseCtxt, attrs: &mut ParsedAttrs) -> ParseResult {
         attrs
             .syntax
             .push(SyntaxAttr::Invariant(delimited(cx, Parenthesis, |cx| parse_expr(cx, true))?));
+    } else if lookahead.advance_if(sym::no_panic_if) {
+        attrs
+            .syntax
+            .push(SyntaxAttr::NoPanicIf(parse_expr(cx, true)?));
     } else {
         return Err(lookahead.into_error());
     };
@@ -768,6 +783,7 @@ pub(crate) fn parse_fn_sig<T: PeekExpected>(cx: &mut ParseCtxt, end: T) -> Parse
         output: FnOutput { returns, ensures, node_id: cx.next_node_id() },
         node_id: cx.next_node_id(),
         span: cx.mk_span(lo, hi),
+        no_panic: None, // We attach the `no_panic` expr later
     })
 }
 

crates/flux-syntax/src/surface.rs

@@ -354,6 +354,7 @@ pub struct FnSig {
     /// source span
     pub span: Span,
     pub node_id: NodeId,
+    pub no_panic: Option<Expr>,
 }
 
 #[derive(Debug)]

crates/flux-syntax/src/surface/visit.rs

@@ -414,6 +414,9 @@ pub fn walk_fn_sig<V: Visitor>(vis: &mut V, fn_sig: &FnSig) {
         vis.visit_expr(&requires.pred);
     }
     walk_list!(vis, visit_fn_input, &fn_sig.inputs);
+    if let Some(no_panic_expr) = &fn_sig.no_panic {
+        vis.visit_expr(no_panic_expr);
+    }
     vis.visit_fn_output(&fn_sig.output);
 }
 

crates/flux-syntax/src/symbols.rs

@@ -25,6 +25,7 @@ symbols! {
         Set,
         int,
         no_panic,
+        no_panic_if,
         ptr_size,
         real,
     }