From patchwork Mon Sep 25 09:52:20 2017 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: 818151 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-462866-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="q2rP1MoC"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 3y0zsC67Xwz9t5c for ; Mon, 25 Sep 2017 19:52:31 +1000 (AEST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=KQmdJM1GPxqPDEQ7TyyS2nVk/DhQxVMNAIYOp02ZOge1gNtfvt 0+3PCf1zfxVlwhxI11vfCfV+J7KCVdZR/ptHn71j9vry9UDkPvk6X10AEXn/cmBw tzRQiW+GPOZqrjXYO5JmOe9NC1Rd0kZ21W26jXEJsa9O0C2i5AdmBv8yU= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=y+uLarbsqoh/mLaG8v7pNJGkosQ=; b=q2rP1MoC2rEiclScS5xO XIGK3y9Bniw2j7uQyboA6JqJ+xWX+kXDbMM3QkK+8wvXjfC/w4bJoIhGVFHdlQSL cX5FKfcG+mDTC+IvNWHNhLn62hJP+KgK33+AY+rxbGr0NZm/xiDyPw8hs2G4Lhl4 vvYUWlf5oxctZAAH+el6S5E= Received: (qmail 88535 invoked by alias); 25 Sep 2017 09:52:24 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 88203 invoked by uid 89); 25 Sep 2017 09:52:23 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.2 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=rx, RX, UD:X, RY X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Mon, 25 Sep 2017 09:52:21 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 3F6C25602A; Mon, 25 Sep 2017 05:52:20 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 2v0mx4tdinGm; Mon, 25 Sep 2017 05:52:20 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 2EF3156006; Mon, 25 Sep 2017 05:52:20 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 2DF9A518; Mon, 25 Sep 2017 05:52:20 -0400 (EDT) Date: Mon, 25 Sep 2017 05:52:20 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Insert explicit dereference in GNATprove mode for pointer analysis Message-ID: <20170925095220.GA13149@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes Safe pointer analysis in GNATprove mode depends on explicit dereferences being present in the tree. Insert them where needed on access to components in the special expansion performed in GNATprove mode. The following code is now analysed without errors in GNATprove mode (with -gnatd.F) with the special debug switch to trigger safe pointer analysis (with -gnatdF): $ gcc -c -gnatd.F -gnatdF ptr.adb 1. procedure Ptr with SPARK_Mode is 2. type PInt is access Integer; 3. type Rec is record 4. X, Y : PInt; 5. end record; 6. type PRec is access Rec; 7. type Arr is array (1..10) of PRec; 8. type PArr is access Arr; 9. R : PRec := new Rec; 10. A : PArr := new Arr; 11. begin 12. R.X := R.Y; 13. A(1).X := A(2).Y; 14. end Ptr; Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-25 Yannick Moy * exp_spark.adb (Expand_SPARK_Indexed_Component, Expand_SPARK_Selected_Component): New procedures to insert explicit dereference if required. (Expand_SPARK): Call the new procedures. Index: exp_spark.adb =================================================================== --- exp_spark.adb (revision 253141) +++ exp_spark.adb (working copy) @@ -58,6 +58,9 @@ procedure Expand_SPARK_Freeze_Type (E : Entity_Id); -- Build the DIC procedure of a type when needed, if not already done + procedure Expand_SPARK_Indexed_Component (N : Node_Id); + -- Insert explicit dereference if required + procedure Expand_SPARK_N_Object_Declaration (N : Node_Id); -- Perform object-declaration-specific expansion @@ -67,6 +70,9 @@ procedure Expand_SPARK_Op_Ne (N : Node_Id); -- Rewrite operator /= based on operator = when defined explicitly + procedure Expand_SPARK_Selected_Component (N : Node_Id); + -- Insert explicit dereference if required + ------------------ -- Expand_SPARK -- ------------------ @@ -138,6 +144,12 @@ Expand_SPARK_Freeze_Type (Entity (N)); end if; + when N_Indexed_Component => + Expand_SPARK_Indexed_Component (N); + + when N_Selected_Component => + Expand_SPARK_Selected_Component (N); + -- In SPARK mode, no other constructs require expansion when others => @@ -264,6 +276,20 @@ end if; end Expand_SPARK_Freeze_Type; + ------------------------------------ + -- Expand_SPARK_Indexed_Component -- + ------------------------------------ + + procedure Expand_SPARK_Indexed_Component (N : Node_Id) is + P : constant Node_Id := Prefix (N); + T : constant Entity_Id := Etype (P); + begin + if Is_Access_Type (T) then + Insert_Explicit_Dereference (P); + Analyze_And_Resolve (P, Designated_Type (T)); + end if; + end Expand_SPARK_Indexed_Component; + --------------------------------------- -- Expand_SPARK_N_Object_Declaration -- --------------------------------------- @@ -445,4 +471,31 @@ end if; end Expand_SPARK_Potential_Renaming; + ------------------------------------- + -- Expand_SPARK_Selected_Component -- + ------------------------------------- + + procedure Expand_SPARK_Selected_Component (N : Node_Id) is + P : constant Node_Id := Prefix (N); + Ptyp : constant Entity_Id := Underlying_Type (Etype (P)); + begin + if Present (Ptyp) + and then Is_Access_Type (Ptyp) + then + -- First set prefix type to proper access type, in case it currently + -- has a private (non-access) view of this type. + + Set_Etype (P, Ptyp); + + Insert_Explicit_Dereference (P); + Analyze_And_Resolve (P, Designated_Type (Ptyp)); + + if Ekind (Etype (P)) = E_Private_Subtype + and then Is_For_Access_Subtype (Etype (P)) + then + Set_Etype (P, Base_Type (Etype (P))); + end if; + end if; + end Expand_SPARK_Selected_Component; + end Exp_SPARK;