From patchwork Mon May 30 08:32:37 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: 1636821 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: bilbo.ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=VdOZzv7y; dkim-atps=neutral Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Received: from sourceware.org (server2.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by bilbo.ozlabs.org (Postfix) with ESMTPS id 4LBTKk0s65z9s07 for ; Mon, 30 May 2022 18:36:58 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 146563829BCD for ; Mon, 30 May 2022 08:36:56 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 146563829BCD DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1653899816; bh=kMBShpIIgPZUmiZ3UthD0MzRTaHsVJtn7h76EMFX74Q=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=VdOZzv7yc1Fu/E016YjqKVXyHBmSB404X7Rdil2fj68u8JBrf/FKyDHHeP01rLwFL XnZa25vJYUNb0sRim2uLjkTp8IhAGuJysFhh8N8ooFdBHd5v9+0pRgsNa3AuzTZdT4 XL5NcwNt+wsSsvUcSSFQVleaaczRWB0HEicHPDiA= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x436.google.com (mail-wr1-x436.google.com [IPv6:2a00:1450:4864:20::436]) by sourceware.org (Postfix) with ESMTPS id 456EF3814FD3 for ; Mon, 30 May 2022 08:32:39 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 456EF3814FD3 Received: by mail-wr1-x436.google.com with SMTP id p10so13581764wrg.12 for ; Mon, 30 May 2022 01:32:39 -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=kMBShpIIgPZUmiZ3UthD0MzRTaHsVJtn7h76EMFX74Q=; b=030+EG/oSRHGJjRyfRrBXX98VS/zRPWVvszHrK5oXK69jhc7z1spQPREVFENEn2OlX M+pUS849DI+n2nU27xtJfPPstSTjqbyJx7RGj/zmeBEledIRpon4HFt4osgjEVDkDmYI 42y+c/He3s3l11I4Lhq9GoP2SFjeVkzhuQPBjxcpBU0nKJm9SJKEKgP6FVWmtQqPilrx /6NJ0a6Noq6FGwMtc4rGlgFldDpBYg9VX+uKrQFMnpfZkrBBBHA0wLEFxThMqSPy1v7X ndFSXx7uU76Gu1eCK1+JX5jF3OeD6eAOQpmMjRkv/oEiB7r2n/vB+DePz0t/cjyxiqWT WtJg== X-Gm-Message-State: AOAM531ZvCzKBJTOrp3RITLlBKUnjrG7HisryfQIvYJL4adm8LUqwY7J yBL5iE30bmc4xbC+99GbMhgnHkQ6SP4Ycg== X-Google-Smtp-Source: ABdhPJyHSmZQ9PhFpJg7MBek1VR8QXBTrXbEvCLdT6vc5ZdfV/th9zkFMvRytQ6xlYK2Z97OtNrZBg== X-Received: by 2002:a5d:64c2:0:b0:20f:dc21:e658 with SMTP id f2-20020a5d64c2000000b0020fdc21e658mr31890674wri.508.1653899557944; Mon, 30 May 2022 01:32:37 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id t22-20020a05600c41d600b003942a244ebesm9514705wmh.3.2022.05.30.01.32.37 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 30 May 2022 01:32:37 -0700 (PDT) Date: Mon, 30 May 2022 08:32:37 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit Message-ID: <20220530083237.GA210613@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.9 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, 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: Yannick Moy Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" The internal unit System.Generic_Array_Operations defines only generic subprograms. Thus, pragma Assertion_Policy inside the spec has no effect, as each instantiation is only subject to the assertion policy at the program point of the instantiation. Remove this confusing pragma, and add the pragma inside each generic body making use of additional assertions or ghost code, so that running time of instantiations is not impacted by assertions meant for formal verification. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ PR ada/105303 * libgnat/s-gearop.adb: Add pragma Assertion_Policy in generic bodies making use of additional assertions or ghost code. * libgnat/s-gearop.ads: Remove confusing Assertion_Policy. diff --git a/gcc/ada/libgnat/s-gearop.adb b/gcc/ada/libgnat/s-gearop.adb --- a/gcc/ada/libgnat/s-gearop.adb +++ b/gcc/ada/libgnat/s-gearop.adb @@ -32,7 +32,8 @@ -- Preconditions, postconditions, 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. +-- policy to Ignore, here for non-generic code, and inside the generic for +-- generic code. pragma Assertion_Policy (Pre => Ignore, Post => Ignore, @@ -72,6 +73,12 @@ is -------------- function Diagonal (A : Matrix) return Vector is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + N : constant Natural := Natural'Min (A'Length (1), A'Length (2)); begin return R : Vector (A'First (1) .. A'First (1) + (N - 1)) @@ -126,6 +133,11 @@ is --------------------- procedure Back_Substitute (M, N : in out Matrix) is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); pragma Assert (M'First (1) = N'First (1) and then M'Last (1) = N'Last (1)); @@ -215,6 +227,11 @@ is N : in out Matrix; Det : out Scalar) is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); pragma Assert (M'First (1) = N'First (1) and then M'Last (1) = N'Last (1)); @@ -460,6 +477,11 @@ is ------------- function L2_Norm (X : X_Vector) return Result_Real'Base is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); Sum : Result_Real'Base := 0.0; begin @@ -479,6 +501,11 @@ is ---------------------------------- function Matrix_Elementwise_Operation (X : X_Matrix) return Result_Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin return R : Result_Matrix (X'Range (1), X'Range (2)) with Relaxed_Initialization @@ -524,6 +551,11 @@ is (Left : Left_Matrix; Right : Right_Matrix) return Result_Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin return R : Result_Matrix (Left'Range (1), Left'Range (2)) with Relaxed_Initialization @@ -570,6 +602,11 @@ is Y : Y_Matrix; Z : Z_Scalar) return Result_Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin return R : Result_Matrix (X'Range (1), X'Range (2)) with Relaxed_Initialization @@ -657,6 +694,11 @@ is (Left : Left_Matrix; Right : Right_Scalar) return Result_Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin return R : Result_Matrix (Left'Range (1), Left'Range (2)) with Relaxed_Initialization @@ -705,6 +747,11 @@ is (Left : Left_Scalar; Right : Right_Matrix) return Result_Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin return R : Result_Matrix (Right'Range (1), Right'Range (2)) with Relaxed_Initialization @@ -811,6 +858,11 @@ is (Left : Left_Matrix; Right : Right_Matrix) return Result_Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin return R : Result_Matrix (Left'Range (1), Right'Range (2)) with Relaxed_Initialization @@ -856,6 +908,11 @@ is ---------------------------- function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); procedure Ignore (M : Matrix) with @@ -917,6 +974,11 @@ is ---------------------------- function Matrix_Matrix_Solution (A, X : Matrix) return Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); procedure Ignore (M : Matrix) with @@ -1035,6 +1097,11 @@ is (Left : Left_Vector; Right : Right_Vector) return Matrix is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin return R : Matrix (Left'Range, Right'Range) with Relaxed_Initialization @@ -1078,6 +1145,11 @@ is --------------- procedure Transpose (A : Matrix; R : out Matrix) is + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); begin for J in R'Range (1) loop for K in R'Range (2) loop diff --git a/gcc/ada/libgnat/s-gearop.ads b/gcc/ada/libgnat/s-gearop.ads --- a/gcc/ada/libgnat/s-gearop.ads +++ b/gcc/ada/libgnat/s-gearop.ads @@ -36,16 +36,10 @@ -- overflows in arithmetic operations passed on as formal generic subprogram -- parameters. --- 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); +-- Preconditions in this unit are meant mostly for analysis, but will be +-- activated at runtime depending on the assertion policy for preconditions at +-- the program point of instantiation. These preconditions are simply checking +-- bounds, so should not impact running time. package System.Generic_Array_Operations with SPARK_Mode