From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wm1-x32d.google.com (mail-wm1-x32d.google.com [IPv6:2a00:1450:4864:20::32d]) by sourceware.org (Postfix) with ESMTPS id 8694A38845FF for ; Wed, 11 May 2022 08:54:40 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 8694A38845FF Received: by mail-wm1-x32d.google.com with SMTP id m62so767169wme.5 for ; Wed, 11 May 2022 01:54:40 -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=aYzA11nF4BXdRIG72MgE5fC5A41boB3t+rSTKjQSQ9k=; b=xBK2Yz5819vDJwRchbxznaCzO22QtEowgr1YpeEMFknolKl8PijSS9O5FKJ32SDJel egOVXIQaYCGIP52T8gpe1hRZv/rkIuvuC++co63JAAdNYVgtyK8M8vfeUohkqFgcCwIb 1Tb0kYw0MlTNSTyqd+JqS54W67km/lat+WE4pSpX6n+infbUb8LtcjCyc3fWwDF9xcDS GqmUTVtm47+kno3BMttkXv/WX42O2KKt06684bjTJfcR9nHheOze9YtSi8m8Bn+mUEWz nqv1ZT3dLq5GF07zpPbeo6gTPKJzB7mjaWVeiFmNi5XKRRbUyVql+s3L3yiXkchKtBZw GkjQ== X-Gm-Message-State: AOAM530SifDt2tAlBpSVeC55fDesjibD3UKn8y7HRnQM03hT5b6wBr1e pZpbGO3jesn+PUxKU1bwlGDBBkp0E3g6zg== X-Google-Smtp-Source: ABdhPJwppvA4d9tLl6Epy25FCbIe6DMQ4ey1FlwLTaed9KNtEMOKGa8TcabMkOGZ9io7VrMV/PpZxQ== X-Received: by 2002:a1c:f211:0:b0:381:6c60:742f with SMTP id s17-20020a1cf211000000b003816c60742fmr3857759wmc.130.1652259279358; Wed, 11 May 2022 01:54:39 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id l68-20020a1c2547000000b003947b59dfdesm5448411wml.36.2022.05.11.01.54.38 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 11 May 2022 01:54:38 -0700 (PDT) Date: Wed, 11 May 2022 08:54:38 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Adapt proof of System.Arith_Double after update of Z3 Message-ID: <20220511085438.GA2167242@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="J/dobhs11T7y2rNN" Content-Disposition: inline X-Spam-Status: No, score=-12.9 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_NUMSUBJECT, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE 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-List-Received-Date: Wed, 11 May 2022 08:54:42 -0000 --J/dobhs11T7y2rNN Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-aridou.adb (Double_Divide, Scaled_Divide): Add intermediate assertions. --J/dobhs11T7y2rNN Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" 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 @@ -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)); --J/dobhs11T7y2rNN--