1------------------------------------------------------------------------------
2--                       C O D E P E E R / S P A R K                        --
3--                                                                          --
4--                     Copyright (C) 2015-2019, 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
19pragma Ada_2012;
20
21with Ada.Containers;        use Ada.Containers;
22with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
23
24package 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
243private
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";
267end SA_Messages;
268