From patchwork Thu Jun 2 09:08:43 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: 54712 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 64F3F3955610 for ; Thu, 2 Jun 2022 09:09:20 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 64F3F3955610 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1654160960; bh=3gWmvLse+S5kn0HVoT014AGF+qVFHIejvR8iHWNc3oM=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=AN4RWLZhshBTXm03j2xdQHfeCs8q0OP3kGlAVnFoaOIOfmZBses6BuqnMTdEg0PXV 5na3yd2fJ+NdVConr2US7mX9IkaqMGlGFYHBGGwlngfIRiYIib10WCqomhEgluW6qO vq8B4X5pVOBuHrB5TtSZYheg8RnqwCgH+nwtVETM= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-ej1-x636.google.com (mail-ej1-x636.google.com [IPv6:2a00:1450:4864:20::636]) by sourceware.org (Postfix) with ESMTPS id 95D993954C4A for ; Thu, 2 Jun 2022 09:08:45 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 95D993954C4A Received: by mail-ej1-x636.google.com with SMTP id n10so8721612ejk.5 for ; Thu, 02 Jun 2022 02:08:45 -0700 (PDT) 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=3gWmvLse+S5kn0HVoT014AGF+qVFHIejvR8iHWNc3oM=; b=iWO9Z0nhOk0qNdKF7ZCidZrsOV+FNK3MTlzkH89O8l0IlMYn4r5aAYOYGDiU8SbxwL WryyIHEgO7p65L9ya5Yn/fAPTQHZuYZLNLVGsLPA6h98/aRF4TsqcdcR8xQRiijpykCw o1ug5GU/+cCQSAHt600QZH+wcPLx2H29L1mglzf/MOCR2tVvv4ab3PM0Cz2Yn2fidl8T nXyH6sbvhnKMLFwmDF9dPItXRGJqp2Q/pG1F3fHlhk/74YmmtBt5kK+iIr/X/ViaHLpL XwUVOCvag5jGaZFB0TcK3ZT1VpE9seYwVJb3TB3ILD2RjgTLhgVZfIZxvmJm9tiqBuJO R86A== X-Gm-Message-State: AOAM5309hIAatisSULf2jIUvr9RCzzL5PvDoAc8lxVdPt45BzZpOQ2Z5 gn3SFrPfVJxQXsjz7Ezg1RdX6988vXmQCg== X-Google-Smtp-Source: ABdhPJy94c54EFbs/VqG63P200V4ILsONpOLaEEWacPRUmcyu/dAv+6dVnXoqxl9GDUQwIcASXgjLA== X-Received: by 2002:a17:907:3e1b:b0:6fe:e1a4:a331 with SMTP id hp27-20020a1709073e1b00b006fee1a4a331mr3292252ejc.72.1654160924327; Thu, 02 Jun 2022 02:08:44 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id q9-20020aa7cc09000000b0042dcd6f9994sm2168254edt.9.2022.06.02.02.08.43 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 02 Jun 2022 02:08:43 -0700 (PDT) Date: Thu, 2 Jun 2022 09:08:43 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Add contracts to Interfaces.C.Strings Message-ID: <20220602090843.GA1010457@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, T_SCC_BODY_TEXT_LINE 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.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: Joffrey Huguet Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" This patch adds Global contracts and preconditions to subprograms of Interfaces.C.Strings. Effects on allocated memory are modelled through an abstract state, C_Memory. The preconditions protect against Dereference_Error, but not Storage_Error (which is not handled by SPARK). This patch also disables the use of To_Chars_Ptr, which creates an alias between an ownership pointer and the abstract state, and the use of Free, in SPARK code. Thus, memory leaks will happen if the user creates the Chars_Ptr using New_Char_Array and New_String. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/i-cstrin.ads (To_Chars_Ptr): Add SPARK_Mode => Off. (Free): Likewise. (New_Char_Array): Add global contracts and Volatile attribute. (New_String): Likewise. (Value, Strlen, Update): Add global contracts and preconditions. * libgnat/i-cstrin.adb: Add SPARK_Mode => Off to the package body. diff --git a/gcc/ada/libgnat/i-cstrin.adb b/gcc/ada/libgnat/i-cstrin.adb --- a/gcc/ada/libgnat/i-cstrin.adb +++ b/gcc/ada/libgnat/i-cstrin.adb @@ -34,7 +34,9 @@ with System.Storage_Elements; use System.Storage_Elements; with Ada.Unchecked_Conversion; -package body Interfaces.C.Strings is +package body Interfaces.C.Strings with + SPARK_Mode => Off +is -- Note that the type chars_ptr has a pragma No_Strict_Aliasing in the -- spec, to prevent any assumptions about aliasing for values of this type, diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads --- a/gcc/ada/libgnat/i-cstrin.ads +++ b/gcc/ada/libgnat/i-cstrin.ads @@ -33,7 +33,18 @@ -- -- ------------------------------------------------------------------------------ -package Interfaces.C.Strings is +-- 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. These preconditions +-- do not protect against Storage_Error. + +pragma Assertion_Policy (Pre => Ignore); + +package Interfaces.C.Strings with + SPARK_Mode => On, + Abstract_State => (C_Memory), + Initializes => (C_Memory) +is pragma Preelaborate; type char_array_access is access all char_array; @@ -53,47 +64,75 @@ package Interfaces.C.Strings is function To_Chars_Ptr (Item : char_array_access; - Nul_Check : Boolean := False) return chars_ptr; - - function New_Char_Array (Chars : char_array) return chars_ptr; - - function New_String (Str : String) return chars_ptr; - - procedure Free (Item : in out chars_ptr); + Nul_Check : Boolean := False) return chars_ptr + with + SPARK_Mode => Off; + + function New_Char_Array (Chars : char_array) return chars_ptr with + Volatile_Function, + Post => New_Char_Array'Result /= Null_Ptr, + Global => (Input => C_Memory); + + function New_String (Str : String) return chars_ptr with + Volatile_Function, + Post => New_String'Result /= Null_Ptr, + Global => (Input => C_Memory); + + procedure Free (Item : in out chars_ptr) with + SPARK_Mode => Off; -- When deallocation is prohibited (eg: cert runtimes) this routine -- will raise Program_Error Dereference_Error : exception; - function Value (Item : chars_ptr) return char_array; + function Value (Item : chars_ptr) return char_array with + Pre => Item /= Null_Ptr, + Global => (Input => C_Memory); function Value (Item : chars_ptr; - Length : size_t) return char_array; + Length : size_t) return char_array + with + Pre => Item /= Null_Ptr, + Global => (Input => C_Memory); - function Value (Item : chars_ptr) return String; + function Value (Item : chars_ptr) return String with + Pre => Item /= Null_Ptr, + Global => (Input => C_Memory); function Value (Item : chars_ptr; - Length : size_t) return String; + Length : size_t) return String + with + Pre => Item /= Null_Ptr, + Global => (Input => C_Memory); - function Strlen (Item : chars_ptr) return size_t; + function Strlen (Item : chars_ptr) return size_t with + Pre => Item /= Null_Ptr, + Global => (Input => C_Memory); procedure Update (Item : chars_ptr; Offset : size_t; Chars : char_array; - Check : Boolean := True); + Check : Boolean := True) + with + Pre => Item /= Null_Ptr, + Global => (In_Out => C_Memory); procedure Update (Item : chars_ptr; Offset : size_t; Str : String; - Check : Boolean := True); + Check : Boolean := True) + with + Pre => Item /= Null_Ptr, + Global => (In_Out => C_Memory); Update_Error : exception; private + pragma SPARK_Mode (Off); type chars_ptr is access all Character; for chars_ptr'Size use System.Parameters.ptr_bits;