a³ release 16.10

  • The Windows version now makes use of certain libraries it did not rely on before. Should you get a message about missing libraries on first startup, simply install the Visual C++ redistributable from Microsoft.
  • Jenkins logo
    We now offer a free plugin for automatic integration of a³ in Jenkins, the leading open-source automation server.
  • The alauncher executable is now used for automation of a³ and Astrée (running analyses in batch mode, e.g. within continuous-integration systems). It provides a verbose --help.
  • The Safety Manual now describes qualified tool workflows for a³ and Astrée and also covers regulations for medical devices, in particular the FDA Principles of Software Validation.

Targets

  • StackAnalyzer and ValueAnalyzer now available for TI MSP430(x).
  • aiT for ARM now supports Infineon XMC4500 (Cortex-M4 core).
  • aiT for C28x now supports TMS320F28035, …335, and …069.

Qualification Support Kits

  • New QSKs now available for:
    • aiT and StackAnalyzer for ARM, THUMB2 instruction set, generic and compiler-specific for GCC 4.9.3
    • aiT and StackAnalyzer for C16x, compiler-specific for Tasking VX 2.4r1
  • Removed test for pipeline analysis widening threshold as this option has been removed.
  • Implemented test cases for AIS2 language constructs.

Integration with TargetLink

TargetLink logo
  • “Import Result from XTC File” now puts the result into a new AbsIntAnalysisResults element of the function instead of writing to the function’s properties directly.
  • Improved generation of loop-bound annotations for lookup tables.

Workspaces

You can now save the current analysis state, any results computed so far, and all currently open views as a so-called Workspace.

Unlike simply saving a project, this allows you to take snapshots of your progress at any moment in time, revisit them, and build upon them. This is especially useful for documentation and backup purposes.

In the user interface, this new feature is accessible via “Project” → “Save as workspace”.

In batch mode, you can export analysis results as a Workspace via --export-workspace <workspace.apx>. Then all graphs, statistics and any other output produced so far can be immediately accessed in the GUI without having to re-run the analyses first.

Point-and-click annotations

Annotating your project is now easier than ever before. Whether you are looking at a graph, a statistics table, or an AIS file, simply right-click on any area of interest, e.g. a routine or a loop, and select “Add annotation” from the context menu.

Better still, a³ will automatically determine for you any locations that might benefit from being annotated, and mark them with a light bulb in graphs and messages. Clicking on that symbol will bring up the suggested annotation that you can accept or modify with a couple clicks.

The annotation hints are also added to analysis reports.

Improved statistics

  • All-new Statistics view for minimum and maximum loop bounds for all loops globally and for each context.
  • Improved WCET statistics with bar charts for self contributions and cumulative contributions.
  • The infeasibility statistics view now shows if a routine is top-level infeasible, backwards infeasible or just infeasible.
  • In the Graph view, loop statistics and other analysis details are now linked from the context menu of routines and loops.

Other GUI changes

  • Message view colors and fonts have been optimized to highlight warnings, errors, annotations hints and locations.
  • Analysis results are now always output in all available formats. For example, even if you haven’t specified a report file, it will still be created in a temporary directory and can be shown on request.
  • When creating analyses from an information view, a template dialog is now displayed that enables you to customize the generated analyses. In addition, you can now mass-create analyses simply by typing up the list of entry functions in any editor view and using the context menu.
  • When visualization of recursions is enabled (selected in the combo box in the Graph view), any incoming edges into any recursions are now also highlighted in a different color.
  • Register values (e.g., stack pointer) can now be specified using AIS2 expressions.
  • You can now specify an address range where the stack pointer can be placed. This will usually increase analysis precision.
  • Added a progress indicator for reading DWARF debug information.
  • Improved Memory Usage view.
  • Improved configurations management and problem reporting.
  • Macro information from DWARF debug information is now read on-the-fly to reduce memory consumption.
  • Information → Sources now shows DWARF producer information, if available, for the individual source files. This makes it easy to check which compiler is used for which file. Some compilers include the compile options there, too.
  • Improved ORTI project import:
    • now supporting architectures with multiple stacks
    • you can now specify a global AIS file and source file include directories
    • better computation of task entry function names
  • Improved import of configurations with old settings.
  • The option “Size limit for interval sets” has been renamed into “Size limit for value sets”. Old settings will be imported and converted.

