From patchwork Wed May 18 08:43:27 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: 54147 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 C92453858C56 for ; Wed, 18 May 2022 09:09:54 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org C92453858C56 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1652864994; bh=fgbCxarLYBV6xJLHtwafVgUFSqWAU0IZYPEsVqJKd2c=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=MwGau8/26RqE8XivooVUykbOW7JWpRh8dyqIQrREZfjfeOdLyPekGuFVgZ6ET95Fi P5VBOStwlhYssvt9JkEUk8xepotqqrEsxUN5SVt6I4NZd2S8bi0OOR6mAaxaKUMgoM eWcl/BkEpP5fBpV00E3bcMuru6YNQd8ziiNjXrH4= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x333.google.com (mail-wm1-x333.google.com [IPv6:2a00:1450:4864:20::333]) by sourceware.org (Postfix) with ESMTPS id 2D3E83858434 for ; Wed, 18 May 2022 08:43:29 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 2D3E83858434 Received: by mail-wm1-x333.google.com with SMTP id i20-20020a05600c355400b0039456976dcaso1970854wmq.1 for ; Wed, 18 May 2022 01:43:29 -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=fgbCxarLYBV6xJLHtwafVgUFSqWAU0IZYPEsVqJKd2c=; b=RfvlY6GJaHYeFoqR0pzk5dWEEMEuA/3me+L9zUE+G6chlT+nmJfRASw8O50xW29Wun aaEKblqYk+XuuvlMGBf2tY8vvTzkt7t0hRRiVo50X7rbDG+crOEc7VinEZEgYipesz+d YaboW08iOoVytyewKL4QjlFkU4GjB7t/R3esiTRkIsf9O2w4nKc5isq2mFXeTZkeoIqZ OX5jq/by6LXCWp966a++OjhdorBBHdZUfmXQujDpDVgl3yXtRSy8NVlikH4/S+gdp15m wD6qQH8nXwjb4IdKoLCyC16Tqq5dmly4QSxodnfrnw3Jt2pA5nMLYdI/oRwMxyXP6FUB BN/g== X-Gm-Message-State: AOAM530AEkWvkhHcymUN8zXR3/oV4wXJ4YKA16hv7Ql+Z71NWBUQiSw0 BneOTkwbbC00vq6e6Wz+Jirmuz7p576Y7w== X-Google-Smtp-Source: ABdhPJxTS87e2jdI3mGbftxlaMOWA6XaM7cgw8Qqu7TkzyEVGZ4+gxR/I8dIq5LyqFkupGwEjGLzRA== X-Received: by 2002:a05:600c:214c:b0:394:2dfe:2754 with SMTP id v12-20020a05600c214c00b003942dfe2754mr24964197wml.135.1652863408742; Wed, 18 May 2022 01:43:28 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id d19-20020adf9c93000000b0020d106c0386sm1276468wre.89.2022.05.18.01.43.27 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 18 May 2022 01:43:28 -0700 (PDT) Date: Wed, 18 May 2022 08:43:27 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Adapt proof of double arithmetic runtime unit Message-ID: <20220518084327.GA3379224@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.3 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: Yannick Moy Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" After changes in Why3 and generation of VCs, ghost code needs to be adapted for proofs to remain automatic. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-aridou.adb (Big3): Change return type. (Lemma_Mult_Non_Negative, Lemma_Mult_Non_Positive): Reorder alphabetically. (Lemma_Concat_Definition, Lemma_Double_Big_2xxsingle): New lemmas. (Double_Divide, Scaled_Divide): Add assertions. diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -133,7 +133,7 @@ is Post => Big_2xx'Result > 0; -- 2**N as a big integer - function Big3 (X1, X2, X3 : Single_Uns) return Big_Integer is + function Big3 (X1, X2, X3 : Single_Uns) return Big_Natural is (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (X1)) + Big_2xxSingle * Big (Double_Uns (X2)) + Big (Double_Uns (X3))) @@ -208,20 +208,6 @@ is Ghost, Post => abs (X * Y) = abs X * abs Y; - procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) - with - Ghost, - Pre => (X >= Big_0 and then Y >= Big_0) - or else (X <= Big_0 and then Y <= Big_0), - Post => X * Y >= Big_0; - - procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) - with - Ghost, - Pre => (X <= Big_0 and then Y >= Big_0) - or else (X >= Big_0 and then Y <= Big_0), - Post => X * Y <= Big_0; - procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer) with Ghost, @@ -246,6 +232,12 @@ is Pre => M < N and then N < Double_Size, Post => Double_Uns'(2)**M < Double_Uns'(2)**N; + procedure Lemma_Concat_Definition (X, Y : Single_Uns) + with + Ghost, + Post => Big (X & Y) = Big_2xxSingle * Big (Double_Uns (X)) + + Big (Double_Uns (Y)); + procedure Lemma_Deep_Mult_Commutation (Factor : Big_Integer; X, Y : Single_Uns) @@ -289,6 +281,11 @@ is Pre => A * S = B * S + R and then S /= 0, Post => A = B + R / S; + procedure Lemma_Double_Big_2xxSingle + with + Ghost, + Post => Big_2xxSingle * Big_2xxSingle = Big_2xxDouble; + procedure Lemma_Double_Shift (X : Double_Uns; S, S1 : Double_Uns) with Ghost, @@ -419,6 +416,20 @@ is Ghost, Post => X * (Y + Z) = X * Y + X * Z; + procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) + with + Ghost, + Pre => (X >= Big_0 and then Y >= Big_0) + or else (X <= Big_0 and then Y <= Big_0), + Post => X * Y >= Big_0; + + procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) + with + Ghost, + Pre => (X <= Big_0 and then Y >= Big_0) + or else (X >= Big_0 and then Y <= Big_0), + Post => X * Y <= Big_0; + procedure Lemma_Neg_Div (X, Y : Big_Integer) with Ghost, @@ -552,6 +563,7 @@ is procedure Lemma_Add_Commutation (X : Double_Uns; Y : Single_Uns) is null; procedure Lemma_Add_One (X : Double_Uns) is null; procedure Lemma_Bounded_Powers_Of_2_Increasing (M, N : Natural) is null; + procedure Lemma_Concat_Definition (X, Y : Single_Uns) is null; procedure Lemma_Deep_Mult_Commutation (Factor : Big_Integer; X, Y : Single_Uns) @@ -566,6 +578,7 @@ is procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null; procedure Lemma_Div_Lt (X, Y, Z : Big_Natural) is null; procedure Lemma_Div_Eq (A, B, S, R : Big_Integer) is null; + procedure Lemma_Double_Big_2xxSingle is null; procedure Lemma_Double_Shift (X : Double_Uns; S, S1 : Double_Uns) is null; procedure Lemma_Double_Shift (X : Single_Uns; S, S1 : Natural) is null; procedure Lemma_Double_Shift_Right (X : Double_Uns; S, S1 : Double_Uns) @@ -929,10 +942,18 @@ is pragma Assert (Big (Double_Uns'(Yhi * Zhi)) >= 1); if Yhi > 1 or else Zhi > 1 then pragma Assert (Big (Double_Uns'(Yhi * Zhi)) > 1); + pragma Assert (if X = Double_Int'First and then Round then + Mult > Big_2xxDouble); elsif Zlo > 0 then pragma Assert (Big (Double_Uns'(Yhi * Zlo)) > 0); + pragma Assert (if X = Double_Int'First and then Round then + Mult > Big_2xxDouble); elsif Ylo > 0 then pragma Assert (Big (Double_Uns'(Ylo * Zhi)) > 0); + pragma Assert (if X = Double_Int'First and then Round then + Mult > Big_2xxDouble); + else + pragma Assert (not (X = Double_Int'First and then Round)); end if; Prove_Quotient_Zero; end if; @@ -976,6 +997,7 @@ is Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (Hi (T2))), Big (Double_Uns (Lo (T2)))); + Lemma_Double_Big_2xxSingle; pragma Assert (Mult = Big_2xxDouble * Big (Double_Uns (Hi (T2))) + Big_2xxSingle * Big (Double_Uns (Lo (T2))) @@ -1890,7 +1912,14 @@ is Big_2xx (Scale), Big_2xxDouble); Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xxSingle, Big_2xx (Scale), Big_2xxDouble); - Lemma_Mult_Commutation (2 ** Scale, D (1) & D (2), T1); + declare + Two_xx_Scale : constant Double_Uns := Double_Uns'(2 ** Scale); + D12 : constant Double_Uns := D (1) & D (2); + begin + pragma Assert (Big_2xx (Scale) * Big (D12) < Big_2xxDouble); + pragma Assert (Big (Two_xx_Scale) * Big (D12) < Big_2xxDouble); + Lemma_Mult_Commutation (Two_xx_Scale, D12, T1); + end; declare Big_D12 : constant Big_Integer := Big_2xx (Scale) * Big (D (1) & D (2)); @@ -1954,6 +1983,10 @@ is pragma Assert (Big (Double_Uns (Hi (T3))) + Big (Double_Uns (Hi (T2))) = Big (Double_Uns (S1))); + pragma Assert + (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) + + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3))) + = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1))); end Prove_Multiplication; ----------------------------- @@ -2092,6 +2125,9 @@ is Lemma_Div_Lt (Big (T1), Big_2xxSingle, Big (Double_Uns (Zlo))); Lemma_Div_Commutation (T1, Double_Uns (Zlo)); Lemma_Lo_Is_Ident (T1 / Zlo); + pragma Assert + (Big (T2) <= Big_2xxSingle * (Big (Double_Uns (Zlo)) - 1) + + Big (Double_Uns (D (4)))); Lemma_Div_Lt (Big (T2), Big_2xxSingle, Big (Double_Uns (Zlo))); Lemma_Div_Commutation (T2, Double_Uns (Zlo)); Lemma_Lo_Is_Ident (T2 / Zlo); @@ -2304,6 +2340,9 @@ is -- First normalize the divisor so that it has the leading bit on. -- We do this by finding the appropriate left shift amount. + Lemma_Lt_Commutation (D (1) & D (2), Zu); + pragma Assert (Mult < Big_2xxDouble * Big (Zu)); + Shift := Single_Size; Mask := Single_Uns'Last; Scale := 0; @@ -2376,6 +2415,8 @@ is procedure Prove_Shift_Progress is null; begin + pragma Assert (Mask = Shift_Left (Single_Uns'Last, + Single_Size - Shift_Prev)); Prove_Power; Shift := Shift / 2; @@ -2470,6 +2511,16 @@ is + Big (Double_Uns (D (3))), Big3 (D (1), D (2), D (3)), Big (Double_Uns (D (4)))); + Lemma_Concat_Definition (D (1), D (2)); + Lemma_Double_Big_2xxSingle; + Lemma_Substitution + (Mult * Big_2xx (Scale), Big_2xxSingle * Big_2xxSingle, + Big_2xxSingle * Big (Double_Uns (D (1))) + + Big (Double_Uns (D (2))), + Big (D (1) & D (2)), + Big_2xxSingle * Big (Double_Uns (D (3))) + + Big (Double_Uns (D (4)))); + pragma Assert (Big (D (1) & D (2)) < Big (Zu)); -- Loop to compute quotient digits, runs twice for Qd (1) and Qd (2)