gcc/ada/sa_messages.ads

   1 ------------------------------------------------------------------------------
   2 --                       C O D E P E E R / S P A R K                        --
   3 --                                                                          --
   4 --                     Copyright (C) 2015-2018, AdaCore                     --
   5 --                                                                          --
   6 -- This is free software;  you can redistribute it  and/or modify it  under --
   7 -- terms of the  GNU General Public License as published  by the Free Soft- --
   8 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
   9 -- sion.  This software is distributed in the hope  that it will be useful, --
  10 -- but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- --
  11 -- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --
  12 -- License for  more details.  You should have  received  a copy of the GNU --
  13 -- General  Public  License  distributed  with  this  software;   see  file --
  14 -- COPYING3.  If not, go to http://www.gnu.org/licenses for a complete copy --
  15 -- of the license.                                                          --
  16 --                                                                          --
  17 ------------------------------------------------------------------------------
  18
  19 pragma Ada_2012;
  20
  21 with Ada.Containers;        use Ada.Containers;
  22 with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
  23
  24 package SA_Messages is
  25
  26    --  This package can be used for reading/writing a file containing a
  27    --  sequence of static anaysis results. Each element can describe a runtime
  28    --  check whose outcome has been statically determined, or it might be a
  29    --  warning or diagnostic message. It is expected that typically CodePeer
  30    --  will do the writing and SPARK will do the reading; this will allow SPARK
  31    --  to get the benefit of CodePeer's analysis.
  32    --
  33    --  Each item is represented as a pair consisting of a message and an
  34    --  associated source location. Source locations may refer to a location
  35    --  within the expansion of an instance of a generic; this is represented
  36    --  by combining the corresponding location within the generic with the
  37    --  location of the instance (repeated if the instance itself occurs within
  38    --  a generic). In addition, the type Iteration_Id is intended for use in
  39    --  distinguishing messages which refer to a specific iteration of a loop
  40    --  (this case can arise, for example, if CodePeer chooses to unroll a
  41    --  for-loop). This data structure is only general enough to support the
  42    --  kinds of unrolling that are currently planned for CodePeer. For
  43    --  example, an Iteration_Id can only identify an iteration of the nearest
  44    --  enclosing loop of the associated File/Line/Column source location.
  45    --  This is not a problem because CodePeer doesn't unroll loops which
  46    --  contain other loops.
  47
  48    type Message_Kind is (
  49
  50       --  Check kinds
  51
  52       Array_Index_Check,
  53       Divide_By_Zero_Check,
  54       Tag_Check,
  55       Discriminant_Check,
  56       Range_Check,
  57       Overflow_Check,
  58       Assertion_Check,
  59
  60       --  Warning kinds
  61
  62       Suspicious_Range_Precondition_Warning,
  63       Suspicious_First_Precondition_Warning,
  64       Suspicious_Input_Warning,
  65       Suspicious_Constant_Operation_Warning,
  66       Unread_In_Out_Parameter_Warning,
  67       Unassigned_In_Out_Parameter_Warning,
  68       Non_Analyzed_Call_Warning,
  69       Procedure_Does_Not_Return_Warning,
  70       Check_Fails_On_Every_Call_Warning,
  71       Unknown_Call_Warning,
  72       Dead_Store_Warning,
  73       Dead_Outparam_Store_Warning,
  74       Potentially_Dead_Store_Warning,
  75       Same_Value_Dead_Store_Warning,
  76       Dead_Block_Warning,
  77       Infinite_Loop_Warning,
  78       Dead_Edge_Warning,
  79       Plain_Dead_Edge_Warning,
  80       True_Dead_Edge_Warning,
  81       False_Dead_Edge_Warning,
  82       True_Condition_Dead_Edge_Warning,
  83       False_Condition_Dead_Edge_Warning,
  84       Unrepeatable_While_Loop_Warning,
  85       Dead_Block_Continuation_Warning,
  86       Local_Lock_Of_Global_Object_Warning,
  87       Analyzed_Module_Warning,
  88       Non_Analyzed_Module_Warning,
  89       Non_Analyzed_Procedure_Warning,
  90       Incompletely_Analyzed_Procedure_Warning);
  91
  92    --  Assertion_Check includes checks for user-defined PPCs (both specific
  93    --  and class-wide), Assert pragma checks, subtype predicate checks,
  94    --  type invariant checks (specific and class-wide), and checks for
  95    --  implementation-defined assertions such as Assert_And_Cut, Assume,
  96    --  Contract_Cases, Default_Initial_Condition, Initial_Condition,
  97    --  Loop_Invariant, Loop_Variant, and Refined_Post.
  98    --
  99    --  TBD: it might be nice to distinguish these different kinds of assertions
 100    --  as is done in SPARK's VC_Kind enumeration type, but any distinction
 101    --  which isn't already present in CP's BE_Message_Subkind enumeration type
 102    --  would require more work on the CP side.
 103    --
 104    --  The warning kinds are pretty much a copy of the set of
 105    --  Be_Message_Subkind values for which CP's Is_Warning predicate returns
 106    --  True; see descriptive comment for each in CP's message_kinds.ads .
 107
 108    subtype Check_Kind is Message_Kind
 109      range Array_Index_Check .. Assertion_Check;
 110    subtype Warning_Kind is Message_Kind
 111      range Message_Kind'Succ (Check_Kind'Last) .. Message_Kind'Last;
 112
 113    --  Possible outcomes of the static analysis of a runtime check
 114    --
 115    --  Not_Statically_Known_With_Low_Severity could be used instead of of
 116    --  Not_Statically_Known if there is some reason to believe that (although
 117    --  the tool couldn't prove it) the check is likely to always pass (in CP
 118    --  terms, if the corresponding CP message has severity Low as opposed to
 119    --  Medium). It's not clear yet whether SPARK will care about this
 120    --  distinction.
 121
 122    type SA_Check_Result is
 123      (Statically_Known_Success,
 124       Not_Statically_Known_With_Low_Severity,
 125       Not_Statically_Known,
 126       Statically_Known_Failure);
 127
 128    type SA_Message (Kind : Message_Kind := Message_Kind'Last) is record
 129       case Kind is
 130          when Check_Kind =>
 131             Check_Result : SA_Check_Result;
 132
 133          when Warning_Kind =>
 134             null;
 135       end case;
 136    end record;
 137
 138    type Source_Location_Or_Null (<>) is private;
 139    Null_Location : constant Source_Location_Or_Null;
 140    subtype Source_Location is Source_Location_Or_Null with
 141      Dynamic_Predicate => Source_Location /= Null_Location;
 142
 143    type Line_Number is new Positive;
 144    type Column_Number is new Positive;
 145
 146    function File_Name (Location : Source_Location) return String;
 147    function File_Name (Location : Source_Location) return Unbounded_String;
 148    function Line      (Location : Source_Location) return Line_Number;
 149    function Column    (Location : Source_Location) return Column_Number;
 150
 151    type Iteration_Kind is (None, Initial, Subsequent, Numbered);
 152    --  None is for the usual no-unrolling case.
 153    --  Initial and Subsequent are for use in the case where only the first
 154    --  iteration of a loop (or some part thereof, such as the termination
 155    --  test of a while-loop) is unrolled.
 156    --  Numbered is for use in the case where a for-loop with a statically
 157    --  known number of iterations is fully unrolled.
 158
 159    subtype Iteration_Number is Integer range 1 .. 255;
 160    subtype Iteration_Total  is Integer range 2 .. 255;
 161
 162    type Iteration_Id (Kind : Iteration_Kind := None) is record
 163       case Kind is
 164          when Numbered =>
 165             Number   : Iteration_Number;
 166             Of_Total : Iteration_Total;
 167          when others =>
 168             null;
 169       end case;
 170    end record;
 171
 172    function Iteration (Location : Source_Location) return Iteration_Id;
 173
 174    function Enclosing_Instance
 175      (Location : Source_Location) return Source_Location_Or_Null;
 176    --  For a source location occurring within the expansion of an instance of a
 177    --  generic unit, the Line, Column, and File_Name selectors will indicate a
 178    --  location within the generic; the Enclosing_Instance selector yields the
 179    --  location of the declaration of the instance.
 180
 181    function Make
 182      (File_Name : String;
 183       Line      : Line_Number;
 184       Column    : Column_Number;
 185       Iteration : Iteration_Id;
 186       Enclosing_Instance : Source_Location_Or_Null) return Source_Location;
 187    --  Constructor
 188
 189    type Message_And_Location (<>) is private;
 190
 191    function Location (Item : Message_And_Location) return Source_Location;
 192    function Message (Item : Message_And_Location) return SA_Message;
 193
 194    function Make_Msg_Loc
 195      (Msg : SA_Message;
 196       Loc : Source_Location) return Message_And_Location;
 197    --  Selectors
 198
 199    function "<" (Left, Right : Message_And_Location) return Boolean;
 200    function Hash (Key : Message_And_Location) return Hash_Type;
 201    --  Actuals for container instances
 202
 203    File_Extension : constant String; -- ".json" (but could change in future)
 204    --  Clients may wish to use File_Extension in constructing
 205    --  File_Name parameters for calls to Open.
 206
 207    package Writing is
 208       function Is_Open return Boolean;
 209
 210       procedure Open (File_Name : String) with
 211         Precondition  => not Is_Open,
 212         Postcondition => Is_Open;
 213       --  Behaves like Text_IO.Create with respect to error cases
 214
 215       procedure Write (Message : SA_Message; Location : Source_Location);
 216
 217       procedure Close with
 218         Precondition  => Is_Open,
 219         Postcondition => not Is_Open;
 220       --  Behaves like Text_IO.Close with respect to error cases
 221    end Writing;
 222
 223    package Reading is
 224       function Is_Open return Boolean;
 225
 226       procedure Open (File_Name : String; Full_Path : Boolean := True) with
 227         Precondition  => not Is_Open,
 228         Postcondition => Is_Open;
 229       --  Behaves like Text_IO.Open with respect to error cases
 230
 231       function Done return Boolean with
 232         Precondition => Is_Open;
 233
 234       function Get return Message_And_Location with
 235         Precondition => not Done;
 236
 237       procedure Close with
 238         Precondition  => Is_Open,
 239         Postcondition => not Is_Open;
 240       --  Behaves like Text_IO.Close with respect to error cases
 241    end Reading;
 242
 243 private
 244    type Simple_Source_Location is record
 245       File_Name : Unbounded_String := Null_Unbounded_String;
 246       Line      : Line_Number      := Line_Number'Last;
 247       Column    : Column_Number    := Column_Number'Last;
 248       Iteration : Iteration_Id     := (Kind => None);
 249    end record;
 250
 251    type Source_Locations is
 252      array (Natural range <>) of Simple_Source_Location;
 253
 254    type Source_Location_Or_Null (Count : Natural) is record
 255       Locations : Source_Locations (1 .. Count);
 256    end record;
 257
 258    Null_Location : constant Source_Location_Or_Null :=
 259                      (Count => 0, Locations => (others => <>));
 260
 261    type Message_And_Location (Count : Positive) is record
 262       Message  : SA_Message;
 263       Location : Source_Location (Count => Count);
 264    end record;
 265
 266    File_Extension : constant String := ".json";
 267 end SA_Messages;