test.adb 6.8 KB
Newer Older
1
with orchestrator;
Maxime Perrotin's avatar
Maxime Perrotin committed
2
use orchestrator;
3
with orchestrator_stop_conditions;
4
with asn1_iterators;
5
6
7
use  asn1_iterators;
with TASTE_BasicTypes;
use  TASTE_BasicTypes;
8
9
10
11

with ada.text_io;
use ada.text_io;

12
13
14
15
16
with gnat.md5;
with ada.streams;
use ada.streams;
with ada.Unchecked_Conversion;
with system;
17
18
19
with ada.strings.hash;

with Ada.containers.hashed_sets;
Maxime Perrotin's avatar
Maxime Perrotin committed
20
with Ada.containers.ordered_maps;
21
with Ada.containers.vectors;
22
use Ada.containers;
23

24
25
26
with ada.calendar;
use ada.calendar;

27
procedure test is
Maxime Perrotin's avatar
Maxime Perrotin committed
28
29
    subtype Context_ty is Orchestrator_Ctxt_ty;
    Process_Ctxt : Context_ty renames Orchestrator_Ctxt;
30
31

    -- To save/restore the context when calling a PI:
Maxime Perrotin's avatar
Maxime Perrotin committed
32
33
34
35
36
37
38
39
40
41
42
    backup_ctxt : Context_ty;

    procedure save_context is
    begin
        backup_ctxt := Process_Ctxt;
    end;

    procedure restore_context is
    begin
        Process_Ctxt := backup_ctxt;
    end;
43
44

    -- Type representing an event (input or output)
45
    type Interfaces is (start, pulse_pi, arr_pi, paramless_pi);
46
47
48
    type Event_ty (Option: Interfaces) is
        record
            case Option is
49
50
                when start =>
                    null;
51
                when pulse_pi =>
Maxime Perrotin's avatar
Maxime Perrotin committed
52
                    Pulse_Param: aliased asn1SccT_Int;
53
                when arr_pi =>
Maxime Perrotin's avatar
Maxime Perrotin committed
54
                    Arr_Param: aliased asn1SccT_SeqOf;
55
56
57
58
59
                when paramless_pi =>
                    null;
            end case;
    end record;

Maxime Perrotin's avatar
Maxime Perrotin committed
60
    -- Type representing an entry in the state graph
Maxime Perrotin's avatar
Maxime Perrotin committed
61
    type Global_State (I: Interfaces) is
Maxime Perrotin's avatar
Maxime Perrotin committed
62
        record
Maxime Perrotin's avatar
Maxime Perrotin committed
63
            event   : Event_ty(I);
Maxime Perrotin's avatar
Maxime Perrotin committed
64
            context : Context_ty;
Maxime Perrotin's avatar
Maxime Perrotin committed
65
66
67
    end record;

    -- We'll store only pointers to graph states in the set
68
    type State_Access is access Global_State;
Maxime Perrotin's avatar
Maxime Perrotin committed
69

Maxime Perrotin's avatar
Maxime Perrotin committed
70
71
72
73
    -- 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;
74

Maxime Perrotin's avatar
Maxime Perrotin committed
75
76
77
    -- 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!
78
    Ctxt_Size: constant stream_element_offset :=
Maxime Perrotin's avatar
Maxime Perrotin committed
79
           Context_ty'object_size / stream_element'size;
80
81
82
    type SEA_Pointer is
         access all Stream_Element_Array (1 .. Ctxt_Size);

