From patchwork Mon May 15 09:42:36 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: 94042 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:b0ea:0:b0:3b6:4342:cba0 with SMTP id b10csp6792612vqo; Mon, 15 May 2023 02:49:23 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ6zqwz3sbRnXKSk+j+AgmYbSnauAo1L3EJgVy/MwU7SANoJ7V+lLD/dWIWJ0YcS0rypjf1q X-Received: by 2002:a17:906:eec5:b0:965:9e78:c579 with SMTP id wu5-20020a170906eec500b009659e78c579mr26275608ejb.16.1684144163613; Mon, 15 May 2023 02:49:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1684144163; cv=none; d=google.com; s=arc-20160816; b=iUuTWKRedPm888zA4ybw0YRRiY2dYsNyvDgwdbrVCuItptXSI7Xdp8i+4pSAuB0vLN 3lln6EdDNt60ctUXFVYUCbMmpZcBmXDGI04DA5nuePSNkmv7bH9utun5L4oP2YSWn2Iv zUyrNk22BfAtVamNP7Ms1epooKxyIM6uGdTZKuhKUfMNlVbJh+1dGCDWVuBRja8hbxpc hSsAyEjGfTyif/UVwhBH+AjKNly3O2SLWQnbctKJWk+ah2cv4pSyapVntVBumrgdesMO lByc2p7kYY4MN9Za8yPmJ1jEo0WeRYZMUFY3Fa4nOT3peympyKqjRC9sqlY+gdPkvFg8 SBMA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=nZ2RkOBlLE6JFIFBHuD7E69cu8ecJJObWr8Qu+SBwfg=; b=Dkf73i/OytyvWDuw5UYVggHOE6M3huWlrTJEnhdOdNEdN5NWUYeL30bzqfrNrP5KzR R0qzG+p/rbGr7FM43yQz2RdTMaiI52bNePrZ571Lh4KPupumcrQe99sw065z5WSo5IVe o6mhW7xLXOFthflD+dAQEmTSq0oxCYZlK8MatmDULR+m2Gzmp9qVz1YnYkqrUlnaJDY0 yY0JwzkG8ALD7V2DIVebs+lXJBUx1Du9XfRqBEX0xDpJa4hAEtOfixtRal2KynH/uKHB bkMP/DGBy0vO6svjB2Nf4zFjv67A5BHodsURBTs9b7wj3IJXlGaCRUUAMhl+pGUsR1Ax wG6g== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=aCuKEHl1; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id wi4-20020a170906fd4400b009659d31ac13si10556601ejb.586.2023.05.15.02.49.23 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 May 2023 02:49:23 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=aCuKEHl1; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 302F03888C6D for ; Mon, 15 May 2023 09:45:57 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 302F03888C6D DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1684143957; bh=nZ2RkOBlLE6JFIFBHuD7E69cu8ecJJObWr8Qu+SBwfg=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=aCuKEHl1sN/e657L+yf1AzS9DSlFuM3JiVQdEqgYwYzkEMk73b5H5PPqrJ6HGqrYR ecd2uvS/p65fSgStETnhpdLZYk2mpBul2fZ8gRnZcMj2g8HVfI0J37LlyqodiKTdae x/GagVup9V+IGajurf/1n+xwIYsGpoicPTh6Z4Ww= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x32a.google.com (mail-wm1-x32a.google.com [IPv6:2a00:1450:4864:20::32a]) by sourceware.org (Postfix) with ESMTPS id 621123852912 for ; Mon, 15 May 2023 09:42:41 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 621123852912 Received: by mail-wm1-x32a.google.com with SMTP id 5b1f17b1804b1-3f4ad71b00eso35063935e9.2 for ; Mon, 15 May 2023 02:42:41 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684143760; x=1686735760; 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=nZ2RkOBlLE6JFIFBHuD7E69cu8ecJJObWr8Qu+SBwfg=; b=IXLroYx5V7I78/xEzUttfa5EFyg+lIyx28dX7g8Rm0U5pgw/Wh/05gNs3/3+AlDPFb W1FiA4NQJSxQBp44EusNuxDb1/dOfgrExFDQOvIa/RA+8JaBozVA77n1SFYv/rAHOpjn 4+iiJsAGvBEF8z1omEG3CiyUwoeHwSxd9/UwunGQ+I6BFAATqehm6ovUM8eNTqMM2QDG jwKGEoz7d4uBBN+Gf0aFrwLLkU2O5DcqDS3RKs8iAUBfmFCD94PJN6U+jDutsFbZoFEd ArsfHXSQLixtKj+J/ZemxFdIS3bVOALyGUyHIwWwEA6xgxMnx9deOcf8LTCNYO4igap6 /tuA== X-Gm-Message-State: AC+VfDzbxyDmSy7ElACFLaZUE+/gWebWuEI92DCvsjyUWfk6rnDWl0Io A81ZAW+gQtBS6yc4S3Jrulxm83DCvNUWB9qK2GLqoQ== X-Received: by 2002:a7b:c8c9:0:b0:3f4:f00f:5e09 with SMTP id f9-20020a7bc8c9000000b003f4f00f5e09mr8545888wml.11.1684143760086; Mon, 15 May 2023 02:42:40 -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 12-20020a05600c020c00b003f50e29bce3sm1268127wmi.48.2023.05.15.02.42.39 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 May 2023 02:42:39 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Claire Dross Subject: [COMMITTED] ada: Fix proof of runtime unit System.Value* Date: Mon, 15 May 2023 11:42:36 +0200 Message-Id: <20230515094236.1407706-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.4 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+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1765953150587885219?= X-GMAIL-MSGID: =?utf-8?q?1765953150587885219?= From: Claire Dross Use cut operations to restore the proof of System.Value*. gcc/ada/ * libgnat/s-valueu.adb: Use cut operations inside assertion to restore proofs * gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Add s-spark and s-spcuop dependencies. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/gcc-interface/Make-lang.in | 2 + gcc/ada/libgnat/s-valueu.adb | 92 ++++++++++++++++++++---------- 2 files changed, 64 insertions(+), 30 deletions(-) diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index 9507f2f0920..7b826f2366f 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -536,6 +536,8 @@ GNAT_ADA_OBJS+= \ ada/libgnat/s-secsta.o \ ada/libgnat/s-soflin.o \ ada/libgnat/s-soliin.o \ + ada/libgnat/s-spark.o \ + ada/libgnat/s-spcuop.o \ ada/libgnat/s-stache.o \ ada/libgnat/s-stalib.o \ ada/libgnat/s-stoele.o \ diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index c6e26b0ee1f..bc6ed1ca669 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -29,6 +29,8 @@ -- -- ------------------------------------------------------------------------------ +with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations; + package body System.Value_U is -- Ghost code, loop invariants and assertions in this unit are meant for @@ -174,6 +176,7 @@ package body System.Value_U is P := Ptr.all; Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init); Uval := Character'Pos (Str (P)) - Character'Pos ('0'); + pragma Assert (Str (P) in '0' .. '9'); P := P + 1; -- Scan out digits of what is either the number or the base. @@ -215,19 +218,24 @@ package body System.Value_U is -- Accumulate result, checking for overflow else + pragma Assert + (By + (Str (P) in '0' .. '9', + By + (Character'Pos (Str (P)) >= Character'Pos ('0'), + Uns '(Character'Pos (Str (P))) >= + Character'Pos ('0')))); Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init, Acc => Uval); Spec.Lemma_Scan_Based_Number_Ghost_Overflow (Str, P, Last_Num_Init, Acc => Uval); if Uval <= Umax then - pragma Assert - (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit); Uval := 10 * Uval + Digit; pragma Assert (if not Overflow then Init_Val = Spec.Scan_Based_Number_Ghost - (Str, P + 1, Last_Num_Init, Acc => Uval)); + (Str, P + 1, Last_Num_Init, Acc => Uval)); elsif Uval > Umax10 then Overflow := True; @@ -241,7 +249,8 @@ package body System.Value_U is pragma Assert (if not Overflow then Init_Val = Spec.Scan_Based_Number_Ghost - (Str, P + 1, Last_Num_Init, Acc => Uval)); + (Str, P + 1, Last_Num_Init, Acc => Uval)); + end if; P := P + 1; @@ -252,7 +261,9 @@ package body System.Value_U is end; pragma Assert_And_Cut - (P = Last_Num_Init + 1 + (By + (P = Last_Num_Init + 1, + P > Max or else Str (P) not in '_' | '0' .. '9') and then Overflow = Init_Val.Overflow and then (if not Overflow then Init_Val.Value = Uval)); @@ -313,13 +324,24 @@ package body System.Value_U is -- already stored in Ptr.all. else + pragma Assert + (By + (Spec.Only_Hexa_Ghost (Str, P, Last_Num_Based), + P > Last_Num_Init + 1 + and Spec.Only_Hexa_Ghost + (Str, Last_Num_Init + 2, Last_Num_Based))); Spec.Lemma_Scan_Based_Number_Ghost_Base (Str, P, Last_Num_Based, Base, Uval); Uval := Base; Base := 10; pragma Assert (Ptr.all = Last_Num_Init + 1); pragma Assert - (if Starts_As_Based then P = Last_Num_Based + 1); + (if Starts_As_Based + then By + (P = Last_Num_Based + 1, + P <= Last_Num_Based + 1 + and Str (P) not in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')); pragma Assert (not Is_Based); pragma Assert (if not Overflow then Uval = Init_Val.Value); exit; @@ -394,11 +416,15 @@ package body System.Value_U is Ptr.all := P + 1; pragma Assert (P = Last_Num_Based + 1); pragma Assert (Ptr.all = Last_Num_Based + 2); - pragma Assert (Starts_As_Based); - pragma Assert (Last_Num_Based < Max); - pragma Assert (Str (Last_Num_Based + 1) = Base_Char); - pragma Assert (Base_Char = Str (Last_Num_Init + 1)); - pragma Assert (Is_Based); + pragma Assert + (By + (Is_Based, + So + (Starts_As_Based, + So + (Last_Num_Based < Max, + Str (Last_Num_Based + 1) = Base_Char + and Base_Char = Str (Last_Num_Init + 1))))); Spec.Lemma_Scan_Based_Number_Ghost_Base (Str, P, Last_Num_Based, Base, Uval); exit; @@ -414,41 +440,40 @@ package body System.Value_U is (if not Overflow then Based_Val = Spec.Scan_Based_Number_Ghost (Str, P, Last_Num_Based, Base, Uval)); - pragma Assert (Str (P) /= '_'); - pragma Assert (Str (P) /= Base_Char); + pragma Assert (Str (P) not in '_' | Base_Char); end if; Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max); - pragma Assert (Str (P) /= '_'); - pragma Assert (Str (P) /= Base_Char); + pragma Assert (Str (P) not in '_' | Base_Char); end loop; end; pragma Assert (if Starts_As_Based then P = Last_Num_Based + 1 else P = Last_Num_Init + 2); pragma Assert - (Last_Num_Init < Max - 1 - and then Str (Last_Num_Init + 1) in '#' | ':'); - pragma Assert - (Overflow = - (Init_Val.Overflow - or else Init_Val.Value not in 2 .. 16 - or else (Starts_As_Based and then Based_Val.Overflow))); - pragma Assert - (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)); + (By + (Overflow /= Spec.Scan_Split_No_Overflow_Ghost + (Str, Ptr_Old, Max), + So + (Last_Num_Init < Max - 1 + and then Str (Last_Num_Init + 1) in '#' | ':', + Overflow = + (Init_Val.Overflow + or else Init_Val.Value not in 2 .. 16 + or else (Starts_As_Based and Based_Val.Overflow))))); end if; pragma Assert_And_Cut (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max) - and then - (if not Overflow then - (if Is_Based then Uval = Based_Val.Value - else Uval = Init_Val.Value)) and then Ptr.all = First_Exp and then Base in 2 .. 16 and then (if not Overflow then - (if Is_Based then Base = Init_Val.Value else Base = 10))); + (if Is_Based then Base = Init_Val.Value else Base = 10)) + and then + (if not Overflow then + (if Is_Based then Uval = Based_Val.Value + else Uval = Init_Val.Value))); -- Come here with scanned unsigned value in Uval. The only remaining -- required step is to deal with exponent if one is present. @@ -456,7 +481,14 @@ package body System.Value_U is Scan_Exponent (Str, Ptr, Max, Expon); pragma Assert - (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max)); + (By + (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max), + (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max)) + then Ptr.all = First_Exp + elsif Str (First_Exp + 1) in '-' | '+' then + Ptr.all = Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1 + else Ptr.all = + Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1))); pragma Assert (if not Overflow then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) =