# Changeset 3337

Ignore:
Timestamp:
Jun 7, 2013, 3:12:26 PM (4 years ago)
Message:

Final changes

File:
1 edited

### Legend:

Unmodified
 r3336 Frama-C \cite{framac} is a set of analysers for C programs with a specification language called ACSL. New analyses can be dynamically added through a plugin system. For instance, the Jessie plugin allows deductive via a plugin system. For instance, the Jessie plugin allows deductive verification of C programs with respect to their specification in ACSL, with various provers as back-end tools. Lustre compiler. \paragraph{Soundness.} The soundness of the whole framework depends on the cost \paragraph{Soundness} The soundness of the whole framework depends on the cost annotations added by the CerCo compiler, the synthetic costs produced by the Cost plugin, the verification conditions (VCs) generated by Jessie, and the cost plugin, 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 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 plugin, which can in soundness does not really depend on the action of the cost plugin, 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 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. \paragraph{Experience with Lustre.} Lustre is a data-flow language to program synchronous systems and the language comes with a compiler to C. We designed a \paragraph{Experience with Lustre} Lustre is a data-flow language for programming synchronous systems, with the language coming with a compiler to C. We designed a wrapper for supporting Lustre files. The C function produced by the compiler implements the step function of the bound on the reaction time of the system. We tested the Cost plugin and the Lustre wrapper on the C programs generated by the Lustre compiler. For programs consisting of a few hundred lines of code, the Cost plugin computes a WCET and Alt- consisting of a few hundred lines of code, the cost plugin computes a WCET and Alt- Ergo is able to discharge all VCs automatically. \paragraph{Handling C programs with simple loops.} \paragraph{Handling C programs with simple loops} 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. through during the flow of execution. In order to do the analysis the plugin makes the following assumptions on the programs: 1. No recursive functions. 2. Every loop must be annotated with a variant. The variants of ‘for’ loops are 1) there are no recursive functions; 2) every loop must be annotated with a variant. The variants of for' loops are automatically inferred. loop. An axiom is added to account the fact that the cost is accumulated at each step of the loop. The cost of the function is directly added as post-condition of the function The user can influence the annotation by different means: by using more precise variants or by annotating function with cost specification. The plugin will use this cost The cost of the function is directly added as post-condition of the function. The user can influence the annotation by two different means: 1) by using more precise variants; 2) by annotating functions with cost specifications. The plugin will use this cost for the function instead of computing it. \paragraph{C programs with pointers.} \paragraph{C programs with pointers} When it comes to verifying programs involving pointer-based data structures, such as linked lists, trees, or graphs, the use of traditional first-order logic to specify, and of SMT solvers to verify, shows some limitations. Separation logic \cite{separation} is then an elegant alternative. It is a program logic logic~\cite{separation} is an elegant alternative. It is a program logic with a new notion of conjunction to express spatial heap separation. Bobot has recently introduced in the Jessie plugin automatically generated separation predicates to simulate separation logic reasoning in a traditional verification framework where the specification language, the verification condition recently introduced automatically generated separation predicates to simulate separation logic reasoning in the Jessie plugin where the specification language, the verification condition generator, and the theorem provers were not designed with separation logic in mind. CerCo's plugin can exploit the separation predicates to automatically in-place list reversal. \subsection{The CerCo Compiler} \subsection{The CerCo compiler} In CerCo we have developed a certain number of cost preserving compilers based on the labeling approach. Excluding an initial certified compiler for a While on the labeling approach. Excluding an initial certified compiler for a while' language, all remaining compilers target realistic source languages---a pure higher order functional language and a large subset of C with pointers, gotos and all data structures---and real world target processors---MIPS and the Intel 8051/8052 processor family. Moreover, they achieve a level of optimization that ranges from moderate (comparable to gcc level 1) to intermediate (including Intel 8051/8052 processor family. Moreover, they achieve a level of optimisation that ranges from moderate (comparable to GCC level 1) to intermediate (including loop peeling and unrolling, hoisting and late constant propagation). The so called Trusted CerCo Compiler is the only one that was implemented in the called \emph{Trusted CerCo Compiler} is the only one that was implemented in the interactive theorem prover Matita~\cite{matita} and its costs certified. The code distributed is obtained extracting OCaml code from the Matita implementation. In the rest of is extracted OCaml code from the Matita implementation. In the rest of this section we will only focus on the Trusted CerCo Compiler, that only targets the C language and the 8051/8052 family, and that does not implement the advanced optimizations yet. Its user interface, however, is the same as the one the C language and the 8051/8052 family, and that does not implement any advanced optimisations yet. Its user interface, however, is the same as the one of the other versions, in order to trade safety with additional performances. In particular, the Frama-C CerCo plugin can work without recompilation with all that may require approximations or dependent costs. The (trusted) CerCo compiler implements the following optimizations: cast The (trusted) CerCo compiler implements the following optimisations: cast simplification, constant propagation in expressions, liveness analysis driven spilling of registers, dead code elimination, branch displacement, tunneling. The two latter optimizations are performed by our optimizing assembler \cite{correctness}. The back-end of the compiler works on three addresses spilling of registers, dead code elimination, branch displacement, and tunneling. The two latter optimisations are performed by our optimising assembler \cite{correctness}. The back-end of the compiler works on three address instructions, preferred to static single assignment code for the simplicity of the formal certification. The CerCo compiler is loosely based on the CompCert compiler \cite{compcert}, a recently developed certified compiler from C to the PowerPC, ARM and x86 microprocessors. Contrarily to CompCert, both the CerCo code and its microprocessors. Contrary to CompCert, both the CerCo code and its certification are open source. Some data structures and language definitions for the front-end are directly taken from CompCert, while the back-end is a redesign of a compiler from Pascal to MIPS used by François Pottier for a course at the of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the Ecole Polytechnique. \begin{enumerate} \item all of our intermediate languages include label emitting instructions to implement the labeling approach, and the compiler preserves execution traces. implement the labeling approach, and the compiler preserves execution traces, \item traditionally compilers target an assembly language with additional macro-instructions to be expanded before assembly; for CerCo we need to go all the way down to object code in order to perform the static analysis. Therefore we integrated also an optimizing assembler and a static analyser. we integrated also an optimising assembler and a static analyser, \item to avoid implementing a linker and a loader, we do not support separate compilation and external calls. Adding a linker and a loader is a transparent process to the labeling approach and should create no unknown problem. \item we target an 8-bit processor. Targeting an 8 bit processor requires process to the labeling approach and should create no unknown problem, \item we target an 8-bit processor. Targeting an 8-bit processor requires several changes and increased code size, but it is not fundamentally more complex. The proof of correctness, however, becomes much harder. complex. The proof of correctness, however, becomes much harder, \item we target a microprocessor that has a non uniform memory model, which is still often the case for microprocessors used in embedded systems and that is \end{enumerate} \subsection{A formal certification of the CerCo compiler} \subsection{Formal certification of the CerCo compiler} We implemented the CerCo compiler in the interactive theorem prover Matita and have formally certified that the cost model induced on the source code correctly and precisely predicts the object code behaviour. We actually induce two cost models, one for time and one for stack space used. We show the correctness of the prediction time and one for stack space consumption. We show the correctness of the prediction only for those programs that do not exhaust the available machine stack space, a property that thanks to the stack cost model we can statically analyse on the property that---thanks to the stack cost model---we can statically analyse on the source code using our Frama-C tool. The preservation of functional properties we take as an assumption, not itself formally proved in CerCo.  Other projects have out to be more complex than what we expected at the beginning. \paragraph{The statement.} \paragraph{The statement} Real time programs are often reactive programs that loop forever responding to events (inputs) by performing some computation followed by some action (output) space is a clear requirement of meaningfulness of a run, because source programs do not crash for lack of space while object code ones do. The balancing of function calls/returns is a requirement for precision: the labeling approach function calls and returns is a requirement for precision: the labeling approach allows the scope of label emission statements to extend after function calls to minimize the number of labels. Therefore a label pays for all the instructions safe bound, not that it is exact. The last condition on the entry/exit points of a run is used to identify sub-runs whose code correspond to a sequence of blocks that we can measure precisely. Any other choice would start/end the run in the that we can measure precisely. Any other choice would start or end the run in the middle of a block and we would be forced again to weaken the statement taking as a bound the cost obtained counting in all the instructions that precede the starting one in the block/follow the final one in the block. starting one in the block, or follow the final one in the block. I/O operations can be performed in the prefix of the run, but not in the measurable sub-run. Therefore we prove that we can predict reaction times, but \section{Future work} All the CerCo software and deliverables can be found on-line at the address \url{http://cerco.cs.unibo.it}. All the CerCo software and deliverables can be found on the CerCo homepage at~\url{http://cerco.cs.unibo.it}. The results obtained so far are encouraging and provide evidence that it is possible to perform static time and space analysis at the source level without loosing accuracy, reducing the trusted code base and reconciling the without losing accuracy, reducing the trusted code base and reconciling the study of functional and non-functional properties of programs. The techniques introduced seem to be scalable, cover both imperative and functional languages and are compatible with every compiler optimization functional languages and are compatible with every compiler optimisation considered by us so far. To prove that compilers can keep track of optimizations To prove that compilers can keep track of optimisations and induce a precise cost model on the source code, we targeted a simple architecture that admits a cost model that is execution history independent. to basic blocks that can be later transferred by the labeling approach to the source code and represented in a meaningful way to the user. The dependent labeling approach that we have studied seems a promising tools to achieve labeling approach that we have studied seems a promising tool to achieve this goal, but the cost model generated for a realistic processor could be too large and complex to be exposed in the source code. Further study is required Examples of further future work consist in improving the cost invariant generator algorithms and the coverage of compiler optimizations, in combining the labeling approach with type \& effect discipline \cite{typeffects} the labeling approach with the type and effect discipline of~\cite{typeffects} to handle languages with implicit memory management, and in experimenting with our tools in early development phases. Some larger case study is also necessary to evaluate the CerCo's prototype on industrial size programs. to evaluate the CerCo's prototype on realistic, industrial-scale programs. \bibliographystyle{llncs} \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache, B. Campbell, D. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I. B. Campbell, D. P. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I. Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177. \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C Programs}, N.  Ayache, R.M. Amadio, Y.Régis-Gianas, in Proc. FMICS, Springer Programs}, N.  Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer LNCS 7437: 32-46, 2012. \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of functional programs}. R.M. Amadio, Y. Régis-Gianas. Proceedings of the Second international conference R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer LNCS 7177:72-89, 2012. \bibitem{correctness} \textbf{On the correctness of an optimising assembler for the intel MCS-51 microprocessor}. D.P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second D. P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second international conference on Certified Programs and Proofs, Springer-Verlag 2012. \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time Systems}, F.J. Cazorla, E. Quiñones, T. Vardanega, L. Cucu, B. Triquet, G. Systems}, F.J. Cazorla, E. Qui\~{n}ones, T. Vardanega, L. Cucu, B. Triquet, G. Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions on Embedded Computing Systems, 2012.