a³ release 9.12

New operating systems

Support for 64-bit Windows (Vista and Windows 7).

New targets

  • a³ for HC11: support for MC68HC11K1
  • a³ for LEON2
  • a³ for MPC55xx: support for MPC553x (e200z3 core)

New Qualification Support Kit (QSK)

  • a³ QSK for HC11 (aiT)

New analyses

  • TimingExplorer analysis for
    • ARM7
    • MPC55xx
    • MPC603e
    • MPC755s
  • Difference analysis
    This experimental feature allows to graphically compare two WCET analysis graphs starting at the same entry point. This is especially helpful for comparing different analysis setups (differ­ent annotations, hardware settings, etc.). See screenshot.

General improvements

  • Fixes for user-reported and internally detected issues.
  • Significantly decreased overall memory usage and computation time.
  • Better sorting of analysis results and improved visualization.
  • Executables from AbsInt are now digitally signed. This proves that the software vendor is AbsInt and should guarantee that the code has not been altered or corrupted since it was created and signed.

a³ launcher

  • New command line switch -l to force showing of launcher. For example, a3 mpc755 -l shows launcher with all available MPC755 builds.
  • Initial support for XTC version 1.x and 2.0. Starting integration with T1, a measuring software from Gliwa, to query missing loop bounds via XTC.

a³ GUI — general

  • The performance of the a³ GUI has been greatly improved for projects with many analyses.
  • Combined Results view and Analyses overview. Progress and results for all analyses are now shown on the same page. Sorting and deletion of analyses have been improved.
  • Result graphs are no longer opened automatically after running an analysis. To open the result graph for a particular analysis, double-click on the corresponding row in the analyses overview.
  • a³ now ensures that only up-to-date result graphs are shown. If a graph has changed, its latest version will be loaded automatically.
  • New “Sections” view, which allows to view all sections of the binary and inspect their content like in a hex editor. It also allows to show the memory content for a given address area.
  • MPC55xx, MPC5xx, and TriCore: added import of target/memory configuration from system register contents.
  • The percentage of infeasible code and code that lies on the WCET path is now calculated in the Source Files view.
  • Added syntax highlighting in disassembly view.
  • For both stack-usage and WCET analysis, code sections that lie on the worst-case path are now marked red in the source-code and disassembly view. Infeasible parts of the analyzed program are now grayed out in the resulting graphs and the disassembly view.
    In the source-code view, infeasible code and code that lies on the worst-case path is marked by a colored margin rather than by a colored background. Thus, if a line contains both infeasible code and code that contributes to the WCET, it will have two margins of different colors. See screenshots.
  • For messages that have address information, one can jump to the corresponding address in the disassembly by selecting Go to disassembly” from the context menu. See screenshot. (The executable must have been disassembled via Analysis” → Disassembly” in order for this feature to work.)
  • Improved validation whether all input files needed for the analysis are available. The user is notified about missing files via red input field background and symbols in the navigation bar. See screenshot.
  • MD5sums of input files are now included in the report file. MD5sum calculation under Windows has been improved.
  • Fixed an issue where renaming an analysis item sometimes caused an abnormal termination of the GUI.
  • Analyses sometimes used the wrong configuration if multiple configurations had been configured. This issue has been fixed.
  • a³ GUI no longer forgets analyses results in overview page after a new analysis is added.
  • The user can now copy table entries into the clipboard for further usage.
  • Improved import of license.dat. If the user clicks on “Change License…”, a³ tries to import the selected license file to the installation directory. If there is no writing permission, the license will be stored in a data directory suggested by the operating system.
  • Improved path replacements list. It is now possible to add all proposed replacements to the list at once rather than one by one.
  • Improved search and sorting in “Symbols” view.

