分析设置

引用安全性分析被设置为一个流分析（或抽象解释）。为抽象执行基本块的代码定义了一个抽象状态。维护一个从基本块到抽象状态映射。给定一个基本块 B 开始时的抽象状态 S，B 的抽象执行结果为状态 S'。这个状态 S' 被传播到 B 的所有后续状态，并记录在映射中。如果一个块已存在一个状态，新传播的状态与现有状态“合并”。如果合并失败，则报告错误。如果合并成功但抽象状态保持不变，则不再进行进一步传播。否则，状态被更新并再次通过该块传播。在通过块传播抽象状态时处理指令时也可能报告错误。

抽象状态

抽象状态有三个组成部分

• 从局部变量到抽象值的局部映射。不在该映射域内的局部变量不可用。可用性是初始化概念的泛化。局部变量可能由于移动而初始化后变得不可用。抽象值可以是 引用(n)（对于引用类型的变量）或 值(ns)（对于值类型的变量），其中 n 是一个随机数，ns 是一组随机数。随机数用于表示引用。让 Nonce 代表所有随机数的集合。如果一个局部变量 l 映射到 Value(ns)，则表示存在指向存储在 l 中的值的未完成借用引用。对于 ns 中的每个成员 n，必须有一个局部变量 l 映射到 Reference(n)。如果一个局部变量 x 映射到 Reference(n)，并且存在局部变量 y 和 z 分别映射到 Value(ns1) 和 Value(ns2)，那么 n 可能同时是 ns1 和 ns2 的成员。这仅仅意味着分析是有损失的。当 l 映射到 Value({}) 时，这表示没有指向 l 的借用引用，因此 l 可能被销毁或移动。
• 从局部变量到抽象值的局部映射本身不足以检查字节码程序，因为字节码操作的价值可以是大型嵌套结构，其中包含指向中间的引用。指向值中间的引用可以被扩展以产生另一个引用。某些扩展应该被允许，但其他扩展则不应该。为了跟踪引用之间的相对扩展，抽象状态有第二个组件。这个组件是从随机数到以下两种借用信息之一映射的映射
• 一组随机数。
• 从字段到随机数集合的映射。

当前实现将此信息存储为两个具有不重叠域的单独映射

• borrowed_by 从 Nonce 映射到 Set<Nonce>。
• fields_borrowed_by 从 Nonce 映射到 Map<Field, Set<Nonce>>。
  • 如果 n2 在 borrowed_by[n1] 中，那么表示由 n2 表示的引用是 n1 表示的引用的扩展。
  • 如果 n2 在 fields_borrowed_by[n1][f] 中，表示由 n2 表示的引用是 n1 表示的 f 扩展的引用的扩展。基于这种直觉，将随机数 n 从 fields_borrowed_by 的域移动到 borrowed_by 的域，通过对 fields_borrowed_by[n] 域内所有字段对应的所有随机数集合进行并集操作，是一个有效的上界近似。
• 要在一个块的指令间传播抽象状态，必须也对栈上的值和引用进行建模。我们之前描述了如何将可用的栈后缀建模为类型栈。现在，我们将此栈的内容扩展为一个包含类型和抽象值的结构。我们维护一个不变性，即栈上的非引用值不能有挂起的借用。因此，如果栈上有抽象值 Value(ns)，那么 ns 是空的。

值和引用

让我们更详细地看看共享和专有的值和引用是如何建模的。

• 非引用值建模为 Value(ns)，其中 ns 是表示借用引用的随机数集合。只有当 ns 为空时，此值的销毁/移动/复制才被认为是安全的。栈上的值显然满足此属性，但局部变量中的值可能不满足。
• 引用被建模为 Reference(n)，其中 n 是一个随机数。如果引用被标记为共享，则始终允许读取访问，而不允许写入访问。如果一个引用 Reference(n) 被标记为独占，则只有当 n 没有借用时才允许写入访问，如果所有从 n 借用的随机数都位于标记为共享的引用中，则允许读取访问。此外，构造引用的规则保证，标记为共享的引用的扩展也必须标记为共享。这些检查共同提供了前面提到的引用透明性的属性。

