From patchwork Tue Jul 9 07:52:00 2019 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: 1129612 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-504689-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="k3kYpK+9"; 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 45jZQ836q5z9sN1 for ; Tue, 9 Jul 2019 17:56:16 +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=vVwjPklstyv28vMb4p1pcO1u/OkKexQN4AnwSE3hi3BtwUJbqE aWlCT221lT59FYEOPMkVo8H9YT0exalGROUz3sAjpIb2OYO15oPkn8booy5qDHnA IvwckELnSAIYdtnuRIkyNCEJTM0JeZX4YzcHlrk87RLjA8COKysyX/bkk= 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=l7kqMk8CWCjBBowwApe28cwJM1o=; b=k3kYpK+9isJTGNAfaR+g P4Suv6ucOXFJtAPhp1r+z9y1eG4gVRkleRZJeTDilfSfRQm0AJoG6AtFm0cRgkkB dxkBtqFKP7SRzTqDYcjAdu7WNUwC848dg/V1H96m0qbkap9taAtEXGSFz3EE2s4t 3K/ll1HheNLA9ib8JW6aagg= Received: (qmail 97577 invoked by alias); 9 Jul 2019 07:52:32 -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 96563 invoked by uid 89); 9 Jul 2019 07:52:24 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.4 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, SPF_NEUTRAL autolearn=ham version=3.3.1 spammy= X-HELO: eggs.gnu.org Received: from eggs.gnu.org (HELO eggs.gnu.org) (209.51.188.92) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Tue, 09 Jul 2019 07:52:22 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hkkvC-0002Ak-TM for gcc-patches@gcc.gnu.org; Tue, 09 Jul 2019 03:52:21 -0400 Received: from rock.gnat.com ([2620:20:4000:0:a9e:1ff:fe9b:1d1]:35612) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1hkkvB-0001zF-1D for gcc-patches@gcc.gnu.org; Tue, 09 Jul 2019 03:52:18 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 026A8560D8; Tue, 9 Jul 2019 03:52:01 -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 w+B0B0H6J74D; Tue, 9 Jul 2019 03:52:00 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id E1242561A7; Tue, 9 Jul 2019 03:52:00 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id DE5E6618; Tue, 9 Jul 2019 03:52:00 -0400 (EDT) Date: Tue, 9 Jul 2019 03:52:00 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Expand type of static expressions in GNATprove mode Message-ID: <20190709075200.GA102853@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x X-Received-From: 2620:20:4000:0:a9e:1ff:fe9b:1d1 X-IsSubscribed: yes In the special mode for GNATprove, expand the type of static expressions like done during compilation, to both get suitable legality checks and increase the precision of the formal analysis. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-07-09 Yannick Moy gcc/ada/ * exp_util.adb (Expand_Subtype_From_Expr): Still expand the type of static expressions in GNATprove_Mode. * sem_ch3.adb (Analyze_Object_Declaration): Remove obsolete special case for GNATprove_Mode. --- gcc/ada/exp_util.adb +++ gcc/ada/exp_util.adb @@ -5067,9 +5067,15 @@ package body Exp_Util is -- may be constants that depend on the bounds of a string literal, both -- standard string types and more generally arrays of characters. - -- In GNATprove mode, these extra subtypes are not needed - - if GNATprove_Mode then + -- In GNATprove mode, these extra subtypes are not needed, unless Exp is + -- a static expression. In that case, the subtype will be constrained + -- while the original type might be unconstrained, so expanding the type + -- is necessary both for passing legality checks in GNAT and for precise + -- analysis in GNATprove. + + if GNATprove_Mode + and then not Is_Static_Expression (Exp) + then return; end if; --- gcc/ada/sem_ch3.adb +++ gcc/ada/sem_ch3.adb @@ -4592,14 +4592,6 @@ package body Sem_Ch3 is elsif Is_Interface (T) then null; - -- In GNATprove mode, Expand_Subtype_From_Expr does nothing. Thus, - -- we should prevent the generation of another Itype with the - -- same name as the one already generated, or we end up with - -- two identical types in GNATprove. - - elsif GNATprove_Mode then - null; - -- If the type is an unchecked union, no subtype can be built from -- the expression. Rewrite declaration as a renaming, which the -- back-end can handle properly. This is a rather unusual case,