Nicolas Ayache

Roberto M Amadio

Yann Régis-Gianas

= Loadi R

Certifying and reasoning on cost annotations in C programs

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The formal description and certification of software components is reaching a certain level of maturity with impressing case studies ranging from compilers to kernels of operating systems. A well-documented example is the proof of functional correctness of a moderately optimizing compiler from a large subset of the C language to a typical assembly language of the kind used in embedded systems [START_REF] Leroy | Formal verification of a realistic compiler[END_REF].

In the framework of the Certified Complexity (CerCo) project1 [START_REF]Certified complexity (Project description)[END_REF], we aim to refine this line of work by focusing on the issue of the execution cost of the compiled code. Specifically, we aim to build a formally verified C compiler that given a source program produces automatically a functionally equivalent object code plus an annotation of the source code which is a sound and precise description of the execution cost of the object code.

We target in particular the kind of C programs produced for embedded applications; these programs are eventually compiled to binaries executable on specific processors. The current state of the art in commercial products such as Scade2 [START_REF] Fornari | Understanding how SCADE suite KCG generates safe C code[END_REF] is that the reaction time of the program is estimated by means of abstract interpretation methods (such as those developed by AbsInt3 [START_REF] Ferdinand | Combining a high-level design tool for safety-critical systems with a tool for WCET analysis of executables[END_REF]) that operate on the binaries. These methods rely on a specific knowledge of the architecture of the processor and may require explicit (and uncertified) annotations of the binaries to determine the number of times a loop is iterated (see, e.g., [START_REF] Wilhelm | The worst-case execution-time problem -overview of methods and survey of tools[END_REF] for a survey of the state of the art).

In this context, our aim is to produce a mechanically verified compiler which can lift in a provably correct way the pieces of information on the execution cost of the binary code to cost annotations on the source C code. Then the produced cost annotations are manipulated with the Frama -C4 [START_REF] Correnson | Frama-C user manual[END_REF] automatic tool to infer synthetic cost annotations. We stress that the practical relevance of the proposed approach depends on the possibility of obtaining accurate information on the execution cost of relatively short sequences of binary instructions. This seems beyond the scope of current Worst-Case Execution Time (WCET) tools such as AbsInt or Chronos5 which do not support a compositional analysis of WCET. For this reason, we focus on processors with a simple architecture for which manufacturers can provide accurate information on the execution cost of the binary instructions. In particular, our experiments are based on the 8051 [START_REF]MCS 51 Microcontroller Family User's Manual[END_REF] 6 . This is a widely popular 8-bits processor developed by Intel for use in embedded systems with no cache and no pipeline. An important characteristic of the processor is that its cost model is 'additive': the cost of a sequence of instructions is exactly the sum of the costs of each instruction.

The rest of the paper is organized as follows. Section 2 describes the labelling approach and its formal application to a toy compiler. Appendix A gives standard definitions for the toy compiler and sketches the proofs. A formal and browsable Coq development composed of 1 Kloc of specifications and 3.5 Kloc of proofs is available at http://www.pps.univ-paris-diderot.fr/cerco. Section 3 reports our experience in implementing and testing the labelling approach for a compiler from C to 8051 binaries. The CerCo compiler is composed of 30 Kloc of ocaml code; it can be both downloaded and tested as a web application at the URL above. More details are available in Appendix B. Section 4 introduces the automatic Cost tool that starting from the cost annotations produces certified synthetic cost bounds. This is a Frama -C plug-in composed of 5 Kloc of ocaml code also available at the URL above.

A "labelling" method for cost annotating compilation

In this section, we explain in general terms the so-called "labelling" method to turn a compiler into a cost annotating compiler while minimizing the impact of this extension on the proof of the semantic preservation. Then to make our purpose technically precise, we apply the method to a toy compiler.

Overview

As a first step, we need a clear and flexible picture of: (i) the meaning of cost annotations, (ii) the method to provide them being sound and precise, and (iii) the way such proofs can be composed. The execution cost of the source programs we are interested in depends on their control structure. Typically, the source programs are composed of mutually recursive procedures and loops and their execution cost depends, up to some multiplicative constant, on the number of times procedure calls and loop iterations are performed. Producing a cost annotation of a source program amounts to:

enrich the program with a collection of global cost variables to measure resource consumption (time, stack size, heap size,. . .) inject suitable code at some critical points (procedures, loops,. . .) to keep track of the execution cost.

Thus, producing a cost-annotation of a source program P amounts to build an annotated program An(P ) which behaves as P while self-monitoring its execution cost. In particular, if we do not observe the cost variables then we expect the annotated program An(P ) to be functionally equivalent to P . Notice that in the proposed approach an annotated program is a program in the source language. Therefore, the meaning of the cost annotations is automatically defined by the semantics of the source language and tools developed to reason on the source programs can be directly applied to the annotated programs too. Finally, notice that the annotated program An(P ) is only meant to reason on the execution cost of the unannotated program P . Therefore, An(P ) will never be compiled, nor executed. Hence, the influence of cost annotations on the WCET is off-topic.

Soundness and precision of cost annotations Suppose we have a functionally correct compiler C that associates with a program P in the source language a program C(P ) in the object language. Further suppose we have some obvious way of defining the execution cost of an object code. For instance, we have a good estimate of the number of cycles needed for the execution of each instruction of the object code. Now, the annotation of the source program An(P ) is sound if its prediction of the execution cost is an upper bound for the 'real' execution cost. Moreover, we say that the annotation is precise with respect to the cost model if the difference between the predicted and real execution costs is bounded by a constant which only depends on the program.

Compositionality In order to master the complexity of the compilation process (and its verification), the compilation function C must be regarded as the result of the composition of a certain number of program transformations

