Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 30 additions & 0 deletions tests/ui/fail/loop_invariant_trait.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
//@error-in-other-file: Unsat
//@compile-flags: -C debug-assertions=off

#[thrust_macros::requires(true)]
#[thrust_macros::ensures(true)]
#[thrust::trusted]
fn rand() -> i64 { unimplemented!() }

#[thrust_macros::context]
trait Foo {
#[thrust_macros::invariant_context]
fn run(&mut self) {
let mut x: i64 = 0;
while rand() == 0 {
thrust_macros::invariant!(|x: i64| x >= 1);
x += 1;
}
assert!(x >= 0);
}
}

struct Bar;
impl thrust_models::Model for Bar {
type Ty = ();
}
impl Foo for Bar {}

fn main() {
Bar.run();
}
30 changes: 30 additions & 0 deletions tests/ui/pass/loop_invariant_trait.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
//@check-pass
//@compile-flags: -C debug-assertions=off

#[thrust_macros::requires(true)]
#[thrust_macros::ensures(true)]
#[thrust::trusted]
fn rand() -> i64 { unimplemented!() }

#[thrust_macros::context]
trait Foo {
#[thrust_macros::invariant_context]
fn run(&mut self) {
let mut x: i64 = 0;
while rand() == 0 {
thrust_macros::invariant!(|x: i64| x >= 0);
x += 1;
}
assert!(x >= 0);
}
}

struct Bar;
impl thrust_models::Model for Bar {
type Ty = ();
}
impl Foo for Bar {}

fn main() {
Bar.run();
}
6 changes: 5 additions & 1 deletion thrust-macros/src/invariant.rs
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,11 @@ fn expand_invariant(
}
rewriter.visit_expr_mut(&mut body);

if crate::tokens_contain_ident(&closure.to_token_stream(), "Self") {
let self_used = crate::tokens_contain_ident(&closure.to_token_stream(), "Self")
|| def_wheres
.iter()
.any(|pred| crate::tokens_contain_ident(&pred.to_token_stream(), "Self"));
Comment on lines +180 to +183

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Rewrite Self in copied generic parameter bounds

This detection still ignores Self that is copied through def_params, so trait methods with generic parameter bounds such as fn run<T: Marker<Self>>(&mut self) still expand to a nested formula function like fn _thrust_invariant_0<T: Marker<Self>, __ThrustSelf>(...), which triggers the same E0401 this change is trying to avoid. The branch rewrites parameters, the body, and def_wheres, but it never rewrites the generic parameter bounds already pushed into def_params; include those in the rewrite or move their bounds into the where-clause before rewriting.

Useful? React with 👍 / 👎.

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

out of PR scope

if self_used {
let Some(outer) = context.and_then(|context| context.outer.as_ref()) else {
return Err(syn::Error::new_spanned(
closure,
Expand Down