From patchwork Tue Dec 19 14:30:39 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: 180998 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a05:7300:24d3:b0:fb:cd0c:d3e with SMTP id r19csp1979000dyi; Tue, 19 Dec 2023 06:33:20 -0800 (PST) X-Google-Smtp-Source: AGHT+IH1/Ta5SJfLs+Vz0kxIxiLuiOOj+bVSlQHZAwqPyGuMSgnDhKS/GRBoi+jA0ScHoc/QhZuR X-Received: by 2002:a05:6870:8a29:b0:203:ff14:ba9a with SMTP id p41-20020a0568708a2900b00203ff14ba9amr230816oaq.104.1702996399802; Tue, 19 Dec 2023 06:33:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1702996399; cv=pass; d=google.com; s=arc-20160816; b=TIO9h56TJ9GTLtUavK8ljP7aGsTH9iagNqNhWP/OiL73IiueEFvCDdAGLay/oGIuBq Xid2NH6mitzGJ3uFnYjwsV0qB+fCNb6LPjWAe/9CKZm1F7l6IHcchq8IKmsRqtT747sK 5A0MsMdsVgaENDqwKq4vFYUCeCIX9hZHzlEZPno9sM7uYGZLsMUebcdCdE8/pSNIakNx 14Lavybv5toiNlZcKUFSXGo6MCV/G8ogPKVVbnfJ523umzO6crmIoJHB2k+T+cuq/cTb /cT3+xqm5tGXGV9V1/jb0xT7Pn9DtqBSnQ1EungfYDn5P/qQ+795kcMZpfpRPgmvPCjF GGtQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=errors-to:list-subscribe:list-help:list-post:list-archive :list-unsubscribe:list-id:precedence:content-transfer-encoding :mime-version:message-id:date:subject:cc:to:from:dkim-signature :arc-filter:dmarc-filter:delivered-to; bh=OkedhQerkWhE0+ZFeZkHcpi0YKh+REP8juxPX9TFC6Y=; fh=xkXw4ZjwHxuTwIHh5BpbVWFYGO+bP8cUYTTqcq/2BVI=; b=mKyJuh3Rp8qe66PM7xkQbQhBityz7MwLRhkQfoNNNO2oDfzrT3+tiNF39x/soAvOyA SXJo/CBlP67LPbb1HdWRgY6N9eUfTBv0TqVFmxAfA0zyfpVpgRmSUXEwmbqrEiTriM5n dKxobpOXhYQFHijKb7GUiTYjXnyc0FGX3AuL2d1pGlkm43pmhzzZ3tjdBUEBxIpV1pn9 8wUqzUnLY0dMFH7ETO3Peg4K5tQ13yTKwMglFU49bITi66VuXv7aZlQ47iFbfziOQFfp /4HRPIy0zcCp694tt/lOrhk34zCLOvwJNXLRfaReSujBccTQNx4eCAsH9mjgNRUI8FnM Ro2Q== ARC-Authentication-Results: i=2; mx.google.com; dkim=pass header.i=@adacore.com header.s=google header.b=WxFfbwRJ; arc=pass (i=1); spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=adacore.com Received: from server2.sourceware.org (server2.sourceware.org. [8.43.85.97]) by mx.google.com with ESMTPS id df7-20020a056102440700b0046683cee889si1063520vsb.633.2023.12.19.06.33.19 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 19 Dec 2023 06:33:19 -0800 (PST) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) client-ip=8.43.85.97; Authentication-Results: mx.google.com; dkim=pass header.i=@adacore.com header.s=google header.b=WxFfbwRJ; arc=pass (i=1); spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=adacore.com Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 0BC3938293D0 for ; Tue, 19 Dec 2023 14:31:42 +0000 (GMT) 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 3B9573870857 for ; Tue, 19 Dec 2023 14:30:42 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 3B9573870857 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org 3B9573870857 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::32a ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1702996244; cv=none; b=mBA2hnSX35bcHPfTKHk1TSPxzpjX4T5h8l1SG72UAqssSFnp40L6AC5ZjgdMOptm3JEHZDwEk1Jpg4mY8rsN5ZdhJrOobApFNZ3qIrYd+YgCXRbSnat89I2KaiWXevBpQzx/Aur8LYVk+DuUK9xwHUXVFEUHYd/YCZxF235NPss= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1702996244; c=relaxed/simple; bh=YIrGcJ5R/gDoCSgyoUShUNDupx374jbU+qyeKxGW2+Q=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=pjruPnTXnJKJXO1ZAXkMrz9OS6x9I6aLm3REFKoW74VDg+bFKPguQqYYi6pz5KDve4hXdGVV3JBwIJqmuOCbO4Zr8djAmX+Xs44OX0qrWl5CZnEWxolKIBgUdf8P5gcGDCfiDEJzBgVh4SJNFIqm+/b1CoiGqe0h/vhCzoKjjL4= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-wm1-x32a.google.com with SMTP id 5b1f17b1804b1-40d12ade25dso32556385e9.2 for ; Tue, 19 Dec 2023 06:30:42 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1702996241; x=1703601041; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=OkedhQerkWhE0+ZFeZkHcpi0YKh+REP8juxPX9TFC6Y=; b=WxFfbwRJrqkV+eCcTYNZppWb2kSa9ya9Kayp936pPEFNASsz6S27xTMnr3ivOtJxKr 01Eqgc5f/FKy5yJMncYZuTDy2FVDMfAVo53eUgXNggaXtkJGe9IlK9sIPMsrQ4Vq5w+D 8g+veQoHkVY5A571gjZyaRwegQJtSUEBUoV1FThvLpEukL9+2fGPb5Kv2iZk2ivkqgaI jbvmzI1vgQ3BX3+45ZUJbvYzzNFtEgVOvdvwETDLbbcfC+SlN/je4JvyY7cukk/celXJ QuZWIc6VsT3md5IDKaID/hFxHvtcbREEjGb2kQtfkFj1lxB9R6fa+MmUMzSTfca9G0/C o/uw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1702996241; x=1703601041; 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=OkedhQerkWhE0+ZFeZkHcpi0YKh+REP8juxPX9TFC6Y=; b=KgShpDapCrCVhwcBRp9YcxpvJwbDFlP7paTXPqTkLblsGoMp8OE5eIhJha0HT4kCOI InhNe4OsZ4y4FMDnAKOyQ1/RjooZF1FEld4iXnaZJdSqRjud0gnJaATMh1BbPD3D7L6B amGGE3nvA7hPkkMxc48hJsUrGA69VtKslfxTEPiCtMlDcGVI0Cb9u3nFercbE1UfGNrX FqHubzyNUdEJ+wOoy3wlik4TC0fCXn9UYpa9Lrm8R0VO3OkltrrYsJx3EBi8c251EbtR j2/smky1BjOGsRJMede9X7ZByHB4gUVrvc1TuzO4CFcFDghJgFYuPe47w/3VpiDomEs3 Ii0A== X-Gm-Message-State: AOJu0Yx+12x5PVKy4i5Dr6L6MneaY1ys8wPKG/yAJijqfQNo4NL70bAN WOf5DbgmsSIg6TRWk5XbNP0wjvlpWTZtQGd3dIE= X-Received: by 2002:a05:600c:2106:b0:40c:3270:ecb4 with SMTP id u6-20020a05600c210600b0040c3270ecb4mr8677462wml.181.1702996240981; Tue, 19 Dec 2023 06:30:40 -0800 (PST) Received: from poulhies-Precision-5550.lan ([2001:861:3382:1a90:fe1e:443:c34f:edaa]) by smtp.gmail.com with ESMTPSA id o42-20020a05600c512a00b0040c25abd724sm3095971wms.9.2023.12.19.06.30.40 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 19 Dec 2023 06:30:40 -0800 (PST) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Fix SPARK expansion of container aggregates Date: Tue, 19 Dec 2023 15:30:39 +0100 Message-ID: <20231219143039.455106-1-poulhies@adacore.com> X-Mailer: git-send-email 2.43.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, 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.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org X-getmail-retrieved-from-mailbox: INBOX X-GMAIL-THRID: 1785721153241707539 X-GMAIL-MSGID: 1785721153241707539 From: Yannick Moy GNATprove supports container aggregates, except for indexed aggregates. It needs all expressions to have suitable target types and Do_Range_Check flags, which are added by the special expansion for GNATprove. There is no impact on code generation. gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Aggregate): New procedure for the special expansion. (Expand_SPARK): Call the new expansion procedure. * sem_util.adb (Is_Container_Aggregate): Implement missing test. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/exp_spark.adb | 146 ++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_util.adb | 17 ++--- 2 files changed, 155 insertions(+), 8 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index ae0e616c797..f77d5f9f829 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -23,6 +23,7 @@ -- -- ------------------------------------------------------------------------------ +with Aspects; use Aspects; with Atree; use Atree; with Checks; use Checks; with Einfo; use Einfo; @@ -47,6 +48,7 @@ with Sem_Aggr; use Sem_Aggr; with Sem_Aux; use Sem_Aux; with Sem_Ch7; use Sem_Ch7; with Sem_Ch8; use Sem_Ch8; +with Sem_Ch13; use Sem_Ch13; with Sem_Prag; use Sem_Prag; with Sem_Res; use Sem_Res; with Sem_Util; use Sem_Util; @@ -64,6 +66,10 @@ package body Exp_SPARK is -- Local Subprograms -- ----------------------- + procedure Expand_SPARK_N_Aggregate (N : Node_Id); + -- Perform specific expansion of container aggregates, to ensure suitable + -- checking of expressions. + procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id); -- Perform attribute-reference-specific expansion @@ -139,6 +145,9 @@ package body Exp_SPARK is when N_Delta_Aggregate => Expand_SPARK_N_Delta_Aggregate (N); + when N_Aggregate => + Expand_SPARK_N_Aggregate (N); + when N_Expanded_Name | N_Identifier => @@ -418,6 +427,143 @@ package body Exp_SPARK is end if; end Expand_SPARK_Delta_Or_Update; + ------------------------------ + -- Expand_SPARK_N_Aggregate -- + ------------------------------ + + procedure Expand_SPARK_N_Aggregate (N : Node_Id) is + + -- Local subprograms + + procedure Parse_Named_Subp + (Subp : Subprogram_Kind_Id; + Key_Type : out Type_Kind_Id; + Element_Type : out Type_Kind_Id); + -- Retrieve key and element types from subprogram for named addition + + procedure Parse_Unnamed_Subp + (Subp : Subprogram_Kind_Id; + Element_Type : out Type_Kind_Id); + -- Retrieve element types from subprogram for unnamed addition + + procedure Wrap_For_Checks (Expr : N_Subexpr_Id; Typ : Type_Kind_Id); + -- If Expr might require a range check for conversion to type Typ, set + -- Do_Range_Check on Expr. In all cases, wrap Expr in a type conversion + -- if Typ is not the type of Expr already, for GNATprove to correctly + -- identity the target type for the range check and insert any other + -- checks. + + ---------------------- + -- Parse_Named_Subp -- + ---------------------- + + procedure Parse_Named_Subp + (Subp : Subprogram_Kind_Id; + Key_Type : out Type_Kind_Id; + Element_Type : out Type_Kind_Id) + is + Formal : Entity_Id := First_Formal (Subp); + begin + Next_Formal (Formal); + Key_Type := Etype (Formal); + Next_Formal (Formal); + Element_Type := Etype (Formal); + end Parse_Named_Subp; + + ------------------------ + -- Parse_Unnamed_Subp -- + ------------------------ + + procedure Parse_Unnamed_Subp + (Subp : Subprogram_Kind_Id; + Element_Type : out Type_Kind_Id) + is + Formal : Entity_Id := First_Formal (Subp); + begin + Next_Formal (Formal); + Element_Type := Etype (Formal); + end Parse_Unnamed_Subp; + + --------------------- + -- Wrap_For_Checks -- + --------------------- + + procedure Wrap_For_Checks (Expr : N_Subexpr_Id; Typ : Type_Kind_Id) is + begin + if Is_Scalar_Type (Typ) then + Apply_Scalar_Range_Check (Expr, Typ); + end if; + + Convert_To_And_Rewrite (Typ, Expr); + end Wrap_For_Checks; + + -- Local variables + + Typ : constant Entity_Id := Etype (N); + Asp : constant Node_Id := Find_Value_Of_Aspect (Typ, Aspect_Aggregate); + + Empty_Subp : Node_Id := Empty; + Add_Named_Subp : Node_Id := Empty; + Add_Unnamed_Subp : Node_Id := Empty; + New_Indexed_Subp : Node_Id := Empty; + Assign_Indexed_Subp : Node_Id := Empty; + Key_Type : Entity_Id; + Element_Type : Entity_Id; + + Assocs : constant List_Id := Component_Associations (N); + Exprs : constant List_Id := Expressions (N); + Choice : Node_Id; + Assoc : Node_Id; + Expr : Node_Id; + + -- Start of processing for Expand_SPARK_N_Aggregate + + begin + if Is_Container_Aggregate (N) then + + Parse_Aspect_Aggregate (Asp, + Empty_Subp, Add_Named_Subp, Add_Unnamed_Subp, + New_Indexed_Subp, Assign_Indexed_Subp); + + Assoc := First (Assocs); + Expr := First (Exprs); + + -- Both lists could be empty as in [] but they can't be both + -- non-empty. + pragma Assert (not (Present (Assoc) and then Present (Expr))); + + -- Deal with cases supported in GNATprove: + -- - named container aggregate which is not an indexed aggregate + -- - positional container aggregate + + if Present (Assoc) + and then Present (Add_Named_Subp) + then + Parse_Named_Subp (Entity (Add_Named_Subp), Key_Type, Element_Type); + + while Present (Assoc) loop + Choice := First (Choice_List (Assoc)); + + while Present (Choice) loop + Wrap_For_Checks (Choice, Key_Type); + Next (Choice); + end loop; + + Wrap_For_Checks (Expression (Assoc), Element_Type); + Next (Assoc); + end loop; + + elsif Present (Expr) then + Parse_Unnamed_Subp (Entity (Add_Unnamed_Subp), Element_Type); + + while Present (Expr) loop + Wrap_For_Checks (Expr, Element_Type); + Next (Expr); + end loop; + end if; + end if; + end Expand_SPARK_N_Aggregate; + ---------------------------------- -- Expand_SPARK_N_Freeze_Entity -- ---------------------------------- diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 2a31a11f9a2..f8922fed322 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -12349,14 +12349,15 @@ package body Sem_Util is function Is_Container_Aggregate (Exp : Node_Id) return Boolean is - function Is_Record_Aggregate return Boolean is (False); - -- ??? Unimplemented. Given an aggregate whose type is a - -- record type with specified Aggregate aspect, how do we - -- determine whether it is a record aggregate or a container - -- aggregate? If the code where the aggregate occurs can see only - -- a partial view of the aggregate's type then the aggregate - -- cannot be a record type; an aggregate of a private type has to - -- be a container aggregate. + function Is_Record_Aggregate return Boolean is + (Is_Parenthesis_Aggregate (Exp)); + -- Given an aggregate whose type is a record type with specified + -- Aggregate aspect, we determine whether it is a record aggregate or + -- a container aggregate by ckecking whether it uses parentheses () or + -- square brackets []. If the code where the aggregate occurs can see + -- only a partial view of the aggregate's type then the aggregate cannot + -- be a record type and must then use []; an aggregate of a private type + -- has to be a container aggregate and must then use []. begin return Nkind (Exp) = N_Aggregate