CodePeer 19 Release Notes

We present here a few highlights of the new features in CodePeer 19. You can access the complete list here.

New Web Interface

CodePeer comes with a completely redesigned web interface that uses state-of-the-art web technology. It provides real-time updating of message filters and manual reviews, among other new capabilities. This new interface can be generated via the new -html and -html-only switches. The old HTML interface is kept temporarily to help with the transition, and remains available via the -html-output switch.

_images/web_interface_1.jpg _images/web_interface_2.jpg

Libadalang Checkers

CodePeer now integrates a collection of lightweight checkers based on Libadalang. These checkers complement CodePeer’s traditional analysis. They are much faster and typically lead to fewer false positives.

Each checker performs a specialized analysis, aimed at detecting a very specific bug or suspicious code pattern. Some of those checkers provide analyses that are similar to (some parts of) CodePeer’s main analysis (such as null_dereference or test_always_true). These checkers are much faster than the main analysis but focus on specific kinds of errors and are likely to miss many errors detected by CodePeer’s more general analysis. The benefit of this feature is to allow much faster analysis with fewer false positive messages.

Other checkers look for common mistakes. Among those, the checker bad_unequal only looks for tests of the form “X /= A or X /= B” and emits a message indicating test always true:

 1function Always (X : Integer) return Integer is
 2   procedure Compute with Import;
 3begin
 4   if X /= 0 or X /= 1 then --  Always True
 5      Compute;
 6
 7      return 1;
 8   end if;
 9
10   return 0;
11end Always;

With the code above CodePeer outputs:

always.adb:4:17: medium warning: test always true (LAL checker): expression always true: 'X' /= 0 or 1

As another example, the checker duplicate_branches looks for branching expressions (if-then-else or case expressions) that contain syntactically equivalent branches:

 1   function Dup (X : Integer) return Integer is
 2   begin
 3      if X > 0 then
 4         declare
 5            A : Integer := X;
 6            B : Integer := A + 1;
 7            C : Integer := B + 1;
 8            D : Integer := C + 1;
 9         begin
10            return D;
11         end;
12      else
13         declare
14            A : Integer := X;
15            B : Integer := A + 1;
16            C : Integer := B + 1;
17            D : Integer := C + 1;
18         begin
19            return D;  -- Suspicious duplicated code
20         end;
21      end if;
22   end Dup;

For which CodePeer will flag:

dup.adb:13:7: medium warning: code duplicated (LAL checker): code duplicated with line 4

These new analyses are either run in parallel with CodePeer’s traditional analysis (at levels 1 to 4) or alone (at level 0).

You can get more information on these checkers with the switch --lal-checkers-help. You can also look at the two blog posts, Going After the Low Hanging Bug and (Many) More Low Hanging Bugs, that describe the work at the heart of the new Libadalang checkers.

New Entry Level and Simple Project Setup

In order to provide a smoother initial experience to users, and offer gradual added capabilities, level 0 is now the default analysis level (compared to level 3 previously), and is Libalang checkers only. Hence, if you launch CodePeer on a new project without specifying a level you will get a fast analysis with very few false positives.

In addition, level 0 comes with the new Simple Project setup: CodePeer now provides a very simple project file setup where you only need to provide a list of source directories and optionally a list of filename patterns to get initial results. In particular, the project does not need to be compilable at this level. This capability is enabled via a new switch --simple-project. Higher levels still require a complete setup of your project file (.gpr).

Security Report

You can use CodePeer to perform a security-oriented analysis and generate a separate report, taking advantage in particular of its CWE support, with the switch --security-report.

This report is tailored for security engineers. It is aimed at non-Ada experts and focuses on security objectives.

The report is generated as an HTML page that you can either use as is, or convert to e.g. PDF, and include in a larger report as part of your security assessment:

_images/security_report.jpg

Documentation Updates

We reorganized the CodePeer User’s Guide. In particular we documented many cases of user workflow in the new section CodePeer Workflows. And we improved the documentation of the messages issued by CodePeer by adding examples for each category of message. You can find them in the section Messages and Annotations.

GNATcheck Integration

