6.Related work Colby et al.implemented a certifying compiler called Spe- cial J [3]for a large subset of Java.It compiled Java byte Verifying compiler [8]is a research topic proposed in re- code into target code for Intel IA32 architecture.The ma- cent years.It uses mathematical and logical reasoning to jor advance of Special J over Touchstone was the scope of check the correctness of the program that it compiles be- the source language compiled,which in turn necessitated fore the program executes.The criterion of correctness is the handling of non-trivial run-time mechanisms such as specified by types,assertions,and other redundant annota- object representation,dynamic method dispatch and excep- tions associated with the program.Now it can be classified tion handling.Moreover,Special J was freely able to apply into two research directions on this topic.One is to prove many standard local and global optimizations. the correctness of the compiler formally,that is,the com- Our design has the following significant differences from piler carries a formal proof which confirms the correctness Touchstone and Special J: of the generated objective code.Such a compiler is called 1.PointerC has more pointer types and operations,and a certified compiler.The other is to prove the correctness also provides dynamic storage allocation and deallo- of the compiled code formally,i.e.,the code carries a for- cation.These features make it suitable for writing mal proof to guarantee its correctness,safety or some other system-level programs.Both Touchstone and Special J properties and the proof can be checked by a code consumer have no dynamic storage deallocation. independently.This kind of compiler is called a certifying compiler.Obviously,this paper presents the design of parts 2.We use some new techniques to handle the features of of a certifying compiler. the language equipped with both a type system and a In the research area of certified compiler,Moore was logic system.For example,our VC generator can per- one of the first to mechanically verify semantic preserva- form both forward and backward VC generations,and tion for a compiler [14],although for a custom language the theorem prover embedded in the compiler and the and a custom processor that were not commonly used.Af- Coq proof assistant can be used to prove VCs for dif- ter that,more compilers were verified,including a compiler ferent types of data respectively. for a subset of Common Lisp,a byte-code compiler for a 3.To certify the proof-carrying assembly code,we adopt subset of Java,and a compiler for a tiny subset of C.The an approach that applies the method of Hoare logic di- most recent typical work is the certification of a lightly- rectly to the operational semantics of Intel x86 ISA. optimizing back end that generates PowerPC assembly code We use machine state as the parameter of assertions,so from a simple imperative intermediate language called Cmi- as to describe program properties which may change nor [10]by Leroy.A front end translating a subset of C to with the machine state.These properties are usu- Cminor is under development and certification.One of the ally difficult to be expressed in common type systems. novel features of his work is to emphasize the certification Touchstone and Special J mainly focus on type proper- of a complete compilation chain instead of parts of a com- ties of programs,and rarely concern complicated pro- piler.Another novelty is that most of the compiler is written gram properties directly in the Coq specification language,in a purely func- tional style. 4.Due to the simplicity of the source language,loop in- Generally,it is much easier to prove the correctness of variants which only concern types can be generated au- a calculation result than to prove the correctness of the cal- tomatically in Touchstone and Special J.In our certify- culation itself,so that certifying compiler has more possi- ing compiler,loop invariants may contain more infor- bility to come into use than certified compiler.Necula first mation than types,and it should be provided by pro- proposed the concept of Proof-Carrying Code,and imple- grammers explicitly. mented a certifying compiler called Touchstone [17].This compiler was composed of a traditional optimizing com- 7.Conclusion piler for a type-safe subset of C and a certifier that automati- cally produced a proof of type safety and memory safety for This paper presents the design and implementation of a each assembly program.A proof checker could be used to certifying compiler for PointerC(a programming language check the generated proofs automatically.Since the source equipped with both a type system and a logic system).Al- programs compiled by Touchstone were written in a very though the implemented certifying compiler prototype only small safe subset of C,their type safety and memory safety enforces the primary safety policies such as type safety and were easy to be checked.The main limitations of the source memory safety,the whole framework can fit in the situation language in Touchstone were in the aspects of pointer types where user-defined safety policies are allowed.This paper and memory deallocation,which made the language only only concentrates on the main work of the certifying com- used in writing programs with simple data structures.Later, piler and skips the translation of assertions,VCs and proofs6. Related work Verifying compiler [8] is a research topic proposed in re￾cent years. It uses mathematical and logical reasoning to check the correctness of the program that it compiles be￾fore the program executes. The criterion of correctness is specified by types, assertions, and other redundant annota￾tions associated with the program. Now it can be classified into two research directions on this topic. One is to prove the correctness of the compiler formally, that is, the com￾piler carries a formal proof which confirms the correctness of the generated objective code. Such a compiler is called a certified compiler. The other is to prove the correctness of the compiled code formally, i.e., the code carries a for￾mal proof to guarantee its correctness, safety or some other properties and the proof can be checked by a code consumer independently. This kind of compiler is called a certifying compiler. Obviously, this paper presents the design of parts of a certifying compiler. In the research area of certified compiler, Moore was one of the first to mechanically verify semantic preserva￾tion for a compiler [14], although for a custom language and a custom processor that were not commonly used. Af￾ter that, more compilers were verified, including a compiler for a subset of Common Lisp, a byte-code compiler for a subset of Java, and a compiler for a tiny subset of C. The most recent typical work is the certification of a lightly￾optimizing back end that generates PowerPC assembly code from a simple imperative intermediate language called Cmi￾nor [10] by Leroy. A front end translating a subset of C to Cminor is under development and certification. One of the novel features of his work is to emphasize the certification of a complete compilation chain instead of parts of a com￾piler. Another novelty is that most of the compiler is written directly in the Coq specification language, in a purely func￾tional style. Generally, it is much easier to prove the correctness of a calculation result than to prove the correctness of the cal￾culation itself, so that certifying compiler has more possi￾bility to come into use than certified compiler. Necula first proposed the concept of Proof-Carrying Code, and imple￾mented a certifying compiler called Touchstone [17]. This compiler was composed of a traditional optimizing com￾piler for a type-safe subset of C and a certifier that automati￾cally produced a proof of type safety and memory safety for each assembly program. A proof checker could be used to check the generated proofs automatically. Since the source programs compiled by Touchstone were written in a very small safe subset of C, their type safety and memory safety were easy to be checked. The main limitations of the source language in Touchstone were in the aspects of pointer types and memory deallocation, which made the language only used in writing programs with simple data structures. Later, Colby et al. implemented a certifying compiler called Spe￾cial J [3] for a large subset of Java. It compiled Java byte code into target code for Intel IA32 architecture. The ma￾jor advance of Special J over Touchstone was the scope of the source language compiled, which in turn necessitated the handling of non-trivial run-time mechanisms such as object representation, dynamic method dispatch and excep￾tion handling. Moreover, Special J was freely able to apply many standard local and global optimizations. Our design has the following significant differences from Touchstone and Special J: 1. PointerC has more pointer types and operations, and also provides dynamic storage allocation and deallo￾cation. These features make it suitable for writing system-level programs. Both Touchstone and Special J have no dynamic storage deallocation. 2. We use some new techniques to handle the features of the language equipped with both a type system and a logic system. For example, our VC generator can per￾form both forward and backward VC generations, and the theorem prover embedded in the compiler and the Coq proof assistant can be used to prove VCs for dif￾ferent types of data respectively. 3. To certify the proof-carrying assembly code, we adopt an approach that applies the method of Hoare logic di￾rectly to the operational semantics of Intel x86 ISA. We use machine state as the parameter of assertions, so as to describe program properties which may change with the machine state. These properties are usu￾ally difficult to be expressed in common type systems. Touchstone and Special J mainly focus on type proper￾ties of programs, and rarely concern complicated pro￾gram properties. 4. Due to the simplicity of the source language, loop in￾variants which only concern types can be generated au￾tomatically in Touchstone and Special J. In our certify￾ing compiler, loop invariants may contain more infor￾mation than types, and it should be provided by pro￾grammers explicitly. 7. Conclusion This paper presents the design and implementation of a certifying compiler for PointerC (a programming language equipped with both a type system and a logic system). Al￾though the implemented certifying compiler prototype only enforces the primary safety policies such as type safety and memory safety, the whole framework can fit in the situation where user-defined safety policies are allowed. This paper only concentrates on the main work of the certifying com￾piler and skips the translation of assertions, VCs and proofs