AdaControl is a powerful Ada source code verification tool. It's freely available here. As a side note, its name sounds like "flight control" and it is no coincidence 😊.
Our HAC (HAC Ada Compiler) project is a good opportunity to use AdaControl from scratch on a given project and to show you how capable it is.
***
A note about installation. The free version of AdaControl works so far with the GNAT Ada toolset called Community Edition 2019 - not later, for reasons explained in a newsgroup post titled "Status of AdaControl".
So, for example on Windows, the installation steps include installing GNAT CE 2019 (even if you use a later version), writing a script, say, go19.cmd, with the line "path c:\gnat\2019\bin;%path%". The AdaControl installer (adactl-1.21r6b-exe_setup.exe) will work correctly if you first set the correct temporary path with "go19", then launch the installer, from the same command line session.
Then, you can write a second script, say, gps_19.cmd, with the lines:
call go19
start gps -P hac.gpr
That way you can start your AdaControl session comfortably through GNAT Studio by just double-clicking gps_19.cmd.
***
AdaControl works with rules that you can choose to apply (or not), sometimes with sub-rules. You list the rules you want to apply in a text file. In the HAC project (see hac.gpr) we have called it "test/verif_hac.aru".
Let's start with a first rule which seems promising: "simplifiable_statements". As you know, unnecessary complications are the biggest threat to programs of any size. Small simplifications that are automatically detected are very welcome. Of course it doesn't replace larger, conceptual simplifications - but for that, you need a brain 😉.
------------------------------------------------
-- AdaControl verification rules --
-- https://www.adalog.fr/en/adacontrol.html --
------------------------------------------------
-- Set for HAC (HAC Ada Compiler).
--------------------------------------
-- (1) Required ("check" command) --
--------------------------------------
check simplifiable_statements;
------------------------------------------------------------------
-- (2) Acceptable, but should be looked at ("search" command) --
------------------------------------------------------------------
All but one line of the above rules file are comments starting with "--". But since AdaControl provides 579+ possible rules and sub-rules, the comments will be useful later.
So, we courageously begin with the first rule, on the main procedure of the HAC command-line compiler and VM interpreter, hac.adb (that GNAT turns into hac.exe).
 |
| Click to enlarge |
After a few seconds, AdaControl completes with 74 diagnostics in 18 files (it scans recursively all units that the initial unit (hac.adb) depends on, and the units those units depend on, and so on).
That, for the "simplifiable_statements" rule only. Ouch! 😨
|
| Click to enlarge |
The first item is a loop that is simplifiable into a "for" loop. First, a disclaimer: I did not write that loop👐🚿. Remember that HAC stems from an automatic translation of SmallAda (written in the late 1980's), itself a derivation of CoPascal, which derives from Pascal-S by Pr. Wirth himself around 1975. At the time some languages did not produce a check to skip a "for" loop from a to b when a > b. If it is not skipped, the loop parameter will be incremented to "the infinity", and practically, towards an overflow error in best cases. So probably authors of SmallAda or earlier felt better using a "while" loop instead of a "for" loop in such cases.
In Ada every situation is defined in the Reference Manual (an ISO standard!), and programmers can count on the fact that the loop "for i in a .. b" is skipped if a > b.
Back to AdaControl. Obviously, it has found a case where you can simplify a "while" loop into a "for" loop.
This finding looks easy, a posteriori, for the human reader, because it is a tiny loop. But it is not trivial. Logically, AdaControl was able to figure out that the "OC'Last" part of the exit condition is invariant during the loop's activity (if not, you must stick with the "while" loop). Clever!
Plus, it has seen that the exit condition was equivalent to an upper bound check in a "for" loop. Very clever!
Plus, it has detected simple increment (LC0 := LC0 + 1;) in the main execution path of the loop - and nothing else, nowhere else, like, for instance, a modification of LC0 in the "if" statement. That's very, very clever!
So let's do the recommended simplification. The loop in
procedure Patch_Addresses (
OC : in out Object_Code_Table;
dummy_address : Operand_2_Type
)
is
LC0 : Integer := OC'First;
use Defs;
use type HAC_Integer;
begin
while LC0 < OC'Last loop
if OC (LC0).F in Jump_Opcode and then OC (LC0).Y = dummy_address then
OC (LC0).Y := HAC_Integer (OC'Last);
end if;
LC0 := LC0 + 1;
end loop;
end Patch_Addresses;
becomes:
for LC0 in OC'First .. OC'Last - 1 loop
if OC (LC0).F in Jump_Opcode and then OC (LC0).Y = dummy_address then
OC (LC0).Y := HAC_Integer (OC'Last);
end if;
end loop;
As a bonus, the variable declaration, "LC0 : Integer := OC'First;", can be deleted (it is implicitely defined in Ada for the "for" loop).
But the simplification is not enough for AdaControl! It detects, on a second round, that the loop parameter (LC0) is always used as an index to an array. It says that the "for ... of" Ada 2012 statement can be used instead. This means that instead of having a loop incrementing an index to the OC array, the loop could as well scan OC's elements directly. The job is the same, but the Ada code is shorter and cleaner for human readers. In this case the gain is small, but for an array like "foo(k).bar.x3.grogu(l)" it makes a big difference in readability.
Let's apply again the recommanded change.
for Op of OC (OC'First .. OC'Last - 1) loop
if Op.F in Jump_Opcode and then Op.Y = dummy_address then
Op.Y := HAC_Integer (OC'Last);
end if;
end loop;
Beautiful!
Here are both changes together, in colour, via GitHub:
More AdaControl adventures in a further post...
Login
