From patchwork Thu Oct 17 10:32:31 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 284150 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client did not present a certificate) by ozlabs.org (Postfix) with ESMTPS id 9C8EA2C00CD for ; Thu, 17 Oct 2013 21:32:46 +1100 (EST) 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=II4tEBm5Ku5Vyc/iBC4Bk4orDFrw42LLlF0KkacFmstrxDPUJj z8V785L5IPEG1xVU1DwDbpdIhgQBkJoMd2aCRQWpLF2lnX+TOgrv69vHBsF2xLeY AQC2EfSdA2rOhDHs5mjeFD6YiLl7Jm1lnvjpf4Uki3fiOGv1euO110cAc= 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=eerrr4XM28kmc49f2zvqmsroQJ8=; b=TFnIAOe06LyqMVo9BtaY Ib79rWvt7YwQghr3bAI9g4NJnhXoGhebY+CLdxW1nxFG+884hPoCJqTJOv5EQ0ZM ET5und0aCvrFeF/JLUJFXraNQ0r8IVpoflBpdLGob0nhW30RrXDnecj6AcmxIhZT CbxSvvIoMrkbcSQ02kTkw+g= Received: (qmail 12064 invoked by alias); 17 Oct 2013 10:32:35 -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 12029 invoked by uid 89); 17 Oct 2013 10:32:34 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham version=3.3.2 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 (AES256-SHA encrypted) ESMTPS; Thu, 17 Oct 2013 10:32:33 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 8DFA211675B; Thu, 17 Oct 2013 06:32:54 -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 2jTRELBVEzaR; Thu, 17 Oct 2013 06:32:54 -0400 (EDT) Received: from kwai.gnat.com (unknown [IPv6:2620:20:4000:0:a6ba:dbff:fe26:1f63]) by rock.gnat.com (Postfix) with ESMTP id 7C7C4116734; Thu, 17 Oct 2013 06:32:54 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 3DF923FB31; Thu, 17 Oct 2013 06:32:31 -0400 (EDT) Date: Thu, 17 Oct 2013 06:32:31 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Clean ups in SPARK mode Message-ID: <20131017103231.GA2010@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) 1) Remove special expansion of NOT IN operator in SPARK verification The special expansion for NOT IN operator in the SPARK formal verification mode is not needed anymore. Now removed. 2) Document additional requirements on tree for SPARK verification Formal verification of SPARK code is done in a special mode, in which the tree generated by the frontend must respect additional requirements. These are now described in a special section of sinfo.ads 2013-10-17 Yannick Moy * exp_spark.adb (Expand_SPARK): Remove special case for NOT IN operation. * sinfo.ads: Add special comment section to describe SPARK mode effect on tree. * exp_spark.ads: Remove comments, moved to sinfo.ads. Index: exp_spark.adb =================================================================== --- exp_spark.adb (revision 203568) +++ exp_spark.adb (working copy) @@ -25,7 +25,6 @@ with Atree; use Atree; with Einfo; use Einfo; -with Exp_Ch4; use Exp_Ch4; with Exp_Dbug; use Exp_Dbug; with Exp_Util; use Exp_Util; with Sem_Aux; use Sem_Aux; @@ -80,12 +79,6 @@ N_Identifier => Expand_Potential_Renaming (N); - -- A NOT IN B gets transformed to NOT (A IN B). This is the same - -- expansion used in the normal case, so shared the code. - - when N_Not_In => - Expand_N_Not_In (N); - when N_Object_Renaming_Declaration => Expand_SPARK_N_Object_Renaming_Declaration (N); Index: exp_spark.ads =================================================================== --- exp_spark.ads (revision 203568) +++ exp_spark.ads (working copy) @@ -30,54 +30,6 @@ -- Expand_SPARK is called directly by Expander.Expand. --- SPARK expansion has three main objectives: - --- 1. Perform limited expansion to explicit some Ada rules and constructs --- (translate 'Old and 'Result, replace renamings by renamed, insert --- conversions, expand actuals in calls to introduce temporaries, expand --- generics instantiations) - --- 2. Facilitate treatment for the formal verification back-end (fully --- qualify names, expand set membership, compute data dependences) - --- 3. Avoid the introduction of low-level code that is difficult to analyze --- formally, as typically done in the full expansion for high-level --- constructs (tasking, dispatching) - --- To fulfill objective 1, Expand_SPARK selectively expands some constructs. - --- To fulfill objective 2, the tree after SPARK expansion should be fully --- analyzed semantically. In particular, all expression must have their proper --- type, and semantic links should be set between tree nodes (partial to full --- view, etc.) Some kinds of nodes should be either absent, or can be ignored --- by the formal verification backend: - --- N_Object_Renaming_Declaration: can be ignored safely --- N_Expression_Function: absent (rewitten) --- N_Expression_With_Actions: absent (not generated) - --- SPARK cross-references are generated from the regular cross-references --- (used for browsing and code understanding) and additional references --- collected during semantic analysis, in particular on all --- dereferences. These SPARK cross-references are output in a separate section --- of ALI files, as described in spark_xrefs.adb. They are the basis for the --- computation of data dependences in the formal verification backend. This --- implies that all cross-references should be generated in this mode, even --- those that would not make sense from a user point-of-view, and that --- cross-references that do not lead to data dependences for subprograms can --- be safely ignored. - --- To support the formal verification of units parameterized by data, the --- value of deferred constants should not be considered as a compile-time --- constant at program locations where the full view is not visible. - --- To fulfill objective 3, Expand_SPARK does not expand features that are not --- formally analyzed (tasking), or for which formal analysis relies on the --- source level representation (dispatching, aspects, pragmas). However, these --- should be semantically analyzed, which sometimes requires the insertion of --- semantic pre-analysis, for example for subprogram contracts and pragma --- check/assert. - with Types; use Types; package Exp_SPARK is Index: sinfo.ads =================================================================== --- sinfo.ads (revision 203568) +++ sinfo.ads (working copy) @@ -508,6 +508,48 @@ -- simply ignore these nodes, since they are not relevant to the task -- of back annotating representation information. + ---------------- + -- SPARK Mode -- + ---------------- + + -- When a file is compiled in SPARK mode (-gnatd.F), a very light expansion + -- is performed and the analysis must generate a tree in a form that meets + -- additional requirements. + + -- The SPARK expansion does two transformations of the tree, that cannot be + -- postponed after the frontend semantic analysis: + + -- 1. Replace renamings by renamed (object/subprogram). This requires + -- introducing temporaries at the point of the renaming, which must be + -- properly analyzed. + + -- 2. Fully qualify entity names. This is needed to generate suitable + -- local effects/call-graphs in ALI files, with the completely + -- qualified names (in particular the suffix to distinguish homonyms). + + -- The tree after SPARK expansion should be fully analyzed semantically, + -- which sometimes requires the insertion of semantic pre-analysis, for + -- example for subprogram contracts and pragma check/assert. In particular, + -- all expression must have their proper type, and semantic links should be + -- set between tree nodes (partial to full view, etc.) Some kinds of nodes + -- should be either absent, or can be ignored by the formal verification + -- backend: + + -- N_Object_Renaming_Declaration: can be ignored safely + -- N_Expression_Function: absent (rewitten) + -- N_Expression_With_Actions: absent (not generated) + + -- SPARK cross-references are generated from the regular cross-references + -- (used for browsing and code understanding) and additional references + -- collected during semantic analysis, in particular on all dereferences. + -- These SPARK cross-references are output in a separate section of ALI + -- files, as described in spark_xrefs.adb. They are the basis for the + -- computation of data dependences in the formal verification backend. + -- This implies that all cross-references should be generated in this mode, + -- even those that would not make sense from a user point-of-view, and that + -- cross-references that do not lead to data dependences for subprograms + -- can be safely ignored. + ------------------------ -- Common Flag Fields -- ------------------------