Source file paste.ml
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
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
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
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
354
355
356
357
358
359
360
361
362
363
364
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
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
(** Pasting module. *)
open Cil
open Cil_types
let dkey = Options.register_category "trace-table"
let hidden_attr = "hidden"
let () = Ast_attributes.register AttrUnknown hidden_attr
let loop_body_attr = "acsl!loop_body!"
let loop_number_attr = "acsl!loop_number!"
(** To get a fresh attribute name for a loop body inside a function *)
let loop_body_attr_name n =
loop_body_attr ^ (string_of_int n)
(** To get a fresh attribute name for a loop number inside a function *)
let loop_number_attr_name n =
loop_number_attr ^ (string_of_int n)
module S_Stmt = Cil_datatype.Stmt.Set
module Statement:sig
(** find the ith loop of a function *)
val find_loop_stmt_set: int -> kernel_function -> Cil_datatype.Stmt.Set.t
(** find the ith loop body of a function *)
val find_body_stmt_set:int -> kernel_function -> Cil_datatype.Stmt.Set.t
(** find the ith asm stmt of a function *)
val find_asm_stmt_set:int -> kernel_function -> Cil_datatype.Stmt.Set.t
(** find the ith call stmt of a function *)
val find_call_stmt_set:int -> kernel_function -> Cil_datatype.Stmt.Set.t
(** find the ith/all direct/indirect call stmt of a function *)
val find_call2_stmt_set:kernel_function option -> int -> kernel_function -> Cil_datatype.Stmt.Set.t
(** find ith statement of a function *)
val find_stmt: int -> kernel_function -> stmt
(** Clear the memoized tables. *)
val clear_temporary_table: unit -> unit
end
=
struct
(** Iter on statements of a kernel function *)
let iter_from_func f kf =
let definition = Kernel_function.get_definition kf
and visitor = object
inherit nopCilVisitor as super
method! vstmt stmt = f stmt; super#vstmt stmt
method! vvdec _ = SkipChildren
method! vspec _ = SkipChildren
method! vcode_annot _ = SkipChildren
method! vinst _ = SkipChildren
method! vexpr _ = SkipChildren
method! vlval _ = SkipChildren
method! vattr _ = SkipChildren
end
in
ignore (visitCilFunction (visitor:>cilVisitor) definition)
exception FoundStmt of stmt
module H_Int = Datatype.Int.Hashtbl
module H_Int_S_Stmt = H_Int.Make(S_Stmt)
let memoized_find find create find_kf replace_kf kf n compute =
let tbl =
try find_kf kf
with Not_found ->
let tbl = create 5
in compute tbl ;
replace_kf kf tbl ;
tbl
in find tbl n
let on_acsl_attr tbl attr_regexp stmt battrs =
List.iter (function (attr_name, args) when attr_name = hidden_attr ->
List.iter (function AStr(name) ->
(try (match Str.bounded_split_delim attr_regexp name 2 with
[ "" ; n ] ->
let n = int_of_string n in
let stmts =
try H_Int.find tbl n
with Not_found -> S_Stmt.empty
in
let stmts = S_Stmt.add (stmt ()) stmts
in H_Int.replace tbl n stmts
| _ -> ())
with _ -> ())
| _ -> ()) args
| _ -> ()) battrs
let find_from_func f kf =
let f stmt = if f stmt then raise (FoundStmt stmt) in
try
iter_from_func f kf ;
raise Not_found
with FoundStmt stmt -> stmt
(** Memoized loop number table. *)
module Sloop =
State_builder.Hashtbl
(Cil_datatype.Kf.Hashtbl)
(H_Int_S_Stmt)
(struct
let name = "LoopNumberIndex"
let dependencies = [ ]
let size = 7
end)
let _ = Ast.add_linked_state Sloop.self
let find_loop_stmt_set n kf =
memoized_find H_Int.find H_Int.create Sloop.find Sloop.replace kf n
(fun tbl ->
Options.debug ~level:2 ~dkey "Computing loop index table for function \"%a\""
Kernel_function.pretty kf;
let attr_regexp = Str.regexp_string loop_number_attr in
let on_loop stmt = match stmt.skind with
| Loop (_,{battrs},_,_,_) ->
on_acsl_attr tbl attr_regexp (fun () -> stmt) battrs
| _ -> ()
in iter_from_func on_loop kf)
(** Memoized loop body table. *)
module Sbody =
State_builder.Hashtbl
(Cil_datatype.Kf.Hashtbl)
(H_Int_S_Stmt)
(struct
let name = "LoopBodyIndex"
let dependencies = [ ]
let size = 7
end)
let _ = Ast.add_linked_state Sbody.self
let find_body_stmt_set n kf =
memoized_find H_Int.find H_Int.create Sbody.find Sbody.replace kf n
(fun tbl ->
Options.debug ~level:2 ~dkey "Computing loop body table for function \"%a\""
Kernel_function.pretty kf;
let attr_regexp = Str.regexp_string loop_body_attr in
let on_body stmt = match stmt.skind with
| Block {battrs} ->
on_acsl_attr tbl attr_regexp (fun () -> stmt) battrs
| _ -> ()
in iter_from_func on_body kf)
(** Memoized asm table. *)
module Sasm =
State_builder.Hashtbl
(Cil_datatype.Kf.Hashtbl)
(H_Int_S_Stmt)
(struct
let name = "AsmIndex"
let dependencies = [ ]
let size = 7
end)
let _ = Ast.add_linked_state Sasm.self
let find_asm_stmt_set n kf =
memoized_find H_Int.find H_Int.create Sasm.find Sasm.replace kf n
(fun tbl ->
Options.debug ~level:2 ~dkey "Computing asm call table for function \"%a\""
Kernel_function.pretty kf;
let cpt = ref 0 in
let on_asm stmt = match stmt.skind with
| Instr (Asm _) ->
incr cpt ;
H_Int.replace tbl !cpt (S_Stmt.singleton stmt)
| _ -> ()
in iter_from_func on_asm kf)
(** Memoized call table. *)
module P_S_Stmt = Datatype.Pair(S_Stmt)(S_Stmt)
module H_Int_P_S_Stmt = H_Int.Make(P_S_Stmt)
module Scall =
State_builder.Hashtbl
(Cil_datatype.Kf.Hashtbl)
(H_Int_P_S_Stmt)
(struct
let name = "CallIndex"
let dependencies = [ ]
let size = 7
end)
let _ = Ast.add_linked_state Scall.self
let find_call_stmt n kf =
memoized_find H_Int.find H_Int.create Scall.find Scall.replace kf n
(fun tbl ->
Options.debug ~level:2 ~dkey "Computing call table1 for function \"%a\""
Kernel_function.pretty kf;
let cpt = ref 0 in
let cpt_indirect = ref 0 in
let indirect_calls = ref S_Stmt.empty in
let get n = try H_Int.find tbl n with Not_found -> S_Stmt.empty, S_Stmt.empty in
let on_call stmt = match stmt.skind with
| Instr (Call (_, f, _ , _)) ->
begin
match Kernel_function.get_called f with
| None ->
incr cpt_indirect ;
let all,indirect = get !cpt_indirect in
H_Int.replace tbl !cpt_indirect (all,(S_Stmt.add stmt indirect));
indirect_calls := (S_Stmt.add stmt !indirect_calls)
| _ ->
incr cpt ;
let all,indirect = get !cpt in
H_Int.replace tbl !cpt ((S_Stmt.add stmt all), indirect) ;
end
| _ -> ()
in iter_from_func on_call kf; H_Int.replace tbl 0 (S_Stmt.empty, !indirect_calls))
let find_call_stmt_set n kf = fst (find_call_stmt n kf)
(** Memoized call2 table. *)
module H_Kf = Cil_datatype.Kf.Hashtbl
module H_Kf_H_Int_S_Stmt = H_Kf.Make(H_Int_S_Stmt)
module Scall2 =
State_builder.Hashtbl
(Cil_datatype.Kf.Hashtbl)
(H_Kf_H_Int_S_Stmt)
(struct
let name = "Call2Index"
let dependencies = [ ]
let size = 7
end)
let _ = Ast.add_linked_state Scall2.self
let find_call2_stmt called_kf kf =
memoized_find H_Kf.find H_Kf.create Scall2.find Scall2.replace kf called_kf
(fun tbl ->
Options.debug ~level:2 ~dkey "Computing call table2 for function \"%a\""
Kernel_function.pretty kf;
let tbl_cpt = H_Kf.create 3 in
let on_call stmt = match stmt.skind with
| Instr (Call (_, f, _ , _)) -> begin
match Kernel_function.get_called f with
| Some called_kf ->
let cpt =
let cpt = try H_Kf.find tbl_cpt called_kf with Not_found -> 0 in
let cpt = cpt + 1 in
H_Kf.replace tbl_cpt called_kf cpt ; cpt
in
let tbl_stmt = try H_Kf.find tbl called_kf
with Not_found -> let tbl_stmt = H_Int.create 3 in
H_Kf.replace tbl called_kf tbl_stmt ; tbl_stmt
in
let s = try H_Int.find tbl_stmt cpt with Not_found -> S_Stmt.empty in
H_Int.replace tbl_stmt cpt (S_Stmt.add stmt s) ;
let s = try H_Int.find tbl_stmt 0 with Not_found -> S_Stmt.empty in
H_Int.replace tbl_stmt 0 (S_Stmt.add stmt s)
| _ -> ()
end
| _ -> ()
in iter_from_func on_call kf)
let find_call2_stmt_set kf_opt n kf =
match kf_opt with
| None -> snd (find_call_stmt n kf)
| Some called_kf -> H_Int.find (find_call2_stmt called_kf kf) n
let find_stmt n kf =
let nb = ref 0 in
let is_stmt _stmt =
incr nb ;
!nb = n
in find_from_func is_stmt kf
(** Clear the memoized tables. *)
let clear_temporary_table () =
Options.debug ~level:2 ~dkey "Clear loop index table";
Sloop.clear ();
Options.debug ~level:2 ~dkey "Clear loop body table";
Sbody.clear ();
Options.debug ~level:2 ~dkey "Clear asm call table";
Sasm.clear ();
Options.debug ~level:2 ~dkey "Clear function call tables";
Scall.clear ();
Scall2.clear ()
end
module MacroIndex: sig
(** Macro table management. *)
type scope_t = Sfile | Smodule | Sfunction
val pp_scope: Format.formatter -> scope_t -> unit
val dkey: Options.category
val clear_macro_table : scope_t -> unit
(** To clear macro table in order to free memory,
without clearing the result dependencies. *)
val add_macro: scope_t -> string -> Logic_ptree.lexpr -> unit
(** Modify the macro table,
without clearing the result dependencies. *)
val find_macro: scope_t -> string -> Logic_ptree.lexpr
(** Find the macro definition.
@raise Not_found for undefined macro.*)
end = struct
type scope_t = Sfile | Smodule | Sfunction
let pp_scope fmt = function
| Sfile -> Format.fprintf fmt "%s" "file"
| Smodule -> Format.fprintf fmt "%s" "module"
| Sfunction -> Format.fprintf fmt "%s" "function"
(** Memoized index macro table. *)
module Sfile =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
(Cil_datatype.Lexpr)
(struct
let name = "FileMacroIndex"
let dependencies = [ Ast.self ]
let size = 3
end)
let _ = Ast.add_linked_state Sfile.self
module Smodule =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
(Cil_datatype.Lexpr)
(struct
let name = "ModuleMacroIndex"
let dependencies = [ Ast.self ]
let size = 3
end)
let _ = Ast.add_linked_state Smodule.self
module Sfunction =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
(Cil_datatype.Lexpr)
(struct
let name = "FunctionMacroIndex"
let dependencies = [ Ast.self ]
let size = 3
end)
let _ = Ast.add_linked_state Sfunction.self
let find_macro scope m =
try if scope = Sfunction then Sfunction.find m else raise Not_found
with Not_found ->
try if scope <> Sfile then Smodule.find m else raise Not_found
with Not_found ->
Sfile.find m
let dkey = Options.register_category "trace-tables"
let add_macro scope m def =
Options.debug ~level:2 ~dkey "Add macro %S at %a scope"
m pp_scope scope;
let replace = match scope with
| Sfile -> Sfile.replace
| Smodule -> Smodule.replace
| Sfunction -> Sfunction.replace
in replace m def
(** Clear the memoized "MacroIndex" table in order to free memory,
without clearing the result dependencies. *)
let clear_macro_table scope =
Options.debug ~level:2 ~dkey "Clear macro table from %a scope"
pp_scope scope;
if scope = Sfile then Sfile.clear () ;
if scope <> Sfunction then Smodule.clear () ;
Sfunction.clear () ;
end
module A2fc_inner_ast =
State_builder.Option_ref(Cil_datatype.File)
(struct
let name = "A2fcPaste.A2fc_inner_ast"
let dependencies = [ Ast.self ]
end)
let _ = Ast.add_linked_state A2fc_inner_ast.self
module SymbolIndex: sig
(** Symbol table management. *)
val self : State.t
(** Dependencies of the result of find_xxx functions. *)
val clear_temporary_table : unit -> unit
(** To clear temporary index table in order to free memory,
without clearing the result dependencies. *)
val find_kf : file:File.t option -> string -> Kernel_function.t
(** Find [Kernel_function] related to a global annotation. *)
val find_var_annot : file:File.t option -> Kernel_function.t -> stmt ->
?label:string -> string -> logic_var
(** Find variables related to a code annotation. *)
val find_var_funspec : file:File.t option -> Kernel_function.t -> string -> logic_var
(** Find variables related to a function contract. *)
val find_var_global : file:File.t option -> string -> logic_var
(** Find variables related to a global annotation. *)
val find_enum_item : file:File.t option -> string -> exp * typ
val find_type : file:File.t option -> Logic_typing.type_namespace -> string -> typ
end = struct
module SymbolCode = struct
type symbol_code =
| SGdef | SGdec
| SFdef | SFdec
| STdef
| SItem
| SEdef | SEdec
| SSdef | SSdec
| SUdef | SUdec
include Datatype.Make_with_collections
(struct
type t = symbol_code
let name = "SymbolCode"
let reprs = [ SGdef ]
let structural_descr = Structural_descr.t_abstract
let hash = function
| SGdef -> 0
| SGdec -> 1
| SFdef -> 2
| SFdec -> 3
| STdef -> 4
| SItem -> 5
| SEdef -> 6
| SEdec -> 7
| SSdef -> 8
| SSdec -> 9
| SUdef -> 10
| SUdec -> 11
let compare s1 s2 = Stdlib.compare (hash s1) (hash s2)
let equal s1 s2 = s1 = s2
let copy id = id
let rehash = Datatype.identity
let pretty = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
end
(** To encapsulate all global C symbols *)
module Symbol = struct
let dkey = Options.register_category "trace-symbols"
type symbol =
| Gdef of varinfo | Gdec of varinfo
| Fdef of varinfo | Fdec of varinfo
| Tdef of typeinfo
| Item of enumitem
| Edef of enuminfo | Edec of enuminfo
| Sdef of compinfo | Sdec of compinfo
| Udef of compinfo | Udec of compinfo
let symbol_code = function
| Gdef _ -> SymbolCode.SGdef | Gdec _ -> SymbolCode.SGdec
| Fdef _ -> SymbolCode.SFdef | Fdec _ -> SymbolCode.SFdec
| Tdef _ -> SymbolCode.STdef
| Item _ -> SymbolCode.SItem
| Edef _ -> SymbolCode.SEdef | Edec _ -> SymbolCode.SEdec
| Sdef _ -> SymbolCode.SSdef | Sdec _ -> SymbolCode.SSdec
| Udef _ -> SymbolCode.SUdef | Udec _ -> SymbolCode.SUdec
let encode = function
| GType (t,_) ->
Options.debug ~level:2 ~dkey
"Type: %S@." t.torig_name;
Some (t.torig_name,
Tdef (t))
| GCompTag (c,_) ->
Options.debug ~level:2 ~dkey
"CompTag: %S@." c.corig_name;
Some (c.corig_name,
if c.cstruct then Sdef (c) else Udef (c))
| GCompTagDecl (c,_) ->
Options.debug ~level:2 ~dkey
"CompTagDecl: %S@." c.cname;
Some (c.cname,
if c.cstruct then Sdec (c)else Udec (c))
| GEnumTag (e,_) ->
Options.debug ~level:2 ~dkey
"EnumTag: %S@." e.eorig_name;
Some (e.eorig_name,
Edef (e))
| GEnumTagDecl (e,_) ->
Options.debug ~level:2 ~dkey
"EnumTagDecl: %S@." e.eorig_name;
Some (e.eorig_name,
Edec (e))
| GVarDecl (vi,_) ->
if vi.vglob then
(Options.debug ~level:2 ~dkey
"VarDecl: %S@." vi.vorig_name;
Some (vi.vorig_name, Gdec (vi)))
else None
| GFunDecl (_,vi,_) ->
if vi.vglob then
(Options.debug ~level:2 ~dkey
"FunDecl: %S@." vi.vorig_name;
Some (vi.vorig_name,Fdec (vi)))
else None
| GVar (vi,_,_) ->
if vi.vglob then
(Options.debug ~level:2 ~dkey
"Var: %S@." vi.vorig_name;
Some (vi.vorig_name, Gdef (vi)))
else None
| GFun (f,_) ->
if f.svar.vglob then
(Options.debug ~level:2 ~dkey
"Fun: %S@." f.svar.vorig_name;
Some (f.svar.vorig_name, Fdef (f.svar)))
else None
| _ -> None
include Datatype.Make_with_collections
(struct
type t = symbol
let name = "Symbol"
let reprs = List.map (fun v -> Gdef v) Cil_datatype.Varinfo.reprs
let structural_descr = Structural_descr.t_abstract
let compare s1 s2 =
match s1, s2 with
| ( Gdef (v1), Gdef (v2) | Gdec (v1), Gdec (v2)
| Fdef (v1), Fdef (v2) | Fdec (v1), Fdec (v2)) ->
Cil_datatype.Varinfo.compare v1 v2
| Tdef (t1), Tdef (t2) ->
Cil_datatype.Typeinfo.compare t1 t2
| Item (i1), Item (i2) ->
Cil_datatype.Enumitem.compare i1 i2
| ( Edef (e1), Edef (e2) | Edec (e1), Edec (e2)) ->
Cil_datatype.Enuminfo.compare e1 e2
| ( Sdef (c1), Sdef (c2) | Sdec (c1), Sdec (c2)
| Udef (c1), Udef (c2) | Udec (c1), Udec (c2)) ->
Cil_datatype.Compinfo.compare c1 c2
| _,_ ->
SymbolCode.compare (symbol_code (s1)) (symbol_code (s2))
let hash s1 =
let h1 = match s1 with
| ( Gdef (v1) | Gdec (v1) | Fdef (v1) | Fdec (v1)) ->
Cil_datatype.Varinfo.hash v1
| Tdef (t1) -> Cil_datatype.Typeinfo.hash t1
| Item (i1) -> Cil_datatype.Enumitem.hash i1
| ( Edef (e1) | Edec (e1)) -> Cil_datatype.Enuminfo.hash e1
| ( Sdef (c1) | Sdec (c1)
| Udef (c1) | Udec (c1)) -> Cil_datatype.Compinfo.hash c1
in
let h2 = SymbolCode.hash (symbol_code (s1)) in
Hashtbl.hash (h1, h2)
let equal s1 s2 =
match s1, s2 with
| ( Gdef (v1), Gdef (v2) | Gdec (v1), Gdec (v2)
| Fdef (v1), Fdef (v2) | Fdec (v1), Fdec (v2)) ->
Cil_datatype.Varinfo.equal v1 v2
| Tdef (t1), Tdef (t2) ->
Cil_datatype.Typeinfo.equal t1 t2
| Item (i1), Item (i2) ->
Cil_datatype.Enumitem.equal i1 i2
| ( Edef (e1), Edef (e2) | Edec (e1), Edec (e2)) ->
Cil_datatype.Enuminfo.equal e1 e2
|(Sdef c1, Sdef c2 | Sdec c1, Sdef c2 | Udef c1, Udef c2
| Udec c1, Udec c2) ->
Cil_datatype.Compinfo.equal c1 c2
| _,_ -> false
let copy = Datatype.undefined
let rehash = Datatype.identity
let pretty = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
end
module H_String = Datatype.String.Hashtbl
module S_Symbol = Symbol.Set
module M_SymbolCode = SymbolCode.Map
module S_SymbolCode = SymbolCode.Set
module H_String2S_Symbol = Datatype.String.Hashtbl.Make(S_Symbol)
module M_SymbolCode2H_String2S_Symbol =
SymbolCode.Map.Make(H_String2S_Symbol)
(** Memoized index symbol table:
orig_name -hash-> SymbolCode.t -map-> filename -hash-> Set of Symbol.t
Note:
-hash-> is used as -map-> (only one binding)
-map -> is used when iteration order should use the key order *)
module S =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
(M_SymbolCode2H_String2S_Symbol)
(struct
let name = "SymbolIndex"
let dependencies = [ ]
let size = 7
end)
let _ = Ast.add_linked_state S.self
module First =
State_builder.True_ref
(struct
let dependencies = [ S.self ]
let name = "SymbolIndex.compute"
end)
let apply_once f =
(fun () ->
if First.get () then begin
First.set false;
try
f ();
assert (First.get () = false)
with exn ->
First.set true;
raise exn
end),
First.self
(** Compute once the index symbol table. *)
let compute, self =
let compute () =
Options.debug
~level:2 ~dkey:MacroIndex.dkey "Indexing the C symbol table...";
let ast =
try A2fc_inner_ast.get ()
with Not_found ->
Options.fatal "No AST registered in ACSL importer plug-in"
in
iterGlobals
ast
(fun glob ->
match Symbol.encode glob with
| None -> ()
| Some (name,symb) ->
let file = Filepath.to_string
(fst (Cil_datatype.Global.loc glob)).Filepath.pos_path
in
let index na sy =
let code = Symbol.symbol_code sy in
let update_map htable symbols old_map =
H_String.replace htable file symbols ;
M_SymbolCode.add code htable old_map
in
let new_index old_map =
let htable = H_String.create(5) in
update_map htable (S_Symbol.singleton sy) old_map
in
ignore (S.memo
~change:(fun old_map ->
try
let htable = M_SymbolCode.find code old_map in
let symbols =
try H_String.find htable file
with Not_found -> S_Symbol.empty
in
update_map htable (S_Symbol.add sy symbols) old_map
with Not_found -> new_index old_map)
(fun _ -> new_index M_SymbolCode.empty)
na) ;
in
index name symb;
match symb with
| Symbol.Edef (enum) ->
List.iter
(fun it -> index it.eiorig_name (Symbol.Item (it)))
enum.eitems
| _ -> ()
)
in
apply_once compute
(** Clear the memoized [SymbolIndex] table and the fact it hash been computed
in order to free memory. *)
let clear_temporary_table () =
Options.debug ~level:2 ~dkey "Clear symbol table";
First.set true ;
S.clear () ;
Statement.clear_temporary_table ()
exception FoundSymbol of Symbol.t
(** Find a [Symbol.t] from an original name having the highest priority among
[kinds], and lookup for [Symbol.t] used into [file] first when given. *)
let find ~kinds ~file name =
compute () ;
let map = S.find name in
let find_first_symbol () =
try
S_SymbolCode.iter
(fun code ->
try let htable = M_SymbolCode.find code map in
H_String.iter
(fun _f set -> S_Symbol.iter (fun s -> raise(FoundSymbol s)) set)
htable
with Not_found -> ())
kinds ;
raise Not_found
with FoundSymbol symb -> symb
in
match file with
| None -> find_first_symbol ()
| Some file -> let file = (File.get_name file) in
try
S_SymbolCode.iter
(fun code ->
try
let htable = M_SymbolCode.find code map in
let symbols = H_String.find htable file in
S_Symbol.iter (fun s -> raise(FoundSymbol s)) symbols
with Not_found -> ())
kinds ;
find_first_symbol ()
with FoundSymbol symb -> symb
let make_kinds kinds =
List.fold_left
(fun acc sc -> S_SymbolCode.add sc acc)
S_SymbolCode.empty
kinds
let var_kinds = make_kinds [SymbolCode.SGdef ; SymbolCode.SGdec ;
SymbolCode.SFdef; SymbolCode.SFdec]
let kf_kinds = make_kinds [SymbolCode.SFdef; SymbolCode.SFdec]
let item_kinds = S_SymbolCode.singleton SymbolCode.SItem
let type_kinds = S_SymbolCode.singleton SymbolCode.STdef
let struct_kinds = make_kinds [SymbolCode.SSdef ; SymbolCode.SSdec]
let union_kinds = make_kinds [SymbolCode.SUdef ; SymbolCode.SUdec]
let enum_kinds = make_kinds [SymbolCode.SEdef ; SymbolCode.SEdec]
let find_varinfo ~file name =
match find ~kinds:var_kinds ~file name
with
| ( Symbol.Gdef (vi)
| Symbol.Gdec (vi)
| Symbol.Fdef (vi)
| Symbol.Fdec (vi)) -> vi
| _ -> assert false
let find_kf_varinfo ~file name =
match find ~kinds:kf_kinds ~file name
with
| ( Symbol.Fdef (vi)
| Symbol.Fdec (vi)) -> vi
| _ -> assert false
let find_enum_item ~file name =
match find ~kinds:item_kinds ~file name
with
| Symbol.Item (item) ->
let typ = Cil_const.mk_tint item.eihost.ekind in
let exp = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Const (CEnum (item)))
in
Options.debug ~level:2 ~dkey "Found enum item of name %s: symbol=%a type=%a@."
name Printer.pp_exp exp Printer.pp_logic_type (Ctype typ);
exp, typ
| _ -> assert false
let find_typedef_type ~file name =
match find ~kinds:type_kinds ~file name
with
| Symbol.Tdef (ti) -> ti.ttype
| _ -> assert false
let find_struct_type ~file name =
match find ~kinds:struct_kinds ~file name
with
| (Symbol.Sdef (ci) | Symbol.Sdec (ci)) ->
Cil_const.mk_tcomp ci
| _ -> assert false
let find_union_type ~file name =
match find ~kinds:union_kinds ~file name
with
| (Symbol.Udef (ci) | Symbol.Udec (ci)) ->
Cil_const.mk_tcomp ci
| _ -> assert false
let find_enum_type ~file name =
match find ~kinds:enum_kinds ~file name
with
| (Symbol.Edef (e) | Symbol.Edec (e)) ->
Cil_const.mk_tenum e
| _ -> assert false
let find_type ~file tkind name =
let find_type = match tkind with
| Logic_typing.Typedef -> find_typedef_type
| Logic_typing.Struct -> find_struct_type
| Logic_typing.Union -> find_union_type
| Logic_typing.Enum -> find_enum_type
in find_type ~file name
let lookup vars x = List.find (fun vi -> vi.vorig_name = x) vars
(** Find variables related to a global annotation. *)
let find_var_global ~file x =
let vi =
find_varinfo ~file x
in
cvar_to_lvar vi
(** Find [Kernel_function] related to a global annotation. *)
let find_kf ~file x =
let vi =
find_kf_varinfo ~file x
in
Globals.Functions.get vi
(** Find variables related to a function contract. *)
let find_var_funspec ~file kf x =
let vi =
try
lookup (Kernel_function.get_formals kf) x
with Not_found ->
find_varinfo ~file x
in
cvar_to_lvar vi
(** Find variables related to a code annotation. *)
let find_var_annot ~file kf stmt ?label var =
let scope =
match label with
| None | Some "Here" | Some "Old" | Some "Post" -> Block_scope stmt
| Some "Pre" ->
let stmt = Kernel_function.find_first_stmt kf in Block_scope stmt
| Some "Init" -> Program
| Some "LoopEntry" | Some "LoopCurrent" ->
let stmt = Kernel_function.find_enclosing_loop kf stmt in
Block_scope stmt
| Some lab ->
let stmt = Kernel_function.find_label kf lab in Block_scope !stmt
in
let vi = Globals.Syntactic_search.find_in_scope var scope in
let vi = match vi with
| Some vi -> vi
| None -> find_varinfo ~file var
in
cvar_to_lvar vi
end
let buffer = Buffer.create 80
let add_buffer s =
Buffer.add_string buffer s
let prop_file = ref Filepath.empty
let prop_line = ref 0
let buff_line = ref 0
let set_prop_loc file line =
prop_file := file ;
prop_line := line
let set_buff_loc line =
buff_line := line ;
Buffer.clear buffer
(** Get location of the first character of
the string to parse with acsl parser *)
let get_buff_loc () =
{Cil_datatype.Position.unknown with
Filepath.pos_path= !prop_file;
Filepath.pos_lnum = !buff_line}
(** Get location of the first property token *)
let get_prop_loc () =
{Cil_datatype.Position.unknown with
Filepath.pos_path= !prop_file;
Filepath.pos_lnum = !prop_line}
let basename_chop_extension file =
let basename = Filename.basename file in
try
Filename.chop_extension basename
with
Invalid_argument _ -> basename
let current_scope = ref MacroIndex.Sfile
let current_module = ref None
let current_function = ref None
let dkey = Options.register_category "trace-actions"
let set_current_scope scope =
Options.debug ~level:2 ~dkey "Set current scope to %a@."
MacroIndex.pp_scope scope ;
MacroIndex.clear_macro_table scope ;
current_scope := scope
let set_current_module ~is_from_file_name m =
Options.debug ~level:2 ~dkey "Set current module to %S@." m ;
set_current_scope (if is_from_file_name
then MacroIndex.Sfile
else MacroIndex.Smodule) ;
current_function := None ;
current_module :=
if m = "" then None
else
try
let file =
Some (List.find
(fun file -> m = basename_chop_extension (File.get_name file))
(File.get_all ()))
in
Options.debug ~level:2 ~dkey "MODULE %s@." m ;
file
with Not_found -> None
let find_kf fct = SymbolIndex.find_kf ~file:!current_module fct
let set_current_function (fct,(source,_loc2)) =
set_current_scope MacroIndex.Sfunction ;
Options.debug ~level:2 ~dkey
"Set current function to %S@." fct ;
try
current_function := Some (find_kf fct) ;
Options.debug ~level:2 ~dkey "FUNCTION %s@." fct
with
Not_found ->
Options.annot_error ~source "could not find function %s for ACSL importer." fct;
current_function := None
exception Kf_not_found
let with_current_function ?source () =
match !current_function with
| None -> Options.annot_warning ~raising:(fun () -> raise Kf_not_found)
?source "no proper function found for ACSL importer."
| Some kf -> kf
let get_current_function ?source () =
match !current_function with
| None -> Options.abort ?source "no proper function found for ACSL importer."
| Some kf -> kf
let init_ast =
let first = ref true in
fun ~file ~init_module_from_file_name ~init_typenames ast ->
A2fc_inner_ast.set ast;
if !first then begin
first := false ;
Logic_env.builtin_types_as_typenames ();
end;
if init_typenames then
Cil.iterGlobals ast
(function
| GType (tn, _loc) -> Logic_env.add_typename tn.torig_name
| _ -> ()) ;
if init_module_from_file_name then
set_current_module ~is_from_file_name:true
(basename_chop_extension (Filepath.to_string file))
(** Parse a global annotation. *)
let parse_global s =
match Logic_lexer.annot (get_buff_loc (), s) with
| Some (_, Logic_ptree.Adecl decls) ->
List.map (fun d -> {d with Logic_ptree.decl_loc
= (get_prop_loc (),
snd d.Logic_ptree.decl_loc)})
decls
| _ -> Options.abort "[Syntax error] Unallowed global annotation."
(** Parse a function contract. *)
let parse_spec s =
match Logic_lexer.spec (get_buff_loc (), s) with
| Some (loc2, a) ->
a, (get_prop_loc (), loc2)
| None -> Options.abort "[Syntax error] Invalid function contract"
(** Parse a code annotation. *)
let parse_annots s =
match Logic_lexer.annot (get_buff_loc (), s) with
| Some (_,Logic_ptree.Acode_annot ((_loc1,loc2),a)) ->
(get_prop_loc (), loc2), [a]
| Some (_,Logic_ptree.Aloop_annot ((_loc1,loc2),a)) ->
(get_prop_loc (), loc2), a
| _ ->
Options.abort "[Syntax error] Unallowed annotation."
(** Parse a term/pred. *)
let parse_lexpr s =
match Logic_lexer.lexpr (get_buff_loc (), s) with
| Some (_, t) -> t, get_prop_loc ()
| None -> Options.abort "[Syntax error] Invalid logic term"
exception Stmt_not_found of Kernel_function.t
let find_stmt_set ?source find =
let kf = with_current_function ?source () in
let stmts = try find kf with Not_found -> raise (Stmt_not_found kf) in
stmts
let find_loop_stmt_set_from_loop_number ?source number =
find_stmt_set ?source (Statement.find_loop_stmt_set number)
let find_loop_body_set_from_loop_number ?source number =
find_stmt_set ?source (Statement.find_body_stmt_set number)
let find_stmt_set_from_call_to ?source kf_opt num_opt =
find_stmt_set ?source (Statement.find_call2_stmt_set kf_opt num_opt)
let find_stmt_set_from_call_number ?source number =
find_stmt_set ?source (Statement.find_call_stmt_set number)
let find_stmt_set_from_asm_number ?source number =
find_stmt_set ?source (Statement.find_asm_stmt_set number)
let find_stmt_set_from_label ?source label =
find_stmt_set ?source (fun kf -> S_Stmt.singleton !(Kernel_function.find_label kf label))
let find_stmt_set_from_sid ?source local_sid =
find_stmt_set ?source (fun kf -> S_Stmt.singleton (Statement.find_stmt local_sid kf))
let find_stmt_set_from_return ?source () =
find_stmt_set ?source (fun kf -> S_Stmt.singleton (Kernel_function.find_return kf))
let find_stmt_set_from_misc ?source label =
let kf = get_current_function ?source () in
let find_stmt,otherwise =
try
let local_sid = int_of_string label in
(fun () -> Statement.find_stmt local_sid kf),
(fun () -> Options.abort ?source "statement ID %s not found into %a function for ACSL import."
label Kernel_function.pretty kf)
with
| Failure _ ->
let find_stmt =
if label = "return" then
(fun () -> Kernel_function.find_return kf)
else
(fun () -> !(Kernel_function.find_label kf label))
in
find_stmt,
(fun () -> Options.abort ?source "statement label %S not found into %a function for ACSL import."
label Kernel_function.pretty kf)
in
let stmt =
try
find_stmt ()
with Not_found -> otherwise ()
in S_Stmt.singleton stmt
let add_macro ~is_global_scope m =
MacroIndex.add_macro (if is_global_scope then MacroIndex.Sfile else !current_scope) m
let integral_cast ty t =
if Options.AddonIntegerCast.get () then
begin
let loc = t.term_loc in
let source = fst loc in
let ty = Ast_types.remove_attributes_for_logic_type ty in
Options.warning ~wkey:Options.wkey_integer_cast ~source "Casting term %a of type %a into type %a."
Printer.pp_term t Printer.pp_logic_type Linteger Printer.pp_typ ty;
Logic_const.tcast ~loc t ty
end
else
Cabs2cil.integral_cast ty t
let lt_error (source, _ ) fmt = Options.annot_warning ~raising:(fun () -> raise Exit) ~source fmt
let lt_on_error action finally arg =
try action arg
with Exit -> finally (Cil_datatype.Location.unknown,"Error"); raise Exit
(** Add global annotations. *)
let dkey = Options.register_category "trace-pasting"
let add_global_annot g_annots =
let file = !current_module in
let scope = !current_scope in
let module LT =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () = false
let find_macro m = MacroIndex.find_macro scope m
let find_var ?label:_ var = SymbolIndex.find_var_global ~file var
let find_enum_tag s = SymbolIndex.find_enum_item ~file s
let find_comp_field info s =
Cabs2cil.find_field_offset
(fun fi -> fi.forig_name = s)
(Option.value ~default:[] info.cfields)
let find_type tkind s = SymbolIndex.find_type ~file tkind s
let find_label _s = raise Not_found
let integral_cast = integral_cast
let error = lt_error
let on_error = lt_on_error
end)
in
let add_global parsed_g_annot =
LT.annot parsed_g_annot |> function None -> () | Some g_annot ->
if Options.continue_after_typing () then begin
Options.debug ~level:2 ~dkey
"Adding global annotation:@.%a" Printer.pp_global_annotation g_annot;
Annotations.add_global Options.emitter g_annot
end
in
let add_global parsed_g_annot=
try add_global parsed_g_annot
with | Exit ->
Options.annot_error "global annotation ignored by ACSL import."
in
List.iter add_global g_annots
(** Add a function contract. *)
let add_funspec spec loc =
try
let kf = with_current_function ~source:(fst (loc)) () in
let file = !current_module in
let scope = !current_scope in
let module LT =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () = false
let find_macro m = MacroIndex.find_macro scope m
let find_var ?label:_ var = SymbolIndex.find_var_funspec ~file kf var
let find_enum_tag s = SymbolIndex.find_enum_item ~file s
let find_comp_field info s =
Cabs2cil.find_field_offset
(fun fi -> fi.forig_name = s)
(Option.value ~default:[] info.cfields)
let find_type tkind s = SymbolIndex.find_type ~file tkind s
let find_label s = Kernel_function.find_label kf s
let integral_cast = integral_cast
let error = lt_error
let on_error = lt_on_error
end)
in
let vi = Kernel_function.get_vi kf in
let formals = Some (Kernel_function.get_formals kf) in
let typ = Kernel_function.get_type kf in
let old_spec = Annotations.funspec kf in
let behaviors = Logic_utils.get_behavior_names old_spec in
let ({ spec_behavior;
spec_terminates;
spec_variant;
spec_complete_behaviors;
spec_disjoint_behaviors } as spec) =
LT.funspec behaviors vi formals typ spec
in
if Options.continue_after_typing () then begin
Options.debug ~level:2 ~dkey
"Adding function specification:@.%a" Printer.pp_funspec spec;
Annotations.add_behaviors Options.emitter kf spec_behavior;
Option.iter
(Annotations.add_terminates Options.emitter kf)
spec_terminates;
Option.iter
(Annotations.add_decreases Options.emitter kf)
spec_variant;
List.iter
(Annotations.add_complete Options.emitter kf)
spec_complete_behaviors;
List.iter
(Annotations.add_disjoint Options.emitter kf)
spec_disjoint_behaviors
end
with | Kf_not_found
| Exit ->
Options.annot_error "function contract ignored by ACSL import."
(** Add code annotations. *)
let add_annots_aux kf file ?loop_number loc annots stmt =
let scope = !current_scope in
let module LT =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () = Kernel_function.stmt_in_loop kf stmt
let find_macro m = MacroIndex.find_macro scope m
let find_var ?label var =
SymbolIndex.find_var_annot ~file kf stmt ?label var
let find_enum_tag s = SymbolIndex.find_enum_item ~file s
let find_comp_field info s =
Cabs2cil.find_field_offset
(fun fi -> fi.forig_name = s)
(Option.value ~default:[] info.cfields)
let find_type tkind s = SymbolIndex.find_type ~file tkind s
let find_label s = Kernel_function.find_label kf s
let integral_cast = integral_cast
let error = lt_error
let on_error = lt_on_error
end)
in
let add_annot parsed_annot =
let spec = Annotations.funspec kf in
let annot =
LT.code_annot loc
(Logic_utils.get_behavior_names spec)
(Ctype (Kernel_function.get_return_type kf))
parsed_annot
in
let add_annot stmt =
let keep_empty = false in
if Options.continue_after_typing () then begin
match annot.annot_content with
| AStmtSpec (_bhv,_spec) ->
Options.debug ~level:2 ~dkey
"Adding statement contract:@.%a" Printer.pp_code_annotation annot;
Annotations.add_code_annot
~keep_empty Options.emitter ~kf stmt annot
| AAllocation (_bhv,_fa) ->
Options.debug ~level:2 ~dkey
"Adding loop allocation clause:@.%a" Printer.pp_code_annotation annot;
Annotations.add_code_annot
~keep_empty Options.emitter ~kf stmt annot
| AAssigns (_bhv,_a) ->
Options.debug ~level:2 ~dkey
"Adding loop assigns clause:@.%a" Printer.pp_code_annotation annot;
Annotations.add_code_annot
~keep_empty Options.emitter ~kf stmt annot
| AInvariant (bhv,false,pred) when loop_number <> None ->
Options.debug ~level:2 ~dkey
"Adding invariant annotation:@.%a" Printer.pp_code_annotation annot;
let loop_number =
match loop_number with
| Some loop_number -> loop_number
| _ -> assert false
in let add_invariant loop_stmt =
let is_convertible =
match loop_stmt.skind with
| Loop (_li,{blocals=[];bstmts=s::_},_loc,_cont,_brk) when s.sid = stmt.sid -> true
| Loop _ -> false
| _ -> assert false
in let stmt,annot =
if is_convertible then
(Options.debug ~level:2 ~dkey
"Converting invariant into loop invariant for loop #%d" loop_number;
loop_stmt, {annot with annot_content=AInvariant (bhv,true,pred)})
else stmt,annot
in
Annotations.add_code_annot
~keep_empty Options.emitter ~kf stmt annot
in
S_Stmt.iter add_invariant
(try find_loop_stmt_set_from_loop_number loop_number
with Stmt_not_found kf ->
lt_error loc "loop %d not found into %a function for ACSL import"
loop_number Kernel_function.pretty kf)
| _ ->
Options.debug ~level:2 ~dkey
"Adding statement annotation:@.%a"
Printer.pp_code_annotation annot;
Annotations.add_code_annot
~keep_empty Options.emitter ~kf stmt annot
end
in
let loop_stmt =
let rec get_loop_stmt stmt = match stmt.skind with
| Loop _ -> Some stmt
| Block { bstmts=stmt::_ } -> get_loop_stmt stmt
| _ -> None
in get_loop_stmt stmt
in
match loop_stmt with
| None when Logic_utils.is_loop_annot annot ->
lt_error loc "loop annotations are only allowed for loop statements."
| Some loop_stmt when Logic_utils.is_loop_annot annot -> add_annot loop_stmt
| _ -> add_annot stmt
in
let add_annot parsed_annot =
try add_annot parsed_annot
with | Exit ->
Options.annot_error "code annotation ignored by ACSL import."
in
List.iter add_annot annots
let add_annots ?loop_number stmts loc annots =
try
let kf = with_current_function ~source:(fst (loc)) () in
let file = !current_module in
S_Stmt.iter (add_annots_aux kf file ?loop_number loc annots) stmts
with | Kf_not_found ->
Options.annot_error "code annotation ignored by ACSL import."
(** Add Caveat Post clauses as an ensures and an exits clause. *)
let add_post kf id _loc post =
let visitor = object(self)
inherit Visitor.frama_c_inplace
val mutable status = None
method! vterm_lhost term_lhost =
let change_to lvar = ChangeDoChildrenPost (TVar lvar, fun x -> x) in
let continue () = JustCopy in
match status, term_lhost with
| None, TVar{lv_name = "\\exit_status"} ->
let lvar = Cil_const.make_logic_var_quant "exit_status" Linteger in
status <- Some (Normal, lvar, None) ;
change_to lvar
| None, TResult (typ) ->
let lvar = Cil_const.make_logic_var_quant "result" (Ctype typ) in
status <- Some (Exits, lvar, None) ;
change_to lvar
| Some (Normal, lvar, _), TVar{lv_name = "\\exit_status"} ->
change_to lvar
| Some (Exits, lvar, _), TResult (_) ->
change_to lvar
| Some (Normal, lvar, None), TResult (typ) ->
status <-
Some (Normal, lvar,
Some (Cil_const.make_logic_var_quant "result" (Ctype typ)));
continue ()
| Some (Exits, lvar, None), TVar{lv_name = "\\exit_status"} ->
status <-
Some (Exits, lvar,
Some (Cil_const.make_logic_var_quant "exit_status" Linteger));
continue ()
| _ -> continue ()
(** Transform the predicate into two clauses: one ensures + one
exits. *)
method make_post_cond pred =
let new_pred = visitCilPredicate (self :> Cil.cilVisitor) pred in
let make_clause pred kind name =
let nameid = if id = "" then name else (id ^ "_" ^ name) in
kind,
Logic_const.new_predicate {pred with pred_name=nameid::pred.pred_name}
in
let quantif lvar pred =
{pred with pred_content=Pforall([lvar], {pred with pred_name=[]})}
in
let make_other_clause other pred kind =
let other_pred =
match other with
| None -> pred
| Some lvar ->
status <- Some (kind, lvar, None) ;
quantif lvar (visitCilPredicate (self :> Cil.cilVisitor) pred)
in
make_clause other_pred kind
in
match status with
| Some(Normal, lvar, other) ->
[make_clause (quantif lvar new_pred) Normal "at_return" ;
make_other_clause other pred Exits "at_exit" ]
| Some(Exits, lvar, other) ->
[make_other_clause other pred Normal "at_return" ;
make_clause (quantif lvar new_pred) Exits "at_exit" ]
| _ ->
[make_clause new_pred Normal "at_return" ;
make_clause pred Exits "at_exit" ]
end
in
let file = !current_module in
let scope = !current_scope in
let module LT =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () = false
let find_macro m = MacroIndex.find_macro scope m
let find_var ?label:_ var = SymbolIndex.find_var_funspec ~file kf var
let find_enum_tag s = SymbolIndex.find_enum_item ~file s
let find_comp_field info s =
Cabs2cil.find_field_offset
(fun fi -> fi.forig_name = s)
(Option.value ~default:[] info.cfields)
let find_type tkind s = SymbolIndex.find_type ~file tkind s
let find_label s = Kernel_function.find_label kf s
let integral_cast = integral_cast
let error = lt_error
let on_error = lt_on_error
end)
in
let env = Logic_typing.post_state_env Exits
(Ctype (Kernel_function.get_return_type kf))
in
let add_formal env vi =
Logic_typing.add_var vi.vorig_name (cvar_to_lvar vi) env
in
let env = List.fold_left add_formal env (Kernel_function.get_formals kf) in
try
let pred = LT.predicate env post in
if Options.continue_after_typing () then begin
let behavior =
Cil.mk_behavior ~name:id ~post_cond:(visitor#make_post_cond pred) ()
in
Annotations.add_behaviors Options.emitter kf [ behavior ]
end
with | Exit ->
Options.annot_error "extended annotation ignored by ACSL import."
(** Grammar extension for "ensures_and_exits" clauses given into C files. *)
let ensures_and_exits_typer ~typing_context ~loc ps =
match ps with
| [p] ->
begin
let env =
typing_context.Logic_typing.post_state [Normal; Exits] in
let pred =
typing_context.Logic_typing.type_predicate typing_context env p in
let visitor = object(self)
inherit Visitor.frama_c_inplace
val mutable status = None
method! vterm_lhost term_lhost =
let change_to lvar = ChangeDoChildrenPost (TVar lvar, fun x -> x)
and continue () = JustCopy
in match status, term_lhost with
| None, TVar{lv_name = "\\exit_status"} ->
let lvar = Cil_const.make_logic_var_quant "exit_status" Linteger in
status <- Some (Normal, lvar, None) ;
change_to lvar
| None, TResult (typ) ->
let lvar = Cil_const.make_logic_var_quant "result" (Ctype typ) in
status <- Some (Exits, lvar, None) ;
change_to lvar
| Some (Normal, lvar, _), TVar{lv_name = "\\exit_status"} ->
change_to lvar
| Some (Exits, lvar, _), TResult (_) ->
change_to lvar
| Some (Normal, lvar, None), TResult (typ) ->
status <-
Some (Normal, lvar,
Some
(Cil_const.make_logic_var_quant "result" (Ctype typ)));
continue ()
| Some (Exits, lvar, None), TVar{lv_name = "\\exit_status"} ->
status <-
Some (Exits, lvar,
Some
(Cil_const.make_logic_var_quant "exit_status" Linteger));
continue ()
| _ -> continue ()
(** Transform the predicate into two clauses: one ensures + one
exits. *)
method make_post_cond pred =
let new_pred = visitCilPredicate (self :> Cil.cilVisitor) pred
and make_clause pred name =
let pred_name = name :: pred.pred_name in {pred with pred_name}
and quantif lvar pred =
{pred with pred_content=Pforall([lvar], {pred with pred_name=[]})}
in
let make_other_clause other pred kind =
let other_pred =
match other with
| None -> pred
| Some lvar ->
status <- Some (kind, lvar, None) ;
quantif lvar
(visitCilPredicate (self :> Cil.cilVisitor) pred)
in
make_clause other_pred
in
match status with
| Some(Normal, lvar, other) ->
[make_clause (quantif lvar new_pred) "at_return" ;
make_other_clause other pred Exits "at_exit" ]
| Some(Exits, lvar, other) ->
[make_other_clause other pred Normal "at_return" ;
make_clause (quantif lvar new_pred) "at_exit" ]
| _ ->
[make_clause new_pred "at_return";
make_clause pred "at_exit"]
end
in
Ext_preds (visitor#make_post_cond pred)
end
| _ ->
typing_context.Logic_typing.error loc
"[Syntax error] Expecting a predicate after keyword ensures_and_exits."
let clause_extension = "ensures_and_exits"
let () =
let clause_typer typing_context loc ps =
if Options.AddonEnsuresAndExits.get () then
ensures_and_exits_typer ~typing_context ~loc ps
else typing_context.Logic_typing.error loc
"[Setting error] Rejected clause extension: %s." clause_extension
in
Acsl_extension.register_behavior ~plugin:"acsl_importer"
clause_extension clause_typer false
let () =
let dkey = Options.register_category "trace-ensures-and-exits" in
let code_transformation =
File.register_code_transformation_category clause_extension
in
let mk_clause p =
let kind =
match p.pred_name with
| "at_exit" :: _ -> Exits
| "at_return" :: _ -> Normal
| _ ->
Options.fatal
"Unrecognized predicate in %s extension %a"
clause_extension Printer.pp_predicate p
in
let pred_name = match p.pred_name with
| name::first::tl -> (name ^ "_" ^ first)::tl
| _ -> p.pred_name
in
let pred = Logic_const.new_predicate { p with pred_name } in
Options.debug ~level:2 ~dkey
"Adding clause: %s %a@." (Cil_printer.get_termination_kind_name kind)
Cil_printer.pp_identified_predicate pred;
kind, pred
in
let transform ast =
let vis =
object(self)
inherit Visitor.frama_c_inplace
val mutable active = None
method! vcode_annot ca =
match ca.annot_content with
| AStmtSpec(a,_) ->
active <- Some a;
DoChildrenPost (fun r -> active <- None; r)
| _ -> SkipChildren
method! vbehavior bhv =
let my_ext =
List.filter
(fun {ext_name} -> ext_name = clause_extension) bhv.b_extended
in
match my_ext with
| [] -> SkipChildren
| _ ->
List.iter
(fun clause_extension ->
Options.debug ~level:2 ~dkey
"Removing clause: %a@."
Cil_printer.pp_extended clause_extension;
Annotations.remove_extended Emitter.end_user
(Option.get self#current_kf)
clause_extension;
Annotations.remove_extended Options.emitter
(Option.get self#current_kf)
clause_extension
)
my_ext;
let clauses =
List.concat
(List.map
(function
| {ext_kind = Ext_preds l} -> List.map mk_clause l
| _ ->
Options.fatal
"Unrecognized content of extension %s"
clause_extension)
my_ext)
in
let kf = Option.get self#current_kf in
let stmt = self#current_stmt in
let behavior =
if Cil.is_default_behavior bhv then None else Some bhv.b_name
in
Annotations.add_ensures
Options.emitter kf ?stmt ?active ?behavior clauses;
SkipChildren
end
in
Visitor.visitFramacFileSameGlobals vis ast
in
let deps =
[(module Options.AddonEnsuresAndExits: Parameter_sig.S)]
in
let after = [Options.main_import] in
File.add_code_transformation_after_cleanup
~deps ~after code_transformation transform
(** Do not forget "Implicit state variables" for plug-in API: *)
let paste_global_annot s =
let global_annot = parse_global s in
add_global_annot global_annot
(** Do not forget "Implicit state variables" for plug-in API: *)
let paste_fun_spec s =
let fun_spec, loc = parse_spec s in
add_funspec fun_spec loc
(** Do not forget "Implicit state variables" for plug-in API: *)
let paste_postcond kf id s =
let post, loc = parse_lexpr s in
add_post kf id loc post
(** Do not forget "Implicit state variables" for plug-in API: *)
let paste_code_annot ?loop_number stmts s =
let loc, annots = parse_annots s in
add_annots ?loop_number stmts loc annots
let dkey = Options.register_category "trace-importations"
let paste_at_global ~clause =
let prop = Buffer.contents buffer in
Options.debug ~level:2 ~dkey
"Importing %s %s;@." clause prop ;
paste_global_annot (clause ^ " " ^ prop ^ ";")
let paste_at_func ~clause =
let prop = Buffer.contents buffer in
Options.debug ~level:2 ~dkey
"Importing %s %s;@." clause prop ;
paste_fun_spec (clause ^ " " ^ prop ^ ";")
let paste_at_func_behavior ~clause ~behav =
let prop = Buffer.contents buffer in
let prop = clause ^ " " ^ prop ^ ";" in
let prop = if behav = "" then prop else ("behavior " ^ behav ^ ": " ^ prop) in
Options.debug ~level:2 ~dkey
"Importing %s@." prop ;
paste_fun_spec prop
let paste_post ~behav =
let prop = Buffer.contents buffer in
Options.debug ~level:2 ~dkey
"Importing ensures_and_exits %s: %s;@." behav prop ;
let kf = get_current_function () in
paste_postcond kf behav prop
let paste_loop_body ~clause ~loop =
let prop = Buffer.contents buffer in
Options.debug ~level:2 ~dkey
"Importing AT loop %s: %s %s;@." loop clause prop ;
let loop_number = int_of_string loop in
let stmts = try find_loop_body_set_from_loop_number loop_number
with Stmt_not_found kf ->
Options.abort "loop body %d not found into %a function for ACSL import."
loop_number Kernel_function.pretty kf
in paste_code_annot ~loop_number stmts (clause ^ " " ^ prop ^ ";")
let paste_code ~clause ~label =
let prop = Buffer.contents buffer in
Options.debug ~level:2 ~dkey
"Importing AT %s: %s %s;@." label clause prop ;
let stmts = find_stmt_set_from_misc label
in paste_code_annot stmts (clause ^ " " ^ prop ^ ";")
let paste_at_stmt ~clause ~loop ~label =
if loop = "" then paste_code ~clause ~label
else paste_loop_body ~clause ~loop
let paste_at_loop ~clause ~loop =
let prop = Buffer.contents buffer in
Options.debug ~level:2 ~dkey
"Importing AT loop %s: loop %s %s;@." loop clause prop ;
let loop_number = int_of_string loop in
let stmts = try find_loop_stmt_set_from_loop_number loop_number
with Stmt_not_found kf ->
Options.abort "loop %d not found into %a function for ACSL import."
loop_number Kernel_function.pretty kf
in paste_code_annot stmts ("loop " ^ clause ^ " " ^ prop ^ ";")
let init_pasting ~pfile ~pline ?(bline=pline) ~cfile ast =
init_ast ~file:cfile ~init_module_from_file_name:true ~init_typenames:true ast;
prop_file := (Filepath.of_string pfile) ;
prop_line := pline ;
buff_line := bline
(** For external plug-in API: *)
let paste_global_annot ~pfile ~pline ~cfile s ast =
init_pasting ~pfile ~pline ~cfile ast ;
paste_global_annot s
let dkey = Options.register_category "trace-actions"
(** For external plug-in API: *)
let paste_fun_spec kf ~pfile ~pline ~cfile s ast =
init_pasting ~pfile ~pline ~cfile ast ;
Options.debug ~level:2 ~dkey
"Set current function to %a@." Kernel_function.pretty kf ;
current_function := Some kf ;
paste_fun_spec s
(** For external plug-in API: *)
let paste_code_annot kf stmt ~pfile ~pline ~cfile s ast=
init_pasting ~pfile ~pline ~cfile ast;
Options.debug ~level:2 ~dkey
"Set current function to %a@." Kernel_function.pretty kf ;
current_function := Some kf ;
paste_code_annot (S_Stmt.singleton stmt) s