AIS2

  • The AIS1 format is now officially deprecated.
    If you need help converting AIS1 annotations to AIS2, contact support@absint.com.
  • New annotation to directly specify call targets and declare that a call is a tail call: 
    instruction <pp> tail calls: ...;
  • The annotations “instruction calls/branches to/returns to” now have an implied instruction class. For example, 
    instruction <pp> calls: ...;
    also changes the instruction type of <pp> to call, just like the annotation 
    instruction <pp> type: call;
    This means that the annotation 
    instruction <pp> {
     calls: ...;
     type: tail call;
}
    can now be simplified to: 
    instruction <pp> tail calls: ...;
  • Initialization values can now be collected for all structure members at once by specifying: 
    collect initialization: ("<name>".);
    where <name> is the name of a structure variable.
  • New AIS2 expression to compute the end address of an address range. Instead of writing: 
    address(<area>) + width(<area>) - 1
    you can now simply write: 
    end(<area>)
  • New AIS2 functor to determine the offset of a structure field in a global structure variable. For example, to determine the offset of a structure field “data” in a global structure variable “fTable”, the following expression can be used: 
    offset(("fTable"."data"));
    This expression is a shorthand for 
    address(("fTable"."data")) - address("fTable");
  • The “collect initialization” annotation has been extended to enable collecting values for specific types, for example:
    • values written into function pointer variables 
      collect initialization: type(function pointer)
    • values written into variables of type "void () *" 
      collect initialization: type("void () *");
    • values written into variables that match a regular expression 
      collect initialization: type("int.*");
  • Improved error reporting in case a pointer dereference operation, e.g., in an annotation to resolve a computed call, fails to read data from memory. For example, consider the annotation 
    instruction "main" -> computed(1) calls: *("b"[]);
    When the AIS2 resolver is unable to read data from memory, it previously reported:
    At address 0x1000380:
    Unable to resolve '("b"[]->)':
    - Unable to read target address from '0x40028b60'.
    Starting with this release, it will also explain why the data cannot be read, and even provide annotation hints when necessary:
    At address 0x1000380:
    Unable to resolve '("b"[]->)':
    - Refusing to read 4 bytes at address 0x40028b60 (variable 'b') from writable section '.sdata' to reconstruct the control flow.
    You may need to annotate branch/call targets in case it is.
    Additionally, you should check whether section is writable.
    Please consider writing an AIS annotation.
    ais2 { area section(".sdata") { readable: true; writable: false; } }
  • Improved handling of calls via trampoline routines: “skip target check” can now be annotated at the original call site instead of the return inside the trampoline routine.
  • Improved handling of interval area contains annotations. Either an unsigned or signed interval fitting into the destination width is allowed. If that constraint is not met, the decoder will issue a warning. Given a 32-bit wide element, feasible annotations are: 
    ais2 { area 0x100C to 0x100F { contains data: 0x1 .. 0xFFFFFFFF; } }
ais2 { area 0x100C to 0x100F { contains data: -123123 .. 1212435; } }
    Out-of-range annotations would be e.g. 
    • ais2 { area 0x100C to 0x100F { contains data: -123123 .. 2147483648; } }
      resulting in
      Ignoring contains data annotation because signed cell value [-123123..2147483648] exceeds cell width of 4 byte.
      The allowed range is [-2147483648..2147483647].
    • ais2 { area 0x100C to 0x100F { contains data: 0x0 .. 0xFF0000000; } }
      resulting in
      Ignoring contains data annotation because unsigned cell value [0..68451041280] exceeds cell width of 4 byte.
      The allowed range is [0..4294967295].
  • Improved performance of program point resolution for match(<regular expression>).

Decoding

  • Improved DWARF debug information extraction and usage, especially for C++ debug information.
  • Now supporting binaries with mixed DWARF1 and DWARF2 line information.
  • Extended DWARF debug information reader to show structure types with flexible array members.
  • Added support for ELF files with more than 65535 program or section headers.
  • Decoder now reports annotated register contents, such as the user stack pointer.
  • The byte order of additional executables (e.g. HEX files for calibration) is now derived from the main executable.
  • The '.text' section is now automatically marked as read-only for Coff binaries.
  • Better heuristic for symbol table reading in Coff binaries to sort out not-needed symbols.
  • Improved stack pointer guessing for GCC.
  • Improved handling of debug line information for binaries with relocations if line info points to the relocated code and not the original location.
  • Improved handling of non-contiguous data sections in IEEE965 reader.
  • Allocated sections without content are marked as writable per default.
  • Empty sections are now discarded.
  • ARM:
    • improved decoding of switch tables via thumb tbb and tbh instructions
    • improved decoding of computed calls and branches
    • improved patterns for computed calls in THUMB mode
    • support for more variants of VFP instructions
    • better TI compiler detection for Coff binaries.
    • improved stack pointer guessing
  • C28x:
    • improved zero overhead loop handling
    • improved stack pointer guessing
  • C33: improved stack pointer guessing.
  • FR81: added support for FeOMF debug information.
  • MPC7448 and 7448s: support for code duplication.
  • PPC:
    • improved decoding of VLE binaries
    • improved call/switch table decoding
  • SuperH: improved decoding of computed calls and branches.
  • TriCore: improved decoding of switch tables.
  • V850:
    • improved decoding of computed call tables
    • improved handling of code factorization optimization of Greenhills compiler
    • improved read/write classification of store instructions
    • added support for full 22-bit offsets in jarl/jr instructions

