From patchwork Wed Dec 5 10:13:12 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 203816 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]) by ozlabs.org (Postfix) with SMTP id A2EF02C00C4 for ; Wed, 5 Dec 2012 21:13:22 +1100 (EST) Comment: DKIM? See http://www.dkim.org DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=gcc.gnu.org; s=default; x=1355307202; h=Comment: DomainKey-Signature:Received:Received:Received:Received:Received: Received:Received:Date:From:To:Cc:Subject:Message-ID: MIME-Version:Content-Type:Content-Disposition:User-Agent: Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:Sender:Delivered-To; bh=yhnzRaNwsvxqrNP2efLi dVdt2OE=; b=IpTGFqeBHmftaymGQj7XR+nT7syxF0zNFtWo2JtpsOUo5Rw3sjPU tUoXBF7PqLHUyROHbFmkdVn9KFgL75q17cADM6cylZCU9HWU2SqZegDXr4UX+xwX Pt6z1qfxFOCFqtN4BzSJCnvZmsYdTB2+K//GpPFM96+Mw3RLJ4BZRC0= Comment: DomainKeys? See http://antispam.yahoo.com/domainkeys DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=default; d=gcc.gnu.org; h=Received:Received:X-SWARE-Spam-Status:X-Spam-Check-By:Received:Received:Received:Received:Received:Date:From:To:Cc:Subject:Message-ID:MIME-Version:Content-Type:Content-Disposition:User-Agent:Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive:List-Post:List-Help:Sender:Delivered-To; b=UfDnElleWFi9LmR8/YTl8nEVixo7Du/AUKeXaCp57z2Naf8Coyg/VXsHGzG18g CgeZR7gQbg9+MbjqnBipk12LS3AcpSLAtPygPaUSqQFvH9kX24cOt3XMocdbBGgs 4HqwiZoQFEHY+sogPnnAyFgHMw9+Cn8D4jeRoacfAY854=; Received: (qmail 6279 invoked by alias); 5 Dec 2012 10:13:19 -0000 Received: (qmail 6271 invoked by uid 22791); 5 Dec 2012 10:13:18 -0000 X-SWARE-Spam-Status: No, hits=-1.9 required=5.0 tests=AWL, BAYES_00, RCVD_IN_HOSTKARMA_NO X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Wed, 05 Dec 2012 10:13:13 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 784D81C623C; Wed, 5 Dec 2012 05:13:12 -0500 (EST) 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 kmgDw+MYZ+WZ; Wed, 5 Dec 2012 05:13:12 -0500 (EST) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 4E1381C616B; Wed, 5 Dec 2012 05:13:12 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 491CA919E3; Wed, 5 Dec 2012 05:13:12 -0500 (EST) Date: Wed, 5 Dec 2012 05:13:12 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Set overflow check mode to STRICT in Alfa mode, unless set already Message-ID: <20121205101312.GA28336@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) 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 In order to be able to rely on frontend marks for checks in formal verification (Alfa mode), we need to set the overflow mode to STRICT, thus forcing checking formal verification when the user wants no run-time checks. Modes MINIMIZED and ELIMINATED are respected if set by the user. Tested on x86_64-pc-linux-gnu, committed on trunk 2012-12-05 Yannick Moy * gnat1drv.adb (Adjust_Global_Switches): Move setting of flags for Alfa mode before general treatment of flags, so that overflow checks settings are set appropriately in Alfa mode. Also set the mode to STRICT in Alfa mode if not already set by the user. Index: gnat1drv.adb =================================================================== --- gnat1drv.adb (revision 194190) +++ gnat1drv.adb (working copy) @@ -201,7 +201,9 @@ Dynamic_Elaboration_Checks := False; - -- Set STRICT mode for overflow checks if not set explicitly + -- Set STRICT mode for overflow checks if not set explicitly. This + -- prevents suppressing of overflow checks by default, in code down + -- below. if Suppress_Options.Overflow_Checks_General = Not_Set then Suppress_Options.Overflow_Checks_General := Strict; @@ -268,6 +270,129 @@ Try_Semantics := True; end if; + -- Set switches for formal verification mode + + if Debug_Flag_Dot_VV then + Formal_Extensions := True; + end if; + + if Debug_Flag_Dot_FF then + Alfa_Mode := True; + + -- Set strict standard interpretation of compiler permissions + + if Debug_Flag_Dot_DD then + Strict_Alfa_Mode := True; + end if; + + -- Turn off inlining, which would confuse formal verification output + -- and gain nothing. + + Front_End_Inlining := False; + Inline_Active := False; + + -- Disable front-end optimizations, to keep the tree as close to the + -- source code as possible, and also to avoid inconsistencies between + -- trees when using different optimization switches. + + Optimization_Level := 0; + + -- Enable some restrictions systematically to simplify the generated + -- code (and ease analysis). Note that restriction checks are also + -- disabled in Alfa mode, see Restrict.Check_Restriction, and user + -- specified Restrictions pragmas are ignored, see + -- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings. + + Restrict.Restrictions.Set (No_Initialize_Scalars) := True; + + -- Note: at this point we used to suppress various checks, but that + -- is not what we want. We need the semantic processing for these + -- checks (which will set flags like Do_Overflow_Check, showing the + -- points at which potential checks are required semantically). We + -- don't want the expansion associated with these checks, but that + -- happens anyway because this expansion is simply not done in the + -- Alfa version of the expander. + + -- Turn off dynamic elaboration checks: generates inconsistencies in + -- trees between specs compiled as part of a main unit or as part of + -- a with-clause. + + Dynamic_Elaboration_Checks := False; + + -- Set STRICT mode for overflow checks if not set explicitly. This + -- prevents suppressing of overflow checks by default, in code down + -- below. + + if Suppress_Options.Overflow_Checks_General = Not_Set then + Suppress_Options.Overflow_Checks_General := Strict; + Suppress_Options.Overflow_Checks_Assertions := Strict; + end if; + + -- Kill debug of generated code, since it messes up sloc values + + Debug_Generated_Code := False; + + -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD) + -- as it is needed for computing effects of subprograms in the formal + -- verification backend. + + Xref_Active := True; + + -- Polling mode forced off, since it generates confusing junk + + Polling_Required := False; + + -- Set operating mode to Generate_Code, but full front-end expansion + -- is not desirable in Alfa mode, so a light expansion is performed + -- instead. + + Operating_Mode := Generate_Code; + + -- Skip call to gigi + + Debug_Flag_HH := True; + + -- Disable Expressions_With_Actions nodes + + -- The gnat2why backend does not deal with Expressions_With_Actions + -- in all places (in particular assertions). It is difficult to + -- determine in the frontend which cases are allowed, so we disable + -- Expressions_With_Actions entirely. Even in the cases where + -- gnat2why deals with Expressions_With_Actions, it is easier to + -- deal with the original constructs (quantified, conditional and + -- case expressions) instead of the rewritten ones. + + Use_Expression_With_Actions := False; + + -- Enable assertions and debug pragmas, since they give valuable + -- extra information for formal verification. + + Assertions_Enabled := True; + Debug_Pragmas_Enabled := True; + + -- Turn off style check options since we are not interested in any + -- front-end warnings when we are getting Alfa output. + + Reset_Style_Check_Options; + + -- Suppress compiler warnings, since what we are interested in here + -- is what formal verification can find out. + + Warning_Mode := Suppress; + + -- Suppress the generation of name tables for enumerations, which are + -- not needed for formal verification, and fall outside the Alfa + -- subset (use of pointers). + + Global_Discard_Names := True; + + -- Suppress the expansion of tagged types and dispatching calls, + -- which lead to the generation of non-Alfa code (use of pointers), + -- which is more complex to formally verify than the original source. + + Tagged_Type_Expansion := False; + end if; + -- Set Configurable_Run_Time mode if system.ads flag set if Targparm.Configurable_Run_Time_On_Target or Debug_Flag_YY then @@ -335,8 +460,8 @@ -- Set proper status for overflow check mechanism - -- If already set (by -gnato or above in CodePeer mode) then we have - -- nothing to do. + -- If already set (by -gnato or above in Alfa or CodePeer mode) then we + -- have nothing to do. if Opt.Suppress_Options.Overflow_Checks_General /= Not_Set then null; @@ -430,114 +555,6 @@ Back_End_Handles_Limited_Types := False; end if; - -- Set switches for formal verification mode - - if Debug_Flag_Dot_VV then - Formal_Extensions := True; - end if; - - if Debug_Flag_Dot_FF then - Alfa_Mode := True; - - -- Set strict standard interpretation of compiler permissions - - if Debug_Flag_Dot_DD then - Strict_Alfa_Mode := True; - end if; - - -- Turn off inlining, which would confuse formal verification output - -- and gain nothing. - - Front_End_Inlining := False; - Inline_Active := False; - - -- Disable front-end optimizations, to keep the tree as close to the - -- source code as possible, and also to avoid inconsistencies between - -- trees when using different optimization switches. - - Optimization_Level := 0; - - -- Enable some restrictions systematically to simplify the generated - -- code (and ease analysis). Note that restriction checks are also - -- disabled in Alfa mode, see Restrict.Check_Restriction, and user - -- specified Restrictions pragmas are ignored, see - -- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings. - - Restrict.Restrictions.Set (No_Initialize_Scalars) := True; - - -- Note: at this point we used to suppress various checks, but that - -- is not what we want. We need the semantic processing for these - -- checks (which will set flags like Do_Overflow_Check, showing the - -- points at which potential checks are required semantically). We - -- don't want the expansion associated with these checks, but that - -- happens anyway because this expansion is simply not done in the - -- Alfa version of the expander. - - -- Kill debug of generated code, since it messes up sloc values - - Debug_Generated_Code := False; - - -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD) - -- as it is needed for computing effects of subprograms in the formal - -- verification backend. - - Xref_Active := True; - - -- Polling mode forced off, since it generates confusing junk - - Polling_Required := False; - - -- Set operating mode to Generate_Code, but full front-end expansion - -- is not desirable in Alfa mode, so a light expansion is performed - -- instead. - - Operating_Mode := Generate_Code; - - -- Skip call to gigi - - Debug_Flag_HH := True; - - -- Disable Expressions_With_Actions nodes - - -- The gnat2why backend does not deal with Expressions_With_Actions - -- in all places (in particular assertions). It is difficult to - -- determine in the frontend which cases are allowed, so we disable - -- Expressions_With_Actions entirely. Even in the cases where - -- gnat2why deals with Expressions_With_Actions, it is easier to - -- deal with the original constructs (quantified, conditional and - -- case expressions) instead of the rewritten ones. - - Use_Expression_With_Actions := False; - - -- Enable assertions and debug pragmas, since they give valuable - -- extra information for formal verification. - - Assertions_Enabled := True; - Debug_Pragmas_Enabled := True; - - -- Turn off style check options since we are not interested in any - -- front-end warnings when we are getting Alfa output. - - Reset_Style_Check_Options; - - -- Suppress compiler warnings, since what we are interested in here - -- is what formal verification can find out. - - Warning_Mode := Suppress; - - -- Suppress the generation of name tables for enumerations, which are - -- not needed for formal verification, and fall outside the Alfa - -- subset (use of pointers). - - Global_Discard_Names := True; - - -- Suppress the expansion of tagged types and dispatching calls, - -- which lead to the generation of non-Alfa code (use of pointers), - -- which is more complex to formally verify than the original source. - - Tagged_Type_Expansion := False; - end if; - -- If the inlining level has not been set by the user, compute it from -- the optimization level: 1 at -O1/-O2 (and -Os), 2 at -O3 and above.