a³ GUI — editor

  • a³ text editor defaults to UTF-8 encoding, fallback to Latin-1.
  • One can comment and uncomment all selected lines in the text editors by using the shortcuts Ctrl + K and Ctrl + Shift + K, respectively. If no line has been selected, the action is applied to the current line.
  • Report and source files displayed in the a³ GUI are now write-protected by default. The mode can be switched between read-only and editable in the “Edit” menu under “Toggle editable”.
  • The AIS Wizard now supports more annotations and paged architectures. See screenshot.
  • Improved automatic reloading in the text editor.

AIS annotations

  • The program point in “instruction … is entered with …” can now be a symbolic loop expression. For example, it is now possible to specify:
    instruction "prime" + 1 loop is entered with @ctr = @ctr + 1;
  • AIS expressions now support two new operators:
    • restrict for the intersection of result intervals
    • try for supplying default values for expressions that fail to produce a bounded interval.
  • Parametric loop bounds can now contain a special variable “value” that stands for the result of the automatic loop bound analysis. By using this variable, the analysis result may be mod­i­fied, e.g. restricted by “restrict” or replaced by a default value if it is unbounded.
    Examples (let E be a general expression):
    • loop <PP> max restrict (value, E)
      This restricts the automatically determined loop bound value by the value of expression E. The resulting loop bound is the intersection of the two intervals. For example, if the provided expression E evaluates to (1..6) and the automatically determined value is (3..9), the resulting loop bound will be (3..6).
    • loop <PP> max try (value, E)
      This supplies E as the default value to be taken if the automatic analysis returns the value “unbounded” or “undefined”. However, in all other cases the value returned by the analysis is taken, even if it is less precise than E.
    • loop <PP> max try (restrict (value, E), 1000)
      This specifies that either the result of the automatic loop analysis or the user-provided expression E will be used, depending on which is more precise. The number 1000 in this example serves as a fall-back solution if both the automatic analysis and the evaluation of E fail to produce a bounded interval.
  • Memory cells can be referenced in expressions, e.g. “mem (0x123)” or “mem (sp + 8)”. The access width is the standard access width of the target architecture. Non-standard widths can be specified as “mem byte (0x123)” or “mem (0x123, 1)”.
    Examples:
    • loop <PP> max try (mem(sp+1, 1), 10)
      If the value analysis can determine the top-most byte on the stack (because of the “, 1” in mem), then the value of the byte is taken as the loop bound. Otherwise, the loop bound is 10.
    • snippet <PP> is not executed if try ((mem byte (0x123)) ≤ 2, 0)
      The referenced code snippet is excluded from analysis if the byte content of memory cell 0x123 is less than 2. If the content of the memory cell is not known by the analysis, the expression evaluates to the default value 0 (which corresponds to false).
  • New annotation “tail call”:
    instruction <PP> is a tail call;
    This is equivalent to:
    instruction <PP> is a call and immediately returns;
  • The WCET contribution of code snippets with a single entry and a single exit that are not routines can now be listed in the report file by using the AIS command
    SNIPPET P1..P2 IS EVALUATED AS "Name";
    where Name is a label to identify the code snippet in the report file. It will then appear in the report file under the heading
    * WCET contributions of region 'Name' (routine 'R'):
    Note: this additional output can only be produced if “Path analysis variant: ILP based” is selected under Configuration” → Analyses”.

Decoding and control flow reconstruction

  • Improved decoding for ARM7, C33, HC12, M68020, Sparc, TriCore and x86.
  • Improved source code visualization in graph and disassembly view.
  • Improved symbol table handling:
    • Skip “File” symbols.
    • Remove duplicate symbols.
  • Unresolved source positions from source code annotations are now warnings, not errors.
  • DWARF Debug Reader:
    • Improved handling of the debug information for variables that have multiple locations throughout their lifetime.
    • Debug information is available for inlined functions as well.
    • Several changes regarding the debugging information:
      • The absolute address of variables or parameters that can change their location through­out their lifetime is now displayed. For example, a variable with the absolute address “reg(3) or reg(13)” is stored in register 3 during some part of its lifetime and in register 13 the rest of the time.
      • Information about the location of variables and parameters that are stored in more than one location is now provided. For example, the absolute address “reg(3):4, ?:4, fp-12:4” indicates a twelve-byte value whose first four bytes reside in register three, the middle four bytes are unavailable (e.g. due to optimization), and the last four bytes are in memory, twelve bytes before the frame base.
      • Negative offsets to the frame base are correctly displayed.
  • ARM7: improved stack pointer guessing.
  • C33: corrected decoding of  “ldi || ldi”.
  • HC12:
    • Improved switch pattern detection.
    • Improved handling of user annotations for computed calls.
  • M68020: improved switch pattern detection.
  • PowerPC: improved support for AdaCore GNAT compiler.
  • x86:
    • Reader for Map File implemented to read symbol entries for OMF386 executables.
    • Decoding problem with certain multiple instruction prefix combinations fixed.
    • Improved handling of floating-point instructions.

