语言运行时JIT编译编译器【免费下载链接】wasmtimeA lightweight WebAssembly runtime that is fast, secure, and standards-compliant项目地址https://gitcode.com/gh_mirrors/wa/wasmtime点击查看免费下载导读VeriISLE 是 wasmtime 仓库中针对 ISLE 指令选择语言Instruction Selection Language即cranelift/isle构建的 SMT 求解器形式化验证器它通过分析 ISLE 规则链结合手写的spec声明与从权威 ISA 语义如 AArch64 的 ASL推导出的规范证明 Cranelift 后端在指令选择重写前后行为等价。本文档cranelift/isle/veri/docs/language.md定义了 VeriISLE 用于描述这种行为的规范语言Specification Language从类型模型、规范声明、表达式与运算符语法到类型实例化、状态建模与属性标注。阅读完本文你将能够读懂并书写(spec ...)、(model ...)、(state ...)、(instantiate ...)、(attr ...)等规范构造掌握 provide/require/match/modifies 的语义差异并能借助仓库中的 filetests 示例与veri二进制运行验证。一、规范语言在 VeriISLE 中的定位VeriISLE详见 cranelift/isle/veri/README.md是一个基于 SMT 的 ISLE 规则验证器。其验证对象是 ISLE 规则链——例如一条把 CLIF 指令iadd改写为后端指令的规则。为了证明这些重写正确验证器需要知道每个 ISLE term项应当做什么这正是规范语言的职责它用声明式的方式描述 term 的语义再交给 cvc5 / z3 等 SMT 求解器去证明规则链满足这些语义。从源码看规范语言的解析结果由 spec.rs 中的SpecEnv承载它是验证的核心数据结构pub struct SpecEnv { /// Specification for the given term. pub term_spec: HashMapTermId, Spec, /// State elements. pub state: VecState, /// Terms that should be chained. pub chain: HashSetTermId, /// Tags applied to each term. pub term_tags: HashMapTermId, HashSetString, // Type instantiations for the given term. pub term_instantiations: HashMapTermId, VecSignature, /// Rules for which priority is significant. pub priority: HashSetRuleId, /// Model for the given type. pub type_model: HashMapTypeId, Compound, /// Value for the given constant. pub const_value: HashMapSym, Expr, /// Macro definitions. pub macros: HashMapString, Macro, }可以看到规范语言的所有顶层构造——model、spec、state、instantiate、attr、macro——最终都收敛到这个环境中供后续的规则链展开expand、条件生成Conditions见 veri.rs与 SMT 求解使用。下面我们按语言文档的脉络逐一展开。二、类型TypesISLE 类型到验证域的映射ISLE 中的每个类型在验证域中都有一个对应的模型model通过(model ...)声明建立映射(model isle_type (type type))例如 filetests 中常见的一段声明见 add_commutative.isle(type Value (primitive Value)) (model Value (type (bv 8)))即把 ISLE 的Value类型建模为 8 位位向量。验证域的类型type可以是原始类型、命名类型或复合类型。原始类型Primitives写法含义Int数学整数无界Bool布尔值(bv)宽度未知的位向量(bv n)固定宽度位向量如(bv 8)、(bv 64)Unit单元类型!未指定类型Unspecified_自动类型Auto交由类型推断推导!未指定的存在意义在文档中有明确说明当必须给出某个类型才能继续但它与手头问题无关时用它做占位。例如一个枚举类型可能引入了携带新类型的变体这些类型并不重要但需要某种规范。在 types.rs 中Type::Unspecified在is_concrete()中被视为具体类型且Display渲染为⨳符号而Type::Unknown对应_则被当作非具体类型需要在类型推断中求解。命名类型Named命名类型引用会解析到与isle_type相同的验证域类型模型(named isle_type)即允许用(named Value)指代已经建模的Value类型。在实现上Compound::Named(Ident)需要通过SpecEnv::resolve_type在type_model中查找对应的模型若找不到会报错并提示Add a(model ...)form。结构体Structs结构体是纯结构类型purely structurally typed即按字段布局定义(struct (field1 type1) (field2 type2) ... )枚举Enums验证域中存在枚举类型但用户不能自定义——它们只能从对应的 ISLE 枚举类型自动推断而来Compound::from_isle会把 ISLE 的sema::Type::Enum转换为验证域的Compound::Enum。不过文档允许一种例外可以用自定义的非枚举模型覆盖某个 ISLE 枚举被推断出的枚举类型。也就是说如果你不想按枚举语义建模可以显式(model MyEnum (type Int))之类把该 ISLE 枚举当作整数建模。三、规范声明Specifications描述 term 的语义契约Term 规范specification是规范语言的核心形式如下(spec (term params...) (modifies state cond?) (provide expr...) (require expr...) (match expr...) )其中所有expr...列表必须为布尔表达式且多个表达式会被隐式包进(and exprs...)即所有条件同时成立。四个子句的语义(modifies state cond?)声明该 term 对状态变量的修改行为详见后文状态一节。(provide expr...)term 的后置条件。当 term 作为被调用方callee出现时后置条件被假定assumed当 term 作为调用方caller即规则展开的根出现时后置条件被断言asserted。(require expr...)term 的前置条件。语义与 provide 相反作为 callee 时被断言作为 caller规则展开根时被假定。(match expr...)只能出现在部分 termpartial terms的规范中即非无懈可击的 extractor可能失败的提取器或部分构造器partial constructor。部分 term 可视为隐式返回Option类型match子句指定了返回值是Some(..)时须满足的条件此时provide规范是以 match 规范成立为前提的条件化。一个直观的例子来自 priority_operand_size.isle(decl fits_in_32 (Type) Type) (extern extractor fits_in_32 fits_in_32) (spec (fits_in_32 ty) (provide ( result ty)) (match ( result 32)))fits_in_32是一个 extractor它只有在类型宽度不超过 32 时才匹配成功match匹配成功时结果等于输入provide。另一个展示 match 只条件化 provide 的回归测试见 provide_only_if_match.isleextractorodd73的provide( result #x41)只有在match奇数成立时才被假定。变量作用域规则规范表达式中可访问的变量取决于 term 类型与子句。对于参数为(term params...)、隐式结果保存在特殊变量result中的 term构造器Constructor输入是[params...]输出是[result]提取器Extractor输入是[result]输出是[params...]注意方向相反extractor 是从结果反推参数。变量的可见性规则变量来源可用范围Term 输入参数所有子句Term 输出result或提取器参数仅provide子句状态变量State全局所有子句可用修改条件变量modifies cond所有子句可用在 spec.rs 中Spec结构体正是按此建模args、ret固定为result标识符、provides、requires、matches、modifies各自独立保存。四、表达式Expressions规范中的值语言规范表达式是构造后置/前置条件的值语言支持以下形式。常量Constants整数decimal如42位向量#bbinary二进制如#b1010或#xhex十六进制如#x2a布尔值true/false。实现中常量由 types.rs 的Const枚举表示Bool/Int/BitVector位向量内部用BigUint承载任意宽度。变量Variables普通标识符引用作用域内的变量可指代term 参数、隐式result、let/with 绑定、宏参数、已声明的状态以及状态修改路径条件。运算符应用Operator Applications形式为(op args...)可用运算符见下一节。Let 绑定Let Bindings用带初始化器的表达式引入新变量并求值为可引用新变量的 body(let ( (v1 init1) (v2 init2) ... ) body )注意let 绑定不得遮蔽shadow外层作用域中的变量同名是不允许的。With 绑定With Bindingswith表达式把新的、未初始化的变量引入作用域再求值 body(with (v1 v2 ...) body )与 let 的区别在于变量没有初始值表达式——它们更像是声明性的自由变量。字段访问Field Access表达式(:field x)访问结构体值x的field字段。判别器Discriminator表达式(?variant x)当枚举值x是给定变体时求值为 true。变体构造Variant Constructor(enum.variant fields...)用指定变体和可选字段构造一个枚举值如(Op.Add42)无字段或带字段的形式。结构体构造Struct Constructor(struct (field value) ...)用给定字段构造结构体值。Match 运算符Matchmatch 运算符对枚举类型做模式匹配(match on ((enum1.variant1 fields1...) body1) ((enum2.variant2 fields2...) body2) ... )整个表达式的值是匹配到on的那个分支的 body字段会被带入作用域如果没有分支匹配值未定义。真实用法见 enum_exhaustive.isle(spec (op_xy op x y) (provide ( result (match op ((Add) (bvadd x y)) ((Mul) (bvmul x y)) )) ) )⚠️ 文档特别提醒在实现中match与switch被区别对待——match是一等表达式类型而switch是运算符。文档原文指出这没有道理应当修复This makes no sense and should be fixed但对用户没有区别。这也解释了 spec.rs 中ExprKind::Match与ExprKind::Switch分立的现状。宏展开Macro Expansion(macro! args...)以给定参数求值宏macro宏的定义见后文。限定表达式Qualified Expressions(as x ty)求值为x同时提供类型推断注解要求x必须具有类型ty。它在位向量宽度无法从上下文推断时非常关键——type_qualifier.isle 专门为此设计(spec (add_then_mask x y) (provide ( result (extract 7 0 (bvadd x (as y (bv 16)))))))注释明确说明没有这个(as ...)限定类型推断会欠约束underconstrained。在 veri.rs 中(as ...)会生成Qualifier { value, ty }记录供类型推断阶段消费。五、运算符全集Operators规范表达式支持完整的一阶逻辑 SMT-LIB 运算符集合分为以下几类布尔运算Eq // 相等 And // 与变参 Or // 或变参 Not // 非 Imp // 蕴含整数比较Lt Lte Gt Gte位向量按位运算直接对应 SMT-LIBBVNot BVAnd BVOr BVXor位向量算术运算直接对应 SMT-LIBBVNeg BVAdd BVSub BVMul BVUdiv BVUrem // 无符号除 / 余 BVSdiv BVSrem // 有符号除 / 余 BVShl BVLshr BVAshr // 逻辑左移 / 逻辑右移 / 算术右移位向量比较运算直接对应 SMT-LIBBVUle BVUlt BVUgt BVUge // 无符号 BVSlt BVSle BVSgt BVSge // 有符号位向量溢出检查SMT-LIB 待标准化BVSaddo // 有符号加法溢出检测脱糖后的位向量算术运算desugaredRotr Rotl // 循环右移 / 左移 Extract // 提取位段带位界参数 ZeroExt SignExt // 零扩展 / 符号扩展 Concat // 位向量拼接变参浮点运算IEEE 754-2008FPPositiveInfinity FPNegativeInfinity FPPositiveZero FPNegativeZero FPNaN FPAdd FPSub FPMul FPDiv FPMin FPMax FPNeg FPSqrt FPIsZero FPIsInfinite FPIsNaN FPIsNegative FPIsPositive自定义编码custom encodingsPopcnt // 统计 1 的个数 Clz // 统计前导零 Cls // 统计前导符号位 Rev // 位反转转换运算conversionsConvTo // 位宽转换不显式扩展 Int2BV // 整数转位向量 BV2Nat // 位向量转自然数 WidthOf // 取位向量宽度控制运算If // 条件表达式if-then-else Switch // 基于值的多路分支运算符形态从 veri.rs 的Expr枚举可以看到上述运算符在验证域中被编译为带ExprId引用的结构化表达式树sources()方法递归收集子表达式用于可达性分析与 SMT 编码。六、宏Macros规范宏可以这样声明(macro (name params...) body)宏展开形式为(name! args...)。宏体在参数被设为实参值的作用域中求值结果替换展开表达式的位置。宏参数在宏体中就作为普通变量使用。宏可以互相嵌套调用——macro_calls_macro.isle 展示了在宏展开实参里再传入一个匿名宏(macro (apply_op op x y) (op! x y)) (spec (add_with_macro x y) (provide ( result (apply_op! (macro (a b) (bvadd a b)) x y))))在 spec.rs 中宏定义收集到SpecEnv::macros: HashMapString, Macro而宏展开ExprKind::Expand会延迟到验证条件生成阶段才进行内联展开veri.rs 中专门注释说明了这一延迟设计。七、类型实例化Type Instantiation由于 ISLE 中许多 term 是多态的作用于多个类型规范语言允许用instantiate枚举一个 term 可能的类型签名(instantiate term sigs...)其中每个 term 签名的形式为((args types...) (ret type))由于某些类型实例化非常常见可以把一组签名声明为form(form name sigs...)然后在instantiate声明中作为简写引用(instantiate term form)验证时所有出现 term 的类型实例化会取笛卡尔积cartesian product考虑当然在进入验证之前许多组合已经被类型推断排除掉了。一个需要显式实例化的真实场景是 enum_variant_instantiation.isle(type Op (enum (Add42) (Unused (val Value)) ) ) ; Provide instantiations for the unused variant. (instantiate Op.Unused ((args (bv 8)) (ret (named Op))) )这里Op.Unused变体携带一个Value字段而类型推断无法推断Value的位宽因此显式给出实例化(args (bv 8)) (ret (named Op))。实现上collect_instantiationsspec.rs会先收集所有form签名再解析instantiate声明带 tag 的实例化tagged_term_instantiations只在运行排除集不含对应 tag 时才生效例如把slow标记的高开销实例化留给专门的运行。八、状态State建模执行副作用与陷阱验证器的执行状态execution state机制通过state声明引入(state name (type type) (default default) )type是前文所述的验证域类型default是一个必须为布尔值的表达式它在状态变量绑定到同名变量name的作用域中被求值——即描述状态处于默认情形时成立的条件。状态变量作为全局变量可从所有 spec 访问。modifies子句决定默认规范在什么条件下被应用(modifies state)无条件声明修改状态变量state。此时state的默认规范被禁用因为状态已被改变默认情形不再成立。(modifies state cond)以条件变量cond为条件地修改state。这种情况下对应的 spec 必须提供约束来定义cond何时成立以及若成立时对state的隐含约束。state的默认规范只在cond为 false 时适用。无条件修改等价于断言cond恒为真的条件修改。在验证中对于给定状态收集到的所有条件变量cond1、cond2……默认规范会被条件化假定为( (not (or cond1 cond2 ...)) default)也就是说只要没有任何修改条件成立就假定状态处于默认情形。这种机制的实际用途README 有详细说明是建模陷阱与浮点 NaN 松弛。例如 mid-end 的浮点simplify规则需要比整数规则更弱的健全性契约CLIF 浮点算术产生 NaN 时可以返回任意算术 NaN符号与载荷任意因此(fmul (fneg x) (fneg y)) (fmul x y)这类重写虽然改变 NaN 符号仍是正确的。模型通过一个relax_nan状态标志实现默认 false每个浮点算术操作fadd/fsub/fmul/fdiv/sqrt/fmin/fmax等声明(modifies relax_nan ...)仅在产生 NaN 时置 true确定性位操作fneg/fabs/fcopysign不修改它。simplify契约再读取标志(if relax_nan (fp_equiv! result arg) ( result arg))其中fp_equiv在两个值按位相等或均为算术 NaN时成立。整个模型完全存在于 spec 层验证器无需特例处理。九、属性Attributes链式展开、优先级与标签属性可以应用到 term 和规则上(attr rule? name kind)不带rule关键字时默认视为 term 属性。(attr term (veri chain))—— 规则链展开标记为 chaining 的 term 在验证中可以省略规范spec。此时该 term 的所有可能规则应用都会被生成并验证。换句话说chain 属性是用规则本身替代手写规范的机制——这正是 README 所述大多数辅助 term 通过规则链验证的基础。从源码看spec.rs 的check_for_chained_terms_with_spec断言被标记 chain 的 term 不得再有手写 spec。(attr rule rule (veri priority))—— 规则优先级在验证中声明较低优先级规则的正确性依赖于本规则不匹配。在规则展开期间任何带 priority 标签的、更高优先级的重叠规则其匹配条件会被取反并加入验证条件negated and added to the verification conditions。文档对使用此属性给出了重要警告如果高优先级规则的匹配条件的规范是真实情况的超近似over-approximation那么低优先级规则所做的假设就是欠近似under-approximation——极端情况下验证器会判定低优先级规则从不适用更微妙的情况下可能漏掉真正的 bug。因此 priority 属性需要谨慎使用。真实用例见 priority_operand_size.isle规则operand_size_32优先级为 1规则operand_size_64依赖前者不匹配才能成立(rule operand_size_32 1 (test (fits_in_32 ty)) (OperandSize.Size32)) (rule operand_size_64 (test (fits_in_64 ty)) (OperandSize.Size64)) (attr rule operand_size_32 (veri priority))另一个回归测试 provide_only_if_match.isle 验证了 priority 语义的一个重要细节取反的是高优先级规则的 match 条件而不是其 provide——test_tails规则否定test_odd73_heads的match奇数判定但仍保留其provide不受影响。(attr rule? name (tag tag))—— 标签分类Tag 属性用于给 term 和规则分类。它们没有语义含义但对命令行过滤验证、以及聚合展示验证状态很有用。从SpecEnv的term_tags/rule_tags字段都是HashMap.., HashSetString可以看到标签以集合形式存储一个 term/规则可有多个标签。十、综合实战读懂一个完整的规范文件把上述语法组合起来看一个覆盖 spec match 枚举 条件表达式的完整例子enum_exhaustive.isle; 8-bit value type (type Value (primitive Value)) (model Value (type (bv 8))) ; Operation type. (type Op (enum (Add) (Mul))) ; Top-level test term asserts equality (decl test (Value) Value) (spec (test arg) (provide ( result arg))) ; op(x, y) (decl op_xy (Op Value Value) Value) (extern extractor op_xy op_xy) (spec (op_xy op x y) (provide ( result (match op ((Add) (bvadd x y)) ((Mul) (bvmul x y)) )) ) ) ; op(y, x) (decl op_yx (Op Value Value) Value) (extern constructor op_yx op_yx) (spec (op_yx op x y) (provide ( result (match op ((Add) (bvadd y x)) ((Mul) (bvmul y x)) )) ) ) ; Test rule commutes operands (rule test (test (op_xy op x y)) (op_yx op x y))该测试证明交换加法/乘法操作数的重写规则op_xy与op_yx的 provide 都按op枚举的变体分情形定义SMT 求解器据此验证(test (op_xy op x y)) (op_yx op x y)对所有枚举变体成立。这个文件位于 veri 的 filetests 目录可通过cargo test或 filetests 框架运行见 veri/filetests.rs。十一、如何运行验证器与进一步阅读书写规范语言本身并不直接执行验证最终需要交给veri二进制配合 SMT 求解器运行依赖 cvc5 与 z3详见 veri/README.md 的 Dependencies 一节。例如验证 AArch64 后端默认规则链cargo run -p cranelift-isle-veri --bin veri -- --default-excludes验证 mid-end 优化单元中某条具体规则如x0xcargo run -p cranelift-isle-veri --bin veri -- --name opt --rule iadd_x_plus_zero也可以使用配置文件如 configs/aarch64-fast.args集中管理命令行参数。仓库中的规范语言示例集中在 veri/filetestspass/broken/spec_conflict 三组生产环境的真实规范位于 cranelift/codegen/src/specmid-endopt.isle与 cranelift/codegen/src/isa/aarch64/spec由 ARM ASL 规范推导的 ISA 语义README 的 ISA Specifications 一节有详细说明。语言文档正文之外规范语言的解析与语义定义可以参考 cranelift/isle/veri/veri/src/spec.rsSpecEnv/Spec/State 结构与 cranelift/isle/veri/veri/src/types.rsType/Compound/Const 类型系统。结语VeriISLE 规范语言是一个小而完整的声明式形式化语言类型模型把 ISLE 类型映射到验证域spec 用 provide/require/match/modifies 四类子句刻画 term 的前置、后置与匹配语义表达式层覆盖布尔逻辑、位向量、浮点、转换与宏展开instantiate/form 处理多态实例化state 机制建模陷阱与浮点 NaN 等执行状态attr 则控制链式验证与优先级语义。理解这套语言是阅读 Cranelift 各后端规范文件、参与指令选择验证工作的第一步。赞分享语言运行时JIT编译编译器【免费下载链接】wasmtimeA lightweight WebAssembly runtime that is fast, secure, and standards-compliant项目地址https://gitcode.com/gh_mirrors/wa/wasmtime点击查看免费下载相关推荐VeriISLE 验证器基于 SMT 的 Cranelift ISLE 指令选择与优化规则形式化验证实战VeriISLE 验证器基于 SMT 的 Cranelift ISLE 指令选择与优化规则形式化验证实战 导读 VeriISLE 是 Wasmtime 项目语言运行时JIT编译编译器Aptos Move 规范语言Specification Language完整参考从函数契约到循环不变量的形式化验证实践Aptos Move 规范语言Specification Language完整参考从函数契约到循环不变量的形式化验证实践 导读 本文是面向 Aptos 链区块链Web3Vim Unicode规范化完全指南如何选择NFC、NFD等规范化形式Vim Unicode规范化完全指南如何选择NFC、NFD等规范化形式 Vim作为一款强大的文本编辑器在处理多语言和Unicode字符时表现出色。Unico文档教程开发工具上一篇GitHub_Trending/ai/aie-book内容定位AI工程教育的新范式下一篇告别Math.random()Rando.js让JavaScript随机数生成变得超级简单创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考