Following the integration of warnings from GNAT in CodePeer 18, we now also integrate the coding-standard checker GNATcheck into CodePeer. As a result, CodePeer can automatically launch GNATcheck, collect its messages, add them into its database, and report them as for any other CodePeer message. In particular, this allows you to compare the last GNATchek run with a baseline run and review the messages, similarly to what you can do with any CodePeer message.

GPS Client/Server

A Client/Server interface to CodePeer is now provided as part of the GPS IDE. This new mode allows users to manually access and review the messages of a CodePeer analysis from a remote workstation.

Improved Display of Backtraces

The backtrace information associated with precondition messages is now available directly in the Locations view for easier access. The previously available Backtraces view has been removed. In addition, a new preference has been introduced to enable/disable this extra information.

_images/backtraces.jpg

Detailed Timing Information

The analysis time for each file is now displayed in CodePeer’s default output, making it easier to identify which units CodePeer is spending the most time on, and possibly allowing users to fine-tune the analysis or exclude files from analysis when speed matters more than completeness of results:

analyzed admin.scil in 1.21 seconds
analyzed msgproc__body.scil in 0.09 seconds
analyzed msgproc.scil in 0.00 seconds
analyzed cryptotypes.scil in 6.02 seconds

Other Noteworthy Features

Ability to show only new messages

A new switch -show-added is provided to highlight messages that are new compared to the baseline run, via the [added] marker, for easy retrieval. To use this switch on a project, say prj, use the command:

codepeer -Pprj -output-msg-only -show-added

The output would then be something like:

file1.adb:16:10: [added] low: access check might fail: requires Ptr /= null
file2.adb:8:10: medium warning: loop does not complete normally
file2.adb:28:19: low: overflow check might fail: requires BP <= Integer_32'Last-1
file2.adb:29:21: [added] medium: array index check might fail: requires (BP-1) <= (Buf.all'Last)
file3.adb:24:9: [added] high: validity check: X is uninitialized here
file3.adb:61:4: medium warning: unused assignment into Y

Ability to compare any two runs

It is now possible to perform comparison between two arbitrary runs, in text and CSV mode, with the new switch -current. As an example, in combination with the new switch -show-added and the switch -cutoff, you can display the new messages in, say, run 4 of prj with the following command:

codepeer -Pprj -output-msg-only -current 4 -cutoff 3 -show-added

This might display something like:

file1.adb:16:10: [added] low: access check might fail: requires Ptr /= null
file2.adb:8:10: medium warning: loop does not complete normally
file2.adb:28:19: low: overflow check might fail: requires BP <= Integer_32'Last-1
file2.adb:29:21: medium: array index check might fail: requires (BP-1) <= (Buf.all'Last)
file3.adb:61:4: medium warning: unused assignment into Y

Filter messages via switches

The new switch --be-messages=[...] allows users to specify a set of message kinds, and directs CodePeer to only emit and save a message when its kind is part of the specified message kinds. You can then launch a new run on prj and decide to filter out all warning messages and validity checks with the command:

codepeer -Pprj -output-msg -show-added --be-messages=-warnings,-validity_check

This would display:

file1.adb:16:10: [added] low: access check might fail: requires Ptr /= null
file2.adb:28:19: low: overflow check might fail: requires BP <= Integer_32'Last-1
file2.adb:29:21: [added] medium: array index check might fail: requires (BP-1) <= (Buf.all'Last)

Reproducible successive runs

To terminate the analysis of complex subprograms, CodePeer formerly used timeouts. The problem with a timeout is that it does not ensure reproducibility of results. To address this, CodePeer now uses a notion of steps. While analyzing a subprogram, CodePeer deterministically increments a counter. If the counter exceeds a default or specified limit, CodePeer terminates analysis of the subprogram and continues analyzing the rest of the source code.

Performing reviews via a CSV file

The codepeer_bridge --import-reviews switch now supports importing a CSV file (in addition to an XML file) to allow manual review of messages via a spreadsheet.

New partitioning algorithm

We improved the algorithm that computes partitions for the analysis of large projects. The new algorithm increases the number of cases where the units containing a caller and its callee are assigned to the same partition. This also increases the number of subprogram calls that CodePeer can precisely analyze when partitions are involved.