深入解析:原理、接口与调试实践)
Rust 编译器 trait solver 证明树Proof Trees深入解析原理、接口与调试实践【免费下载链接】rustEmpowering everyone to build reliable and efficient software.项目地址: https://gitcode.com/GitHub_Trending/ru/rust导读rustc 的新一代 trait solverrustc_next_trait_solver对外只返回目标是否成立以及必要的推断约束内部求值过程如同黑盒。为了让编译器其他组件能够观察求值过程中发生了什么Rust 编译器引入了proof trees证明树机制通过实现ProofTreeVisitortrait诊断、一致性检查coherence、闭包签名推断、codegen 等模块可以程序化地翻阅求解过程。本文以 rustc-dev-guide 中 proof-trees.md 为骨架结合本仓库中 proof tree 的构建、数据结构与消费端源码完整讲解它的设计动机、计算原理、公开 API以及如何用tracing日志调试 trait solver。为什么需要 proof treestrait solver 作为一个查询系统正常使用场景下只需要两个输出目标是否成立QueryResult以及在求解过程中产生的约束如类型推断变量、region 约束。对编译器的其余部分而言把 solver 当作黑盒是最稳妥的——它的内部状态特别是嵌套InferCtxt中的推断变量对调用方毫无意义。但有些场景确实需要了解求解过程中发生了什么例如为新求解器next solver计算跨 crate 歧义原因intercrate ambiguity causes用于改善 coherence 错误诊断改进 trait solver 相关的编译错误信息找出真正导致失败的最佳叶子义务急切地推断闭包签名eagerly infer closure signatures在闭包体尚未完整类型检查前就通过自 trait 边界还原签名。为此solver 提供了 proof trees 作为观察接口求解时不只记录结论还把一步步的求值过程组织成一棵树供外部程序化分析。rustc-dev-guide 明确指出虽然 trait solver 一般应被其余编译器代码视为黑盒但我们不能完全忽略其内部因此提供 proof trees 作为接口。计算 proof treesCanonicalization 与嵌套 InferCtxtproof tree 的计算方式与 trait solver 本身的架构深度绑定。核心事实是trait solver 使用 Canonicalization并且每个嵌套目标都使用完全独立的InferCtxt。嵌套目标的 canonicalize → instantiate 循环考虑目标VecVec?x: Debug其中?x是尚未约束的推断变量。求解流程如下对应 rustc-dev-guide 的原始示例将根目标 canonicalize 为existsT0 VecVecT0: Debug在求解查询内部实例化该目标得到VecVec?0: Debug求解产生嵌套目标Vec?0: Debug再次 canonicalize 为existsT0 VecT0: Debug再次实例化为Vec?0: Debug进而得到嵌套目标?0: Debug——此时它是歧义的ambiguous。可以看出每次进入嵌套目标都经历一次 canonicalize → instantiate 的循环而每次实例化都发生在新的独立InferCtxt中。这也意味着proof tree 里记录的任何数据目标、推断变量、impl 参数等如果直接存引用就会泄漏嵌套InferCtxt的推断变量导致调用方根本无法理解。CanonicalState把局部数据举升到调用方上下文解决方案是凡是涉及推断变量或 placeholder 的数据在存储时都连同本次计算过程中创建的所有未约束推断变量列表一起 canonicalize。这个组合就是CanonicalState——见 compiler/rustc_type_ir/src/solve/inspect.rs 中的定义pub struct StateI: Interner, T { pub var_values: CanonicalVarValuesI, pub data: T, } pub type CanonicalStateI, T CanonicalI, StateI, T;当外部遍历 proof tree 时CanonicalState会在父级推理上下文中被实例化instantiate借助记录下来的推断变量列表把所有 canonicalized 的值重新连接起来。这正是 rustc-dev-guide 所说的ThisCanonicalStateis then instantiated in the parent inference context while walking the proof tree, using the list of inference variables to connect all the canonicalized values created during this evaluation.补充关于 canonicalize 本身的具体规则类型/常量推断变量映射为存在量化变量、placeholder 映射为全称量化变量、region 唯一化等参见 canonicalization.md它是理解 proof tree 中变量连接方式的前提。求值入口ProofTreeBuilder 注入搜索图proof tree 的构建发生在求值过程中。ProofTreeBuilder会被传入搜索图search graph把 trait solver 的求值步骤逐步转换为一棵树。实现在 compiler/rustc_next_trait_solver/src/solve/inspect/build.rspub(crate) struct ProofTreeBuilderD, I D as SolverDelegate::Interner { state: OptionBoxOptioninspect::ProbeI, _infcx: PhantomDataD, }关键设计点state: Some(Box::new(None))表示要构建证明树new_noop()则产生state: None即求值过程中完全不记录零开销路径单步求值的构建由EvaluationStepBuilder完成EvalCtxt在合适时机更新它根目标的求值入口是evaluate_root_goal_for_proof_tree_raw_providercompiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs它创建ProofTreeBuilder::new()调用SearchGraph::evaluate_root_goal_for_proof_tree求值最后inspect.unwrap()取出Probe作为最终修订final revision。EvaluationStepBuilder记录了每个求值步骤中新增的推断变量add_var_value、嵌套 probeenter_probe/finish_probe、添加的目标add_goal、impl 参数record_impl_args以及最终响应make_canonical_response/query_result所有数据都经canonical::make_canonical_state转换为CanonicalState后存储。proof tree 的数据结构Probe、ProbeStep 与 ProbeKindproof tree 的树干是一棵Probe树。相关类型全部定义在 compiler/rustc_type_ir/src/solve/inspect.rs模块文档明确说明了设计约束由于每个嵌套目标会被分别 canonicalize且推断进展会被probe丢弃因此无法机械地直接使用 proof tree必须把所有数据举升为CanonicalState同时proof tree 本身是浅层的shallow——它不为嵌套目标预先计算证明树访问者需要时会在父级推理上下文中重新求值嵌套目标。Probepub struct ProbeI: Interner { /// 该 probe 内部按时间顺序发生的事情 pub steps: VecProbeStepI, pub kind: ProbeKindI, pub final_state: CanonicalStateI, (), }Probe表示 trait 求解过程中的一次自包含计算要么对应一次EvalCtxt::probe(_X)调用例如多候选探索时每个候选各占一个 probe要么对应根目标的求值ProbeKind::Root。ProbeSteppub enum ProbeStepI: Interner { /// 向 EvalCtxt 添加了一个目标将在下次 try_evaluate_added_goals 时证明 AddGoal(GoalSource, CanonicalStateI, GoalI, I::Predicate), /// 证明当前目标过程中的一次 probe 调用存在多个候选时使用 NestedProbe(ProbeI), /// trait 目标由某个 impl 候选满足 RecordImplArgs { impl_args: CanonicalStateI, I::GenericArgs }, /// 调用 evaluate_added_goals_make_canonical_response 并传入 Certainty MakeCanonicalResponse { shallow_certainty: Certainty }, }其中MakeCanonicalResponse记录的shallow_certainty是传入的确定性并非与内部try_evaluate_added_goals结果统一后的确定性如果它是Certainty::Yes说明可以信任该候选已完成没有因某种原因被强制歧义化。ProbeKindpub enum ProbeKindI: Interner { Root { result: QueryResultI }, // 证明目标的根推理上下文 NormalizedSelfTyAssembly, // 候选组装时归一化 self 类型 TraitCandidate { source: CandidateSourceI, result: QueryResultI }, UnsizeAssembly, // unsize trait 非 self 类型归一化 ProjectionCompatibility, // 投影/upcast 相关 ShadowedEnvProbing, // 查找满足投影的 param-env 候选 OpaqueTypeStorageLookup { result: QueryResultI }, RigidAlias { result: QueryResultI }, // 刚性别名 well-formed 检查 }ProbeKind::Root对应一次目标求值的完整结果TraitCandidate则标记该 probe 是一个证明当前 trait 目标的候选是消费端分析的重点。程序化分析 APIProofTreeVisitor公开 traitproof tree 的消费接口是ProofTreeVisitortrait定义于 compiler/rustc_trait_selection/src/solve/inspect/analyse.rspub trait ProofTreeVisitortcx { type Result: VisitorResult (); fn span(self) - Span; fn config(self) - InspectConfig { InspectConfig { max_depth: 10 } } fn visit_goal(mut self, goal: InspectGoal_, tcx) - Self::Result; fn on_recursion_limit(mut self) - Self::Result { Self::Result::output() } }要点span()访问者必须提供 span用于在嵌套目标重新求值时定位源码位置config()默认InspectConfig { max_depth: 10 }限制 proof tree 遍历的嵌套深度超限时触发on_recursion_limit()Result默认为()但可以自定义如select.rs中的ControlFlowSelectionResult...见下文遍历入口在扩展 traitInferCtxtProofTreeExt中visit_proof_tree/visit_proof_tree_at_depth同文件 L399-L418内部调用evaluate_root_goal_for_proof_tree重新求值根目标并构造InspectGoal。InspectGoal 与 InspectCandidate访问者面对的核心对象是InspectGoal封装目标、结果ResultCertainty, NoSolution、required_depth、orig_values、final_revision等与InspectCandidate。常用方法goal.candidates()返回该目标的所有候选VecInspectCandidate含根求值本身当只有一种证明路径时例如WellFormedgoal.unique_applicable_candidate()当且仅当恰好存在一个可行候选时返回它cand.kind()/cand.result()/cand.shallow_certainty()候选的 ProbeKind、深层结果与浅层确定性cand.visit_nested_no_probe(visitor)遍历候选的所有嵌套目标不回滚推断约束会修改infcx状态cand.visit_nested_in_probe(visitor)遍历嵌套目标全部回滚推断约束cand.instantiate_impl_args(span)若候选来自CandidateSource::Impl实例化其 impl 参数。一个值得注意的实现细节对应 analyse.rs 中的注释proof tree 是浅层的——instantiate_nested_goals会把AddGoal步骤中的CanonicalState实例化到当前InferCtxt然后调用evaluate_root_goal_for_proof_tree重新求值嵌套目标来获得其子证明树位于infcx.probe内避免候选间推断约束相互污染。一个最小访问者的骨架结合 coherence.rs 中AmbiguityCausesVisitor的写法最小实现如下struct MyVisitortcx { /* 自定义状态 */ } impltcx ProofTreeVisitortcx for MyVisitortcx { type Result (); fn span(self) - Span { DUMMY_SP } fn visit_goal(mut self, goal: InspectGoal_, tcx) - Self::Result { for cand in goal.candidates() { // 处理当前候选例如记录 TraitCandidate 的来源与结果 // 递归进入嵌套目标 cand.visit_nested_in_probe(self); } } } // 调用方 infcx.visit_proof_tree(goal, mut MyVisitor { /* ... */ });proof tree 的四个真实消费场景rustc-dev-guide 提到三个典型用途源码中实际共有四类消费端均可作为实现参考。1. coherence 错误的 intercrate ambiguity causes在 compiler/rustc_trait_selection/src/traits/coherence.rs 中compute_intercrate_ambiguity_causes对每个义务调用search_ambiguity_causes后者由AmbiguityCausesVisitor实现ProofTreeVisitor它遍历候选仅关注Certainty::Maybe(_)的歧义目标找出ProbeKind::TraitCandidate且CandidateSource::CoherenceUnknowable的候选从而精确定位跨 crate 不可知导致的冲突。代码注释直言其足够用于 UI 测试中的诊断改进这类只用于改善诊断的实现接受一定程度的近似。2. 改善 trait solver 错误信息fulfillment errors错误报告需要找到最佳失败叶子义务。在 compiler/rustc_trait_selection/src/solve/fulfill/derive_errors.rs 中fulfillment_error_for_no_solution通过find_best_leaf_obligation定位根义务并由BestObligation访问者同文件 L422 附近利用 proof tree 在失败的候选之间挑选信息量最大的那一个。这套机制替代了旧求解器中基于深层嵌套义务猜测的做法。3. 急切推断闭包签名类型检查阶段需要在遍历闭包体之前尽量还原闭包签名。在 compiler/rustc_hir_typeck/src/closure.rs 中deduce_closure_signature_from_predicates通过 elaborate 后的自 trait 边界如投影子句推断闭包参数与返回值类型而 fn_ctxt/inspect_obligations.rs 中的NestedObligationsForSelfTy等访问者正是借助 proof tree 找出与 self 类型相关的嵌套义务为签名推断提供依据。4. codegen 阶段的候选筛选Selectcompiler/rustc_trait_selection/src/solve/select.rs 中Select结构体实现了ProofTreeVisitor并把Result定制为ControlFlowSelectionResulttcx, Selectiontcxvisit_goal中先过滤出可行的候选没有候选返回Unimplemented只有一个候选直接返回多个候选且目标只是Certainty::Maybe(_)时暂不 winnowcodegen 才需要必要时才进行候选间的相互淘汰。这是 proof tree 在 codegen 阶段做 trait 选择selection的典型用法。用 tracing 调试 trait solverproof tree 适合程序化分析但用它来调试 solver 实现并不理想rustc-dev-guide 明确指出两者设计需求不同This has different design requirements than analyzing it programmatically。推荐的调试方式是tracing日志trait solver 仅用debug级别记录求解的总体形状general shape用trace级别提供额外细节。因此# 查看求解过程的大致轮廓目标、候选、歧义等 RUSTC_LOGrustc_next_trait_solverdebug cargo nightly build # 需要更精确的信息时再升级到 trace RUSTC_LOGrustc_next_trait_solvertrace cargo nightly build其中rustc_next_trait_solver对应本仓库中的 crate compiler/rustc_next_trait_solver注意本仓库结构与 rustc-dev-guide 写作时略有差异rustc_trait_selection下的相关代码位于 compiler/rustc_trait_selection/src/solve。这一约定保证了日志量可控先看debug大纲再针对性地用trace深入。小结proof trees 是新一代 trait solver 暴露给编译器其余部分的窥视孔计算方式求值时通过ProofTreeBuilderbuild.rs把步骤组织成Probe树所有涉及推断变量的数据都先 canonicalize 成CanonicalStateinspect.rs遍历时再在父级InferCtxt中实例化分析接口实现ProofTreeVisitoranalyse.rs即可获得目标、候选、确定性、嵌套目标与 impl 参数等信息默认最大嵌套深度为 10可通过config()调整典型用途coherence 歧义原因分析coherence.rs、fulfillment 错误诊断derive_errors.rs、闭包签名推断closure.rs以及 codegen 阶段的候选筛选select.rs调试手段日常开发调试 solver 本身优先使用RUSTC_LOGrustc_next_trait_solverdebug大纲与trace细节。理解 proof tree 的前提是理解 canonicalization——两者共同构成了在独立InferCtxt中求解、在调用方上下文中重建视图的完整闭环。【免费下载链接】rustEmpowering everyone to build reliable and efficient software.项目地址: https://gitcode.com/GitHub_Trending/ru/rust创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考