AbsInt Angewandte Informatik GmbH

CompCert is a formally verified optimizing C compiler. Its intended use is the compilation of safety-critical and mission-critical software written in C and meeting high levels of assurance. It accepts ISO C99 programs and produces machine code for PowerPC (32-bit/64-bit hybrid), ARM, IA32 (x86 32-bit), AMD64 (x86 64-bit), and RISC-V.

What sets CompCert apart?

Unlike any other production compiler, CompCert is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. In other words, the code it produces is proved to behave exactly as specified by the semantics of the source C program.

This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance.

The formal proof covers all transformations from the abstract syntax tree to the generated assembly code. To preprocess and produce object and executable files, an external C preprocessor, assemblers, linkers, and C libraries have to be used.  However, these unverified stages are well-understood and robust from an implementation perspective, hence they can be covered well by traditional qualification kits. The reliability of CompCert has been demonstrated on a development version of CompCert by a 2011 study by Regehr, Yang et al.:

“The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.”

Your benefits

• Using the CompCert C compiler is a natural complement to applying formal verification techniques (static analysis, program proof, model checking) at the source-code level. The correctness proof of CompCert guarantees that all safety properties verified on the source code automatically hold for the generated code as well.

• On typical embedded processors, the code generated by CompCert typically runs twice as fast as the code generated by GCC without optimizations, and only 20% slower than GCC at optimization level 3. (Details about the benchmark mix used to obtain these numbers are available on request.)

• Costs for finding and avoiding or fixing compiler bugs and shipping patches to the customers of the embedded system can be avoided.

Stack overflow is now a thing of the past.

StackAnalyzer automatically determines the worst-case stack usage of the tasks in your appli­cation. The analysis results are shown as annotations in the call graph and control flow graph.

Features
 

• Detailed and precise information on both user stack and system stack usage by application tasks
• Stack analysis for all hierarchy levels: routines, basic blocks, assembly instructions
• Freely selectable entry points for the analysis
• Immediate recognition of critical program sections thanks to customizable color coding (see screenshots)

Why do you need StackAnalyzer?

Stack memory has to be allocated statically by the programmer. Underestimating stack usage can lead to serious runtime errors which can be difficult to find. Overestimating stack usage means a waste of memory resources.

• StackAnalyzer provides automatic tool support to calculate the stack usage of your application. The analysis results are valid for all inputs and each task execution.
• StackAnalyzer not only reduces development effort but also helps to prevent runtime errors due to stack overflow.
• The analysis results provide valuable feedback in optimizing the stack usage of your application.

AbsInt offers two static analyzers to check coding guidelines and find programming defects at the C code level: RuleChecker and Astrée.

Astrée

Astrée is a sound static analyzer designed to prove the absence of runtime errors and further critical program defects. It is based on abstract interpretation – a provably correct formal method. If no errors are reported, this is a guarantee that there are no errors from the class of errors under investigation. Astrée does not require the program under analysis to be instrumented, executed, or stimulated by test cases. The tool can be used on handwritten code, automatically generated code, or by any combination thereof. Open interfaces and full batch mode execution make Astrée ideally suited to be used in continuous verification frameworks. Tool couplings, e.g., to dSPACE TargetLink, are available that provide a seamless integration in existing development environments. By using its Qualification Support Kit and AbsInt’s Qualification Software Life Cycle Data Reports, Astrée can be automatically qualified according to all contemporary safety norms (e.g., ISO 26262 or DO-178B/C).

Astrée reports program defects caused by unspecified and undefined behaviors according to the C norm (ISO/IEC 9899:1999 (E)), program defects caused by invalid concurrent behavior, violations of user-specified programming guidelines, and computes program properties relevant for functional safety.

Users are notified about:

• integer/floating-point division by zero
• out-of-bounds array indexing
• erroneous pointer manipulation and dereferencing (null, uninitialized, and dangling pointers)
• data races (read/write or write/write concurrent accesses by two threads to the same memory location without proper mutex locking)
• inconsistent locking (lock/unlock problems)
• invalid calls to operating system services (e.g. OSEK-calls to TerminateTask() on a task with unreleased resources)
• integer and floating-point arithmetic overflows
• read accesses to uninitialized variables
• unreachable code
• violations of optional user-defined assertions to prove additional runtime properties
• non-terminating loops

