[multiple changes]

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.

2012-12-05  Robert Dewar  <dewar@adacore.com>

	* sem_ch3.adb: Minor reformatting.

2012-12-05  Steve Baird  <baird@adacore.com>

	* sinfo.ads: Improve comments about SCIL-related node kinds and selector
	functions.

2012-12-05  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch10.adb (Build_Limited_Views): Even though the unit is
	not analyzed, place its entity on the name in the with clause,
	so that warnings on unused with-clause are properly supported
	for limited withs.

2012-12-05  Robert Dewar  <dewar@adacore.com>

	* gnat_ugn.texi: Update overflow description. Pragma
	Overflow_Checks changed to Overflow_Mode.

From-SVN: r194191
This commit is contained in:
Arnaud Charlet 2012-12-05 11:12:49 +01:00
parent 97948f419d
commit ceee0bde36
6 changed files with 252 additions and 226 deletions

View File

@ -1,3 +1,31 @@
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.
2012-12-05 Robert Dewar <dewar@adacore.com>
* sem_ch3.adb: Minor reformatting.
2012-12-05 Steve Baird <baird@adacore.com>
* sinfo.ads: Improve comments about SCIL-related node kinds and selector
functions.
2012-12-05 Ed Schonberg <schonberg@adacore.com>
* sem_ch10.adb (Build_Limited_Views): Even though the unit is
not analyzed, place its entity on the name in the with clause,
so that warnings on unused with-clause are properly supported
for limited withs.
2012-12-05 Robert Dewar <dewar@adacore.com>
* gnat_ugn.texi: Update overflow description. Pragma
Overflow_Checks changed to Overflow_Mode.
2012-12-05 Ed Schonberg <schonberg@adacore.com>
* sem_ch3.adb (Build_Derived_Private_Type): Handle properly a

View File

@ -201,7 +201,9 @@ procedure Gnat1drv is
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 @@ procedure Gnat1drv is
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 @@ procedure Gnat1drv is
-- 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 @@ procedure Gnat1drv is
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.

View File

