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
<endif>

end;'''

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

checker_template = '''with <model>;
use <model>;
74
75
76
with <model>_Stop_Conditions;
with ASN1_Ada_Iterators.Iterators;
use ASN1_Ada_Iterators.Iterators;
Maxime Perrotin's avatar
Maxime Perrotin committed
77
78
79

<asn1_modules;separator="\n">

80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
with Ada.Unchecked_Conversion,
     System,
     Ada.Text_IO,
     Ada.Streams,
     Ada.Strings.Hash,
     Ada.Containers.Ordered_Maps,
     Ada.Containers.Ordered_Sets,
     Ada.Containers.Vectors,
     Ada.Calendar,
     GNAT.MD5;

use Ada.Containers,
    Ada.Calendar,
    Ada.Streams,
    Ada.Text_IO;

procedure Model_Checker is
Maxime Perrotin's avatar
Maxime Perrotin committed
97
98
99
100
101
    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;
102
    backup_hash : Hash_Type;
Maxime Perrotin's avatar
Maxime Perrotin committed
103
    start_hash  : Hash_Type;
104
105
106

    -- 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
107
108
109

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

Maxime Perrotin's avatar
Maxime Perrotin committed
119
120
121
122
123
124
125
126
127
128
    -- 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;

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

Maxime Perrotin's avatar
Maxime Perrotin committed
136
    package Edges_Pkg is new Vectors (Element_Type => Edge_ty,
137
138
139
140
                                      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
141
        record
142
            edges   : Edges_Pkg.Vector := Edges_Pkg.Empty_Vector;
Maxime Perrotin's avatar
Maxime Perrotin committed
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
            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);

165
166
    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
167
168
169

    -- 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
170
        New_State: State_Access;
Maxime Perrotin's avatar
Maxime Perrotin committed
171
        New_Hash : Hash_Type;
Maxime Perrotin's avatar
Maxime Perrotin committed
172
        New_Edge : constant Edge_ty := (event => event, state => backup_hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
173
    begin
174
        New_Hash := State_Hash(Process_Ctxt);
Maxime Perrotin's avatar
Maxime Perrotin committed
175
        if not Grafset.Contains(Key => New_Hash) then
176
177
            New_State := new Global_State;
            New_State.context := Process_Ctxt;
Maxime Perrotin's avatar
Maxime Perrotin committed
178
            Grafset.Insert(Key => New_Hash, New_Item => New_State);
179
180
        else
            New_State := Grafset.Element(Key => New_Hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
181
        end if;
182
        New_State.edges.append(New_Edge);
Maxime Perrotin's avatar
Maxime Perrotin committed
183
184
185
186
187
188
189
190
191
192
        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);

193
194
    package Sets is new Ordered_Sets(Element_Type => Hash_Type);

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

    -- 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
215
216
217
            if properties.Length \<= 10 then
                properties.include(s_hash);
            end if;
Maxime Perrotin's avatar
Maxime Perrotin committed
218
        end if;
219
220
        if not visited.contains(s_hash) then
            visited.insert(s_hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
221
222
223
224
225
226
227
228
229
230
231
232
            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
233
234
        backup_ctxt := Process_Ctxt;
        backup_hash := State_Hash(Backup_ctxt);
Maxime Perrotin's avatar
Maxime Perrotin committed
235
236
237
        <exhausts;separator="\n">
    end;

Maxime Perrotin's avatar
Maxime Perrotin committed
238
239
240
241
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
    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
294
    event      : Event_ty(start);
Maxime Perrotin's avatar
Maxime Perrotin committed
295
    Start_Time : constant Time := Clock;
Maxime Perrotin's avatar
Maxime Perrotin committed
296
297
298
begin
    put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
    orchestrator.startup;
Maxime Perrotin's avatar
Maxime Perrotin committed
299
300
301
302
303
    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
304
305
306
307
        Process_Ctxt := Grafset.Element(Key => queue.Last_Element).Context;
        exhaustive_simulation;
        queue.delete_last;
    end loop;
Maxime Perrotin's avatar
Maxime Perrotin committed
308
309
310
    if properties.length > 0 then
        Generate_MSC;
    end if;
Maxime Perrotin's avatar
Maxime Perrotin committed
311
312
313
314
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
    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
354
    print_events = []
Maxime Perrotin's avatar
Maxime Perrotin committed
355
356
    for name, sort in pis.viewitems():
        event_tpl = StringTemplate(event, group=group)
Maxime Perrotin's avatar
Maxime Perrotin committed
357
358
359
360
361
362
        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
363
        events.append(str(event_tpl))
Maxime Perrotin's avatar
Maxime Perrotin committed
364
        print_events.append(str(print_event_tpl))
Maxime Perrotin's avatar
Maxime Perrotin committed
365
366
367
368
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

    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
401
    complete['print_events'] = print_events
Maxime Perrotin's avatar
Maxime Perrotin committed
402
403
404
405
406
407
    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'))