Page 133 - 《软件学报》2025年第8期

3556 软件学报 2025 年第 36 卷第 8 期

译过程提供严格的验证机制, 确保源码与目标码之间的可追溯性, 达到对编译系统形式化验证的要求. 该验证方法
不仅适用于当前的编译任务, 还为未来在其他语言环境中的应用奠定了基础.

Lustre* AST parse
(abstract syntax tree) Lustre*
static check
LustreSGen
Well-typed Lustre* AST LustreS
LustreRGen Toposort
TransTypecmp TransMainArgs
LustreR3 LustreR2 LustreR1
LustreFGen
OutstructGen ClassifyRetsVar
LustreF1 LustreF2 LustreE2
ResetfuncGen
ClassifyArgsVar SimpIEnv
LustreC LustreD LustreE2
CtempGen
CompCert
ClightGen Compiler
Ctemp Clight Assembly
图 2 L2C 编译器翻译过程

1 源语言特性

Lustre 语言是同步数据流语言的一个重要实例, 也是 SCADE 语言的主要组成部分. Lustre 语言遵循同步数据
流的基本要求: 满足同步假设、具有数据流特性、满足并行性. 除此之外, Lustre 遵循单时钟模型, 即系统中存在
一个基础时钟, 在每一个周期之内都恒定为真, 而其他的时钟都严格是基础时钟的子时钟, 只在基础时钟为真的时
刻才可能为真.
Lustre 语言是以赋值语句和表达式为核心的语言, 不存在显式的控制语句, 一个 Lustre 程序主要由以下几个
部分构成.
(1) Program (程序): 描述了程序的整体框架.
(2) Package & Model (包和模型): 描述了包和模型的定义以及导入, 提供了某种封装性的特性, 类似 C 语言中
的类.
(3) Node & Function (节点和函数): 节点和函数是 Lustre 中运行的基本单位, 其地位相当与其他语言当中的函
数. 基础的 Lustre 的节点和函数定义由一条节点定义语句、一系列变量声明语句和一系列赋值语句和断言语句组
成. Node 和 Function 的区别在于 Node 是有状态的, 依赖之前周期的值, 而 Function 是无状态的, 只依赖当前周期
的输入.
(4) 声明语句: Lustre 的声明语句主要集中出现在节点定义之后、节点中的赋值语句之前. 声明的变量主要有
bool、int、real 这 3 种基础类型和枚举类型、用户自定义的结构体.
(5) 赋值语句和表达式: 赋值语句由左值和右值组成, 左值为已经声明的变量, 右值为表达式. 表达式中包含各
种基本的运算符、Lustre 中特有的高阶运算符和时态算子. 此外, Lustre 也支持函数调用作为表达式的一部分.
下面是 Lustre 较为重要的特性, 包括时态算子、时钟算子等.
(1) 时态算子: 时态算子是一类依赖于先前周期信息的运算符, 包括 pre、→和 fby. 其中 pre 运算符是单目运
算符, 获取被操作流上一个周期的值; arrow 运算符是双目运算符, 在第 1 个周期内获取左侧流的值, 在此后的周期
获取右侧流的值; fby 运算符是双目运算符, 是 pre 和→的结合 (A fby B 等价于 A →pre(B)), 在第 1 个周期内获取
左侧流的值, 在此后的每个周期内获取右侧流在上一个周期的值.
(2) 时钟算子: 时钟算子是一类改变流的时钟的运算符, 包括 when 运算符、current 运算符和 merge 运算符.
前面提到的例子中, 几乎所有的流在每个周期内都有值, 这个周期就是基础时钟周期. 而 Lustre 允许通过 when 运