How Do We Use CodePeer at AdaCore
by Arnaud Charlet –
A question that our users sometimes ask us is "do you use CodePeer at AdaCore and if so, how?". The answer is yes! and this blog post will hopefully give you some insights into how we are doing it for our own needs.
First, I should note that at AdaCore we are in a special situation since we are both developing lots of Ada code, and at the same time we are also developing and evolving CodePeer itself. One of the consequences is that using CodePeer on our own code has actually two purposes: one is to improve the quality of our code by using an advanced static analyzer, and the other is to eat our own dog food and improve the analyzer itself by finding limitations, sub-optimal usage, etc...
In the past few years, we've gradually added automated runs of CodePeer on many of our Ada code base, in addition to the systematic use of light static analysis performed by the compiler: GNAT already provides many useful built-in checks such as all the static Ada legality rules, as well as many clever warnings fine tuned over the past 25 years and available via the -gnatwa compiler switch and coupled with -gnatwe that transforms warnings into errors, not mentioning also the built-in style checks available via the -gnaty switch.
GNAT
For GNAT sources (Ada front-end and runtime source code) given that this is a large and complex piece of Ada code (compilers do come with a high level of algorithmic complexity and code recursion!) and that we wanted to favor rapid and regular feedback, we've settled on running CodePeer at level 1 with some extra fine tuning: we've found that some categories of messages didn't generate any extra value for the kind of code found in GNAT, so we've disabled these categories via the --be-messages switch. We've also excluded some files from analysis which were taking a long time compared to other files, for little benefits, via the Excluded_Source_Files project attribute as explained in the Partial Analysis section of the User's Guide.
Given that the default build mechanism of GNAT is based on Makefiles, we've written a separate project file for performing the CodePeer analysis, coupled with a separate simple Makefile that performs the necessary setup phase (automatic generation of some source files in the case of GNAT sources).
After this fine tuning, CodePeer generated a few dozen useful messages that we analyzed and allowed us to fix potential issues, as well as improve the general quality of the code. You'll find a few examples below. The most useful findings on the GNAT code base are related to redundant or dead code and potential access to uninitialized variables when complex conditions are involved, which is often the case in a compiler! CodePeer also detected useful cases of code cleanups in particular related to wrong parameter modes: in out parameters that should be out or in, out parameters that should be in out.
Once we've addressed these findings by improving the source code, we ended up in a nice situation where the CodePeer run was completely clean: no new messages found. So we've decided on a strict policy similar to our no warning policy: no CodePeer messages should be left alone moving forward. To ensure that, we've put in place a continuous run that triggers after each commit in the GNAT repository and reports back its findings within half an hour.
One of the most useful categories of potential issues found by CodePeer in our case is related to not always initializing a variable before using it (what CodePeer calls validity checks). For example in gnatchop.adb we had the following code:
Offset_FD : File_Descriptor;
[...]
exception
when Failure | Types.Terminate_Program =>
Close (Offset_FD);
[...]CodePeer detected that at line 6 Offset_FD may not have been initialized (precisely because an exception may have been raised before assigning Offset_FD. We fixed this potential issue by explicitly assigning a default value and testing for it:
Offset_FD : File_Descriptor := Invalid_FD;
[...]
exception
when Failure | Types.Terminate_Program =>
if Offset_FD /= Invalid_FD then
Close (Offset_FD);
end if;
[...]CodePeer also helped detect suspicious or dead code that should not have been there in the first place. Here is an example of code smell that CodePeer detected in the file get_scos.adb:
procedure Skip_EOL is
C : Character;
begin
loop
Skipc;
C := Nextc;
exit when C /= LF and then C /= CR;
if C = ' ' then
Skip_Spaces;
C := Nextc;
exit when C /= LF and then C /= CR;
end if;
end loop;
end Skip_EOL;in the code above, CodePeer complained that the test at line 9 is always false because C is either LF or CR. And indeed, if you look closely at line 7, when the code goes past this line, then C will always be either CR or LF, and therefore cannot be a space character. The code was simplified into:
procedure Skip_EOL is
C : Character;
begin
loop
Skipc;
C := Nextc;
exit when C /= LF and then C /= CR;
end loop;
end Skip_EOL;GPS
Analysis of GPS sources with CodePeer is used at AdaCore both for improving the code quality and also to test our integration with the SonarQube tool via our GNATdashboard integration.
For GPS, we are using CodePeer in two modes: one mode where developers can manually run CodePeer on their local set up at level 0. This mode runs in about 3 to 5 minutes to analyze all the GPS sources and runs the first level of checks provided by CodePeer, which is a very useful complement to the compiler warnings and style checks and allows to stay 100% clean of messages after an initial set of code cleanups.
In addition, an automated run is performed nightly on a server using level 1, further tuned in a similar way to what we did for GNAT. Here we have some remaining messages under analysis and we use SonarQube to track and analyze these messages.
Here is an example of code that looked suspicious in GPS sources:
View : constant Registers_View := Get_Or_Create_View (...);
begin
View.Locked := True;
if View /= null then
[...]
end if;CodePeer complained at line 5 that the test is always True since View cannot be null at this point. Why? Because at line 3 we are already dereferencing View, so CodePeer knows that after this point either an exception was raised or, if not, View cannot be null anymore.
In this case, we've replaced the test by an explicit assertion since it appears that Get_Or_Create_View can never return null:
View : constant Registers_View := Get_Or_Create_View (...);
begin
pragma Assert (View /= null);
View.Locked := True;
[...]Run Time Certification
As part of a certification project of one of our embedded runtimes for a bare metal target, we ran CodePeer at its highest level (4) in order to detect all potentially cases of a number of vulnerabilities and in particular: validity checks, divide by zero, overflow checks, as well as confirming that the runtime did not contain dead code or unused assignments. CodePeer was run manually and then all messages produced were reviewed and justified, as part of our certification work.
GNAT LLVM
As part of the GNAT LLVM project (more details on this project if you're curious in a future post!) in its early stages, we ran CodePeer manually on all the GNAT LLVM sources - excluding the sources common to GNAT, already analyzed separately - initially at level 1 and then at level 3, and we concentrated on analyzing all (and only) the potential uninitialized variables (validity checks). In this case we use the same project file used to build GNAT LLVM itself and added the CodePeer settings which basically looked like:
package CodePeer is
for Switches use ("-level", "3", "--be-messages=validity_check", "--no-lal-checkers");
for Excluded_Source_Dirs use ("gnat_src", "obj");
end CodePeer;which allowed us to perform a number of code cleanups and review more closely the code pointed by CodePeer.
CodePeer
Last but not least, we also run CodePeer on its own code base! For CodePeer given that this is another large and complex piece of Ada code and we wanted to favor rapid and regular feedback, we've settled on a setting similar to GNAT: level 1 with some extra fine tuning via --be-messages. We also added a few pragma Annotate to both justify some messages - pragma Annotate (CodePeer, False_Positive) - as well as skipping analysis of some subprograms or files where CodePeer was taking too long to analyze, for little benefits (via either the Excluded_Source_Files project attribute or pragma Annotate (CodePeer, Skip_Analysis)).
A CodePeer run is triggered after each change in the repository in a continuous builder and made available to the team within 30 minutes. We've found that in this case the most interesting messages where: validity checks on local variables and out parameters, test always true/false, duplicated code and potential wrong parameter mode.
We also run CodePeer on other code bases in a similar fashion, such as analysis of the SPARK tool sources.
As part of integrating CodePeer in our daily work, we also took the opportunity to improve the documentation and describe many possible workflows corresponding to the various needs of teams wanting to analyze Ada code, with an explanation on how to put these various scenarios in place, check Chapter 5 of the User's Guide if you're curious.
What about you? Do not hesitate to tell us how you are using CodePeer and what are the most useful benefits you are getting by commenting below.
About Arnaud Charlet
Arnaud Charlet is the lead of Product Engineering at AdaCore and is also coordinating the development of the GNAT front-end. In addition, he has recently led the design and implementation effort on the GNAT CCG and GNAT LLVM technologies. Arnaud previously worked on the implementation of the GNAT tasking runtime, GNAT Programming Studio and CodePeer, both as a software engineer and as product manager.