C = C k •• • ••C 1 .
When building a system of cost annotations on top of an existing compiler, a certain number of problems arise. First, the estimated cost of executing a piece of source code is determined only at the end of the compilation process. Thus, while we are used to define the compilation functions C i in increasing order, the annotation function An is the result of a progressive abstraction from the object to the source code. Second, we must be able to foresee in the source language the looping and branching points of the object code. Missing a loop may lead to unsound cost annotations while missing a branching point may lead to rough cost predictions. This means that we must have a rather good idea of the way the source code will eventually be compiled to object code. Third, the definition of the annotation of the source code depends heavily on contextual information. For instance, the cost of the compiled code associated with a simple expression such as x + 1 will depend on the place in the memory hierarchy where the variable x is allocated. A previous experience described in [START_REF] Amadio | Compiler Design and Intermediate Languages[END_REF] suggests that the process of pushing 'hidden parameters' in the definitions of cost annotations and of manipulating directly numerical cost is error prone and produces complex proofs. For this reason, we advocate next a 'labelling approach' where costs are handled at an abstract level and numerical values are produced at the very end of the construction.

The labelling approach, formally

The 'labelling' approach to the problem of building cost annotations is summarized in the following diagram.

L1 L 1, I o o er 1 Ù Ù C 1 G G L 2, er 2 . . . C k G G L k+1, er k+1 L1 L s s C 1 G G L2 . . . C k G G L k+1 er i+1 • Ci = Ci • er i er 1 • L = id L 1 An = I • L
For each language L i considered in the compilation process, we define an extended labelled language L i, and an extended operational semantics. The labels are used to mark certain points of the control. The semantics makes sure that whenever we cross a labelled control point a labelled and observable transition is produced.

For each labelled language there is an obvious function er i erasing all labels and producing a program in the corresponding unlabelled language. The compilation functions C i are extended from the unlabelled to the labelled language so that they enjoy commutation with the erasure functions. Moreover, we lift the soundness properties of the compilation functions from the unlabelled to the labelled languages and transition systems.

A labelling L of the source language L 1 is a function such that er L1 • L is the identity function. An instrumentation I of the source labelled language L 1, is a function replacing the labels with suitable increments of, say, a fresh global cost variable. Then, an annotation An of the source program can be derived simply as the composition of the labelling and the instrumentation functions:

An = I • L.
Suppose s is some adequate representation of the state of a program. Let P be a source program. The judgement (P, s) ⇓ s is the big-step evaluation of P transforming state s into a state s . Let us write s[v/x ] to denote a state s in which the variable x is assigned a value v. Suppose now that its annotation satisfies the following property:

(An(P ), s[c/cost]) ⇓ s [c + δ/cost] (1)
where c and δ are some non-negative numbers. Then, the definition of the instrumentation and the fact that the soundness proofs of the compilation functions have been lifted to the labelled languages allows to conclude that

(C(L(P )), s[c/cost]) ⇓ (s [c/cost], λ) (2)
where

C = C k • • • • • C 1
and λ is a sequence (or a multi-set) of labels whose 'cost' corresponds to the number δ produced by the annotated program. Then, the commutation properties of erasure and compilation functions allows to conclude that the erasure of the compiled labelled code er k+1 (C(L(P ))) is actually equal to the compiled code C(P ) we are interested in. Given this, the following question arises: under which conditions the sequence λ, i.e., the increment δ, is a sound and possibly precise description of the execution cost of the object code?

To answer this question, we observe that the object code we are interested in is some kind of assembly code and its control flow can be easily represented as a control flow graph. The idea is then to perform two simple checks on the control flow graph. The first check is to verify that all loops go through a labelled node. If this is the case then we can associate a finite cost with every label and prove that the cost annotations are sound. The second check amounts to verify that all paths starting from a label have the same cost. If this check is successful then we can conclude that the cost annotations are precise.

A toy compiler

As a first case study, we apply the labelling approach to a toy compiler.

The syntax of the source, intermediate and target languages is given in Figure 1. The three languages considered can be shortly described as follows: Imp is a very simple imperative language with pure expressions, branching and looping commands, Vm is an assembly-like language enriched with a stack, and Mips is a Mips-like assembly language [START_REF] Larus | Assemblers, linkers, and the SPIM simulator[END_REF] with registers and main memory.

The semantics of Imp is defined over configurations (S, K, s) where S is a statement, K is a continuation and s is a state. A continuation K is a list of Figure1: Syntax definitions. commands which terminates with a special symbol halt. The semantics of Vm is defined over stack-based machine configurations C (i, σ, s) where C is a program, i is a program counter, σ is a stack and s is a state. The semantics of Mips is defined over register-based machine configurations C (i, m) where C is a program, i is a program counter and m is a machine memory (with registers and main memory).

The first compilation function C relies on the stack of the Vm language to implement expression evaluation while the second compilation function C allocates (statically) the base of the stack in the registers and the rest in main memory. This is of course a naive strategy but it suffices to expose some of the problems that arise in defining a compositional approach. The formal definitions of these compilation functions C from Imp to Vm and C from Vm to Mips are standard and thus eluded. (See Appendix A for formal details about semantics and the compilation chain.)

Applying the labelling approach to this toy compiler results in the following diagram. The next sections aim at describing this diagram in details.

Imp Imp I o o er Imp Ù Ù C G G Vm er Vm C G G Mips er Mips Imp L s s C G G Vm C G G Mips er Vm • C = C • er Imp er Mips • C = C • er Vm er Imp • L = id Imp An Imp = I • L

Labelled languages: Syntax and Semantics

Syntax The syntax of Imp is extended so that statements can be labelled: S ::

= . . . | | : S. A new instruction emit( ) (resp. (emit )) is introduced in the syntax of Vm (resp. Mips).
Semantics The small step semantics of Imp statements is extended as described by the following rule.

( : S, K, s) -→ (S, K, s)
We denote with λ, λ , . . . finite sequences of labels. In particular, the empty sequence is written . We also identify an unlabelled transition with a transition labelled with . Then, the small step reduction relation we have defined on statements becomes a labelled transition system. We derive a labelled big-step semantics as follows: (S, s)

⇓ (s , λ) if (S, halt, s) λ1 -→ • • • λn --→ (skip, halt, s ) and λ = λ 1 • • • λ n .
Following the same pattern, the small step semantics of Vm and Mips are turned into a labelled transition system as follows:

C (i, σ, s) -→ (i + 1, σ, s) if C[i] = emit( ) . M (i, m) -→ (i + 1, m) if M [i] = (emit ) .
The evaluation predicate for labelled Vm is defined as

