checker.py 13.9 KB
Newer Older
Maxime Perrotin's avatar
Maxime Perrotin committed
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
#!/usr/bin/python
# -*- coding: utf-8 -*-

''' Property parser for SDL systems

Template for a simple model checker

(c) European Space Agency, 2015-2017

Author: Maxime Perrotin
'''
from stringtemplate3 import StringTemplateGroup, StringTemplate
import opengeode

asn1_module = '''with <module>;
use <module>;
'''

provided_interface = '''<interface>_pi'''

required_interface = '''<interface>_ri'''

event = '''when <interface>_pi =>
<if(param)>
    <interface>_Param: aliased asn1Scc<sort>;
<else>
    null;
<endif>'''

Maxime Perrotin's avatar
Maxime Perrotin committed
30
31
32
33
34
35
36
print_event = '''when <interface>_pi =>
<if(param)>
    Put_Line("<interface>(" & <sort>_Pkg.Image(Event.<interface>_Param) & ")");
<else>
    Put_Line("<interface>");
<endif>'''

Maxime Perrotin's avatar
Maxime Perrotin committed
37
38
39
40
41
42
43
44
check_ppty = u'''errno := <num>;
res := <model>_stop_conditions.p\u00dcproperty_<num>;
if res then
    return res;
end if;'''

exhaust_procedure = '''procedure exhaust_<interface> is
    <if(param)><interface>_it    : <sort>_pkg.Instance;<endif>
Maxime Perrotin's avatar
Maxime Perrotin committed
45
46
    event     : Event_ty(<interface>_pi);
    S_Hash    : Hash_Type;
Maxime Perrotin's avatar
Maxime Perrotin committed
47
48
49
begin
<if(param)>
    for each of <interface>_it loop
50
        <sort>_pkg.To_ASN1(each, event.<interface>_param);
Maxime Perrotin's avatar
Maxime Perrotin committed
51
52
53
54
55
        <model>.<interface>(event.<interface>_param'access);
        count := count + 1;
        S_Hash := Add_to_graph(event => event);
        check_and_report(S_Hash);
        Process_Ctxt := backup_ctxt;
Maxime Perrotin's avatar
Maxime Perrotin committed
56
        exit when properties.length >= 10;
Maxime Perrotin's avatar
Maxime Perrotin committed
57
58
59
60
61
62
    end loop;
<else>
    <model>.<interface>;
    count := count + 1;
    S_Hash := Add_to_graph(event => event);
    check_and_report(S_Hash);
63
    Process_Ctxt := backup_ctxt;
Maxime Perrotin's avatar
Maxime Perrotin committed
64
65
66
67
68
69
70
71
72
73
74
<endif>

end;'''

exhaust = '''if Process_Ctxt.State in <states;separator= " | "> then
    exhaust_<interface>;
end if;'''

