From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 14166 invoked by alias); 27 Sep 2011 10:03:34 -0000 Received: (qmail 14155 invoked by uid 22791); 27 Sep 2011 10:03:33 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 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; Tue, 27 Sep 2011 10:03:19 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 5B67D2BAFBF; Tue, 27 Sep 2011 06:03:18 -0400 (EDT) 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 nBJU81D2YIZO; Tue, 27 Sep 2011 06:03:18 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 3350D2BAFB3; Tue, 27 Sep 2011 06:03:18 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 22D0592BF6; Tue, 27 Sep 2011 06:03:18 -0400 (EDT) Date: Tue, 27 Sep 2011 12:29:00 -0000 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Add option for strict standard interpretation in Alfa mode Message-ID: <20110927100318.GA13638@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="LZvS9be/3tNcYl/X" 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-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org X-SW-Source: 2011-09/txt/msg01711.txt.bz2 --LZvS9be/3tNcYl/X Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-length: 748 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 * 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. --LZvS9be/3tNcYl/X Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename=difs Content-length: 9135 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; --LZvS9be/3tNcYl/X--