可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言（如Lustre）近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好”误编译”问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证取得了很大的成功,如CompCert C编译器.L2C是基于这种方法开发的可信编译器,它以扩展的Lustre语言为源语言,以Clight （CompCert中的C语言子集）为目标语言.就我们所知,L2C是同类工作中唯一面向实际工业应用的同步数据流语言编译器.本文重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.     

同步数据流语言高阶运算消去的可信翻译

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.     

同步数据流语言可信编译器的构造

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.     

同步数据流程序的可信排序

Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效提高编译器的安全性。因为Lustre程序是并发执行的,需要对其进行因果分析和串行化。利用Coq工具,形式化定义拓扑排序的性质和相应层次的Lustre的语义;对Lustre程序进行因果分析和排序;证明排序后的程序满足拓扑排序的性质;证明任意两个满足拓扑排序性质的程序语义执行等价。从而实现了一种针对Lustre程序的可信排序过程。     

同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.     

同步语言Lustre的编译前端的设计与实现

同步语言Lustre所描述的反应系统通常应用在航空航天、国防建设等领域,对系统的正确性和安全性都要求很高。如果系统在运行时出现了正确性问题,很可能会导致系统崩溃,产生非常严重的后果。系统中的任何一个词法错误或者语法错误都应该受到重视,而且应该被及时纠正。因此,对Lustre语言进行正确的编译是十分重要的。传统的Lustre语言的编译器都采用OCaml语言描述,无法保证所有人员都能够很容易地理解和使用,而且,需要耗费开发人员大量的时间和精力。基于上述问题,提出了一种新型的Lustre语言编译器。新型的Lustre语言编译器前端主要采用C++语言进行描述,并对生成的抽象语法树的结构进行重新定义,简化了编译的过程。该编译前端会对一个经典的Lustre语言模型进行检测,通过对检测的结果进行分析,验证了该编译前端的可行性。     

一种包解析器硬件配置描述语言及其编译结构

设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解,从软硬件协同角度出发,最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络(SDN)、可编程数据平面的重要一环,因此,实现P3C的可信编译结构将对SDN的安全性具有重大意义.期待P3C项目的开展能够促进网络与形式化领域相关工作的进一步研究.     

一个C语言安全子集的可信编译器

以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器.然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估.之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器.最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率.     

试论C语言编译器的设计与实现

编译程序被认为是现代计算机系统的基本构成,本文重点分析了C语言编译器设计与实现的相关问题,文章先阐述了C语言编译器总体设计的相关内容,包括词法、语义分析等;再介绍了C语言编译器的实现路径,希望能对相关人员工作有所帮助.     

基于程序转化的SCADE模型检测

SCADE同步语言是一种常用的嵌入式系统程序设计语言.在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统.SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语言结构来精简代码.目前,相比Lustre语言,SCADE程序模型检测的学术研究相对落后.为此,文中提出了一种对SCADE程序进行模型检测的方法并实现了一款SCADE模型检测工具,该方法的核心思想是基于程序转化,即把SCADE程序经过词法分析、语法分析、抽象语法树生成与化简等操作最终转化为等价的Lustre程序,然后用JKind与SMT求解器完成模型检测.此外,通过理论推导和大量实验证明了工具的模型检测的正确性.实验结果表明,功能相同的两个SCADE和Lustre测试用例模型的检测结果相同,但SCADE程序的模型检测效率相对较低.     

一种用于Java虚拟机的类型化低级语言

为了能够减小运算系统的需信任计算基础、描述较小粒度的安全策略，目前的研究倾向于从程序设计语言和编译器入手来提高软件的安全性．基于以上研究背景设计了一种类型化的低级语言TLL,TLL是一种为Java虚拟机即时编译器设计的类型安全中间语言，以构造一个具有更小需信任计算基础的Java虚拟机系统为目的．TLL的类型系统基于多态的类型化λ演算，它具有丰富的表现力且能够编码各种高级语言的抽象．基于TLL的一个虚拟机原型系统已经实现，它可以作为实现一个高安全且面向多种源语言的运行时系统的起点．     

An optimizing compiler for the icon programming language

Compiling code for the Icon programming language presents several challenges, particularly in dealing with types and goal-directed expression evaluation. In order to produce optimized code, it is necessary for the compiler to know much more about operations than is necessary for the compilation of most programming languages. This paper describes the organization of the Icon compiler and the way it acquires and maintains information about operations. The Icon compiler generates C code, which makes it portable to a wide variety of platforms and also allows the use of existing C compilers for performing routine optimizations on the final code. A specially designed implementation language, which is a superset of C, is used for writing Icon's run-time system. This language allows the inclusion of information about the abstract semantics of Icon operations and their type-checking and conversion requirements. A translator converts code written in the run-time language to C code to provide an object library for linking with the code produced by the Icon compiler. The translation process also automatically produces a database that contains the information the Icon compiler needs to generate and optimize code. This approach allows easy extension of Icon's computational repertoire, alternate computational extensions, and cross compilation.     

一种改进数据流图的子字并行程序表示方法

论文致力于对图像处理算法的串行C程序进行子字并行分析,并重定向到带有多媒体扩展的通用处理器和多媒体专用嵌入式微处理器。图像处理算法的特点决定其是内在可并行的,这种并行粒度介于数据并行(DLP)和指令级并行(ILP)之间,称之为子字并行。但是,当前的编译技术很难充分挖掘和定位程序基本块内的子字并行,对此设计了一种基于流图程序表示的编译方法,能够从串行程序中显式地定位子字并行。扩展了编译器的功能,增加了特定的模式库,基于模式识别的控制流和数据流分析后,产生特定的子字并行流图(SWFG,Sub-WordFlowGraph),并将该图作为中间表示,提供给子字并行指令选择,进而实现有效的子字并行代码产生。     

Visual language implementation through standard compiler–compiler techniques

We present a technique for implementing visual language compilers through standard compiler generation platforms. The technique exploits eXtended Positional Grammars (XPGs, for short) for modeling the visual languages in a natural way, and uses a set of mapping rules to translate an XPG specification into a translation schema. This lets us generate visual language parsers through standard compiler–compiler techniques and tools like YACC. The generated parser accepts exactly the same set of visual sentences derivable through the application of XPG productions. The technique represents an important achievement, since it enables us to perform visual language compiler construction through standard compiler–compilers rather than specific compiler generation tools. This makes our approach particularly appealing, since compiler–compilers are widely used and rely on a well-founded theory. Moreover, the approach provides the basis for the unification of traditional textual language technologies and visual language compiler technologies.     

UCB策略在Prolog中的应用

Prolog(Programming in Logic)程序语言是一种逻辑程序设计语言.它是在逻辑学理论基础上建立起来的并广泛应用在人工智能研究中.这几十年已经出现了各具特色的Prolog编译器,而且各种编译器也都很成功.虽然在现阶段已经出现了各种版本Prolog编译器,但是Prolog编译器的发展空间还是很大.本文先通过现代Prolog编译器的不足,介绍了新Prolog编译器的特点,然后简单叙述了Prolog编译器词法分析和语法分析的过程,最后介绍了UCB策略.     

The structure of the MARY/2 compiler

The MARY12 language implemented at Penobscot Research Center contains language differences from previous MARY implementations. These differences significantly increase the difficulty of implementing a compiler. Similar constructs have appeared in recent language proposals such as those for ADA. The methods of the MARY/2 compiler should be useful in compilers for these and other future languages. This paper discusses the language constructs which are the source of the difficulty; the implementation methods actually used; possible trade used; and the character of the programs which these constructs facilitate.