checker_template = '''with <model>;
use <model>;
with <model>_stop_conditions;
75
76
with asn1_iterators.iterators;
use asn1_iterators.iterators;
Maxime Perrotin's avatar
Maxime Perrotin committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

<asn1_modules;separator="\n">

with Ada.Text_IO;
use Ada.Text_IO;

with GNAT.MD5;

with Ada.Streams;
use Ada.Streams;

with Ada.Unchecked_Conversion;
with System;
with Ada.Strings.Hash;

92
93
with Ada.Containers.Ordered_Maps;
with Ada.Containers.Ordered_Sets;
Maxime Perrotin's avatar
Maxime Perrotin committed
94
95
96
97
98
99
100
101
102
103
104
105
with Ada.Containers.Vectors;
use Ada.Containers;

with Ada.Calendar;
use Ada.Calendar;

procedure model_checker is
    subtype Context_ty is <model>_ctxt_ty;
    Process_Ctxt : Context_ty renames <model>_Ctxt;

    -- To save/restore the context when calling a PI:
    backup_ctxt : Context_ty;
106
    backup_hash : Hash_Type;
Maxime Perrotin's avatar
Maxime Perrotin committed
107
    start_hash  : Hash_Type;
108
109
110

    -- Set a maximum size for vectors (set of states and edges)
    subtype Vect_Count is Positive range 1 .. 1000000;
Maxime Perrotin's avatar
Maxime Perrotin committed
111
112
113

    -- Type representing an event (input or output)
    type Interfaces is (start, <interfaces;separator=", ">);
114
    type Event_ty (Option: Interfaces := start) is
Maxime Perrotin's avatar
Maxime Perrotin committed
115
116
117
118
119
120
121
122
        record
            case Option is
                when start =>
                    null;
                <events;separator="\n">
            end case;
    end record;

Maxime Perrotin's avatar
Maxime Perrotin committed
123
124
125
126
127
128
129
130
131
132
    -- Display scenario (in the future: generate MSC)
    procedure Print_Event(Event: Event_ty) is
    begin
         case Event.Option is
            when start =>
                Put_Line("START");
            <print_events;separator="\n">
        end case;
    end;

133
    -- An edge is made of a past state reference and an event to leave it
Maxime Perrotin's avatar
Maxime Perrotin committed
134
    type Edge_ty is
135
136
        record
            event   : Event_ty;
Maxime Perrotin's avatar
Maxime Perrotin committed
137
            state   : Hash_Type;
138
139
    end record;

Maxime Perrotin's avatar
Maxime Perrotin committed
140
    package Edges_Pkg is new Vectors (Element_Type => Edge_ty,
141
142
143
144
                                      Index_Type   => Vect_Count);

    -- A state is made of a context and a set of edges leading to it
    type Global_State is
Maxime Perrotin's avatar
Maxime Perrotin committed
145
        record
146
            edges   : Edges_Pkg.Vector := Edges_Pkg.Empty_Vector;
Maxime Perrotin's avatar
Maxime Perrotin committed
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
            context : Context_ty;
    end record;

    -- We store only pointers to graph states in the map
    type State_Access is access Global_State;

    -- The state graph itself is stored in a dictionary type (map)
    package State_graph is new Ordered_Maps (Key_Type     => Hash_Type,
                                             Element_Type => State_Access);
    Grafset : State_graph.Map;

    -- State graph index: Use md5 first to get a string representing
    -- the context object, then strings.hash to get a number that can be used
    -- as a map key. This can surely be improved!
    Ctxt_Size: constant stream_element_offset :=
           Context_ty'object_size / stream_element'size;
    type SEA_Pointer is
         access all Stream_Element_Array (1 .. Ctxt_Size);

    function As_SEA_Ptr is
       new Ada.Unchecked_Conversion (System.Address, SEA_Pointer);

169
170
    function State_Hash(Context: Context_Ty) return Hash_Type is
        (Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(Context'Address).all)));
Maxime Perrotin's avatar
Maxime Perrotin committed
171
172
173

    -- Add a state to the graph: compute the hash (key) and store if not already there
    function Add_to_graph(event : Event_ty) return Hash_Type is
174
        New_State: State_Access;
Maxime Perrotin's avatar
Maxime Perrotin committed
175
        New_Hash : Hash_Type;
Maxime Perrotin's avatar
Maxime Perrotin committed
176
        New_Edge : constant Edge_ty := (event => event, state => backup_hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
177
    begin
178
        New_Hash := State_Hash(Process_Ctxt);
Maxime Perrotin's avatar
Maxime Perrotin committed
179
        if not Grafset.Contains(Key => New_Hash) then
180
181
            New_State := new Global_State;
            New_State.context := Process_Ctxt;
Maxime Perrotin's avatar
Maxime Perrotin committed
182
            Grafset.Insert(Key => New_Hash, New_Item => New_State);
183
184
        else
            New_State := Grafset.Element(Key => New_Hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
185
        end if;
186
        New_State.edges.append(New_Edge);
Maxime Perrotin's avatar
Maxime Perrotin committed
187
188
189
190
191
192
193
194
195
196
        return New_Hash;
    end;

    -- To count the number of calls to the function's provided interfaces
    count : natural := 0;

    -- Vector of hashes (integers) used for the model checking
    package Lists is new Vectors (Element_Type => Hash_Type,
                                  Index_type   => Vect_Count);

197
198
    package Sets is new Ordered_Sets(Element_Type => Hash_Type);

Maxime Perrotin's avatar
Maxime Perrotin committed
199
    queue   : Lists.Vector;
200
    visited : Sets.Set;
Maxime Perrotin's avatar
Maxime Perrotin committed
201
    properties: Sets.Set;
Maxime Perrotin's avatar
Maxime Perrotin committed
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218

    -- Check all properties in one go, and if one fails, set errno
    function check_properties(errno: out natural) return boolean is
        res : Boolean := false;
    begin
        <check_properties;separator="\n">
        return res;
    end;

    -- Report the result of the property check to the user
    procedure check_and_report (S_Hash: Hash_Type) is
        errno: Natural := 0;
        stop_condition: boolean := false;
    begin
        if check_properties(errno) then
            put_line("Property " & errno'img & " is verified, at step " & count'img);
            stop_condition := true;
Maxime Perrotin's avatar
Maxime Perrotin committed
219
220
221
            if properties.Length \<= 10 then
                properties.include(s_hash);
            end if;
Maxime Perrotin's avatar
Maxime Perrotin committed
222
        end if;
223
224
        if not visited.contains(s_hash) then
            visited.insert(s_hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
225
226
227
228
229
230
231
232
233
234
235
236
            if stop_condition = false then
                queue.append(S_Hash);
            end if;
        end if;
    end;


    -- One function per PI to exhaust the interface parameters
    <exhaust_procedures;separator="\n\n">

    procedure exhaustive_simulation is
    begin
237
238
        backup_ctxt := Process_Ctxt;
        backup_hash := State_Hash(Backup_ctxt);
Maxime Perrotin's avatar
Maxime Perrotin committed
239
240
241
        <exhausts;separator="\n">
    end;

Maxime Perrotin's avatar
Maxime Perrotin committed
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
    procedure Generate_MSC is
        package Loc_Maps is new Ordered_Maps(Key_Type     => Hash_Type,
                                             Element_Type => Boolean);
        package Evt_Lists is new Vectors(Element_Type => Event_ty,
                                         Index_Type   => Vect_Count);
        package Parent_Maps is new Ordered_Maps(Key_Type     => Hash_Type,
                                                Element_Type => Edge_ty);
        function Find_Path(From: Hash_Type) return Evt_Lists.Vector is
            Loc_Q       : Lists.Vector;
            Loc_Visited : Loc_Maps.Map;
            Next_Hash   : Hash_Type;
            State       : State_Access;
            Parent_Map  : Parent_Maps.Map;
            Curr        : Hash_Type;
            Edge        : Edge_Ty;
            Scenario    : Evt_Lists.Vector;
        begin
            Loc_Q.append(From);
            Loc_Visited.Include(Key => From, New_Item => True);
            while not Loc_Q.Is_Empty loop
                Next_Hash := Loc_Q.Last_Element;
                exit when Next_Hash = Start_Hash;
                State := Grafset.Element(Key => Next_Hash);
                for each_edge of State.Edges loop
                    if not Loc_Visited.Contains(each_edge.state) then
                        Loc_Q.append(Each_Edge.state);
                        Loc_Visited.Include(Key      => each_edge.state,
                                            New_Item => True);
                        Parent_Map.Include(Key      => Each_Edge.State,
                                           New_Item => (State => Next_Hash,
                                                        Event => Each_Edge.Event));
                    end if;
                end loop;
                Loc_Q.Delete_Last;
            end loop;
            Curr := Start_Hash;
            Put_Line("Found path!");
            while Parent_Map.Contains(Curr) loop
                Edge := Parent_Map.Element(Curr);
                Curr := Edge.State;
                Scenario.Append(Edge.Event);
            end loop;
            return Scenario;
        end;

        Scenario : Evt_Lists.Vector;
    begin
        for each_hash of properties loop
            put_line("Path from hash " & each_hash'img & " to hash " & start_hash'img);
            Scenario := Find_Path(each_hash);
            for each_evt of Scenario loop
                Print_Event(each_evt);
            end loop;
        end loop;
    end;

Maxime Perrotin's avatar
Maxime Perrotin committed
298
    event      : Event_ty(start);
Maxime Perrotin's avatar
Maxime Perrotin committed
299
    Start_Time : constant Time := Clock;
Maxime Perrotin's avatar
Maxime Perrotin committed
300
301
302
begin
    put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
    orchestrator.startup;
Maxime Perrotin's avatar
Maxime Perrotin committed
303
304
305
306
307
    Start_Hash := Add_to_graph(event => event);
    check_and_report(Start_Hash);
    queue.append(Start_Hash);
    visited.include(Start_Hash);
    while queue.Length > 0 and properties.length \<= 10 loop
Maxime Perrotin's avatar
Maxime Perrotin committed
308
309
310
311
        Process_Ctxt := Grafset.Element(Key => queue.Last_Element).Context;
        exhaustive_simulation;
        queue.delete_last;
    end loop;
Maxime Perrotin's avatar
Maxime Perrotin committed
312
313
314
    if properties.length > 0 then
        Generate_MSC;
    end if;
Maxime Perrotin's avatar
Maxime Perrotin committed
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
    put_line("Executed" & count'img & " functions");
    put_line("Visited" & Grafset.Length'img & " states");
    Put_Line("Execution time:" & Duration'Image(Clock - Start_Time) & "s.");
end;
'''

