Source file data_for_aorai.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
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
1933
1934
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
1954
1955
1956
1957
1958
1959
1960
1961
1962
1963
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
2026
2027
2028
2029
2030
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
2056
2057
2058
2059
2060
2061
2062
2063
2064
2065
2066
2067
2068
2069
2070
2071
2072
2073
2074
2075
2076
2077
2078
2079
2080
2081
2082
2083
2084
2085
2086
2087
2088
2089
2090
2091
2092
2093
2094
2095
2096
2097
2098
2099
2100
2101
2102
2103
2104
2105
2106
2107
2108
2109
2110
2111
2112
2113
2114
2115
2116
2117
2118
2119
2120
2121
2122
2123
2124
2125
2126
2127
2128
2129
2130
2131
2132
2133
2134
2135
2136
2137
2138
2139
2140
2141
2142
2143
2144
2145
2146
2147
2148
2149
2150
2151
2152
2153
2154
2155
2156
2157
2158
2159
2160
2161
2162
2163
2164
2165
2166
2167
2168
2169
2170
2171
2172
2173
2174
2175
2176
2177
2178
2179
2180
2181
2182
2183
2184
2185
2186
2187
2188
2189
2190
2191
2192
2193
2194
2195
2196
2197
2198
2199
2200
2201
2202
2203
2204
2205
2206
2207
2208
2209
2210
2211
2212
2213
2214
2215
2216
2217
2218
2219
2220
2221
2222
2223
2224
2225
2226
2227
2228
2229
2230
2231
2232
2233
2234
2235
2236
2237
2238
2239
2240
2241
2242
2243
2244
2245
2246
2247
2248
2249
2250
2251
2252
2253
2254
2255
2256
2257
2258
2259
2260
2261
2262
2263
2264
2265
2266
2267
2268
2269
2270
2271
2272
2273
2274
2275
2276
2277
2278
2279
2280
2281
2282
2283
2284
2285
2286
2287
2288
2289
2290
2291
2292
2293
2294
2295
2296
2297
2298
2299
2300
2301
2302
2303
2304
2305
2306
2307
2308
2309
2310
open Logic_ptree
open Cil
open Cil_types
open Automaton_ast
open Logic_simplification
exception Empty_automaton
let typing_dkey = Aorai_option.register_category "type-automaton"
module Aorai_state =
Datatype.Make_with_collections(
struct
type t = Automaton_ast.state
let structural_descr = Structural_descr.t_abstract
let reprs = [ { nums = -1; name = ""; multi_state = None;
acceptation = Bool3.False; init = Bool3.False
} ]
let name = "Aorai_state"
let equal x y = Datatype.Int.equal x.nums y.nums
let hash x = x.nums
let rehash = Datatype.identity
let compare x y = Datatype.Int.compare x.nums y.nums
let copy = Datatype.identity
let pretty fmt x = Format.fprintf fmt "state_%d" x.nums
let mem_project = Datatype.never_any_project
end
)
module Aorai_typed_trans =
Datatype.Make_with_collections(
struct
let name = "Aorai_typed_trans"
type t = Automaton_ast.typed_trans
let structural_descr = Structural_descr.t_abstract
let reprs = [ { numt = -1; start = List.hd (Aorai_state.reprs);
stop = List.hd (Aorai_state.reprs);
cross = TTrue; actions=[]; } ]
let equal x y = Datatype.Int.equal x.numt y.numt
let hash x = x.numt
let rehash = Datatype.identity
let compare x y = Datatype.Int.compare x.numt y.numt
let copy = Datatype.identity
let pretty = Pretty_automaton.Typed.print_transition
let mem_project = Datatype.never_any_project
end)
module Aorai_automaton =
Datatype.Make(
struct
include Datatype.Serializable_undefined
let name = "Aorai_automaton"
type t = Automaton_ast.typed_automaton
let structural_descr = Structural_descr.t_abstract
let reprs = [ { states = Aorai_state.reprs;
trans = Aorai_typed_trans.reprs;
metavariables = Datatype.String.Map.empty;
observables = Some Datatype.String.Set.empty;
}]
end
)
module State_var =
State_builder.Hashtbl
(Aorai_state.Hashtbl)
(Cil_datatype.Varinfo)
(struct
let name = "Data_for_aorai.State_var"
let dependencies = [ Ast.self; Aorai_option.Ya.self ]
let size = 7
end)
let get_state_var =
let add_var state = Cil.makeGlobalVar ~ghost:true state.name Cil_const.intType in
State_var.memo add_var
let get_state_logic_var state = Cil.cvar_to_lvar (get_state_var state)
module Max_value_counter =
State_builder.Hashtbl
(Cil_datatype.Term.Hashtbl)
(Cil_datatype.Term)
(struct
let name = "Data_for_aorai.Max_value_counter"
let dependencies = [ Ast.self; Aorai_option.Ya.self ]
let size = 7
end)
let find_max_value t =
try Some (Max_value_counter.find t) with Not_found -> None
let por t1 t2 =
match t1,t2 with
PTrue,_ | _,PTrue -> PTrue
| PFalse,t | t,PFalse -> t
| _,_ -> POr(t1,t2)
let pand t1 t2 =
match t1,t2 with
PTrue,t | t,PTrue -> t
| PFalse,_ | _,PFalse -> PFalse
| _,_ -> PAnd(t1,t2)
let pnot t =
match t with
PTrue -> PFalse
| PFalse -> PTrue
| PNot t -> t
| _ -> PNot t
let rec is_same_expression e1 e2 =
match e1,e2 with
| PVar x, PVar y -> x = y
| PVar _,_ | _,PVar _ -> false
| PCst cst1, PCst cst2 -> Logic_utils.is_same_pconstant cst1 cst2
| PCst _,_ | _,PCst _ -> false
| PPrm (f1,x1), PPrm(f2,x2) -> f1 = f2 && x1 = x2
| PPrm _,_ | _,PPrm _ -> false
| PMetavar x, PMetavar y -> x = y
| PMetavar _,_ | _,PMetavar _ -> false
| PBinop(b1,l1,r1), PBinop(b2,l2,r2) ->
b1 = b2 && is_same_expression l1 l2 && is_same_expression r1 r2
| PBinop _, _ | _, PBinop _ -> false
| PUnop(u1,e1), PUnop(u2,e2) -> u1 = u2 && is_same_expression e1 e2
| PUnop _,_ | _,PUnop _ -> false
| PArrget(a1,i1), PArrget(a2,i2) ->
is_same_expression a1 a2 && is_same_expression i1 i2
| PArrget _,_ | _,PArrget _ -> false
| PField(e1,f1), PField(e2,f2) -> f1 = f2 && is_same_expression e1 e2
| PField _,_ | _,PField _ -> false
| PArrow(e1,f1), PArrow(e2,f2) -> f1 = f2 && is_same_expression e1 e2
let declared_logics = Hashtbl.create 97
let add_logic name log_info = Hashtbl.replace declared_logics name log_info
let get_logic name =
try Hashtbl.find declared_logics name
with Not_found ->
Aorai_option.fatal "Logic function '%s' not declared in hashtbl" name
let declared_predicates = Hashtbl.create 97
let add_predicate name pred_info =
Hashtbl.replace declared_predicates name pred_info
let get_predicate name =
try Hashtbl.find declared_predicates name
with Not_found ->
Aorai_option.fatal "Predicate '%s' not declared in hashtbl" name
let transStart = "aorai_Trans_Start"
let transStop = "aorai_Trans_Stop"
let transCond = "aorai_Trans_Cond"
let transCondP = "aorai_Trans_Cond_param"
let loopInit = "aorai_Loop_Init"
let curState = "aorai_CurStates"
let history n = "aorai_StatesHistory_" ^ string_of_int n
let whole_history () =
let rec aux acc n =
if n > 0 then aux (history n :: acc) (n - 1) else acc
in
aux [] (Aorai_option.InstrumentationHistory.get ())
let curTrans = "aorai_CurTrans"
let curOp = "aorai_CurOperation"
let curOpStatus = "aorai_CurOpStatus"
let acceptSt = "aorai_AcceptStates"
let nbOp = "aorai_NbOper"
let nbAcceptSt = "aorai_NbAcceptStates"
let nbTrans = "aorai_NbTrans"
let macro_ligth = "aorai_Macro_Prop_St_Tr_Without_Conds"
let macro_full = "aorai_Macro_Prop_St_Tr"
let macro_pure = "aorai_Macro_Op_without_sub_call"
let listOp = "aorai_ListOper"
let listStatus = "aorai_OpStatusList"
let callStatus = "aorai_Called"
let termStatus = "aorai_Terminated"
let states = "aorai_States"
let buch_sync = "Aorai_Sync"
module Automaton =
State_builder.Ref
(Datatype.Option(Aorai_automaton))
(struct
let name = "Data_for_aorai.Automaton"
let dependencies = [ Aorai_option.Ya.self ]
let default () = None
end)
let cond_of_parametrizedTransitions = ref (Array.make (1) [[]])
let defined_functions = ref []
let ignored_functions = ref []
(** Return the buchi automaton as stored after parsing *)
let getAutomata () =
match Automaton.get() with
| Some auto -> auto
| None ->
Aorai_option.fatal "The automaton has not been compiled yet"
let getGraph () =
let auto = getAutomata () in
auto.states, auto.trans
(** Return the number of transitions of the automaton *)
let getNumberOfTransitions () =
List.length (getAutomata ()).trans
(** Return the number of states of the automaton *)
let getNumberOfStates () =
List.length (getAutomata ()).states
let is_c_global name =
try ignore (Globals.Vars.find_from_astinfo name Global); true
with Not_found ->
try ignore (Globals.Functions.find_by_name name); true
with Not_found -> false
let get_fresh =
let used_names = Hashtbl.create 5 in
fun name ->
if Clexer.is_c_keyword name
|| Logic_lexer.is_acsl_keyword name || is_c_global name
|| Hashtbl.mem used_names name
then begin
let i = ref (try Hashtbl.find used_names name with Not_found -> 0) in
let proposed_name () = name ^ "_" ^ string_of_int !i in
while is_c_global (proposed_name()) do incr i done;
Hashtbl.replace used_names name (!i+1);
proposed_name ()
end
else begin
Hashtbl.add used_names name 0;
name
end
module AuxVariables =
State_builder.List_ref
(Cil_datatype.Varinfo)
(struct
let name = "Data_for_aorai.AuxVariables"
let dependencies = [ Aorai_option.Ya.self; Ast.self ]
end)
module AbstractLogicInfo =
State_builder.List_ref
(Cil_datatype.Logic_info)
(struct
let name = "Data_for_aorai.AbstractLogicInfo"
let dependencies = [ Aorai_option.Ya.self; Ast.self ]
end)
class change_var vi1 vi2 =
object
inherit Visitor.frama_c_copy (Project.current ())
method! vlogic_var_use vi =
if Cil_datatype.Logic_var.equal vi1 vi then ChangeTo vi2 else SkipChildren
end
let change_var_term vi1 vi2 t =
Visitor.visitFramacTerm (new change_var vi1 vi2) t
let update_condition vi1 vi2 cond =
let rec aux e =
match e with
| TOr (e1,e2) -> TOr(aux e1, aux e2)
| TAnd (e1,e2) -> TAnd(aux e1, aux e2)
| TNot e -> TNot (aux e)
| TCall _ | TReturn _ | TTrue | TFalse -> e
| TRel(rel,t1,t2) ->
TRel(rel,change_var_term vi1 vi2 t1,change_var_term vi1 vi2 t2)
in aux cond
let pebble_set_at li lab =
assert (li.l_profile = []);
let labels = List.map (fun _ -> lab) li.l_labels in
Logic_const.term (Tapp (li,labels,[])) (Option.get li.l_type)
let memo_multi_state st =
match st.multi_state with
| None ->
let aux =
Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_aux") Cil_const.intType
in
let laux = Cil.cvar_to_lvar aux in
let set = Cil_const.make_logic_info (get_fresh (st.name ^ "_pebble")) in
let typ = Logic_const.make_set_type (Ctype Cil_const.intType) in
set.l_var_info.lv_type <- typ;
set.l_labels <- [FormalLabel "L"];
set.l_type <- Some typ;
set.l_body <-
LBreads
[ Logic_const.new_identified_term (Logic_const.tvar laux) ];
let multi_state = set,laux in
st.multi_state <- Some multi_state;
multi_state
| Some multi_state -> multi_state
let change_bound_var st1 st2 cond =
if Option.is_some st1.multi_state then begin
let (_,idx1) = Option.get st1.multi_state in
let (_,idx2) = memo_multi_state st2 in
update_condition idx1 idx2 cond
end else cond
let add_aux_variable vi = AuxVariables.add vi
let aux_variables = AuxVariables.get
let abstract_logic_info = AbstractLogicInfo.get
module StateIndex =
State_builder.Counter(struct let name = "Data_for_aorai.StateIndex" end)
module TransIndex =
State_builder.Counter(struct let name = "Data_for_aorai.TransIndex" end)
let new_state name =
{ name = get_fresh name; acceptation = Bool3.False;
init = Bool3.False; nums = StateIndex.next();
multi_state = None
}
let new_intermediate_state () = new_state "aorai_intermediate_state"
let new_trans start stop cross actions =
{ start; stop; cross; actions; numt = TransIndex.next () }
let check_states s =
let {states;trans} = getAutomata() in
let max = getNumberOfStates () in
List.iter
(fun x -> if x.nums >= max then
Aorai_option.fatal "%s: State %d found while max id is supposed to be %d"
s x.nums max)
states;
List.iter
(fun x ->
try
let y = List.find (fun y -> x.nums = y.nums && not (x==y)) states in
Aorai_option.fatal "%s: State %s and %s share same id %d"
s x.name y.name x.nums
with Not_found -> ()
)
states;
List.iter
(fun x ->
if not (List.memq x.start states) then
Aorai_option.fatal
"%s: Start state %d of transition %d is not among known states"
s x.start.nums x.numt;
if not (List.memq x.stop states) then
Aorai_option.fatal
"%s: End state %d of transition %d is not among known states"
s x.start.nums x.numt;)
trans
let cst_one = PCst (Logic_ptree.IntConstant "1")
let cst_zero = PCst (Logic_ptree.IntConstant "0")
let is_cst_zero e =
match e with
| PCst(IntConstant "0") -> true
| _ -> false
let is_cst_one e =
match e with
PCst (IntConstant "1") -> true
| _ -> false
let is_single elt =
match elt.min_rep, elt.max_rep with
| Some min, Some max -> is_cst_one min && is_cst_one max
| _ -> false
type 'a eps = Normal of 'a | Epsilon of 'a
let print_eps f fmt = function
| Normal x -> f fmt x
| Epsilon x -> Format.fprintf fmt "epsilon-trans:@\n%a" f x
let print_eps_trans fmt tr =
Format.fprintf fmt "%s -> %s:@[%a%a@]"
tr.start.name tr.stop.name
(print_eps Pretty_automaton.Typed.print_condition) tr.cross
Pretty_automaton.Typed.print_actionl tr.actions
type current_event =
| ECall of
kernel_function
* Cil_types.logic_var Cil_datatype.Varinfo.Hashtbl.t
* (typed_condition eps,typed_action) Automaton_ast.trans
| EReturn of kernel_function
| ECOR of kernel_function
| ENone
| EMulti
let add_current_event event env cond =
let is_empty tbl = Cil_datatype.Varinfo.Hashtbl.length tbl = 0 in
match env with
[] -> assert false
| old_event :: tl ->
match event, old_event with
| ENone, _ -> env, cond
| _, ENone -> event::tl, cond
| ECall (kf1,_,_), ECall (kf2,_,_)
when Kernel_function.equal kf1 kf2 -> env, cond
| ECall (kf1,tbl1,_), ECall (kf2,tbl2,_)->
if is_empty tbl1 && is_empty tbl2 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: two call events for distinct \
functions %a and %a at the same time."
Kernel_function.pretty kf1 Kernel_function.pretty kf2
| ECall (_,_,_), EMulti -> event::tl, cond
| ECall (kf1,tbl1,_), EReturn kf2 ->
if is_empty tbl1 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: trying to call %a and \
return from %a at the same time."
Kernel_function.pretty kf1 Kernel_function.pretty kf2
| ECall(kf1,_,_), ECOR kf2
when Kernel_function.equal kf1 kf2 ->
event::tl, cond
| ECall (kf1,tbl1,_), ECOR kf2 ->
if is_empty tbl1 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: trying to call %a and \
call or return from %a at the same time."
Kernel_function.pretty kf1 Kernel_function.pretty kf2
| EReturn kf1, ECall(kf2,tbl2,_) ->
if is_empty tbl2 then ENone::tl, TFalse
else
Aorai_option.abort
"specification is inconsistent: trying to call %a and \
return from %a at the same time."
Kernel_function.pretty kf2 Kernel_function.pretty kf1
| EReturn kf1, (ECOR kf2 | EReturn kf2)
when Kernel_function.equal kf1 kf2 -> event::tl, cond
| EReturn _, EReturn _ -> ENone::tl, TFalse
| EReturn _, ECOR _ -> ENone::tl, TFalse
| EReturn _, EMulti -> ENone::tl, TFalse
| (EMulti | ECOR _), _ -> assert false
let merge_current_event env1 env2 cond1 cond2 =
assert (List.tl env1 == List.tl env2);
let old_env = List.tl env2 in
match List.hd env1, List.hd env2 with
| ENone, _ -> env2, tor cond1 cond2
| _, ENone -> env1, tor cond1 cond2
| ECall(kf1,_,_), ECall(kf2,_,_)
when Kernel_function.equal kf1 kf2 -> env2, tor cond1 cond2
| ECall _, ECall _ -> EMulti::old_env, tor cond1 cond2
| ECall _, EMulti -> env2, tor cond1 cond2
| ECall (kf1,_,_), ECOR kf2 when Kernel_function.equal kf1 kf2 ->
env2, tor cond1 cond2
| ECall (kf1,_,_), EReturn kf2 when Kernel_function.equal kf1 kf2 ->
ECOR kf1 :: old_env, tor cond1 cond2
| ECall _, (ECOR _ | EReturn _) -> EMulti :: old_env, tor cond1 cond2
| EReturn kf1, ECall (kf2,_,_) when Kernel_function.equal kf1 kf2 ->
ECOR kf1 :: old_env, tor cond1 cond2
| EReturn _, ECall _ -> EMulti :: old_env, tor cond1 cond2
| EReturn kf1, EReturn kf2 when Kernel_function.equal kf1 kf2 ->
env2, tor cond1 cond2
| EReturn _, EReturn _ -> EMulti :: old_env, tor cond1 cond2
| EReturn _, EMulti -> env2, tor cond1 cond2
| EReturn kf1, ECOR kf2 when Kernel_function.equal kf1 kf2 ->
env2, tor cond1 cond2
| EReturn _, ECOR _ ->
EMulti :: old_env, tor cond1 cond2
| ECOR kf1, (ECall(kf2,_,_) | EReturn kf2 | ECOR kf2)
when Kernel_function.equal kf1 kf2 -> env1, tor cond1 cond2
| ECOR _, (ECall _ | EReturn _ | ECOR _) ->
EMulti :: old_env, tor cond1 cond2
| ECOR _, EMulti -> env2, tor cond1 cond2
| EMulti, (ECall _ | EReturn _ | ECOR _) -> env1, tor cond1 cond2
| EMulti, EMulti -> EMulti::old_env, tor cond1 cond2
let get_bindings st my_var =
let my_lval = TVar my_var, TNoOffset in
match st with
None -> my_lval
| Some st ->
let (_,idx) = memo_multi_state st in
Logic_const.addTermOffsetLval (TIndex (Logic_const.tvar idx,TNoOffset)) my_lval
let get_bindings_term st my_var typ =
Logic_const.term (TLval (get_bindings st my_var)) typ
let memo_aux_variable tr counter used_prms vi =
try
let my_var = Cil_datatype.Varinfo.Hashtbl.find used_prms vi in
get_bindings_term counter my_var (Ctype vi.vtype)
with Not_found ->
let my_type =
match counter with
| None -> vi.vtype
| Some _ -> TArray(vi.vtype,None,[])
in
let my_var =
Cil.makeGlobalVar ~ghost:true (get_fresh ("aorai_" ^ vi.vname)) my_type
in
add_aux_variable my_var;
let my_lvar = Cil.cvar_to_lvar my_var in
Cil_datatype.Varinfo.Hashtbl.add used_prms vi my_lvar;
(match tr.cross with
| Normal _ ->
let st = Option.map (fun _ -> tr.stop) counter in
let loc = get_bindings st my_lvar in
let copy = Copy_value (loc,Logic_const.tvar (Cil.cvar_to_lvar vi)) in
tr.actions <- copy :: tr.actions
| Epsilon _ ->
Aorai_option.fatal "Epsilon transition used as Call event"
);
get_bindings_term counter my_lvar (Ctype vi.vtype)
let check_one top info counter s =
match info with
| ECall (kf,used_prms,tr) ->
Globals.Syntactic_search.find_in_scope ~strict:true s (Formal kf) |>
(Fun.flip Option.bind
(fun vi ->
if top then Some (Logic_const.tvar (Cil.cvar_to_lvar vi))
else Some (memo_aux_variable tr counter used_prms vi)))
| EReturn kf when top && ( Datatype.String.equal s "return"
|| Datatype.String.equal s "\\result") ->
let rt = Kernel_function.get_return_type kf in
if Cil.isVoidType rt then
Aorai_option.abort
"%a returns void. \\result is meaningless in this context"
Kernel_function.pretty kf;
Some (Logic_const.term (TLval (TResult rt,TNoOffset)) (Ctype rt))
| ECOR _ | EReturn _ | EMulti | ENone -> None
let find_metavar s metaenv =
try
Datatype.String.Map.find s metaenv
with Not_found ->
Aorai_option.abort "Metavariable %s not declared" s
let find_in_env env counter s =
let current, stack =
match env with
| current::stack -> current, stack
| [] -> Aorai_option.fatal "Empty type-checking environment"
in
match check_one true current counter s with
Some lv -> lv
| None ->
let module M = struct exception Found of term end in
(try
List.iter
(fun x ->
match check_one false x counter s with
None -> ()
| Some lv -> raise (M.Found lv))
stack;
(match Globals.Syntactic_search.find_in_scope s Program with
| Some vi -> Logic_const.tvar (Cil.cvar_to_lvar vi)
| None -> Aorai_option.abort "Unknown variable %s" s)
with
M.Found lv -> lv)
let find_prm_in_env env ?tr counter f x =
let kf =
try Globals.Functions.find_by_name f
with Not_found -> Aorai_option.abort "Unknown function %s" f
in
if Datatype.String.equal x "return" ||
Datatype.String.equal x "\\result" then begin
let rt = Kernel_function.get_return_type kf in
if Cil.isVoidType rt then
Aorai_option.abort
"%a returns void. %s().%s is meaningless in this context"
Kernel_function.pretty kf f x;
let env,cond = add_current_event (EReturn kf) env (TReturn kf) in
env,
Logic_const.term (TLval (TResult rt,TNoOffset)) (Ctype rt),
cond
end else begin
let rec treat_env top =
function
| ECall(kf',_,_) as event :: _
when Kernel_function.equal kf kf'->
(match check_one top event counter x with
Some lv ->
env, lv, TTrue
| None ->
Aorai_option.abort "Function %s has no parameter %s" f x)
| (ENone | EReturn _ | EMulti | ECOR _ | ECall _ )
:: tl ->
treat_env false tl
| [] ->
let env, cond =
match tr with
None ->
Aorai_option.abort
"Function %s is not in the call stack. \
Cannot use its parameter %s here" f x
| Some tr ->
add_current_event
(ECall (kf, Cil_datatype.Varinfo.Hashtbl.create 3, tr))
env
(TCall (kf,None))
in
let vi =
match
Globals.Syntactic_search.find_in_scope ~strict:true x (Formal kf)
with
| Some vi -> vi
| None -> Aorai_option.abort "Function %s has no parameter %s" f x
in
env, Logic_const.tvar (Cil.cvar_to_lvar vi), cond
in treat_env true env
end
module C_logic_env =
struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () = false
let find_macro _ = raise Not_found
let find_var ?label:_ _ = raise Not_found
let find_enum_tag _ = raise Not_found
let find_comp_field info s =
let field = Cil.getCompField info s in
Field(field,NoOffset)
let find_type _ = raise Not_found
let find_label _ = raise Not_found
let integral_cast ty t =
Aorai_option.abort
"term %a has type %a, but %a is expected."
Printer.pp_term t Printer.pp_logic_type Linteger Printer.pp_typ ty
let error (source,_) msg = Aorai_option.abort ~source msg
let on_error f _ x = f x
end
module LTyping = Logic_typing.Make(C_logic_env)
let type_expr metaenv env ?tr ?current e =
let loc = Cil_datatype.Location.unknown in
let rec aux env cond e =
match e with
| PVar s ->
let var = find_in_env env current s in
env, var, cond
| PPrm(f,x) -> find_prm_in_env env ?tr current f x
| PMetavar s ->
let var = Logic_const.tvar (Cil.cvar_to_lvar (find_metavar s metaenv)) in
env, var, cond
| PCst (Logic_ptree.IntConstant s) ->
let e = Cil.parseIntLogic ~loc s in
env, e, cond
| PCst (Logic_ptree.FloatConstant str) ->
env, Logic_utils.parse_float ~loc str, cond
| PCst (Logic_ptree.StringConstant s) ->
let t =
Logic_const.term
(TConst(LStr (Logic_typing.unescape s))) (Ctype Cil_const.charPtrType)
in
env,t,cond
| PCst (Logic_ptree.WStringConstant s) ->
let t =
Logic_const.term
(TConst (LWStr (Logic_typing.wcharlist_of_string s)))
(Ctype (TPtr(Machine.wchar_type (),[])))
in env,t,cond
| PBinop(bop,e1,e2) ->
let op = Logic_typing.type_binop bop in
let env,e1,cond = aux env cond e1 in
let env,e2,cond = aux env cond e2 in
let t1 = e1.term_type in
let t2 = e2.term_type in
let t =
if Logic_typing.is_arithmetic_type t1
&& Logic_typing.is_arithmetic_type t2
then
let t = Logic_typing.arithmetic_conversion t1 t2 in
Logic_const.term
(TBinOp (op,LTyping.mk_cast e1 t,LTyping.mk_cast e2 t))
t
else
(match bop with
| Logic_ptree.Badd
when
Logic_typing.is_integral_type t2
&& Logic_utils.isLogicPointerType t1 ->
Logic_const.term (TBinOp (PlusPI,e1,e2)) t1
| Logic_ptree.Bsub
when
Logic_typing.is_integral_type t2
&& Logic_utils.isLogicPointerType t1 ->
Logic_const.term (TBinOp (MinusPI,e1,e2)) t1
| Logic_ptree.Badd
when
Logic_typing.is_integral_type t1
&& Logic_utils.isLogicPointerType t2 ->
Logic_const.term (TBinOp (PlusPI,e2,e1)) t2
| Logic_ptree.Bsub
when
Logic_typing.is_integral_type t1
&& Logic_utils.isLogicPointerType t2 ->
Logic_const.term (TBinOp (MinusPI,e2,e1)) t2
| Logic_ptree.Bsub
when
Logic_utils.isLogicPointerType t1
&& Logic_utils.isLogicPointerType t2 ->
Logic_const.term
(TBinOp (MinusPP,e1,LTyping.mk_cast e2 t1))
Linteger
| _ ->
Aorai_option.abort
"Invalid operands for binary operator %a: \
unexpected %a and %a"
Printer.pp_binop op
Printer.pp_term e1
Printer.pp_term e2)
in
env, t, cond
| PUnop(Logic_ptree.Uminus,e) ->
let env,t,cond = aux env cond e in
if Logic_typing.is_arithmetic_type t.term_type then
env,Logic_const.term (TUnOp (Neg,t)) Linteger,cond
else Aorai_option.abort
"Invalid operand for unary -: unexpected %a" Printer.pp_term t
| PUnop(Logic_ptree.Ubw_not,e) ->
let env,t,cond = aux env cond e in
if Logic_typing.is_arithmetic_type t.term_type then
env,Logic_const.term (TUnOp (BNot,t)) Linteger,cond
else Aorai_option.abort
"Invalid operand for bitwise not: unexpected %a" Printer.pp_term t
| PUnop(Logic_ptree.Uamp,e) ->
let env, t, cond = aux env cond e in
(match t.term_node with
| TLval v | TStartOf v ->
begin try
env, Logic_utils.mk_logic_AddrOf v t.term_type, cond
with Failure _ ->
Aorai_option.abort "Cannot take address: not a C type(%a): %a"
Printer.pp_logic_type t.term_type Printer.pp_term t
end
| _ ->
Aorai_option.abort "Cannot take address: not an lvalue %a"
Printer.pp_term t
)
| PUnop (Logic_ptree.Ustar,e) ->
let env, t, cond = aux env cond e in
if Logic_utils.isLogicPointerType t.term_type then
env,
Logic_const.term
(TLval (TMem t, TNoOffset))
(Logic_typing.type_of_pointed t.term_type),
cond
else
Aorai_option.abort "Cannot dereference term %a" Printer.pp_term t
| PArrget(e1,e2) ->
let env, t1, cond = aux env cond e1 in
let env, t2, cond = aux env cond e2 in
let t =
if Logic_utils.isLogicPointerType t1.term_type
&& Logic_typing.is_integral_type t2.term_type
then
Logic_const.term
(TBinOp (PlusPI,t1,t2))
(Logic_typing.type_of_pointed t1.term_type)
else if Logic_utils.isLogicPointerType t2.term_type
&& Logic_typing.is_integral_type t1.term_type
then
Logic_const.term
(TBinOp (PlusPI,t2,t1))
(Logic_typing.type_of_pointed t2.term_type)
else if Logic_utils.isLogicArrayType t1.term_type
&& Logic_typing.is_integral_type t2.term_type
then
(match t1.term_node with
| TStartOf lv | TLval lv ->
Logic_const.term
(TLval
(Logic_const.addTermOffsetLval
(TIndex (t2, TNoOffset)) lv))
(Logic_typing.type_of_array_elem t1.term_type)
| _ ->
Aorai_option.fatal
"Unsupported operation: %a[%a]"
Printer.pp_term t1 Printer.pp_term t2)
else if Logic_utils.isLogicArrayType t2.term_type
&& Logic_typing.is_integral_type t1.term_type
then
(match t2.term_node with
| TStartOf lv | TLval lv ->
Logic_const.term
(TLval
(Logic_const.addTermOffsetLval (TIndex (t1, TNoOffset)) lv))
(Logic_typing.type_of_array_elem t2.term_type)
| _ ->
Aorai_option.fatal
"Unsupported operation: %a[%a]"
Printer.pp_term t1 Printer.pp_term t2)
else
Aorai_option.abort
"Subscripted value is neither array nor pointer: %a[%a]"
Printer.pp_term t1 Printer.pp_term t2
in
env, t, cond
| PField(e,s) ->
let env, t, cond = aux env cond e in
(match t.term_node with
| TLval lv ->
let off, ty = LTyping.type_of_field loc s t.term_type in
let lv = Logic_const.addTermOffsetLval off lv in
env, Logic_const.term (TLval lv) ty, cond
| _ ->
Aorai_option.fatal
"Unsupported operation: %a.%s" Printer.pp_term t s)
| PArrow(e,s) ->
let env, t, cond = aux env cond e in
if Logic_utils.isLogicPointerType t.term_type then begin
let off, ty =
LTyping.type_of_field loc s
(Logic_typing.type_of_pointed t.term_type)
in
let lv = Logic_const.addTermOffsetLval off (TMem t,TNoOffset) in
env, Logic_const.term (TLval lv) ty, cond
end else
Aorai_option.abort "base term is not a pointer in %a -> %s"
Printer.pp_term t s
in
aux env TTrue e
let type_cond needs_pebble metaenv env tr cond =
let current = if needs_pebble then Some tr.stop else None in
let loc = Cil_datatype.Location.unknown in
let rec aux pos env =
function
| PRel(rel,e1,e2) ->
let env, e1, c1 = type_expr metaenv env ~tr ?current e1 in
let env, e2, c2 = type_expr metaenv env ~tr ?current e2 in
let rt = LTyping.conditional_conversion loc (Some rel) e1 e2 in
let e1 = LTyping.mk_cast e1 rt in
let e2 = LTyping.mk_cast e2 rt in
let call_cond = if pos then tand c1 c2 else tor (tnot c1) (tnot c2) in
let rel = TRel(Logic_typing.type_rel rel,e1,e2) in
let cond = if pos then tand call_cond rel else tor call_cond rel in
env, cond
| PTrue -> env, TTrue
| PFalse -> env, TFalse
| POr(c1,c2) ->
let env1, c1 = aux pos env c1 in
let env2, c2 = aux pos env c2 in
let env, c = merge_current_event env1 env2 c1 c2 in
env, c
| PAnd(c1,c2) ->
let env, c1 = aux pos env c1 in
let env, c2 = aux pos env c2 in
env, TAnd (c1,c2)
| PNot c ->
let env, c = aux (not pos) env c in
env, TNot c
| PCall (s,b) ->
let kf =
try Globals.Functions.find_by_name s
with Not_found -> Aorai_option.abort "No such function: %s" s
in
let b =
Option.map
(fun b ->
let bhvs = Annotations.behaviors kf in
try List.find (fun x -> x.b_name = b) bhvs
with Not_found ->
Aorai_option.abort "Function %a has no behavior named %s"
Kernel_function.pretty kf b)
b
in
if pos then
let env, c = add_current_event
(ECall (kf, Cil_datatype.Varinfo.Hashtbl.create 3, tr)) env
(TCall (kf,b))
in
env, c
else
env, TCall (kf,b)
| PReturn s ->
let kf =
try
Globals.Functions.find_by_name s
with Not_found -> Aorai_option.abort "No such function %s" s
in
if pos then
let env,c = add_current_event (EReturn kf) env (TReturn kf) in
env, c
else
env, TReturn kf
in
aux true (ENone::env) cond
module Reject_state =
State_builder.Option_ref(Aorai_state)
(struct
let name = "Data_for_aorai.Reject_state"
let dependencies = [ Aorai_option.Ya.self]
end)
let get_reject_state () =
let create () = new_state "aorai_reject" in
Reject_state.memo create
let is_reject_state state =
match Reject_state.get_option () with
None -> false
| Some state' -> Aorai_state.equal state state'
let has_reject_state () =
match Reject_state.get_option () with None -> false | Some _ -> true
let add_if_needed states st =
if List.for_all (fun x -> not (Aorai_state.equal x st)) states
then st::states
else states
let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end seq =
let dkey = typing_dkey in
let loc = Cil_datatype.Location.unknown in
match seq with
| [] ->
(env, [], [], curr_end, curr_end)
| elt :: seq ->
let is_single_trans =
match elt.min_rep, elt.max_rep with
| Some min, Some max -> is_cst_one min && is_cst_one max
| None, _ | _, None -> false
in
let is_opt =
match elt.min_rep with
| Some min -> is_cst_zero min
| None-> true
in
let might_be_zero =
is_opt ||
(match Option.get elt.min_rep with PCst _ -> false | _ -> true)
in
let at_most_one =
is_opt &&
match elt.max_rep with
| None -> false
| Some max -> is_cst_one max
in
let has_loop = not at_most_one && not is_single_trans in
let needs_counter =
match elt.min_rep, elt.max_rep with
| None, None -> false
| Some min, None -> not (is_cst_zero min || is_cst_one min)
| None, Some max -> not (is_cst_one max)
| Some min, Some max ->
not (is_cst_zero min || is_cst_one min) || not (is_cst_one max)
in
let fixed_number_of_loop =
match elt.min_rep, elt.max_rep with
| _, None -> false
| None, Some max -> not (is_cst_zero max)
| Some min, Some max -> is_same_expression min max
in
let my_end =
match seq with
[] when not (curr_end.nums = tr.stop.nums)
|| is_single_trans || at_most_one -> curr_end
| _ -> new_intermediate_state ()
in
Aorai_option.debug ~dkey "Examining single elt:@\n%s -> %s:@[%a@]"
curr_start.name my_end.name Pretty_automaton.Parsed.print_seq_elt elt;
let guard_exit_loop env current counter =
if is_opt then TTrue
else
let e = Option.get elt.min_rep in
let _,e,_ = type_expr metaenv env ?current e in
TRel(Cil_types.Rle,e,counter)
in
let guard_loop env current counter =
match elt.max_rep with
| None ->
let i = Cil.max_signed_number (Cil.bitsSizeOf Cil_const.intType) in
let e = Logic_const.tint ~loc i in
TRel(Cil_types.Rlt, counter, e)
| Some e ->
let _,e,_ = type_expr metaenv env ?current e in
Max_value_counter.replace counter e;
TRel(Cil_types.Rlt, counter, e)
in
let env,inner_states, inner_trans, inner_start, inner_end =
match elt.condition with
| None ->
assert (elt.nested <> []);
type_seq
default_state tr metaenv env needs_pebble curr_start my_end elt.nested
| Some cond ->
let seq_start =
match elt.nested with
[] -> my_end
| _ -> new_intermediate_state ()
in
let trans_start = new_trans curr_start seq_start (Normal TTrue) []
in
let inner_env, cond =
type_cond needs_pebble metaenv env trans_start cond
in
let (env,states, seq_transitions, seq_end) =
match elt.nested with
| [] -> inner_env, [], [], my_end
| _ ->
let intermediate = new_intermediate_state () in
let (env, states, transitions, _, seq_end) =
type_seq
default_state tr metaenv
inner_env needs_pebble seq_start intermediate elt.nested
in env, states, transitions, seq_end
in
let states = add_if_needed states curr_start in
let transitions = trans_start :: seq_transitions in
(match trans_start.cross with
| Normal conds ->
trans_start.cross <- Normal (tand cond conds)
| Epsilon _ ->
Aorai_option.fatal
"Transition guard translated as epsilon transition");
let states = add_if_needed states seq_start in
(match env with
| [] | (ENone | ECall _) :: _ ->
(env, states, transitions, curr_start, seq_end)
| EReturn kf1 :: ECall (kf2,_,_) :: tl
when Kernel_function.equal kf1 kf2 ->
tl, states, transitions, curr_start, seq_end
| (EReturn _ | ECOR _ ) :: _ ->
(env, states, transitions, curr_start, seq_end)
| EMulti :: env_tmp ->
env_tmp, states, transitions, curr_start, seq_end)
in
let loop_end = if has_loop then new_intermediate_state () else inner_end
in
let (_,oth_states,oth_trans,oth_start,_) =
type_seq default_state tr metaenv env needs_pebble loop_end curr_end seq
in
let trans = inner_trans @ oth_trans in
let states = List.fold_left add_if_needed oth_states inner_states in
let auto = (inner_states,inner_trans) in
if at_most_one then begin
let opt = new_trans curr_start oth_start (Epsilon TTrue) [] in
env, states, opt::trans, curr_start, curr_end
end
else if has_loop then begin
let counter =
let ty = if needs_pebble then
Cil_types.TArray (Cil_const.intType,None,[])
else Cil_const.intType
in
lazy (
let
vi = Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_counter") ty
in
add_aux_variable vi;
vi
)
in
let make_counter st =
let vi = Lazy.force counter in
let base = TVar (Cil.cvar_to_lvar vi), TNoOffset in
if needs_pebble then
let (_,idx) = memo_multi_state st in
Logic_const.addTermOffsetLval
(TIndex (Logic_const.tvar idx,TNoOffset)) base
else base
in
let make_counter_term st =
Logic_const.term (TLval (make_counter st)) (Ctype Cil_const.intType)
in
Aorai_option.debug ~dkey "Inner start is %s; Inner end is %s"
inner_start.name inner_end.name;
let treat_state (states, oth_trans) st =
let trans = Path_analysis.get_transitions_of_state st auto in
if st.nums = inner_start.nums then begin
let loop_trans =
if has_loop then begin
List.fold_left
(fun acc tr ->
let init_actions =
if needs_counter then
Counter_init (make_counter tr.stop) :: tr.actions
else tr.actions
in
let init_trans =
new_trans st tr.stop tr.cross init_actions
in
Aorai_option.debug ~dkey "New init trans %a"
print_eps_trans init_trans;
if at_most_one then init_trans :: acc
else begin
let st =
if needs_pebble then Some curr_start else None
in
let loop_cond =
if needs_counter then
guard_loop env st
(make_counter_term curr_start)
else TTrue
in
let loop_actions =
if needs_counter then
let counter = make_counter curr_start in
Counter_incr counter :: tr.actions
else tr.actions
in
let loop_cross =
match tr.cross with
| Normal cond -> Normal (tand loop_cond cond)
| Epsilon cond -> Epsilon (tand loop_cond cond)
in
let loop_trans =
new_trans inner_end tr.stop loop_cross loop_actions
in
Aorai_option.debug ~dkey "New loop trans %a"
print_eps_trans loop_trans;
init_trans :: loop_trans :: acc
end)
oth_trans trans
end else oth_trans
in
let trans =
if might_be_zero then begin
let zero_cond =
if is_opt then TTrue
else
let current =
if needs_pebble then Some curr_start else None
in
let _,t,_ =
type_expr metaenv env ?current (Option.get elt.min_rep)
in
TRel (Cil_types.Req, t, Logic_const.tinteger ~loc 0)
in
let no_seq = new_trans st oth_start (Epsilon zero_cond) [] in
no_seq :: loop_trans
end else loop_trans
in
states, trans
end
else if st.nums = inner_end.nums then begin
let st =
if needs_pebble then Some curr_end else None
in
let min_cond =
if needs_counter then
guard_exit_loop env st (make_counter_term curr_end)
else TTrue
in
let min_cond = Epsilon min_cond in
let exit_trans = new_trans inner_end oth_start min_cond [] in
Aorai_option.debug ~dkey "New exit trans %a"
print_eps_trans exit_trans;
let trans = exit_trans :: trans @ oth_trans in
states, trans
end else begin
if fixed_number_of_loop || default_state then
states, trans @ oth_trans
else begin
let cond =
List.fold_left
(fun acc tr ->
match tr.cross with
| Normal cond | Epsilon cond ->
let cond = change_bound_var tr.stop st cond in
tor acc cond)
TFalse trans
in
let (cond,_) = Logic_simplification.simplifyCond cond in
let cond = tnot cond in
(match cond with
TFalse -> states, trans @ oth_trans
| _ ->
let reject = get_reject_state () in
let states = add_if_needed states reject in
let trans = new_trans st reject (Normal cond) [] :: trans
in states, trans @ oth_trans
)
end
end
in
let states, trans =
List.fold_left treat_state
(states, oth_trans)
inner_states
in
env, states, trans, curr_start, curr_end
end else
env, states, trans, curr_start, curr_end
let type_action metaenv env = function
| Metavar_assign (s, e) ->
let vi = find_metavar s metaenv in
let _, e, _ = type_expr metaenv env e in
Copy_value ((TVar (Cil.cvar_to_lvar vi), TNoOffset), e)
let single_path (states,transitions as auto) tr =
Aorai_option.Deterministic.get () ||
(let init = Path_analysis.get_init_states auto in
match init with
| [ st ] ->
let auto = (states,
List.filter (fun x -> x.numt <> tr.numt) transitions)
in
Path_analysis.at_most_one_path auto st tr.start
| _ -> false)
let find_otherwise_trans auto st =
let trans = Path_analysis.get_transitions_of_state st auto in
try let tr = List.find (fun x -> x.cross = Otherwise) trans in Some tr.stop
with Not_found -> None
let type_trans auto metaenv env tr =
let dkey = typing_dkey in
let needs_pebble = not (single_path auto tr) in
let has_siblings =
match Path_analysis.get_transitions_of_state tr.start auto with
| [] -> Aorai_option.fatal "Ill-formed automaton"
| [ _ ] -> false
| _::_::_ -> true
in
Aorai_option.debug ~dkey
"Analyzing transition %s -> %s: %a (needs pebble: %B)"
tr.start.name tr.stop.name
Pretty_automaton.Parsed.print_guard
tr.cross needs_pebble;
match tr.cross with
| Seq seq ->
let default_state = find_otherwise_trans auto tr.start in
let has_default_state = Option.is_some default_state in
let env,states, transitions,_,_ =
type_seq has_default_state tr metaenv env needs_pebble tr.start tr.stop seq
in
let meta_actions = List.map (type_action metaenv env) tr.actions in
let add_meta_actions t =
if Aorai_state.equal t.stop tr.stop then
{ t with actions = t.actions @ meta_actions }
else
t
in
let transitions = List.map add_meta_actions transitions in
let transitions =
if List.exists (fun st -> st.multi_state <> None) states then begin
let start = tr.start in
let count =
Cil.makeGlobalVar
~ghost:true
(get_fresh ("aorai_cnt_" ^ start.name)) Cil_const.intType
in
add_aux_variable count;
let transitions =
List.map
(fun trans ->
match trans.cross with
| Epsilon _ -> trans
| Normal _ ->
let (dest,d_aux) = memo_multi_state tr.stop in
let actions =
if tr.start.nums <> start.nums then begin
let src,s_aux = memo_multi_state tr.start in
Pebble_move(dest,d_aux,src,s_aux) :: trans.actions
end else begin
let v = Cil.cvar_to_lvar count in
let incr = Counter_incr (TVar v, TNoOffset) in
let init = Pebble_init (dest, d_aux, v) in
init::incr::trans.actions
end
in
{ trans with actions })
transitions
in
transitions
end else
transitions
in
let needs_default =
has_siblings &&
match transitions with
| [] | [ _ ] -> false
| _::_::_ -> true
in
Aorai_option.debug ~dkey "Resulting transitions:@\n%a"
(Pretty_utils.pp_list ~sep:"@\n"
(fun fmt tr -> Format.fprintf fmt "%a"
print_eps_trans tr))
transitions;
states, transitions, needs_default
| Otherwise -> [],[], false
let add_reject_trans auto intermediate_states =
let treat_one_state (states, trans) st =
let my_trans = Path_analysis.get_transitions_of_state st auto in
let reject_state = get_reject_state () in
let states = add_if_needed states reject_state in
let cond =
List.fold_left
(fun acc tr ->
let cond = change_bound_var tr.stop st tr.cross in
tor cond acc)
TFalse my_trans
in
let cond = fst (Logic_simplification.simplifyCond (tnot cond)) in
match cond with
TFalse -> states,trans
| _ ->
Aorai_option.debug ~dkey:typing_dkey
"Adding default transition %s -> %s: %a"
st.name reject_state.name Pretty_automaton.Typed.print_condition cond;
states, new_trans st reject_state cond [] :: trans
in
List.fold_left treat_one_state auto intermediate_states
let propagate_epsilon_transitions (states, _ as auto) =
let dkey = typing_dkey in
let rec transitive_closure start conds actions known_states curr =
let known_states = curr :: known_states in
let trans = Path_analysis.get_transitions_of_state curr auto in
List.fold_left
(fun acc tr ->
match tr.cross with
| Epsilon cond ->
Aorai_option.debug ~dkey
"Treating epsilon trans %s -> %s" curr.name tr.stop.name;
if List.exists (fun st -> st.nums = tr.stop.nums) known_states
then acc
else
transitive_closure
start (tand cond conds) (tr.actions @ actions)
known_states tr.stop @ acc
| Normal cond ->
Aorai_option.debug ~dkey
"Adding transition %s -> %s from epsilon trans"
start.name tr.stop.name;
let tr =
new_trans start tr.stop (tand cond conds) (tr.actions @ actions)
in
tr :: acc)
[] trans
in
let treat_one_state acc st =
acc @ transitive_closure st TTrue [] [] st
in
let trans = List.fold_left treat_one_state [] states in
(states, trans)
let add_default_trans (states, transitions as auto) otherwise =
let dkey = typing_dkey in
let add_one_trans acc tr =
let st = tr.start in
let my_trans = Path_analysis.get_transitions_of_state st auto in
Aorai_option.debug ~dkey "Considering new otherwise transition: %s -> %s"
st.name tr.stop.name;
let cond =
List.fold_left
(fun acc c ->
let cond = c.cross in
Aorai_option.debug ~dkey "considering trans %s -> %s: %a"
c.start.name c.stop.name Pretty_automaton.Typed.print_condition cond;
let neg = tnot cond in
Aorai_option.debug ~dkey "negation: %a"
Pretty_automaton.Typed.print_condition neg;
Aorai_option.debug ~dkey "acc: %a"
Pretty_automaton.Typed.print_condition acc;
let res = tand acc (tnot cond) in
Aorai_option.debug ~dkey "partial result: %a"
Pretty_automaton.Typed.print_condition res;
res)
TTrue
my_trans
in
Aorai_option.debug ~dkey "resulting transition: %a"
Pretty_automaton.Typed.print_condition cond;
let cond,_ = Logic_simplification.simplifyCond cond in
let new_trans = new_trans st tr.stop cond [] in
new_trans::acc
in
let transitions = List.fold_left add_one_trans transitions otherwise in
states, transitions
let type_cond_auto auto =
let dkey = typing_dkey in
let original_auto = auto in
let otherwise = List.filter (fun t -> t.cross = Otherwise) auto.trans in
let add_if_needed acc st =
if List.memq st acc then acc else st::acc
in
let type_trans (states,transitions,add_reject) tr =
let (intermediate_states, trans, needs_reject) =
type_trans (auto.states,auto.trans) auto.metavariables [] tr
in
Aorai_option.debug ~dkey
"Considering parsed transition %s -> %s" tr.start.name tr.stop.name;
Aorai_option.debug ~dkey
"Resulting transitions:@\n%a@\nEnd of transitions"
(Pretty_utils.pp_list ~sep:"@\n" print_eps_trans) trans;
let add_reject =
if needs_reject then
(List.filter
(fun x -> not (Aorai_state.equal tr.start x ||
Aorai_state.equal tr.stop x))
intermediate_states) @ add_reject
else add_reject
in
(List.fold_left add_if_needed states intermediate_states,
transitions @ trans,
add_reject)
in
let (states, trans, add_reject) =
List.fold_left type_trans (auto.states,[],[]) auto.trans
in
let auto = propagate_epsilon_transitions (states, trans) in
let auto = add_reject_trans auto add_reject in
let (states, transitions as auto) = add_default_trans auto otherwise in
let states, trans =
match Reject_state.get_option () with
| Some state ->
(states, new_trans state state TTrue [] :: transitions)
| None -> auto
in
let auto = { original_auto with states ; trans } in
if Aorai_option.is_debug_key_enabled typing_dkey then
Pretty_automaton.Typed.output_dot_automata auto "aorai_debug_typed.dot";
let (_,trans) =
List.fold_left
(fun (i,l as acc) t ->
let cond = fst (Logic_simplification.simplifyCond t.cross)
in match cond with
TFalse -> acc
| _ -> (i+1,{ t with cross = cond; numt = i } :: l))
(0,[]) trans
in
let states =
if Aorai_option.Deterministic.get () then
add_if_needed states (get_reject_state())
else states
in
let _, states =
List.fold_left
(fun (i,l as acc) s ->
if
is_reject_state s ||
List.exists
(fun t -> t.start.nums = s.nums || t.stop.nums = s.nums)
trans
then begin
s.nums <- i;
(i+1, s :: l)
end else acc)
(0,[]) states
in
{ original_auto with states = List.rev states; trans = List.rev trans }
let checkMetavariableCompatibility auto =
let is_extended_trans trans =
match trans.cross with
| Otherwise -> false
| Seq [ elt ] ->
elt.nested <> [] || not (is_single elt)
| Seq _ -> true
in
let has_metavariables = not (Datatype.String.Map.is_empty auto.metavariables)
and deterministic = Aorai_option.Deterministic.get ()
and uses_extended_guards = List.exists is_extended_trans auto.trans in
if has_metavariables && (not deterministic || uses_extended_guards) then
Aorai_option.abort
"The use of metavariables is incompatible with non-deterministic \
automata, such as automata using extended transitions."
let check_observables auto =
match auto.observables with
| None -> ()
| Some set ->
let is_relevant name =
try
let kf = Globals.Functions.find_by_name name in
if not (Kernel_function.is_definition kf) then
Aorai_option.warning
"Function %a is observable by the automaton but is not defined \
in the C code. It will be ignored in the instrumentation"
Printer.pp_varname (Kernel_function.get_name kf)
with Not_found ->
Aorai_option.abort "Observable %s doesn't match any function" name
in
let rec check = function
| TAnd (c1,c2) | TOr (c1,c2) -> check c1; check c2
| TNot (c) -> check c
| TRel _ | TTrue | TFalse -> ()
| TCall (kf,_) | TReturn kf ->
let name = Kernel_function.get_name kf in
if not (Datatype.String.Set.mem name set) then
Aorai_option.abort "Function %s is not observable" name
in
Datatype.String.Set.iter is_relevant set;
List.iter (fun tr -> check tr.cross) auto.trans
(** Stores the buchi automaton and its variables and
functions as it is returned by the parsing *)
let setAutomata auto =
checkMetavariableCompatibility auto;
let auto = type_cond_auto auto in
Automaton.set (Some auto);
check_states "typed automaton";
check_observables auto;
if Aorai_option.is_debug_key_enabled typing_dkey then
Pretty_automaton.Typed.output_dot_automata auto "aorai_debug_reduced.dot";
if (Array.length !cond_of_parametrizedTransitions) <
(getNumberOfTransitions ())
then
cond_of_parametrizedTransitions :=
Array.make (getNumberOfTransitions ()) [[]] ;
Aorai_metavariables.checkInitialization auto ;
Aorai_metavariables.checkSingleAssignment auto
let getState num =
List.find (fun st -> st.nums = num) (getAutomata ()).states
let getStateName num = (getState num).name
let getTransition num =
List.find (fun trans -> trans.numt = num) (getAutomata ()).trans
(** Initializes some tables according to data from Cil AST. *)
let setCData () =
let (f_decl,f_def) =
Globals.Functions.fold
(fun f (lf_decl,lf_def) ->
match f.fundec with
| Definition _ -> (lf_decl, f :: lf_def)
| Declaration _ -> (f :: lf_decl, lf_def))
([],[])
in
defined_functions := f_def;
ignored_functions := f_decl
(** Return true if and only if the given string fname denotes an ignored function. *)
let isIgnoredFunction kf =
List.exists (Kernel_function.equal kf) !ignored_functions
let isDeclaredObservable kf =
let auto = getAutomata () in
let fname = Kernel_function.get_name kf in
match auto.observables with
| None -> true
| Some set ->
Datatype.String.Set.mem fname set
let isObservableFunction kf =
not (isIgnoredFunction kf) && isDeclaredObservable kf
(** Return the list of all function name observed in the C file, except ignored functions. *)
let getObservablesFunctions () =
List.filter isDeclaredObservable !defined_functions
(** Return the list of names of observable but ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
let getIgnoredFunctions () =
List.filter isDeclaredObservable !ignored_functions
module Aux_varinfos =
State_builder.Hashtbl(Datatype.String.Hashtbl)(Cil_datatype.Varinfo)
(struct
let name = "Data_for_aorai.Aux_varinfos"
let dependencies =
[ Ast.self; Aorai_option.Ya.self; Aorai_option.Deterministic.self ]
let size = 13
end)
let () = Ast.add_linked_state Aux_varinfos.self
module StringPair =
Datatype.Pair_with_collections
(Datatype.String)(Datatype.String)
(struct let module_name = "Data_for_aorai.StringPair" end)
module Paraminfos =
State_builder.Hashtbl(StringPair.Hashtbl)(Cil_datatype.Varinfo)
(struct
let name = "Data_for_aorai.Paraminfos"
let dependencies =
[ Ast.self; Aorai_option.Ya.self; Aorai_option.Deterministic.self ]
let size = 13
end)
let set_varinfo = Aux_varinfos.add
let get_varinfo name =
try
Aux_varinfos.find name
with Not_found -> Aorai_option.fatal "Variable %s not declared" name
let get_logic_var name =
let vi = get_varinfo name in Cil.cvar_to_lvar vi
let get_varinfo_option name =
try
Some(Aux_varinfos.find name)
with
| Not_found -> None
let set_paraminfo funcname paramname vi =
Paraminfos.add (funcname,paramname) vi
let get_paraminfo funcname paramname =
try
Paraminfos.find (funcname,paramname)
with Not_found ->
Aorai_option.fatal
"Parameter '%s' not declared for function '%s'." paramname funcname
let set_returninfo funcname vi =
Paraminfos.add (funcname,"\\return") vi
let get_returninfo funcname =
try
Paraminfos.find (funcname,"\\return")
with Not_found ->
Aorai_option.fatal "Return varinfo not declared for function '%s'." funcname
type range =
| Fixed of int (** constant value *)
| Interval of int * int (** range of values *)
| Bounded of int * term (** range bounded by a logic term (depending on
program parameter).
*)
| Unbounded of int (** only the lower bound is known,
there is no upper bound *)
| Unknown (** completely unknown value. *)
module Range = Datatype.Make_with_collections
(struct
type t = range
let name = "Data_for_aorai.Range"
let rehash = Datatype.identity
let structural_descr = Structural_descr.t_abstract
let reprs =
Fixed 0 :: Interval (0,1) :: Unbounded 0 ::
List.map (fun x -> Bounded (0,x)) Cil_datatype.Term.reprs
let equal = Datatype.from_compare
let compare x y =
match x,y with
| Fixed c1, Fixed c2 -> Datatype.Int.compare c1 c2
| Fixed _, _ -> 1
| _, Fixed _ -> -1
| Interval (min1,max1), Interval(min2, max2) ->
let c1 = Datatype.Int.compare min1 min2 in
if c1 = 0 then Datatype.Int.compare max1 max2 else c1
| Interval _, _ -> 1
| _,Interval _ -> -1
| Bounded (min1,max1), Bounded(min2,max2) ->
let c1 = Datatype.Int.compare min1 min2 in
if c1 = 0 then Cil_datatype.Term.compare max1 max2 else c1
| Bounded _, _ -> 1
| _, Bounded _ -> -1
| Unbounded c1, Unbounded c2 -> Datatype.Int.compare c1 c2
| Unbounded _, _ -> 1
| _, Unbounded _ -> -1
| Unknown, Unknown -> 0
let hash = function
| Fixed c1 -> 2 * c1
| Interval(c1,c2) -> 3 * (c1 + c2)
| Bounded (c1,c2) -> 5 * (c1 + Cil_datatype.Term.hash c2)
| Unbounded c1 -> 7 * c1
| Unknown -> 11
let copy = function
| Fixed c1 ->
Fixed (Datatype.Int.copy c1)
| Interval(c1,c2) ->
Interval(Datatype.Int.copy c1, Datatype.Int.copy c2)
| Bounded(c1,c2) ->
Bounded(Datatype.Int.copy c1, Cil_datatype.Term.copy c2)
| Unbounded c1 -> Unbounded (Datatype.Int.copy c1)
| Unknown -> Unknown
let pretty fmt = function
| Fixed c1 -> Format.fprintf fmt "%d" c1
| Interval (c1,c2) ->
Format.fprintf fmt "@[<2>[%d..@;%d]@]" c1 c2
| Bounded(c1,c2) ->
Format.fprintf fmt "@[<2>[%d..@;%a]@]" c1
Cil_datatype.Term.pretty c2
| Unbounded c1 -> Format.fprintf fmt "[%d..]" c1
| Unknown -> Format.fprintf fmt "[..]"
let mem_project = Datatype.never_any_project
end)
module Intervals = Cil_datatype.Term.Map.Make(Range)
module Vals = Cil_datatype.Term.Map.Make(Intervals)
let absolute_range loc min =
let max = find_max_value loc in
match max with
| Some { term_node = TConst(Integer (t,_)) } ->
Interval(min,Integer.to_int_exn t)
| Some x ->
Bounded (min, Logic_const.term x.term_node x.term_type)
| None -> Unbounded min
let merge_range loc base r1 r2 =
match r1,r2 with
| Fixed c1, Fixed c2 when Datatype.Int.compare c1 c2 = 0 -> r1
| Fixed c1, Fixed c2 ->
let min, max =
if Datatype.Int.compare c1 c2 <= 0 then c1,c2 else c2,c1 in
Interval (min,max)
| Fixed c1, Interval(min,max) ->
let min = if Datatype.Int.compare c1 min <= 0 then c1 else min in
let max = if Datatype.Int.compare max c1 <= 0 then c1 else max in
Interval (min,max)
| Fixed c1, Bounded(min,_) ->
let min = if Datatype.Int.compare c1 min <= 0 then c1 else min in
Unbounded min
| Fixed c1, Unbounded min ->
let min = if Datatype.Int.compare c1 min <= 0 then c1 else min in
Unbounded min
| Interval(min,max), Fixed c ->
if Datatype.Int.compare c min < 0 || Datatype.Int.compare c max > 0 then
begin
let min = if Datatype.Int.compare c min < 0 then c else min in
if Cil.isLogicZero base then
absolute_range loc min
else Unbounded min
end else r1
| Interval(min1,max1), Interval(min2,max2) ->
if Datatype.Int.compare min2 min1 < 0
|| Datatype.Int.compare max2 max1 > 0 then
begin
let min =
if Datatype.Int.compare min2 min1 < 0 then min2 else min1
in
if Cil.isLogicZero base then
absolute_range loc min
else Unbounded min
end else r1
| Interval(min1,_), (Bounded(min2,_) | Unbounded min2)->
let min = if Datatype.Int.compare min1 min2 <= 0 then min1 else min2 in
Unbounded min
| Bounded(min1,max1), Bounded(min2,max2)
when Cil_datatype.Term.equal max1 max2 ->
let min =
if Datatype.Int.compare min2 min1 < 0 then min2 else min1
in
Bounded(min,max1)
| Bounded(min1,_),
(Fixed min2 | Interval(min2,_) | Bounded (min2,_) | Unbounded min2) ->
let min =
if Datatype.Int.compare min2 min1 < 0 then min2 else min1
in Unbounded min
| Unbounded min1,
(Fixed min2 | Interval(min2,_) | Bounded (min2,_) | Unbounded min2) ->
let min =
if Datatype.Int.compare min2 min1 < 0 then min2 else min1
in Unbounded min
| Unknown, _ | _, Unknown -> Unknown
let tlval lv = Logic_const.term (TLval lv) (Cil.typeOfTermLval lv)
let included_range range1 range2 =
match range1, range2 with
| Fixed c1, Fixed c2 -> Datatype.Int.equal c1 c2
| Fixed c, Interval(l,h) ->
Datatype.Int.compare l c <= 0 && Datatype.Int.compare c h <= 0
| Fixed _, Bounded _ -> false
| Fixed c1, Unbounded c2 -> Datatype.Int.compare c1 c2 >= 0
| Interval (l1,h1), Interval(l2,h2) ->
Datatype.Int.compare l1 l2 >= 0 && Datatype.Int.compare h1 h2 <= 0
| Interval (l1,_), Unbounded l2 ->
Datatype.Int.compare l1 l2 >= 0
| Interval _, (Fixed _ | Bounded _ ) -> false
| Bounded _, (Fixed _ | Interval _) -> false
| Bounded(l1,h1), Bounded(l2,h2) ->
Datatype.Int.compare l1 l2 >= 0 && Cil_datatype.Term.equal h1 h2
| Bounded(l1,_), Unbounded l2 -> Datatype.Int.compare l1 l2 <= 0
| Unbounded l1, Unbounded l2 -> Datatype.Int.compare l1 l2 <= 0
| Unbounded _, (Fixed _ | Interval _ | Bounded _) -> false
| _, Unknown -> true
| Unknown, _ -> false
let unchanged loc =
Cil_datatype.Term.Map.add loc (Fixed 0) Cil_datatype.Term.Map.empty
let merge_bindings tbl1 tbl2 =
let merge_range loc = Extlib.merge_opt (merge_range loc) in
let merge_vals loc tbl1 tbl2 =
match tbl1, tbl2 with
| None, None -> None
| Some tbl, None | None, Some tbl ->
Some
(Cil_datatype.Term.Map.merge
(merge_range loc) tbl (unchanged loc))
| Some tbl1, Some tbl2 ->
Some (Cil_datatype.Term.Map.merge (merge_range loc) tbl1 tbl2)
in
Cil_datatype.Term.Map.merge merge_vals tbl1 tbl2
module End_state =
Aorai_state.Map.Make(Datatype.Triple(Aorai_state.Set)(Aorai_state.Set)(Vals))
type end_state = End_state.t
(** The data associated to each statement: We have a mapping from each
possible state at the entrance to the function (before actual transition)
to the current state possibles, associated to any action that has occurred
on that path.
*)
module Case_state = Aorai_state.Map.Make(End_state)
type state = Case_state.t
let pretty_end_state start fmt tbl =
Aorai_state.Map.iter
(fun stop (fst,last, actions) ->
Format.fprintf fmt
"Possible path from %s to %s@\n Initial trans:@\n"
start.Automaton_ast.name stop.Automaton_ast.name;
Aorai_state.Set.iter
(fun state ->
Format.fprintf fmt " %s -> %s@\n"
start.Automaton_ast.name
state.Automaton_ast.name)
fst;
Format.fprintf fmt " Final trans:@\n";
Aorai_state.Set.iter
(fun state ->
Format.fprintf fmt " %s -> %s@\n"
state.Automaton_ast.name stop.Automaton_ast.name)
last;
Format.fprintf fmt " Related actions:@\n";
Cil_datatype.Term.Map.iter
(fun loc tbl ->
Cil_datatype.Term.Map.iter
(fun base itv ->
Format.fprintf fmt " %a <- %a + %a@\n"
Cil_datatype.Term.pretty loc
Cil_datatype.Term.pretty base
Range.pretty itv)
tbl)
actions)
tbl
let pretty_state fmt cases =
Aorai_state.Map.iter (fun start tbl -> pretty_end_state start fmt tbl) cases
let included_state tbl1 tbl2 =
try
Aorai_state.Map.iter
(fun s1 tbl1 ->
let tbl2 = Aorai_state.Map.find s1 tbl2 in
Aorai_state.Map.iter
(fun s2 (fst1, last1, tbl1) ->
let (fst2, last2, tbl2) = Aorai_state.Map.find s2 tbl2 in
if not (Aorai_state.Set.subset fst1 fst2)
|| not (Aorai_state.Set.subset last1 last2)
then raise Not_found;
Cil_datatype.Term.Map.iter
(fun base bindings1 ->
let bindings2 =
Cil_datatype.Term.Map.find base tbl2
in
Cil_datatype.Term.Map.iter
(fun loc range1 ->
let range2 = Cil_datatype.Term.Map.find loc bindings2 in
if not
(included_range range1 range2) then raise Not_found)
bindings1)
tbl1)
tbl1)
tbl1;
true
with Not_found -> false
let merge_end_state tbl1 tbl2 =
let merge_stop_state _ (fst1, last1, tbl1) (fst2, last2, tbl2) =
let fst = Aorai_state.Set.union fst1 fst2 in
let last = Aorai_state.Set.union last1 last2 in
let tbl = merge_bindings tbl1 tbl2 in
(fst, last, tbl)
in
Aorai_state.Map.merge (Extlib.merge_opt merge_stop_state) tbl1 tbl2
let merge_state tbl1 tbl2 =
let merge_state _ = merge_end_state in
Aorai_state.Map.merge (Extlib.merge_opt merge_state) tbl1 tbl2
module Pre_state =
Kernel_function.Make_Table
(Case_state)
(struct
let name = "Data_for_aorai.Pre_state"
let dependencies =
[ Ast.self; Aorai_option.Ya.self; Aorai_option.Deterministic.self ]
let size = 17
end)
let set_kf_init_state kf state =
let change old_state = merge_state old_state state in
let set _ = state in
ignore (Pre_state.memo ~change set kf)
let dataflow_dkey = Aorai_option.register_category "dataflow"
let replace_kf_init_state kf state =
Aorai_option.debug ~dkey:dataflow_dkey
"Replacing pre-state of %a:@\n @[%a@]"
Kernel_function.pretty kf pretty_state state;
Pre_state.replace kf state
let get_kf_init_state kf =
try
Pre_state.find kf
with Not_found -> Aorai_state.Map.empty
module Post_state =
Kernel_function.Make_Table
(Case_state)
(struct
let name = "Data_for_aorai.Post_state"
let dependencies =
[ Ast.self; Aorai_option.Ya.self; Aorai_option.Deterministic.self ]
let size = 17
end)
let set_kf_return_state kf state =
let change old_state = merge_state old_state state in
let set _ = state in
ignore (Post_state.memo ~change set kf)
let replace_kf_return_state = Post_state.replace
let get_kf_return_state kf =
try
Post_state.find kf
with Not_found -> Aorai_state.Map.empty
module Loop_init_state =
State_builder.Hashtbl
(Cil_datatype.Stmt.Hashtbl)
(Case_state)
(struct
let name = "Data_for_aorai.Loop_init_state"
let dependencies =
[ Ast.self; Aorai_option.Ya.self; Aorai_option.Deterministic.self ]
let size = 17
end)
let set_loop_init_state stmt state =
let change old_state = merge_state old_state state in
let set _ = state in
ignore (Loop_init_state.memo ~change set stmt)
let replace_loop_init_state = Loop_init_state.replace
let get_loop_init_state stmt =
try
Loop_init_state.find stmt
with Not_found -> Aorai_state.Map.empty
module Loop_invariant_state =
State_builder.Hashtbl
(Cil_datatype.Stmt.Hashtbl)
(Case_state)
(struct
let name = "Data_for_aorai.Loop_invariant_state"
let dependencies =
[ Ast.self; Aorai_option.Ya.self; Aorai_option.Deterministic.self ]
let size = 17
end)
let set_loop_invariant_state stmt state =
let change old_state = merge_state old_state state in
let set _ = state in
ignore (Loop_invariant_state.memo ~change set stmt)
let replace_loop_invariant_state = Loop_invariant_state.replace
let get_loop_invariant_state stmt =
try Loop_invariant_state.find stmt
with Not_found -> Aorai_state.Map.empty
let pretty_pre_state fmt =
Pre_state.iter
(fun kf state ->
Format.fprintf fmt "Function %a:@\n @[%a@]@\n"
Kernel_function.pretty kf pretty_state state)
let pretty_post_state fmt =
Post_state.iter
(fun kf state ->
Format.fprintf fmt "Function %a:@\n @[%a@]@\n"
Kernel_function.pretty kf pretty_state state)
let pretty_loop_init fmt =
Loop_init_state.iter
(fun stmt state ->
let kf = Kernel_function.find_englobing_kf stmt in
Format.fprintf fmt "Function %a, sid %d:@\n @[%a@]@\n"
Kernel_function.pretty kf stmt.sid pretty_state state)
let pretty_loop_invariant fmt =
Loop_invariant_state.iter
(fun stmt state ->
let kf = Kernel_function.find_englobing_kf stmt in
Format.fprintf fmt "Function %a, sid %d:@\n @[%a@]@\n"
Kernel_function.pretty kf stmt.sid pretty_state state)
let debug_computed_state ?(dkey=dataflow_dkey) () =
Aorai_option.debug ~dkey
"Computed state:@\nPre-states:@\n @[%t@]@\nPost-states:@\n @[%t@]@\n\
Loop init:@\n @[%t@]@\nLoop invariants:@\n @[%t@]"
pretty_pre_state pretty_post_state pretty_loop_init pretty_loop_invariant
let removeUnusedTransitionsAndStates () =
let auto = getAutomata () in
let treat_one_state state map set =
Aorai_state.Map.fold
(fun state (fst, last, _) set ->
Aorai_state.Set.add state
(Aorai_state.Set.union last
(Aorai_state.Set.union fst set)))
map
(Aorai_state.Set.add state set)
in
let reached _ state set = Aorai_state.Map.fold treat_one_state state set in
let init = Path_analysis.get_init_states (getGraph ()) in
let reached_states = Pre_state.fold reached (Aorai_state.Set.of_list init) in
let reached_states = Post_state.fold reached reached_states in
let reached_states = Loop_init_state.fold reached reached_states in
let reached_states = Loop_invariant_state.fold reached reached_states in
if Aorai_state.Set.is_empty reached_states then
raise Empty_automaton;
let reached_states =
if Aorai_option.Deterministic.get() then
Aorai_state.Set.add (get_reject_state()) reached_states
else reached_states
in
let state_list =
List.sort
(fun x y -> Datatype.String.compare x.Automaton_ast.name y.Automaton_ast.name)
(Aorai_state.Set.elements reached_states)
in
let (_, translate_table) =
List.fold_left
(fun (i,map) x ->
let map = Aorai_state.Map.add x { x with nums = i } map in (i+1,map))
(0,Aorai_state.Map.empty) state_list
in
let new_state s = Aorai_state.Map.find s translate_table in
let (_, trans_list) =
List.fold_left
(fun (i,list as acc) trans ->
try
let new_start = new_state trans.start in
let new_stop = new_state trans.stop in
(i+1,
{ trans with start = new_start; stop = new_stop; numt = i } :: list)
with Not_found -> acc)
(0,[]) auto.trans
in
let state_list = List.map new_state state_list in
Reject_state.may
(fun reject_state ->
try
let new_reject = Aorai_state.Map.find reject_state translate_table in
Reject_state.set new_reject
with Not_found -> Reject_state.clear ());
Automaton.set (Some { auto with states =state_list; trans = trans_list });
check_states "reduced automaton";
let rewrite_state state =
let rewrite_set set =
Aorai_state.Set.fold
(fun s set -> Aorai_state.Set.add (new_state s) set)
set Aorai_state.Set.empty
in
let rewrite_bindings (fst_states, last_states, bindings) =
(rewrite_set fst_states, rewrite_set last_states, bindings)
in
let rewrite_curr_state s bindings acc =
let new_s = new_state s in
let bindings = rewrite_bindings bindings in
Aorai_state.Map.add new_s bindings acc
in
let rewrite_one_state s map acc =
let new_s = new_state s in
let new_map =
Aorai_state.Map.fold rewrite_curr_state map Aorai_state.Map.empty
in
Aorai_state.Map.add new_s new_map acc
in
Aorai_state.Map.fold rewrite_one_state state Aorai_state.Map.empty
in
Pre_state.iter (fun kf state -> Pre_state.replace kf (rewrite_state state));
Post_state.iter (fun kf state -> Post_state.replace kf (rewrite_state state));
Loop_init_state.iter
(fun s state -> Loop_init_state.replace s (rewrite_state state));
Loop_invariant_state.iter
(fun s state -> Loop_invariant_state.replace s (rewrite_state state))
let func_to_op_func f = "op_"^f
let used_enuminfo = Hashtbl.create 2
let set_usedinfo name einfo =
Hashtbl.add used_enuminfo name einfo
let get_usedinfo name =
try Hashtbl.find used_enuminfo name
with Not_found -> Aorai_option.fatal "Incomplete enum information."
let get_cenum_option name =
let opnamed = func_to_op_func name in
Hashtbl.fold
(fun _ ei value ->
match value with
| Some(_) as r -> r
| None ->
let rec search = function
| {einame = n} as ei ::_ when n=name -> Some(CEnum ei)
| {einame = n} as ei ::_ when n=opnamed -> Some(CEnum ei)
| _::l -> search l
| [] -> None
in
search ei.eitems
)
used_enuminfo
None
let func_enum_type () =
try TEnum(Hashtbl.find used_enuminfo listOp,[])
with Not_found ->
Aorai_option.fatal
"Enum type indicating current function (%s) is unknown" listOp
let status_enum_type () =
try TEnum(Hashtbl.find used_enuminfo listStatus,[])
with Not_found ->
Aorai_option.fatal
"Enum type indicating current event (%s) is unknown" listStatus
let func_to_cenum func =
try
let ei = Hashtbl.find used_enuminfo listOp in
let name = func_to_op_func func in
let rec search = function
| {einame = n} as ei ::_ when n=name -> CEnum ei
| _::l -> search l
| [] ->
Aorai_option.fatal
"Operation '%s' not found in operations enumeration" name
in
search ei.eitems
with Not_found -> Aorai_option.fatal "Operation not found"
let op_status_to_cenum status =
try
let ei = Hashtbl.find used_enuminfo listStatus in
let name = if status = Automaton_ast.Call then callStatus else termStatus in
let rec search = function
| {einame=n} as ei ::_ when n=name -> CEnum ei
| _::l -> search l
| [] -> Aorai_option.fatal "Status not found"
in
search ei.eitems
with Not_found -> Aorai_option.fatal "Status not found"