# Changeset 3436

Ignore:
Timestamp:
Feb 14, 2014, 7:21:57 PM (7 years ago)
Message:

Section 4.5 revisions.

File:
1 edited

### Legend:

Unmodified
 r3435 \label{sec:exploit} We now turn our attention to synthesising high-level costs, such as the execution time of a whole program.  We consider as our starting point source level costs the reaction time of a real-time program.  We consider as our starting point source level costs provided by basic labelling, in other words annotations on the source code which are constants that provide a sound and sufficiently The principle that we have followed in designing the cost synthesis tools is that the synthetic bounds should be expressed and proved within a general that the synthesised bounds should be expressed and proved within a general purpose tool built to reason on the source code. In particular, we rely on the Frama-C tool to reason on C code and on the Coq proof-assistant to reason on higher-order functional programs. This principle entails that: 1) The inferred synthetic bounds are indeed correct as long as the general purpose tool is; 2) there is no limitation on the class of programs that can be handled as long as the user is willing to carry on an interactive proof. This principle entails that the inferred synthetic bounds are indeed correct as long as the general purpose tool is, and that there is no limitation on the class of programs that can be handled, for example by resorting to interactive proof. Of course, automation is desirable whenever possible. Within this framework, concept of an automatic environment exploiting the cost annotations produced by the CerCo compiler. It consists of an OCaml program which essentially 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 uses the CerCo compiler to produce a related C program with cost annotations, and 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 plugin to discharge the parameters. The user can then call the Jessie plugin to discharge the related proof obligations. In the following we elaborate on the soundness of the framework and the experiments we performed with the Cost tool on the C programs produced by a experiments we performed with the Cost tool on C programs, including some produced by a Lustre compiler. \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 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 annotations added by the CerCo compiler, the verification conditions (VCs) generated by Jessie, and the external provers discharging the VCs. Jessie can be used to verify the synthesised bounds because our plugin generates them in ACSL format. Thus, even if the added synthetic costs are incorrect (relatively to the cost annotations), the process as a whole 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 plugin, which can in soundness does not depend on 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 for programming synchronous systems, with a compiler which targets C. We designed a wrapper for supporting Lustre files. 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 The C function produced by the compiler is relatively simple loop-free code which implements the step function of the synchronous system and computing the WCET of the function amounts to obtaining a 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 that update the cost variable and establish the number of times they are passed through during the flow of execution. To perform the analysis the plugin makes the following assumptions on the programs: 1) there are no recursive functions; 2) every loop must be annotated with a variant. The variants of for' loops are automatically inferred. The plugin proceeds as follows. First the call graph of the program is computed. Then the computation of the cost of the function is performed by traversing its control flow graph. If the function $f$ calls the function $g$ then the function $g$ is processed before the function $f$. The cost at a node is the maximum of the assumes that there are no recursive functions in the program, and that every loop is annotated with a variant. In the case of for' loops the variants are automatically inferred where a loop counter can be syntactically detected. The plugin computes a call-graph and proceeds to calculate bounds for each function from the leaves up to the main function. The computation of the cost of each function is performed by traversing its control flow graph, where the cost of a node is the maximum of the costs of the successors. In the case of a loop with a body that has a constant cost for every step of the 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. The user can also specify more precise variants and annotate functions with their own cost specifications. The plugin will use these instead of computing its own, allowing greater precision and the ability to analyse programs which the variant generator does not support. In addition to the loop-free Lustre code, this method was successfully applied to a small range of cryptographic code.  See~\cite{labelling} for more details. \paragraph{C programs with pointers.} When it comes to verifying programs involving pointer-based data structures,