* [Ada] Add option for strict standard interpretation in Alfa mode
@ 2011-09-27 12:29 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2011-09-27 12:29 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 748 bytes --]
In Alfa mode for formal verification, the default is now to interpret compiler
permissions like GNAT does, with an option to have a stricter standard-only
interpretation. This is currently used for sizes of implicit base types of
integer types.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-09-27 Yannick Moy <moy@adacore.com>
* debug.adb (d.D): New option for strict Alfa mode.
* opt.ads (Strict_Alfa_Mode): New flag to interpret compiler
permissions as strictly as possible.
* sem_ch3.adb (Signed_Integer_Type_Declaration): In non-strict
Alfa mode, now, interpret ranges of base types like GNAT does; in
strict mode, simply change the range of the implicit base Itype.
* gnat1drv.adb: Update comments. Set Strict_Alfa_Mode.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 9135 bytes --]
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 179247)
+++ sem_ch3.adb (working copy)
@@ -19792,7 +19792,6 @@
-- Complete both implicit base and declared first subtype entities
Set_Etype (Implicit_Base, Base_Typ);
- Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
Set_Size_Info (Implicit_Base, (Base_Typ));
Set_RM_Size (Implicit_Base, RM_Size (Base_Typ));
Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Base_Typ));
@@ -19800,80 +19799,64 @@
Set_Ekind (T, E_Signed_Integer_Subtype);
Set_Etype (T, Implicit_Base);
- -- In formal verification mode, override partially the decisions above
- -- to restrict base type's range to the minimum allowed by RM 3.5.4,
- -- namely the smallest symmetric range around zero with a possible extra
- -- negative value that contains the subtype range. Keep Size, RM_Size
- -- and First_Rep_Item info, which should not be relied upon in formal
- -- verification.
+ -- In formal verification mode, restrict the base type's range to the
+ -- minimum allowed by RM 3.5.4, namely the smallest symmetric range
+ -- around zero with a possible extra negative value that contains the
+ -- subtype range. Keep Size, RM_Size and First_Rep_Item info, which
+ -- should not be relied upon in formal verification.
- if Alfa_Mode then
+ if Strict_Alfa_Mode then
+ declare
+ Sym_Hi_Val : Uint;
+ Sym_Lo_Val : Uint;
+ Dloc : constant Source_Ptr := Sloc (Def);
+ Lbound : Node_Id;
+ Ubound : Node_Id;
+ Bounds : Node_Id;
- -- If the range of the type is already symmetric with a possible
- -- extra negative value, leave it this way.
+ begin
+ -- If the subtype range is empty, the smallest base type range
+ -- is the symmetric range around zero containing Lo_Val and
+ -- Hi_Val.
- if UI_Le (Lo_Val, Hi_Val)
- and then (UI_Eq (Lo_Val, UI_Negate (Hi_Val))
- or else
- UI_Eq (Lo_Val, UI_Sub (UI_Negate (Hi_Val), Uint_1)))
- then
- null;
+ if UI_Gt (Lo_Val, Hi_Val) then
+ Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val));
+ Sym_Lo_Val := UI_Negate (Sym_Hi_Val);
- else
- declare
- Sym_Hi_Val : Uint;
- Sym_Lo_Val : Uint;
- Decl : Node_Id;
- Dloc : constant Source_Ptr := Sloc (Def);
- Lbound : Node_Id;
- Ubound : Node_Id;
-
- begin
- -- If the subtype range is empty, the smallest base type range
- -- is the symmetric range around zero containing Lo_Val and
- -- Hi_Val.
-
- if UI_Gt (Lo_Val, Hi_Val) then
- Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val));
- Sym_Lo_Val := UI_Negate (Sym_Hi_Val);
-
-- Otherwise, if the subtype range is not empty and Hi_Val has
-- the largest absolute value, Hi_Val is non negative and the
-- smallest base type range is the symmetric range around zero
-- containing Hi_Val.
- elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then
- Sym_Hi_Val := Hi_Val;
- Sym_Lo_Val := UI_Negate (Hi_Val);
+ elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then
+ Sym_Hi_Val := Hi_Val;
+ Sym_Lo_Val := UI_Negate (Hi_Val);
-- Otherwise, the subtype range is not empty, Lo_Val has the
-- strictly largest absolute value, Lo_Val is negative and the
-- smallest base type range is the symmetric range around zero
-- with an extra negative value Lo_Val.
- else
- Sym_Lo_Val := Lo_Val;
- Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1);
- end if;
+ else
+ Sym_Lo_Val := Lo_Val;
+ Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1);
+ end if;
- Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val);
- Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val);
- Set_Is_Static_Expression (Lbound);
- Set_Is_Static_Expression (Ubound);
+ Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val);
+ Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val);
+ Set_Is_Static_Expression (Lbound);
+ Set_Is_Static_Expression (Ubound);
+ Analyze_And_Resolve (Lbound, Any_Integer);
+ Analyze_And_Resolve (Ubound, Any_Integer);
- Decl := Make_Full_Type_Declaration (Dloc,
- Defining_Identifier => Implicit_Base,
- Type_Definition =>
- Make_Signed_Integer_Type_Definition (Dloc,
- Low_Bound => Lbound,
- High_Bound => Ubound));
+ Bounds := Make_Range (Dloc, Lbound, Ubound);
+ Set_Etype (Bounds, Base_Typ);
- Analyze (Decl);
- Set_Etype (Implicit_Base, Base_Type (Implicit_Base));
- Set_Etype (T, Base_Type (Implicit_Base));
- Insert_Before (Parent (Def), Decl);
- end;
- end if;
+ Set_Scalar_Range (Implicit_Base, Bounds);
+ end;
+
+ else
+ Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
end if;
Set_Size_Info (T, (Implicit_Base));
Index: debug.adb
===================================================================
--- debug.adb (revision 179247)
+++ debug.adb (working copy)
@@ -121,7 +121,7 @@
-- d.A Read/write Aspect_Specifications hash table to tree
-- d.B
-- d.C Generate concatenation call, do not generate inline code
- -- d.D
+ -- d.D Strict Alfa mode
-- d.E Force Alfa mode for gnat2why
-- d.F Alfa mode
-- d.G Precondition only mode for gnat2why
@@ -580,6 +580,9 @@
-- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases
-- where we would normally generate inline concatenation code.
+ -- d.D Strict Alfa mode. Interpret compiler permissions as strictly as
+ -- possible in Alfa mode.
+
-- d.E Force Alfa mode for gnat2why. In this mode, errors are issued for
-- all violations of Alfa in user code, and warnings are issued for
-- constructs not yet implemented in gnat2why.
Index: opt.ads
===================================================================
--- opt.ads (revision 179247)
+++ opt.ads (working copy)
@@ -1883,6 +1883,11 @@
-- generation of Why code for those parts of the input code that belong to
-- the Alfa subset of Ada. Set by debug flag -gnatd.F.
+ Strict_Alfa_Mode : Boolean := False;
+ -- Interpret compiler permissions as strictly as possible. E.g. base ranges
+ -- for integers are limited to the strict minimum with this option. Set by
+ -- debug flag -gnatd.D.
+
function Full_Expander_Active return Boolean;
pragma Inline (Full_Expander_Active);
-- Returns the value of (Expander_Active and not Alfa_Mode). This "flag"
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb (revision 179252)
+++ gnat1drv.adb (working copy)
@@ -392,6 +392,12 @@
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.
@@ -428,6 +434,8 @@
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;
@@ -473,13 +481,15 @@
Warning_Mode := Suppress;
- -- Suppress the generation of name tables for enumerations
- -- why???
+ -- 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
- -- why???
+ -- 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;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2011-09-27 10:03 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2011-09-27 12:29 [Ada] Add option for strict standard interpretation in Alfa mode Arnaud Charlet
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).