WCET-Oriented Loop Bound Analysis
A companion web page

WCET-Oriented Loop Bound Analysis is built on top of the C CompCert verified compiler via the addition of a function that performs the loop bound computation and outputs the results of the analysis. These results can, for instance, be used by WCET tools to estimate the WCET of the program.

Page last updated on: 2014-03-10

Submitted Paper

This work has been presented at VSTTE 2013. You can download the paper and the slides.
To contact any of the authors (Sandrine Blazy, Andre Maroneze and David Pichardie), send an e-mail to [firstname].[lastname]@irisa.fr.

The main theorems listed in the paper can be found at the following files:

  1. Theorem 1 (main theorem) - bound_correct: GlobalBounds_proof
  2. Theorem 2 (start-to-end correctness) - transf_c_program_with_bound_correct: Main
  3. Theorem 3 (soundness of program slicing) - program_slicing_is_sound: WCETSlice
  4. Theorem 4 (termination of program slicing) - slicing_preserves_termination: WCETSlice

Coq Development

Download the last stable version of the Coq development: [.tgz]
(tested with OCaml 4.00 and Coq 8.3pl5).

Installation instructions

  1. Download and extract the loopbound archive (tar xvf loopbound.tgz)
  2. Inside the loopbound directory, run make all (optionally add -j4 for parallel processing) to Coq-prove all files, to extract the OCaml code and to compile it (this will take several minutes).
  3. Run make benchs to launch the analysis on a subset of the Mälardalen WCET benchmarks, displaying the obtained global bounds for each loop. Each loop is identified by its header node on the RTL language.

Afterwards, you can run rtlcomp -loopbounds <file> on a specific C program to analyze it.

Local bounds information

Adding option -localbounds to rtlcomp prints information about local loop bounds. You can therefore run rtlcomp -loopbounds -localbounds <file> on a C program. Running make benchs.debug will run all benchmarks with this extra flag.

Inserting annotations

To insert annotations such as the ones in the paper, you need to use CompCert's syntax for annotations: __builtin_annot("id"), where id is a string containing an unique identifier of your choice (note that, if you reuse an identifier, the result associated to it will be the sum of the executions of all program points containing the identifier, but it will still be a correct bound).
Annotations can be placed at any program point. For instance, consider the following example program: 

  int main() {
    int _reg_vint = 0; /* always add this line at the beginning of the main function */
    int i = 0;
    __builtin_annot("entry");
    do {
      i++;
      __builtin_annot("loop");
      } while (i < 5);
    __builtin_annot("exit");
    return 0;
  }
Running ccomp -bounds <file> will produce the following result: 
  Annotation bounds (3 annotations):
  exit -> Some (1)
  entry -> Some (1)
  loop -> Some (5)
Note: running ccomp -bounds <file> on a file that does not contain any annotations will not produce any output. To automatically bound all program loops, use rtlcomp -loopbounds <file> instead.

Additional information

  • To see the RTL representation of a program (after inlining), you can run ccomp -dinlining <file>, which generates a <file>.inlining.rtl file.
  • To see the result of the value analysis on a program, you can run rtlcomp <file>, which generates a <file>.value.rtl file where after each program point there is a line containing the inferred interval for each RTL variable. T (top) indicates an unknown interval.
  • To slice the program w.r.t. a particular statement, you can use the <file>.inlining.rtl file to obtain the number of the statement (say NN), and then run rtlcomp -slice NN <file> to obtain a <file>.slice.rtl file containing the result of the value analysis on the sliced program. Statements in the slice are prefixed with a dollar sign ($) and the slicing criterion is prefixed with an 'at' symbol (@).
  • In the development, our files are placed in the following directories: wcet, slice, vanalysis, bourdoncle and dev directories. The benchs directory contains the subset of Mälardalen benchmarks used in our experiments.

    • Browsable version of the Coq development

    The documentation gives a commented listing of the Coq specifications and proofs for the main development files.
    Proof scripts are folded by default, but can be viewed by clicking on "Proof".