CodePeer Find the Bug Challenge
Challenge 4 – Protected objects, tasks and race conditions
Abstract:
This package defines tasks to track friendly and enemy ships, based on a protected type defining a short list of nearby ships. A flag is set when the combat zone becomes crowded, in order to switch to a different combat mode.
Have a look at the following code and see if you can spot the errors. Once you think you’ve got them all, click on the “Go CodePeer” button to see how well you matched up to CodePeer’s comprehensive and rapid analysis of the same code.
Error line 76: “warning: unprotected access of Saturated_Combat_Zone via radar.track_ship’Task_Type_Body”
Here’s how CodePeer came to this conclusion:
CodePeer is warning that global variable Saturated_Combat_Zone is accessed
through task type Track_Ship without proper locking, which makes it possible to
have a race condition when more than one task attempts to write to this global
variable. Indeed, Add_Ship is called twice in Track_Ship on two different
protected objects, Friends and Foes, which makes it possible that a first task
of type Track_Ship calls it on Friends and a second task calls it on Foes, hence
the race condition.
Error line 98: “warning: unprotected access of Saturated_Combat_Zone via radar.track_ship’Task_Type_Body”
Here’s how CodePeer came to this conclusion:
This warning is similar to the one on line 76. Putting both warnings together,
this also reveals a possible race condition between accesses to
Saturated_Combat_Zone in Add_Ship and Remove_Ship.
Error line 100: “medium: range check might fail: requires (Num_Untracked_Ships – 1) >= 0″
Here’s how CodePeer came to this conclusion:
CodePeer detects that Num_Untracked_Ship might be assigned a negative value at
this point, which would violate the constraint that Num_Untracked_Ship is a
Natural. Looking just 3 lines above, we see indeed that Num_Untracked_Ship might
be null at this point, so that the subtraction on line 100 returns -1. The error
is that the statements on lines 97 and 100 are in the wrong order.
Error line 115: “medium: validity check: Index might be uninitialized”
Here’s how CodePeer came to this conclusion:
Index is not initialized on line 105, so it remains uninitialized if the loop
terminates without finding a bigger ship, which would occur for example if no
ships are currently tracked.
package Radar is
type Friend_Or_Foe is (Friend, Foe, Unknown);
type Class_Of_Ship is
(Not_A_Ship, Coastal_Patrol, Fast_Attack_Craft, Corvette, Frigate,
Destroyer, Cruiser, Pocket_Battleship, Battlecruiser, Helicopter_Carrier,
Battleship, Dreadnought, Aircraft_Carrier, Supercarrier);
type Kilometer is new Natural;
-- Every ship detected by the radar is assigned a unique identifier that
-- allows tracking it until it espaces the radar's scope.
type Ship is record
Quality : Friend_Or_Foe := Unknown;
Category : Class_Of_Ship := Not_A_Ship;
Distance : Kilometer := 0;
Unique_ID : Natural := 0;
end record;
function "=" (X, Y : Ship) return Boolean;
type Ship_Array is array (Positive range <>) of Ship;
-- Detect when too many ships are sailing in the combat zone, which makes
-- it very likely to be hit by enemy fire or friendly fire. This triggers
-- a different combat mode where the ship principally attempts to escape
-- the crowded zone.
Saturated_Combat_Zone : Boolean := False;
-- Track ships closer than this distance
Short_Distance : constant Kilometer := 20;
-- Short list of nearest ships that should be dealt with higher priority,
-- whether it is to engage combat for enemies or to agree on maneuvers
-- for friends.
protected type Short_List (Max_Tracked_Ships : Positive) is
-- Add a ship when entering the short range
procedure Add_Ship (E : Ship);
-- Remove a ship when leaving the short range
procedure Remove_Ship (E : Ship);
-- Return the biggest ship in the short range
function Biggest_Ship return Ship;
private
Num_Tracked_Ships : Natural := 0;
Num_Untracked_Ships : Natural := 0;
-- Only tracked ships are included in Ships
Ships : Ship_Array (1 .. Max_Tracked_Ships);
end Short_List;
Friends : Short_List (50); -- 50 friendly ships tracked for maneuvers
Foes : Short_List (18); -- 18 enemy ships tracked (# of weapon systems)
-- Track a ship entering and leaving the short range
task type Track_Ship is
entry New_Ship (E : Ship);
entry Update_Position (Distance : Kilometer);
end Track_Ship;
end Radar;
package body Radar is
function "=" (X, Y : Ship) return Boolean is
begin
return X.Unique_ID = Y.Unique_ID;
end "=";
protected body Short_List is
procedure Add_Ship (E : Ship) is
begin
if Num_Tracked_Ships < Max_Tracked_Ships then
Ships (Num_Tracked_Ships) := E;
Num_Tracked_Ships := Num_Tracked_Ships + 1;
else
Num_Untracked_Ships := Num_Untracked_Ships + 1;
Saturated_Combat_Zone := True;
end if;
end Add_Ship;
procedure Remove_Ship (E : Ship) is
begin
for J in Ships'First .. Num_Tracked_Ships loop
if Ships (J) = E then
-- Ship E was found. First remove it.
for K in J + 1 .. Num_Tracked_Ships loop
Ships (K - 1) := Ships (K);
end loop;
-- Then update the number of tracked ships and return.
Num_Tracked_Ships := Num_Tracked_Ships - 1;
return;
end if;
end loop;
-- Ship E was not found, so it is an untracked ship.
-- Update the number of untracked ships and possibly leave the mode
-- where combat zone is saturated.
if Num_Untracked_Ships = 0 then
Saturated_Combat_Zone := False;
end if;
Num_Untracked_Ships := Num_Untracked_Ships - 1;
end Remove_Ship;
function Biggest_Ship return Ship is
Current : Class_Of_Ship := Not_A_Ship;
Index : Integer;
begin
for J in Ships'First .. Num_Tracked_Ships loop
if Current < Ships (J).Category then
-- Found a bigger ship. Update Current and Index.
Current := Ships (J).Category;
Index := J;
end if;
end loop;
return Ships (Index);
end Biggest_Ship;
end Short_List;
task body Track_Ship is
Current : Ship;
begin
-- Define the ship being tracked.
accept New_Ship (E : Ship)
do
Current := E;
end New_Ship;
loop
-- Following a movement of the ship entering or leaving the short
-- range, add or remove it from the corresponding short list.
accept Update_Position (Distance : Kilometer)
do
Current.Distance := Distance;
if Distance < Short_Distance then
case Current.Quality is
when Friend =>
Friends.Add_Ship (Current);
when Foe =>
Foes.Add_Ship (Current);
when Unknown =>
null;
end case;
else
case Current.Quality is
when Friend =>
Friends.Remove_Ship (Current);
when Foe =>
Foes.Remove_Ship (Current);
when Unknown =>
null;
end case;
end if;
end;
end loop;
end Track_Ship;
end Radar;
See CodePeer in Action!
In this video, AdaCore engineer Yannick Moy walks you through this month’s challenge using CodePeer and GNAT Programming Studio, GNAT Pro IDE.
Anh Vo said:
I think I have found one that avoided CodePeer’s detection :-). The main culprit is at line 72. The first ship added will raise exception. Why? Num_Tracked_Ships is initially set to zero. However, Ships is an array having lower index of 1 (Positive range ). Zero index is out of range.
The solution is to swap line 72 and line 73. That makes first ship will added to index 1. The second one will be at 2 and so on.
Yannick Moy said:
Nice catch Anh! Another example of the infamous off-by-one bug!
In fact, CodePeer cannot “miss” errors, as it will always report a possible error (possibly with a “low” rank) when it cannot prove there is none.
So here CodePeer proved that no error was possible … under the condition that procedure Add_Ship is called in a context which respects the precondition generated by CodePeer. Which says:
— Preconditions:
— _object.num_tracked_ships >= 1
Indeed, if Add_Ship is always called in a context where Num_Tracked_Ships is greater or equal to one, there is no possible error on line 72.
Now, as you noted, the first call to Add_Ship will occur in a context where Num_Tracked_Ships is zero, but CodePeer is not capable of taking this high-level view.
Still, it is my fault if this bug slipped through, as the relevant information was present in the contracts generated by CodePeer. I just did not look at them.
Since the start of this series, I wondered when someone would catch a bug that I did not see, so congrats for being the first one!
Alexis Paluel-Marmont said:
Hi!
I don’t want to be nitpicking, and maybe I am a complete moron. But you tell me.
Looks like Remove_Ship was designed to “remove” only ships that were previously “added” by Add_Ship. What happens if Remove_Ship is called with a Ship that is not being tracked? Well, because no such tracked Ship can be found, the code sequence intended for untracked Ships is executed, even if the number of tracked Ships is not actually maximal – which leads to a Constraint_Error when assigning -1 to Num_Untracked_Ships. No big deal (it was the last statement of the procedure, in the corrected code, so you would not leave a protected object in an inconsistent state) but it might be bugging the caller…
I can hear your objection already: “But this can not happen in our context, because the Ships are exclusively managed by the Track_Ship instances and they always add a ship before removing it.” However, this is a very unsafe assumption…
If I understand well, Update_Position is called *only* every time a ship moves in or moves out of the Short_Distance range. Well, this may work, but makes the implementation of Track_Ship dangerously dependent on such an assumption on the caller of the entry. What if the caller updates the position on every move or detection? What if the Ship is already within Short_Distance when the Radar is activated and then leaves the Short_Distance perimeter afterwards?
In our case,maybe an invariant like “Num_Untracked_Ships > 0 implies Num_tracked_Ships = Max_Tracked_Ships”, or the equivalent “Num_tracked_Ships = Max_Tracked_Ships or Num_Untracked_Ships <= 0" or the like could help.
It would be interesting to be able to define such invariants for entities or code sections in CodePeer, as additional high-level semantic information, even if this cannot be formulated in the source code language (Ada 95 or 2005).
Yannick Moy said:
Hi Alexis,
You are right that proper use of the API of task Track_Ship is necessary for the code to execute without any error. CodePeer detects this possible error and warns about it by generating the following precondition for procedure Remove_Ship, which expresses the constraint that Num_Untracked_Ships should be positive when the execution reaches after the loop:
(soft) _object.num_untracked_ships >= 1
In these small examples, we aim at showing errors and their detection in simple ways, so we make no attempt at guarding against all possible errors. Still, this is a good occasion to show how CodePeer signals the possible error here through a precondition.
The invariant you propose is indeed an intended invariant for proper use of Track_Ship’s API, but it does not guard against the error you reported, as the loop may still end with no ship found when Num_tracked_Ships = Max_Tracked_Ships.
Still, invariants of this kind are indeed a very good way to express rich properties, so that testing or static analysis can check them! So you will be happy to learn that Ada 2012 will define type invariants that will allow you to express a boolean expression serving as predicate for a private type of a package, to be checked at execution at various points (on subprogram parameters, etc.). We expect to also support these type invariants in CodePeer, both to perform more precise analyses and to detect possible violations.