def generate(ast, stop_conditions):
    ''' Generate the code for the model checker '''
    process = ast.processes[0]

    # Set up a StringTemplate group (needed to configure angle-bracket)
    group = StringTemplateGroup('checker', '/tmp', lexer='angle-bracket')

    # List of ASN.1 modules
    asn1 = [name.replace('-', '_') for name in ast.asn1Modules]

    # Provided interfaces (process.input_signals)
    pis = {pi['name']: pi.get('type', None) for pi in process.input_signals}

    # Required interfaces (process.output_signals)
    ris = {ri['name']: ri.get('type', None) for ri in process.output_signals}

    # Instiantate and fill in the templates with the model data

    asn1_modules = []
    for each in asn1:
        asn1_tpl = StringTemplate(asn1_module, group=group)
        asn1_tpl['module'] = each
        asn1_modules.append(str(asn1_tpl))

    provided_interfaces = []
    for each in pis.keys():
        pi_tpl = StringTemplate(provided_interface, group=group)
        pi_tpl['interface'] = each
        provided_interfaces.append(str(pi_tpl))

    required_interfaces = []
    for each in ris.keys():
        ri_tpl = StringTemplate(required_interface, group=group)
        ri_tpl['interface'] = each
        required_interfaces.append(str(ri_tpl))

    events = []
