Development of a semantics compiler for C
Matthias Daum · 2003
theory of class X Model theory of class X Figure 5.1: Example for a circular dependency if all global functions live in one theory 5.3 Structural overview This section outlines general design and structure of the translation component. Obviously, some interfaces and design decisions were self-suggesting or yet already determined by the used framework. Furthermore, many design issues arose late during the implementation process due to the semantics representation was developed together with the compiler’s implementation. This certainly sometimes influenced specific decisions. However, all decisions were made based foremost on the general design criteria discussed in chapter 3. 5.3.1 Processing statements and expressions Like the annotator, the translator has to examine parse trees in various situations. Evidently, both should share the same mechanisms for similar tasks. Therefore, the translator re-uses the Paranoid_visitor class template from the annotator. The return type of the visit method is the translation’s result. Usually, this will simply be a theorem prover’s formula. However, under certain circumstances it might be useful to return some additional informa- tion. For instance, the expression translator could carry around a type annotation. This is not done in the current implementation, but was kept in mind for flexibility and extensibility. Since statements and expressions might have quite different needs on additional information, two distinct visitors were implemented to allow different return types. Sc_stmt_translator and Sc_expr_translator translate respectively statements and expressions into their semantics representation. One-pass translation The parse tree structures are passed exactly once. This is just done for simplicity. A one-pass system is a clean and simple approach with a long tradition. C and C++ were actually designed to allow a single-pass translation. All entities (such as types, functions and variables) must be declared before they can be used; and declarations always provide just enough information to encode the use of the declared entity. 36 5 Translating C++ source code into PVS Nonetheless, the compiler—regarded as a whole—already passes the code multiple times. At first, it is completely parsed by OpenC++; subsequently, the parse trees are processed by the annotator, and finally, the symbol table is translated. If needed, even more passes could be easily introduced. This might become necessary if possibly recursive functions will be translated (see section 4.6.1).