Astrée includes RuleChecker to report violations of coding rules and to compute code metric thresholds (MISRA C:2004, MISRA C:2012, HIS metrics, …).

RuleChecker

Safety-critical software has to be developed according to coding guidelines to ensure high-quality code, and to reduce the risk of programming errors and security vulnerabilities.

RuleChecker is a static analyzer designed to check coding guidelines and compute code metrics for safety-critical C programs. RuleChecker is fast and easy to use. Multiple result views and graphical visualizations enable an efficient result exploration.

RuleChecker supports:

- MISRA C:2004
- MISRA C:2012 incl. Amendment 1
- MISRA C++:2008
- ISO/IEC TS 17961:2013
- SEI CERT Secure C
- MITRE Common Weakness Enumeration (CWE).

RuleChecker can be coupled with the sound static analyzer Astrée to guarantee zero false negatives and minimal false positives on semantical rules.

RuleChecker is fully batch-mode compatible and can be used in continuous integration frameworks. Open formats enable the analysis results to be automatically processed. A Jenkins plugin is available.

RuleChecker can be automatically qualified according to all relevant safety norms, including ISO-26262, DO-178B/C, IEC-61508, EN-50128, etc.

In real-time systems, timely task completion is of the essence. Each real-time task has to be completed within a specified time frame in order to ensure that the system works correctly. In other words, it is essential that the worst-case execution time (WCET) of each task is known.

AbsInt provides three different tools for WCET analysis which are tailored to three different use cases. All of them support batch mode execution and integration in continuous integration frameworks.

aiT WCET Analyzer - Static WCET Guarantees

aiT statically computes tight upper bounds for the worst-case execution time of tasks on timing-predictable single-core and multicore processors. aiT directly analyzes binary executables and takes the intrinsic cache and pipeline behavior into account.

aiT is based on the technique of abstract interpretation, a formal methodology for semantics-based static analysis, which can provide soundness guarantees: the WCET bounds will never be exceeded by any possible program execution.

A graphical user interface supports the visualization of the worst-case program path and the interactive inspection of all pipeline and cache states at arbitrary program points.

aiT is available for a variety of microprocessors ranging from simple processors like ARM7 to complex superscalar processors like Freescale MPC755, or MPC7448, and multicore processors like Freescale MPC 5777M, and Infineon AURIX TC27x.

TimeWeaver - Non-Intrusive Hybrid WCET Analysis

TimeWeaver combines static path analysis with real-time instruction-level tracing to provide worst-case execution time estimates. The computed time bounds provide valuable feedback for assessing system safety and for optimizing worst-case performance. It supports many modern high-performance processors, e.g. all PowerPC boards providing Nexus program trace messages (IEEE-ISTO 5001, class 2 or higher), or ARM using cycle-accurate ETM traces.

TimeWeaver analyses all potential execution paths and computes the longest path based on the execution times of trace segments observed in real-time traces. The trace information covers interference effects, e.g., by accesses to shared resources from different cores, without being distorted by probe effects since no instrumentation code is needed. The computed time bounds are compliant to requirements of safety standards like ISO-26262.

The analysis results include the computed WCET bound with the time-critical path, and information about the trace coverage obtained. They provide valuable feedback for optimizing trace coverage, for assessing system safety, and for optimizing worst-case performance.

TimingProfiler - Zero-Overhead WCET Estimation in Early Design Stages

TimingProfiler helps developers identify application parts that are causing unsatisfactory execution times. It is ideally suited for constantly monitoring timing behavior during software development and in model-based development environments. TimingProfiler delivers results as soon as there is compiled code. It can be used early in the process when measurements on physical hardware are costly or not even possible. The analysis is purely static. No access to physical hardware and no code instrumentation are required.

TimingProfiler takes executable code as input and explores the timing of all potential execution paths of each task on a generic processor with the target instruction set, e.g. PowerPC. No user interaction is required; information not statically available is filled in by specialized heuristics. Hence, the resulting execution time is a realistic worst-case scenario, albeit not a guarantee as provided by aiT.

TimingProfiler gives detailed information about the execution time and time-critical paths. The tool shows call and control flow graphs, and displays all relevant information about the executable. Hotspots and bottlenecks can be identified at early development stages so that late-stage integration problems can be avoided.