From patchwork Thu Aug 1 15:17:37 2024 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 1967849 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@legolas.ozlabs.org Authentication-Results: legolas.ozlabs.org; dkim=pass (2048-bit key; secure) header.d=adacore.com header.i=@adacore.com header.a=rsa-sha256 header.s=google header.b=d2eQi1oQ; dkim-atps=neutral Authentication-Results: legolas.ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=2620:52:3:1:0:246e:9693:128c; helo=server2.sourceware.org; envelope-from=gcc-patches-bounces~incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=patchwork.ozlabs.org) Received: from server2.sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (secp384r1) server-digest SHA384) (No client certificate requested) by legolas.ozlabs.org (Postfix) with ESMTPS id 4WZY5C4TNDz1ybX for ; Fri, 2 Aug 2024 01:38:07 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id CF69E386182A for ; Thu, 1 Aug 2024 15:38:05 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-lj1-x22c.google.com (mail-lj1-x22c.google.com [IPv6:2a00:1450:4864:20::22c]) by sourceware.org (Postfix) with ESMTPS id 33A7E386102B for ; Thu, 1 Aug 2024 15:18:36 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 33A7E386102B Authentication-Results: sourceware.org; dmarc=pass (p=quarantine dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org 33A7E386102B Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::22c ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1722525531; cv=none; b=bmRU9jB7TRtznnqWvSOpQBteujivGracNkf1oqvYxvMcnMC1HqQASjqQLYeOSCDmdNZ0gZ50iMbCQyi4sBYCtTbhO1uRu+pmzNHM1k0KDQZsSqxyGzkull+REd6gbiiWL8wJOUPXdrEWkwgbbgSohgxs5TRIhzLUECOh3qxl9gU= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1722525531; c=relaxed/simple; bh=sB1ev/kznnIZ8dPp2w6f+FbyyjgnvncbQiK0q4tdn/I=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=Wz2KvfVVql2Q+f3s5t9y2kY/4AJl2TazSJGKezM3uTdFzXZfXejz8vuCxJkMCaMTRKirjCvKtr5kWpipE7CMHy53c8i23n+n0Zt5des6E4zDwWkt/DKZBOUOQIq08xumikEJgQftNtCT/3mDIQ/svgRi5wZqOMVe+szFC55PAx4= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-lj1-x22c.google.com with SMTP id 38308e7fff4ca-2ef27bfd15bso93965631fa.2 for ; Thu, 01 Aug 2024 08:18:36 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1722525515; x=1723130315; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=K2at1y8a+bzlT3ZhXVnJnKU//8DgDrof8NZ6DYfrzS8=; b=d2eQi1oQlxgGFoYYAsb0mN8cXr/jX44xOyzBaL2+QXojzNAZB7AsYWYG4Mptt6Pdm9 VpFmwhwM1nkpG0FGC1xKXDZ9SI4f7MFBBcDIjtoeXbuxgXGuPTm9Fn78zepkf+9GSB1w W/++iq0fuhNPz577Wgujq8jqy/TArKI2pvDx09J08CsxkzWTKmsee0JpvVaMXVZFz51V LUq8HcDp+zH0PUG67IywH4jyWk488zXjpmEr2oahFG/UtaQul6Z9GZ8w0r+jGqcW9xSf 2XSXgO79x9D8zeW/jvG3SABcwVISThgI5qJgQCn/PLW65KTFY1xi5rNiU8dZz3BpN7mM EwMg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1722525515; x=1723130315; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=K2at1y8a+bzlT3ZhXVnJnKU//8DgDrof8NZ6DYfrzS8=; b=w/zu0/BEEb1aL9wzFD7UeHzAz/xzS9snJ5+qrPAMzI2jofCEdRBzw9R4JJJcLgzCOY RlG6xerGGsn51jJxC2vxNfEb9nMnvEjm/5wDRQUjFrxDTfLIn/iGVoCPR06hPPV7cOgh IZ/QZ8EbiJBgnF2z3kFpxHDBwvpuFaEEWQE6JK9h0d8P7KDIjL2Wgsi1Sabw8AJNxNB8 INdGx6LZxyVcPu7B6HFNYfslDudtGOEhABX6yPdus9oSPNDi+ikVzVj1TC+ojghpwMY/ 3DlzlfY4urCDsQzxudUws8k9BbcBeXv3iHBhVu30dQ8iJ6qVdAkxqsCAjRQ5CFs28iO3 O1Lg== X-Gm-Message-State: AOJu0YzNZHcBc7Z+8Vnm65n8vnUM/YnV95CMABsg/IAH1EwPMUX3qOl4 FyTe9PIjyehMMI/rgXt/pTCqYS2EFVh9k2bJt60AUS2BUx1K3e2mOwAy9ompcuY3RI/t55r67fk nog== X-Google-Smtp-Source: AGHT+IFt9cC5vQTg6sHr0HjlXHK5D5MSHrcpiQJiSY7i45cqVmkgJ1M9+uqLnxh8XLaz32+XNA0UHA== X-Received: by 2002:a2e:2e0f:0:b0:2ef:18b7:440b with SMTP id 38308e7fff4ca-2f15aa916f0mr4787181fa.12.1722525514418; Thu, 01 Aug 2024 08:18:34 -0700 (PDT) Received: from localhost.localdomain ([2001:861:3382:1a90:b6aa:4751:9ea1:da1e]) by smtp.gmail.com with ESMTPSA id ffacd0b85a97d-36b36857fdesm20065995f8f.75.2024.08.01.08.18.33 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 01 Aug 2024 08:18:33 -0700 (PDT) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED 29/30] ada: Update contracts on Strings libraries Date: Thu, 1 Aug 2024 17:17:37 +0200 Message-ID: <20240801151738.400796-29-poulhies@adacore.com> X-Mailer: git-send-email 2.45.2 In-Reply-To: <20240801151738.400796-1-poulhies@adacore.com> References: <20240801151738.400796-1-poulhies@adacore.com> MIME-Version: 1.0 X-Spam-Status: No, score=-13.7 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces~incoming=patchwork.ozlabs.org@gcc.gnu.org From: Yannick Moy The contracts of Ada.Strings.Bounded.To_String and Ada.Strings.Fixed.Delete are updated to reflect the standard spec and to allow proof of callers. gcc/ada/ * libgnat/a-strbou.ads (To_String): Add a postcondition to state the value of bounds of the returned string, which helps with proof of callers. * libgnat/a-strfix.adb (Delete): Fix implementation to produce correct result in all cases. For example, returned string should always have a lower bound of 1, which was not respected in one case. This was not detected by proof, since this code was dead according to the too strict precondition. * libgnat/a-strfix.ads (Delete): State the correct precondition from standard which allows a value of Through beyond the last valid index, and also restricts values of From from below. Update the Contract_Cases accordingly to allow new values of parameters. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-strbou.ads | 3 +++ gcc/ada/libgnat/a-strfix.adb | 33 ++++++++++++--------------------- gcc/ada/libgnat/a-strfix.ads | 20 ++++++++++++-------- 3 files changed, 27 insertions(+), 29 deletions(-) diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index 827c0dc7448..a4830e56b78 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -127,6 +127,9 @@ is -- * If Drop=Error, then Strings.Length_Error is propagated. function To_String (Source : Bounded_String) return String with + Post => + To_String'Result'First = 1 + and then To_String'Result'Length = Length (Source), Global => null; -- To_String returns the String value with lower bound 1 -- represented by Source. If B is a Bounded_String, then diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb index 901fd60284b..2da5367985b 100644 --- a/gcc/ada/libgnat/a-strfix.adb +++ b/gcc/ada/libgnat/a-strfix.adb @@ -266,36 +266,27 @@ package body Ada.Strings.Fixed with SPARK_Mode is return Result_Type (Source); end; - elsif From not in Source'Range - or else Through > Source'Last - then - pragma Annotate - (CodePeer, False_Positive, - "test always false", "self fullfilling prophecy"); - - -- In most cases this raises an exception, but the case of deleting - -- a null string at the end of the current one is a special-case, and - -- reflects the equivalence with Replace_String (RM A.4.3 (86/3)). - - if From = Source'Last + 1 and then From = Through then - return Source; - else - raise Index_Error; - end if; - else declare - Front : constant Integer := From - Source'First; + Front_Len : constant Integer := + Integer'Max (0, From - Source'First); + -- Length of prefix of Source copied to result + Back_Len : constant Integer := + Integer'Max (0, Source'Last - Through); + -- Length of suffix of Source copied to result + + Result_Length : constant Integer := Front_Len + Back_Len; + -- Length of result begin - return Result : String (1 .. Source'Length - (Through - From + 1)) + return Result : String (1 .. Result_Length) with Relaxed_Initialization do - Result (1 .. Front) := + Result (1 .. Front_Len) := Source (Source'First .. From - 1); if Through < Source'Last then - Result (Front + 1 .. Result'Last) := + Result (Front_Len + 1 .. Result'Last) := Source (Through + 1 .. Source'Last); end if; end return; diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index 9d5e9d92341..aed0851493b 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -1061,9 +1061,9 @@ is From : Positive; Through : Natural) return String with - Pre => (if From <= Through - then (From in Source'Range - and then Through <= Source'Last)), + Pre => From > Through + or else (From - 1 <= Source'Last + and then Through >= Source'First - 1), -- Lower bound of the returned string is 1 @@ -1079,12 +1079,14 @@ is -- Length of the returned string - Delete'Result'Length = Source'Length - (Through - From + 1) + Delete'Result'Length = + Integer'Max (0, From - Source'First) + + Integer'Max (Source'Last - Through, 0) -- Elements before From are preserved and then - Delete'Result (1 .. From - Source'First) + Delete'Result (1 .. Integer'Max (0, From - Source'First)) = Source (Source'First .. From - 1) -- If there are remaining characters after Through, they are @@ -1092,9 +1094,11 @@ is and then (if Through < Source'Last - then Delete'Result - (From - Source'First + 1 .. Delete'Result'Last) - = Source (Through + 1 .. Source'Last)), + then + Delete'Result + (Integer'Max (0, From - Source'First) + 1 + .. Delete'Result'Last) + = Source (Through + 1 .. Source'Last)), -- Otherwise, the returned string is Source with lower bound 1