(C, s) ⇓ (s , λ) if C (0, , s) λ1 -→ • • • λn --→ (i, , s ), λ = λ 1 • • • λ n and C[i] = halt. The evaluation predicate for labelled Mips is defined as (M, m) ⇓ (m , λ) if M (0, m) λ1 -→ • • • λn --→ (j, m ), λ = λ 1 • • • λ n and M [j] = halt.

Erasure functions

There is an obvious erasure function er Imp from the labelled language to the unlabelled one which is the identity on expressions and boolean conditions, and traverses commands removing all labels. The erasure function er Vm amounts to remove from a Vm code C all the emit( ) instructions and recompute jumps accordingly. Specifically, let n(C, i, j) be the number of emit instructions in the interval [i, j]. Then, assuming C[i] = branch(k) we replace the offset k with an offset k determined as follows:

k = k -n(C, i, i + k) if k ≥ 0 k + n(C, i + 1 + k, i) if k < 0
The erasure function er Mips is also similar to the one of Vm as it amounts to remove from a Mips code all the (emit ) instructions and recompute jumps accordingly. The compilation function C is extended to Vm by simply translating emit( ) as (emit ):

C (i, C) = (emit ) if C[i] = emit( )

Compilation of labelled languages

The compilation function C is extended to Imp by defining:

C( : b, k) = (emit( )) • C(b, k) C( : S) = (emit( )) • C(S) .
Proposition 1. For all commands S in Imp , we have that:

(1) er Vm (C(S)) = C(er Imp (S)).

(

) If (S, s) ⇓ (s , λ) then (C(S), s) ⇓ (s , λ). 2
The following proposition relates Vm code and its compilation and it is similar to proposition 1. Here m -σ, s means "the low-level Mips memory m realizes the Vm stack σ and state s". Proposition 2. Let C be a Vm code. Then:

(1) er Mips (C (C)) = C (er Vm (C)).
(2) If (C, s) ⇓ (s , λ) and m -, s then (C (C), m) ⇓ (m , λ) and m -, s .

Labellings and instrumentations

Assuming a function κ which associates an integer number with labels and a distinct variable cost which does not occur in the program P under consideration, we abbreviate with inc( ) the assignment cost := cost + κ( ). Then we define the instrumentation I (relative to κ and cost) as follows:

I( : S) = inc( ); I(S) .
The function I just distributes over the other operators of the language. We extend the function κ on labels to sequences of labels by defining κ( 1 , . . .

, n ) = κ( 1 ) + • • • + κ( n ).

Sound and precise labellings

With any Mips code M , we can associate a directed and rooted (control flow) graph whose nodes are the instruction positions {0, . . . , |M | -1}, whose root is the node 0, and whose directed edges correspond to the possible transitions between instructions. We say that a node is labelled if it corresponds to an instruction emit .

Definition 2. A simple path in a Mips code M is a directed finite path in the graph associated with M where the first node is labelled, the last node is the predecessor of either a labelled node or a leaf, and all the other nodes are unlabelled.

Definition 3. A Mips code M is soundly labelled if in the associated graph the root node 0 is labelled and there are no loops that do not go through a labelled node. Besides, we say that a soundly labelled code is precise if for every label in the code, the simple paths starting from a node labelled with have the same cost.

In a soundly labelled graph there are finitely many simple paths. Thus, given a soundly labelled Mips code M , we can associate with every label a number κ( ) which is the maximum (estimated) cost of executing a simple path whose first node is labelled with . Thus for a soundly labelled Mips code the sequence of labels associated with a computation is a significant information on the execution cost.

For an example of command which is not soundly labelled, consider : while 0 < x do x := x + 1, which when compiled, produces a loop that does not go through any label. On the other hand, for an example of a program which is not precisely labelled consider : (if 0 < x then x := x + 1 else skip). In the compiled code, we find two simple paths associated with the label whose cost will be quite different in general. Proposition 6. If M is soundly (resp. precisely) labelled and (M, m) ⇓ (m , λ) then the cost of the computation is bounded by κ(λ) (resp. is exactly κ(λ)).

The next point we have to check is that there are labelling functions (of the source code) such that the compilation function does produce sound and possibly precise labelled Mips code. To discuss this point, we introduce in table 1 a labelling function L p for the Imp language. This function relies on a function "new" which is meant to return fresh labels and on an auxiliary function L p which returns a labelled command and a binary directive d ∈ {0, 1}. If d = 1 then the command that follows (if any) must be labelled.

A C compiler producing cost annotations

We now consider an untrusted C compiler prototype in ocaml in order to experiment with the scalability of our approach. Its architecture is described below:

C → Clight → Cminor → RTLAbs (front end) ↓ Mips or 8051 ← LIN ← LTL ← ERTL ← RTL (back-end)
The most notable difference with CompCert [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] is that we target the Intel 8051 [START_REF]MCS 51 Microcontroller Family User's Manual[END_REF] and Mips assembly languages (rather than PowerPc). The compilation from C to Clight relies on the CIL front-end [START_REF] Necula | CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs[END_REF]. The one from Clight to RTL has been programmed from scratch and it is partly based on the Coq definitions available in the CompCert compiler. Finally, the back-end from RTL to Mips is based on a compiler developed in ocaml for pedagogical purposes 7 ; we extended this back-end to target the Intel 8051. The main optimizations the back-end performs are liveness analysis and register allocation, and graph compression. We ran some benchmarks to ensure that our prototype implementation is realistic. The results are given in appendix B.9.

This section informally describes the labelled extensions of the languages in the compilation chain (see Appendix B for details), the way the labels are propagated by the compilation functions, and the (sound and precise) labelling of the source code. A related experiment concerning a higher-order functional language of the ML family is described in [START_REF] Amadio | Certifying and reasoning on cost annotations of functional programs[END_REF].

Labelled languages

Both the Clight and Cminor languages are extended in the same way by labelling both statements and expressions (by comparison, in the toy language Imp we just used labelled statements). The labelling of expressions aims to capture precisely their execution cost. Indeed, Clight and Cminor include expressions such as a 1 ?a 2 ; a 3 whose evaluation cost depends on the boolean value a 1 . As both languages are extended in the same way, the extended compilation does nothing more than sending Clight labelled statements and expressions to those of Cminor.