Maxime Perrotin's avatar
Maxime Perrotin committed
358
    print_events = []
Maxime Perrotin's avatar
Maxime Perrotin committed
359
360
    for name, sort in pis.viewitems():
        event_tpl = StringTemplate(event, group=group)
Maxime Perrotin's avatar
Maxime Perrotin committed
361
362
363
364
365
366
        print_event_tpl = StringTemplate(print_event, group=group)
        event_tpl['interface'] = print_event_tpl['interface'] = name
        event_tpl['param'] = print_event_tpl['param'] = True if sort else False
        event_tpl['sort'] = print_event_tpl['sort'] = \
                (opengeode.AdaGenerator.type_name(sort, use_prefix=False)
                             if sort else "")
Maxime Perrotin's avatar
Maxime Perrotin committed
367
        events.append(str(event_tpl))
Maxime Perrotin's avatar
Maxime Perrotin committed
368
        print_events.append(str(print_event_tpl))
Maxime Perrotin's avatar
Maxime Perrotin committed
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404

    check_ppties = []
    for idx in range(len(stop_conditions)):
        check_ppty_tpl = StringTemplate(check_ppty, group=group)
        check_ppty_tpl['model'] = process.processName
        check_ppty_tpl['num'] = str(idx)
        check_ppties.append(unicode(check_ppty_tpl))

    exhaust_procedures = []
    for name, sort in pis.viewitems():
        exhaust_procedure_tpl = StringTemplate(exhaust_procedure, group=group)
        exhaust_procedure_tpl['interface'] = name
        exhaust_procedure_tpl['param'] = True if sort else False
        exhaust_procedure_tpl['sort'] = (opengeode.AdaGenerator.type_name(sort,
                                                              use_prefix=False)
                                                               if sort else '')
        exhaust_procedure_tpl['model'] = process.processName
        exhaust_procedures.append(str(exhaust_procedure_tpl))

    exhausts = []
    for name, sort in pis.viewitems():
        exhaust_tpl = StringTemplate(exhaust, group=group)
        exhaust_tpl['interface'] = name
        # get a mapping {input: {state : transition}}
        opengeode.Helper.flatten(process, sep=u'\u00dc')
        mapping = opengeode.Helper.map_input_state(process)
        states = [state for state in mapping[name].keys() if "START" not
                  in state]
        exhaust_tpl['states'] = states
        exhausts.append(str(exhaust_tpl))

    complete = StringTemplate(checker_template, group=group)
    complete['model'] = process.processName
    complete['asn1_modules'] = asn1_modules
    complete['interfaces'] = provided_interfaces
    complete['events'] = events
Maxime Perrotin's avatar
Maxime Perrotin committed
405
    complete['print_events'] = print_events
Maxime Perrotin's avatar
Maxime Perrotin committed
406
407
408
409
410
411
    complete['check_properties'] = check_ppties
    complete['exhaust_procedures'] = exhaust_procedures
    complete['exhausts'] = exhausts

    with open('model_checker.adb', 'w') as ada_file:
        ada_file.write(unicode(complete).encode('latin1'))