From 5e9397eff453f39b827f5b73b7b3087245c1481c Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 15 Aug 2026 12:15:46 +0000 Subject: [PATCH 1/2] Register enum defs reachable through ADT fields `register_enum_defs` discovered the enums a body needs by visiting the types of its local declarations, and a `TypeVisitor` descends into an ADT's generic arguments only. An enum occurring solely as the field type of another ADT -- `struct Wrap { o: Option }`, or `enum Outer { X(Inner), Y }` -- was therefore never registered, while the elaboration of the outer ADT does reach it, so the lookup of its `EnumDatatypeDef` through `EnumDefProvider` unwrapped a `None`. Collect the enums with `EnumDefCollector`, which follows the structure the elaboration follows: an ADT that is not translated as a model type is elaborated into its fields, so the enums those fields mention are needed too. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01BFzi5Pc3p3DwocuhvTiVLK --- src/analyze/basic_block.rs | 29 +++++--------------- src/refine.rs | 2 +- src/refine/template.rs | 55 +++++++++++++++++++++++++++++++++++++- 3 files changed, 62 insertions(+), 24 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 4ed04196..77591eb9 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -13,8 +13,8 @@ use crate::analyze; use crate::chc; use crate::pretty::PrettyDisplayExt as _; use crate::refine::{ - Assumption, BasicBlockType, BasicBlockTypeParamKind, PlaceType, PlaceTypeBuilder, PlaceTypeVar, - TempVarIdx, TypeBuilder, Var, + Assumption, BasicBlockType, BasicBlockTypeParamKind, EnumDefCollector, PlaceType, + PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, TypeBuilder, Var, }; use crate::rty::{ self, ClauseBuilderExt as _, ClauseScope as _, ShiftExistential as _, Subtyping as _, @@ -1326,27 +1326,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } fn register_enum_defs(&mut self) { + let mut collector = EnumDefCollector::new(self.type_builder.clone()); for local_decl in &self.local_decls { - use mir_ty::{TypeSuperVisitable as _, TypeVisitable as _}; - #[derive(Default)] - struct EnumCollector { - enums: std::collections::HashSet, - } - impl<'tcx> mir_ty::TypeVisitor> for EnumCollector { - fn visit_ty(&mut self, ty: mir_ty::Ty<'tcx>) { - if let mir_ty::TyKind::Adt(adt_def, _) = ty.kind() { - if adt_def.is_enum() { - self.enums.insert(adt_def.did()); - } - } - ty.super_visit_with(self); - } - } - let mut visitor = EnumCollector::default(); - local_decl.ty.visit_with(&mut visitor); - for def_id in visitor.enums { - self.ctx.get_or_register_enum_def(def_id); - } + collector.collect(local_decl.ty); + } + for def_id in collector.into_enums() { + self.ctx.get_or_register_enum_def(def_id); } } } diff --git a/src/refine.rs b/src/refine.rs index 5a1fd8d3..79ad7db9 100644 --- a/src/refine.rs +++ b/src/refine.rs @@ -8,7 +8,7 @@ //! module and remove this one. mod template; -pub use template::{TemplateRegistry, TemplateScope, TypeBuilder}; +pub use template::{EnumDefCollector, TemplateRegistry, TemplateScope, TypeBuilder}; mod basic_block; pub use basic_block::{BasicBlockType, BasicBlockTypeParamKind}; diff --git a/src/refine/template.rs b/src/refine/template.rs index bf123213..648df85c 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -1,4 +1,4 @@ -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; use rustc_index::IndexVec; use rustc_middle::mir::{Local, Mutability}; @@ -327,6 +327,59 @@ impl<'tcx> TypeBuilder<'tcx> { } } +/// Collects the enums whose datatype definitions [`TypeBuilder::build`] needs. +/// +/// A type needs the definition of every enum it mentions, but also of every enum +/// mentioned by the ADTs it mentions: a struct is elaborated into the tuple of its +/// fields and an enum into the fields of its variants, so `struct Wrap { o: Option }` +/// needs the definition of `Option` even though no `Option` occurs in `Wrap` itself. +/// Model types are the exception, as they are translated directly without elaborating +/// their fields. +pub struct EnumDefCollector<'tcx> { + builder: TypeBuilder<'tcx>, + elaborated_adts: HashSet, + enums: HashSet, +} + +impl<'tcx> EnumDefCollector<'tcx> { + pub fn new(builder: TypeBuilder<'tcx>) -> Self { + Self { + builder, + elaborated_adts: Default::default(), + enums: Default::default(), + } + } + + pub fn collect(&mut self, ty: mir_ty::Ty<'tcx>) { + use mir_ty::TypeVisitable as _; + ty.visit_with(self); + } + + pub fn into_enums(self) -> HashSet { + self.enums + } +} + +impl<'tcx> mir_ty::TypeVisitor> for EnumDefCollector<'tcx> { + fn visit_ty(&mut self, ty: mir_ty::Ty<'tcx>) { + use mir_ty::{TypeSuperVisitable as _, TypeVisitable as _}; + + let ty = self.builder.resolve_model_ty(ty); + if let mir_ty::TyKind::Adt(def, args) = ty.kind() { + let is_elaborated = self.builder.model_adt(def, args).is_none(); + if is_elaborated && self.elaborated_adts.insert(def.did()) { + if def.is_enum() { + self.enums.insert(def.did()); + } + for field in def.all_fields() { + field.ty(self.builder.tcx, args).visit_with(self); + } + } + } + ty.super_visit_with(self); + } +} + /// Translates [`mir_ty::Ty`] to [`rty::Type`] using templates for refinements. /// /// [`rty::Template`] is a refinement type in the form of `{ T | P(x1, ..., xn) }` where `P` is a From 2d637f3070c1e6be65885ec7b7bdbb22e4764349 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 15 Aug 2026 12:15:46 +0000 Subject: [PATCH 2/2] Declare the datatypes reachable through another datatype's selector A polymorphic datatype is monomorphized for the datatype sorts collected from the clauses, and a sort that occurs only as the selector of another datatype occurs in none of them: `struct Wrap { o: Option }` gives its locals the sort of the tuple `Wrap` elaborates to, which mentions `std.option.Option` in its declaration alone. The emitted SMT-LIB2 then referred to a sort it never declared and the solver rejected the file. Run the sort collection to a fixpoint over the selectors of the datatypes being declared. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01BFzi5Pc3p3DwocuhvTiVLK --- src/chc/format_context.rs | 41 ++++++++++++++++++++++++++++++++++----- 1 file changed, 36 insertions(+), 5 deletions(-) diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index b0f5f782..cc0744c3 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -231,11 +231,25 @@ fn collect_sorts(system: &chc::System) -> BTreeSet { sorts } +fn find_datatype<'a>( + datatypes: &'a [chc::Datatype], + symbol: &chc::DatatypeSymbol, +) -> &'a chc::Datatype { + datatypes.iter().find(|d| &d.symbol == symbol).unwrap() +} + +fn selector_sorts(datatype: &chc::Datatype) -> impl Iterator + '_ { + datatype + .ctors + .iter() + .flat_map(|ctor| ctor.selectors.iter().map(|selector| selector.sort.clone())) +} + fn monomorphize_datatype( sort: &chc::DatatypeSort, datatypes: &[chc::Datatype], ) -> Option { - let datatype = datatypes.iter().find(|d| d.symbol == sort.symbol).unwrap(); + let datatype = find_datatype(datatypes, &sort.symbol); if datatype.params == 0 { return None; } @@ -269,11 +283,28 @@ fn monomorphize_datatype( impl FormatContext { pub fn from_system(system: &chc::System) -> Self { - let mut sorts = collect_sorts(system); let mut datatypes = system.datatypes.clone(); - for sort in sorts.iter().flat_map(|s| s.as_datatype()) { - if let Some(mono_datatype) = monomorphize_datatype(sort, &datatypes) { - datatypes.push(mono_datatype); + let mut sorts = BTreeSet::new(); + let mut pending: Vec<_> = collect_sorts(system).into_iter().collect(); + // Declaring a datatype requires the sorts of its selectors to be declared as well, + // and those need not occur in the clauses at all: the sort of a field that is only + // ever read through a projection is mentioned by the declaration alone. + while let Some(sort) = pending.pop() { + let mut datatype_sorts = Vec::new(); + sort.walk(|inner_sort| { + if sorts.insert(inner_sort.clone()) { + datatype_sorts.extend(inner_sort.as_datatype().cloned()); + } + }); + for datatype_sort in datatype_sorts { + let datatype = match monomorphize_datatype(&datatype_sort, &datatypes) { + Some(mono_datatype) => { + datatypes.push(mono_datatype.clone()); + mono_datatype + } + None => find_datatype(&datatypes, &datatype_sort.symbol).clone(), + }; + pending.extend(selector_sorts(&datatype)); } } let int_array_elem_sorts: BTreeSet<_> = sorts