a³ release 15.04

Targets

  • a³ for ARM now supports the IAR and Tasking compilers.
  • a³ for V850 now supports the WindRiver compiler.
  • StackAnalyzer for Renesas RX and SuperH now available.
  • TimingProfiler for PowerPC and TriCore now available.

EVA framework

Stack analysis and value analysis for SPARC, TriCore, and V850 have been ported to the new EVA value analysis framework. This implies changes in analysis behavior and precision, see the corresponding notes for PowerPC, C28x and FR81 in release 14.10.

Qualification Support Kits

  • New QSKs:
    • aiT for ARM, compiler-specific (TI 4.9.1)
    • StackAnalyzer for ARM, generic
    • StackAnalyzer for ARM, compiler-specific (TI 4.9.1)
  • Added a test case for the default loop bound option.
  • Added test cases for the default recursion bound and the default incarnation bound options for recursive routines.
  • Improved requirement documentation of the QK_COMPILER_FUNCTION_POINTER_LOOKUP_COUNTING test case.
  • Improved evaluation of the not analyzed stack usage/effect feature.
  • Tool run evaluation messages now inform if the test run has passed due to an expected failure.
  • qk_setting_expected_result: check all variants of violated expected bounds.

32-bit Windows support

32-bit Windows is no longer supported.

User interface

  • The Functions and Variables views have been merged into a single DWARF view. Additionally, this view is now able to handle larger and more complex DWARF debug information.
  • The analysis options have been reorganized.
  • In AIS editor views, every annotation that has been applied to an object in the call graph is now marked with an orange star. Clicking on the star allows jumping directly to that location in the graph or assembly.
  • Improved and extended statistics:
    • Some of the data presented in tables is now additionally visualized as bar charts.
    • Global and per-context variable usage statistics are now computed for WCET paths.
    • Statistics on the memory usage of global variables and code are now available.
  • New wizard for submitting a support request.
  • Various improvements to the AIS wizard.
  • The keyboard shortcut for reload in the Disassembly view is now F5, consistent with the rest of the user interface.
  • Improved file dialogs to start in the directory the current file/project is located in, or the default document directory when no file has been opened yet.

AIS2

First AIS2 annotations are now officially available.

  • New AIS2 annotations:
    • for using sets of values in expressions and register/memory cell refinements, e.g.
      ais2 { routine "func" enter with: reg("r2") = [ 4, 56, 14 ]; }
      // register r2 contains the value 4, or 56, or 14
    • for memory contents using sets of values, e.g.
      ais2 { area "configValue" contains data: [ 7, 300, 14 ]; }
      // memory cell "configValue" contains 7, or 300, or 14
    • for asserting instruction assembly strings, e.g.
      instruction "f" -> call(1) {
          enter with: "r4" = 0x400080;
          assert assembly: "bl <memcpy>";
      }
      This annotates the contents of register r4 at the first call within routine f. By means of the assembly string assertion we ensure that the call is a non-computed call to memcpy. If the assembly string does not match, the decoder reports this accordingly:
      Assertion failed: Assembly string 'bctrl <fInput, gOutput>' does not match expected assembly string 'bl <memcpy>'.
  • New annotations for EVA targets (currently C28x, FR81, PowerPC, SPARC, TriCore, and V850):
    • AIS2 offers the possibility to assert targets of memory accesses. The following example demonstrates a few memory access assertions:
      instruction 0x8500 assert accesses: 0x8100 to 0x81ff;
      instruction "main" -> read(1) assert accesses: "tab";
      instruction 0x2100 assert accesses speculatively: 0x1000;
    • The user may specify that calls to certain routines are not possible from a selected routine. The following example annotates that any call from main to cma and cmk is infeasible:
      routine "main" calls to "cma", "cmk" infeasible;
    • Relocated sections can be accessed not only by the new .section(0xABCDEF) name but also the original .section name, e.g.:
      ais2 { area relocated section(".ROM.SECTION") {writable:true;}; }
    • EVA targets support trace partitioning that is triggered on and off as follows:
      ais2 {
         instruction 0x1000 begin partitioning: trace;
         instruction 0x1120 end partitioning;
      }
  • AIS2 allows defining symbolic expressions:
    define <name>: <expression>;
    The decoder will attempt to evaluate the <expression> to a constant. If this is possible, every occurrence of def(<name>) is replaced by the evaluated constant. Otherwise, any reference to <name> is replaced by the <expression> that is evaluated by later analysis phases, such as the value analysis. Example:
    define "count": reg("r1") + 1;
    define "n": 4;
    
    routine "main" {
        instruction -> computed(1) enter with:
        reg("r4") = def("n") * def("count");
    }
    The symbolic expression def("n") evaluates to 4, whereas the symbolic expression def("count") cannot be evaluated during decoding. After that, the value analysis attempts to compute 4 * (reg("r1") + 1) to determine the contents of register r4.
  • Improved extraction of source code annotations (removed wrong parsing warnings about include directives and string problems).
  • Improved detection of unused calls, branches to, and returns to annotations.

