Example of Bound-T/8051 analysis


This note shows how a small 'C' program for the Intel-8051 is analysed by Bound-T and what the results are. Both execution time (WCET) analysis and stack-usage analysis are demonstrated.

The example program

The source code of the example 'C' program is displayed with line numbers for reference, when it can, Bound-T uses source-line numbers in its outputs to identify the relevant part of the program, for example a loop or a call.

This program does nothing useful, but has been designed to illustrate several features and limitations of Bound-T with a compact example.

Some points to be noted in this example are:

Compiling and linking the example program

For this example, the C program was compiled with the SDCC compiler for a "standard" 8051 target.

The SDCC compiler generates an image of the executable code in Intel-Hex form and a separate file of debugging information (a "*.cdb" file). Both these files are given as input to Bound-T for the analysis. However, it is enough to name the Intel-Hex file in the Bound-T command, because Bound-T automatically looks for a "*.cdb" file with the same name.

Here is a ZIP archive with the source-code and executable files.

First attempt with fully automatic analysis

Assuming that the example program is compiled and linked into an executable machine-code file called example.exe, we can try to find an upper bound on the worst-case execution time (WCET) of the whole program (the main function) by invoking Bound-T in fully automatic mode, using the following command:

boundt_8051 example.exe main

The components of this command are:

Bound-T tries to compute a WCET bound but fails, with the error message:

Error:example.exe:example.c:main:9-14:Could not be fully bounded.

The fields (between colons) of this message have the following meaning:

In addition to the error message, Bound-T produces the following output (on the standard-output stream). This output includes more detailed error messages. Line numbers are added here for reference.

 1  Device:example.exe::::8051
 2  Time_Unit:example.exe::::Machine cycles.
 3  Compiler:example.exe::::SDCC
 4  Loop_Bound:example.exe:example.c:Solve:31-35:8
 5  Loop_Bound:example.exe:example.c:main@12-=>Foo@19=>Count:23-26:9
 6  Loop_Bound:example.exe:example.c:main@14=>Solve:31-35:8
 7  Wcet_Call:example.exe:example.c:main@12-=>Foo@19=>Count:21-26:240
 8  Wcet_Call:example.exe:example.c:main@12-=>Foo:16-19:249
11  main@14=>Solve@33-=>Ones
12     Loop unbounded at example.c:44-45, offset 0006H
13  main@14=>Solve@35-=>Count
14     Loop unbounded at example.c:23-26, offset 0002H

In line 1, Bound-T notes that it assumes that the program to be analysed will run on an "8051" device, that is, a processor that implements the original or "standard Intel-8051 (MCS-51) instruction set with the original instruction timing. This is the default that Bound-T assumes if there is no specific "-device" option.

In line 2, Bound-T notes that the WCET bounds will be given in "machine cycle" units. In a standard" 8051 processor each machine cycle is 12 clock cycles. In "accelerated" 8051 processors, a machine cycle may be shorter, or there may be no "machine cycle" concept and instructions are timed directly in clock cycles.

In line 3, Bound-T notes that it assumes that the example program was compiled with SDCC. It makes this assumption because it detects that the executable file, example.exe, is in Intel-Hex format. (The assumption can be overridden by a command-line option if necessary.)

In line 4, Bound-T reports that it has determined that the loop in the function Solve, at lines 31-35 in example.c, will repeat at most 8 times in any call of Solve.

Line 5 also reports a loop-bound, now for the loop in the function Count, at lines 23-26 in example.c. However, the loop depends on a parameter of Count, so this bound (9 repetitions) is valid for a specific call path where main calls Foo, and Foo calls Count. Looking at the source code in example.c, we see that the first call supplies a value of 6 for the parameter num in Foo, and the second call adds 3 to give the value 9 for the parameter u in Count, which in the end determines the number of loop repetitions in Count.

Line 6 shows that the general bound of 8 iterations on the loop in Solve (which is shown in line 4) is not improved by taking into account the parameter values supplied in the call from main to Solve. Bound-T reanalyses Solve for this specific call because it has not found a general bound on the loop in Ones which is called from Solve.

Lines 7 and 8 report WCET bounds that Bound-T has computed for the subprograms Count and Foo. These WCET bounds are context-specific, that is, they are valid for some but not all calls of the subprogram in question. This is why the lines begin with the keyword "Wcet_Call" instead of just "Wcet". The WCET bound on Count in line 7 applies when Count is called from Foo (which is called from main) and corresponds to the Loop_Bound in line 5. The WCET bound on Foo in line 8 applies to this call of Foo and also corresponds to the Loop_Bound in line 5.

Lines 11 through 14 are the most important in this case, since they report two loops for which Bound-T could not find repetition bounds. Both loops are reached from main via the call of Solve.

Lines 11-12 report that the loop in Ones, called from Solve could not be bounded. To understand why, we must look at the source code, and see that the loop in Ones is a while-loop without any evident loop-counter, a kind of loop that Bound-T cannot handle automatically. We must specify a manual bound as will be shown later.

Lines 13-14 report that the loop in Count, called from Solve could not be bounded. The source code shows that the loop depends on the parameter u of Count, which comes from the local variable k in Solve, which is assigned the return value of Ones. Bound-T does not analyse the values returned by subprograms and therefore cannot bound this loop.

Second attempt with manual assertions

