Scilla检查器¶

Scilla 检查器 (scilla-checker) 用作编译器前端，解析合约并执行静态检查，包括类型检查。

Scilla 检查器的阶段¶

Scilla 检查器在不同的阶段运行，每个阶段都可以执行检查（并可能拒绝未通过检查的合约）并为每段语法添加注释：

词法分析读取合约代码并构建抽象语法树（AST）。树中的每个节点都以行号和列号的形式使用源文件中的位置进行注释。
ADT 检查检查用户定义的 ADT 上的各种约束。
类型检查检查合约中的值是否以与类型系统一致的方式使用。类型检查器还用它的类型注释每个表达式。
模式检查检查合约中的每个模式匹配是否是详尽的（这样不会因为找不到匹配而导致执行失败），并且每个模式都可以到达（这样开发者不会无意中引入一个永远无法到达的模式分支）。
Event-info 检查合约中的消息和事件是否包含所有必需的字段。对于事件，如果合约发出两个具有相同名称（_eventname）的事件，则它们的结构（字段和类型）也必须相同。
现金流分析分析变量、字段和 ADT 的使用，并尝试确定哪些字段用于表示（原生）区块链货币。不执行任何检查，但表达式、变量、字段和 ADT 都使用标记进行注释，表明它们的用法。
付款承兑检查检查付款承兑合约。如果合约没有接受付款的 transition，那么它会发出警告。此外，如果 transition 具有任何包含多个接受语句的代码路径的可能，则检查会引发警告。此检查不会引发错误，因为不可能通过静态分析在所有情况下都确定是否会到达多个接受语句（如果存在），原因是这可能取决于仅在运行时已知的条件。 Scilla 检查器仅在命令行上指定 -cf 标志时才执行此检查，即它与现金流分析一起执行。例如，可互换代币合约通常不需要接受语句，因此此检查不是强制性的。
健全性检查执行多种次要检查，例如，transition 或procedure 的所有参数都具有不同的名称。

注释¶

Scilla 检查器中的每个阶段都可以为抽象语法树中的每个节点添加注释。注解的类型通过模块签名 Rep 的实例化来指定。 Rep 指定类型 rep，即注释的类型：

module type Rep = sig
  type rep
  ...
end

除了注释类型之外，Rep 的实例化还可以声明辅助函数，允许后续阶段访问先前阶段的注释。其中一些函数在 Rep 签名中声明，因为它们涉及创建新的抽象语法节点，必须从解析器开始使用注释创建这些节点：

module type Rep = sig
  ...

  val mk_id_address : string -> rep ident
  val mk_id_uint128 : string -> rep ident
  val mk_id_bnum    : string -> rep ident
  val mk_id_string  : string -> rep ident

  val rep_of_sexp : Sexp.t -> rep
  val sexp_of_rep : rep -> Sexp.t

  val parse_rep : string -> rep
  val get_rep_str: rep -> string
end

如果注释是已执行的阶段之一，则 mk_id_<type> 使用适当的类型注释创建标识符。如果类型检查器还没有被执行，函数就简单地创建一个（无类型的）标识符和一个虚拟位置。

