a³ Release 16.10 ---------------- General ------- ● 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: https://www.microsoft.com/en-US/download/details.aspx?id=48145 In an upcoming release, the a³ installer will be updated to include this package. ● A free plugin is now available for automatic integration of a³ in Jenkins, the leading open-source automation server: https://wiki.jenkins-ci.org/display/JENKINS/AbsInt+a%C2%B3+Plugin ● 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 also covers regulations for medical devices, in particular the FDA Principles of Software Validation. ● The Safety Manual now describes qualified tool workflows for a³ and Astrée. 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 --------------------------- ●"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 or a statistics table, simply right-click on a routine or loop and select "Add annotation" from the context menu. You will then be taken straight to the AIS file, with the selected annotation already typed out for you. Now simply fill in the values as desired, and you're done. Likewise, in the AIS editor itself you can now use "Insert AIS annotation" from the context menu to add further annotations, rather than typing everything by hand. Annotation hints ---------------- a³ now automatically determines any locations that might benefit from being annotated, and marks them for you with a light bulb in graphs and messages. Clicking on that symbol will bring up the suggested annotation, and another click will add it to your AIS file. The annotation hints are also included in analysis reports for documentation purposes. Below are some examples of messages with annotation hints. Placeholders enclosed in angle brackets are highlighted in the GUI and can be double-clicked on to enter values of your choosing. ● Missing call targets: exec2crl: Info #1027: In "error.c", line 41: In routine 'os_ErrorHook', at address 0x180138c: Unresolved computed call in routine os_ErrorHook. Annotation hint: ais2 { instruction "os_ErrorHook" -> computed(1) { calls: <targets>; } } ● Missing loop bounds: Info: In routine 'main.L3', at address 0x1001b4: Loop 'main.L3' is unbounded. Annotation hint: ais2 { loop "main.L3" { bound: 0 .. <int>; } } ● Missing incarnation bounds: Warning #3097: In "fibfac.c", line 1: In routine 'fac', at address 0x180029c: For routine 'fac' the default incarnation limit of 1 is used. Please verify that this is correct. The recursion details are: 0: main 1: fac -> 2: fac -> 3: fac Annotation hint: ais2 { routine "fac" { incarnation limit: 1; } } 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. ○ The memory usage is now broken down by category. ○ You can now toggle the view between overall usage and that of the current analysis. ● 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. ● Support ELF files with more than 65535 program or section headers. ● Decoder now reports annotated register contents, such as the user stack pointer. ● Derive byte order of additional executables (e.g. HEX files for calibration) from 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 ○ allow 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 GHS 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. ● Improve 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 "Enable widening for cache states" option. ● 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 "Reduce number of identical messages" option was removed in favor of dynamic filtering in the GUI. You can hide duplicates directly in the Messages view, but will now be able to 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 calls/routines with many targets/callers. ------------------------------------------------------------------------------ Last modified on 14 October 2016 by alex@absint.com. Copyright 2016 AbsInt. ------------------------------------------------------------------------------ An HTML version of these release notes is available at www.absint.com/releasenotes/a3/16.10