目前，字节码语言不包含任何直接构造共享引用的构造函数。 BorrowLoc 和 BorrowGlobal 创建独占引用。 BorrowField 创建一个继承其标记自源引用的引用。移动操作（当应用于包含引用的局部变量时）将引用从局部变量移动到栈上。 FreezeRef 用于将现有的独占引用转换为共享引用。将来，我们可能会添加一个 BorrowGlobal 版本，该版本生成共享引用

错误。 如前所述，检查器在以下情况之一中报告错误：

• 无法证明指令在通过块传播抽象状态时是安全的。
• 通过不同入边传播的抽象状态的连接失败。

让我们更详细地看看上述错误报告的第二种原因。请注意，在块的开始时，表示可用栈后缀的可用类型和抽象值对的堆栈为空。因此，连接仅在表示可用局部变量和借用信息的抽象状态之间发生。只有在两个边上的可用局部变量集不同时，连接才会失败。如果可用变量的集相同，则连接本身很简单——借用的集合是逐点连接的。然而，有两个细节值得注意

• 沿两个边的抽象状态中使用的随机数集可能没有任何关联。由于实际的随机数值无关紧要，在进行连接之前，随机数被规范地映射到固定的整数（包含随机数的局部变量的索引）。
• 在连接过程中，如果随机数 n 在一边的 borrowed_by 的域中，在另一边的 fields_borrowed_by 的域中，则在执行连接之前，将 n 从 fields_borrowed_by 移动到 borrowed_by。

借用引用

每个引用构造函数 —— BorrowLoc，BorrowField，BorrowGlobal，FreezeRef 和 CopyLoc —— 都通过生成一个新的随机数来建模。虽然 BorrowLoc 从局部变量中的值借用，BorrowGlobal 从全局值池中借用。 BorrowField，FreezeRef 和 CopyLoc（当应用于包含引用的局部变量时）从源引用中借用。由于每个新的随机数都与所有先前生成的随机数不同，分析维护了这样一个不变量：所有可用的局部变量和引用类型的栈位置的抽象值都有不同的随机数表示。另一个重要不变量是，在借用信息中引用的每个随机数必须位于表示局部变量或栈位置的某个抽象值中。

释放引用。

全局和局部引用都通过ReleaseRef操作释放。如果一个函数在局部变量中未释放引用就返回，则是一个错误。所有的引用都必须显式释放。因此，使用StLoc操作覆盖可用引用是一个错误。

当引用被ReadRef、WriteRef、Eq和Neq操作消费时，会隐式释放。

全局引用

全局引用的安全性依赖于静态分析和动态分析的组合。静态分析不能区分全局和局部引用。但是，动态分析会区分它们，并对全局引用进行引用计数，如下所示：字节码解释器维护一个从地址和完全限定的资源类型对到联合（Rust枚举）的映射M，该联合包含以下值

• 空
• RefCount(n)，其中n >= 0

MoveFrom<T>(addr) {
    assert M[addr, T] == RefCount(0);
    M[addr, T] := Empty;
}

MoveToSender<T>(addr) {
    assert M[addr, T] == Empty;
    M[addr, T] := RefCount(0);
}

BorrowGlobal<T>(addr) {
    if let RefCount(n) = M[addr, T] then {
        assert n == 0;
        M[addr, T] := RefCount(n+1);
    } else {
        assert false;
    }
}

CopyLoc(ref) {
    if let Global(addr, T) = ref {
        if let RefCount(n) = M[addr, T] then {
            assert n > 0;
            M[addr, T] := RefCount(n+1);
        } else {
            panic false;
        }
    }
}

ReleaseRef(ref) {
    if let Global(addr, T) = ref {
        if let RefCount(n) = M[addr, T] then {
            assert n > 0;
            M[addr, T] := RefCount(n-1);
        } else {
            panic false;
        }
    }
}

*
├── invalid_mutations  # Library used by proptests
├── src                # Core bytecode verifier files
├── tests              # Proptests