83
84
85
86
87
88
    function As_SEA_Ptr is
       new Ada.Unchecked_Conversion (System.Address, SEA_Pointer);

    function State_Hash(state: State_Access) return Hash_Type is
        (Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(state.context'address).all)));

Maxime Perrotin's avatar
Maxime Perrotin committed
89
90
    -- 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
Maxime Perrotin's avatar
Maxime Perrotin committed
91
92
        New_State: constant State_Access := new Global_State(event.Option);
        New_Hash : Hash_Type;
93
    begin
Maxime Perrotin's avatar
Maxime Perrotin committed
94
        New_State.event   := event;
Maxime Perrotin's avatar
Maxime Perrotin committed
95
        New_State.context := Process_Ctxt;
Maxime Perrotin's avatar
Maxime Perrotin committed
96
97
98
99
100
        New_Hash := State_Hash(New_State);
        if not Grafset.Contains(Key => New_Hash) then
            Grafset.Insert(Key => New_Hash, New_Item => New_State);
        end if;
        return New_Hash;
101
102
    end;

Maxime Perrotin's avatar
Maxime Perrotin committed
103
104
    -- To count the number of calls to the function's provided interfaces
    count : natural := 0;
105

Maxime Perrotin's avatar
Maxime Perrotin committed
106
107
108
109
110
111
112
113
114
    -- Vector of hashes (integers) used for the model checking
    subtype Vect_Count is Positive range 1 .. 1000;
    package Lists is new Vectors (Element_Type => Hash_Type,
                                  Index_type   => Vect_Count);
    use Lists;

    queue   : Lists.Vector;
    qcursor : Lists.Cursor := queue.First;
    visited : Lists.Vector;
Maxime Perrotin's avatar
Maxime Perrotin committed
115
116
117
118
119
120
121
122
123
124
125

    -- 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
        errno := 0;
        res := orchestrator_stop_conditions.pÜproperty_0;
        return res;
    end;

    -- Report the result of the property check to the user
Maxime Perrotin's avatar
Maxime Perrotin committed
126
    procedure check_and_report (S_Hash: Hash_Type) is
Maxime Perrotin's avatar
Maxime Perrotin committed
127
        errno: Natural := 0;
Maxime Perrotin's avatar
Maxime Perrotin committed
128
129
        stop_condition: boolean := false;
        done : boolean := false;
Maxime Perrotin's avatar
Maxime Perrotin committed
130
131
132
    begin
        if check_properties(errno) then
            put_line("Property " & errno'img & " is verified, at step " & count'img);
133
            stop_condition := true;
Maxime Perrotin's avatar
Maxime Perrotin committed
134
        end if;
Maxime Perrotin's avatar
Maxime Perrotin committed
135
136
137
138
139
140
141
142
143
144
145
146
        for each_hash of visited loop
            if each_hash = S_Hash then
                done := true;
                exit;
            end if;
        end loop;
        if not done then
            visited.append(S_Hash);
            if stop_condition = false then
                queue.append(S_Hash);
            end if;
        end if;
147

Maxime Perrotin's avatar
Maxime Perrotin committed
148
    end;
149

Maxime Perrotin's avatar
Maxime Perrotin committed
150
151
152
153
    -- One function per PI to exhaust the interface parameters
    procedure exhaust_pulse is
        pulse_it : T_Int_pkg.Instance;
        event    : Event_ty (pulse_pi);
154
        S_Hash   : Hash_Type;
Maxime Perrotin's avatar
Maxime Perrotin committed
155
    begin
Maxime Perrotin's avatar
Maxime Perrotin committed
156
        save_context;
Maxime Perrotin's avatar
Maxime Perrotin committed
157
        for each of pulse_it loop
Maxime Perrotin's avatar
Maxime Perrotin committed
158
159
            event.pulse_param := each;
            orchestrator.pulse(event.pulse_param'access);
Maxime Perrotin's avatar
Maxime Perrotin committed
160
            count := count + 1;
Maxime Perrotin's avatar
Maxime Perrotin committed
161
            S_Hash := Add_to_graph(event => event);
Maxime Perrotin's avatar
Maxime Perrotin committed
162
            check_and_report(S_Hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
163
164
165
166
167
168
169
            restore_context;
        end loop;
    end;

    procedure exhaust_arr is
        arr_it : T_SeqOf_pkg.Instance;
        event  : Event_ty (arr_pi);
170
        S_Hash : Hash_Type;
Maxime Perrotin's avatar
Maxime Perrotin committed
171
    begin
Maxime Perrotin's avatar
Maxime Perrotin committed
172
        save_context;
Maxime Perrotin's avatar
Maxime Perrotin committed
173
        for each of arr_it loop
Maxime Perrotin's avatar
Maxime Perrotin committed
174
175
176
            event.arr_param.length := each.length; -- only variable-sized arrays
            for idx in 1..each.length loop
                event.arr_param.data(idx) := each.data(idx);
Maxime Perrotin's avatar
Maxime Perrotin committed
177
            end loop;
Maxime Perrotin's avatar
Maxime Perrotin committed
178
            orchestrator.arr(event.arr_param'access);
Maxime Perrotin's avatar
Maxime Perrotin committed
179
            count := count + 1;
Maxime Perrotin's avatar
Maxime Perrotin committed
180
            S_Hash := Add_to_graph(event => event);
Maxime Perrotin's avatar
Maxime Perrotin committed
181
            check_and_report(S_Hash);
Maxime Perrotin's avatar
Maxime Perrotin committed
182
183
184
185
            restore_context;
        end loop;
    end;

186
187
    procedure exhaust_paramless is
        event  : Event_ty (paramless_pi);
188
        S_Hash : Hash_Type;
189
190
191
    begin
        save_context;
        orchestrator.paramless;
Maxime Perrotin's avatar
Maxime Perrotin committed
192
        count := count + 1;
Maxime Perrotin's avatar
Maxime Perrotin committed
193
        S_Hash := Add_to_graph(event => event);
Maxime Perrotin's avatar
Maxime Perrotin committed
194
        check_and_report(S_Hash);
195
196
197
198
199
200
201
202
203
        restore_context;
    end;

    procedure exhaustive_simulation is
    begin
        exhaust_paramless;
        exhaust_pulse;
        exhaust_arr;
    end;
Maxime Perrotin's avatar
Maxime Perrotin committed
204

205
206
207
    event      : Event_ty(start);
    S_Hash     : Hash_Type;
    Start_Time : Time := Clock;
208
begin
209
    put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
210
    orchestrator.startup;
Maxime Perrotin's avatar
Maxime Perrotin committed
211
    S_Hash := Add_to_graph(event => event);
Maxime Perrotin's avatar
Maxime Perrotin committed
212
    check_and_report(S_Hash);
213
214
    queue.append(S_Hash);
    visited.append(S_Hash);
215
    while queue.Length > 0 loop
Maxime Perrotin's avatar
Maxime Perrotin committed
216
        Process_Ctxt := Grafset.Element(Key => queue.Last_Element).Context;
217
218
219
        exhaustive_simulation;
        queue.delete_last;
    end loop;
220
    put_line("Executed" & count'img & " functions");
Maxime Perrotin's avatar
Maxime Perrotin committed
221
    put_line("Visited" & Grafset.Length'img & " states");
222
    Put_Line("Execution time:" & Duration'Image(Clock - Start_Time) & "s.");
223
end;