diff mbox

[Ada] Satisfy representation invariants in operation Move

Message ID 20111120114449.GA19607@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Nov. 20, 2011, 11:44 a.m. UTC 
The list container maintains a pair of array index components, First and Last,
to keep track of the first and last nodes of the linked list. For an empty
list, the First and Last values should be 0. Operation Move empties the Source
container as it copies elements from the Source to the Target. However, it did
not set the Last component of the Source list to 0 after all of the elements
had been copied to the Target, thus violating the representation invariant of
the Source container.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-11-20  Matthew Heaney  <heaney@adacore.com>

	* a-cbdlli.adb, a-cfdlli.adb (Move): Set Last component to 0
	for Source list.
diff mbox

Patch

Index: a-cfdlli.adb
===================================================================
--- a-cfdlli.adb	(revision 181528)
+++ a-cfdlli.adb	(working copy)
@@ -1007,16 +1007,65 @@ 
 
       Clear (Target);
 
-      while Source.Length > 0 loop
+      while Source.Length > 1 loop
+
+         pragma Assert (Source.First in 1 .. Source.Capacity);
+         pragma Assert (Source.Last /= Source.First);
+         pragma Assert (N (Source.First).Prev = 0);
+         pragma Assert (N (Source.Last).Next = 0);
+
+         --  Copy first element from Source to Target
+
          X := Source.First;
          Append (Target, N (X).Element);  -- optimize away???
 
+         --  Unlink first node of Source
+
          Source.First := N (X).Next;
          N (Source.First).Prev := 0;
 
          Source.Length := Source.Length - 1;
+
+         --  The representation invariants for Source have been restored. It is
+         --  now safe to free the unlinked node, without fear of corrupting the
+         --  active links of Source.
+
+         --  Note that the algorithm we use here models similar algorithms used
+         --  in the unbounded form of the doubly-linked list container. In that
+         --  case, Free is an instantation of Unchecked_Deallocation, which can
+         --  fail (because PE will be raised if controlled Finalize fails), so
+         --  we must defer the call until the very last step. Here in the
+         --  bounded form, Free merely links the node we have just
+         --  "deallocated" onto a list of inactive nodes, so technically Free
+         --  cannot fail. However, for consistency, we handle Free the same way
+         --  here as we do for the unbounded form, with the pessimistic
+         --  assumption that it can fail.
+
          Free (Source, X);
       end loop;
+
+      if Source.Length = 1 then
+
+         pragma Assert (Source.First in 1 .. Source.Capacity);
+         pragma Assert (Source.Last = Source.First);
+         pragma Assert (N (Source.First).Prev = 0);
+         pragma Assert (N (Source.Last).Next = 0);
+
+         --  Copy element from Source to Target
+
+         X := Source.First;
+         Append (Target, N (X).Element);
+
+         --  Unlink node of Source
+
+         Source.First := 0;
+         Source.Last := 0;
+         Source.Length := 0;
+
+         --  Return the unlinked node to the free store
+
+         Free (Source, X);
+      end if;
    end Move;
 
    ----------
Index: a-cbdlli.adb
===================================================================
--- a-cbdlli.adb	(revision 181528)
+++ a-cbdlli.adb	(working copy)
@@ -1164,18 +1164,67 @@ 
            "attempt to tamper with cursors of Source (list is busy)";
       end if;
 
-      Clear (Target);
+      Clear (Target);  -- checks busy bit of Target
 
-      while Source.Length > 0 loop
+      while Source.Length > 1 loop
+
+         pragma Assert (Source.First in 1 .. Source.Capacity);
+         pragma Assert (Source.Last /= Source.First);
+         pragma Assert (N (Source.First).Prev = 0);
+         pragma Assert (N (Source.Last).Next = 0);
+
+         --  Copy first element from Source to Target
+
          X := Source.First;
          Append (Target, N (X).Element);
 
+         --  Unlink first node of Source
+
          Source.First := N (X).Next;
          N (Source.First).Prev := 0;
 
          Source.Length := Source.Length - 1;
+
+         --  The representation invariants for Source have been restored. It is
+         --  now safe to free the unlinked node, without fear of corrupting the
+         --  active links of Source.
+
+         --  Note that the algorithm we use here models similar algorithms used
+         --  in the unbounded form of the doubly-linked list container. In that
+         --  case, Free is an instantation of Unchecked_Deallocation, which can
+         --  fail (because PE will be raised if controlled Finalize fails), so
+         --  we must defer the call until the very last step. Here in the
+         --  bounded form, Free merely links the node we have just
+         --  "deallocated" onto a list of inactive nodes, so technically Free
+         --  cannot fail. However, for consistency, we handle Free the same way
+         --  here as we do for the unbounded form, with the pessimistic
+         --  assumption that it can fail.
+
          Free (Source, X);
       end loop;
+
+      if Source.Length = 1 then
+
+         pragma Assert (Source.First in 1 .. Source.Capacity);
+         pragma Assert (Source.Last = Source.First);
+         pragma Assert (N (Source.First).Prev = 0);
+         pragma Assert (N (Source.Last).Next = 0);
+
+         --  Copy element from Source to Target
+
+         X := Source.First;
+         Append (Target, N (X).Element);
+
+         --  Unlink node of Source
+
+         Source.First := 0;
+         Source.Last := 0;
+         Source.Length := 0;
+
+         --  Return the unlinked node to the free store
+
+         Free (Source, X);
+      end if;
    end Move;
 
    ----------