Decoding

  • Significantly reduced the decoder’s memory consumption by discarding internal symbols such as .L<number>.
  • Improved sanity check for the area is copied annotation.
  • Improved decoding of path names in symbol entries for the GHS compiler.
  • Improved reporting of annotation files not found during decoding and files that are more recent than the analyzed binaries.
  • Improved message about unreadable or writable areas in the executable during the control-flow reconstruction phase. When possible, the matching DWARF variable name is provided.
  • Improved stripping of the compilation directory from DWARF file and line information.
  • ARM:
    • Improved decoding of trampoline function calls, computed calls via tables of function pointers, and THUMB ldr*/str* instructions.
    • Improved switch/call table resolution for TI and ARM compilers.
    • Improved switch table decoding for GHS.
    • Improved detection of ARM/THUMB mode switches.
    • Improved detection of calls via bx with manual saving of LR.
    • Improved instruction set switching for automatically resolved computed call and branch targets.
    • Improved routine name selection if special symbols for the routine start exist, like $a/$t for ARM/THUMB switching.
    • Improved loop bound detection.
    • Improved routine return type detection (normal or immediate).
    • Support for ARM and THUMB encodings of FLDMX and DSTMX as VLDM/VSTM or VPUSH/VPOP.
    • Support for 32-bit variants of THUMB bl instructions.
  • C16x: improved loop bound detection for loops using 8-bit loop counters.
  • C28x: improved switch table decoding.
  • FR81: improved switch table decoding.
  • HCS12: improved handling of calls via trampoline routines.
  • PowerPC:
    • Improved decoding of tlbsync instructions.
    • Further improvements to switch table decoding for GHS.
  • TriCore: improved initial register contents guessing (SDA base, CSA).
  • V850:
    • Added support for WindRiver compiler.
    • Improved automatic switch and call table decoding for GHS.
    • Decoding stops upon encountering a HALT instruction, that point is considered the end of the program.
  • x86: improved switch table decoding for the Cygnus LynxOS compiler.