To compute a WCET bound for the example program, we must help Bound-T find bounds on the loops reported in lines 11 through 14 above. This is done by writing an assertion file. This can be done in several ways, for example as in the following text (line numbers added for reference):

 1  subprogram "Ones"
 2     loop repeats <= 16 times;
 3     end loop;
 4  end "Ones";
 6  subprogram "Solve"
 7     variable "k" 0 .. 16;
 8  end "Solve";

Line 1 declares that the following lines, up to line 4, refer to the subprogram Ones. Lines 2-3 specify that the loop repeats at most 16 times in any call of Ones. This is because the SDCC compiler uses 16 bits forint variables and so the variable x is 16 bits long and can be shifted right at most 16 times before it becomes zero. For the same reason, the value returned from Ones is always between 0 and 16.

Line 6 declares that the following lines, up to line 8, refer to the subprogram Solve. Line 7 asserts that the variable k will always be greater or equal to zero and less or equal to 16, at any point in the execution of any call of Solve. This holds because k is assigned the return value from Ones, which is between 0 and 16 as explained above.

Assuming that the assertion file is named ass.txt, the following command invokes Bound-T as above to analyse the main function, but under these assertions:

boundt_8051 -assert ass.txt example.exe main

This time, the analysis succeeds without error messages. The output is the following, with line numbers added for reference:

 1  Device:example.exe::::8051
 2  Time_Unit:example.exe::::Machine cycles.
 3  Compiler:example.exe::::SDCC
 4  Loop_Bound:example.exe:example.c:Solve:31-35:8
 5  Loop_Bound:example.exe:example.c:Solve@35-=>Count:23-26:16
 6  Loop_Bound:example.exe:example.c:main@12-=>Foo@19=>Count:23-26:9
 7  Wcet_Call:example.exe:example.c:main@12-=>Foo@19=>Count:21-26:240
 8  Wcet_Call:example.exe:example.c:main@12-=>Foo:16-19:249
 9  Wcet:example.exe:example.c:Ones:39-48:285
10  Wcet_Call:example.exe:example.c:Solve@35-=>Count:21-26:422
11  Wcet:example.exe:example.c:Solve:28-37:6343
12  Wcet:example.exe:example.c:main:9-14:6606

Lines 1 through 5 are as in the first attempt. Line 6 reports a new loop-bound found in Count, which is deduced from the assertion on the value of k in Solve. No "Loop_Bound" line appears for the loop in Ones, because this loop was directly bounded by an assertion.

Lines 7 through 12 report WCET estimates (upper bounds) for various subprograms and calls. The last line (line 12) is the final result: the WCET for main is at most 6606 machine cycles. To find this value, Bound-T also computed WCET bounds for Ones (285 cycles, line 9) and Solve (6343 cycles, line 11). These WCET values apply to any call of these subprograms. For the subprograms Count and Foo, Bound-T had to consider the context of the call, and found WCET bounds for three different calls paths as shown by lines 7, 8, and 10.

Tabular output

If we add the command-line option "-table", Bound-T writes a tabular form of the analysis results as a number of output lines beginning with the keyword Time_Table:


The table is best viewed by passing the output through a script that formats the table for easy reading, with this result:

Total     Self      Num       Time Per Call
Time      Time      Calls     Min       Max       Subprogram
-----     ----      -----     -------------       ----------
6606      14        1         6606      6606      main
6343      402       1         6343      6343      Solve
3616      3616      9         240       422       Count
2565      2565      9         285       285       Ones
249       9         1         249       249       Foo

As you can see, the table shows at a glance which subprograms are used in the worst-case scenario, how many times each subprogram is called, how much time is spent in the subprogram including its callees, and how much of this time is spent in other subprogram itself, excluding callees.

Call graph and control-flow graphs

If we add the command-line option "-dot graphs.dot", Bound-T draws the call-graph of main and the control-flow graphs of each analysed subprogram. The graphs are written to the file named in the -dot option (here "graphs.dot") in a textual notation called the DOT form (from Drawer Of Trees). The program dot, from the Bell Labs GraphViz package, converts the graphs to other forms such as Postscript. The images that you can open from the links below have been converted to the PNG (Portable Network Graphics) form.

Stack analysis

With the additional command-line option "-stack_path", Bound-T will find the worst-case stack consumption of the main subprogram. This option adds the following lines to the output:


The output lines beginning with keyword Stack show the upper bounds on the stack usage of each subprogram, as Bound-T finds these bounds. The main result is thus on the last Stack line which shows that the main subprogram in this example needs at most 4 octets of space on the Intel-8051 hardware stack, which is called "sp". (Some compilers for the Intel-8051 use additional, software-managed stacks, which then have other names.)

The Stack_Path lines and Stack_Leaf line show a call-path starting from main that uses the maximal amount of stack space. In this example, there is only one Stack_Path line, because this worst-case call call-path contains only the call from main to Solve; the later calls from Solve to Ones and Count need no more stack space. (This is because the stack space for a return address is counted in the stack usage of the calling subprogram.) In detail, these lines show:

As in this example, there may be calls from the subprogram identified in a Stack_Leaf line to other, deeper subprograms, so this subprogram is not necessarily a "leaf" subprogram in the call-graph. However, these calls do not increase the maximum stack usage of the subprogram.

Note that the execution path with the worst-case execution time is often different from the path with the worst-case stack usage. Bound-T finds them separately. Note also that there may be several different call-paths with the same worst-case stack usage; Bound-T shows only one of them.

Valid HTML 4.01 Transitional