From e836a4e9f41b6c688ee5ad2feea0b02089fff922 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 28 Sep 2026 10:59:07 +0000 Subject: [PATCH 1/5] Support associated consts (e.g. i64::MAX) in annotations Path expressions in requires/ensures formulas only resolved local variables and enum variant constructors, so a const item or an associated const like i64::MAX could not be referenced. Evaluate the constant via const_eval_resolve and lower its scalar value to a term, mirroring how ordinary function bodies already handle constants. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_01HKidXs2a4RaRhcEDvgwcKt --- src/analyze/annot_fn.rs | 44 ++++++++++++++++++++++++++++++ tests/ui/fail/assoc_const_annot.rs | 10 +++++++ tests/ui/pass/assoc_const_annot.rs | 10 +++++++ 3 files changed, 64 insertions(+) create mode 100644 tests/ui/fail/assoc_const_annot.rs create mode 100644 tests/ui/pass/assoc_const_annot.rs diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 136b4f4c..f3767f9e 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -3,6 +3,7 @@ use std::collections::HashMap; use pretty::{termcolor, Pretty}; use rustc_hir::{def_id::LocalDefId, HirId}; use rustc_index::IndexVec; +use rustc_middle::mir; use rustc_middle::ty::{self as mir_ty, TyCtxt}; use crate::analyze::{self, did_cache::DefIdCache}; @@ -603,6 +604,45 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { chc::Term::datatype_ctor(d_sym, sort_args, v_sym, field_terms) } + /// The term for a reference to the constant `const_did` (a `const` item or an + /// associated `const` such as `i64::MAX`) appearing in a formula. + fn const_term( + &self, + const_did: rustc_span::def_id::DefId, + hir: &'tcx rustc_hir::Expr<'tcx>, + ) -> chc::Term { + let ty = self.expr_ty(hir); + let generic_args = mir_ty::EarlyBinder::bind(self.typeck.node_args(hir.hir_id)) + .instantiate(self.tcx, self.generic_args); + let typing_env = mir_ty::TypingEnv::fully_monomorphized(); + let unevaluated = mir::UnevaluatedConst::new(const_did, generic_args); + let val = self + .tcx + .const_eval_resolve(typing_env, unevaluated, hir.span) + .unwrap_or_else(|e| panic!("failed to evaluate constant in formula: {:?}", e)); + self.const_value_term(&val, ty) + } + + fn const_value_term( + &self, + val: &mir::ConstValue, + ty: mir_ty::Ty<'tcx>, + ) -> chc::Term { + use mir::interpret::Scalar; + match (ty.kind(), val) { + (mir_ty::TyKind::Int(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { + chc::Term::int(v.to_int(v.size())) + } + (mir_ty::TyKind::Uint(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { + chc::Term::int(v.to_uint(v.size())) + } + (mir_ty::TyKind::Bool, mir::ConstValue::Scalar(Scalar::Int(v))) => { + chc::Term::bool(v.try_to_bool().unwrap()) + } + _ => unimplemented!("unsupported constant type in formula: {:?}", ty), + } + } + fn to_formula_with_quantified_vars( &self, closure: &rustc_hir::Body<'tcx>, @@ -743,6 +783,10 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { ) => { FormulaOrTerm::Term(self.variant_ctor_term(ctor_did, self.expr_ty(hir), vec![])) } + rustc_hir::def::Res::Def( + rustc_hir::def::DefKind::Const | rustc_hir::def::DefKind::AssocConst, + const_did, + ) => FormulaOrTerm::Term(self.const_term(const_did, hir)), _ => unimplemented!("unsupported path in formula: {:?}", qpath), }, ExprKind::Tup(exprs) => { diff --git a/tests/ui/fail/assoc_const_annot.rs b/tests/ui/fail/assoc_const_annot.rs new file mode 100644 index 00000000..14754003 --- /dev/null +++ b/tests/ui/fail/assoc_const_annot.rs @@ -0,0 +1,10 @@ +//@error-in-other-file: Unsat + +#[thrust_macros::requires(x == i64::MAX)] +fn only_max(x: i64) -> i64 { + x +} + +fn main() { + let _ = only_max(9223372036854775806); +} diff --git a/tests/ui/pass/assoc_const_annot.rs b/tests/ui/pass/assoc_const_annot.rs new file mode 100644 index 00000000..728c4157 --- /dev/null +++ b/tests/ui/pass/assoc_const_annot.rs @@ -0,0 +1,10 @@ +//@check-pass + +#[thrust_macros::requires(x == i64::MAX)] +fn only_max(x: i64) -> i64 { + x +} + +fn main() { + let _ = only_max(9223372036854775807); +} From ead5c8c9563bb73c4ad15a2198a8476dce2db170 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 28 Sep 2026 22:56:13 +0000 Subject: [PATCH 2/5] Share scalar constant lowering between MIR and annotation paths annot_fn's new associated-const support duplicated the int/uint/bool scalar-to-term match already in basic_block's const_value_ty. Extract it as analyze::scalar_const_term, generic over the term's variable type, and have both call it. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_01HKidXs2a4RaRhcEDvgwcKt --- src/analyze.rs | 20 ++++++++++++++++++++ src/analyze/annot_fn.rs | 23 ++--------------------- src/analyze/basic_block.rs | 26 ++++++++------------------ 3 files changed, 30 insertions(+), 39 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 3b5e7d1f..64dee4cb 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -35,6 +35,26 @@ mod reconstruct_slice_indexing; // TODO: organize structure and remove cross dependency between refine pub use did_cache::DefIdCache; +/// The term for a scalar constant of an integer or boolean type, shared by the MIR-level +/// (`basic_block`) and annotation-level (`annot_fn`) constant translation, which otherwise +/// evaluate constants from different starting points (a MIR operand vs. a HIR path) but agree +/// on how a scalar value becomes a term. `None` for any other type or value shape. +fn scalar_const_term(ty: mir_ty::Ty<'_>, val: &mir::ConstValue) -> Option> { + use mir::interpret::Scalar; + match (ty.kind(), val) { + (mir_ty::TyKind::Int(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { + Some(chc::Term::int(v.to_int(v.size()))) + } + (mir_ty::TyKind::Uint(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { + Some(chc::Term::int(v.to_uint(v.size()))) + } + (mir_ty::TyKind::Bool, mir::ConstValue::Scalar(Scalar::Int(v))) => { + Some(chc::Term::bool(v.try_to_bool().unwrap())) + } + _ => None, + } +} + fn fn_operand<'tcx>( tcx: TyCtxt<'tcx>, def_id: DefId, diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index f3767f9e..072422c8 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -620,27 +620,8 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { .tcx .const_eval_resolve(typing_env, unevaluated, hir.span) .unwrap_or_else(|e| panic!("failed to evaluate constant in formula: {:?}", e)); - self.const_value_term(&val, ty) - } - - fn const_value_term( - &self, - val: &mir::ConstValue, - ty: mir_ty::Ty<'tcx>, - ) -> chc::Term { - use mir::interpret::Scalar; - match (ty.kind(), val) { - (mir_ty::TyKind::Int(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { - chc::Term::int(v.to_int(v.size())) - } - (mir_ty::TyKind::Uint(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { - chc::Term::int(v.to_uint(v.size())) - } - (mir_ty::TyKind::Bool, mir::ConstValue::Scalar(Scalar::Int(v))) => { - chc::Term::bool(v.try_to_bool().unwrap()) - } - _ => unimplemented!("unsupported constant type in formula: {:?}", ty), - } + analyze::scalar_const_term(ty, &val) + .unwrap_or_else(|| unimplemented!("unsupported constant type in formula: {:?}", ty)) } fn to_formula_with_quantified_vars( diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 740d41c9..e198eb38 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -435,26 +435,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } fn const_value_ty(&self, val: &mir::ConstValue, ty: &mir_ty::Ty<'tcx>) -> PlaceType { + if let Some(term) = analyze::scalar_const_term(*ty, val) { + let scalar_ty = if ty.is_bool() { + rty::Type::bool() + } else { + rty::Type::int() + }; + return PlaceType::with_ty_and_term(scalar_ty, term); + } use mir::{interpret::Scalar, ConstValue, Mutability}; match (ty.kind(), val) { - (mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => { - PlaceType::with_ty_and_term( - rty::Type::int(), - chc::Term::int(val.to_int(val.size())), - ) - } - (mir_ty::TyKind::Uint(_), ConstValue::Scalar(Scalar::Int(val))) => { - PlaceType::with_ty_and_term( - rty::Type::int(), - chc::Term::int(val.to_uint(val.size())), - ) - } - (mir_ty::TyKind::Bool, ConstValue::Scalar(Scalar::Int(val))) => { - PlaceType::with_ty_and_term( - rty::Type::bool(), - chc::Term::bool(val.try_to_bool().unwrap()), - ) - } (mir_ty::TyKind::Tuple(tys), _) if tys.is_empty() => { PlaceType::with_ty_and_term(rty::Type::unit(), chc::Term::tuple(vec![])) } From 2681ca0b9c46d68dab597b2284d89cf12a05ae30 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 28 Sep 2026 23:01:48 +0000 Subject: [PATCH 3/5] Drop redundant doc comments on the new const-term helpers Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_01HKidXs2a4RaRhcEDvgwcKt --- src/analyze.rs | 4 ---- src/analyze/annot_fn.rs | 2 -- 2 files changed, 6 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 64dee4cb..deae9e8f 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -35,10 +35,6 @@ mod reconstruct_slice_indexing; // TODO: organize structure and remove cross dependency between refine pub use did_cache::DefIdCache; -/// The term for a scalar constant of an integer or boolean type, shared by the MIR-level -/// (`basic_block`) and annotation-level (`annot_fn`) constant translation, which otherwise -/// evaluate constants from different starting points (a MIR operand vs. a HIR path) but agree -/// on how a scalar value becomes a term. `None` for any other type or value shape. fn scalar_const_term(ty: mir_ty::Ty<'_>, val: &mir::ConstValue) -> Option> { use mir::interpret::Scalar; match (ty.kind(), val) { diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 072422c8..f3182b85 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -604,8 +604,6 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { chc::Term::datatype_ctor(d_sym, sort_args, v_sym, field_terms) } - /// The term for a reference to the constant `const_did` (a `const` item or an - /// associated `const` such as `i64::MAX`) appearing in a formula. fn const_term( &self, const_did: rustc_span::def_id::DefId, From 0e8cdf876a4179628d57f6526c480753d0686500 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 28 Sep 2026 23:30:29 +0000 Subject: [PATCH 4/5] Make the scalar_const_term fallthrough exhaustive, not bool-or-else is_bool() ? bool : int silently mapped any future non-bool addition to scalar_const_term (e.g. a string or tuple case) to rty::Type::int(), so extending that function would corrupt types instead of failing loudly. Match on TyKind explicitly and panic on anything else. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_01HKidXs2a4RaRhcEDvgwcKt --- src/analyze/basic_block.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index e198eb38..72c47e65 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -436,10 +436,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn const_value_ty(&self, val: &mir::ConstValue, ty: &mir_ty::Ty<'tcx>) -> PlaceType { if let Some(term) = analyze::scalar_const_term(*ty, val) { - let scalar_ty = if ty.is_bool() { - rty::Type::bool() - } else { - rty::Type::int() + let scalar_ty = match ty.kind() { + mir_ty::TyKind::Bool => rty::Type::bool(), + mir_ty::TyKind::Int(_) | mir_ty::TyKind::Uint(_) => rty::Type::int(), + _ => unreachable!("scalar_const_term only returns Some for Int/Uint/Bool"), }; return PlaceType::with_ty_and_term(scalar_ty, term); } From 87a3e535f746de125cbd4db9a3fca0ce45a2c3ca Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 28 Sep 2026 23:33:25 +0000 Subject: [PATCH 5/5] Return rty::Type from scalar_const_term instead of re-deriving it Pairing the term with its rty::Type inside scalar_const_term (both generic in the same unconstrained parameter, same as chc::Term) removes the second, independently-maintained match on TyKind that a prior fix only made panic-safe instead of eliminating. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_01HKidXs2a4RaRhcEDvgwcKt --- src/analyze.rs | 11 +++++++---- src/analyze/annot_fn.rs | 5 +++-- src/analyze/basic_block.rs | 7 +------ 3 files changed, 11 insertions(+), 12 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index deae9e8f..f0d79fe5 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -35,17 +35,20 @@ mod reconstruct_slice_indexing; // TODO: organize structure and remove cross dependency between refine pub use did_cache::DefIdCache; -fn scalar_const_term(ty: mir_ty::Ty<'_>, val: &mir::ConstValue) -> Option> { +fn scalar_const_term( + ty: mir_ty::Ty<'_>, + val: &mir::ConstValue, +) -> Option<(rty::Type, chc::Term)> { use mir::interpret::Scalar; match (ty.kind(), val) { (mir_ty::TyKind::Int(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { - Some(chc::Term::int(v.to_int(v.size()))) + Some((rty::Type::int(), chc::Term::int(v.to_int(v.size())))) } (mir_ty::TyKind::Uint(_), mir::ConstValue::Scalar(Scalar::Int(v))) => { - Some(chc::Term::int(v.to_uint(v.size()))) + Some((rty::Type::int(), chc::Term::int(v.to_uint(v.size())))) } (mir_ty::TyKind::Bool, mir::ConstValue::Scalar(Scalar::Int(v))) => { - Some(chc::Term::bool(v.try_to_bool().unwrap())) + Some((rty::Type::bool(), chc::Term::bool(v.try_to_bool().unwrap()))) } _ => None, } diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index f3182b85..7fdba444 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -618,8 +618,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { .tcx .const_eval_resolve(typing_env, unevaluated, hir.span) .unwrap_or_else(|e| panic!("failed to evaluate constant in formula: {:?}", e)); - analyze::scalar_const_term(ty, &val) - .unwrap_or_else(|| unimplemented!("unsupported constant type in formula: {:?}", ty)) + let (_, term) = analyze::scalar_const_term(ty, &val) + .unwrap_or_else(|| unimplemented!("unsupported constant type in formula: {:?}", ty)); + term } fn to_formula_with_quantified_vars( diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 72c47e65..38bba814 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -435,12 +435,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } fn const_value_ty(&self, val: &mir::ConstValue, ty: &mir_ty::Ty<'tcx>) -> PlaceType { - if let Some(term) = analyze::scalar_const_term(*ty, val) { - let scalar_ty = match ty.kind() { - mir_ty::TyKind::Bool => rty::Type::bool(), - mir_ty::TyKind::Int(_) | mir_ty::TyKind::Uint(_) => rty::Type::int(), - _ => unreachable!("scalar_const_term only returns Some for Int/Uint/Bool"), - }; + if let Some((scalar_ty, term)) = analyze::scalar_const_term(*ty, val) { return PlaceType::with_ty_and_term(scalar_ty, term); } use mir::{interpret::Scalar, ConstValue, Mutability};