How GNATkp Safeguards Against Known Compiler Issues

by Fabien Chouteau – Sep 17, 2024

GNAT Pro Assurance customers have access to a special variant of GNATcheck called GNATkp (GNAT Known Problems detector). This tool is packaged with rules designed to detect Ada constructs affected by known problems in compiler releases. Note that GNATkp is an addition to and not a replacement for GNATcheck.

Replacing error-prone manual code inspection with an automatic and systematic verification relevant to specific GNAT Pro versions and targets, GNATkp ensures that your code remains robust and free from potential bugs introduced by known problems. It integrates seamlessly into existing workflows, offering a targeted approach to safeguarding software quality,

Let’s consider one example.

Here is the definition of a data structure that triggers an invalid code generation on GNAT 17 for powerpc targets only:

A record component whose type is a record type with an Unchecked_Union and a representation clause specifying a size that is not a power of two for some of the fields.

As you can see, the triggering condition is very precise, and not easy to spot during code review, while weakening it is liable to introduce many false positives.

Here is a piece of code that matches:

type A (Kind : Boolean := True) is record
     case Kind is
       when True =>
         A1 : Integer;
       when False =>
         A2 : Boolean;
     end case;
   end record
     with Unchecked_Union;
	
   for A use record
     A1 at 0 range 0 .. 31;
     A2 at 0 range 0 .. 12; -- Note the size is not a power of 2
   end record;

    type B is record
       AF : A;
    end record;

Now let’s see how we can use GNATkp to spot the problem.

There are two important switches for GNATkp:

--kp-version: Specify the compiler version used
--target: Specify the target architecture

$ gnatkp --kp-version=17.1 --target=powerpc -P simple.gpr
info: kp_s124_035 enabled
info: kp_s814_034 enabled
info: kp_u727_033 disabled, target does not match
info: kp_v120_015 enabled
main.adb:19:08: possible occurrence of KP V120-015 on powerpc targets

GNATkp lists all the known problems for the given GNAT version. Problems specific to a target architecture are either disabled or enabled depending on the --target switch. Then, for each enabled problem, a rule is checked against the project source code.

Infringing pieces of code will result in a message like this one:

main.adb:19:08: possible occurrence of KP V120-015 on powerpc targets

Under the hood, GNATkp rules, like GNATcheck rules, are written using the LKQL (short for LangKit Query Language). This means you can implement your own rules to detect other forbidden constructs, e.g. related to hardware malfunctions.

GNATkp can be integrated into developers’ workflows, continuous integration systems, or certification processes. In summary, it empowers teams to proactively manage known compiler-related issues. By integrating GNATkp into your development process, you can significantly reduce the chances of encountering costly or hazardous errors in deployed systems.

Posted in #GNATkp

About Fabien Chouteau

Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.