From patchwork Sun Nov 20 11:44:50 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 126649 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) by ozlabs.org (Postfix) with SMTP id 10CBDB7226 for ; Sun, 20 Nov 2011 22:45:10 +1100 (EST) Received: (qmail 14995 invoked by alias); 20 Nov 2011 11:45:07 -0000 Received: (qmail 14983 invoked by uid 22791); 20 Nov 2011 11:45:05 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Sun, 20 Nov 2011 11:44:51 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 2B22D2BB010; Sun, 20 Nov 2011 06:44:50 -0500 (EST) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id Uq0CM0xsgF5u; Sun, 20 Nov 2011 06:44:50 -0500 (EST) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 192DD2BB00B; Sun, 20 Nov 2011 06:44:50 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 0B65E92BF6; Sun, 20 Nov 2011 06:44:50 -0500 (EST) Date: Sun, 20 Nov 2011 06:44:50 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Matthew Heaney Subject: [Ada] Satisfy representation invariants in operation Move Message-ID: <20111120114449.GA19607@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org 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 * a-cbdlli.adb, a-cfdlli.adb (Move): Set Last component to 0 for Source list. 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; ----------