The labelled versions of RTLAbs and the languages in the back-end simply consist in adding a new instruction whose semantics is to emit a label without modifying the state. For the CFG based languages (RTLAbs to LTL), this new instruction is emit label → node. For LIN, Mips and 8051, it is emit label . The translation of these label instructions is immediate.

Labelling of the source language

As for the toy compiler, the goals of a labelling are soundness, precision, and possibly economy. Our labelling for Clight resembles that of Imp for their common instructions (e.g. loops). We only consider the instructions of Clight that are not present in Imp8 .

Ternary expressions They may introduce a branching in the control flow. We achieve precision by associating a label with each branch.

Program Labels and Gotos Program labels and gotos are intraprocedural. Their only effect on the control flow is to potentially introduce an unguarded loop. This loop must contain at least one cost label in order to satisfy the soundness condition, which we ensure by adding a cost label right after each program label.

Function calls In the general case, the address of the callee cannot be inferred statically. But in the compiled assembly code, we know for a fact that the callee ends with a return statement that transfers the control back to the instruction following the function call in the caller. As a result, we treat function calls according to the following invariants: (1) the instructions of a function are covered by the labels inside this function, (2) we assume a function call always returns and runs the instruction following the call. Invariant (1) entails in particular that each function must contain at least one label. Invariant ( 2) is of course an over-approximation of the program behavior as a function might fail to return because of an error or an infinite loop. In this case, the proposed labelling remains correct: it just assumes that the instructions following the function call will be executed, and takes their cost into consideration. The final computed cost is still an over-approximation of the actual cost.

Frama -C is a set of analysers for C programs with a specification language called ACSL. New analyses can be dynamically added through a plug-in system. For instance, the Jessie plug-in allows deductive verification of C programs with respect to their specification in ACSL, with various provers as back-end tools.

We developed the Cost plug-in for the Frama -C platform as a proof of concept of an automatic environment exploiting the cost annotations produced by the CerCo compiler. It consists of an ocaml program of 5 Kloc which in first approximation takes the following actions: (1) it receives as input a C program, (2) it applies the CerCo compiler to produce a related C program with cost annotations, (3) it applies some heuristics to produce a tentative bound on the cost of executing the C functions of the program as a function of the value of their parameters, (4) the user can then call the Jessie tool to discharge the related proof obligations. In the following we elaborate on the soundness of the framework, the algorithms underlying the plug-in, and the experiments we performed with the Cost tool.

Soundness

The soundness of the whole framework depends on the cost annotations added by the CerCo compiler, the synthetic costs produced by the Cost plug-in, the verification conditions (VCs) generated by Jessie, and the external provers discharging the VCs. The synthetic costs being in ACSL format, Jessie can be used to verify them. Thus, even if the added synthetic costs are incorrect (relatively to the cost annotations), the process in its globality is still correct: indeed, Jessie will not validate incorrect costs and no conclusion can be made about the WCET of the program in this case. In other terms, the soundness does not really depend on the action of the Cost plug-in, which can in principle produce any synthetic cost. However, in order to be able to actually prove a WCET of a C function, we need to add correct annotations in a way that Jessie and subsequent automatic provers have enough information to deduce their validity. In practice this is not straightforward even for very simple programs composed of branching and assignments (no loops and no recursion) because a fine analysis of the VCs associated with branching may lead to a complexity blow up.

Inner workings

The cost annotations added by the CerCo compiler take the form of C instructions that update by a constant a fresh global variable called the cost variable. Synthesizing a WCET of a C function thus consists in statically resolving an upper bound of the difference between the value of the cost variable before and after the execution of the function, i.e. find in the function the instructions that update the cost variable and establish the number of times they are passed through during the flow of execution. The plug-in proceeds as follows.

-Each function is independently processed and is associated a WCET that may depend on the cost of the other functions. This is done with a mix between abstract interpretation [START_REF] Cousot | Abstract Interpretation Frameworks[END_REF] and syntactic recognition of specific loops. -As result of the previous step, a system of inequations is built and its solution is attempted by an iterative process. At each iteration, one replaces in all the inequations the references to the cost of a function by its associated cost if it is independent of the other functions. This step is repeated till a fixpoint is reached. -ACSL annotations are added to the program according to the result of the above fixpoint. The two previous steps may fail in finding a concrete WCET for some functions, because of imprecision inherent in abstract interpretation, and because of recursive definitions in the source program not solved by the fixpoint. At each program point that requires an annotation (function definitions and loops), annotations are added if a solution was found for the program point. -The most difficult instructions to handle are loops. We consider loops for which we can syntactically find a counter (its initial, increment and last values are domain dependent). Other loops are associated an undefined cost ( ). When encountering a loop, the analysis first sets the cost of its entry point to 0. The cost inside the loop is thus relative to the loop. Then, for each exit point, we fetch the value of the cost at that point and multiply it by an upper bound of the number of iterations (obtained through arithmetic over the initial, increment and last values of the counter); this results in an upper bound of the cost of the whole loop, which is sent to the successors of the considered exit point.

Figure 2 shows the action of the Cost plug-in on a C program. The most notable differences are the added so-called cost variable, some associated update (increment) instructions inside the code, and an ensures clause that specifies the WCET of the is sorted function with respect to the cost variable. One can notice that this WCET depends on the inputs of the function. Running Jessie on the annotated and specified program generates VCs that are all proved by the automatic prover AltErgo9 .

Experiments

The Cost plug-in has been developed in order to validate CerCo's framework for modular WCET analysis. The plug-in allows (semi-)automatic generation and certification of WCET for C programs. Also, we designed a wrapper for supporting Lustre files. Indeed, Lustre is a data-flow language to program synchronous systems and the language comes with a compiler to C. The C function produced by the compiler implements the step function of the synchronous system and computing the WCET of the function amounts to obtain a bound on the reaction time of the system. We tested the Cost plug-in and the Lustre wrapper on the C programs generated by the Lustre compiler. We also tested it on some basic algorithms and cryptographic functions; these examples, unlike those generated by the Lustre compiler include arrays and for-loops. Table 3 provides a list of concrete programs and describes their type, functionality, the number of lines of the source code, and the number of VCs generated. In each case, the Cost plug-in computes a WCET and AltErgo is able to discharge all VCs. Obviously the generation of synthetic costs is an undecidable and open-ended problem. Our experience just shows that there are classes of C programs which are relevant for embedded applications and for which the synthesis and verification tasks can be completely automatized.

