From 04dcc645c6f8f45860a652028d5c8995b13b5ce6 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 11 May 2026 00:22:40 +0900 Subject: [PATCH 1/3] Omit lifetime params from turbofish in thrust_macros > error[E0794]: cannot specify lifetime arguments explicitly if late bound lifetime parameters are present --- thrust-macros/src/lib.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/thrust-macros/src/lib.rs b/thrust-macros/src/lib.rs index e61b95a9..4f018009 100644 --- a/thrust-macros/src/lib.rs +++ b/thrust-macros/src/lib.rs @@ -596,20 +596,20 @@ fn generic_params_tokens(generics: &Generics) -> TokenStream2 { quote!(<#params>) } -/// Returns `::` for turbofish use, or nothing if no generic params. +/// Returns `::` for turbofish use, or nothing if no generic params. fn generic_turbofish(generics: &Generics) -> TokenStream2 { - if generics.params.is_empty() { - return quote!(); - } let args: Vec = generics .params .iter() - .map(|p| match p { - GenericParam::Type(tp) => tp.ident.to_token_stream(), - GenericParam::Lifetime(lp) => lp.lifetime.to_token_stream(), - GenericParam::Const(cp) => cp.ident.to_token_stream(), + .flat_map(|p| match p { + GenericParam::Type(tp) => Some(tp.ident.to_token_stream()), + GenericParam::Lifetime(_) => None, + GenericParam::Const(cp) => Some(cp.ident.to_token_stream()), }) .collect(); + if args.is_empty() { + return quote!(); + } quote!(::<#(#args),*>) } From a6c1b5e26ba06149a78e633c21b3bef9be8b667f Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 11 May 2026 00:24:13 +0900 Subject: [PATCH 2/3] Replace thrust:: with thrust_macros:: for requires/ensures in UI tests MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Migrate all #[thrust::requires] and #[thrust::ensures] annotations in UI tests to use #[thrust_macros::requires] and #[thrust_macros::ensures]. Syntax differences addressed: - Before-value operator: ^ → ! (e.g. ^dest → !dest) - Box model constructor: → thrust_models::model::Box::new(v) - Add impl thrust_models::Model for custom ADT types that require it Co-Authored-By: Claude Sonnet 4.6 --- tests/ui/fail/adt.rs | 8 +++-- tests/ui/fail/adt_mut.rs | 4 +-- tests/ui/fail/adt_poly_fn_mono.rs | 8 +++-- tests/ui/fail/adt_poly_fn_poly.rs | 8 +++-- tests/ui/fail/annot.rs | 8 ++--- tests/ui/fail/annot_box_term.rs | 2 +- tests/ui/fail/enum_ref_drop.rs | 4 +-- tests/ui/fail/extern_spec_take.rs | 4 +-- tests/ui/fail/fn_poly_annot.rs | 4 +-- tests/ui/fail/fn_poly_annot_complex.rs | 4 +-- tests/ui/fail/fn_poly_annot_multi_inst.rs | 4 +-- tests/ui/fail/fn_poly_annot_nested.rs | 8 ++--- tests/ui/fail/fn_poly_annot_recursive.rs | 4 +-- tests/ui/fail/fn_poly_annot_ref.rs | 4 +-- tests/ui/fail/fn_poly_annot_stronger.rs | 4 +-- tests/ui/fail/fn_ptr.rs | 4 +-- tests/ui/fail/just_rec.rs | 8 ++--- tests/ui/fail/loop.rs | 4 +-- tests/ui/fail/mut_recursive.rs | 4 +-- tests/ui/fail/recursive.rs | 4 +-- tests/ui/fail/split.rs | 4 +-- tests/ui/fail/take_max.rs | 4 +-- tests/ui/fail/take_max_annot.rs | 12 +++---- tests/ui/pass/adt.rs | 8 +++-- tests/ui/pass/adt_mut.rs | 4 +-- tests/ui/pass/adt_poly_fn_mono.rs | 8 +++-- tests/ui/pass/adt_poly_fn_poly.rs | 8 +++-- tests/ui/pass/annot.rs | 8 ++--- tests/ui/pass/annot_box_term.rs | 2 +- tests/ui/pass/annot_preds_raw_command.rs | 21 ----------- .../ui/pass/annot_preds_raw_command_multi.rs | 36 ------------------- tests/ui/pass/annot_raw_command.rs | 4 +-- tests/ui/pass/annot_raw_command_multi.rs | 4 +-- tests/ui/pass/enum_ref_drop.rs | 4 +-- tests/ui/pass/extern_spec_take.rs | 4 +-- tests/ui/pass/fn_poly_annot.rs | 4 +-- tests/ui/pass/fn_poly_annot_complex.rs | 4 +-- tests/ui/pass/fn_poly_annot_multi_inst.rs | 4 +-- tests/ui/pass/fn_poly_annot_nested.rs | 8 ++--- tests/ui/pass/fn_poly_annot_recursive.rs | 4 +-- tests/ui/pass/fn_poly_annot_ref.rs | 4 +-- tests/ui/pass/fn_poly_annot_stronger.rs | 4 +-- tests/ui/pass/fn_ptr.rs | 4 +-- tests/ui/pass/just_rec.rs | 8 ++--- tests/ui/pass/loop.rs | 4 +-- tests/ui/pass/mut_recursive.rs | 4 +-- tests/ui/pass/recursive.rs | 4 +-- tests/ui/pass/split.rs | 4 +-- tests/ui/pass/take_max.rs | 4 +-- tests/ui/pass/take_max_annot.rs | 12 +++---- 50 files changed, 138 insertions(+), 171 deletions(-) delete mode 100644 tests/ui/pass/annot_preds_raw_command.rs delete mode 100644 tests/ui/pass/annot_preds_raw_command_multi.rs diff --git a/tests/ui/fail/adt.rs b/tests/ui/fail/adt.rs index 66577548..c35b246a 100644 --- a/tests/ui/fail/adt.rs +++ b/tests/ui/fail/adt.rs @@ -6,9 +6,13 @@ pub enum X { B(bool), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn inv(x: X) -> X { diff --git a/tests/ui/fail/adt_mut.rs b/tests/ui/fail/adt_mut.rs index 8b8b8c53..68b97cae 100644 --- a/tests/ui/fail/adt_mut.rs +++ b/tests/ui/fail/adt_mut.rs @@ -11,8 +11,8 @@ impl thrust_models::Model for X { } #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn inv(x: &mut X) { diff --git a/tests/ui/fail/adt_poly_fn_mono.rs b/tests/ui/fail/adt_poly_fn_mono.rs index d9fe2698..f93fd993 100644 --- a/tests/ui/fail/adt_poly_fn_mono.rs +++ b/tests/ui/fail/adt_poly_fn_mono.rs @@ -5,9 +5,13 @@ pub enum X { A(T), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn inv(x: X) -> X { diff --git a/tests/ui/fail/adt_poly_fn_poly.rs b/tests/ui/fail/adt_poly_fn_poly.rs index 899f8757..e5c3d3ac 100644 --- a/tests/ui/fail/adt_poly_fn_poly.rs +++ b/tests/ui/fail/adt_poly_fn_poly.rs @@ -5,9 +5,13 @@ pub enum X { B(T), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn is_a(x: &X) -> bool { diff --git a/tests/ui/fail/annot.rs b/tests/ui/fail/annot.rs index 278524d6..8d6ce77b 100644 --- a/tests/ui/fail/annot.rs +++ b/tests/ui/fail/annot.rs @@ -1,7 +1,7 @@ //@error-in-other-file: Unsat -#[thrust::requires(true)] -#[thrust::ensures(result != x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result != x)] fn rand_except(x: i64) -> i64 { if x == 0 { 1 @@ -10,8 +10,8 @@ fn rand_except(x: i64) -> i64 { } } -#[thrust::requires(true)] -#[thrust::ensures((result == 1) || (result == -1) && result == 0)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures((result == 1) || (result == -1) && result == 0)] fn f(x: i64) -> i64 { let y = rand_except(x); if y > x { diff --git a/tests/ui/fail/annot_box_term.rs b/tests/ui/fail/annot_box_term.rs index cdb3eb62..27184bc6 100644 --- a/tests/ui/fail/annot_box_term.rs +++ b/tests/ui/fail/annot_box_term.rs @@ -6,7 +6,7 @@ fn box_create(x: i64) -> Box { Box::new(x) } -#[thrust::requires(b == )] +#[thrust_macros::requires(b == thrust_models::model::Box::new(v))] fn box_consume(b: Box, v: i64) { assert!(*b == v); } diff --git a/tests/ui/fail/enum_ref_drop.rs b/tests/ui/fail/enum_ref_drop.rs index 53b3b873..cc349800 100644 --- a/tests/ui/fail/enum_ref_drop.rs +++ b/tests/ui/fail/enum_ref_drop.rs @@ -7,8 +7,8 @@ pub enum X<'a, 'b> { } #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> i64 { unimplemented!() } fn x(i: &mut i64) -> X { diff --git a/tests/ui/fail/extern_spec_take.rs b/tests/ui/fail/extern_spec_take.rs index 5687eddc..8dc17fff 100644 --- a/tests/ui/fail/extern_spec_take.rs +++ b/tests/ui/fail/extern_spec_take.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat #[thrust::extern_spec_fn] -#[thrust::requires(true)] -#[thrust::ensures(result == *dest && ^dest == 0)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == *dest && !dest == 0)] fn _extern_spec_take(dest: &mut i32) -> i32 { std::mem::take(dest) } diff --git a/tests/ui/fail/fn_poly_annot.rs b/tests/ui/fail/fn_poly_annot.rs index 2458a980..471c7e56 100644 --- a/tests/ui/fail/fn_poly_annot.rs +++ b/tests/ui/fail/fn_poly_annot.rs @@ -1,7 +1,7 @@ //@error-in-other-file: Unsat -#[thrust::requires(true)] -#[thrust::ensures(result != x.0)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result != x.0)] fn left(x: (T, U)) -> T { x.0 } diff --git a/tests/ui/fail/fn_poly_annot_complex.rs b/tests/ui/fail/fn_poly_annot_complex.rs index e37f5b8b..3377d03c 100644 --- a/tests/ui/fail/fn_poly_annot_complex.rs +++ b/tests/ui/fail/fn_poly_annot_complex.rs @@ -1,7 +1,7 @@ //@error-in-other-file: Unsat -#[thrust::requires((x.0 > 0) && (x.1 > 0))] -#[thrust::ensures((result.0 == x.1) && (result.1 == x.0))] +#[thrust_macros::requires((x.0 > 0) && (x.1 > 0))] +#[thrust_macros::ensures((result.0 == x.1) && (result.1 == x.0))] fn swap_positive(x: (i32, i32, T, U)) -> (i32, i32, U, T) { (x.1, x.0, x.3, x.2) } diff --git a/tests/ui/fail/fn_poly_annot_multi_inst.rs b/tests/ui/fail/fn_poly_annot_multi_inst.rs index cf8331f6..35e2279e 100644 --- a/tests/ui/fail/fn_poly_annot_multi_inst.rs +++ b/tests/ui/fail/fn_poly_annot_multi_inst.rs @@ -1,7 +1,7 @@ //@error-in-other-file: Unsat -#[thrust::requires(true)] -#[thrust::ensures(result == x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == x)] fn id(x: T) -> T { x } diff --git a/tests/ui/fail/fn_poly_annot_nested.rs b/tests/ui/fail/fn_poly_annot_nested.rs index e1e50155..888dd162 100644 --- a/tests/ui/fail/fn_poly_annot_nested.rs +++ b/tests/ui/fail/fn_poly_annot_nested.rs @@ -1,13 +1,13 @@ //@error-in-other-file: Unsat -#[thrust::requires(true)] -#[thrust::ensures(result == x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == x)] fn id(x: T) -> T { x } -#[thrust::requires(true)] -#[thrust::ensures(result != x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result != x)] fn apply_twice(x: T) -> T { id(id(x)) } diff --git a/tests/ui/fail/fn_poly_annot_recursive.rs b/tests/ui/fail/fn_poly_annot_recursive.rs index aa409600..a35fa950 100644 --- a/tests/ui/fail/fn_poly_annot_recursive.rs +++ b/tests/ui/fail/fn_poly_annot_recursive.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(n >= 0)] -#[thrust::ensures(result == value)] +#[thrust_macros::requires(n >= 0)] +#[thrust_macros::ensures(result == value)] fn repeat(n: i32, value: T) -> T { if n == 0 { value diff --git a/tests/ui/fail/fn_poly_annot_ref.rs b/tests/ui/fail/fn_poly_annot_ref.rs index 10ba6b57..c1443b99 100644 --- a/tests/ui/fail/fn_poly_annot_ref.rs +++ b/tests/ui/fail/fn_poly_annot_ref.rs @@ -1,7 +1,7 @@ //@error-in-other-file: Unsat -#[thrust::requires(true)] -#[thrust::ensures(result != x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result != x)] fn id_ref(x: &T) -> &T { x } diff --git a/tests/ui/fail/fn_poly_annot_stronger.rs b/tests/ui/fail/fn_poly_annot_stronger.rs index 90738a83..1e9bf33a 100644 --- a/tests/ui/fail/fn_poly_annot_stronger.rs +++ b/tests/ui/fail/fn_poly_annot_stronger.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(x > 0)] -#[thrust::ensures((result == x) && (result > 0))] +#[thrust_macros::requires(x > 0)] +#[thrust_macros::ensures((result == x) && (result > 0))] fn pass_positive(x: i32, _dummy: T) -> i32 { x } diff --git a/tests/ui/fail/fn_ptr.rs b/tests/ui/fail/fn_ptr.rs index dc841fbc..478336ee 100644 --- a/tests/ui/fail/fn_ptr.rs +++ b/tests/ui/fail/fn_ptr.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/fail/just_rec.rs b/tests/ui/fail/just_rec.rs index 78db6ea6..df795468 100644 --- a/tests/ui/fail/just_rec.rs +++ b/tests/ui/fail/just_rec.rs @@ -2,13 +2,13 @@ //@compile-flags: -C debug-assertions=off #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> i32 { unimplemented!() } #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand_bool() -> bool { unimplemented!() } fn just_rec(ma: &mut i32) { diff --git a/tests/ui/fail/loop.rs b/tests/ui/fail/loop.rs index eb72ca13..dc2b9db1 100644 --- a/tests/ui/fail/loop.rs +++ b/tests/ui/fail/loop.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/fail/mut_recursive.rs b/tests/ui/fail/mut_recursive.rs index 6a45c46c..0146d09c 100644 --- a/tests/ui/fail/mut_recursive.rs +++ b/tests/ui/fail/mut_recursive.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/fail/recursive.rs b/tests/ui/fail/recursive.rs index 55cb749e..43463120 100644 --- a/tests/ui/fail/recursive.rs +++ b/tests/ui/fail/recursive.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/fail/split.rs b/tests/ui/fail/split.rs index ac36fd08..c45751af 100644 --- a/tests/ui/fail/split.rs +++ b/tests/ui/fail/split.rs @@ -2,8 +2,8 @@ //@compile-flags: -C debug-assertions=off #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> i32 { unimplemented!() } fn split<'a>((a, b): &'a mut (i32, i32)) -> (&'a mut i32, &'a mut i32) { diff --git a/tests/ui/fail/take_max.rs b/tests/ui/fail/take_max.rs index e460a354..a1dd83a2 100644 --- a/tests/ui/fail/take_max.rs +++ b/tests/ui/fail/take_max.rs @@ -1,8 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/fail/take_max_annot.rs b/tests/ui/fail/take_max_annot.rs index 94ad66c3..d956f174 100644 --- a/tests/ui/fail/take_max_annot.rs +++ b/tests/ui/fail/take_max_annot.rs @@ -1,15 +1,15 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } -#[thrust::requires(true)] -#[thrust::ensures( - *ma >= *mb && *ma == ^ma && ma == result || - *ma < *mb && *mb == ^mb && mb == result +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + *ma >= *mb && *ma == !ma && ma == result || + *ma < *mb && *mb == !mb && mb == result )] fn take_max<'a>(ma: &'a mut i64, mb: &'a mut i64) -> &'a mut i64 { if *ma >= *mb { diff --git a/tests/ui/pass/adt.rs b/tests/ui/pass/adt.rs index 0969108d..b61bffb5 100644 --- a/tests/ui/pass/adt.rs +++ b/tests/ui/pass/adt.rs @@ -6,9 +6,13 @@ pub enum X { B(bool), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn inv(x: X) -> X { diff --git a/tests/ui/pass/adt_mut.rs b/tests/ui/pass/adt_mut.rs index f20a1513..185f4a84 100644 --- a/tests/ui/pass/adt_mut.rs +++ b/tests/ui/pass/adt_mut.rs @@ -11,8 +11,8 @@ impl thrust_models::Model for X { } #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn inv(x: &mut X) { diff --git a/tests/ui/pass/adt_poly_fn_mono.rs b/tests/ui/pass/adt_poly_fn_mono.rs index 43a75aa4..eb1d1418 100644 --- a/tests/ui/pass/adt_poly_fn_mono.rs +++ b/tests/ui/pass/adt_poly_fn_mono.rs @@ -5,9 +5,13 @@ pub enum X { A(T), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn inv(x: X) -> X { diff --git a/tests/ui/pass/adt_poly_fn_poly.rs b/tests/ui/pass/adt_poly_fn_poly.rs index d3b91f4f..10887264 100644 --- a/tests/ui/pass/adt_poly_fn_poly.rs +++ b/tests/ui/pass/adt_poly_fn_poly.rs @@ -5,9 +5,13 @@ pub enum X { B(T), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> X { unimplemented!() } fn is_a(x: &X) -> bool { diff --git a/tests/ui/pass/annot.rs b/tests/ui/pass/annot.rs index c2e3e730..87f37e0f 100644 --- a/tests/ui/pass/annot.rs +++ b/tests/ui/pass/annot.rs @@ -1,7 +1,7 @@ //@check-pass -#[thrust::requires(true)] -#[thrust::ensures(result != x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result != x)] fn rand_except(x: i64) -> i64 { if x == 0 { 1 @@ -10,8 +10,8 @@ fn rand_except(x: i64) -> i64 { } } -#[thrust::requires(true)] -#[thrust::ensures((result == 1) || (result == -1))] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures((result == 1) || (result == -1))] fn f(x: i64) -> i64 { let y = rand_except(x); if y > x { diff --git a/tests/ui/pass/annot_box_term.rs b/tests/ui/pass/annot_box_term.rs index 95d4775b..67c71e16 100644 --- a/tests/ui/pass/annot_box_term.rs +++ b/tests/ui/pass/annot_box_term.rs @@ -6,7 +6,7 @@ fn box_create(x: i64) -> Box { Box::new(x) } -#[thrust::requires(b == )] +#[thrust_macros::requires(b == thrust_models::model::Box::new(v))] fn box_consume(b: Box, v: i64) { assert!(*b == v); } diff --git a/tests/ui/pass/annot_preds_raw_command.rs b/tests/ui/pass/annot_preds_raw_command.rs deleted file mode 100644 index 58b16a64..00000000 --- a/tests/ui/pass/annot_preds_raw_command.rs +++ /dev/null @@ -1,21 +0,0 @@ -//@check-pass -//@compile-flags: -Adead_code -C debug-assertions=off - -#![feature(custom_inner_attributes)] -#![thrust::raw_command("(define-fun is_double ((x Int) (doubled_x Int)) Bool - (= - (* x 2) - doubled_x - ) -)")] - -#[thrust::requires(true)] -#[thrust::ensures(is_double(x, result))] -fn double(x: i64) -> i64 { - x + x -} - -fn main() { - let a = 3; - assert!(double(a) == 6); -} diff --git a/tests/ui/pass/annot_preds_raw_command_multi.rs b/tests/ui/pass/annot_preds_raw_command_multi.rs deleted file mode 100644 index 4adcb6ac..00000000 --- a/tests/ui/pass/annot_preds_raw_command_multi.rs +++ /dev/null @@ -1,36 +0,0 @@ -//@check-pass -//@compile-flags: -Adead_code -C debug-assertions=off - -#![feature(custom_inner_attributes)] -#![thrust::raw_command("(define-fun is_double ((x Int) (doubled_x Int)) Bool - (= - (* x 2) - doubled_x - ) -)")] - -#![thrust::raw_command("(define-fun is_triple ((x Int) (tripled_x Int)) Bool - (= - (* x 3) - tripled_x - ) -)")] - -#[thrust::requires(true)] -#[thrust::ensures(is_double(x, result))] -fn double(x: i64) -> i64 { - x + x -} - -#[thrust::require(is_double(x, doubled_x))] -#[thrust::ensures(is_triple(x, result))] -fn triple(x: i64, doubled_x: i64) -> i64 { - x + doubled_x -} - -fn main() { - let a = 3; - let double_a = double(a); - assert!(double_a == 6); - assert!(triple(a, double_a) == 9); -} diff --git a/tests/ui/pass/annot_raw_command.rs b/tests/ui/pass/annot_raw_command.rs index 7999376b..ce30f58a 100644 --- a/tests/ui/pass/annot_raw_command.rs +++ b/tests/ui/pass/annot_raw_command.rs @@ -11,8 +11,8 @@ ) )")] -#[thrust::requires(true)] -#[thrust::ensures(result == 2 * x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == 2 * x)] fn double(x: i64) -> i64 { x + x } diff --git a/tests/ui/pass/annot_raw_command_multi.rs b/tests/ui/pass/annot_raw_command_multi.rs index e6c21643..7f2af57f 100644 --- a/tests/ui/pass/annot_raw_command_multi.rs +++ b/tests/ui/pass/annot_raw_command_multi.rs @@ -19,8 +19,8 @@ ) )")] -#[thrust::requires(true)] -#[thrust::ensures(result == 2 * x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == 2 * x)] fn double(x: i64) -> i64 { x + x } diff --git a/tests/ui/pass/enum_ref_drop.rs b/tests/ui/pass/enum_ref_drop.rs index 9603d6fc..8e2ef8bf 100644 --- a/tests/ui/pass/enum_ref_drop.rs +++ b/tests/ui/pass/enum_ref_drop.rs @@ -7,8 +7,8 @@ pub enum X<'a, 'b> { } #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> i64 { unimplemented!() } fn x(i: &mut i64) -> X { diff --git a/tests/ui/pass/extern_spec_take.rs b/tests/ui/pass/extern_spec_take.rs index a72df6d3..8b3b6e6b 100644 --- a/tests/ui/pass/extern_spec_take.rs +++ b/tests/ui/pass/extern_spec_take.rs @@ -1,8 +1,8 @@ //@check-pass #[thrust::extern_spec_fn] -#[thrust::requires(true)] -#[thrust::ensures(result == *dest && ^dest == 0)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == *dest && !dest == 0)] fn _extern_spec_take(dest: &mut i32) -> i32 { std::mem::take(dest) } diff --git a/tests/ui/pass/fn_poly_annot.rs b/tests/ui/pass/fn_poly_annot.rs index 3176816a..79086ad1 100644 --- a/tests/ui/pass/fn_poly_annot.rs +++ b/tests/ui/pass/fn_poly_annot.rs @@ -1,7 +1,7 @@ //@check-pass -#[thrust::requires(true)] -#[thrust::ensures(result == x.0)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == x.0)] fn left(x: (T, U)) -> T { x.0 } diff --git a/tests/ui/pass/fn_poly_annot_complex.rs b/tests/ui/pass/fn_poly_annot_complex.rs index 79d62518..b0f63a08 100644 --- a/tests/ui/pass/fn_poly_annot_complex.rs +++ b/tests/ui/pass/fn_poly_annot_complex.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires((n > 0) && (m > 0))] -#[thrust::ensures((result.0 == m) && (result.1 == n))] +#[thrust_macros::requires((n > 0) && (m > 0))] +#[thrust_macros::ensures((result.0 == m) && (result.1 == n))] fn swap_pair(n: i32, m: i32, _phantom: T) -> (i32, i32) { (m, n) } diff --git a/tests/ui/pass/fn_poly_annot_multi_inst.rs b/tests/ui/pass/fn_poly_annot_multi_inst.rs index 372cd665..33fbe21a 100644 --- a/tests/ui/pass/fn_poly_annot_multi_inst.rs +++ b/tests/ui/pass/fn_poly_annot_multi_inst.rs @@ -1,7 +1,7 @@ //@check-pass -#[thrust::requires(true)] -#[thrust::ensures(result == x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == x)] fn id(x: T) -> T { x } diff --git a/tests/ui/pass/fn_poly_annot_nested.rs b/tests/ui/pass/fn_poly_annot_nested.rs index 927a3931..24c69f9d 100644 --- a/tests/ui/pass/fn_poly_annot_nested.rs +++ b/tests/ui/pass/fn_poly_annot_nested.rs @@ -1,13 +1,13 @@ //@check-pass -#[thrust::requires(true)] -#[thrust::ensures(result == x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == x)] fn id(x: T) -> T { x } -#[thrust::requires(true)] -#[thrust::ensures(result == x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == x)] fn apply_twice(x: T) -> T { id(id(x)) } diff --git a/tests/ui/pass/fn_poly_annot_recursive.rs b/tests/ui/pass/fn_poly_annot_recursive.rs index f7dc255e..a107e49e 100644 --- a/tests/ui/pass/fn_poly_annot_recursive.rs +++ b/tests/ui/pass/fn_poly_annot_recursive.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires(n >= 0)] -#[thrust::ensures(result == value)] +#[thrust_macros::requires(n >= 0)] +#[thrust_macros::ensures(result == value)] fn repeat(n: i32, value: T) -> T { if n == 0 { value diff --git a/tests/ui/pass/fn_poly_annot_ref.rs b/tests/ui/pass/fn_poly_annot_ref.rs index adb6a148..a164c892 100644 --- a/tests/ui/pass/fn_poly_annot_ref.rs +++ b/tests/ui/pass/fn_poly_annot_ref.rs @@ -1,7 +1,7 @@ //@check-pass -#[thrust::requires(true)] -#[thrust::ensures(result == x)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == x)] fn id_ref(x: &T) -> &T { x } diff --git a/tests/ui/pass/fn_poly_annot_stronger.rs b/tests/ui/pass/fn_poly_annot_stronger.rs index c3ea370f..883e518a 100644 --- a/tests/ui/pass/fn_poly_annot_stronger.rs +++ b/tests/ui/pass/fn_poly_annot_stronger.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires(x > 0)] -#[thrust::ensures((result == x) && (result > 0))] +#[thrust_macros::requires(x > 0)] +#[thrust_macros::ensures((result == x) && (result > 0))] fn pass_positive(x: i32, _dummy: T) -> i32 { x } diff --git a/tests/ui/pass/fn_ptr.rs b/tests/ui/pass/fn_ptr.rs index a248446a..2f1a5915 100644 --- a/tests/ui/pass/fn_ptr.rs +++ b/tests/ui/pass/fn_ptr.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/pass/just_rec.rs b/tests/ui/pass/just_rec.rs index 10c69ca1..646b684e 100644 --- a/tests/ui/pass/just_rec.rs +++ b/tests/ui/pass/just_rec.rs @@ -2,13 +2,13 @@ //@compile-flags: -C debug-assertions=off #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> i32 { unimplemented!() } #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand_bool() -> bool { unimplemented!() } fn just_rec(ma: &mut i32) { diff --git a/tests/ui/pass/loop.rs b/tests/ui/pass/loop.rs index 61b80f9c..aefeb3e2 100644 --- a/tests/ui/pass/loop.rs +++ b/tests/ui/pass/loop.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/pass/mut_recursive.rs b/tests/ui/pass/mut_recursive.rs index 978a62ec..f2538ecc 100644 --- a/tests/ui/pass/mut_recursive.rs +++ b/tests/ui/pass/mut_recursive.rs @@ -2,8 +2,8 @@ //@compile-flags: -C debug-assertions=off //@rustc-env: THRUST_SOLVER_TIMEOUT_SECS=60 -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/pass/recursive.rs b/tests/ui/pass/recursive.rs index 8be284f1..89a8d075 100644 --- a/tests/ui/pass/recursive.rs +++ b/tests/ui/pass/recursive.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/pass/split.rs b/tests/ui/pass/split.rs index 4d8f3453..9bf8197d 100644 --- a/tests/ui/pass/split.rs +++ b/tests/ui/pass/split.rs @@ -2,8 +2,8 @@ //@compile-flags: -C debug-assertions=off #[thrust::trusted] -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] fn rand() -> i32 { unimplemented!() } fn split<'a>((a, b): &'a mut (i32, i32)) -> (&'a mut i32, &'a mut i32) { diff --git a/tests/ui/pass/take_max.rs b/tests/ui/pass/take_max.rs index 9a8802ac..dc371ff6 100644 --- a/tests/ui/pass/take_max.rs +++ b/tests/ui/pass/take_max.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } diff --git a/tests/ui/pass/take_max_annot.rs b/tests/ui/pass/take_max_annot.rs index 1f467a69..3683cfe4 100644 --- a/tests/ui/pass/take_max_annot.rs +++ b/tests/ui/pass/take_max_annot.rs @@ -1,15 +1,15 @@ //@check-pass //@compile-flags: -C debug-assertions=off -#[thrust::requires(true)] -#[thrust::ensures(true)] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] #[thrust::trusted] fn rand() -> i64 { unimplemented!() } -#[thrust::requires(true)] -#[thrust::ensures( - *ma >= *mb && *mb == ^mb && ma == result || - *ma < *mb && *ma == ^ma && mb == result +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + *ma >= *mb && *mb == !mb && ma == result || + *ma < *mb && *ma == !ma && mb == result )] fn take_max<'a>(ma: &'a mut i64, mb: &'a mut i64) -> &'a mut i64 { if *ma >= *mb { From 18bb8169f2803fd325933a883aea9c5b7b3c1f85 Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 11 May 2026 00:36:30 +0900 Subject: [PATCH 3/3] Implement int operators in annotations where const is lhs --- std.rs | 66 +++++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 49 insertions(+), 17 deletions(-) diff --git a/std.rs b/std.rs index a83813f2..dc30924e 100644 --- a/std.rs +++ b/std.rs @@ -172,30 +172,62 @@ mod thrust_models { type Ty = model::Int; } - impl Model for isize { - type Ty = model::Int; - } + macro_rules! int_model { + ($T:ty) => { + impl Model for $T { + type Ty = model::Int; + } - impl Model for i32 { - type Ty = model::Int; - } + impl PartialEq for $T { + #[thrust::ignored] + fn eq(&self, _other: &model::Int) -> bool { + unimplemented!() + } + } - impl Model for i64 { - type Ty = model::Int; - } + impl PartialOrd for $T { + #[thrust::ignored] + fn partial_cmp(&self, _other: &model::Int) -> Option { + unimplemented!() + } + } - impl Model for usize { - type Ty = model::Int; - } + impl std::ops::Add for $T { + type Output = model::Int; - impl Model for u32 { - type Ty = model::Int; - } + #[thrust::ignored] + fn add(self, _rhs: model::Int) -> Self::Output { + unimplemented!() + } + } - impl Model for u64 { - type Ty = model::Int; + impl std::ops::Sub for $T { + type Output = model::Int; + + #[thrust::ignored] + fn sub(self, _rhs: model::Int) -> Self::Output { + unimplemented!() + } + } + + impl std::ops::Mul for $T { + type Output = model::Int; + + #[thrust::ignored] + fn mul(self, _rhs: model::Int) -> Self::Output { + unimplemented!() + } + } + }; } + int_model!(isize); + int_model!(i32); + int_model!(i64); + int_model!(usize); + int_model!(u32); + int_model!(u64); + impl Model for bool { type Ty = bool; }