Stack and value analysis

  • Improved memory usage and analysis speed.
  • Improved precision for:
    • value analysis for computed calls with many infeasible targets
    • sharpening of expressions containing a + b, a - b, a ^ b
    • multiplication and bit extraction instructions
    • multiplication emulated via shift-and-add
    • the relational domain for shifts and multiplications
    • iterative decoding for guarded execution
  • Improved reporting for infeasible control flow transitions. Symbol names for targets and annotations for the instruction in question are now reported, too:
    Warning #3078: In "test.c", line 42:
    In routine 'test', at address 0x110:
    In context '..., 0x020->"test"':
    In "annotations.ais", line 12:
    Detected an infeasible control flow transition.

    Edge (true) from 0x110 to possible targets:
    * [0x0200] (0x200 => 'Test_Function_0')
    * [0x0300] (0x300 => 'Test_Function_1')

    Contradicting computed targets:
    * [0x0400] => 'Test_Function_2'
  • Out-of-bound array accesses detected are marked as infeasible if DWARF is used to restrict memory accesses. The value analyzer will issue a message:
    Info #3118: In "test.c", line 106:
    In routine 'test.L6', at address 0x1310:
    In context '0x1444->"test", 0x1030->"test.L1"[21]':
    The read-access is assumed to access array 'array_test' which conflicts with the computed address [0x003f97fc] (index is [21], but array has only 20 members).
    Marking this path as infeasible.
  • Extended restriction of memory accesses via DWARF debug information to arrays which are struct members.
  • Improved restriction of array accesses with DWARF debug info for architectures with address segmentation.
  • Added support for restricting accesses to arrays with element size of 1 using DWARF debug info.
  • Sharpen the register or memory cell used as index for array access if DWARF is used to restrict memory accesses.
  • Optimized maximum stack analysis path enumeration algorithm.
  • Improved reporting for potential infinite loops, now warning if they have user-annotated loop bounds.
  • Improved simplification for expressions like “((d3 + d4) - d4)”.
  • Improved collection of initializiation data if values are written in steps (triggered by the “collect initialization” annotation).
  • Improved combination of relational information on control flow joins.
  • Improved loop bound detection.
  • Improved heuristic to filter out pseudo loop bounds only detected because of casting small loop counters to larger datatypes.
  • Improved handling of complex loop exit conditions.
  • Improved detection of loop bounds for shift loops.
  • Improved output of computed vs. annotated memory contents clashes:
    Warning #3088: In "test.c", line 128:
    In routine 'schedule', at address 0x114c:
    In context '0x1048->"task", 0x104c->"schedule"':
    Write access to [0x00810000]:4 ('globalVariableName') in constant memory contradicts user annotation.

    Annotated value:
    * [0x00000000]

    Contradicting computed value:
    * [0x00000001]
  • Improved performance of context mapping computation.
  • ARM: improved handling of SP writeback for SRS instructions.
  • C16x: restrict accesses of the form 
    <base> + <index> * <factor>
    to the segment indicated by <base>.
  • MCS51: improved modeling of memory-mapped registers.
  • SuperH: improved stack analysis of external routines.

Cache and pipeline analysis

  • Improved speed and memory consumption.
  • Greatly improved performance for small max-length values.
  • Improved performance and precision for additional starts.
  • Now avoiding unbounded results for additional starts in combination with small max-length values.
  • Removed the option “Enable widening for cache states”.
  • Cortex R4: improved pipeline model.
  • Cortex R5:
    • Improved pipeline model.
    • Return stack now supported in timing analysis.
  • MPC5674F and 5777M(z7): improved handling of memory serialized instructions.
  • PowerPC: improved stability of TimingProfiler analysis for variable instruction length code sequences.
  • e300, MPC755, MPC755s, PPC750: improved cache-hit counter computation for writes into locked memory areas.
  • MPC7448 and 7448s: added code-duplication support.
  • Cortex-R: improved memory map and pipeline model for TimingProfiler.

Reporting

  • The option “Reduce number of identical messages” has been removed in favor of dynamic filtering in the GUI. You can hide duplicates directly in the Messages view, and also unhide them without re-running the analysis.
  • Suppressed messages for each analysis step are now reported via
    • info messages in the GUI:
      Suppressed messages: #3079 (2×), #3082 (4×)
    • report files:
      *** Suppressed messages: #3079 (2×), #3082 (4×)
    • XML report files: 
      <messages>
    <suppressed_message number="3079" suppressions="2" />
    <suppressed_message number="3082" suppressions="4" />
</messages>
  • Text and XML reports now include information on completely infeasible contexts for a routine as an extra column/attribute.
  • Potential reasons for not-computed results of timing analysis are now reported.
  • The a³ XML Result File format has been revised. The structure is more consistent now. The new XML scheme definition file can be found at absint.com/dtd/a3-results-16.10.xsd.

Visualization

  • Faster initial creation of control flow graphs.
  • Improved memory usage.
  • Improved “Go go caller/target” context menu for routines/calls with many callers/targets.