企业官网建设流程全解析

• 语言运行时
• JIT编译
• 编译器

导读

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: HashMap<TermId, Spec>, /// State elements. pub state: Vec<State>, /// Terms that should be chained. pub chain: HashSet<TermId>, /// Tags applied to each term. pub term_tags: HashMap<TermId, HashSet<String>>, // Type instantiations for the given term. pub term_instantiations: HashMap<TermId, Vec<Signature>>, /// Rules for which priority is significant. pub priority: HashSet<RuleId>, /// Model for the given type. pub type_model: HashMap<TypeId, Compound>, /// Value for the given constant. pub const_value: HashMap<Sym, Expr>, /// Macro definitions. pub macros: HashMap<String, Macro>, }

可以看到，规范语言的所有顶层构造——model、spec、state、instantiate、attr、macro——最终都收敛到这个环境中，供后续的规则链展开（expand）、条件生成（Conditions，见 veri.rs）与 SMT 求解使用。下面我们按语言文档的脉络逐一展开。

二、类型（Types）：ISLE 类型到验证域的映射

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）

!（未指定）的存在意义在文档中有明确说明：当"必须给出某个类型才能继续，但它与手头问题无关"时，用它做占位。例如一个枚举类型可能引入了携带新类型的变体，这些类型并不重要但需要某种规范。在 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...>)：只能出现在部分 term（partial 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.isle：extractorodd73的provide（(= result #x41)）只有在match（奇数）成立时才被假定。

变量作用域规则

规范表达式中可访问的变量取决于 term 类型与子句。对于参数为(<term> <params...>)、隐式结果保存在特殊变量result中的 term：

• 构造器（Constructor）：输入是[<params...>]，输出是[result]；
• 提取器（Extractor）：输入是[result]，输出是[<params...>]（注意方向相反！extractor 是从结果反推参数）。

变量的可见性规则：

在 spec.rs 中，Spec结构体正是按此建模：args、ret（固定为result标识符）、provides、requires、matches、modifies各自独立保存。

四、表达式（Expressions）：规范中的值语言

规范表达式是构造后置/前置条件的值语言，支持以下形式。

常量（Constants）

• 整数：<decimal>，如42；
• 位向量：#b<binary>（二进制，如#b1010）或#x<hex>（十六进制，如#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 Bindings）

with表达式把新的、未初始化的变量引入作用域，再求值 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 运算符（Match）

match 运算符对枚举类型做模式匹配：

(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-LIB）：

BVNot BVAnd BVOr BVXor

位向量算术运算（直接对应 SMT-LIB）：

BVNeg BVAdd BVSub BVMul BVUdiv BVUrem // 无符号除 / 余 BVSdiv BVSrem // 有符号除 / 余 BVShl BVLshr BVAshr // 逻辑左移 / 逻辑右移 / 算术右移

位向量比较运算（直接对应 SMT-LIB）：

BVUle BVUlt BVUgt BVUge // 无符号 BVSlt BVSle BVSgt BVSge // 有符号

位向量溢出检查（SMT-LIB 待标准化）：

BVSaddo // 有符号加法溢出检测

脱糖后的位向量算术运算（desugared）：

Rotr Rotl // 循环右移 / 左移 Extract // 提取位段（带位界参数） ZeroExt SignExt // 零扩展 / 符号扩展 Concat // 位向量拼接（变参）

浮点运算（IEEE 754-2008）：

FPPositiveInfinity FPNegativeInfinity FPPositiveZero FPNegativeZero FPNaN FPAdd FPSub FPMul FPDiv FPMin FPMax FPNeg FPSqrt FPIsZero FPIsInfinite FPIsNaN FPIsNegative FPIsPositive

自定义编码（custom encodings）：

Popcnt // 统计 1 的个数 Clz // 统计前导零 Cls // 统计前导符号位 Rev // 位反转

转换运算（conversions）：

ConvTo // 位宽转换（不显式扩展） 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: HashMap<String, 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_instantiations（spec.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<.., HashSet<String>>）可以看到标签以集合形式存储，一个 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 优化单元中某条具体规则（如x+0==x）：

cargo run -p cranelift-isle-veri --bin veri -- --name opt --rule iadd_x_plus_zero

也可以使用配置文件（如 configs/aarch64-fast.args）集中管理命令行参数。仓库中的规范语言示例集中在 veri/filetests（pass/broken/spec_conflict 三组），生产环境的真实规范位于 cranelift/codegen/src/spec（mid-endopt.isle）与 cranelift/codegen/src/isa/aarch64/spec（由 ARM ASL 规范推导的 ISA 语义，README 的 ISA Specifications 一节有详细说明）。语言文档正文之外，规范语言的解析与语义定义可以参考 cranelift/isle/veri/veri/src/spec.rs（SpecEnv/Spec/State 结构）与 cranelift/isle/veri/veri/src/types.rs（Type/Compound/Const 类型系统）。

结语

VeriISLE 规范语言是一个小而完整的声明式形式化语言：类型模型把 ISLE 类型映射到验证域，spec 用 provide/require/match/modifies 四类子句刻画 term 的前置、后置与匹配语义，表达式层覆盖布尔逻辑、位向量、浮点、转换与宏展开，instantiate/form 处理多态实例化，state 机制建模陷阱与浮点 NaN 等执行状态，attr 则控制链式验证与优先级语义。理解这套语言，是阅读 Cranelift 各后端规范文件、参与指令选择验证工作的第一步。

• 语言运行时
• JIT编译
• 编译器