L2C

同步数据流语言(如 Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用。这些领域对相关开发工具本身的安全性有着相当高的要求。为尽力解决好“误编译”问题，近期人们借助 reliable-by-construction 辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功，如 CompCert C 编译器。L2C 是基于这种方法开发的可信编译器。它以扩展的 Lustre 语言为源语言，以 Clight(CompCert 中的 C 语言子集)为目标语言。L2C 是面向实际工业应用的同步数据流语言编译器。

Introduction

CompCert

CompCert 编译器是经过形式化验证的可信编译器的杰出代表。该编译器将 C 的一个重要子集 Clight 翻译为 PowerPC 汇编代码(后来也支持 IA32和ARM后端)，并实现了对翻译过程本身的验证，使其可直接应用于范围广泛的嵌入式应用开发。
L2C

L2C 是采用类似于 CompCert 编译器的方法开发的可信编译器。它以扩展的 Lustre 语言作为源语言，以CompCert 的 Clight 作为目标语言，并且从验证方面也与 CompCert 完全对接。L2C 是采用对翻译过程本身进行验证的可信编译器中，面向实际工业应用的同步数据流语言编译器。

Process

为了满足国内某安全攸关领域的需求，L2C 编译器的开发始于 2010 年 9 月，其目标是设计实现一个经过形式化验证的可信编译器，其源语言是面向领域的同步数据流语言 Lustre*(Lustre 语言的一个变种)，目标语言是 C，最终可用作相关领域数字化仪控系统的安全级代码生成器。

L2C 编译器的发展进程可归为 3 个里程碑：

一个是面向 Lustre*的一个核心子集，设计实现了 L2C 编译器的一个原型系统，于 2013 年 6 月完成验收。
另一个里程碑是已实现除嵌套时钟外 Lustre*全部特性的一个单时钟L2C 编译器版本，完全能够满足国内该安全攸关领域目前的实际应用需求，并于 2015 年 4 月完成严格的企业级验收，这些工作的相关技术和代码已在实际应用中发挥作用.。
在上述第 2 个里程碑之后，项目组对 L2C 编译器的设计框架进行了较大程度的优化调整，目标是拓展应用领域以及开源系统的建设。目前，L2C 编译器进入了第 3 个里程碑的发展阶段，其目标是在目前面向企业的版本(不开源)基础上裁减并适当改造，形成了覆盖 Lustre V6全部特性的可开源版本。目前，这一 L2C 编译器的单时钟版本(L2C-MC)已经开放源码https://github.com/l2ctsinghua/l2c/releases/tag/version-0.8，支持嵌套时钟的版本处于测试与完善的周期，其源码不久也将开放。

Lustre V6：学术Lustre编译器的最后一个版本，具有ada-like的包机制、结构化数据类型（枚举、结构）、数组迭代器和静态递归。在经典的Lustre语言特性上扩展了更为丰富的语言特性，如三元的fby算子等等。

Lustre* ：Lustre*覆盖了Lustre V6的全部特性，并且根据实际应用的需求在此基础上有许多扩展，特别是在高阶运算方面比 Lustre V6更加丰富。

Example

一个 Lustre*程序(program)由多个节点(node)组成，节点中包含输入参数(parameters)、输出参数(returns)和函数体(body)，其中函数体又由局部变量(local variables)和等式(或语句)序列组成，结构清晰。

翻译至Clight:

翻译至Clight:

Framework

下图刻画了最新的L2C编译器架构，是目前的开源版L2C[31]所采用的架构。以前的L2C版本(主要有原型版与企业版)的架构与此有所不同。

参考文献

[1]尚书，甘元科，石刚，王生原，董渊.可信编译器L2C的核心翻译步骤及其设计与实现[J].软件学报，2017，28(05):1233-1246.

[2]康跃馨, 甘元科, 王生原. 同步数据流语言可信编译器Vélus与L2C的比较. 软件学报, 2019, 30(7): 2003-2017.http://www.jos.org.cn/1000-9825/5755.htm

L2C Project

附录

来自：L2C单时钟版本

Version 0.8

Introduction

The goal of L2C project is to build a compiler to implement formally certified tranlation from a Lustre-like synchronous data-flow language which totally covers Lustre V6 to Clight.
This open source version of L2C has completed the certified translation from a mono-clocked Lustre-like language to Clight. Next we will open the nested-clocked version.

1
2

L2C项目的目标是构建一个编译器，以实现从Lustre-like同步数据流语言（完全涵盖Lustre V6到Clight）的正式认证转换。
L2C的开源版本已经完成了从单时钟Lustre-like语言到Clight的认证翻译。接下来，我们将开源嵌套时钟版本。

Nouns Explaination
Lustre
Lustre is a formally defined, declarative, and synchronous dataflow programming language, for programming reactive systems. see http://en.wikipedia.org/wiki/Lustre_(programming_language)

Lustre V6
Lustre V6 is a stable and popular version of Lustre programming language. see http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/
1
Lustre V6 是 Lustre编程语言一个稳定和流行的版本。
Clight
Clight is a large subset of C programming language used in CompCert which is an existing formally certified compiler from Clight to assembly. see http://compcert.inria.fr
1
Clight是CompCert中使用的C语言的一个很大的子集，CompCert是从Clight到汇编的现有形式化验证编译器。

Framework

The framework of L2C is shown below. This open source version complete the formally certified translation from Well-typed Lustre* AST to Clight as the red box covers.

Get Started

Environment:

The Coq Proof Assistant, version 8.4pl3 (July 2015)
The Objective Caml compiler, version 4.02.1
Pproofgeneral 4.2

（用来证明数学逻辑的正确性）

Installation:

make
make install (option)
– install l2c to ~/bin

Test

make test
– compile ast files into c files

Uninstallation

make uninstall
– remove ~/bin

How To Use

USAGE

1	l2c [options] <source.ast>

options

   **-save-temp**:        Save temporary intermediate files

-ctemp: Output ctemp source

   **-target_dir `<dir>`**:    Set the directory of target files to `<dir>`

   **-o `<file>`**:        Indicate the output file name

   **-version**:        Print version information

   **-help**:            Print this usage message

Website

More Details, see http://soft.cs.tsinghua.edu.cn:8000/