Aptos move-model Builder 模块解析Legacy 模式与 Compiler 模式的双轨构建机制【免费下载链接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.项目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core导读本文聚焦 Aptos 仓库中 Move 规范验证体系的核心前置模块——third_party/move/move-model/src/builder它是将一组 Move 模块构建编译为全局环境GlobalEnv的入口。文章以 builder/README.md 定义的legacy 模式与compiler 模式两条主线展开结合模块源码剖析两种模式在源码信息与 bytecode 信息如何组合上的本质差异、三阶段翻译流水线、符号表结构与关键 API 调用链帮助读者理解 Move Prover / 规范检查工具从 Move 代码到可分析模型的完整构建路径。builder 模块的定位为 Move 模块构建全局环境在 Aptos 的 move-model 中builder是一个负责前端构建的子模块其职责在 README 开头一句话即已点明This module handles building (compiling) a global environment for a set of Move modules.这里的构建并不是指生成链上部署的字节码而是指把一组 Move 模块可能同时包含 Move 源码与已编译的 bytecode翻译成规范验证系统可以查询、遍历、做类型检查的全局环境GlobalEnv。GlobalEnv是 move-model 的核心数据结构定义于 model.rs承载模块、结构体、函数、规格spec、常量等全部模型信息是 Move Prover 后续所有分析阶段的数据基础。从目录结构看builder由以下文件组成见 builder 目录文件职责mod.rs子模块声明与若干文本辅助函数复数化等model_builder.rsModelBuilder主状态机维护全部符号表负责将各模块按无环依赖顺序登记进模型module_builder.rsModuleBuilder单个模块的翻译器实现声明分析、定义分析、环境填充三阶段exp_builder.rsExpTranslatorMove 表达式含 spec 语言表达式到模型 AST 的翻译与类型检查builtins.rs注册内建函数与操作符ModelBuilder::new时调用builtins::declare_builtinsbinary_module_loader.rs二进制模块加载器将CompiledModuleSourceMap载入环境xir_loader.rsXIR 加载器字节码中间表示相关macros.rs内建宏展开辅助两种构建模式README 定义的双轨机制README 指出该模块可以以两种模式运行这是全文的核心骨架legacy 模式遗留模式合并 bytecode 与 Move 源码中代表表达式语言构造的部分。由此得到的模型同时具备源码信息与 bytecode 信息。compiler 模式编译器模式完整分析 Move 源码。由此得到的模型默认不包含 bytecode 相关信息但 bytecode 可以在后续阶段通过GlobalEnv::attach_compiled_module附加进来。两种模式的差异本质在于模型的信息来源legacy 模式以已编译的CompiledModule为主体、以源码补全表达式层信息compiler 模式则以源码为主体、bytecode 是可选的后置附件。下文分别深入。Legacy 模式bytecode 为主、源码补充表达式信息Legacy 模式的实现集中在 binary_module_loader.rs。其入口是GlobalEnv::load_compiled_modulebinary_module_loader.rspub fn load_compiled_module( mut self, with_dep_closure: bool, module: CompiledModule, source_map: SourceMap, ) - ModuleId { let mut loader BinaryModuleLoader::new(self, with_dep_closure, module, source_map); loader.load(); let BinaryModuleLoader { module_id, .. } loader; self.attach_compiled_module(module_id, module, source_map); self.update_loaded_modules(); module_id }其注释清楚地说明了实现策略we leverage the already existing and battle-testedenv.attach_compiled_modulefunction... This function here basically simulates populating the initial env from bytecode instead of AST, and then calls the bytecode attach.即legacy 模式先假装从 AST 填充环境实际上从 bytecode 反推再调用字节码附加逻辑从而让最终模型同时拥有两类信息。几个值得注意的实现细节依赖处理with_dep_closure为false时模块的全部依赖必须已存在于环境中为true时会按使用表为缺失依赖创建 stub占位定义形成部分模块并可在后续load_compiled_module调用中被逐步精化binary_module_loader.rs。0x1::vector特殊处理加载时若发现vector模块尚未加载会调用add_well_known_vector_funsbinary_module_loader.rs把empty、length、borrow、borrow_mut、push_back、pop_back、destroy_empty、swap等以字节码指令形式存在、没有 handle 的 vector 函数以 native public 函数的形式补进环境——这是合并 bytecode 信息的直接体现。结构体/函数签名一致性校验若同一结构体或函数已被加载load过程会做逻辑签名比对type_params_logical_equal、params_logical_equal不一致时报错并保证环境在无错前提下自洽。Compiler 模式完全分析源码bytecode 后置附加Compiler 模式的入口在 lib.rs 的run_model_builder_in_compiler_modeBuilds the Move model for the v2 compiler. This builds the model, compiling both code and specs from sources into typed-checked AST. No bytecode is attached to the model. This currently uses the v1 compiler as the parser (up to expansion AST), after that a new type checker.其流程见run_model_builder_with_options_and_compilation_flagslib.rs大致如下解析用编译器Compiler::from_package_paths运行到PASS_PARSER收集源码文件、注释与命名地址映射。扩展运行到PASS_EXPANSION得到 expansion AST期间把vector、cmp、string、string_utils、signer等隐式模块及其依赖闭包纳入编译集。模型构建调用run_move_checkerlib.rs这是 compiler 模式的核心——不做 bytecode 附加The expansion AST will be type checked. No bytecode is attached.。因此compiler 模式产出的模型只含源码层信息结构体、函数签名、spec 块、宏展开结果等bytecode 相关的派生数据如字节码指令序列默认缺失需要在后续阶段调用GlobalEnv::attach_compiled_modulemodel.rs手动附加。该方法要求module_data[module_id]已通过GlobalEnv::add初始化/// Attaches a bytecode module to the module in the environment. This functions expects /// the self.module_data[module_id] to be already initialized using the self.add /// function. pub fn attach_compiled_module( mut self, module_id: ModuleId, module: CompiledModule, source_map: SourceMap, )这一设计的意义在于compiler 模式可以在不依赖链上/本地字节码的情况下先行完成源码级检查类型检查、spec 检查需要字节码级分析如字节码指令层面的验证时再按需附加实现了源码检查与字节码分析的解耦。模块翻译的三阶段流水线无论哪种模式单个模块的翻译都由ModuleBuilder::translate驱动module_builder.rs分为三个阶段pub fn translate(mut self, loc: Loc, module_def: EA::ModuleDefinition) { self.decl_ana(module_def); // 阶段 1声明分析 self.def_ana(module_def); // 阶段 2定义分析 self.synthesize_validity_slots(); self.collect_spec_block_infos(module_def); let attrs self.translate_attributes(module_def.attributes); self.populate_and_finalize_env(loc, attrs); // 阶段 3填充环境 }声明分析declaration analysis收集模块内结构体、函数、spec 函数、spec 变量与 schema 的全部声明信息但暂不分析函数体、条件与不变量。原因在于全局声明是顺序无关的且可能存在循环引用——必须先让所有声明可见才能正确解析相互引用。定义分析definition analysis回头处理阶段 1 跳过的定义体对表达式与 schema 包含inclusion做完整分析与类型检查。此阶段由ExpTranslatorexp_builder.rs完成表达式到模型 AST 的翻译并支持old表达式、ghost字段等规格语言特性。填充阶段population phase将本模块的信息正式登记进GlobalEnv并完成环境级后处理如常量访问器注入、package 可见性的 friend 声明补全等。在 compiler 模式下run_move_checker会先把模块按dependency_order排序保证依赖先于使用者被翻译同时通过pre_register_lemma_declslib.rs预注册所有模块的 lemma 声明使跨模块 lemma 引用不依赖模块处理顺序即可解析。ModelBuilder环境构建的状态核心ModelBuildermodel_builder.rs是构建过程的总账本以多张符号表维护增量状态每翻译一个模块就扩展一次。其核心字段包括spec_fun_tablespec 函数符号表因支持重载一项可对应多个函数spec_var_table/spec_schema_tablespec 变量与 schema 符号表后者附带unused_schema_set用于生成未使用 schema 的告警struct_table/reverse_struct_table结构体符号表及其反向映射供错误消息中类型可视化fun_table函数符号表并维护builtin_receiver_functions与receiver_functions用于 receiver 风格方法调用如v.length()分发到0x1::vector::lengthconst_table常量符号表支持跨模块常量使用者追踪sync_const_usersintrinsics内建声明列表populate_env时统一注册进GlobalEnvlemma_decl_table全局 lemma 查询表首次扫描时预填充保证跨模块引用可解析。ModelBuilder::newmodel_builder.rs在初始化时会调用builtins::declare_builtins把语言内建的操作符与 spec 函数预先登记这是表达式翻译的前提。两种模式的选择与适用场景需要完整字节码信息的场景legacy 模式例如对已部署模块做验证、需要访问指令级信息的分析、或者依赖SourceMap做源码↔字节码映射的场景。此时通过load_compiled_module(with_dep_closure, module, source_map)一次性获得源码 bytecode双全模型。纯源码分析场景compiler 模式例如在编译早期对包内源码做类型检查、spec 检查、宏展开验证。此时使用run_model_builder_in_compiler_mode或带选项/编译标志的run_model_builder_with_options_and_compilation_flags产出纯源码模型若后续阶段需要字节码再调用GlobalEnv::attach_compiled_module按需附加。从代码结构可以推断两者并非互斥的封闭体系而是共享同一套GlobalEnv/ModelBuilder/ModuleBuilder基础设施legacy 模式通过BinaryModuleLoader从 bytecode 反推环境初始状态compiler 模式则从 expansion AST 正向翻译最终都收敛到attach_compiled_module所定义的源码信息 字节码信息统一模型表示上。源码地图与延伸阅读模式定义与模块定位builder/README.md环境构建主状态机model_builder.rs单模块三阶段翻译module_builder.rs表达式与 spec 翻译器exp_builder.rsbytecode 加载legacy 模式核心binary_module_loader.rs内建函数注册builtins.rsCompiler 模式入口与run_move_checkerlib.rs全局环境与attach_compiled_modulemodel.rs综上builder模块以legacy 合并 bytecode与compiler 纯源码分析两种模式覆盖了从 Move 代码到可验证模型的全部构建路径是理解 Aptos move-model 乃至 Move Prover 前端流水线的关键入口。【免费下载链接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.项目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考