From patchwork Tue Jan 11 13:32:14 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 49852 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id DE7DD38A9406 for ; Tue, 11 Jan 2022 13:53:13 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org DE7DD38A9406 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1641909193; bh=g/miDOITORdq4kGCX5xkKzl2PfkdEiDQmEtyx+r6c54=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=BhsvmalO1c9MUJRoq7qKTVv13OKY/CH75s7DuOaQIR1rI8tiQjUJo+8aijVhiZy7R I6694UF/U/v5ng04+NfjvqE90yKMBDQAyPt90GeqjlWud6KYdJ42SSMC8EC5LW77PF Nijk1cUsXfxeZ0GBtpU/8Rp6SpQ2mHMs+SK2YwOA= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x330.google.com (mail-wm1-x330.google.com [IPv6:2a00:1450:4864:20::330]) by sourceware.org (Postfix) with ESMTPS id D6CCD38A942C for ; Tue, 11 Jan 2022 13:32:16 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org D6CCD38A942C Received: by mail-wm1-x330.google.com with SMTP id q141-20020a1ca793000000b00347b48dfb53so1848702wme.0 for ; Tue, 11 Jan 2022 05:32:16 -0800 (PST) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=g/miDOITORdq4kGCX5xkKzl2PfkdEiDQmEtyx+r6c54=; b=AxZlymH1U9lLb1jYcTxLxHBsZBsrZ0thspzHKMlIZZCwDT+f1LTovTvt/kGi7EVt7l kjNpyLj3asvL1iegrC4jTsWq42YNiDlUw2it69/D4Me3QD0PoYxMzW66rNTzZ0tmKAu2 HuBqv7YyNtQZT+DnZhHCIf0raVIGcSi6QJjwmiIouzmM72l7x43aN3Wigamyg5Z+Sogg GvMJQHUeAZgvFyzb2FUZR7FZYFsYYQe7NxJpw8KUTBIp4dEddsxRaFWnvg1cdWqgmFCk +sJVbt4nd8Mh6wJWk8r/S2oavhwqRVqD1i/ECSNyWKJOexoPc6ZTruunSu2ueAtniVYm ldaw== X-Gm-Message-State: AOAM530aylUooh8+BkLQEXNo0ykC3STkqdGCPDKrwhGE7eB6TzE5wEMB 39ZINhrbvWHd+9p6mUiDzLhQahYG4lWBJA== X-Google-Smtp-Source: ABdhPJyC1CH5WmL8lIMuxrV6ty8x8Y49ErOC4pTwGly8OBR26Ej2YC9EiYoRT0q+N84gDPrvFvwXpQ== X-Received: by 2002:a05:600c:2f97:: with SMTP id t23mr2538752wmn.85.1641907935986; Tue, 11 Jan 2022 05:32:15 -0800 (PST) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id bh26sm2389539wmb.3.2022.01.11.05.32.15 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 11 Jan 2022 05:32:15 -0800 (PST) Date: Tue, 11 Jan 2022 13:32:14 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Proof of unit System.Case_Util Message-ID: <20220111133214.GA748696@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.2 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.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" This unit is needed to prove System.Val_Bool, as it is used in System.Val_Util called from System.Val_Bool. Add contracts that reflect the implementation, as we don't want these units to depend on units under Ada.Characters. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-casuti.adb: Add ghost code. * libgnat/s-casuti.ads: Add contracts. diff --git a/gcc/ada/libgnat/s-casuti.adb b/gcc/ada/libgnat/s-casuti.adb --- a/gcc/ada/libgnat/s-casuti.adb +++ b/gcc/ada/libgnat/s-casuti.adb @@ -29,8 +29,17 @@ -- -- ------------------------------------------------------------------------------ -package body System.Case_Util is +-- Ghost code, loop invariants and assertions in this unit are meant for +-- analysis only, not for run-time checking, as it would be too costly +-- otherwise. This is enforced by setting the assertion policy to Ignore. +pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + +package body System.Case_Util + with SPARK_Mode +is -------------- -- To_Lower -- -------------- @@ -53,6 +62,9 @@ package body System.Case_Util is begin for J in A'Range loop A (J) := To_Lower (A (J)); + + pragma Loop_Invariant + (for all K in A'First .. J => A (K) = To_Lower (A'Loop_Entry (K))); end loop; end To_Lower; @@ -78,6 +90,15 @@ package body System.Case_Util is A (J) := To_Lower (A (J)); end if; + pragma Loop_Invariant + (for all K in A'First .. J => + (if K = A'First + or else A'Loop_Entry (K - 1) = '_' + then + A (K) = To_Upper (A'Loop_Entry (K)) + else + A (K) = To_Lower (A'Loop_Entry (K)))); + Ucase := A (J) = '_'; end loop; end To_Mixed; @@ -111,6 +132,9 @@ package body System.Case_Util is begin for J in A'Range loop A (J) := To_Upper (A (J)); + + pragma Loop_Invariant + (for all K in A'First .. J => A (K) = To_Upper (A'Loop_Entry (K))); end loop; end To_Upper; diff --git a/gcc/ada/libgnat/s-casuti.ads b/gcc/ada/libgnat/s-casuti.ads --- a/gcc/ada/libgnat/s-casuti.ads +++ b/gcc/ada/libgnat/s-casuti.ads @@ -34,29 +34,98 @@ -- This package provides simple casing functions that do not require the -- overhead of the full casing tables found in Ada.Characters.Handling. -package System.Case_Util is - pragma Pure; +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); + +package System.Case_Util + with Pure, SPARK_Mode +is -- Note: all the following functions handle the full Latin-1 set - function To_Upper (A : Character) return Character; + function To_Upper (A : Character) return Character + with + Post => (declare + A_Val : constant Natural := Character'Pos (A); + begin + (if A in 'a' .. 'z' + or else A_Val in 16#E0# .. 16#F6# + or else A_Val in 16#F8# .. 16#FE# + then + To_Upper'Result = Character'Val (A_Val - 16#20#) + else + To_Upper'Result = A)); -- Converts A to upper case if it is a lower case letter, otherwise -- returns the input argument unchanged. - procedure To_Upper (A : in out String); - function To_Upper (A : String) return String; + procedure To_Upper (A : in out String) + with + Post => (for all J in A'Range => A (J) = To_Upper (A'Old (J))); + + function To_Upper (A : String) return String + with + Post => To_Upper'Result'First = A'First + and then To_Upper'Result'Last = A'Last + and then (for all J in A'Range => + To_Upper'Result (J) = To_Upper (A (J))); -- Folds all characters of string A to upper case - function To_Lower (A : Character) return Character; + function To_Lower (A : Character) return Character + with + Post => (declare + A_Val : constant Natural := Character'Pos (A); + begin + (if A in 'A' .. 'Z' + or else A_Val in 16#C0# .. 16#D6# + or else A_Val in 16#D8# .. 16#DE# + then + To_Lower'Result = Character'Val (A_Val + 16#20#) + else + To_Lower'Result = A)); -- Converts A to lower case if it is an upper case letter, otherwise -- returns the input argument unchanged. - procedure To_Lower (A : in out String); - function To_Lower (A : String) return String; + procedure To_Lower (A : in out String) + with + Post => (for all J in A'Range => A (J) = To_Lower (A'Old (J))); + + function To_Lower (A : String) return String + with + Post => To_Lower'Result'First = A'First + and then To_Lower'Result'Last = A'Last + and then (for all J in A'Range => + To_Lower'Result (J) = To_Lower (A (J))); -- Folds all characters of string A to lower case - procedure To_Mixed (A : in out String); - function To_Mixed (A : String) return String; + procedure To_Mixed (A : in out String) + with + Post => + (for all J in A'Range => + (if J = A'First + or else A'Old (J - 1) = '_' + then + A (J) = To_Upper (A'Old (J)) + else + A (J) = To_Lower (A'Old (J)))); + + function To_Mixed (A : String) return String + with + Post => To_Mixed'Result'First = A'First + and then To_Mixed'Result'Last = A'Last + and then (for all J in A'Range => + (if J = A'First + or else A (J - 1) = '_' + then + To_Mixed'Result (J) = To_Upper (A (J)) + else + To_Mixed'Result (J) = To_Lower (A (J)))); -- Converts A to mixed case (i.e. lower case, except for initial -- character and any character after an underscore, which are -- converted to upper case.