From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-lf1-x12e.google.com (mail-lf1-x12e.google.com [IPv6:2a00:1450:4864:20::12e]) by sourceware.org (Postfix) with ESMTPS id 24E6E3858417 for ; Tue, 7 May 2024 08:00:20 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 24E6E3858417 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 24E6E3858417 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::12e ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1715068825; cv=none; b=nUdx7aw7Q8YkGtd21W8ArdPMOcOw5sRby/jxl1bZGo8V6RvSY327ODy9m615wd0A/pd550ScKSyFV20vZYvvlVdUAlOGmBV0MWMsWcm1tRuQ1H3UjrlcvXj0mJGmgtlyOEf68aRsXMI8/1z5H6iISWRIyMtZZi/EPO/FCx0Qhw4= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1715068825; c=relaxed/simple; bh=bsimrz7orBG0kpIzSgz0m2aHJGZR0enbk/3b2C7UBIA=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=fOg0wi8yYngll6E7C4LQeLN6HI0rgJls8v2F9MXRcjPB2m/TtxlDp/RXKEt5nbRwSgLxJdC1GqDHxgdb9UPbgs8ju7jHhjdEcl9aObsA0K6utdaj8SWMXXC8lpmJt6gJhxpvz48cxiWT2lYaTK59rgGYNm2oUV68FQJYwuRgRkk= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-lf1-x12e.google.com with SMTP id 2adb3069b0e04-51f60817e34so3228891e87.2 for ; Tue, 07 May 2024 01:00:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1715068818; x=1715673618; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=I7fHGuFIXhgaXxMbtVhhtL7K+uDDCg+DiC241Tgd4rU=; b=U8TBF2UbkQuic3AvDWHox1Aqdx7+XRaVmqIwbzbUMGp1kyn0BJJMs9Z3pUhXHSy95Y xG/pzoIV2zViHagCAFcav1vyVmLMMX7punjEHTbRO/GWFkLveDUtToKxFGoQH/hAN7lt 6UgW/3e+M+Xq+0LGmei5M0y1FucSa/+x4EMqLCXmtN/w+oKyJogOaTWxIYT/TKKNDZGM qGktnHNPQOe4oJC/O+SNUs9aqB6zFCRakkV7V83eEpMewDYnLHaDhsTuo8GxF7tsPeoj ujhIBxfeJavKFKOh4J93+c1DxMKp0otUM0Xz/AUEthvPaW9tf5in2ztvv8+Ui4FkbLdX uW5A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1715068818; x=1715673618; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=I7fHGuFIXhgaXxMbtVhhtL7K+uDDCg+DiC241Tgd4rU=; b=n1qxohSu27dn1yEL3iHOQXgUr9LTla6FD+2ccc6OZPxECgS4ADIQHiFLKMwGohvDmz Zh+bo5mLtIeuBfTTMqML/4Az9dBXM6OOvsoMlYCWi8ubfwbsDCrkF4JXZ6UOp2J4jjX8 fo05miPm/110ujuB7X4zAaWxj1J2tL3OS5hwasGlFPIfFBHPD/PravCycGw5FbxENzuS ucwGUKhELhIADUux75rJgPNboHs5MERX7/jwL6DFDCIjZpdUzIwn1bPT4tiC/17FcieO 6LbhdxfL/gX6DytGgBwZGUNxtSKgLNo6vVCl/JT7HN3X8TC/PaZRhA6wzoBCHocxIrJj Fuvw== X-Gm-Message-State: AOJu0YxAT0D1q2Ik0trK0Pq7n+NsTgxpwvOELecCd9YazDTK7Pb5Urxh 3yI9xKfCKl0vjm0rLDOZLkt9J40hFmtHqgX/XhNDMcG05WXjl0Cik+WOG9f1AcmjfsU9FQIaJkM = X-Google-Smtp-Source: AGHT+IFHNcZhOde1evf7sTRXQ/smApRMDiZC1SV7n0Qzjb05twCcmYwMp6IHgAndVd03f0Vctr0yIg== X-Received: by 2002:a05:6512:159a:b0:51e:245a:8ed3 with SMTP id bp26-20020a056512159a00b0051e245a8ed3mr9821480lfb.28.1715068818619; Tue, 07 May 2024 01:00:18 -0700 (PDT) Received: from localhost.localdomain ([2001:861:3382:1a90:11a6:1c9d:5099:b1e8]) by smtp.gmail.com with ESMTPSA id s11-20020a05600c45cb00b00419f572671dsm18679290wmo.20.2024.05.07.01.00.18 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 07 May 2024 01:00:18 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Adapt proof of runtime units Date: Tue, 7 May 2024 10:00:17 +0200 Message-ID: <20240507080017.37354-1-poulhies@adacore.com> X-Mailer: git-send-email 2.43.2 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit 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 List-Id: From: Yannick Moy Restore proof of runtime units after changes in SPARK. gcc/ada/ * libgnat/a-strsea.adb (Index): Add assertions. * libgnat/a-strsup.ads ("="): Remove useless precondition. * libgnat/s-aridou.adb (Prove_Rounding_Case): Add assertions. (Lemma_Shift_Right): Add call to lemma. * libgnat/s-arit32.adb (Prove_Rounding_Case): Add assertion. (Prove_ Signs): Add assertions. (Scaled_Divide32): Add assertions. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-strsea.adb | 2 ++ gcc/ada/libgnat/a-strsup.ads | 1 - gcc/ada/libgnat/s-aridou.adb | 9 +++++++-- gcc/ada/libgnat/s-arit32.adb | 17 +++++++++++++++-- 4 files changed, 24 insertions(+), 5 deletions(-) diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb index 1dad3be4f4a..54f12199fcc 100644 --- a/gcc/ada/libgnat/a-strsea.adb +++ b/gcc/ada/libgnat/a-strsea.adb @@ -623,6 +623,7 @@ package body Ada.Strings.Search with SPARK_Mode is (if (for some J in From .. Source'Last - PL1 => Match (Source, Pattern, Mapping, J)) then Result in From .. Source'Last - PL1 + and then Match (Source, Pattern, Mapping, Result) else Result = 0); else @@ -636,6 +637,7 @@ package body Ada.Strings.Search with SPARK_Mode is (if (for some J in Source'First .. From - PL1 => Match (Source, Pattern, Mapping, J)) then Result in Source'First .. From - PL1 + and then Match (Source, Pattern, Mapping, Result) else Result = 0); end if; diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index cb1dcc9a076..6c360f1982b 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -689,7 +689,6 @@ is (Left : Super_String; Right : Super_String) return Boolean with - Pre => Left.Max_Length = Right.Max_Length, Post => "="'Result = (Super_To_String (Left) = Super_To_String (Right)), Global => null; diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index ac25e6a9183..6f27487db37 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -971,7 +971,7 @@ is procedure Prove_Rounding_Case is begin if Same_Sign (Big (X), Big (Y) * Big (Z)) then - null; + pragma Assert (abs Big_Q = Big (Qu)); end if; end Prove_Rounding_Case; @@ -1603,6 +1603,7 @@ is pragma Loop_Invariant (XX = Shift_Right (X, J)); pragma Loop_Invariant (XX = X / Double_Uns'(2) ** J); end loop; + Lemma_Div_Commutation (X, Double_Uns'(2) ** Shift); end Lemma_Shift_Right; ------------------------------ @@ -2441,7 +2442,11 @@ is procedure Prove_Rounding_Case is begin if Same_Sign (Big (X) * Big (Y), Big (Z)) then - null; + pragma Assert + (abs Big_Q = + (if Ru > (Zu - Double_Uns'(1)) / Double_Uns'(2) + then abs Quot + 1 + else abs Quot)); end if; end Prove_Rounding_Case; diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index 59a6db08199..221ef1e635e 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -415,7 +415,11 @@ is procedure Prove_Rounding_Case is begin if Same_Sign (Big (X) * Big (Y), Big (Z)) then - null; + pragma Assert + (abs Big_Q = + (if Ru > (Zu - Uns32'(1)) / Uns32'(2) + then abs Quot + 1 + else abs Quot)); end if; end Prove_Rounding_Case; @@ -432,7 +436,14 @@ is -- Prove_Signs -- ----------------- - procedure Prove_Signs is null; + procedure Prove_Signs is + begin + if (X >= 0) = (Y >= 0) then + pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q); + else + pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q); + end if; + end Prove_Signs; -- Start of processing for Scaled_Divide32 @@ -483,6 +494,8 @@ is Lemma_Div_Commutation (D, Uns64 (Zu)); Lemma_Rem_Commutation (D, Uns64 (Zu)); + pragma Assert (Uns64 (Qu) = D / Uns64 (Zu)); + pragma Assert (Uns64 (Ru) = D rem Uns64 (Zu)); pragma Assert (Big (Ru) = abs Big_R); pragma Assert (Big (Qu) = abs Quot); pragma Assert (Big (Zu) = Big (Uns32'(abs Z))); -- 2.43.2