rep_of_sexp 和 sexp_of_rep 用于美观打印。如果 rep 是用 [@@deriving sexp]` 指令定义的，那么它们会自动生成。

parse_rep 和 get_rep_str 用于缓存类型检查的库，因此如果它们没有改变就不需要再次检查它们。这些可能会在 Scilla 检查器的未来版本中被删除。

例如，考虑注释模块 TypecheckerERep：

module TypecheckerERep (R : Rep) = struct
  type rep = PlainTypes.t inferred_type * R.rep
  [@@deriving sexp]

  let get_loc r = match r with | (_, rr) -> R.get_loc rr

  let mk_id s t =
    match s with
    | Ident (n, r) -> Ident (n, (PlainTypes.mk_qualified_type t, r))

  let mk_id_address s = mk_id (R.mk_id_address s) (bystrx_typ address_length)
  let mk_id_uint128 s = mk_id (R.mk_id_uint128 s) uint128_typ
  let mk_id_bnum    s = mk_id (R.mk_id_bnum s) bnum_typ
  let mk_id_string  s = mk_id (R.mk_id_string s) string_typ

  let mk_rep (r : R.rep) (t : PlainTypes.t inferred_type) = (t, r)

  let parse_rep s = (PlainTypes.mk_qualified_type uint128_typ, R.parse_rep s)
  let get_rep_str r = match r with | (_, rr) -> R.get_rep_str rr

  let get_type (r : rep) = fst r
end

函子（参数化结构）将前一阶段的注释作为参数 R。在 Scilla 检查器中，前一阶段是解析器，但可以通过在顶层解释器指定阶段来把任何阶段添加到两个阶段之间。

rep 类型指定新注释是类型和前一个注释的一对。

函数 get_loc 只是作为上一阶段 get_loc 函数的代理。

函数 mk_id 是 mk_id_<type> 函数的辅助函数，它使用适当的类型注释创建标识符。

mk_rep 函数是类型检查器使用的辅助函数。

美观打印不输出 AST 节点的类型，因此函数 parse_rep 和 get_rep_str 忽略类型注释。

最后，函数 get_type 提供对后续阶段的类型信息的访问。这个函数在 Rep 签名中没有提到，因为一旦类型注释被添加到 AST，它就会被类型检查器使用。

抽象语法¶

ScillaSyntax 函子定义了 AST 节点类型。每个阶段都会将函子实例化两次，一次用于输入语法，一次用于输出语法。这两个语法实例的区别仅在于每个语法节点的注释类型。如果阶段不产生额外的注释，则两个实例化将是相同的。

参数 SR 和 ER 都是 Rep 类型，分别定义语句和表达式的注释。

module ScillaSyntax (SR : Rep) (ER : Rep) = struct

  type expr_annot = expr * ER.rep
  and expr = ...

  type stmt_annot = stmt * SR.rep
  and stmt = ...
end

初始注释¶

解析器生成初始注释，其中仅包含有关语法节点在源文件中的位置的信息。函数 get_loc 允许后续阶段访问该位置。

ParserRep 结构用于语句和表达式的注释。

module ParserRep = struct
  type rep = loc
  [@@deriving sexp]

  let get_loc l = l
  ...
end

典型阶段¶

产生附加注释的每个阶段都需要提供 Rep 模块类型的新实现。实现应该以之前的注释类型（作为实现 Rep 模块类型的结构体）作为参数，这样阶段的注释就可以添加到之前阶段的注释中。

类型检查器向 AST 中的每个表达式节点添加类型，但不会向语句节点注释添加任何内容。因此，类型检查器只为表达式定义一个注释类型。

此外，Rep 实现定义了一个函数 get_type，以便后续阶段可以访问注释中的类型。

module TypecheckerERep (R : Rep) = struct
  type rep = PlainTypes.t inferred_type * R.rep
  [@@deriving sexp]

  let get_loc r = match r with | (_, rr) -> R.get_loc rr

  ...
  let get_type (r : rep) = fst r
end

Scilla 类型检查器获取上一阶段的语句和表达式注释，然后实例化 TypeCheckerERep （创建新的注释类型）、ScillaSyntax （创建前一阶段的抽象语法类型，作为类型检查器的输入）和 ScillaSyntax （创建类型检查器输出的抽象语法类型）。

module ScillaTypechecker
  (SR : Rep)
  (ER : Rep) = struct

  (* No annotation added to statements *)
  module STR = SR
  (* TypecheckerERep is the new annotation for expressions *)
  module ETR = TypecheckerERep (ER)

  (* Instantiate ScillaSyntax with source and target annotations *)
  module UntypedSyntax = ScillaSyntax (SR) (ER)
  module TypedSyntax = ScillaSyntax (STR) (ETR)

  (* Expose target syntax and annotations for subsequent phases *)
  include TypedSyntax
  include ETR

  (* Instantiate helper functors *)
  module TU = TypeUtilities (SR) (ER)
  module TBuiltins = ScillaBuiltIns (SR) (ER)
  module TypeEnv = TU.MakeTEnv(PlainTypes)(ER)
  module CU = ScillaContractUtil (SR) (ER)
  ...
end

至关重要的是，类型检查器模块公开了它生成的注释和语法类型，以便它们可用于下一阶段。

类型检查器最终会实例化辅助函子，例如 TypeUtilities 和 ScillaBuiltIns。

现金流分析¶

现金流分析阶段分析合约变量、字段和 ADT 构造函数的使用，并尝试确定哪些字段和 ADT 用于表示（原生）区块链货币。每个合约字段都用一个标签进行注释，指示该字段的用法。

结果标签是基于合约字段、变量和 ADT 构造函数的使用的近似值。标签不保证准确，但旨在作为帮助合约开发人员以预期方式使用其字段的工具。

运行分析¶

通过使用选项 -cf 运行 scilla-checker 来激活现金流分析。默认情况下不运行分析，因为它仅打算在合约开发期间使用。

合约永远不会因为现金流分析的结果而被拒绝。由合约开发者决定现金流标签是否与每个合约字段的预期用途一致。

详细分析¶

分析的工作方式是不断分析合约的 transition 和 procedure，直到没有收集到进一步的信息。

分析的起点是调用合约 transition 的传入消息、合约可能发送的传出消息和事件、合约的账户余额以及从区块链读取的任何字段，例如当前区块高度。

传入和传出消息都包含一个字段 _amount，其值是消息在帐户之间转移的金额。每当传入消息的 _amount 字段的值加载到局部变量中时，该局部变量就会被标记为代表资金。类似地，用于初始化外发消息的 _amount 字段的局部变量也被标记为表示资金。

相反，已知消息字段 _sender、_origin、_recipient 和 _tag、事件字段 _eventname、异常字段 _exception 和区块链字段 BLOCKNUMBER 不代表货币，因此任何用于初始化这些字段或从这些字段之一读取保存值的变量都被标记为不代表资金。

一旦标记了某些变量，它们的用法就意味着如何标记其他变量。例如，如果两个标记为货币的变量相加，则结果也被视为代表货币。相反，如果两个标记为非货币的变量相加，则结果被视为代表非货币。

当加载或存储合约字段而使用局部变量时，会发生合约字段的标记。在这些情况下，该字段被认为具有与局部变量相同的标签。

自定义 ADT 的标记是在它们用于构造值时以及在模式匹配中使用时完成的。

一旦 transition 或 procedure 被分析时，局部变量和它们的标签就会被保存并且分析继续到下一个 transition 或 procedure，同时保留合约字段和 ADT 的标签。分析一直持续到所有 transition 和 procedure 都已分析完毕，同时没有任何现有标签已经更改。

标签¶

分析使用以下标签集：

No information：未收集到有关该变量的信息。这有时（但并非总是）表明该变量未被使用，同时还表明它存在潜在错误。
Money：变量代表货币。
Not money：变量代表货币以外的东西。
Map t`（其中 `t 是一个标签）：该变量表示一个映射或一个函数，其共同域被标记为 t。因此，当在映射中执行查找时，或对存储在映射中的值应用函数时，结果用 t 标记。映射的键总是被假定为 Not money。使用变量作为函数参数不会产生标签。
T t1 … tn`（其中 `T 是 ADT，t1 … tn 是标签）：变量表示 ADT 的值，例如 List 或 Option。标签 t1 … tn 对应于 ADT 的每个类型参数的标签。（请参阅下面的简单 example。）
Inconsistent：该变量已被用于表示货币和非货币。不一致的用法表示存在错误。

仅部分支持库函数和本地函数，因为没有尝试将参数标签连接到结果标签。但是，完全支持内置函数。

一个简单的例子¶

思考以下代码片段：

match p with
| Nil =>
| Cons x xs =>
  msg = { _amount : x ; ...}
  ...
end

x 用于初始化消息的 _amount 字段，因此 x 被标记为 Money。由于 xs 是列表的尾部，其中 x 是第一个元素，因此 xs 必须是与 x 具有相同标签的元素列表。由于存在 List 'A 类型具有一个类型参数的事实，因此 xs 被标记为 List Money。

类似地，p 与模式 Nil 和 Cons x xs 匹配。 Nil 是一个列表，但由于列表是空的，我们对列表的内容一无所知，因此 Nil 模式对应于标签 List (No information)。 Cons x xs 也是一个列表，但这次我们确实知道了一些关于内容的信息，即第一个元素 x 用 Money 标记，列表的尾部用 List Money 标记。因此，Cons x xs 对应于 List Money。

统一两个标签 List (No information) 和 List Money 从而给出了 List Money 标签，所以 p 被标记为 List Money。

ADT 构造函数标记¶

除了标记字段和局部变量，现金流分析器还标记自定义 ADT 的构造函数。

要了解其工作原理，请思考以下自定义 ADT：

type Transaction =
| UserTransaction of ByStr20 Uint128
| ContractTransaction of ByStr20 String Uint128

用户交易是接收方为用户账户的交易，因此 UserTransaction 构造函数采用两个参数：接收方用户账户的地址和要转账的金额。

合约交易是接收方是另一个合约的交易，因此 ContractTransaction 接受三个参数：接收方合约的地址、在接收方合约上调用的 transition 名称以及要转移的金额。

就现金流而言，很明显，两个构造函数的最后一个参数都用于表示货币，而所有其他参数都用于表示非货币。因此，现金流分析器尝试使用前几节中描述的原则，用适当的标签来标记两个构造函数的参数。

一个更详细的例子¶

例如，思考一下用 Scilla 编写的众筹合约。这样的合约可以声明以下不可变参数和可变字段：

contract Crowdfunding

(*  Parameters *)
(owner     : ByStr20,
max_block : BNum,
goal      : Uint128)

(* Mutable fields *)
field backers : Map ByStr20 Uint128 = ...
field funded : Bool = ...

owner 参数表示部署合约的人的地址。 goal 参数是所有者试图筹集的金额，max_block 参数表示达到目标的截止日期。

字段 backers 是捐赠者地址与捐赠金额的映射，funded 字段表示目标是否已经达到。

由于字段 goal 代表金额，因此分析应将目标标记为 Money。类似地，backers 字段是一个带有代表 Money 的共同域的映射，因此应使用 Map Money 标记捐赠者。

相反，owner、max_block 和 funded 都代表货币以外的东西，所以它们都应该被标记为 Not money。

现金流分析将根据参数和字段在合约的 transition 和 procedure 中的使用情况对其进行标记，如果结果标签与预期不符，则合约可能在某处包含错误。