Rust程序的限界模型检测方法及装置

本发明属于计算机技术、rust程序限界模型检测，具体涉及一种rust程序的限界模型检测方法及装置。

背景技术：

1、首先对本发明涉及的技术术语解释如下：

2、中间表示: 在程序编译过程中，介于源代码和目标代码之间的一种表示形式，用于进行代码分析和优化。

3、公式: 在形式化验证中，用来描述程序性质和约束的逻辑表达式。

4、编码: 将程序的语义和性质转换为形式化逻辑公式的过程。

5、求解器: 自动化推理工具，用于求解形式化验证中的逻辑公式。

6、rust: 一种系统级编程语言，以其内存安全保证、并发安全和高性能而著称。rust的核心创新在于所有权系统，该系统在编译时进行检查，保证内存安全。

7、所有权: ownership。rust编程语言的核心概念，定义了如何管理内存的一套规则。所有权规则包括：每个值都有一个被称为其所有者的变量、值在任何时刻只能有一个所有者、当所有者离开作用域时值将被自动释放。

8、安全模式: safe mode。rust程序中不使用unsafe关键字编写的代码部分，在该模式下编译器会严格执行所有权和借用规则，保证内存安全。

9、非安全模式: unsafe mode。rust程序中使用unsafe关键字编写的代码部分，在该模式下编译器不执行借用检查，程序员需要手动保证内存安全。

10、特征: trait。rust语言中用于定义共享行为的一组方法接口，程序员可以为不同类型实现相应的特征。通过特征机制，代码能够以统一的方式处理不同类型，同时保持静态分发和零成本抽象的特性。

11、生命周期: lifetime。rust语言中用于确保引用有效性的编译时概念。生命周期描述了引用在其作用域内保持有效的时间范围，编译器通过生命周期分析防止悬垂引用等内存安全问题。

12、借用规则: borrowing rules。rust所有权系统的一部分，定义了如何在不获取所有权的情况下访问值的规则。借用规则包括：同一时间只能有一个可变引用或多个不可变引用，但可变引用和不可变引用不能同时存在；引用必须始终有效。

13、mir: mid-level intermediate representation。rust编译器内部使用的一种中间表示，位于高级抽象语法树和低级llvm中间表示之间。mir保留了rust的类型信息、所有权语义等重要信息，是进行rust程序分析和验证的理想表示形式。mir采用控制流图的结构，适合进行静态分析和验证。

14、goto-c: 一种用于形式化验证的c语言中间表示格式。

15、llvm: low level virtual machine。一个广泛使用的编译器基础设施项目，提供了一套中间表示和优化工具链。llvm中间表示是一种类型化的、静态单赋值形式的中间表示，被多种编程语言的编译器采用。

16、限界模型检测: bounded model checking (bmc)。一种形式化验证技术，通过将程序转换为逻辑公式并设置执行步数上限，使用可满足性模理论（smt）求解器来检测程序在限定步数内是否满足指定的性质。限界模型检测能够在合理的计算资源下，对程序进行深度的验证。

17、验证条件: verification condition (vc)。将静态分析结果转换为smt求解器可求解的逻辑公式的过程。验证条件表示待验证的性质的编码，通常是性质编码的否定。

18、smt求解器: satisfiability modulo theories solver。一种自动化推理工具，用于判断一阶逻辑公式在特定理论（如整数、数组、位向量等）下的可满足性。

19、sat: satisfiable。在可满足性理论和形式化验证中，sat表示逻辑公式存在至少一个解。当smt求解器返回sat时，表示验证条件可满足，即程序存在违反性质的路径（发现错误）。

20、unsat: unsatisfiable。在可满足性理论和形式化验证中，unsat表示逻辑公式不存在任何解。当smt求解器返回unsat时，表示验证条件不可满足，即程序在给定边界内满足指定性质（未发现错误）。

21、unknown: unknown。在可满足性理论和形式化验证中，unknown表示求解器无法在给定的时间和资源限制下确定逻辑公式的可满足性。这通常发生在问题过于复杂或超时的情况下。

22、静态分析: 在不执行程序的情况下，通过分析程序代码来推断程序属性的技术。静态分析可以用于检测潜在的错误、验证程序的性质、优化程序性能等。

23、所有权敏感静态分析: ownership-sensitive static analysis。一种专门为rust程序设计的静态分析技术，在静态分析过程中显式区分安全模式和非安全模式，并跟踪和维护堆对象的所有权语义。所有权敏感静态分析通过扩展分配状态函数的取值范围，能够精确表达堆对象在不同模式下的分配状态。

24、控制流图: control flow graph。一种用于表示程序执行流程的图形结构，其中节点表示基本块，边表示控制流跳转关系。控制流图是静态分析和优化的重要基础结构，广泛用于编译器优化、程序分析等形式化验证工具中。