Stack and value analysis

  • The option "Faster stack analysis without worst-case path information at routines" is now on by default. If worst-case stack paths for all routines are required, deactivate this setting.
  • Improved speed of StackAnalyzer’s path enumeration algorithm.
  • Improved prevision in flag computation for bitwise logical operations.
  • AIS user registers are now always treated like 32-bit hardware registers, independent of the target architecture.
  • More precise analysis of trampoline routines and prolog/epilog functions generated by the compiler by keeping more contexts alive for them.
  • Improved precision when a default incarnation bound of 1 is used.
  • StackAnalyzer now outputs a warning and computes no stack height if the analysis start is (backwards) infeasible.
  • The analyzer now outputs recursion call stacks if the default recursion bound is used:
    a8daan: Warning #3097: In "test.c", line 200:
    In routine 'test1', at address thumb::0x1000:
    For routine 'test1' the default incarnation bound of 1 is used.
    Please verify that this is correct, recursion details:
           1: test1
           2: test_middle
           3: test_middle2
           4: test1
  • Routines with calls to multiple targets are now marked with an asterisk in StackAnalyzer’s output to make it easier to search for overapproximations:
    => Call stack for maximum global usage:
    ->     0 <  32> 'main' (*)
    ->    32 <   0> 'cma'
    => 32 bytes of system stack
  • The global stack information in the graph now has an additional info field with the stack history for the global worst path.
  • Warnings about access to read-only or constant memory now include the matching variable name if possible:
    Warning #3075: In "dry2_1.c", line 214:
    In routine 'Proc0.L1', at address 0x3f40ea:
    Write access to [0x003f8000]:1 ('counter'),
    which overlaps with read-only memory.
  • All EVA targets (C28x, FR81, PowerPC, SPARC, TriCore, V850):
    • Faster value analysis.
    • More precise value analysis for targets with speculative execution.
    • Higher precision of value analysis for small max-length mapping settings.
    • Higher precision for
      • arithmetical right shifts,
      • carry-bit computations for shift operations,
      • addresses stored in registers across conditionals that check for specific alignment constraints,
      • C-like a%b operations emulated via div/mul/sub instruction sequences,
      • multiplication operations emulated via shift/add instruction sequences,
      • and multiplication in general.
    • Improved loop analysis for loops with exit checks containing ==.
    • More precise computation of carry out for add/sub (with carry).
    • Show the accessed section in the interactive value analysis.
    • Improved reporting of missing loop bounds, with the relevant contexts now being listed:
      eva-ppc: Info: In "allloops.inc", line 190:
         In routine 'nestedLDep.L2', at address 0x80338:
         Loop 'nestedLDep.L2' is unbounded in 2 contexts:
         ..., 0x80398->"nestedLDep", 0x80320->"nestedLDep.L1"[1/2..]
         ..., 0x80398->"nestedLDep", 0x80320->"nestedLDep.L1"[2/2..]
    • Improved application of loop ranges.
    • StackAnalyzer skips enumeration of call stacks when the result is known to be unbounded because of local unbounded effects.
    • Improved precision of value analysis by intersecting the stack pointer on function returns. A message is issued if the intersection leads to infeasibilities.
  • ARM:
    • Higher precision for branch splitting, arithmetic shift operations, multiply–accumulate instructions, and the value analysis of computed calls.
    • Improved stack analysis of conditional returns with a stack effect.
    • Improved handling of calling conventions.
  • HCS12: faster stack analysis for programs with stack-modifying loops.
  • PowerPC: for bclr, bclrl, bcctr, and bcctrl, only the lowest bit of LR or CTR is assumed to be masked to be compatible with the VLE extension.
  • SPARC: changed handling of traps, consult the manual for a detailed description of the behavior.
  • V850:
    • Added support for the WindRiver Diab compiler.
    • Corrected address computations for CALLT instructions via the CTBP register.

Cache and pipeline analysis

  • Cortex R4F:
    • Improved pipeline model.
    • Improved handling of COF instructions.
  • MPC7448: improved analysis computation time by optimizing instruction property caching in the analysis.
  • XC2000: experimental support for co-processor (MAC) instructions.

Visualization and reporting

  • Improved and faster HTML reporting.
  • Improved visualisation of WCET paths, stack analysis results, and infeasible routines in the result graph.
  • Trampoline routines like ICALL/__ind_call/F_CALL are now inlined in the call graph.
  • Improved sorting of graph search results.
  • The notification about a graph being outdated is now less intrusive.
  • New license feature viewer: a³ now offers a mode for viewing existing analysis results without running any analysis.