Journal of Frontiers of Computer Science and Technology ›› 2019, Vol. 13 ›› Issue (12): 2008-2014.DOI: 10.3778/j.issn.1673-9418.1901029

Previous Articles     Next Articles

KRust: Formal Executable Semantics of Rust

WANG Feng, ZHANG Jun   

  1. 1.Shanghai Institute of Microsystem and Information Technology, Chinese Academy of Sciences, Shanghai 200050, China
    2.School of Information Science & Technology, Shanghai Tech University, Shanghai 201210, China
    3.University of Chinese Academy of Sciences, Beijing 100049, China
  • Online:2019-12-01 Published:2019-12-10

KRust:Rust形式化可执行语义

王丰张俊   

  1. 1.中国科学院 上海微系统与信息技术研究所,上海 200050
    2.上海科技大学 信息科学与技术学院,上海 201210
    3.中国科学院大学,北京 100049

Abstract: Rust is a promising high-level system programming language, aiming at achieving memory safety while maintaining high performance. A formal semantics for Rust is the first step to prove memory safety and develop formal analysis tools for Rust. Since there is no formal semantics describing the exact behavior of Rust, this paper presents the first formal executable operational semantics for Rust, called KRust. KRust is implemented using K framework to make sure the semantics is both executable and applicable. Currently, KRust covers common syntax and semantics of Rust, including 3 core features of Rust: ownership, borrowing and lifetime. KRust has been validated by testing with 191 tests, including 157 tests from the official Rust test suite. The conformance test for semantics shows a bug of Rust compiler. In addition, KRust can be further exploited to construct formal analysis tools of Rust.

Key words: programming language, Rust, semantics, K framework

摘要: Rust是新兴的系统级编程语言,旨在提供内存安全的同时保证极高的性能。Rust形式化语义是用来证明其内存安全和开发Rust程序分析工具的基础。鉴于目前没有直接描述Rust的形式化语义,提出了针对Rust语言的形式化可执行语义KRust。为了确保语义的可执行性和应用性,使用了K框架进行语义的开发。KRust目前涵盖了Rust常见的语法和语义,包括了Rust的3个核心特性:所有权、借用和生命周期。KRust通过了191个测试样例,其中157个都是来自Rust官方的测试集。语义对比测试实验发现了Rust编译器的缺陷。此外,KRust的语义还可以被应用于开发Rust程序分析工具。

关键词: 编程语言, Rust, 语义, K框架