25、虚拟函数表: virtual function table。在面向对象编程中，用于实现动态分发的一种数据结构。虚拟函数表存储了对象类型的函数指针，通过这些指针可以在运行时正确调用对象的方法。在限界模型检测中，虚拟函数表用于处理动态分发和trait多态。

26、rust是一种系统级编程语言，具有内存安全保证和零成本抽象的特点。其核心创新在于所有权类型系统，通过编译时检查确保内存安全，同时提供安全和非安全两种编程模式以平衡安全性和灵活性。尽管有强大的编译期保护，由于unsafe代码块的存在，内存安全风险在实际应用中仍然存在。限界模型检测是一种成熟的程序验证技术，通过将程序语义和待验证性质编码为逻辑公式，利用约束求解器进行自动化验证。为提高验证效率，该技术结合静态分析引擎进行优化，包括生成精炼的验证条件和减少求解器负担。静态分析引擎在验证过程中扮演关键角色，通过多种优化技术显著提升整体验证性能。

27、现有rust程序限界模型检测技术主要采用以下技术方案：

28、1）基于goto-c中间表示的限界模型检测技术。该技术方案首先将rust程序转换为goto-c中间表示，然后利用现有的基于goto-c的c程序限界模型检测框架进行验证。具体实现过程包括：通过rust编译器生成mir，然后将mir翻译为goto-c格式的程序。在翻译过程中，需要使用goto-c的语法结构来表示rust的复杂类型系统、trait多态、生命周期等特性。

29、2）基于llvm中间表示的限界模型检测技术。该技术方案基于rust编译链中的llvm中间表示进行限界模型检测。具体实现过程包括：通过rust编译器生成llvm二进制代码，然后提取llvm中间表示，利用现有的基于llvm的限界模型检测框架进行验证。

30、基于全面性分析，现有rust程序限界模型检测技术方案存在以下主要缺陷：

31、1）翻译过程丢失关键类型信息。现有技术方案在将rust程序翻译到其他中间表示的过程中，存在严重的类型信息丢失问题。goto-c作为c语言的中间表示格式，其类型系统无法完整表达rust复杂的类型体系，特别是rust特有的所有权、生命周期、借用规则等高级类型概念。llvm中间表示虽然提供了类型化支持，但主要为通用语言设计，同样无法保留rust的高级类型信息和所有权语义。这些丢失的类型信息和所有权语义对于程序验证具有重要价值，导致验证算法无法利用rust编译器提供的丰富语义约束，不仅增加了计算开销，还可能影响验证的准确性。

32、2）验证效率明显低下。由于缺失了rust类型信息和所有权语义，现有的限界模型检测算法采用传统的所有权无关静态分析方法，在验证效率方面存在显著局限。传统分析方法将所有堆对象统一处理，忽略了安全模式和非安全模式之间的本质差异，在状态表示和合并过程中产生大量不确定性，导致生成的验证条件规模庞大。smt求解器需要处理大量不必要的验证条件，在求解过程中面临巨大的计算负担，导致验证时间显著增加，整体验证效率低下。

33、3）工具链版本兼容性问题。现有基于llvm中间表示的验证技术需要从rust编译链中提取llvm二进制代码，再进行中间表示转换，涉及多个处理阶段，整个验证流程复杂且容易出错。每个阶段都可能引入信息损失或转换错误，增加了验证结果的不确定性。同时，llvm中间表示与rust编译器版本紧密耦合，不同版本的rust编译器生成的llvm代码可能存在差异，导致验证工具需要针对特定版本进行适配，增加了维护成本和使用门槛。当rust语言特性更新时，基于llvm的验证工具往往存在滞后性，无法及时支持新的语言特性

技术实现思路

1、针对现有技术存在的缺陷，本发明要解决的具体技术问题如下：

2、1）解决翻译过程丢失rust类型信息问题。针对现有技术在翻译过程中丢失rust类型信息和所有权语义的问题，本发明通过直接基于rust编译器的mir中间表示进行限界模型检测。mir作为rust编译器内部的一种表示，能够完整保留rust的类型系统信息、所有权语义、借用规则等关键内容。这种直接基于mir的分析方法避免了翻译过程中的信息损失，为后续的静态分析和验证条件生成提供了丰富的类型约束和语义信息，显著提高了验证的准确性。

3、2）提升验证效率。针对传统所有权无关静态分析验证效率低下的问题，本发明通过引入所有权敏感静态分析技术，显著提升了验证效率。所有权敏感分析通过扩展分配状态函数的取值范围和状态合并策略，能够精确表达堆对象在不同模式下的分配状态，减少状态表示的不确定性。这种优化策略使得在生成验证条件时，能够识别并消除大量不必要的验证条件，显著减少了smt求解器的求解负担，大幅提升了验证效率。

