Add #[no_panic_if]

[nilehmann]

Based on #1387

[Copilot]

Pull request overview

This PR adds support for conditional no_panic specifications using the new #[flux::no_panic_if(expr)] attribute. This builds on PR #1387 and allows functions to specify conditional guarantees that they won't panic, based on refinement expressions. The old #[flux::no_panic] attribute (which is unconditional) is preserved, but using both attributes together is properly flagged as an error.

Changes:

• Introduces #[flux::no_panic_if(expr)] attribute for conditional panic specifications
• Updates the type system to treat no_panic as an expression (with true/false for the old boolean attribute)
• Adds duplicate attribute detection for no_panic and no_panic_if used together

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
tests/tests/neg/surface/no_panic03.rs	Tests duplicate attribute detection for no_panic + no_panic_if on function
tests/tests/neg/surface/no_panic04.rs	Tests conditional no_panic with traits using associated refinements
tests/tests/neg/surface/no_panic05.rs	Tests duplicate attribute detection for no_panic + no_panic_if(true)
crates/flux-syntax/src/symbols.rs	Adds no_panic_if symbol
crates/flux-syntax/src/surface/visit.rs	Updates visitor to traverse no_panic expression in FnSig
crates/flux-syntax/src/surface.rs	Adds no_panic field to FnSig surface syntax
crates/flux-syntax/src/parser/mod.rs	Adds parsing for no_panic_if attribute (contains critical bug)
crates/flux-refineck/src/checker.rs	Adds subtyping check for no_panic conditions using implication
crates/flux-middle/src/fhir.rs	Adds no_panic_if field to FHIR FnSig
crates/flux-fhir-analysis/src/conv/mod.rs	Converts no_panic_if expression and integrates with old boolean no_panic
crates/flux-driver/src/collector/mod.rs	Adds attribute collection and duplicate detection for no_panic_if
crates/flux-desugar/src/desugar/lift.rs	Initializes no_panic_if to None for lifted signatures
crates/flux-desugar/src/desugar.rs	Desugars no_panic_if expression from surface to FHIR

[Copilot]

The no_panic_if attribute parsing is missing the delimited wrapper to properly parse the parentheses around the expression. This is inconsistent with similar attributes like invariant (line 424) and refined_by (line 420).

The attribute is used as #[flux::no_panic_if(expr)] in tests (see tests/tests/neg/surface/no_panic03.rs and no_panic04.rs), which requires parentheses. However, the current implementation calls parse_expr(cx, true)? directly without using delimited(cx, Parenthesis, |cx| parse_expr(cx, true))?, which means the parser won't expect or consume the opening and closing parentheses.

This should be changed to match the pattern used by similar attributes.

Suggested change

	.push(SyntaxAttr::NoPanicIf(parse_expr(cx, true)?));
	.push(SyntaxAttr::NoPanicIf(delimited(cx, Parenthesis, |cx| parse_expr(cx, true))?));

[Copilot]

The nested if-else can be simplified for better readability. The inner if-expression can be converted to use then_some or restructured with the outer if-let pattern.

Suggested change

	} else {
	if self.genv().no_panic(fn_id) { Expr::tt() } else { Expr::ff() }
	} else if self.genv().no_panic(fn_id) {
	Expr::tt()
	} else {
	Expr::ff()

[Copilot]

This PR adds three negative test cases but no positive test cases for the no_panic_if feature. Positive test cases should be added to verify that the no_panic_if attribute works correctly when:

1. A simple condition like no_panic_if(true) is used with a function that doesn't panic
2. A conditional no_panic like no_panic_if(x > 0) is satisfied when calling the function with valid arguments
3. The trait/impl scenario from no_panic04.rs works correctly when the condition is true

These tests would ensure the feature works as expected, not just that errors are caught.

Suggested change

	}
	}
	// Positive test 1: simple no_panic_if(true) on a function that does not panic
	#[flux::no_panic_if(true)]
	fn my_fn_ok() -> i32 {
	42
	}
	// Positive test 2: conditional no_panic_if(x > 0) with a valid call
	#[flux::no_panic_if(x > 0)]
	fn my_fn_conditional(x: i32) -> i32 {
	x
	}
	fn use_my_fn_conditional() {
	let _ = my_fn_conditional(1);
	}
	// Positive test 3: trait/impl scenario where the condition is true
	trait NoPanicTrait {
	#[flux::no_panic_if(true)]
	fn do_something(&self) -> i32;
	}
	struct NoPanicImpl;
	impl NoPanicTrait for NoPanicImpl {
	#[flux::no_panic_if(true)]
	fn do_something(&self) -> i32 {
	0
	}
	}
	fn use_trait_impl() {
	let v = NoPanicImpl;
	let _ = v.do_something();
	}