1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240 | pragma Assertion_Policy
(Pre => Ignore, Post => Ignore, Contract_Cases => Ignore, Ghost => Ignore);
-- The pre conditions in this package are intended to be verified with SPARK
-- mode and are not meant for use at runtime.
with Ada.Characters.Latin_1;
with Elogs_Config;
with GNAT.Source_Info;
with Interfaces; use Interfaces;
-- @summary
-- Embedded Logging
-- @description
-- A logging package primarily developed for embedded use, including systems
-- without exception propagation. Validated to SPARKs Silver level and
-- so is proven absent of runtime errors. The Log_Store memory occupation
-- is configurable via alire configration variables Max_Log_Count *
-- Max_Message_Length. Although a managed or ragged array or container may
-- provide more efficient use of memory. Utilising a fixed length String
-- store results in simplifying the use of SPARK.
package Elogs with
SPARK_Mode => On,
Abstract_State => State,
Initializes => State
is
Max_Log_Count : constant Positive := Elogs_Config.Max_Log_Count;
Max_Message_Length : constant Positive := Elogs_Config.Max_Message_Length;
Device_ID_Length : constant Positive := Elogs_Config.Device_ID_Length;
Version_Length : constant Positive := Elogs_Config.Version_Length;
subtype Exception_T is Boolean;
-- Indicates an exceptional situation has occurred.
--
-- Where code flow decisions are required then an alternative application
-- specific status should be provided separately. My personal preference
-- is enums with static predicates.
--
-- Exception_T was originally defaulted to False but setting it manually in
-- the happy path to False, makes SPARK happier.
subtype Stringle is String (1 .. Max_Message_Length);
type Device_ID_Bytes is array (1 .. Device_ID_Length) of Unsigned_8;
subtype Version_String is String (1 .. Version_Length);
Empty_Stringle : constant Stringle :=
[others => Ada.Characters.Latin_1.Space];
Empty_Device_ID : constant Device_ID_Bytes := [others => 0];
Empty_Version : constant Version_String :=
[others => Ada.Characters.Latin_1.Space];
subtype Log_ID_Type is String (1 .. 16);
-- The Log_ID is a 64bit random hex UUID log identifier that can be easily
-- copied and searched for within source code.
type Log_Index is range 1 .. Max_Log_Count with
Default_Value => 1;
-- Log_Index, the number of logs that will be stored
type Log_Msg_Array is array (Log_Index) of Stringle;
type Log_ID_Array is array (Log_Index) of Log_ID_Type;
type Log_Processed_Array is array (Log_Index) of Boolean with
Pack;
-- Records whether each log has been processed, resetting to false when
-- a log is overwritten. Useful for opportunistically sending logs to a
-- server or filesystem.
type Stored is private;
subtype ISO_Date_String is String (1 .. 10);
type Log_Info is record
Compilation_Date : ISO_Date_String := "yyyy-mm-dd";
Software_Version : Version_String := Empty_Version;
Device_ID : Device_ID_Bytes := Empty_Device_ID;
end record;
Empty_Log_ID : constant Log_ID_Type := [others => ' '];
type Retrieved_Log is record
Log_ID : Log_ID_Type := Empty_Log_ID;
Message : Stringle;
end record;
procedure Initialise
(Software_Version : in Version_String;
Device_ID : in Device_ID_Bytes) with
Global => (Input => GNAT.Source_Info.Source_Code_Information,
Output => State), Depends => (State =>
(Software_Version,
Device_ID,
GNAT.Source_Info.Source_Code_Information)), Inline;
-- Set the logs Version number and Compilation Date. This procedure
-- can also be used to reset the Log_Store.
--
-- Initialise (Software_Version => "00.01.00",
-- Device_ID => "
procedure Log
(Log_ID : in Log_ID_Type;
Message : in String) with
Pre => Message'Length < Max_Message_Length;
-- Logs a message along with tracing information.
Exceptive_Prepend : constant String := "Exception: ";
procedure Status_Exception
(Log_ID : in Log_ID_Type;
Message : in String;
Exceptive : out Exception_T) with
Pre => Message'Length < (Max_Message_Length - Exceptive_Prepend'Length);
-- Creates a Log entry into the ring buffer (Log_Store) and sets Exceptive
-- to True. If there is space then the message shall have Exception
-- indication text prepended.
--
-- @param Log_ID
-- provides log tracing in any compilation mode such as when debug
-- information is unavailable.
--
-- @Param Message
-- The fixed length string to enter into the log.
--
-- @Param Exceptive
-- indicates that an exception has occurred
--
--
-- Example use
-- Job (Exceptive : out Boolean)
-- is
-- begin
-- Elogs.Status_Exception
-- (Log_ID => "0E8B6E4104989186",
-- Message => "Output String is of an incorrect length"
-- Exceptive => Exceptive);
-- end Job;
--
-- Job (Exceptive => Exceptive);
-- if Exceptive then
-- Carry on as best as possible and optionally log further context
-- or restart the machine
-- end if;
--
-- This is not meant for usual logical flow where an enum is often useful
-- but rather intended for exceptional conditions such as external errors
-- and programmer error in cases where footguns cannot be avoided. An
-- example would be timeouts that should never occur. However I would
-- exclude logical timeouts that are expected to occur that depend upon
-- conditions such as contention.
function Log_Count return Natural;
-- Indicates the numbers of Logs stored.
function Retrieve_Log_Info return Log_Info;
-- Retrieves the logs Version number and Compilation Date entry and
-- Device_ID;
function Retrieve_Log
(Log_Number : in Log_Index)
return Retrieved_Log;
-- Retrieves a log entry to faciliate e.g. log transmissions See Log_Count
-- to get how many logs are retrievable
function Latest_Log return Retrieved_Log;
-- Returns a record containing the latest message and it's Log_ID
function Latest_Message return Stringle;
procedure Mark_Processed (Log_Number : in Log_Index);
-- Mark a log number as having been processed.
procedure Unmark_Processed (Log_Number : in Log_Index);
-- Unmark a log number as having been processed.
function Processed
(Log_Number : in Log_Index)
return Boolean;
-- Returns whether a log number has been marked as processed by the user.
procedure Unmark_Processed_All;
-- Unmarks all stored logs indicating that all logs still need to be
-- processed
function Next_To_Process return Natural;
-- returns the Log_Index of the log that will be overwritten next and that
-- has not been marked as processed. This function returns 0 if all logs
-- have been marked as processed.
private
type Stored is record
Compilation_Date : ISO_Date_String := "yyyy-mm-dd";
Software_Version : Version_String := Empty_Version;
Device_ID : Device_ID_Bytes := Empty_Device_ID;
Index : Log_Index := 1;
Log_Count : Natural := 0;
Log_IDs : Log_ID_Array := [others => Empty_Log_ID];
Log_Processed : Log_Processed_Array := [others => False];
Messages : Log_Msg_Array := [others => Empty_Stringle];
-- Messages doesn't expand in Gnat studio currently. It did when it was
-- an array of bounded strings but maybe coincidence. You can still view
-- it by unchecking the box and adding print Log_Store.Messages.
end record;
Log_Store : Stored with
Part_Of => State;
function Compile_Date return ISO_Date_String with
Volatile_Function;
procedure Increment_Index (Index : in out Log_Index) with
Inline;
function Last_Used_Index
(Index : in Log_Index)
return Log_Index;
procedure Increment_Count (Count : in out Natural) with
Inline;
procedure Update_Log
(Log_ID : in Log_ID_Type;
Formatted_Message : in Stringle) with
Global => (In_Out => Log_Store);
-- Adds a new log in round robin fashion to the Log_Store.
end Elogs;
-- ISC License (Simplified BSD)
--
-- Copyright (c) 2023, Kevin Chadwick Copyright (c) 2023, Elansys Limited
--
-- Permission to use, copy, modify, and distribute this software for any
-- purpose with or without fee is hereby granted, provided that the above
-- copyright notice and this permission notice appear in all copies.
--
-- THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
-- WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
-- MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
-- ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
-- WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
-- ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
-- OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|