From patchwork Wed Oct 20 19:27:58 2021 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: 1544030 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=WVr114tX; 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 (4096 bits) server-digest SHA256) (No client certificate requested) by bilbo.ozlabs.org (Postfix) with ESMTPS id 4HZLdH5Qqpz9sNH for ; Thu, 21 Oct 2021 06:43:31 +1100 (AEDT) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 4B5733857C76 for ; Wed, 20 Oct 2021 19:43:29 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 4B5733857C76 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1634759009; bh=NnR8ijItRpiksx8ePGLEmGMl9joyKm8P4RUSollfTL8=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=WVr114tXLoaIEjb73sVdzPNkQ37LgTL8luTj6Cl9MyNtbL8M+aTljj7qSzFjaM7NT zhUioh5l8ebIeag+TrGCoas7dizO2uBwmZqNfWk14Q7JJHCH3YtwfY1XtC7fRx3vGJ ySfizGj8ggQr/cqg1Whu7OldDICY4VK2InEYDz/Q= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-lf1-x135.google.com (mail-lf1-x135.google.com [IPv6:2a00:1450:4864:20::135]) by sourceware.org (Postfix) with ESMTPS id CA2E33857C52 for ; Wed, 20 Oct 2021 19:28:01 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org CA2E33857C52 Received: by mail-lf1-x135.google.com with SMTP id y26so343858lfa.11 for ; Wed, 20 Oct 2021 12:28:01 -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=NnR8ijItRpiksx8ePGLEmGMl9joyKm8P4RUSollfTL8=; b=rOzCgNwB4KCs/UdcEIPNpDgjM8pJ6HJknRitG3xrOYz6Sg8fr/0ITFB0Tic8Nfu7mD 1+/5F7Z/e8KlS5RFPC5X2tishbVGoFbCa0N9smq44Sibhvow314+lwK2sOprR8JKWqMH rb7CaC74e9ICHBTpLoogcZihnO1aaSD0dmBHJooINFkT/lVJxOi3/Za5QUCkO/wh5uDF p2ulkJbd8L2zOEJ2ig0uWYg/aDeHUsik5jFWrs6q0J6FYOsWmorVWu7XC8mir8OYtSJh X2PCjW56pEO6inedo15mfEEyonJ7mrOyz6XoWWhE3qZZ9O2A3u9mAwJerT3NgFowio1B 85Rw== X-Gm-Message-State: AOAM531Wj+tafSjicJxREvPOwNshPAxFYjfsxBq3CCUpH0IUgc1XJQBn da9Gq1RL+N+enp1lhBb5zLUZqyhEUQs= X-Google-Smtp-Source: ABdhPJw8mfqMwrup5kMuEFV7JBdriueeuaxiEdJBilYbUuPCc/9aC6srTUXnghxsaJNVwQAxS3g9xA== X-Received: by 2002:a05:6512:791:: with SMTP id x17mr1074623lfr.155.1634758080677; Wed, 20 Oct 2021 12:28:00 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id bu21sm261751lfb.39.2021.10.20.12.27.59 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 20 Oct 2021 12:27:59 -0700 (PDT) Date: Wed, 20 Oct 2021 19:27:58 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Proof of the runtime support for attribute 'Width Message-ID: <20211020192758.GA3154456@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.0 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+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" This proves the absence of runtime errors and the functional spec of function System.Width_U which implements the runtime support for attribute 'Width. It requires using the library unit Ada.Numerics.Big_Numbers.Big_Integers because it was not possible to achieve even absence of runtime errors by attempting the same proofs completely in machine integer type Uns, as provers don't succeed in that case to abstract from the constant need to prove absence of wrap-around/overflow. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-widlllu.ads: Mark in SPARK. * libgnat/s-widllu.ads: Likewise. * libgnat/s-widuns.ads: Likewise. * libgnat/s-widthu.adb: Add ghost code and a pseudo-postcondition. diff --git a/gcc/ada/libgnat/s-widlllu.ads b/gcc/ada/libgnat/s-widlllu.ads --- a/gcc/ada/libgnat/s-widlllu.ads +++ b/gcc/ada/libgnat/s-widlllu.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_LLLU is - +package System.Wid_LLLU + with SPARK_Mode +is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; function Width_Long_Long_Long_Unsigned is diff --git a/gcc/ada/libgnat/s-widllu.ads b/gcc/ada/libgnat/s-widllu.ads --- a/gcc/ada/libgnat/s-widllu.ads +++ b/gcc/ada/libgnat/s-widllu.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_LLU is - +package System.Wid_LLU + with SPARK_Mode +is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; function Width_Long_Long_Unsigned is new Width_U (Long_Long_Unsigned); diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,10 +29,87 @@ -- -- ------------------------------------------------------------------------------ +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + function System.Width_U (Lo, Hi : Uns) return Natural 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); + W : Natural; T : Uns; + package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); + + function Big (Arg : Uns) return Big_Integer is + (Unsigned_Conversion.To_Big_Integer (Arg)) + with Ghost; + + -- Maximum value of exponent for 10 that fits in Uns'Base + function Max_Log10 return Natural is + (case Uns'Base'Size is + when 8 => 2, + when 16 => 4, + when 32 => 9, + when 64 => 19, + when 128 => 38, + when others => raise Program_Error) + with Ghost; + + Max_W : constant Natural := Max_Log10 with Ghost; + Big_10 : constant Big_Integer := Big (10) with Ghost; + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) + with + Ghost, + Pre => A <= B, + Post => A * C <= B * C; + + procedure Lemma_Div_Commutation (X, Y : Uns) + with + Ghost, + Pre => Y /= 0, + Post => Big (X) / Big (Y) = Big (X / Y); + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) + with + Ghost, + Post => X / Y / Z = X / (Y * Z); + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is + begin + null; + end Lemma_Lower_Mult; + + procedure Lemma_Div_Commutation (X, Y : Uns) is + begin + null; + end Lemma_Div_Commutation; + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is + XY : constant Big_Natural := X / Y; + YZ : constant Big_Natural := Y * Z; + XYZ : constant Big_Natural := X / Y / Z; + R : constant Big_Natural := (XY rem Z) * Y + (X rem Y); + begin + pragma Assert (X = XY * Y + (X rem Y)); + pragma Assert (XY = XY / Z * Z + (XY rem Z)); + pragma Assert (X = XYZ * YZ + R); + pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y); + pragma Assert (R <= YZ - 1); + pragma Assert (X / YZ = (XYZ * YZ + R) / YZ); + pragma Assert (X / YZ = XYZ + R / YZ); + end Lemma_Div_Twice; + + Pow : Big_Integer := 1 with Ghost; + T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; + begin if Lo > Hi then return 0; @@ -50,10 +127,40 @@ begin -- Increase value if more digits required while T >= 10 loop + Lemma_Div_Commutation (T, 10); + Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); + T := T / 10; W := W + 1; + Pow := Pow * 10; + + pragma Loop_Variant (Decreases => T); + pragma Loop_Invariant (W in 3 .. Max_W + 3); + pragma Loop_Invariant (Pow = Big_10 ** (W - 2)); + pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow); end loop; + declare + F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; + Q : constant Big_Integer := Big (T_Init) / F with Ghost; + R : constant Big_Integer := Big (T_Init) rem F with Ghost; + begin + pragma Assert (Q < Big_10); + pragma Assert (Big (T_Init) = Q * F + R); + Lemma_Lower_Mult (Q, Big (9), F); + pragma Assert (Big (T_Init) <= Big (9) * F + F - 1); + pragma Assert (Big (T_Init) < Big_10 * F); + pragma Assert (Big_10 * F = Big_10 ** (W - 1)); + end; + + -- This is an expression of the functional postcondition for Width_U, + -- which cannot be expressed readily as a postcondition as this would + -- require making the instantiation Unsigned_Conversion and function + -- Big available from the spec. + + pragma Assert (Big (Lo) < Big_10 ** (W - 1)); + pragma Assert (Big (Hi) < Big_10 ** (W - 1)); + return W; end if; diff --git a/gcc/ada/libgnat/s-widuns.ads b/gcc/ada/libgnat/s-widuns.ads --- a/gcc/ada/libgnat/s-widuns.ads +++ b/gcc/ada/libgnat/s-widuns.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_Uns is - +package System.Wid_Uns + with SPARK_Mode +is subtype Unsigned is Unsigned_Types.Unsigned; function Width_Unsigned is new Width_U (Unsigned);