@ -4362,11 +4362,11 @@ If no digits follow the @option{-gnato}, then it is equivalent to
causing all intermediate overflows to be handled in strict mode.
This switch also causes arithmetic overflow checking to be performed
(as though pragma @code{Unsuppress (Overflow_Check)} has been specified.
(as though pragma @code{Unsuppress (Overflow_Mode)} has been specified.
The default if no option @option{-gnato} is given is that overflow handling
is in @code{STRICT} mode (computations done using the base type), and that
overflow is not enabled.
overflow checking is suppressed.
Note that division by zero is a separate check that is not
controlled by this switch (division by zero checking is on by default).
@ -6931,94 +6931,47 @@ This switch cancels the effect of a previous @option{gnatp} switch.
@item -gnato??
@cindex @option{-gnato??} (@command{gcc})
@cindex Overflow checks
@cindex Overflow mode
@cindex Check, overflow
In @code{CHECKED} and @code{MINIMIZED} modes (@option{-gnato1} and
@option{-gnato2}), it enables overflow checking for integer operations.
In @code{ELIMINATED} mode (@option{-gnato3}), it enables arbitrary
precision arithmetic for integer operations. In all these modes, this
causes @value{EDITION} to generate slower and larger executable programs
by adding code to either check for overflow (resulting in raising
@code{Constraint_Error} as required by standard Ada semantics) or avoid
overflows. In mode @code{CHECKED}, overflow checks correspond to
situations in which the true value of the result of an operation may be
outside the base range of the result type. In mode @code{MINIMIZED},
overflow checks correspond to situations in which the true value of the
result of an operation may be outside the largest available machine
integer type (@code{Long_Long_Integer}). The following example shows the
distinction:
This switch controls the mode used for computing intermediate
arithmetic integer operations, and also enables overflow checking.
For a full description of overflow mode and checking control, see
the ``Overflow Check Handling in GNAT'' appendix in this
User's Guide.
@smallexample @c ada
procedure Add_And_Subtract (X : in out Integer; Y, Z : in Integer) is
begin
X := X + Y - Z;
end Add_And_Subtract;
Overflow checks are always enabled by this switch. The argument
controls the mode, using the codes
X1 : Integer := Integer'Last;
X2 : Integer range 1 .. 5 := 5;
@itemize
@item 1 = STRICT
In STRICT mode, intermediate operations are always done using the
base type, and overflow checking ensures that the result is within
the base type range.
Add_And_Subtract (X1, 1, 0); -- first addition and subtraction
Add_And_Subtract (X1, 1, 1); -- second addition and subtraction
Add_And_Subtract (X2, 1, 0); -- third addition and subtraction
Add_And_Subtract (X2, 1, 1); -- fourth addition and subtraction
@end smallexample
@item 2 = MINIMIZED
In MINIMIZED mode, overflows in intermediate operations are avoided
where possible by using a larger integer type for the computation
(typically @code{Long_Long_Integer). Overflow checking ensures that
the result fits in this larger integer type.
@noindent
Note that if explicit values are assigned at compile time, the compiler
may be able to detect overflow at compile time, in which case no actual
run-time checking code is required, and @code{Constraint_Error} will be
raised unconditionally, with or without @option{-gnato}.
@item 3 = ELIMINATED
In ELIMINATED mode, overflows in intermediate operations are avoided
by using multi-precision arithmetic. In this case, overflow checking
has no effect on intermediate operations (since overflow is impossible).
@end itemize
The first addition results in a value that is outside the base range of
@code{Integer}. In mode @code{CHECKED}, this raises
@code{Constraint_Error} at run time. In mode @code{MINIMIZED}, the
addition and subtraction are performed in type @code{Long_Long_Integer},
which is 64 bits for most machines. The compiler detects that no
overflow check is needed on these operations. The program still raises
@code{Constraint_Error} at run time because the resulting value is too
large to be assigned to @code{X}. The assignment results in a violation
of the explicit range constraint; such range checks are performed by
default, and are unaffected by @option{-gnato??}. In mode
@code{ELIMINATED}, the compiler uses type @code{Long_Long_Integer} for
intermediate computations, as this type is sufficient here to avoid all
overflows. When it is not sufficient, the compiler uses instead a
library for multiple-precision arithmetic, which may cause a significant
run-time overhead. The program still raises @code{Constraint_Error} at
run time when assigning to @code{X}.
If two digits are present after @option{-gnato} then the first digit
sets the mode for expressions outside assertions, and the second digit
sets the mode for expressions within assertions. Here assertions is used
in the technical sense (which includes for example precondition and
postcondition expressions).
The second addition results in a value that is outside the base range of
@code{Integer}. In mode @code{CHECKED}, this raises
@code{Constraint_Error} at run time, like in the previous case. In mode
@code{MINIMIZED}, the addition and subtraction are performed in type
@code{Long_Long_Integer}, resulting in a final value that fits in an
@code{Integer}. Thus, no @code{Constraint_Error} is raised. In mode
@code{ELIMINATED}, the compiler generates the same code as in mode
@code{MINIMIZED}, which avoids all overflows.
If one digit is present, the corresponding mode is applicable to both
expressions within and outside assertion expressions.
The third addition and subtraction result in an intermediate value and a
result well in the base range of @code{Integer}, so no
@code{Constraint_Error} exception is raised at run time in any
mode. However, the copy to @code{X2} when returning from the call to
@code{Add_And_Subtract} fails the range check for the type of
@code{X2}. Hence, a @code{Constraint_Error} exception is raised at run
time in all modes.
The fourth addition and subtraction result in an intermediate value and
a result well in the base range of @code{Integer}, and in a final value
that fits in the type of @code{X2}. Hence, no exception is raised at run
time in any mode.
Basically the rule is that in the default mode (@option{-gnato??} not
used), the generated code assures that all integer variables stay within
their declared ranges, or within the base range if there is no declared
range. This prevents any serious problems like indexes out of range for
array operations.
What is not checked in default mode is an overflow that results in an
in-range, but incorrect value. In the above example, the first
assignment to @code{X1} gives a result that is within the range of the
target variable, but the result is wrong in the sense that it is too
large to be represented correctly. Typically the assignment to @code{X1}
will result in wrap around to the largest negative number.
If no digits are present, the default is to enable overflow checks
and set STRICT mode for both kinds of expressions. This is compatible
with the use of @option{-gnato} in previous versions of GNAT.
@findex Machine_Overflows
Note that the @option{-gnato??} switch does not affect the code generated
@ -25718,10 +25671,11 @@ and for expressions appearing outside assertions.
The three modes are:
@itemize @bullet
@item @i{All intermediate overflows checked} (@code{STRICT})
@item @i{Use base type for intermediate operations} (@code{STRICT})
In this mode, all intermediate results for predefined arithmetic
operators must be in range of the base type. If this is not the
operators are computed using the base type, and the result must
be in range of the base type. If this is not the
case then either an exception is raised (if overflow checks are
enabled) or the execution is erroneous (if overflow checks are suppressed).
This is the normal default mode.
@ -25729,15 +25683,18 @@ The three modes are:
@item @i{Most intermediate overflows avoided} (@code{MINIMIZED})
In this mode, the compiler attempts to avoid intermediate overflows by
using @code{Long_Long_Integer} as the type in which arithmetic is
performed for predefined arithmetic operators. This is slightly more
using a larger integer type, typically @code{Long_Long_Integer},
as the type in which arithmetic is
performed for predefined arithmetic operators. This may be slightly more
expensive at
run time (compared to suppressing intermediate overflow checks), though
the cost is negligible on modern 64-bit machines. For the examples given
earlier, no intermediate overflows would have resulted in exceptions,
since the intermediate results are all in the range of
@code{Long_Long_Integer} (typically 64-bits on nearly all implementations
of GNAT).
of GNAT). In addition, if checks are enabled, this reduces the number of
checks that must be made, so this choice may actually result in an
improvement in space and time behavior.
However, there are cases where @code{Long_Long_Integer} is not large
enough, consider the following example:
@ -25813,12 +25770,12 @@ The three modes are:
@noindent
The desired mode of for handling intermediate overflow can be specified using
either the @code{Overflow_Checks} pragma or an equivalent compiler switch.
either the @code{Overflow_Mode} pragma or an equivalent compiler switch.
The pragma has the form
@cindex pragma @code{Overflow_Checks}
@cindex pragma @code{Overflow_Mode}
@smallexample @c ada
pragma Overflow_Checks ([General =>] MODE [, [Assertions =>] MODE]);
pragma Overflow_Mode ([General =>] MODE [, [Assertions =>] MODE]);
@end smallexample
@noindent
@ -25841,7 +25798,7 @@ are present, then @code{General} applies to expressions outside assertions,
and @code{Assertions} applies to expressions within assertions. For example:
@smallexample @c ada
pragma Overflow_Checks
pragma Overflow_Mode
(General => Minimized, Assertions => Eliminated);
@end smallexample
@ -25856,13 +25813,13 @@ the extra overhead for assertion expressions to ensure that
the behavior at run time matches the expected mathematical
behavior.
The @code{Overflow_Checks} pragma has the same scoping and placement
The @code{Overflow_Mode} pragma has the same scoping and placement
rules as pragma @code{Suppress}, so it can occur either as a
configuration pragma, specifying a default for the whole
program, or in a declarative scope, where it applies to the
remaining declarations and statements in that scope.
Note that pragma @code{Overflow_Checks} does not affect whether
Note that pragma @code{Overflow_Mode} does not affect whether
overflow checks are enabled or suppressed. It only controls the
method used to compute intermediate values. To control whether
overflow checking is enabled or suppressed, use pragma @code{Suppress}
@ -25878,7 +25835,7 @@ Here `@code{?}' is one of the digits `@code{1}' through `@code{3}':
@itemize @bullet
@item @code{1}:
all intermediate overflows checked (@code{CHECKED})
use base type for intermediate operations (@code{STRICT})
@item @code{2}:
minimize intermediate overflows (@code{MINIMIZED})
@item @code{3}:
@ -25893,12 +25850,13 @@ of the example pragma above would be @option{-gnato23}.
If no digits follow the @option{-gnato}, then it is equivalent to
@option{-gnato11},
causing all intermediate overflows to be checked.
causing all intermediate operations to be computed using the base
type (@code{STRICT} mode).
In addition to setting the mode used for computation of intermediate
results, the @code{-gnato} switch also enables overflow checking (which
is suppressed by default). It thus combines the effect of using
a pragma @code{Overflow_Checks} and pragma @code{Unsuppress}.
a pragma @code{Overflow_Mode} and pragma @code{Unsuppress}.
@c -------------------------

View File

@ -5716,6 +5716,17 @@ package body Sem_Ch10 is
raise Program_Error;
end case;
-- The limited unit is not analyzed but the with clause must be
-- minimally decorated so that checks on unused with clause also work
-- with limited with clauses.
if Is_Entity_Name (Name (N)) then
Set_Entity (Name (N), P);
elsif Nkind (Name (N)) = N_Selected_Component then
Set_Entity (Selector_Name (Name (N)), P);
end if;
-- Check if the chain is already built
Spec := Specification (Unit (Library_Unit (N)));

View File

@ -6512,23 +6512,27 @@ package body Sem_Ch3 is
then
Append_Elmt (Derived_Type, Private_Dependents (Parent_Type));
-- Check for unusual case where a type completed by a private
-- derivation occurs within a package nested in a child unit, and
-- the parent is declared in an ancestor.
if Is_Child_Unit (Scope (Current_Scope))
and then Is_Completion
and then In_Private_Part (Current_Scope)
and then Scope (Parent_Type) /= Current_Scope
-- Note that if the parent has a completion in the private part,
-- (which is itself a derivation from some other private type)
-- it is that completion that is visible, there is no full view
-- available, and no special processing is needed.
and then Present (Full_View (Parent_Type))
then
-- This is the unusual case where a type completed by a private
-- derivation occurs within a package nested in a child unit, and
-- the parent is declared in an ancestor. In this case, the full
-- view of the parent type will become visible in the body of
-- the enclosing child, and only then will the current type be
-- possibly non-private. We build a underlying full view that
-- will be installed when the enclosing child body is compiled.
-- Note that if the parent has a completion in the private part,
-- (which is itself a derivation from some other private type)
-- it is that completion that is visible, there is no full view
-- view available, and no special processing is needed.
-- In this case, the full view of the parent type will become
-- visible in the body of the enclosing child, and only then will
-- the current type be possibly non-private. We build an
-- underlying full view that will be installed when the enclosing
-- child body is compiled.
Full_Der :=
Make_Defining_Identifier

View File

@ -7336,29 +7336,37 @@ package Sinfo is
-- SCIL nodes are special nodes added to the tree when the CodePeer
-- mode is active. They help the CodePeer backend to locate nodes that
-- require special processing.
-- Major documentation on the general design of the SCIL interface, and
-- in particular detailed description of these nodes is missing and is
-- to be supplied in the future, when the design has finalized ???
-- Meanwhile these nodes should be considered in experimental form, and
-- should be ignored by all code generating back ends. ???
-- require special processing. They are only generated if SCIL
-- generation is enabled. A standard tree-walk will not encounter
-- these nodes even if they are present; these nodes are only
-- accessible via the function SCIL_LL.Get_SCIL_Node.
-- N_SCIL_Dispatch_Table_Tag_Init
-- Sloc references a node for a tag initialization
-- SCIL_Entity (Node4-Sem)
--
-- An N_SCIL_Dispatch_Table_Tag_Init node may be associated (via
-- Get_SCIL_Node) with the N_Object_Declaration node corresponding to
-- the declaration of the dispatch table for a tagged type.
-- N_SCIL_Dispatching_Call
-- Sloc references the node of a dispatching call
-- SCIL_Target_Prim (Node2-Sem)
-- SCIL_Entity (Node4-Sem)
-- SCIL_Controlling_Tag (Node5-Sem)
--
-- An N_Scil_Dispatching call node may be associated (via Get_SCIL_Node)
-- with the N_Procedure_Call or N_Function_Call node (or a rewriting
-- thereof) corresponding to a dispatching call.
-- N_SCIL_Membership_Test
-- Sloc references the node of a membership test
-- SCIL_Tag_Value (Node5-Sem)
-- SCIL_Entity (Node4-Sem)
--
-- An N_Scil_Membership_Test node may be associated (via Get_SCIL_Node)
-- with the N_In node (or a rewriting thereof) corresponding to a
-- classwide membership test.
---------------------
-- Subprogram_Info --