Skip to content

Commit e255731

Browse files
hlisderohlisdero
committed
Improvement: handle drop and assert of the form [return: bbX, unwind terminate]
This is important since a lot of example programs exhibit this structure since the `UnwindAction` enum was introduced to rustc in rust-lang/rust#102906 In a previous commit, the change in rustc was incorporated but without handling all the cases. This improvement now handles all the variants that enum `UnwindAction` has instead of ignoring some of them. 8cf95cd
1 parent 56a2b28 commit e255731

File tree

27 files changed

+553
-20
lines changed

27 files changed

+553
-20
lines changed

‎examples/results/condvar/self_notify_lost_signal/net.dot

+3
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ digraph petrinet {
4242
main_SWITCH_INT_8 [shape="box" xlabel="" label="main_SWITCH_INT_8"];
4343
main_SWITCH_INT_9 [shape="box" xlabel="" label="main_SWITCH_INT_9"];
4444
main_UNWIND_8 [shape="box" xlabel="" label="main_UNWIND_8"];
45+
main_UNWIND_9 [shape="box" xlabel="" label="main_UNWIND_9"];
4546
std_result_Result_unwrap_0_CALL [shape="box" xlabel="" label="std_result_Result_unwrap_0_CALL"];
4647
std_sync_Condvar_new_0_CALL [shape="box" xlabel="" label="std_sync_Condvar_new_0_CALL"];
4748
std_sync_Condvar_notify_one_0_CALL [shape="box" xlabel="" label="std_sync_Condvar_notify_one_0_CALL"];
@@ -82,6 +83,7 @@ digraph petrinet {
8283
main_BB7_END_PLACE -> main_RETURN;
8384
main_BB8 -> main_UNWIND_8;
8485
main_BB9 -> main_DROP_9;
86+
main_BB9 -> main_UNWIND_9;
8587
CONDVAR_0_T1 -> CONDVAR_0_P1;
8688
CONDVAR_0_T2 -> CONDVAR_0_P1;
8789
CONDVAR_0_T2 -> CONDVAR_0_P4;
@@ -102,6 +104,7 @@ digraph petrinet {
102104
main_SWITCH_INT_8 -> main_BB8;
103105
main_SWITCH_INT_9 -> main_BB9;
104106
main_UNWIND_8 -> PROGRAM_PANIC;
107+
main_UNWIND_9 -> PROGRAM_PANIC;
105108
std_result_Result_unwrap_0_CALL -> main_BB4;
106109
std_sync_Condvar_new_0_CALL -> main_BB2;
107110
std_sync_Condvar_notify_one_0_CALL -> CONDVAR_0_P2;

‎examples/results/condvar/self_notify_lost_signal/net.lola

+5
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,11 @@ TRANSITION main_UNWIND_8
120120
main_BB8 : 1;
121121
PRODUCE
122122
PROGRAM_PANIC : 1;
123+
TRANSITION main_UNWIND_9
124+
CONSUME
125+
main_BB9 : 1;
126+
PRODUCE
127+
PROGRAM_PANIC : 1;
123128
TRANSITION std_result_Result_unwrap_0_CALL
124129
CONSUME
125130
main_BB3 : 1;

‎examples/results/condvar/self_notify_lost_signal/net.pnml

+21
Original file line numberDiff line numberDiff line change
@@ -226,6 +226,11 @@
226226
<text>main_UNWIND_8</text>
227227
</name>
228228
</transition>
229+
<transition id="main_UNWIND_9">
230+
<name>
231+
<text>main_UNWIND_9</text>
232+
</name>
233+
</transition>
229234
<transition id="std_result_Result_unwrap_0_CALL">
230235
<name>
231236
<text>std_result_Result_unwrap_0_CALL</text>
@@ -519,6 +524,14 @@
519524
<text>1</text>
520525
</inscription>
521526
</arc>
527+
<arc source="main_BB9" target="main_UNWIND_9" id="(main_BB9, main_UNWIND_9)">
528+
<name>
529+
<text>(main_BB9, main_UNWIND_9)</text>
530+
</name>
531+
<inscription>
532+
<text>1</text>
533+
</inscription>
534+
</arc>
522535
<arc source="CONDVAR_0_T1" target="CONDVAR_0_P1" id="(CONDVAR_0_T1, CONDVAR_0_P1)">
523536
<name>
524537
<text>(CONDVAR_0_T1, CONDVAR_0_P1)</text>
@@ -679,6 +692,14 @@
679692
<text>1</text>
680693
</inscription>
681694
</arc>
695+
<arc source="main_UNWIND_9" target="PROGRAM_PANIC" id="(main_UNWIND_9, PROGRAM_PANIC)">
696+
<name>
697+
<text>(main_UNWIND_9, PROGRAM_PANIC)</text>
698+
</name>
699+
<inscription>
700+
<text>1</text>
701+
</inscription>
702+
</arc>
682703
<arc source="std_result_Result_unwrap_0_CALL" target="main_BB4" id="(std_result_Result_unwrap_0_CALL, main_BB4)">
683704
<name>
684705
<text>(std_result_Result_unwrap_0_CALL, main_BB4)</text>

‎examples/results/condvar/two_threads_sharing_condvar/net.dot

+12
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,9 @@ digraph petrinet {
9696
main_SWITCH_INT_15 [shape="box" xlabel="" label="main_SWITCH_INT_15"];
9797
main_SWITCH_INT_18 [shape="box" xlabel="" label="main_SWITCH_INT_18"];
9898
main_SWITCH_INT_20 [shape="box" xlabel="" label="main_SWITCH_INT_20"];
99+
main_UNWIND_18 [shape="box" xlabel="" label="main_UNWIND_18"];
99100
main_UNWIND_19 [shape="box" xlabel="" label="main_UNWIND_19"];
101+
main_UNWIND_20 [shape="box" xlabel="" label="main_UNWIND_20"];
100102
main__closure_0__BB0_STMT0 [shape="box" xlabel="" label="main__closure_0__BB0_STMT0"];
101103
main__closure_0__BB1_STMT0 [shape="box" xlabel="" label="main__closure_0__BB1_STMT0"];
102104
main__closure_0__BB1_STMT1 [shape="box" xlabel="" label="main__closure_0__BB1_STMT1"];
@@ -110,6 +112,8 @@ digraph petrinet {
110112
main__closure_0__DROP_UNWIND_5 [shape="box" xlabel="" label="main__closure_0__DROP_UNWIND_5"];
111113
main__closure_0__RETURN [shape="box" xlabel="" label="main__closure_0__RETURN"];
112114
main__closure_0__UNWIND_10 [shape="box" xlabel="" label="main__closure_0__UNWIND_10"];
115+
main__closure_0__UNWIND_8 [shape="box" xlabel="" label="main__closure_0__UNWIND_8"];
116+
main__closure_0__UNWIND_9 [shape="box" xlabel="" label="main__closure_0__UNWIND_9"];
113117
std_clone_Clone_clone_0_CALL [shape="box" xlabel="" label="std_clone_Clone_clone_0_CALL"];
114118
std_clone_Clone_clone_0_CALL_UNWIND [shape="box" xlabel="" label="std_clone_Clone_clone_0_CALL_UNWIND"];
115119
std_ops_DerefMut_deref_mut_0_CALL [shape="box" xlabel="" label="std_ops_DerefMut_deref_mut_0_CALL"];
@@ -175,9 +179,11 @@ digraph petrinet {
175179
main_BB16_END_PLACE -> main_DROP_16;
176180
main_BB17 -> main_RETURN;
177181
main_BB18 -> main_DROP_18;
182+
main_BB18 -> main_UNWIND_18;
178183
main_BB19 -> main_UNWIND_19;
179184
main_BB2 -> main_BB2_STMT0;
180185
main_BB20 -> main_DROP_20;
186+
main_BB20 -> main_UNWIND_20;
181187
main_BB21 -> main_SWITCH_INT_18;
182188
main_BB21 -> main_SWITCH_INT_20;
183189
main_BB2_END_PLACE -> std_sync_Arc_T_new_0_CALL;
@@ -222,7 +228,9 @@ digraph petrinet {
222228
main__closure_0__BB6 -> main__closure_0__DROP_6;
223229
main__closure_0__BB7 -> main__closure_0__RETURN;
224230
main__closure_0__BB8 -> main__closure_0__DROP_8;
231+
main__closure_0__BB8 -> main__closure_0__UNWIND_8;
225232
main__closure_0__BB9 -> main__closure_0__DROP_9;
233+
main__closure_0__BB9 -> main__closure_0__UNWIND_9;
226234
CONDVAR_0_T1 -> CONDVAR_0_P1;
227235
CONDVAR_0_T2 -> CONDVAR_0_P1;
228236
CONDVAR_0_T2 -> CONDVAR_0_P4;
@@ -259,7 +267,9 @@ digraph petrinet {
259267
main_SWITCH_INT_15 -> main_BB15;
260268
main_SWITCH_INT_18 -> main_BB18;
261269
main_SWITCH_INT_20 -> main_BB20;
270+
main_UNWIND_18 -> PROGRAM_PANIC;
262271
main_UNWIND_19 -> PROGRAM_PANIC;
272+
main_UNWIND_20 -> PROGRAM_PANIC;
263273
main__closure_0__BB0_STMT0 -> main__closure_0__BB0_END_PLACE;
264274
main__closure_0__BB1_STMT0 -> main__closure_0__BB1_STMT0_END;
265275
main__closure_0__BB1_STMT1 -> main__closure_0__BB1_STMT1_END;
@@ -275,6 +285,8 @@ digraph petrinet {
275285
main__closure_0__DROP_UNWIND_5 -> main__closure_0__BB9;
276286
main__closure_0__RETURN -> THREAD_0_END;
277287
main__closure_0__UNWIND_10 -> THREAD_0_END;
288+
main__closure_0__UNWIND_8 -> THREAD_0_END;
289+
main__closure_0__UNWIND_9 -> THREAD_0_END;
278290
std_clone_Clone_clone_0_CALL -> main_BB4;
279291
std_clone_Clone_clone_0_CALL_UNWIND -> main_BB18;
280292
std_ops_DerefMut_deref_mut_0_CALL -> main__closure_0__BB4;

‎examples/results/condvar/two_threads_sharing_condvar/net.lola

+20
Original file line numberDiff line numberDiff line change
@@ -238,11 +238,21 @@ TRANSITION main_SWITCH_INT_20
238238
main_BB21 : 1;
239239
PRODUCE
240240
main_BB20 : 1;
241+
TRANSITION main_UNWIND_18
242+
CONSUME
243+
main_BB18 : 1;
244+
PRODUCE
245+
PROGRAM_PANIC : 1;
241246
TRANSITION main_UNWIND_19
242247
CONSUME
243248
main_BB19 : 1;
244249
PRODUCE
245250
PROGRAM_PANIC : 1;
251+
TRANSITION main_UNWIND_20
252+
CONSUME
253+
main_BB20 : 1;
254+
PRODUCE
255+
PROGRAM_PANIC : 1;
246256
TRANSITION main__closure_0__BB0_STMT0
247257
CONSUME
248258
THREAD_0_START : 1;
@@ -310,6 +320,16 @@ TRANSITION main__closure_0__UNWIND_10
310320
main__closure_0__BB10 : 1;
311321
PRODUCE
312322
THREAD_0_END : 1;
323+
TRANSITION main__closure_0__UNWIND_8
324+
CONSUME
325+
main__closure_0__BB8 : 1;
326+
PRODUCE
327+
THREAD_0_END : 1;
328+
TRANSITION main__closure_0__UNWIND_9
329+
CONSUME
330+
main__closure_0__BB9 : 1;
331+
PRODUCE
332+
THREAD_0_END : 1;
313333
TRANSITION std_clone_Clone_clone_0_CALL
314334
CONSUME
315335
main_BB3_END_PLACE : 1;

‎examples/results/condvar/two_threads_sharing_condvar/net.pnml

+84
Original file line numberDiff line numberDiff line change
@@ -496,11 +496,21 @@
496496
<text>main_SWITCH_INT_20</text>
497497
</name>
498498
</transition>
499+
<transition id="main_UNWIND_18">
500+
<name>
501+
<text>main_UNWIND_18</text>
502+
</name>
503+
</transition>
499504
<transition id="main_UNWIND_19">
500505
<name>
501506
<text>main_UNWIND_19</text>
502507
</name>
503508
</transition>
509+
<transition id="main_UNWIND_20">
510+
<name>
511+
<text>main_UNWIND_20</text>
512+
</name>
513+
</transition>
504514
<transition id="main__closure_0__BB0_STMT0">
505515
<name>
506516
<text>main__closure_0__BB0_STMT0</text>
@@ -566,6 +576,16 @@
566576
<text>main__closure_0__UNWIND_10</text>
567577
</name>
568578
</transition>
579+
<transition id="main__closure_0__UNWIND_8">
580+
<name>
581+
<text>main__closure_0__UNWIND_8</text>
582+
</name>
583+
</transition>
584+
<transition id="main__closure_0__UNWIND_9">
585+
<name>
586+
<text>main__closure_0__UNWIND_9</text>
587+
</name>
588+
</transition>
569589
<transition id="std_clone_Clone_clone_0_CALL">
570590
<name>
571591
<text>std_clone_Clone_clone_0_CALL</text>
@@ -996,6 +1016,14 @@
9961016
<text>1</text>
9971017
</inscription>
9981018
</arc>
1019+
<arc source="main_BB18" target="main_UNWIND_18" id="(main_BB18, main_UNWIND_18)">
1020+
<name>
1021+
<text>(main_BB18, main_UNWIND_18)</text>
1022+
</name>
1023+
<inscription>
1024+
<text>1</text>
1025+
</inscription>
1026+
</arc>
9991027
<arc source="main_BB19" target="main_UNWIND_19" id="(main_BB19, main_UNWIND_19)">
10001028
<name>
10011029
<text>(main_BB19, main_UNWIND_19)</text>
@@ -1020,6 +1048,14 @@
10201048
<text>1</text>
10211049
</inscription>
10221050
</arc>
1051+
<arc source="main_BB20" target="main_UNWIND_20" id="(main_BB20, main_UNWIND_20)">
1052+
<name>
1053+
<text>(main_BB20, main_UNWIND_20)</text>
1054+
</name>
1055+
<inscription>
1056+
<text>1</text>
1057+
</inscription>
1058+
</arc>
10231059
<arc source="main_BB21" target="main_SWITCH_INT_18" id="(main_BB21, main_SWITCH_INT_18)">
10241060
<name>
10251061
<text>(main_BB21, main_SWITCH_INT_18)</text>
@@ -1372,6 +1408,14 @@
13721408
<text>1</text>
13731409
</inscription>
13741410
</arc>
1411+
<arc source="main__closure_0__BB8" target="main__closure_0__UNWIND_8" id="(main__closure_0__BB8, main__closure_0__UNWIND_8)">
1412+
<name>
1413+
<text>(main__closure_0__BB8, main__closure_0__UNWIND_8)</text>
1414+
</name>
1415+
<inscription>
1416+
<text>1</text>
1417+
</inscription>
1418+
</arc>
13751419
<arc source="main__closure_0__BB9" target="main__closure_0__DROP_9" id="(main__closure_0__BB9, main__closure_0__DROP_9)">
13761420
<name>
13771421
<text>(main__closure_0__BB9, main__closure_0__DROP_9)</text>
@@ -1380,6 +1424,14 @@
13801424
<text>1</text>
13811425
</inscription>
13821426
</arc>
1427+
<arc source="main__closure_0__BB9" target="main__closure_0__UNWIND_9" id="(main__closure_0__BB9, main__closure_0__UNWIND_9)">
1428+
<name>
1429+
<text>(main__closure_0__BB9, main__closure_0__UNWIND_9)</text>
1430+
</name>
1431+
<inscription>
1432+
<text>1</text>
1433+
</inscription>
1434+
</arc>
13831435
<arc source="CONDVAR_0_T1" target="CONDVAR_0_P1" id="(CONDVAR_0_T1, CONDVAR_0_P1)">
13841436
<name>
13851437
<text>(CONDVAR_0_T1, CONDVAR_0_P1)</text>
@@ -1668,6 +1720,14 @@
16681720
<text>1</text>
16691721
</inscription>
16701722
</arc>
1723+
<arc source="main_UNWIND_18" target="PROGRAM_PANIC" id="(main_UNWIND_18, PROGRAM_PANIC)">
1724+
<name>
1725+
<text>(main_UNWIND_18, PROGRAM_PANIC)</text>
1726+
</name>
1727+
<inscription>
1728+
<text>1</text>
1729+
</inscription>
1730+
</arc>
16711731
<arc source="main_UNWIND_19" target="PROGRAM_PANIC" id="(main_UNWIND_19, PROGRAM_PANIC)">
16721732
<name>
16731733
<text>(main_UNWIND_19, PROGRAM_PANIC)</text>
@@ -1676,6 +1736,14 @@
16761736
<text>1</text>
16771737
</inscription>
16781738
</arc>
1739+
<arc source="main_UNWIND_20" target="PROGRAM_PANIC" id="(main_UNWIND_20, PROGRAM_PANIC)">
1740+
<name>
1741+
<text>(main_UNWIND_20, PROGRAM_PANIC)</text>
1742+
</name>
1743+
<inscription>
1744+
<text>1</text>
1745+
</inscription>
1746+
</arc>
16791747
<arc source="main__closure_0__BB0_STMT0" target="main__closure_0__BB0_END_PLACE" id="(main__closure_0__BB0_STMT0, main__closure_0__BB0_END_PLACE)">
16801748
<name>
16811749
<text>(main__closure_0__BB0_STMT0, main__closure_0__BB0_END_PLACE)</text>
@@ -1796,6 +1864,22 @@
17961864
<text>1</text>
17971865
</inscription>
17981866
</arc>
1867+
<arc source="main__closure_0__UNWIND_8" target="THREAD_0_END" id="(main__closure_0__UNWIND_8, THREAD_0_END)">
1868+
<name>
1869+
<text>(main__closure_0__UNWIND_8, THREAD_0_END)</text>
1870+
</name>
1871+
<inscription>
1872+
<text>1</text>
1873+
</inscription>
1874+
</arc>
1875+
<arc source="main__closure_0__UNWIND_9" target="THREAD_0_END" id="(main__closure_0__UNWIND_9, THREAD_0_END)">
1876+
<name>
1877+
<text>(main__closure_0__UNWIND_9, THREAD_0_END)</text>
1878+
</name>
1879+
<inscription>
1880+
<text>1</text>
1881+
</inscription>
1882+
</arc>
17991883
<arc source="std_clone_Clone_clone_0_CALL" target="main_BB4" id="(std_clone_Clone_clone_0_CALL, main_BB4)">
18001884
<name>
18011885
<text>(std_clone_Clone_clone_0_CALL, main_BB4)</text>

‎examples/results/function_call/greet/net.dot

+3
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ digraph petrinet {
5959
main_RETURN [shape="box" xlabel="" label="main_RETURN"];
6060
main_SWITCH_INT_4 [shape="box" xlabel="" label="main_SWITCH_INT_4"];
6161
main_SWITCH_INT_9 [shape="box" xlabel="" label="main_SWITCH_INT_9"];
62+
main_UNWIND_15 [shape="box" xlabel="" label="main_UNWIND_15"];
6263
main_UNWIND_16 [shape="box" xlabel="" label="main_UNWIND_16"];
6364
std_env_args_0_CALL [shape="box" xlabel="" label="std_env_args_0_CALL"];
6465
std_fmt_Arguments_a_new_v1_0_CALL [shape="box" xlabel="" label="std_fmt_Arguments_a_new_v1_0_CALL"];
@@ -95,6 +96,7 @@ digraph petrinet {
9596
main_BB13 -> main_DROP_13;
9697
main_BB14 -> main_RETURN;
9798
main_BB15 -> main_DROP_15;
99+
main_BB15 -> main_UNWIND_15;
98100
main_BB16 -> main_UNWIND_16;
99101
main_BB2 -> main_BB2_STMT0;
100102
main_BB2_END_PLACE -> std_vec_Vec_T_A_len_0_CALL;
@@ -145,6 +147,7 @@ digraph petrinet {
145147
main_RETURN -> PROGRAM_END;
146148
main_SWITCH_INT_4 -> main_BB4;
147149
main_SWITCH_INT_9 -> main_BB9;
150+
main_UNWIND_15 -> PROGRAM_PANIC;
148151
main_UNWIND_16 -> PROGRAM_PANIC;
149152
std_env_args_0_CALL -> main_BB1;
150153
std_fmt_Arguments_a_new_v1_0_CALL -> main_BB7;

‎examples/results/function_call/greet/net.lola

+5
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,11 @@ TRANSITION main_SWITCH_INT_9
162162
main_BB3 : 1;
163163
PRODUCE
164164
main_BB9 : 1;
165+
TRANSITION main_UNWIND_15
166+
CONSUME
167+
main_BB15 : 1;
168+
PRODUCE
169+
PROGRAM_PANIC : 1;
165170
TRANSITION main_UNWIND_16
166171
CONSUME
167172
main_BB16 : 1;

0 commit comments

Comments
 (0)