From patchwork Tue May 23 08:09:04 2023 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: 1784967 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@legolas.ozlabs.org Authentication-Results: legolas.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=) Authentication-Results: legolas.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=EZMHzqTP; dkim-atps=neutral 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 ECDSA (P-384) server-digest SHA384) (No client certificate requested) by legolas.ozlabs.org (Postfix) with ESMTPS id 4QQRzd3xyNz20Pr for ; Tue, 23 May 2023 18:18:53 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id EE8B13857835 for ; Tue, 23 May 2023 08:18:50 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org EE8B13857835 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1684829931; bh=0jAvnVDOrQRQeb3suCsTbpEL8SXXZTm5uLdx8kr6wzI=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=EZMHzqTPAKd3SSG1gKWCbiR/x81A+d9vNy9OSCCNdQkQ8otG1aJZbUNOI2T55vvFb EgLOS0+IILGjIexcl8oOTIeBIxCj3ttKMFigVIeT0p/TaoP79xLGhJsPeoWhQ1Ayf4 uIfX6jmkc1MsLbbXNEUpVvYM3oA8Aj0etKGDm3OA= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x331.google.com (mail-wm1-x331.google.com [IPv6:2a00:1450:4864:20::331]) by sourceware.org (Postfix) with ESMTPS id B39EC3839DCD for ; Tue, 23 May 2023 08:09:05 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org B39EC3839DCD Received: by mail-wm1-x331.google.com with SMTP id 5b1f17b1804b1-3f6042d60b5so21233285e9.2 for ; Tue, 23 May 2023 01:09:05 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684829345; x=1687421345; 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=0jAvnVDOrQRQeb3suCsTbpEL8SXXZTm5uLdx8kr6wzI=; b=UMlKo9KyNqQ37uCEnssin8kkcOyZvywClZacAFsJL/IP+PyEPbTKs880wLdant7QL3 SFm59lJJ/gWf/bI3xi9ca+pNRMbpkqU1kdtW6r+HqtVZVcyNSGRamBPsYypYZB2dwWiQ YBc/4cfY36Jo7sp6f+PFuVY0EZRCGu0NTNefARjd/+wAsaEyZf/1ZNeB+DEXXkig86ZL XaTYLVgrlMjjNBiRP4sDl6OkoEEDq+yNnRYAgjW8VReCcbpk0GltkAAN89ABlLMPu5t5 ZgqHQdbWYNv0g8Fi6xc74W1NpvejsTEOIegGDJkZ0cnsnGyCn3gGsEHBBCbt6+Dlo17/ s0xw== X-Gm-Message-State: AC+VfDy7rccsV/pVDdDHKHWgAmxnz231mIpoHfgf8JHFJv+93s3ggp6c Qfu/QUsdwaOOjwuSaiweKT2sp7tDOj/LKQOc5dQRfA== X-Google-Smtp-Source: ACHHUZ44RbR88yGRx05O/F4/rBca+u3+DnB/Tfrf7Xy3+EtKoWaJ8efceABeZP4+Wnf35IqPvHrmJA== X-Received: by 2002:a7b:cd01:0:b0:3f4:2174:b29d with SMTP id f1-20020a7bcd01000000b003f42174b29dmr9597464wmj.1.1684829345314; Tue, 23 May 2023 01:09:05 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id 18-20020a05600c229200b003f42d8dd7d1sm14234050wmf.7.2023.05.23.01.09.04 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 23 May 2023 01:09:04 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Claire Dross Subject: [COMMITTED] ada: Update ghost code for proof of integer input functions Date: Tue, 23 May 2023 10:09:04 +0200 Message-Id: <20230523080904.1874544-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.6 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: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" From: Claire Dross Introduce new ghost helper functions to facilitate proof. gcc/ada/ * libgnat/s-valueu.adb (Scan_Raw_Unsigned): Use new helpers. * libgnat/s-vauspe.ads (Raw_Unsigned_Starts_As_Based_Ghost, Raw_Unsigned_Is_Based_Ghost): New ghost helper functions. (Is_Raw_Unsigned_Format_Ghost, Scan_Split_No_Overflow_Ghost, Scan_Split_Value_Ghost, Raw_Unsigned_Last_Ghost): Use new helpers. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/s-valueu.adb | 10 ++---- gcc/ada/libgnat/s-vauspe.ads | 63 ++++++++++++++++++++++-------------- 2 files changed, 41 insertions(+), 32 deletions(-) diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index 062ad33b1e9..9c77caa3bcb 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -140,10 +140,7 @@ package body System.Value_U is Spec.Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init) with Ghost; Starts_As_Based : constant Boolean := - Last_Num_Init < Max - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + Spec.Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Max) with Ghost; Last_Num_Based : constant Integer := (if Starts_As_Based @@ -151,9 +148,8 @@ package body System.Value_U is else Last_Num_Init) with Ghost; Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < Max - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1) + Spec.Raw_Unsigned_Is_Based_Ghost + (Str, Last_Num_Init, Last_Num_Based, Max) with Ghost; Based_Val : constant Spec.Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads index 117769d20cb..960ad8ec486 100644 --- a/gcc/ada/libgnat/s-vauspe.ads +++ b/gcc/ada/libgnat/s-vauspe.ads @@ -279,24 +279,50 @@ is Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base)); -- Normal case: exponentiation without overflows + function Raw_Unsigned_Starts_As_Based_Ghost + (Str : String; + Last_Num_Init, To : Integer) + return Boolean + is + (Last_Num_Init < To - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Str (Last_Num_Init + 2) in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F') + with Ghost, + Pre => Last_Num_Init in Str'Range + and then To in Str'Range; + -- Return True if Str starts as a based number + + function Raw_Unsigned_Is_Based_Ghost + (Str : String; + Last_Num_Init : Integer; + Last_Num_Based : Integer; + To : Integer) + return Boolean + is + (Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To) + and then Last_Num_Based < To + and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)) + with Ghost, + Pre => Last_Num_Init in Str'Range + and then Last_Num_Based in Last_Num_Init .. Str'Last + and then To in Str'Range; + -- Return True if Str is a based number + function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is (Is_Natural_Format_Ghost (Str) and then (declare Last_Num_Init : constant Integer := Last_Number_Ghost (Str); Starts_As_Based : constant Boolean := - Last_Num_Init < Str'Last - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Str'Last); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) else Last_Num_Init); Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < Str'Last - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Raw_Unsigned_Is_Based_Ghost + (Str, Last_Num_Init, Last_Num_Based, Str'Last); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); begin @@ -330,10 +356,7 @@ is Init_Val : constant Uns_Option := Scan_Based_Number_Ghost (Str, From, Last_Num_Init); Starts_As_Based : constant Boolean := - Last_Num_Init < To - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) @@ -378,18 +401,13 @@ is Init_Val : constant Uns_Option := Scan_Based_Number_Ghost (Str, From, Last_Num_Init); Starts_As_Based : constant Boolean := - Last_Num_Init < To - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) else Last_Num_Init); Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < To - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To); Based_Val : constant Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow then Scan_Based_Number_Ghost @@ -468,18 +486,13 @@ is Last_Num_Init : constant Integer := Last_Number_Ghost (Str (From .. To)); Starts_As_Based : constant Boolean := - Last_Num_Init < To - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) else Last_Num_Init); Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < To - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); begin