一个面向C和Fortran数值程序的静态分析工具

程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上,本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题。     

面向RISC-V的汇编程序语义等价性自动化测试系统

本文设计并实现了一套面向RISC-V的汇编程序语义等价性自动化测试系统.在面向RISC-V开发软件时,尤其是基于扩展指令(例如向量指令)编写高效的程序时,很难避免以手写汇编的方式编写代码.例如,为标准的C函数库编写相应的向量版函数.与编译器自动生成的代码不同,手写的汇编代码虽然可以最大限度地提高程序的效率,但因绕过了编译时对程序的约束(如类型检查、寄存器分配等)而对开发者提出了更高的要求.能否对新版本与标准版本的汇编程序进行快速地、自动化的语义等价性测试,将大大影响代码的正确性和软件开发和调试的效率.已有面向RISC-V的测试框架缺乏对语义等价性测试的支持,也未考虑程序执行带来的副作用.本研究基于模拟器的动态测试环境,设计并实现了一套面向RISC-V的汇编程序语义等价性自动化测试系统.系统通过跟踪机器状态,捕获程序执行的副作用,并结合用户定义的测试目标生成测试报告.实验表明,本系统相比已有的测试系统,能够有效地对RISC-V汇编程序的语义等价性进行测试.     

Experience with Abstraction-carrying Code

Abstraction-carrying Code (ACC) certifies a general temporal property for a mobile program using an abstract interpretation of the mobile program. A client receiving the code and the certificate will first validate the abstraction and then run a model checker to verify the temporal property.In this paper, we report our experience in designing the ACC Evaluation Prototype Toolkit (ACCEPT) and the application of ACCEPT to simple concurrent programs and Linux device drivers. The toolkit is distinguished by an abstraction preserving compilation scheme that generates a Boolean program for an intermediate program compiled from the source program. Some common compiler optimizations are still possible. We report several applications of ACCEPT, including the reachability properties of industrial strength C programs. Preliminary results show that the size of a typical certificate is significantly smaller than the size of the intermediate program. Compared with traditional proof-based certification method, using ACC verification a client spends more time to verify the desired property. Our experience shows this penalty is often tolerable in practice.     

Certifying Compilation and Run-Time Code Generation

A certifying compiler takes a source language program and produces object code, as well as a certificate that can be used to verify that the object code satisfies desirable properties, such as type safety and memory safety. Certifying compilation helps to increase both compiler robustness and program safety. Compiler robustness is improved since some compiler errors can be caught by checking the object code against the certificate immediately after compilation. Program safety is improved because the object code and certificate alone are sufficient to establish safety: even if the object code and certificate are produced on an unknown machine by an unknown compiler and sent over an untrusted network, safe execution is guaranteed as long as the code and certificate pass the verifier.Existing work in certifying compilation has addressed statically generated code. In this paper, we extend this to code generated at run time. Our goal is to combine certifying compilation with run-time code generation to produce programs that are both fast and verifiably safe. To achieve this goal, we present two new languages with explicit run-time code generation constructs: Cyclone, a type safe dialect of C, and TAL/T, a type safe assembly language. We have designed and implemented a system that translates a safe C program into Cyclone, which is then compiled to TAL/T, and finally assembled into executable object code. This paper focuses on our overall approach and the front end of our system; details about TAL/T will appear in a subsequent paper.     

Dynamic Event Generation for Runtime Checking using the JDI

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to the compilation or by modifying the target code, e.g. Java byte code, before running the program.The jassda [4,3] framework and tool enable runtime checking of Java programs against a CSP-like specification. For generating events it uses the Java Debug Interface (JDI) and thus no modifications to the code are necessary. Another advantage is that events are generated on demand, i.e. dynamically at runtime it is determined which events to generate for the current debug run without modifying the program itself. This paper shows how this event generation is done by the jassda framework.     

Certifying assembly programs with trails

In this paper, we introduce a new way of certifying assembly programs. Unlike previous program logics, we extract the control-flow information from the code and generate an intermediate trail between the specification and the real code. Trails are auxiliary specifications and treated as modules in the certification process. We define a simple modular program logic called trail-based certified assembly programming (TCAP) to certify and link different parts of a program using the corresponding trails. Because the control flow information in trails is explicit, the rules are easier to design. We show that our logic is powerful enough to prove partial correctness of assembly programs with features including stack-based abstractions and self-modifying code.We also provide a semantics for TCAP and prove that the logic is sound with respect to the semantics.     

Algorithmic program synthesis: introduction

Program synthesis is a process of producing an executable program from a specification. Algorithmic synthesis produces the program automatically, without an intervention from an expert. While classical compilation falls under the definition of algorithmic program synthesis, with the source program being the specification, the synthesis literature is typically concerned with producing programs that cannot be (easily) obtained with the deterministic transformations of a compiler. To this end, synthesis algorithms often perform a search, either in a space of candidate programs or in a space of transformations that might be composed to transform the specification into a desired program. In this introduction to the special journal issue, we survey the history of algorithmic program synthesis and introduce the contributed articles. We divide the field into reactive synthesis, which is concerned with automata-theoretic techniques for controllers that handle an infinite stream of requests, and functional synthesis, which produces programs consuming finite input. Contributed articles are divided analogously. We also provide pointers to synthesis work outside these categories and list many applications of synthesis.     

Toward an automatic parallelization of sparse matrix computations

In this paper, we propose a generic method of automatic parallelization for sparse matrix computation. This method is based on both a refinement of the data-dependence test proposed by Bernstein and an inspector–executor scheme which is specialized to each input program of the compiler. This analysis mixes compilation process and run-time process.The sparsity of underlying data-structure determines a specific parallelism which increases the degree of parallelism of an algorithm. Such a source of parallelism had already been applied to many numerical algorithms such as the usual Cholesky factorization or LU-decomposition algorithms considered as the gold standards of parallelization based on sparsity. The standard automatic parallelization method cannot tackle such source of parallelism because it is based on the value of cells arrays and not merely on the memory addressing function.Addressing the automatization of this parallelism requires to develop a mixed compile-time and runtime approach integrated in a inspector–executor process. The compilation step provides a dedicated inspector devoted to the analyzed program. The inspector computes the dependence graph at runtime which allows a dynamic parallelization of the execution.As expressed just before, the generic scheme developed in this paper follows the design principles which have been applied, but at each time in an ad hoc way, to many sparse parallelization of numerical algorithms such as Cholesky algorithm. As far as we know, no general formal framework has been proposed to automate such a method of sparse parallelization. In this paper, we propose a generic framework of sparse parallelization (i.e. numerical program independent) which can be applied to any numerical programs satisfying the usual syntactic constraints of parallelization.     

基于符号约束的PLC程序正确性验证

符号约束描述了程序中的变量关系,被广泛运用于模型检测、符号执行等程序的静态分析方法中。将符号约束应用于可编程逻辑控制器(PLC)程序的正确性验证,能够发现程序中的逻辑错误。人工计算符号约束不仅冗杂枯燥,而且错误率高。针对语句表形式的PLC程序,提出一种基于符号约束的正确性验证方法,通过分析PLC源代码的控制流及数据流,构造程序的控制流图并将其转换为静态单赋值形式的三地址码,最后使用迭代计算的方法求出每个变量的符号约束。