Acknowledgement The master students Kayvan Memarian and Ronan Saillard contributed both to the Coq proofs and the CerCo compiler in the early stages of their development. A.6 Notation Let t -→ be a family of reduction relations where t ranges over the set of labels and . Then we define:

File

t ⇒= ( - →) * if t = ( - →) * • t - → •( - →) * otherwise
where as usual R * denote the reflexive and transitive closure of the relation R and • denotes the composition of relations.

A.7 Proof of proposition 1

(1) By induction on the structure of the command S.

(2) By iterating the following proposition.

Proposition 14. If (S, K, s) t → (S , K , s ) and R(C, i, S •K) with t = or t = then C (i, σ, s) t ⇒ (j, σ, s ) and R(C, j, S • K ). This is an extension of proposition 11 and it is proven in the same way with an additional case for labelled commands. A.12 Proof of proposition 6

We discuss first the case for sound labelling. If λ = 1 • • • n then the computation is the concatenation of simple paths labelled with 1 , . . . , n . Since κ( i ) bounds the cost of a simple path labelled with i , the cost of the overall computation is bounded by κ

(λ) = κ( 1 ) + • • • κ( n ).
For the sound and precise labelling the proof above is repeated, by replacing the word bounds by is exactly and the words bounded by by exactly.

A.13 Proof of proposition 7

In both labellings under consideration the root node is labelled. An obvious observation is that only commands of the shape while b do S introduce loops in the compiled code. We notice that both labelling introduce a label in the loop (though at different places). Thus all loops go through a label and the compiled code is always sound.

To show the precision of the second labelling L p , we note the following property.

Lemma 1. A soundly labelled graph is precise if each label occurs at most once in the graph and if the immediate successors of the bge nodes are either halt (no successor) or labelled nodes.

Indeed, in a such a graph starting from a labelled node we can follow a unique path up to a leaf, another labelled node, or a bge node. In the last case, the hypotheses in the lemma 1 guarantee that the two simple paths one can follow from the bge node have the same length/cost.

A.14 Proof of proposition 8

By applying consecutively propositions 5 and propositions 6.

A.15 Proof of proposition 11

Given a Vm code C, we define an 'accessibility relation'

C

; as the least binary relation on {0, . . . , |C| -1} such that:

i C ; i C[i] = branch(k) (i + k + 1) C ; j i C ; j
We also introduce a ternary relation R(C, i, K) which relates a Vm code C, a number i ∈ {0, . . . , |C| -1} and a continuation K. The relation is defined as the least one that satisfies the following conditions.

C ; j C[j] = halt R(C, i, halt) i C ; i C = C1 • C(S) • C2 i = |C1| j = |C1 • C(S)| R(C, j, K) R(C, i, S • K)
.

The following properties are useful. (

) If i C ; j and R(C, j, K) then R(C, i, K). 2
The first property can be proven by induction on the definition of

C

; and the second by induction on the structure of K.

Next we can focus on the proposition. The notation

C i • C means that i = |C|. Suppose that: (S, K, s) → (S , K , s ) (1) and R(C, i, S • K) (2) .
From (2), we know that there exist i and i such that:

C ; i (3), C = C1 i • C(S) i • C2 (4), and R(C, i , K) (5)
and from (3) it follows that:

C (i, σ, s) * → (i , σ, s) (3 ) .
We are looking for j such that: C (i, σ, s) * → (j, σ, s ) (6), and R(C, j, S • K ) [START_REF] Fornari | Understanding how SCADE suite KCG generates safe C code[END_REF] .

We proceed by case analysis on S. We just detail the case of the conditional command as the the remaining cases have similar proofs. If S = if e 1 < e 2 then S 1 else S 2 then (4) is rewritten as follows:

C = C1 i • C(e1) • C(e2).bge(k1) a • C(S1) b • branch(k2) c • C(S2) i • C2
where c = a + k 1 and i = c + k 2 . We distinguish two cases according to the evaluation of the boolean condition. We describe the case (e 1 < e 2 ) ⇓ true. We set j = a.

-The instance of ( 1) is (S, K, s) → (S 1 , K, s).

-The reduction required in (6) takes the form C (i, σ, s) * → (i , σ, s) * → (a, σ, s ), and it follows from (3 ), the fact that (e 1 < e 2 ) ⇓ true, and proposition 10(2).

-Property [START_REF] Fornari | Understanding how SCADE suite KCG generates safe C code[END_REF], follows from lemma 2(2), fact [START_REF] Cousot | Abstract Interpretation Frameworks[END_REF], and the following proof tree:

B A C compiler

This section gives an informal overview of the compiler, in particular it highlights the main features of the intermediate languages, the purpose of the compilation steps, and the optimisations. The CerCo compiler can be both downloaded and tested as a web application at the URL http://www.pps.jussieu.fr/ ~yrg/ cerco.

B.1 Clight

Clight is a large subset of the C language that we adopt as the source language of our compiler. It features most of the types and operators of C. It includes pointer arithmetic, pointers to functions, and struct and union types, as well as all C control structures. The main difference with the C language is that Clight expressions are side-effect free, which means that side-effect operators (=,+=,++,. . .) and function calls within expressions are not supported. Given a C program, we rely on the CIL tool [START_REF] Necula | CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs[END_REF] to deal with the idiosyncrasy of C concrete syntax and to produce an equivalent program in Clight abstract syntax. We refer to the CompCert project [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] for a formal definition of the Clight language. Here we just recall in figure 4 its syntax which is classically structured in expressions, statements, functions, and whole programs. In order to limit the implementation effort, our current compiler for Clight does not cover the operators relating to the floating point type float. So, in a nutshell, the fragment of C we have implemented is Clight without floating point.

There is a notable difficulty to compile the C language into 8051 assembly code due to the fact that 8051's machine word are 8bits long and C has 32bits primitive datatypes. To deal with the dissimilarity in that case, we first translate the Clight input program into a Clight input program that only uses 8bits primitive datatypes.

B.2 Cminor