4、3）解决验证流程复杂且版本兼容性差的技术问题。针对现有基于llvm中间表示的验证技术流程复杂、容易出错以及与rust版本兼容性差的问题，本发明通过直接基于rust编译器的mir中间表示进行限界模型检测，避免了从rust编译链中提取llvm二进制代码再到中间表示转换的复杂多阶段处理过程。这种直接基于mir的方案简化了验证流程，减少了每个阶段可能引入的信息损失和转换错误，降低了验证结果的不确定性。同时，本发明与rust编译器内部表示直接对接，不再依赖llvm中间表示，解决了与rust编译器版本紧密耦合的问题，当rust语言特性更新时能够及时支持，提高了维护成本和使用便利性。

5、本发明采用的技术方案如下：

6、一种rust程序的限界模型检测方法，包括以下步骤：

7、获取rust程序的mir中间表示，对mir中间表示进行预处理；

8、对预处理后的mir中间表示进行所有权敏感静态分析，生成验证条件；

9、对验证条件进行切片优化，得到精简的验证条件；

10、利用smt求解器对精简的验证条件进行求解，根据求解结果生成验证报告。

11、进一步地，所述预处理包括：计算从入口函数可达的所有函数集合并构建函数表，识别程序中的循环结构和递归函数，构建虚拟函数表。

12、进一步地，所述所有权敏感静态分析包括：沿mir控制流传播抽象状态，并根据mir语句更新抽象状态中的赋值函数、指向函数和分配状态函数；根据预处理得到的循环结构和递归函数，在控制流图和调用图上按照预设展开边界进行有限展开，然后根据各程序点的抽象状态生成验证条件。

13、进一步地，所述分配状态函数定义为从堆对象到状态集合的映射，状态集合，其中strue表示堆对象由安全rust构造产生并且在当前程序点可确定为已分配，sfalse表示堆对象在安全模式下已释放，utrue表示堆对象由非安全分配操作产生并且在当前程序点可确定为已分配，ufalse表示堆对象在非安全模式下已释放，unknown表示根据当前控制流和指向关系无法确定该堆对象是否仍处于已分配状态。

14、进一步地，所述验证条件包括程序编码的验证条件和问题编码的验证条件；在生成验证条件时将待检测问题划分为非法解引用、非法释放和内存泄漏三类，并分别进行编码优化以减少三类问题对应的验证条件规模。

15、进一步地，所述对验证条件进行切片优化，包括：接收静态分析阶段输出的验证条件作为输入，并对程序编码的验证条件进行切片；若问题编码的验证条件为空，表示不存在需要smt求解器判断的检查项，则不再调用smt求解器；若问题编码的验证条件非空，则以问题编码的验证条件中出现的变量为初始相关集合，利用初始相关集合对程序编码的验证条件进行反向依赖分析，删除与问题编码的验证条件无关的公式，得到切片后的验证条件。

16、进一步地，所述根据求解结果生成验证报告，包括：如果smt求解器返回sat，表示发现程序错误，生成包含错误信息和反例路径的详细报告；如果smt求解器返回unsat，表示程序在给定边界内安全，生成安全确认报告；如果smt求解器返回unknown，生成未知状态报告。

17、一种rust程序的限界模型检测装置，其包括：

18、预处理模块，用于获取rust程序的mir中间表示，对mir中间表示进行预处理；

19、静态分析模块，用于对预处理后的mir中间表示进行所有权敏感静态分析，生成验证条件；

20、验证条件切片模块，用于对验证条件进行切片优化，得到精简的验证条件；

21、smt求解模块，用于利用smt求解器对精简的验证条件进行求解；

22、报告生成模块，用于根据求解结果生成验证报告。

23、本发明通过引入所有权敏感静态分析技术，基于mir进行限界模型检测，相比现有技术具有以下显著有益效果：

24、1）基于mir进行限界模型检测：避免了将rust程序翻译到其他中间表示的复杂过程，简化了验证流程，减少了转换过程中的信息损失和潜在错误。直接基于mir进行分析能够充分利用rust编译器的内部组件，提高了验证的准确性和效率。相比基于goto-c或llvm的验证技术，本发明的流程更加简洁，维护成本更低。

25、2）所有权敏感的静态分析：通过区分安全模式和非安全模式，并在静态分析过程中跟踪和维护所有权语义，所有权敏感分析能够提供更精确的程序状态抽象。相比传统静态分析，所有权敏感分析能够利用rust的所有权规则改进状态合并，减少了抽象状态的不确定性，提高了分析精度。这种改进使得验证过程更加精确，减少了误报和漏报的可能性。

26、3）基于所有权语义的验证条件简化：利用所有权语义对验证条件进行简化，能够显著减少需要求解的逻辑公式规模。根据所有权性质，某些验证条件可以直接判定为true或false，避免了不必要的smt求解。这种简化策略大幅提高了验证效率，特别是在处理大型程序时效果更为显著。通过减少冗余的验证条件，smt求解器的求解时间和内存占用都得到明显改善。