Patchwork [Ada] Set overflow check mode to STRICT in Alfa mode, unless set already

login
register
mail settings
Submitter Arnaud Charlet
Date Dec. 5, 2012, 10:13 a.m.
Message ID <20121205101312.GA28336@adacore.com>
Download mbox | patch
Permalink /patch/203816/
State New
Headers show

Comments

Arnaud Charlet - Dec. 5, 2012, 10:13 a.m.
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  <moy@adacore.com>

	* 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.

Patch

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.