Cminor is a simple, low-level imperative language, comparable to a strippeddown, typeless variant of C. Again we refer to the CompCert project for its formal definition and we just recall in figure 5 its syntax which as for Clight is structured in expressions, statements, functions, and whole programs.

Translation of Clight to Cminor As in Cminor stack operations are made explicit, one has to know which variables are stored in the stack. This information is produced by a static analysis that determines the variables whose address may be 'taken'. Also space is reserved for local arrays and structures. In a second step, the proper compilation is performed: it consists mainly in translating Clight control structures to the basic ones available in Cminor.

Proposition 4 . 3 ) 5 .

 435 The instrumented Imp program relates to the labelled one as follows. Proposition 3. Let S be an Imp command. If (I(S), s[c/cost]) ⇓ s [c + δ/cost] then ∃ λ κ(λ) = δ and (S, s[c/cost]) ⇓ (s [c/cost], λ). Definition 1. A labelling is a function L from an unlabelled language to the corresponding labelled one such that er Imp • L is the identity function on the Imp language. For any labelling function L, and Imp program P , the following holds: er Mips (C (C(L(P ))) = C (C(P )) . (Proposition Given a function κ for the labels and a labelling function L, for all programs P of the source language if (I(L(P )), s[c/cost]) ⇓ s [c + δ/cost] and m -, s[c/cost] then (C (C(L(P ))), m) ⇓ (m , λ), m -, s [c/cost] and κ(λ) = δ.

Proposition 7 .

 7 For all Imp programs P , C (C(L p (P )) is a soundly and precisely labelled Mips code.Once a sound and possibly precise labelling L has been designed, we can determine the cost of each label and define an instrumentation I whose composition with L will produce the desired cost annotation.Lp(prog S) = prog Lp(S) Lp(S) = let = new , (S , d) = L p(S) in : S L p(S) = (S, 0) if S = skip or S = (x := e) L p(if b then S1 else S2) = (if b then Lp(S1) else Lp(S2),1) L p(while b do S) = (while b do Lp(S), 1) L p(S1; S2) = let (S 1 , d1) = L p(S1), (S 2 , d2) = L p(S2) in case d1 0 : (S 1 ; S 2 , d2) 1 : let = new in (S 1 ; : S 2 , d2) Table1: A labelling for the Imp language Definition 4. Given a labelling function L for the source language Imp and a program P in the Imp language, we define an annotation for the source program as follows: An Imp (P ) = I(L(P )) . Proposition 8. If P is a program and C (C(L(P ))) is a sound (sound and precise) labelling then (An Imp (P ), s[c/cost]) ⇓ s [c + δ/cost] and m -, s[c/cost] entails that (C (C(P )), m) ⇓ m , m -, s [c/cost] and the cost of the execution is bounded by (is exactly) δ.

  int is sorted (int *tab, int size) { int i, res = 1; for (i = 0 ; i < size-1 ; i++) if (tab[i] > tab[i+1]) res = 0; return res; } (a) The initial C source code. int cost = 0; /*@ ensures ( cost ≤ \old( cost)+(101+(0<size-1?(size-1)*195:0))); */ int is sorted (int *tab, int size) { int i, res = 1, cost tmp0; cost += 97; cost tmp0 = cost; /*@ loop invariant (0 < size-1) ⇒ (i ≤ size-1); @ loop invariant (0 ≥ size-1) ⇒ (i ≡ 0); @ loop invariant ( cost ≤ cost tmp0+i*195); @ loop variant (size-1)-i; */ for (i = 0; i < size-1; i++) { cost += 91; if (tab[i] > tab[i+1]) { cost += 104; res = 0; } else cost += 84; } cost += 4; return res; } (b) The annotated source code generated by Cost.

Figure2:

  Figure2: An example of the Cost plug-in action.

Figure3:

  Figure3: Experiments on CerCo and the Cost plug-in.

A. 8 Proof of proposition 2 ( 1 )( 2 )-

 8212 The compilation of the Vm instruction emit( ) is the Mips instruction (emit ). By iterating the following proposition. Proposition 15. Let C : h be a well formed code. If C (i, σ, s) t → (j, σ , s ) with t = or t = , h(i) = |σ| and m -σ, s then C (C) (p(i, C), m) t ⇒ (p(j, C), m ) and m -σ , s .A.9 Proof of proposition 3We extend the instrumentation to the continuations by defining:I(S • K) = I(S) • I(K) I(halt) = halt .Then we examine the possible reductions of a configuration (I(S),I(K), s[c/cost]).-IfS is an unlabelled statement such as while b do S then I(S) = while b do I(S ) and assuming (b, s) ⇓ true the reduction step is: (I(S), I(K), s[c/cost]) → (I(S ), I(S) • I(K), s[c/cost]) . Noticing that I(S) • I(K) = I(S • K), this step is matched in the labelled language as follows: (S, K, s[c/cost]) → (S , S • K, s[c/cost]) . On the other hand, if S = : S is a labelled statement then I(S) = inc( ); I(S ) and, by a sequence of reductions steps, we have: (I(S), I(K), s[c/cost]) * → (I(S ), I(K), s[c + κ( )/cost]) . This step is matched by the labelled reduction: (S, K, s[c/cost]) -→ (S , K, s[c/cost]) . A.10 Proof of proposition 4 By diagram chasing using propositions 1(1), 2(1), and the definition 1 of labelling. A.11 Proof of proposition 5 Suppose that: (I(L(P )), s[c/cost]) ⇓ s [c + δ/cost] and m -s[c/cost] . Then, by proposition 3, for some λ: (L(P ), s[c/cost]) ⇓ (s [c/cost], λ) and κ(λ) = δ . Finally, by propositions 1(2) and 2(2) : (C (C(L(P ))), m) ⇓ (m , λ) and m -s [c/cost] .

  i

Lemma 2 .

 2 [START_REF] Amadio | Compiler Design and Intermediate Languages[END_REF] The relation C ; is transitive.

  i

CerCo project http://cerco.cs.unibo.it

Esterel Technologies. http://www.esterel-technologies.com.

AbsInt Angewandte Informatik. http://www.absint.com/.

Frama -C software analyzers. http://frama-c.com/.

Chronos tool. www.comp.nus.edu.sg/ ~rpembed/chronos.

The recently proposed ARM Cortex M series would be another obvious candidate.

http://www.enseignement.polytechnique.fr/informatique/INF564/

We do not consider expressions with side-effects because they are eliminated by CIL.

AltErgo prover. http://ergo.lri.fr/

There is an obvious circularity in this definition that can be easily eliminated by defining first the function d following the case analysis in table 7, then the function p, and finally the function C as in table7.

A A toy compiler

We formalize the toy compiler introduced in section 2 and sketch the related proofs. The related, browsable formal development in Coq is available at http: //www.pps.jussieu.fr/ ~yrg/cerco.

A.1 Imp: language and semantics

The syntax of the Imp language is described below. This is a rather standard imperative language with while loops and if-then-else. Let s be a total function from identifiers to integers representing the state. If s is a state, x an identifier, and n an integer then s[n/x] is the 'updated' state such that s[n/x](x) = n and s[n/x](y) = s(y) if x = y. The big-step operational semantics of Imp expressions and boolean conditions is defined as follows: A continuation K is a list of commands which terminates with a special symbol halt: K ::= halt | | S • K. Table 2 defines a small-step semantics of Imp commands whose basic judgement has the shape: (S, K, s) → (S , K , s ). We define the semantics of a program prog S as the semantics of the command S with continuation halt. We derive a big step semantics from the small step one as follows: (S, s) ⇓ s if (S, halt, s) → • • • → (skip, halt, s ).

A.2 Vm: language and semantics

Following [START_REF] Leroy | Mechanized semantics, with applications to program proof and compiler verification[END_REF], we define a virtual machine Vm and its programming language. The machine includes the following elements: (1) a fixed code C (a possibly empty sequence of instructions), (2) a program counter pc, (3) a store s (as for the source program), (4) a stack of integers σ.

Given a sequence C, we denote with |C| its length and with C[i] its i th element (the leftmost element being the 0 th element). The operational semantics of the instructions is formalized by rules of the shape C (i, σ, s) → (j, σ , s ) and it is fully described in table 3. Notice that Imp and Vm semantics share the same notion of store. We write, e.g., n • σ to stress that the top element of the stack

Table2: Small-step operational semantics of Imp commands

Table3: Operational semantics Vm programs exists and is n. We will also write (C, s) ⇓ s if C (0, , s) * → (i, , s ) and

Code coming from the compilation of Imp programs has specific properties that are used in the following compilation step when values on the stack are allocated either in registers or in main memory. In particular, it turns out that for every instruction of the compiled code it is possible to predict statically the height of the stack whenever the instruction is executed. We now proceed to define a simple notion of well-formed code and show that it enjoys this property. In the following section, we will define the compilation function from Imp to Vm and show that it produces well-formed code. Definition 5. We say that a sequence of instructions C is well formed if there is a function h : {0, . . . , |C|} → N which satisfies the conditions listed in table 4 for 0 ≤ i ≤ |C| -1. In this case we write C : h.

The conditions defining the predicate C : h are strong enough to entail that h correctly predicts the stack height and to guarantee the uniqueness of h up to the initial condition.

Proposition 9. (1) If

Table4: Conditions for well-formed code

A.3 Compilation from Imp to Vm

In table 5, we define compilation functions C from Imp to Vm which operate on expressions, boolean conditions, statements, and programs. We write sz (e), sz (b), sz (S) for the number of instructions the compilation function associates with the expression e, the boolean condition b, and the statement S, respectively. We follow [START_REF] Leroy | Mechanized semantics, with applications to program proof and compiler verification[END_REF] for the proof of soundness of the compilation function for expressions and boolean conditions. Proposition 10. The following properties hold:

Next we focus on the compilation of statements. We introduce a ternary relation R(C, i, K) which relates a Vm code C, a number i ∈ {0, . . . , |C| -1} and a continuation K. The intuition is that relative to the code C, the instruction i can be regarded as having continuation K. (A formal definition is available in Appendix 11.) We can then state the correctness of the compilation function as follows.

Proposition 11. If (S, K, s) → (S , K , s ) and R(C, i, S•K) then C (i, σ, s) * → (j, σ, s ) and R(C, j, S • K ).

As announced, we can prove that the result of the compilation is a wellformed code.

Proposition 12. For any program P there is a unique h such that C(P ) : h.

A.4 Mips: language and semantics

We consider a Mips-like machine [START_REF] Larus | Assemblers, linkers, and the SPIM simulator[END_REF] which includes the following elements: (1) a fixed code M (a sequence of instructions), (2) a program counter pc, (3) a finite set of registers including the registers A, B, and R 0 , . . . , R b-1 , and ( 4) an (infinite) main memory which maps locations to integers.

We denote with R, R , . . . registers, with l, l , . . . locations and with m, m , . . . memories which are total functions from registers and locations to (unbounded) integers. We denote with M a list of instructions. The operational semantics is formalized in table 6 by rules of the shape M (i, m) → (j, m ), where M is a list of Mips instructions, i, j are natural numbers and m, m are memories. We write

Table6: Operational semantics Mips programs

A.5 Compilation from Vm to Mips

In order to compile Vm programs to Mips programs we make the following hypotheses: (1) for every Vm program variable x we reserve an address l x , (2) for every natural number h ≥ b, we reserve an address l h (the addresses l x , l h , . . . are all distinct), and (3) we store the first b elements of the stack σ in the registers R 0 , . . . , R b-1 and the remaining (if any) at the addresses l b , l b+1 , . . .. We say that the memory m represents the stack σ and the store s, and write m -σ, s, if the following conditions are satisfied: (1) s(x) = m(l x ), and ( 2

Table7: Compilation from Vm to Mips

The compilation function C from Vm to Mips is described in table 7. It operates on a well-formed Vm code C whose last instruction is halt. Hence, by proposition 12(3), there is a unique h such that C : h. We denote with

Given a well formed Vm code C with i < |C| we denote with p(i, C) the position of the first instruction in C (C) which corresponds to the compilation of the instruction with position i in C. This is defined as 10 Hence d(i,C) is the number of Mips instructions associated with the i th instruction of the (well-formed) C code. The functional correctness of the compilation function can then be stated as follows. RTLAbs is the last architecture independent language in the compilation process. It is a rather straightforward abstraction of the architecture-dependent RTL intermediate language available in the CompCert project and it is intended to factorize some work common to the various target assembly languages (e.g. optimizations) and thus to make retargeting of the compiler a simpler matter. We stress that in RTLAbs the structure of Cminor expressions is lost and that this may have a negative impact on the following instruction selection step. Still, the subtleties of instruction selection seem rather orthogonal to our goals and we deem the possibility of retargeting easily the compiler more important than the efficiency of the generated code.

Syntax. In RTLAbs, programs are represented as control flow graphs (CFGs for short). We associate with the nodes of the graphs instructions reflecting the Cminor commands. As usual, commands that change the control flow of the program (e.g. loops, conditionals) are translated by inserting suitable branching instructions in the CFG. The syntax of the language is depicted in table 8. Local variables are now represented by pseudo registers that are available in unbounded number. The grammar rule op that is not detailed in table 8 defines usual arithmetic and boolean operations (+, xor, ≤, etc.) as well as constants and conversions between sized integers.

Translation of Cminor to RTLAbs. Translating Cminor programs to RTLAbs programs mainly consists in transforming Cminor commands in CFGs. Most commands are sequential and have a rather straightforward linear translation. A conditional is translated in a branch instruction; a loop is translated using a back edge in the CFG.

B.4 RTL

As in RTLAbs, the structure of RTL programs is based on CFGs. RTL is the first architecture-dependant intermediate language of our compiler which, in its current version, targets the Mips and 8051 assembly languages.

Syntax. RTL is very close to RTLAbs. It is based on CFGs and explicits the

Mips or the 8051 instructions corresponding to the RTLAbs instructions. Type information disappears: everything is represented using machine words. Moreover, each global of the program is associated to an offset. The syntax of the language can be found in table 9. The grammar rules unop, binop, uncon, and bincon, respectively, represent the sets of unary operations, binary operations, unary conditions and binary conditions of the target assembly language.

Translation of RTLAbs to RTL. This translation is mostly straightforward. A RTLAbs instruction is often directly translated to a corresponding assembly instruction. There are a few exceptions: some RTLAbs instructions are expanded Table9: Syntax of the RTL language in two or more assembly instructions. When the translation of a RTLAbs instruction requires more than a few simple assembly instruction, it is translated into a call to a function defined in the preamble of the compilation result.

B.5 ERTL

As in RTL, the structure of ERTL programs is based on CFGs. ERTL explicits the calling conventions of the Mips assembly language. In the back-end for 8051, we defined our own calling convention since there were none.

Syntax. The syntax of the language is given in table 10. The main difference between RTL and ERTL is the use of hardware registers. Parameters are passed in specific hardware registers; if there are too many parameters, the remaining are stored in the stack. Other conventionally specific hardware registers are used: a register that holds the result of a function, a register that holds the base address of the globals, a register that holds the address of the top of the stack, and some registers that need to be saved when entering a function and whose values are restored when leaving a function. Following these conventions, function calls do not list their parameters anymore; they only mention their number. Two new instructions appear to allocate and deallocate on the stack some space needed by a function to execute. Along with these two instructions come two instructions to fetch or assign a value in the parameter sections of the stack; these instructions cannot yet be translated using regular load and store instructions because we do not know the final size of the stack area of each function. At last, the return instruction has a boolean argument that tells whether the result of the function may later be used or not (this is exploited for optimizations).

Translation of RTL to ERTL. The work consists in expliciting the conventions previously mentioned. These conventions appear when entering, calling and leaving a function, and when referencing a global variable or the address of a local variable.

Optimizations. A liveness analysis is performed on ERTL to replace unused instructions by a skip. An instruction is tagged as unused when it performs an assignment on a register that will not be read afterwards. Also, the result of the liveness analysis is exploited by a register allocation algorithm whose result is to efficiently associate a physical location (a hardware register or an address in the stack) to each pseudo register of the program.

B.6 LTL

As in ERTL, the structure of LTL programs is based on CFGs. Pseudo registers are not used anymore; instead, they are replaced by physical locations (a hardware register or an address in the stack). Syntax. Except for a few exceptions, the instructions of the language are those of ERTL with hardware registers replacing pseudo registers. Calling and returning conventions were explicited in ERTL; thus, function calls and returns do not need parameters in LTL. The syntax is defined in table 11. Translation of ERTL to LTL. The translation relies on the results of the liveness analysis and of the register allocation. Unused instructions are eliminated and each pseudo register is replaced by a physical location. In LTL, the size of the stack frame of a function is known; instructions intended to load or store values in the stack are translated using regular load and store instructions.

Optimizations. A graph compression algorithm removes empty instructions generated by previous compilation passes and by the liveness analysis.

B.7 LIN

In LIN, the structure of a program is no longer based on CFGs. Every function is represented as a sequence of instructions.

Syntax. The instructions of LIN are very close to those of LTL. Program labels, gotos and branch instructions handle the changes in the control flow. The syntax of LIN programs is shown in table 12. Translation of LTL to LIN. This translation amounts to transform in an efficient way the graph structure of functions into a linear structure of sequential instructions.

B.8 Assembly

We refer to [START_REF]MCS 51 Microcontroller Family User's Manual[END_REF] for a description of the 8051 assembly language. In order to compute tight bounds, the CerCo compiler actually generates 8051 binaries. For instance, the number of memory words associated with branching instructions can only be determined at this level (the number depends on the length of the offset).

In the following we describe the simpler Mips assembly language. A program in Mips is a sequence of instructions. The Mips code produced by the compilation of a Clight program starts with a preamble in which some useful and non-primitive functions are predefined (e.g. conversion from 8 bits unsigned integers to 32 bits integers). The subset of the Mips assembly language that the compilation produces is defined in table 13.

B.9 Benchmarks

To ensure that our prototype compiler is realistic, we performed some preliminary benchmarks on a 183MHz MIPS 4KEc processor, running a linux based distribution. We compared the wall clock execution time of several simple C programs compiled with our compiler against the ones produced by Gcc set up with optimization levels 0 and 1. As shown by Figure 6, our prototype compiler produces executable programs that are on average faster than Gcc's without optimizations.