From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 9E90A3835413; Wed, 11 May 2022 08:55:54 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 9E90A3835413 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-305] [Ada] Adapt proof of System.Arith_Double after update of Z3 X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: a58f70c30c4900bb9024681e0b86e85d96cac2e7 X-Git-Newrev: 4c533da21d6298cdf9eb11df7353b8c8684c7756 Message-Id: <20220511085554.9E90A3835413@sourceware.org> Date: Wed, 11 May 2022 08:55:54 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 11 May 2022 08:55:54 -0000 https://gcc.gnu.org/g:4c533da21d6298cdf9eb11df7353b8c8684c7756 commit r13-305-g4c533da21d6298cdf9eb11df7353b8c8684c7756 Author: Yannick Moy Date: Wed Feb 2 12:52:36 2022 +0100 [Ada] Adapt proof of System.Arith_Double after update of Z3 Update to version 4.8.14 of prover Z3 requires minor adjustments of the ghost code to add necessary intermediate assertions that drive the automatic proof. gcc/ada/ * libgnat/s-aridou.adb (Double_Divide, Scaled_Divide): Add intermediate assertions. Diff: --- gcc/ada/libgnat/s-aridou.adb | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 0fefb6bd945..ffb6f4ca269 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -924,6 +924,8 @@ is else Q := 0; + pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Yhi)); + pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Zhi)); pragma Assert (Big (Double_Uns'(Yhi * Zhi)) >= 1); if Yhi > 1 or else Zhi > 1 then pragma Assert (Big (Double_Uns'(Yhi * Zhi)) > 1); @@ -938,10 +940,12 @@ is return; else T2 := Yhi * Zlo; + pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo))); end if; else T2 := Ylo * Zhi; + pragma Assert (Big (T2) = Big (Double_Uns'(Ylo * Zhi))); end if; T1 := Ylo * Zlo; @@ -1527,10 +1531,14 @@ is Raise_Error; else T2 := Xhi * Ylo; + pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo)) + + Big (Double_Uns'(Xlo * Yhi))); end if; elsif Yhi /= 0 then T2 := Xlo * Yhi; + pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo)) + + Big (Double_Uns'(Xlo * Yhi))); else -- Yhi = Xhi = 0 T2 := 0; @@ -1544,7 +1552,7 @@ is pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi))); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Xhi * Ylo)), - Big (Double_Uns'(Xlo * Yhi))); + Big (Double_Uns'(Xlo * Yhi))); pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1)); Lemma_Add_Commutation (T2, Hi (T1)); pragma Assert @@ -2575,7 +2583,13 @@ is Big (Double_Uns (Qd (J))) - 1, Big (Double_Uns (Qd (J) - 1)), 0); - Qd (J) := Qd (J) - 1; + declare + Prev : constant Single_Uns := Qd (J) - 1 with Ghost; + begin + Qd (J) := Qd (J) - 1; + + pragma Assert (Qd (J) = Prev); + end; pragma Assert (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));