[Ada] Set special options for ALFA mode (formal verification)
Arnaud Charlet
charlet@adacore.com
Fri Aug 5 13:47:00 GMT 2011
In ALFA mode, compiler is working in a special way in which it should believe
it generates actual object code, while it is not; warnings should not be
issued; checks should not be inserted in the code; various pragmas should be
ignored. Changing the startup of frontend to do that.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-05 Yannick Moy <moy@adacore.com>
* debug.adb: Remove use of -gnatd.D.
* gnat1drv.adb (Adjust_Global_Switches): adjust switches for ALFA mode
* opt.ads: Simplify variables for ALFA mode, to keep one only
* restrict.adb, sem_prag.adb: Adapt treatment done for CodePeer mode
to ALFA mode.
-------------- next part --------------
Index: debug.adb
===================================================================
--- debug.adb (revision 177351)
+++ debug.adb (working copy)
@@ -122,8 +122,8 @@
-- d.B
-- d.C Generate concatenation call, do not generate inline code
-- d.D
- -- d.E SPARK generation mode
- -- d.F Why generation mode
+ -- d.E
+ -- d.F ALFA mode
-- d.G
-- d.H
-- d.I SCIL generation mode
@@ -580,12 +580,10 @@
-- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases
-- where we would normally generate inline concatenation code.
- -- d.E SPARK generation mode. Generate intermediate code for the sake of
- -- formal verification through SPARK and the SPARK toolset.
+ -- d.F ALFA mode. Generate AST in a form suitable for formal verification,
+ -- as well as additional cross reference information in ALI files to
+ -- compute effects of subprograms.
- -- d.F Why generation mode. Generate intermediate code for the sake of
- -- formal verification through Why and the Why VC generator.
-
-- d.I Generate SCIL mode. Generate intermediate code for the sake of
-- of static analysis tools, and ensure additional tree consistency
-- between different compilations of specs.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 177395)
+++ sem_prag.adb (working copy)
@@ -5059,9 +5059,9 @@
-- Start of processing for Process_Restrictions_Or_Restriction_Warnings
begin
- -- Ignore all Restrictions pragma in CodePeer mode
+ -- Ignore all Restrictions pragma in CodePeer and ALFA modes
- if CodePeer_Mode then
+ if CodePeer_Mode or else ALFA_Mode then
return;
end if;
@@ -5283,10 +5283,13 @@
-- Start of processing for Process_Suppress_Unsuppress
begin
- -- Ignore pragma Suppress/Unsuppress in codepeer mode on user code:
- -- we want to generate checks for analysis purposes, as set by -gnatC
+ -- Ignore pragma Suppress/Unsuppress in CodePeer and ALFA modes on
+ -- user code: we want to generate checks for analysis purposes, as
+ -- set respectively by -gnatC and -gnatd.F
- if CodePeer_Mode and then Comes_From_Source (N) then
+ if (CodePeer_Mode or else ALFA_Mode)
+ and then Comes_From_Source (N)
+ then
return;
end if;
@@ -9444,11 +9447,12 @@
Check_Valid_Configuration_Pragma;
Check_Restriction (No_Initialize_Scalars, N);
- -- Initialize_Scalars creates false positives in CodePeer,
- -- so ignore this pragma in this mode.
+ -- Initialize_Scalars creates false positives in CodePeer, and
+ -- incorrect negative results in ALFA mode, so ignore this pragma
+ -- in these modes.
if not Restriction_Active (No_Initialize_Scalars)
- and then not CodePeer_Mode
+ and then not (CodePeer_Mode or else ALFA_Mode)
then
Init_Or_Norm_Scalars := True;
Initialize_Scalars := True;
@@ -9475,10 +9479,10 @@
when Pragma_Inline_Always =>
GNAT_Pragma;
- -- Pragma always active unless in CodePeer mode, since this causes
- -- walk order issues.
+ -- Pragma always active unless in CodePeer or ALFA mode, since
+ -- this causes walk order issues.
- if not CodePeer_Mode then
+ if not (CodePeer_Mode or else ALFA_Mode) then
Process_Inline (True);
end if;
@@ -10917,10 +10921,11 @@
Check_Arg_Count (0);
Check_Valid_Configuration_Pragma;
- -- Normalize_Scalars creates false positives in CodePeer, so
- -- ignore this pragma in this mode.
+ -- Normalize_Scalars creates false positives in CodePeer, and
+ -- incorrect negative results in ALFA mode, so ignore this pragma
+ -- in these modes.
- if not CodePeer_Mode then
+ if not (CodePeer_Mode or else ALFA_Mode) then
Normalize_Scalars := True;
Init_Or_Norm_Scalars := True;
end if;
@@ -11287,9 +11292,9 @@
-- In the context of static code analysis, we do not need
-- complex front-end expansions related to pragma Pack,
- -- so disable handling of pragma Pack in this case.
+ -- so disable handling of pragma Pack in these cases.
- if CodePeer_Mode then
+ if CodePeer_Mode or else ALFA_Mode then
null;
-- Don't attempt any packing for VM targets. We possibly
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb (revision 177334)
+++ gnat1drv.adb (working copy)
@@ -390,17 +390,86 @@
Back_End_Handles_Limited_Types := False;
end if;
- -- Set switches for formal verification modes
+ -- Set switches for formal verification mode
- if Debug_Flag_Dot_EE then
- ALFA_Through_SPARK_Mode := True;
- end if;
+ if Debug_Flag_Dot_FF then
- if Debug_Flag_Dot_FF then
- ALFA_Through_Why_Mode := True;
+ ALFA_Mode := True;
+
+ -- 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;
+
+ -- Suppress all language checks since they are handled implicitly by
+ -- the formal verification backend.
+ -- Turn off dynamic elaboration checks.
+ -- Turn off alignment checks.
+ -- Turn off validity checking.
+
+ Suppress_Options := (others => True);
+ Enable_Overflow_Checks := False;
+ Dynamic_Elaboration_Checks := False;
+ Reset_Validity_Check_Options;
+
+ -- 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)
+
+ Xref_Active := True;
+
+ -- Polling mode forced off, since it generates confusing junk
+
+ Polling_Required := False;
+
+ -- Set operating mode to Generate_Code to benefit from full front-end
+ -- expansion (e.g. default arguments).
+
+ Operating_Mode := Generate_Code;
+
+ -- Skip call to gigi
+
+ Debug_Flag_HH := True;
+
+ -- 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;
+
+ -- Always perform semantics and generate ALI files in ALFA mode,
+ -- so that a gnatmake -c -k will proceed further when possible.
+
+ Force_ALI_Tree_File := True;
+ Try_Semantics := True;
end if;
-
- ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode;
end Adjust_Global_Switches;
--------------------
Index: restrict.adb
===================================================================
--- restrict.adb (revision 177274)
+++ restrict.adb (working copy)
@@ -375,11 +375,12 @@
begin
Msg_Issued := False;
- -- In CodePeer mode, we do not want to check for any restriction, or set
- -- additional restrictions other than those already set in gnat1drv.adb
- -- so that we have consistency between each compilation.
+ -- In CodePeer and ALFA mode, we do not want to check for any
+ -- restriction, or set additional restrictions other than those already
+ -- set in gnat1drv.adb so that we have consistency between each
+ -- compilation.
- if CodePeer_Mode then
+ if CodePeer_Mode or else ALFA_Mode then
return;
end if;
Index: opt.ads
===================================================================
--- opt.ads (revision 177395)
+++ opt.ads (working copy)
@@ -1855,25 +1855,17 @@
-- Used to store the ASIS version number read from a tree file to check if
-- it is the same as stored in the ASIS version number in Tree_IO.
- -----------------------------------
- -- Modes for Formal Verification --
- -----------------------------------
+ ----------------------------------
+ -- Mode for Formal Verification --
+ ----------------------------------
- -- These modes are currently defined through debug flags
+ -- This mode is currently defined through a debug flag
ALFA_Mode : Boolean := False;
- -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
+ -- Specific compiling mode targeting formal verification through the
+ -- generation of Why code for those parts of the input code that belong to
+ -- the ALFA subset of Ada. Set by debuf flag -gnatd.F.
- ALFA_Through_SPARK_Mode : Boolean := False;
- -- Specific compiling mode targeting formal verification through
- -- the generation of SPARK code for those parts of the input code that
- -- belong to the ALFA subset of Ada. Set by debug flag -gnatd.E.
-
- ALFA_Through_Why_Mode : Boolean := False;
- -- Specific compiling mode targeting formal verification through
- -- the generation of Why code for those parts of the input code that
- -- belong to the ALFA subset of Ada. Set by debuf flag -gnatd.F.
-
private
-- The following type is used to save and restore settings of switches in
More information about the Gcc-patches
mailing list