5 Control Flow Elements

5.1 Function Element

A function element represents the static location inside the code for the given function. It contains statements so that it becomes possible to access dynamic properties corresponding to certain situations during the function execution.

FUNCTION ::=
  <function LOCATION-ATTRS INFORMATION-ATTRS>
    STATEMENT*
  </function>

The LOCATION-ATTRS are described in the following sections : they identify the static location of the function in the code. The INFORMATION-ATTRS is a generic hook where any flow information may be hooked (frequency, execution time, etc).

5.2 Statement Elements

Inside a function, different statements are supported and represents the flow structure of the code. They may compose themselves to reference situations depending on a specific context.

STATEMENT ::= BLOCK | LOOP | CALL | CONDITIONAL | ...

5.2.1 Block Element

A block element identifies only a piece of code possibly composed of several execution paths but with only one entry point.

BLOCK ::=
  <block LOCATION-ATTRS INFORMATION-ATTRS/>

5.2.2 Loop Element

A loop element matches a loop inside the code. It may contains <iteration> elements in order to distinguish property applied to different iterations.

LOOP ::=
  <loop LOCATION-ATTRS INFORMATION-ATTRS>
    STATEMENT*
  </loop>
| <loop LOCATION-ATTRS INFORMATION-ATTRS>
    <iteration number="INT">
      STATEMENT*
    </iteration>
  </loop>

The iteration number i may be positive identifying the ith iteration or negative, identifying, the ith last iteration.

5.2.3 Call Element

A call element identify the call to a function. Its location represents the code performing a call and it must contain a function element representing the called function. Several call elements embedding functions allows to represent a call-chain location. A call element may contain several functions when an indirect call is performed with several possible targets (like, in C, pointers of functions).

CALL ::=
  <call LOCATION-ATTRS INFORMATION-ATTRS>
    <!-- function -->+
@@ relâcher en FUNCTION | STATEMENT -> CONDITION contient n'importe quel STATEMENT : à débattre
  </call>

5.2.4 Condition Element

A condition element represents a condition with several alternative. In C, it matches as well if statement than switch statement.

CONDITIONAL ::=
  <conditional CONDITION-ATTR* LOCATION-ATTR*>
    CONDITION?
    CASE+
  </conditional>

CONDITION ::=
  <condition CONDITION-ATTR* LOCATION-ATTR*>
    (BLOCK | CONDITIONAL | CALL)*
  </condition>

CASE ::=
  <case CASE-ATTRS LOCATION-ATTR*>
      CONDITIONAL | STATEMENT
  </case>

These tags are used to represent a conditional statement in a very generic and uniform way. The conditional attributes are:

CONDITION-ATTR ::=
  expcond=”TEXT”
| precision=”EXACT|MAX|NOCOMP”

Where expcond is the symbolic expression of the condition and precision the precision of the analysis of count, one of

EXACT – successful computation,
MAX – upper bound of the actual expression,
NOCOMP – can not be computed (in this case, the total of then and else executions may be obtained from the containing scope).

The case attributes are presented below:

CASE-ATTRS ::=
| cond="INT"
| count="INT | NOCOMP"
| expcount="TEXT"

Where cond is the value that activates the case if it matches the condition, count the number of time the condition branch is taken, and expcount a symbolic expression of the count (when count can not be exactly computed).

Example 1: expression of an if( c ) tpart else epart:

<conditional>
  <condition expcond="c"> ... </condition>
  <case cond="1"> tpart </case>
  <case> epart </case>
</conditional>

Example 2: expression of a switch( c ) { case v1: s1; case v2: s2; default: s3; }

<conditional>
  <condition expcond="c"> ...</condition>
  <case cond="v1"> s1 </case>
  <case cond="v2"> s2 </case>
  <case> s3 </case>
</conditional>

5.3 Contextual Path

In this format, the nesting of elements does not need to reflect exactly and wholly the layout of the program. The idea is that an information item is more or less precise according to the context elements driving to it.

5.3.1 Paths in flow facts

First, let's define a path in the format of an ordered list of steps (callee function, function, loop, loop iteration, etc) organized in the reverse order of program execution. For example, the path p1 = [f3, call@1, f2, f1] represents the function f3 called at point 1 from function f2, itself called from function f1.

A flow fact system defining the item I, accessible by this path, would be declared as :

<function name="f1">
  <function name="f2">
    <call address="@1">
      <function name="f3">
        <!-- my information item I here -->
      </function>
    </call>
  </function>
</function>

It is clear that the path p2 = [f3, call@1, f2, call@2, f1] allows also to access I in the flow facts above but we can say that p2 is more precise than p1 because p1 accesses I whatever the call site of f2 in f1 is. Although the flow fact file does not provide enough precision to cope with the call@2 step, it is safe to use the information item at p1 because it is, by definition, an overestimation of I accessible by p2.

5.3.2 Flow fact system soundness

Let S be the set of steps and, therefore, the set of paths is S*.

Definition 1 Let two paths p1, p2, p1 includes p2 means that p1 is less accurate than p2 if

for all s in p1, s is in p2,
for all s1, s2 in p1, such that s1 is before s2 in p1 then s1 is also before s2 in p2.

We note I/p the information item I accessible by path p and a partial order on I domain D, "<" (I1 < I2 means that I1 is less precise than I2).

Definition 2 The partial order "<" is said conservative if

forall I1, I2 in D, I1 < I2
and for an analysis a in A : D → D', if A(I1) < A(I2), that is the analysis A(I1) gives a good approximation of A(I2) but less precise.

Example For the maximum loop bounds for WCET calculation, the domain is N (naturals) and the order is ">". For the program below, the loop bound 20 is sound overestimation but is less precise than 10.

int main(void) {
  int i, s = 0;
  for(i = 0; i < 10; i++)
    s += i;
  return s;
}

Definition 3 The flow fact system is sound relatively to an overstimation order "<" on the domain D of a flow item for an analysis A, if for all p1, p2, such that p1 includes p2 then I/p1 < I/p2.

5.3.3 Path approximation

Let two paths p1, p2 such that p1 includes p2.

If the flow facts have a definition of I2 (domain D, approximation order "<") for p2 but not for p1, can we find an approximation I1 for p1 such that I1 < I2 ?

The solution I1 is such that, for all p, p1 is included in, I1 < I/p. In fact, to ensure to have a sound approximation of I, we need to get all approximations of I and take the minimum.

Let p1 = [s1, ⋯, sn], we can observe that for all 1 <m>⇐</m> i < n, we denote the path pi = [s1, ⋯, si], I/pi < I/p1 but for all i < j, I/pi < I/pj. In fact, the best approximation is the one obtained by p1 (although we have a fall-through method using included paths).

The problem is that we need to know all including path of p1 to compute I/p1 but note that we only need I of one-step p+1 paths including p1, p+1 = [s1, ⋯, sn, sn+1] if we can assert that all possible sn+1 steps ensure the coverage of the different cases.

Looking at the flow fact system, when can we say that it is a full coverage ?

Content