From patchwork Wed Jan 5 11:33:53 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: 1575619 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: bilbo.ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=eZ4bW+4h; dkim-atps=neutral Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Received: from sourceware.org (server2.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by bilbo.ozlabs.org (Postfix) with ESMTPS id 4JTSjc6cZXz9sPC for ; Wed, 5 Jan 2022 23:00:36 +1100 (AEDT) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 91E83385843B for ; Wed, 5 Jan 2022 12:00:34 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 91E83385843B DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1641384034; bh=QIRO3yAiCf2unMf5mN7JtVA7iaFz/7m6xU/PIM0ZDeU=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=eZ4bW+4h2ygEFjwWYkGTihFCQwdv2CdiCoXeTvrbYLccICuxiF908dh/9A+xSmp5f ZSf33t1HBuEQ2xsP6SK1u87bSgNrOEA5GJYYpRfOei6KbL8bgyRSrTq5ptOqZAEcqw Z/1/TJ+bKonTypz+dSbFYstekRc2ELAvPohW0BBA= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x436.google.com (mail-wr1-x436.google.com [IPv6:2a00:1450:4864:20::436]) by sourceware.org (Postfix) with ESMTPS id C108C3858438 for ; Wed, 5 Jan 2022 11:33:55 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org C108C3858438 Received: by mail-wr1-x436.google.com with SMTP id k18so45625361wrg.11 for ; Wed, 05 Jan 2022 03:33:55 -0800 (PST) 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=QIRO3yAiCf2unMf5mN7JtVA7iaFz/7m6xU/PIM0ZDeU=; b=8NSGCgbyJyeClD5nUU55O1hqVoohFHhGJx+cs7d7yPrcHoPGw2BrbSkaYXctluZo2S S7uw+16OxMLD/wl7WQHu9t4yxyXLbOQ+wxpEaZaGbg5diGM6sdbdmKm5mHgEzoVg1Wkb W7TE3+psGfBiet24PENZ+QpAQOI8GASEsfSAUYyBun/kIQv8Sx/w7Qnu0tJekJnJxmwh ob4fFwKH2XRVF9dquB8NDrIzuDzLYAHB/r7c+dprkp6l/sVimXdhhxoJR/6t+ymjwtP+ 2nMuojnx/PwHweU71cqSiql5SObfVdI/OztLTNs9ApPJAl09nEkTCE+r49NmSMhlZDe5 F9bw== X-Gm-Message-State: AOAM530f1gY57a1dKZA0YrGMow6v7S9kGNUTxGOHyV5jhgdbvthpvzwW B0szztYxF2vuOOKlaMxZoL465rnzcxrD9w== X-Google-Smtp-Source: ABdhPJy7hUPhlueFytgVi3IJsR+P19Dsl2lGtNubifXXIOf7fxl+bp8rod4PtR+PnijqDvqRcBYRmg== X-Received: by 2002:a5d:424c:: with SMTP id s12mr45385340wrr.465.1641382434904; Wed, 05 Jan 2022 03:33:54 -0800 (PST) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id k19sm2159828wmo.29.2022.01.05.03.33.54 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 05 Jan 2022 03:33:54 -0800 (PST) Date: Wed, 5 Jan 2022 11:33:53 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Expand controlling functions wrappers in GNATprove mode Message-ID: <20220105113353.GA2716107@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.1 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 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-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Piotr Trojanek Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" Enable expansion of wrappers for dispatching functions with controlling results in GNATprove mode. Without those wrappers the AST for calls to dispatching functions on parent and child objects is exactly the same and the GNATprove backend can't determine what function is actually called. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch3.ads (Make_Controlling_Function_Wrappers): Move declaration from body to spec, so it can be called by SPARK-specific expansion. * exp_ch3.adb (Make_Controlling_Function_Wrappers): Likewise. * exp_spark.adb (SPARK_Freeze_Type): Enable expansion of wrappers for function with controlling result types. diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -294,17 +294,6 @@ package body Exp_Ch3 is -- inherited. If the result is false, the init_proc and the discriminant -- checking functions of the parent can be reused by a derived type. - procedure Make_Controlling_Function_Wrappers - (Tag_Typ : Entity_Id; - Decl_List : out List_Id; - Body_List : out List_Id); - -- Ada 2005 (AI-391): Makes specs and bodies for the wrapper functions - -- associated with inherited functions with controlling results which - -- are not overridden. The body of each wrapper function consists solely - -- of a return statement whose expression is an extension aggregate - -- invoking the inherited subprogram's parent subprogram and extended - -- with a null association list. - function Make_Null_Procedure_Specs (Tag_Typ : Entity_Id) return List_Id; -- Ada 2005 (AI-251): Makes specs for null procedures associated with any -- null procedures inherited from an interface type that have not been diff --git a/gcc/ada/exp_ch3.ads b/gcc/ada/exp_ch3.ads --- a/gcc/ada/exp_ch3.ads +++ b/gcc/ada/exp_ch3.ads @@ -158,6 +158,17 @@ package Exp_Ch3 is -- initialized; if Variable_Comps is True then tags components located at -- variable positions of Target are initialized. + procedure Make_Controlling_Function_Wrappers + (Tag_Typ : Entity_Id; + Decl_List : out List_Id; + Body_List : out List_Id); + -- Ada 2005 (AI-391): Makes specs and bodies for the wrapper functions + -- associated with inherited functions with controlling results which + -- are not overridden. The body of each wrapper function consists solely + -- of a return statement whose expression is an extension aggregate + -- invoking the inherited subprogram's parent subprogram and extended + -- with a null association list. + procedure Make_Predefined_Primitive_Eq_Spec (Tag_Typ : Entity_Id; Predef_List : List_Id; diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -903,6 +903,9 @@ package body Exp_SPARK is Eq_Spec : Node_Id := Empty; Predef_List : List_Id; + Wrapper_Decl_List : List_Id; + Wrapper_Body_List : List_Id := No_List; + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; Saved_IGR : constant Node_Id := Ignored_Ghost_Region; -- Save the Ghost-related attributes to restore on exit @@ -961,6 +964,35 @@ package body Exp_SPARK is end if; end if; + if Ekind (Typ) = E_Record_Type + and then Is_Tagged_Type (Typ) + and then not Is_CPP_Class (Typ) + then + -- Ada 2005 (AI-391): For a nonabstract null extension, create + -- wrapper functions for each nonoverridden inherited function + -- with a controlling result of the type. The wrapper for such + -- a function returns an extension aggregate that invokes the + -- parent function. + + if Ada_Version >= Ada_2005 + and then not Is_Abstract_Type (Typ) + and then Is_Null_Extension (Typ) + then + Exp_Ch3.Make_Controlling_Function_Wrappers + (Typ, Wrapper_Decl_List, Wrapper_Body_List); + Insert_List_Before_And_Analyze (N, Wrapper_Decl_List); + end if; + + -- Ada 2005 (AI-391): If any wrappers were created for nonoverridden + -- inherited functions, then add their bodies to the AST, so they + -- will be processed like ordinary subprogram bodies (even though the + -- compiler adds them into the freezing action). + + if not Is_Interface (Typ) then + Insert_List_Before_And_Analyze (N, Wrapper_Body_List); + end if; + end if; + Restore_Ghost_Region (Saved_GM, Saved_IGR); end SPARK_Freeze_Type;