Loop analysis

  • Loop-bound formulas are now also evaluated for loops with more than one recursive call.
  • Improved information about detected loop bounds in report files.
  • Improved handling of TargetLink-generated code.
  • TriCore, M32, and SPARC: various improvements. Registers inside loops are now restricted to their possible ranges based on the calculated loop bounds.
  • M68020: various improvements.

Value analysis

  • Equality relations between registers and memory cells now supported.
  • Warning message if stack pointer lies in read-only memory.
  • Improved precision on memory load/stores with mixed access widths.
  • HC12: corrected semantics of rti for stack analysis.
  • M68020: various improvements.
  • PowerPC:
    • Optional visualization of the quality of value analysis results in the output graph. In­struc­tions are colored according to the precision of the obtained results. See screenshot.
    • The analyzed target address of computed branches and returns (blr and bctr instructions) is now compared with the instructions that follow in the control flow graph. The result is used to compute infeasible paths and issue warning messages for inconsistent control flows, e.g. resulting from wrong user annotations.
    • Changed quality information in access report from e.g. “unknown at worst” to a total count and percentage of contexts where this access is imprecise or unknown.
  • x86:
    • Support for more 486 cache-manipulating instructions.
    • Improved handling of memory accesses for pop_d_RegS and pop_w_RegS.

Pipeline analysis

  • Better handling of external routines as possible control flow exits.
  • Am486:
    • Improved timing model.
    • Support for dynamic cache switching between locked and not locked.
    • Optional FPU local worst-case mode.
  • ARM7: rewritten parts of the analysis to improve the computation time especially for larger tasks or tasks that use the cache.
  • C16x: rewritten parts of the analysis to improve the computation time especially for larger tasks.
  • i386: trailing writes are now taken into account.
  • M68020:
    • Improved general precision of the timing model.
    • Improved timing model with respect to instructions loading and writing operands from/to memory.
    • Added support for 16-bit ports.
  • MPC5xx: improved handling of accesses to USIU control registers if a non-zero internal memory space base address is used.
  • MPC55xx:
    • Improved VLE instruction timing model.
    • Added support for the e200z3 core used in MPC5533 and MPC5534.
  • MPC603e and MPC7448: improved handling of dispatch stall annotation.
  • MPC755: improved relational cache analysis.
  • TriCore: improved modeling of PLB, LMI and Flash Buffer.
  • V850: correctly determine source operand GPRs for ld*, st*, sld*, sst* and the “bit3 dis16[reg]” forms of not1, set1, clr1, and tst1.

Path analysis

  • Tighter ILP constraints generated from loop bounds. This leads to a better distribution of the runtime over the loop iterations on the WCET path and may increase the precision of the overall WCET bound.
  • Flow constraints work for external routines, too.
  • External routines are now handled as possible control flow exits. This can be forbidden by the “always returns” annotation, for example:
    snippet "R" is external and takes max 0 cycles and always returns;
  • Improved CPLEX output of predpathan.
  • Improved cumulative WCET calculation for predan/predpathan.
  • predpathan now supports tasks that are not completely unrolled.

Visualization of results

  • Improved statistics for external routines.
  • WCET contribution bars shown for external routines.
  • Show analysis name in GDL title.