Tool Integration

The two partners in the APARTS project have each developed their own analysis tool, with somewhat different and even complementary capabilities:

The SWEET tool from Mälardalen University excels at control-flow analysis, finding loop bounds, infeasible paths, and other kinds of "flow facts" which can be useful for several kinds of program analyses, of which WCET analysis is one. SWEET accepts a program in the ALF language and models the program's computations in various ways, based on abstract interpretation and abstract execution, and using several forms of abstract numerical domains. However, to analyse a program in C, it must be translated into ALF; to analyse a program in its executable form (which is usually necessary for WCET analysis), the machine-language program must first be translatated into ALF.
The Bound-T tool from Tidorum Ltd analyses machine-code programs for several target-processor architectures, producing WCET bounds and stack-usage bounds. The tool's analyses of the computation are not based on abstract interpretation, but on a more "analytical" approach in which the program's integer computations are modelled as a system of affine integer equations and inequations (technically speaking, a Presburger Arithmetic model), from which various analysis results such as loop-bounds can be extracted by a solver. Thus, its control-flow analysis is in many cases weaker than that of SWEET, but in other cases it can be faster than SWEET's analysis.

Within the APARTS project we will develop and implement an integration of SWEET and Bound-T such that:

Bound-T can translate its internal program model into ALF, which SWEET can then analyse. This provides a front-end for SWEET to read machine-language programs of several target processor types.
SWEET's analysis results (variable-value bounds, flow facts) can be returned to Bound-T, for use in further analysis phases, for example to calculate a WCET bound by combining the flow facts from SWEET with Bound-T's knowledge of the execution time taken by each basic block of code.
In particular, when the program under analysis contains dynamic control flow (indirect jumps or indirect calls through pointers), SWEET's more powerful and global value-analysis will be used to resolve the possible targets of the dynamic control flow, from which Bound-T can then continue to reconstruct the control-flow graphs and call-graphs of the program under analysis.