Download Bound-T Reference Manual - Bound

example, if v is a volatile cell with no value assertions, and x is a non-volatile cell, the "live"
expression v+x can take any value, whatever value x has. However, if we know (from an
assertion) that v is between 2 and 5, then bounds on x lead to bounds on v+x and therefore x is
"live" at this point in the program.
Arithmetic analysis includes volatile cells, but the Presburger relation which models a flowgraph step defines no relation between the value of a volatile cell, after the step, and the value
of any other cell or expression, before or after the step. In effect, any use of a volatile cell
returns an unknown (opaque) value, only limited by the assertions, if any, on the value of the
cell. However, if the same volatile cell is used several times in one and the same step, this
model assumes that the same value results from each use. This feature of the arithmetic model
must be taken into account in the processor-specific instruction decoders and flow-graph
builders in each version of Bound-T. For example, if the processor has an instruction sub r,x,y
which subtracts two memory operands x and y and stores the result into a register r, and the
program applies this instruction to a volatile memory location v in the form sub r,v,v, and if
the two reads of v in this single instruction can return different values, then the flow-graph
builder must divide this instruction into two flow-graph steps where each step reads v once. If,
instead, the instruction is modelled as one step with the effect r := v ‒ v, then the arithmetic
analysis would see this effect as r := 0, which would be incorrect.
2.3
Execution-time analysis
Execution-time (WCET) analysis is an optional step in Bound-T, enabled with the option -time
and disabled with -no_time. The option is enabled by default.
Execution-time analysis follows (or calls for) the various analyses of the computation, and
consists of three parts:
•
bounding loop repetitions,
•
finding execution-time bounds on flow-graph nodes (basic blocks), and
•
calculating the WCET bound with the IPET method.
Bounding loop repetitions
The loop-bound analysis in Bound-T is aimed at counter-controlled loops, where the loop
termination is controlled by one (or several) loop counters. A loop counter is a program
variable (represented as a storage cell in Bound-T) that is initialized to an initial value before
the loop, increased (or decreased) by a non-zero value on each repetition of the loop, and is
used in the loop termination or repetition condition in such a way that the loop can be
repeated only while the variable is less than (or greater than) a limit value. The initial value,
increment or decrement, and limit value must all be known constants, or have known ranges,
at this point in the analysis (that is, after the constant propagation, possibly including
propagation of context-dependent parameter values).
Accordingly, Bound-T analyses each loop as follows:
•
find possible counter variables by studying the Presburger transfer relation for the loop
body (from and including the loop head up to an edge that repeats the loop) to detect which
storage cells have a bounded and non-zero increment or decrement (of constant sign); such
storage cells are candidates for loop counters,
•
for each such loop-counter candidate, use the Presburger relation for the values of storage
cells on entry (initialization) of the loop to compute bounds on the initial value, and retain
only those candidates where the initial value is bounded in a direction that matches the sign
of the increment or decrement,
•
for each remaining loop-counter candidate, use the Presburer relation for the values of
storage cells on the loop's repeat edges (“back” edges) to see if there is a complementary
limit on the values of the counter that permit repetition of the loop.
Bound-T Reference Manual
Execution-time analysis
21