File: gsoc-ideas.html

package info (click to toggle)
checker-framework-java 3.0.1%2Bds2-3
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 22,736 kB
  • sloc: java: 145,286; xml: 785; sh: 456; makefile: 401; perl: 26
file content (2084 lines) | stat: -rw-r--r-- 84,752 bytes parent folder | download
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
<!DOCTYPE html>
<html>
<head>
  <title>Checker Framework organization: GSoC ideas 2019</title>
  <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <link rel="icon" type="image/png" href=
  "../logo/Checkmark/CFCheckmark_favicon.png">
</head>
<body>

<img src="../logo/Logo/CFLogo.png" alt="Checker Framework logo" />

<h1>GSoC ideas 2019</h1> <!-- omit from toc -->

<p>Contents:</p>
<!-- start toc.  do not edit; run html-update-toc instead -->
<ul>
  <li><a href="#introduction">Introduction</a>
    <ul>
      <li><a href="#get-started">How to get started: do a case study</a></li>
      <li><a href="#ask-questions">How to get help and ask questions</a></li>
      <li><a href="#apply">How to apply</a></li>
    </ul></li>
  <li><a href="#case-studies">Case studies</a>
    <ul>
      <li><a href="#library-annotations">Library annotations</a>
        <ul>
          <li><a href="#choose-a-library">Choosing a library to annotate</a></li>
        </ul></li>
      <li><a href="#case-study-signature">Signature strings</a></li>
      <li><a href="#case-study-android-support">Android support annotations</a></li>
      <li><a href="#case-study-signedness">Signed and unsigned numbers</a></li>
      <li><a href="#optional-case-study">Java's Optional class</a></li>
      <li><a href="#case-study-nullness">Null pointer exceptions</a>
        <ul>
          <li><a href="#case-study-nullness-guava">Guava library</a></li>
          <li><a href="#case-study-nullness-bazel">Bazel tool</a></li>
          <li><a href="#case-study-nullness-bcel">BCEL library</a></li>
        </ul></li>
      <li><a href="#index-errors">Improving error messages</a></li>
      <li><a href="#sound-by-default">Sound checking by default</a></li>
      <li><a href="#compare-other-tools">Comparison to other tools</a></li>
    </ul></li>
  <li><a href="#new-type-systems">New type systems</a>
    <ul>
      <li><a href="#non-empty-checker">Non-Empty Checker for precise handling of Queue.peek() and poll()</a></li>
      <li><a href="#Make_programs_deterministic">Make programs deterministic</a></li>
      <li><a href="#custom-tainting-checking">Custom tainting checking</a></li>
      <li><a href="#Bounded-size_strings">Bounded-size strings</a></li>
      <li><a href="#overflow">Overflow checking</a></li>
      <li><a href="#lock-ordering">Lock ordering</a></li>
      <li><a href="#index-checker-mutable-length">Index checking for mutable length data structures</a></li>
      <li><a href="#nullness-bug-detector">Nullness bug detector</a></li>
      <li><a href="#typestate">Stateful type systems</a></li>
      <li><a href="#your-own-new-type-system">Invent your own new type system</a></li>
    </ul></li>
  <li><a href="#cf-other">Type system enhancements and tools</a>
    <ul>
      <li><a href="#annotated-jdk">JDK annotations</a></li>
      <li><a href="#flow-expression-parser">Flow expression parser</a></li>
      <li><a href="#asm">Upgrade to a newer version of ASM</a></li>
      <li><a href="#analysis_diffs">Tool for analysis diffs</a></li>
      <li><a href="#Whole-program_type_inference">Whole-program type inference</a></li>
      <li><a href="#dataflow">Dataflow enhancements</a></li>
      <li><a href="#Purity_analysis">Purity (side effect) analysis</a></li>
      <li><a href="#javadoc">Javadoc support</a></li>
      <li><a href="#performance">Performance improvements</a></li>
      <li><a href="#run-time-checking">Run-time checking</a></li>
      <li><a href="#ide-support">IDE and build system support</a></li>
      <li><a href="#exhaustive-testing">Model checking of a type system</a></li>
    </ul></li>
</ul>
<!-- end toc -->

<h1 id="introduction">Introduction</h1>

<p>
  The <a href="https://checkerframework.org/">Checker Framework</a> is an
  innovative programming tool that helps you prevent bugs at development
  time, before they escape to production.
</p>

<p>
  Java's type system prevents some bugs, such as <code>int count =
  "hello";</code>.  However, it does not prevent other bugs, such as null
  pointer dereferences, concurrency errors, disclosure of private
  information, incorrect internationalization, out-of-bounds indices, and
  so forth.  <em>Pluggable type-checking</em> replaces a
  programming language's built-in type system with a more powerful,
  expressive one.
</p>

<p>
  We have created around 20
  <a href="https://checkerframework.org/manual/#introduction">new type
  systems</a>, and other people have created
  <a href="https://checkerframework.org/manual/#third-party-checkers">many
  more</a>.
  The more powerful type system is not just a
  bug-finding tool:  it is a verification tool that gives a guarantee that
  no errors (of certain types) exist in your program.  Even though it is
  powerful, it is easy to use.  It follows the standard typing rules
  that programmers already know, and it fits into their workflow.
</p>

<p>
  The Checker Framework is popular:  it is used daily at Google, Amazon,
  Uber, on Wall Street, and in other companies from big to small.  It is
  attractive to programmers who care about their craft and the quality of
  their code.  The Checker Framework is the motivation for Java's type
  annotations feature.  It has received multiple awards.
  <!-- at conferences such as JavaOne. -->
  With this widespread use, there is a need for people to help with the
  project:  everything from bug fixes, to new features, to case studies, to
  integration with other tools.  We welcome your contribution!
</p>

<p>
  Why should you join this project?  It's popular, so you will have an
  impact.  It makes code more robust and secure, which is a socially
  important purpose.  Past GSOC students have had great success.
  (David Lazar became a graduate student at MIT; multiple students
  have published papers in scientific conferences.)  You will
  get to scratch your own itch by creating tools that solve problems that
  frustrate you.  And, we have a lot of fun on this project!
</p>

<p>
  <b>Prerequisites:</b> You should be very comfortable with the Java
  programming language and its type system.  You should know how a type
  system helps you and where it can hinder you.  You should be willing to
  dive into and understand a moderately-sized codebase.
  You should understand fundamental object-oriented programming concepts,
  such as
  <a href="https://en.wikipedia.org/wiki/Liskov_substitution_principle">behavioral
  subtyping</a>:  subtyping theory
  permits argument types to change contravariantly (even though Java forbids it
  for reasons related to overloading), whereas return types may change
  <a href="https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29">covariantly</a>
  both in theory and in Java.
</p>


<p>
<b>Potential projects:</b>
Most of this document lists potential summer projects.  The projects are
grouped roughly from easiest to most challenging.  Many of the projects are
applicable beyond Google Summer of Code.
<!--
You can find more potential projects in the
<a href="https://github.com/typetools/checker-framework/issues">issue
  tracker</a>.
-->
</p>



<h2 id="get-started">How to get started: do a case study</h2>

<p>
  To <b>get started</b>, first do a case study of using the Checker
  Framework.  Do this before submitting your proposal.
</p>
<ol>
  <li>
    <a href="https://checkerframework.org/manual/#installation">Install</a>
    the Checker Framework.
  <li>
    Choose a library or program to type-check.
    <br/>
    This should be an already-existing
    program; it should not be newly-written code, nor a set of tiny
    benchmarks that aim to expose corner cases.
    <!-- (Corner cases are great to
    discover, but they are only worth addressing if they come up in real code.)
    -->
    The library or program should be under active maintenance; don't choose one
    that has not had a commit in several years.
    You will find the case study easier if you are already familiar with
    the program, or if it is written in good style.
    <br/>
    If you need ideas of what program to annotate, you could
    see <a href="#library-annotations">library annotations</a> below.
    Don't choose part of the JDK as your first case study.
  <li>
    Choose one type system, from
    among <a href="https://checkerframework.org/manual/#introduction">those
    distributed with the Checker Framework</a>, that is appropriate for the
    program.
  <li>
    Annotate the program, based on its documentation.
    <br/>
    Please do <em>not</em> make changes unrelated to annotating the
    program, such as inserting/removing whitespace or sorting
    the <code>import</code> statements.  Doing so bloats the size of the
    diffs and makes it hard to understand the essential changes.
  <li>
    Run the type-checker.  If it issues
    warnings, <a href="https://checkerframework.org/manual/#handling-warnings">correct them</a>.
    This might require adding more annotations,
    fixing bugs in the program, or suppressing warnings.
    Be sure that the program's test suite continues to pass.
    Repeat until
    the type-checker passes on the program.
    <ul>
      <li>Don't add an <code>if</code> statement that always succeeds, just
        to suppress a warning.  Convince yourself that both branches can
        execute, or else don't add the <code>if</code> statement.
      <li>If you add a <code>@SuppressWarnings</code> annotation,
        <a href="https://checkerframework.org/manual/#suppresswarnings-best-practices-justification">explain
        why</a> the checker warning is a false positive and you are certain
        the code is safe.
    </ul>
  <li>
    Share it with us so that
    we can evaluate it and give you feedback.  (If the code compiles
    without type-checking warnings, and you didn't
    use <code>@SuppressWarnings</code>, then the annotations are correct,
    your program is correct, and you don't need feedback.  Congratulations!
    You can try a more significant case study.)

    <p>
    Share the case study as soon
    as you finish it or as soon as you have a question that is not answered
    in the <a href="https://checkerframework.org/manual/">manual</a>;
    don't wait until you submit your proposal.
    The subject line should be descriptive (not just "Case study", but
    "Nullness case study of Apache Commons Exec library").
    You should give us access to
    <ul>
      <li>the original (unannotated) version of the program,
      <li>the annotated version of the program, and
      <li>the exact command that runs the type-checker from the command
        line.
    </ul>
    The best way to give all this information is a pointer to your GitHub
    fork of the library.  In your fork, the master branch will be unchanged
    from upstream.  You will create a new branch that contains the
    annotated version.  The only differences between the two branches
    should be related to the annotations you wrote.  Building the annotated
    branch should run the type-checker.
    It is helpful to create a pull request from the annotated to the
    unannotated branch in your fork; you won't merge this pull request, but
    it enables you and others to view and comment on your changes.
</ol>

<p>
Once you have done this work on a small program such as from your
coursework, you can repeat the process with an open-source program or library.
</p>

<p>
The primary result of your case study is that you will discover bugs in the
subject program, or you will verify that it has no bugs (of some particular
type).  If you found bugs in open-source code, report them to the program's
maintainer, and let us know when they are resolved.  If you verified
open-source code to be correct, that is great too; let us know and point us
at the fully-annotated, verified program.
</p>

<p>
Another outcome of your case study is that you may discover bugs, limitations,
or usability problems in the Checker Framework.  Please
<a href="https://checkerframework.org/manual/#reporting-bugs">report them</a>.
We'll try to fix them, or they might give you inspiration for
improvements you would like to make to the Checker Framework this summer.
You can also try to fix them yourself and submit a
<a href="https://github.com/typetools/checker-framework/pulls">pull
  request</a>, but that is <em>not</em> a requirement.
You may discuss your ideas with us by sending mail
to <a href="https://groups.google.com/forum/#!forum/checker-framework-gsoc">checker-framework-gsoc@googlegroups.com</a>.
</p>

<p>
  Note that we do <em>not</em> recommend that you run many different checkers on
  small, artificial programs.  Instead, run one checker on a more
  substantial program.
  </p>

<p>
Why should you start with a case study, instead of diving right into fixing
bugs, designing a new type system, or making other changes to the Checker
Framework?
Before you can contribute to any project, you must
understand the tool from a user point of view, including its strengths,
weaknesses, and how to use it.  Therefore, you need to complete a
substantive case study first.
</p>


<h2 id="ask-questions">How to get help and ask questions</h2>

<p>
We are very happy to answer your questions, and we are eager to interact
with you.
Before you ask a question, read these &ldquo;getting started&rdquo;
instructions (that is, this file) and search in the
<a href="https://checkerframework.org/manual/">Checker Framework manual</a>
for the answer.
Don't send us a message
that says nothing but &ldquo;please guide me&rdquo;
or &ldquo;tell me how to fix this bug&rdquo;.  Such a message shows
that you haven't thought about the problem and haven't tried to solve it
yourself.  It also shows that you have not read this document, and we don't
want to work with people who cannot read instructions!
</p>

<p>
Your questions should show that you will be a productive colleague over the
summer:  tell us what you have tried, tell us what went wrong or
where you got stuck, and ask a concrete technical question that will
help you get past your problem.  If you can do that, then definitely ask
your question, because we don't want you to be stuck or frustrated.
</p>

<p>
Whenever you send email (related to GSoC or not),
please use standard email etiquette, such as:  avoid all-caps; use a
descriptive subject line; don't put multiple different topics in a single
email message; start a new thread with a new subject line
when you change the topic; don't clutter discussions with irrelevant
remarks; don't use screenshots (unless there is a problem with a GUI), but
instead cut-and-paste the code into your message; if you are making a guess, clearly indicate that it is a guess and
your grounds for it.  If you violate these basic rules, you will
look unprofessional, and we don't want you to give a bad impression.  Bug
reports should be
<a href="https://checkerframework.org/manual/#reporting-bugs">complete</a>
and should usually be
<a href="https://checkerframework.org/manual/#reporting-bugs">reported</a>
to the issue tracker.
</p>

<p>
Some GSOC projects have a requirement to fix an issue in the issue tracker.
We do not, because it is unproductive.
Don't try to start fixing issues before you
understand the Checker Framework from the user point of view, which will
not happen until you have completed a case study on an open-source program.
</p>



<h2 id="apply">How to apply</h2>

<p>
  To <b>apply</b>, you will submit a single PDF through the Google Summer
  of Code website.  This PDF should contain two main parts.  We suggest
  that you number the parts and subparts to ensure that you don't forget anything, and
  that we don't overlook anything in your application.  You might find it
  easiest to create multiple PDFs for the different parts, then concatenate
  them before uploading to the website, but how you create your proposal is
  entirely up to you.
</p>

<ol>
  <li>The proposal itself:  what project you want to work on during the
    summer.  You might propose to do a project listed on this webpage, or
    you might propose a different project.

      <p>The proposal should have a descriptive title, both in the PDF and
      in the GSoC submission system.  Don't use a title like "Checker
      Proposal" or "Proposal for GSoC".
      Don't distract from content with gratuitous graphics.

    <p>If you want to create a new type system (whether one proposed on
    this webpage or one of your own devising), then your proposal should be
    the type system's user manual.  You don't have to integrate it in the Checker
    Framework repository (in other words, use any word processor or text
    editor you want to create a PDF file you will submit), but you should describe
    your proposed checker's <a href="https://checkerframework.org/manual/#creating-parts-of-a-checker">parts</a>
    in precise English or simple formalisms and you should follow the
    suggested <a href="https://checkerframework.org/manual/#creating-documenting-a-checker">structure</a>.

    <p>List the tasks or subparts that are required to complete your
    project.  This will help you discover a part that you had forgotten.
    We do not require a detailed timeline, because at this point, you don't
    know enough to create one.
    </p>

    <p>Never literally cut-and-paste text that was not written by you, because
    that would be plagiarism.  If you quote from text written by someone
    else, give proper credit.</p>

    <p>
    If you want to do exactly what is already listed on this page, then
    just say that (but be specific about which one!), and it will not hurt
    your chances of being selected.  However, you might have specific ideas
    about extensions, about details that are not mentioned on this webpage,
    about implementation strategies, and so forth.  If you want to do a
    case study, say what program you will do your case study on.  Don't
    submit a proposal that is just a rearrangement of text that already
    appears on this page or in the Checker Framework manual, because it does
    not help us to assess your likelihood of being successful.  (You can
    propose an idea that's here, but show what progress you have made.)
    </p>
  </li>

  <li>Your qualifications.  Please convince us that you
    are likely to be successful in your proposed summer project.

    <ol>
      <li>A URL that points to a code sample.
        Don't write any new code, but provide code you wrote in the
        past, such as for a class assignment
        or a project you have worked on outside class.
        It does not need to have anything to do with
        the Checker Framework project.  It should be your own personal work.
        The purpose is to assess your programming skills so we can assign you
        to an appropriate project.
        A common problem is to submit undocumented code; we expect every
        programmer to write documentation when working on the Checker
        Framework.
        Don't put a lot of different files in Google Drive and share that
        URL; it's better to upload a single <code>.zip</code> file or
        provide a GitHub URL.
      </li>
      <li>
        What you have done to prepare yourself
        for working with the Checker Framework during the summer.
        You may wish to structure this as a list.
    Examples of items in the list include:
    <ul>
      <li>A URL for code you have annotated as a case study.  Please indicate the
    original unannotated code, the annotated code, and the exact command to
    run the type-checker from the command line.  Ensure that the GSoC
    mentors can compile your code.
    (It is acceptable to use the same code, or different code, for this
      item and the code sample above.)
      </li>
      <li>URLs for bugs or pull requests that you have filed.</li>
      <li>Information about other projects you have done, or classes you
        have taken, that prepare you for your proposed summer task.  This
        is optional, because it might already appear in your resume.</li>
    </ul>
  </li>
  <li>A resume.
    A <a href="https://en.wikipedia.org/wiki/R%C3%A9sum%C3%A9">resume</a>
    contains a brief description of your skills and your job or project
    experience.  It will often list classes you have taken so far and your
    GPA.  It should not be longer than one page.</li>
  <li>An unofficial transcript or grade report (don't spend
    money for an official one).</li>
  </ol>
  </li>
</ol>

<p>
The <b>best way</b> to impress us is by doing a thoughtful job in the case
study.  The case study is even more important than the proposal text,
because it shows us your abilities.
The case study may result in you submitting issues against the issue tracker of the
program you are annotating or of the Checker Framework.
Pull requests against our GitHub project are a plus but are not required:
good submitted bugs are just as valuable as bug fixes!
You can also make a good impression by correctly answering questions from
other students on the GSOC mailing list.
</p>

<p>
Get feedback!  Feel free to <a href="#ask-questions">ask questions</a>
to make your application more
competitive.  We want you to succeed.  Historically, students who start
early and get feedback are most successful.  You can submit a draft
proposal via the Google Summer of Code website, and we will review it.  We
do <em>not</em> receive any notification when you submit a draft
proposal, so if you want feedback, please tell us that.
Also, we can only see draft proposals; we cannot see final proposals until
after the application deadline has passed.
</p>


<h1 id="case-studies">Case studies</h1>

<p>
These projects take an existing type-checker, apply it to a
codebase (you can choose your favorite one, or you can ask for
suggestions), and determine whether the type system is easy to use and
whether it is effective in revealing or preventing defects.
Case studies are our most important source of new ideas and improvements:
our most useful features have arisen as a result of an observation made
during a case study.  Many people have started out &ldquo;just&rdquo; doing a case
study but have ended up making deep, fundamental contributions and even
publishing scientific papers about their discoveries.
</p>

<p>
You should do a small case study during the application process (or maybe a
large one, depending on your ambition).  A case study is the best way to
learn about the Checker Framework, determine whether you would enjoy
joining the project during the summer, and show your aptitude so that you
will be chosen for the summer.
</p>

<p>
A set of large case studies is one possible summer task.  The most common
choice is case studies of a recently-written type system, to determine its
usability.  Another choice is to annotate popular libraries for an existing
type system, to make it more usable.
</p>

<p>
Here are a few suggestions, but a case study of any type system
distributed with the Checker Framework is of value.
</p>


<h2 id="library-annotations">Library annotations</h2>

<p>
When type-checking a method call, the Checker Framework uses the method
declaration's annotations.
This means that in order to type-check code that uses a library, the
Checker Framework needs an annotated version of the library.
</p>

<p>
The Checker Framework comes with a
few <a href="https://search.maven.org/search?q=annotatedlib">annotated
libraries</a>.  Increasing this number will make the Checker Framework even
more useful, and easier to use.
</p>

<p>
After you have <a href="#choose-a-library">chosen a library</a>,
fork the library's source code, adjust
its <a href="https://checkerframework.org/manual/#external-tools">build
system</a> to run the Checker Framework, and add annotations to it until
the type-checker issues no warnings.
</p>

<p>
Before you get started, be sure to read
<a href="https://checkerframework.org/manual/#get-started-with-legacy-code">How
to get started annotating legacy code</a>.  More generally, read the
<a href="https://checkerframework.org/manual/#how-to-read-this-manual">relevant
sections of the Checker Framework manual</a>.
</p>


<h3 id="choose-a-library">Choosing a library to annotate</h3>

<p>
There are several ways to <b>choose a library</b> to annotate:
</p>
<ul>
  <li>
    Choose a <a href="https://docs.google.com/spreadsheets/d/17x_jKkGquEFq7LBQhS9HGXiG7iIl2AlXoPGfB6N5_bw">popular
      Java library</a>.
  </li>
  <li>
    Choose a library that you need annotations for.  That is, choose a
    library that is used by a program (or another library) that you have
    tried to annotate.
  </li>
  <li>
    Choose one of the suggestions below.
  </li>
</ul>

<p>
  Whatever library you choose, you will need to deeply understand its
  source code.  You will find it easier to work with a library that is
  well-designed and well-documented.
</p>

<p>
  You should choose a library that is
  not <a href="https://github.com/typetools/checker-framework/tree/master/checker/lib">already
    annotated</a>.  There are two exceptions to this.
</p>
<ul>
  <li>
    A library might be annotated for one type system, but you add
    annotations for a different type system.  One advantage of this is that
    the library's build system is already set up to run the Checker
    Framework.  You can tell which type systems a library is annotated for
    by examining its source code.
  </li>
  <li>
    A library might be annotated, but the annotations have not been
    verified by running the type-checker on the library source code.  You
    would verify that the annotations in the library are correct.
  </li>
</ul>


<h2 id="case-study-signature">Signature strings</h2>

<p>
Show that the <a href="https://asm.ow2.org/">ASM library</a>, or
the <a href="https://commons.apache.org/proper/commons-bcel/">BCEL
library</a>, properly handles signature strings (or find bugs in them).
</p>

<p>
  To get started:
</p>

<ul>
  <li>Fork https://github.com/typetools/commons-bcel.git</li>
  <li>Clone your new fork</li>
  <li><code>git checkout typecheck-signature</code></li>
  <li>mvn verify</li>
</ul>

<p>
   Some challenging aspects of this case study are:
</p>
<ul>
  <li>
    The Signature String Checker needs to be enhanced to precisely handle code like
        <code>someString.replace('.', '/')</code>
      which converts from <code>@ClassGetName</code> to <code>@FieldDescriptor</code>.  It also converts from <code>@FullyQualifiedName</code> to <code>@BinaryName</code>, but only for non-anonymous classes.
      The full rules for that, and for other calls such
      as <code>someString.replace('/', '.')</code>, need to be worked out
        and implemented.
  </li>
  <li>
    ASM and BCEL define their own new signature string formats (!), which need to be
    defined.  If they are not defined, then warnings need to be suppressed
    and the guarantee is weaker.  (Defining them could be a second part of
    the case study.)
  </li>
  <li>
    Some of ASM's and BCEL's documentation is incorrect, and in other cases the
    string format is not defined.
  </li>
  <li>
    The BCEL codebase has been partially annotated, but we are not sure the
    annotations are 100% correct.
  </li>
</ul>


<h2 id="case-study-android-support">Android support annotations</h2>

<p>
Android uses its own annotations that are similar to some in the Checker
Framework.  Examples include the
<a href="https://tips.seebrock3r.me/annotations-to-support-your-contracts-609ff259d5df">Android
  Studio support annotations</a>,
  including <code>@NonNull</code>, <code>@IntRange</code>, <code>@IntDef</code>,
  and others.
</p>

<p>
The goal of this project is to implement support for these annotations.
That is probably as simple as creating aliased annotations
by calling method <code>addAliasedAnnotation()</code>
in <a href="https://checkerframework.org/api/org/checkerframework/framework/type/AnnotatedTypeFactory.html">AnnotatedTypeFactory</a>.
</p>

<p>
  Then, do a case study to show the utility (or not) of
  pluggable type-checking, by comparison with how Android Studio currently
  checks the annotations.
</p>


<h2 id="case-study-signedness">Signed and unsigned numbers</h2>

<p>
  The <a href="https://checkerframework.org/manual/#signedness-checker">Signedness
  Checker</a> ensures that you do not misuse unsigned values, such as
  by mixing signed and unsigned values in a computation or by performing a
  meaningless operation.
</p>

<p>
  Perform a case study of the Signedness Checker, in order to detect errors
  or guarantee that code is correct.
</p>

<p>
  You will need to find Java projects that use unsigned arithmetic, or
  that <em>could</em> use unsigned arithmetic but do not.
  When doing the case study, it is important to type-check both a library and
  a client that uses it.  Type-checking the client will ensure that the
  library annotations are accurate.
</p>

<p>
  Here are some libraries that you could annotate (some are already
  annotated for you).  You would need to find client code that uses the
  signedness-sensitive routines.
</p>
<ul>
  <li>In the JDK's <code>Integer</code>
  and <code>Long</code>, these include
   <code>compareUnsigned</code>,
   <code>divideUnsigned</code>,
   <code>parseUnsignedInt</code>,
   <code>remainderUnsigned</code>, and
   <code>toUnsignedLong</code>.
   <br/>
   Classes like <code>DataInputStream</code>, <code>ObjectInputStream</code>,
   and <code>RandomAccessFile</code> have <code>readUnsignedByte</code>.
   <br/>
   <code>Arrays</code> has <code>compareUnsigned</code>.
  </li>
  <li>
    In Guava, see
  its <a href="https://github.com/google/guava/wiki/PrimitivesExplained#unsigned-support">unsigned
  support</a>, such
  as <a href="https://google.github.io/guava/releases/snapshot-jre/api/docs/com/google/common/primitives/UnsignedBytes.html">UnsignedBytes</a>,
  <a href="https://google.github.io/guava/releases/snapshot-jre/api/docs/com/google/common/primitives/UnsignedLong.html">UnsignedLong</a>,
  <a href="https://google.github.io/guava/releases/snapshot-jre/api/docs/com/google/common/primitives/UnsignedLongs.html">UnsignedLongs</a>,
  etc.
  </li>
  <li>The <a href="https://github.com/jOOQ/jOOU">jOOU</a> library consists of support for unsigned
      integers.</li>
</ul>

<p>
  Here are some other possible case studies; you would need to determine
  whether this code is the library, the client, or both:
</p>
<ul>
  <li><a href="https://github.com/bcgit/bc-java">bc-java</a>.  This is
  over 200 KLOC of code.</li>

  <!-- Not a good choice because this is just example code, not an actively-maintained project.
  <li>Project
  Nayuki: <a href="https://www.nayuki.io/page/forcing-a-files-crc-to-any-value">CRC</a>, <a href="https://www.nayuki.io/page/notepadcrypt-format-decryptor-java">crypt</a>, <a href="https://www.nayuki.io/page/native-hash-functions-for-java">hash</a>.</li>
  -->

  <!-- Not a good choice because it is not under active development:
  <li><a href="https://bytonic.de/html/jake2.html">Jake2</a></li>
   -->
</ul>

<p>
  Your case studies will show the need for enhancements to the Signedness
  Checker.  For example, the Signedness Checker does not currently handle
  boxed integers and BigInteger; these haven't yet come up in case studies
  but could be worthwhile enhancements.  There may also be the need to
  write more annotations for libraries such as the JDK.
</p>


<h2 id="optional-case-study">Java's Optional class</h2>

<p>
Java 8 introduced the
<a href="https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/util/Optional.html"><code>Optional</code></a>
class, a container that is either empty or contains a non-null value.
It is intended to solve the problem of null
pointer exceptions.  However, <code>Optional</code> has <a href="https://homes.cs.washington.edu/~mernst/advice/nothing-is-better-than-optional.html">its own problems</a>.
</p>

<p>
Because of <code>Optional</code>'s problems, many commentators advise programmers to use
<code>Optional</code> only in limited ways.
</p>

<p>
The goal of this project is to evaluate
the <a href="https://checkerframework.org/manual/#optional-checker">Optional
    Checker</a>, which warns programmers who
have misused <code>Optional</code>.
Another goal is to extend the Optional Checker to make it more precise or
to detect other mis-uses of Optional.
</p>


<h2 id="case-study-nullness">Null pointer exceptions</h2>

<p>
These are just some suggestions; many other libraries need annotations.
</p>


<h3 id="case-study-nullness-guava">Guava library</h3>

<p>
  Guava is already partially annotated with nullness annotations &mdash; in
  part by Guava's developers, and in part by the Checker Framework team.
  However, Guava does not yet type-check without errors.  Doing so could
  find more errors (the Checker Framework has found nullness and indexing
  errors in Guava in the past) and would be a good case study to learn the
  limitations of the Nullness Checker.
</p>


<h3 id="case-study-nullness-bazel">Bazel tool</h3>

<!-- John Field of Google is interested in this. -->

<p>
This project is related to the
<a href="https://bazel.build/">Bazel</a> build system, and was
proposed by its development manager.
</p>

<p>
The Bazel codebase contains 1586 occurrences of the <code>@Nullable</code>
annotation.  This annotation indicates that a variable may hold a null
value.  This is valuable documentation and helps programmers avoid null
pointer exceptions that would crash Bazel.  However, these annotations are
not checked by any tool.  Instead, programmers have to do their best to
obey the <code>@Nullable</code> specifications in the source code.  This is
a lost opportunity, since documentation is most useful when it is
automatically processed and verified.  (For several years, Google tried
using <a href="http://findbugs.sourceforge.net/">FindBugs</a>, but they
eventually abandoned it:  its analysis is too weak, suffering too many
false positives and false negatives.)
</p>

<p>
Despite the programmers' best efforts, null pointer exceptions do still
creep into the code, impacting users.  The Bazel developers would like to
prevent these.  They want a guarantee, at compile time, that no null
pointer exceptions will occur at run time.
</p>

<p>
Such a tool already exists:  the
<a href="https://checkerframework.org/manual/#nullness-checker">Nullness
Checker</a> of the <a href="https://checkerframework.org/">Checker
Framework</a>.  It runs as a compiler plug-in, and it issues a warning at
every possible null pointer dereference.  If it issues no warnings, the
code is guaranteed not to throw a <code>NullPointerException</code> at run time.
</p>

<p>
The goal of this project is to do a large-scale case study of the Nullness
Checker on Bazel.  The main goal is to understand how the Nullness Checker
can be used on a large-scale industrial codebase.  How many lurking bugs
does it find?  What
<a href="https://checkerframework.org/releases/1.9.13/api/org/checkerframework/checker/nullness/qual/Nullable.html"><code>@Nullable</code></a>
annotations are missing from the codebase because the developers failed to
write them?  What are its limitations, such as code patterns that it cannot
recognize as safe?  (You might create new analyses and incorporating them
into the Nullness Checker, or you might just reporting bugs to the Nullness
Checker developers for fixing.)  What burdens does it place on users?  Is
the cost-benefit tradeoff worth the effort &mdash; that is, should Google
adopt this tool more broadly?  How should it be improved?  Are the most
needed improvements in the precision of the analysis, or in the UI of the
tooling?
</p>


<h3 id="case-study-nullness-bcel">BCEL library</h3>

<p>
  Annotate the BCEL library to express its contracts with respect to nullness.
  Show that the BCEL library has no null pointer exceptions (or find bugs
  in BCEL).  There are
  already <a href="https://github.com/apache/commons-bcel/compare/trunk...typetools:trunk?expand=1">some
  annotations</a> in BCEL, but they have not been verified as correct by
  running the Nullness Checker on BCEL.  (Currently, those annotations are
  trusted when type-checking clients of BCEL.)
</p>

<p>
  To get started:
</p>

<ul>
  <li>Fork https://github.com/typetools/commons-bcel.git</li>
  <li>Clone your new fork</li>
  <li><code>git checkout typecheck-nullness</code></li>
  <li>mvn verify</li>
</ul>

<p>
   Some challenging aspects of this case study are:
</p>

<ul>
  <li>
    There is some poor design that needs to be resolved in discussions with
    the BCEL maintainers.  For example, consider the <code>copy()</code>
    method.  Some implementations of <code>copy()</code> return null, but
    are not documented to do so.  In addition, some implementations
    of <code>copy()</code> catch and ignore exceptions.  I think it would
    be nicest to change the methods to never return null, but to throw an
    exception instead.  (This is no more burdensome to users, who currently
    have to check for null.)  Alternately, the methods could all be
    documented to return null.
  </li>
</ul>


<h2 id="index-errors">Improving error messages</h2>

<p>
Compiler writers have come to realize that clarity of error
messages is as important as the speed of the executable
(<a href="http://www.brettbecker.com/wp-content/uploads/2016/06/Becker-Effective-2016-SIGCSE.pdf">1</a>, <a href="https://www.mville.edu/sites/default/files/p53-munson_1.pdf">2</a>,
<a href="http://se.ethz.ch/~meyer/publications/teaching/compiler-errors.pdf">3</a>
<a href="http://static.barik.net/barik/publications/icse2017/PID4655707.pdf">4</a>).  This is especially true when the language or type system has rich features.
</p>

<p>
The goal of this project is to improve a compiler's error messages.  One
example (not the only possible one) is the Checker Framework.  Here are
some distinct challenges:
</p>
<ul>
  <li>
    Some type errors can be more concisely or clearly expressed than the
    standard "found type A, expected type B" message.
  </li>
  <li>
    Some types are complex.  The error message could explain them, or link
    to the manual, or give suggested fixes.
  </li>
  <li>
    Compiler messages currently show
    the <a href="https://checkerframework.org/manual/#effective-qualifier">effective
    type</a>, which may be different than what the user wrote due to
    defaulting, inference, and syntactic sugar.  For example, a user-written
    <code>@IndexFor("a")</code> annotation is syntactic sugar for
    <code>@NonNegative @LTLengthOf("a")</code>, and those types are
    the ones that currently appear in error messages.
    It would be good to show simpler types or ones that the user wrote.
  </li>
  <li>
    Some checkers combine multiple cooperating type systems;
    the <a href="https://checkerframework.org/manual/#nullness-checker">Nullness
    Checker</a> and
    the <a href="https://checkerframework.org/manual/#index-checker">Index
    Checker</a> are examples.  If there is a problem with a variable's
    lower bound type, then its upper bound type should not be shown in the
    error message.  This will make the message shorter and more specific,
    and avoid distracting the user with irrelevant information.
  </li>
  <li>
    When a checker has multiple type systems, a type error or the lack of one may depend on facts from multiple type systems, and this should be expressed to the user.
  </li>
</ul>

<p>
It would be reasonable to start by improving the
<a href="https://checkerframework.org/manual/#index-checker">Index
  Checker</a>'s error messages, which frequently stymie users.  Then,
  generalize the results to other type systems.
</p>

<h2 id="sound-by-default">Sound checking by default</h2>

<p>
By default, the Checker Framework is
<a href="https://checkerframework.org/manual/#unsound-by-default">unsound
in several circumstances</a>.  &ldquo;Unsound&rdquo; means that the Checker Framework
may report no warning even though the program can misbehave at run time.
</p>

<p>
The reason that the Checker Framework is unsound is that we believe that
enabling these checks would cause too many false positive warnings:
warnings that the Checker Framework issues because it cannot prove that the
code is safe (even though a human can see that the code is safe).  Having
too many false positive warnings would irritate users and lead them not to
use the checker at all, or would force them to simply disable those checks.
</p>

<p>
We would like to do studies of these command-line options to see whether
our guess is right.  Is it prohibitive to enable sound checking?  Or can we
think of enhancements that would let us turn on those checks that are
currently disabled by default?
</p>


<h2 id="compare-other-tools">Comparison to other tools</h2>

<p>
  Many other tools exist for prevention of programming errors, such as
  Error Prone, NullAway, FindBugs, JLint, PMD, and IDEs such as Eclipse and
  IntelliJ.  These tools
  are not as powerful as the Checker Framework (some are bug finders rather
  than verification tools, and some perform a shallower analysis), but they
  may be easier to use.
  Programmers who use these tools wonder, "Is it worth my time to switch to
  using the Checker Framework?"
</p>

<p>
  The goal of this project is to perform a head-to-head comparison of as
  many different tools as possible.  You will quantify:
</p>

<ul>
  <li>the number of annotations that need to be written</li>
  <li>the number of bugs detected</li>
  <li>the number of bugs missed</li>
  <li>the number of false positive warnings</li>
</ul>

<p>
  This project will help programmers to choose among the different tools
  &mdash; it will show when a programmer should or should not use the
  Checker Framework.
  This project will also indicate how each tool should be improved.
</p>

<p>
  One place to start would be with an old version of a program that is
  known to contain bugs.  Or, start with the latest version of the program
  and re-introduce fixed bugs.  (Either of these is more realistic than
  introducing artificial bugs into the program.)  A possibility would be to
  use the Lookup program that has been used in previous case studies.
</p>


<h1 id="new-type-systems">New type systems</h1>

<p>
The Checker Framework is shipped with <a href="https://checkerframework.org/manual/#introduction">about 20 type-checkers</a>.  Users can
<a href="https://checkerframework.org/manual/#creating-a-checker">create a
  new checker</a> of their own.  However, some users don't want to go to
that trouble.  They would like to have more type-checkers packaged with the
Checker Framework for easy use.
</p>

<p>
Each of these projects requires you to design a <a href="https://checkerframework.org/manual/#creating-a-checker">new type system</a>,
implement it, and perform case studies to demonstrate that it is both
usable and effective in finding/preventing bugs.
</p>


<h2 id="non-empty-checker">Non-Empty Checker for precise handling of Queue.peek() and poll()</h2>

<p>
The Nullness Checker issues a false positive warning for this code:
</p>

<pre>
import java.util.PriorityQueue;
import org.checkerframework.checker.nullness.qual.NonNull;

public class MyClass {
    public static void usePriorityQueue(PriorityQueue&lt;@NonNull Object&gt; active) {
        while (!(active.isEmpty())) {
            @NonNull Object queueMinPathNode = active.peek();
        }
    }
}
</pre>

<p>
The Checker Framework does not determine that <code>active.peek()</code> returns a non-null value in this context.
</p>

<p>
The contract of <code>peek()</code> is that it returns a non-null value if the queue is not empty and the queue contains no null values.
</p>

<p>
To handle this code precisely, the Nullness Checker needs to know, for each queue, whether it is empty.
This is analogous to how the Nullness Checker tracks whether a particular value is a key in a map.
</p>

<p>
It should be handled the same way:  by adding a new subchecker, called the
  Nonempty Checker, to the Nullness Checker.  Its types are:
</p>
<ul>
<li><code>@UnknownNonEmpty</code> &mdash; the queue might or might not be empty
<li><code>@NonEmpty</code> &mdash; the queue is definitely non-empty
</ul>

<p>
There is a start at this type-checker in branch <code>nonempty-checker</code>.  It:
</p>
<ul>
  <li>defines the annotations
  </li>
  <li>creates the integration into the Nullness Checker
  </li>
</ul>
<p>
However, it is not done.  (In fact, it doesn't even compile.)
For information about what needs to be done, see <a href="https://github.com/typetools/checker-framework/issues/399">issue #399</a>.
</p>

<p>
When you are done, the Nullness Checker should issue only the <code>// ::</code> diagnostics from <code>checker/tests/nullness/IsEmptyPoll.java</code> &mdash; no more and no fewer.
You can test that by running the Nullness Checker on the file, and when you are done you should delete the <code>// @skip-test</code> line so that the file is run as part of the Checker Framework test suite.
</p>


<h2 id="Make_programs_deterministic">Make programs deterministic</h2>

<p>
Programs are easier to use and debug if their output is deterministic.  For
example, it is easier to test a deterministic program, because
nondeterminism can lead to flaky tests that sometimes succeed and sometimes
fail.  As another example, it is easier for a user or programmer to compare
two deterministic executions than two nondeterministic executions.
</p>

<p>
A number of Java methods return nondeterministic results, making any
program that uses them potentially nondeterministic.  Here are a few
examples:
</p>
<dl>
<dt>iteration over <code>HashMap</code>s and <code>HashSet</code>s</dt>
<dd>solution:  sort, or iterate over <code>LinkedHashMaps</code> and <code>LinkedHashSets</code></dd>
<dt><code>File.list()</code></dt>
<dd>solution:  sort the resulting list</dd>
<dt><code>Object.toString()</code>, <code>Object.hashCode()</code></dt>
<dd>solution:  use overriding implementations</dd>
<dt><code>new Random()</code></dt>
<dd>solution:  call it with a fixed seed</dd>
<dt>time and date functions</dt>
<dd>solution:  don't make the program result depend on these</dd>
</dl>

<p>
You can find more examples of non-deterministic specifications,
and suggestions for how to avoid them, in the
<a href="https://randoop.github.io/randoop/manual/index.html#nondeterminism">Randoop
manual</a> and in the ICST 2016 paper
<a href="http://mir.cs.illinois.edu/marinov/publications/ShiETAL16NonDex.pdf">Detecting
assumptions on deterministic implementations of non-deterministic
specifications</a> by A. Shi, A. Gyori, O. Legunsen, and D. Marinov, which
presents the NonDex tool.
</p>

<p>
The NonDex tool works dynamically, which means that it cannot detect all
user-visible nondeterminism nor give a guarantee of correctness &mdash; a
guarantee that the program is deterministic from the user's point of
view.
</p>

<p>
The goal of this project is to create a tool, based on a type system, that
gives a guarantee.  The tool would report to the user all possible
nondeterminism in a program, so that the user can fix the program before it
causes problems during testing or in the field.
</p>

<p>
More concretely, this problem can be handled by creating two simple type
systems that indicate whether a given value is deterministic.
In each diagram, the supertype appears above the subtype.
</p>

<pre>
    @PossiblyNonDeterministic            @PossiblyNonDeterministicOrder
              |                                       |
        @Deterministic                       @DeterministicOrder
</pre>

<p>
The programmer would annotate routines that are expected to take
deterministic inputs.  (An example could be all printing routines.)  Then,
the type system would issue a warning whenever one of those routines is
called on a possibly non-deterministic value.
</p>

<p>
The standard library would have annotations for
</p>
<ul>
  <li>methods that return non-deterministic results</li>
  <li>methods like sort that convert nondeterministically-ordered collections into deterministically-ordered ones</li>
</ul>

<p>
You can find
a <a href="https://checkerframework.org/determinism-checker-manual/manual.html#determinism-checker">draft
manual chapter</a> that documents a possible design for a Determinism
Checker.  It differs slightly from the above proposal, for instance by
having a single type hierarchy instead of two.  That type system
is <a href="https://github.com/t-rasmud/checker-framework/tree/nondet-checker">implemented</a>,
so your best choice for this project is to do a case study of it, which
could lead to design work to improve it.
</p>


<h2 id="custom-tainting-checking">Custom tainting checking</h2>

<p>
The Checker Framework comes with
a <a href="https://checkerframework.org/manual/#tainting-checker">Tainting
  Checker</a> that is so general that it is not good for much of anything.
In order to be useful in a particular domain, a user must customize it:
</p>
<ul>
  <li>
    rename the <code>@Tainted</code> and <code>@Untainted</code> qualifiers
    to something more specific (such as <code>@Private</code>
    or <code>@PaymentDetails</code> or <code>@HtmlQuoted</code>), and
  <li>
    annotate libraries.
</ul>

<p>
The first part of this project is to make this customization easier to do
&mdash; preferably, a user does not have to change any code in the Checker
Framework, as is currently the case for the
<a href="https://checkerframework.org/manual/#subtyping-checker">Subtyping
Checker</a>.
As part of making customization easier, a user should be able to specify
multiple levels of taint &mdash; many information classification hierarchies
have more than two levels (for example, the US government separates classified
information into three categories: Confidential, Secret, and Top Secret).
</p>

<p>
The second part of this project is to provide several examples, and do case
studies showing the utility of compile-time taint checking.
</p>

<p>
  Possible examples include:
</p>
<ul>
  <li>SQL injection
  <li>OS command injection
  <li>the <code>@PrivacySource</code> and <code>@PrivacySink</code>
    annotations used by the Facebook <a href="http://fbinfer.com/">Infer
    static analyzer</a>.
  <li>information flow
  <li>many of the <a href="http://cwe.mitre.org/top25/">CWE/SANS most
  dangerous software programming errors</a> (and the "on the cusp" ones too)
  <!-- More details appear in these files:
      ~/research/games/notes/notes
      ~/prof/grants/2012-02-darpa-verigames/proposal/top25-as-types.pdf
  -->
</ul>

<p>
For some microbenchmarks, see the Juliette test suite for Java from CWE.
</p>




<h2 id="Bounded-size_strings">Bounded-size strings</h2>

<!-- John Field of Google is interested in this. -->

<p>
Windows cannot run command lines longer than 8191 characters.  Creating a
too-long command line causes failures when the program is run on Windows.
These failures are irritating when discovered during testing, and
embarrassing or worse when discovered during deployment.  The same command
line would work on Unix, which has longer command-line limits, and as a
result developers may not realize that their change to a command can cause
such a problem.
</p>

<p>
Programmers would like to enforce that they don't accidentally pass a
too-long string to the <code>exec()</code> routine.  The goal of this
project is to give a compile-time tool that provides such a guarantee.
</p>

<p>
Here are two possible solutions.
</p>

<p>
<b>Simple solution:</b>
For each array and list, determine whether its length is known at compile
time.  The routines that build a command line are only allowed to take such
constant-length lists, on the assumption that if the length is constant,
its concatenation is probably short enough.
</p>

<p>
<b>More complex solution:</b>
For each String, have a compile-time estimate of its maximum length.  Only
permit <code>exec()</code> to be called on strings whose estimate is no more than 8191.
String concatenation would return a string whose estimated size is the sum
of the maximums of its arguments, and likewise for concatenating an array
or list of strings.
</p>


<h2 id="overflow">Overflow checking</h2>

<p>
Overflow is when 32-bit arithmetic differs from ideal arithmetic.  For
example, in Java the <code>int</code> computation 2,147,483,647 + 1 yields
a negative number, -2,147,483,648.  The goal of this project is to detect
and prevent problems such as these.
</p>

<p>
One way to write this is as an extension of the Constant Value Checker,
which already keeps track of integer ranges.  It even already
<a href="https://checkerframework.org/manual/#value-checker-overflow">checks
  for overflow</a>, but it never issues a warning when it discovers
  possible overflow.  Your variant would do so.
</p>

<p>
This problem is so challenging that there has been almost no previous
research on static approaches to the problem.  (Two relevant papers are
<a href="https://www.researchgate.net/publication/221655385_IntScope_Automatically_Detecting_Integer_Overflow_Vulnerability_in_X86_Binary_Using_Symbolic_Execution">IntScope:
Automatically Detecting Integer Overflow Vulnerability in x86 Binary Using
Symbolic Execution</a> and
<a href="https://dl.acm.org/citation.cfm?id=3136872">Integer Overflow
Vulnerabilities Detection in Software Binary Code</a>.)  Researchers are
concerned that users will have to write a lot of annotations indicating the
possible ranges of variables, and that even so there will be a lot of false
positive warnings due to approximations in the conservative analysis.
For example, will every loop that contains <code>i++</code> cause a warning that <code>i</code> might overflow?
That would not be acceptable:  users would just disable the check.
</p>

<p>
You can convince yourself of the difficulty by manually analyzing programs
to see how clever the analysis has to be, or manually simulating your
proposed analysis on a selection of real-world code to learn its
weaknesses.  You might also try it
on <a href="https://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html">good
  and bad binary search code</a>.
</p>

<p>
One way to make the problem tractable is to limit its scope:  instead of
being concerned with all possible arithmetic overflow, focus on a specific
use case.
As one concrete application,
the <a href="https://checkerframework.org/manual/#index-checker">Index
Checker</a> is currently unsound in the presence of integer overflow.  If
an integer <code>i</code> is known to be <code>@Positive</code>, and 1 is
added to it, then the Index Checker believes that its type
remains <code>@Positive</code>. If <code>i</code> was
already <code>Integer.MAX_VALUE</code>, then the result is negative &mdash;
that is, the Index Checker's approximation to it is unsound.
</p>

<p>
This project involves removing this unsoundness by implementing a type system to track when an
integer value might overflow &mdash but this only matters for values that
are used as an array index.
That is, checking can be restricted to computations that involve an operand
of type <code>@IntRange</code>).
Implementing such an analysis would permit the Index Checker
to extend its guarantees even to programs that might overflow.
</p>

<p>
This analysis is important for some indexing bugs in practice.
Using the Index Checker, we found 5 bugs in Google
Guava related to overflow.  Google marked these as high priority and
fixed them immediately.  In practice, there would be a run-time exception
only for an array of size approximately <code>Integer.MAX_INT</code>.
</p>

<p>
You could write an extension of the Constant Value Checker, which already
keeps track of integer ranges and
even <a href="https://checkerframework.org/manual/#value-checker-overflow">determines
when overflow is possible</a>.  It doesn't issue a warning, but your
checker could record whether overflow was possible (this could be a
two-element type system) and then issue a warning, if the value is used as
an array index.
Other implementation strategies may be possible.
</p>

<p>
Here are some ideas for how to avoid the specific problem
of issuing a warning about potential overflow for every <code>i++</code> in
a loop (but maybe other approaches are possible):
</p>
<ul>
  <li>
    The loop checks whether <code>i == Integer.MAX_VALUE</code> before
    incrementing.  This wide-scale, disruptive code change is not
    acceptable.
  </li>
  <li>
    Make the default array size (the length of an unannotated array) be
    <code>@ArrayLenRange(0, Integer.MAX_VALUE-1)</code> rather
    than <code>@UnknownVal</code>, which is equivalent
    to <code>@ArrayLenRange(0, Integer.MAX_VALUE-1)</code>.  Now, every
    array construction requires the client to establish that the length is
    not <code>Integer.MAX_VALUE</code>.  I don't have a feel for whether
    this would be unduly burdensome to users.
  </li>
</ul>


<h2 id="lock-ordering">Lock ordering</h2>

<p>
The <a href="https://checkerframework.org/manual/#lock-checker">Lock
Checker</a> prevents race conditions by ensuring that locks are held when
they need to be.  It does not prevent deadlocks that can result from locks
being acquired in the wrong order.  This project would extend the Lock
Checker to address deadlocks, or create a new checker to do so.
</p>

<p>
Suppose that a program contains two different locks.  Suppose that one
thread tries to acquire lockA then lockB, and another thread tries to
acquire lockB then lockA, and each thread acquires its first lock.  Then
both locks will wait forever for the other lock to become available.  The
program will not make any more progress and is said to
be <a href="https://en.wikipedia.org/wiki/Deadlock">deadlocked</a>.
</p>

<p>
If all threads acquire locks in the same order &mdash; in our example, say
lockA then lockB &mdash; then deadlocks do not happen.  You will extend the
Lock Checker to verify this property.
</p>


<h2 id="index-checker-mutable-length">Index checking for mutable length data structures</h2>

<p>
The <a href="https://checkerframework.org/manual/#index-checker">Index
Checker</a> is currently restricted to fixed-size data structures.
A fixed-size data structure is one whose length cannot be changed once it is created;
examples of fixed-size data structures are arrays and Strings.
This limitation prevents the Index Checker from verifying indexing operations on mutable-size data structures,
like Lists, that have add or remove methods. Since these kind of collections are common
in practice, this is a severe limitation for the Index Checker.
</p>

<p>
The limitation is caused by the Index Checker's use of types that are dependent on the length of data structures,
like <code>@LTLengthOf("data_structure")</code>. If <code>data_structure</code>'s length could change,
then the correctness of this type might change.
</p>

<p>
A naive solution would be to invalidate these types any time a method is called on <code>data_structure</code>.
Unfortunately, aliasing makes this still unsound. Even more, a great solution to this problem would keep
the information in the type when a method like add or remove is called on <code>data_structure</code>.
A more complete solution might involve some special annotations on List that permit the information to be persisted.
</p>

<p>
This project would involve designing and implementing a solution to this problem.
</p>


<h2 id="nullness-bug-detector">Nullness bug detector</h2>

<p>
Verifying a program to be free of errors can be a daunting task.  When
starting out, a user may be more interested in
<a href="https://checkerframework.org/manual/#other-tools">bug-finding</a>
than verification.  The goal of this project is to create a nullness bug
detector that uses the powerful analysis of the Checker Framework and its
Nullness Checker, but omits some of its more confusing or expensive
features.  The goal is to create a fast, easy-to-use bug detector.  It
would enable users to start small and advance to full verification in the
future, rather than having to start out doing full verification.
</p>

<p>
This could be structured as a new NullnessLight Checker, or as a
command-line argument to the current Nullness Checker.  Here are some
differences from the real Nullness checker:
</p>
<ul>
  <li>No initialization analysis; the checker assumes that every value is
  initialized.</li>
  <li>No map key analysis; assume that, at every call to
    <code>Map.get</code>, the given key appears in the map.</li>
  <li>No invalidation of dataflow facts.  Assume all method calls are pure,
  so method calls do not invalidate dataflow facts.  Assume there is no
    aliasing, so field updates do not invalidate dataflow facts.
    </li>
  <li>Assume that boxing of primitives is <code>@Pure</code>: it returns
  the same value on every call.</li>
  <li>If the Checker Framework cannot infer a type argument, assume that
  the type argument is <code>@NonNull</code>.</li>
</ul>
<p>
  Each of these behaviors should be controlled by its own command-line
  argument, as well as being enabled in the NullnessLight Checker.
</p>

<p>
  The implementation may be relatively straightforward, since in most cases
  the behavior is just to disable some functionality of existing checkers.
</p>

<p>Tools such as FindBugs, NullAway, NullnessLight, and the Nullness
  Checker form a spectrum from easy-to-use bug detectors to sound
  verification.  NullnessLight represents a new point in the design space.
  It will be interesting to compare these checkers:
</p>

<ul>
    <li>How much easier is it to use?  For example, how many fewer
      annotations need to be written?</li>
    <li>
      How many more fewer true positives does it report &mdash; in other
      words, how many more false negatives does it suffer?
    </li>
    <li>
      How many fewer false positives does it report?
    </li>
</ul>

<p>
  Uber's <a href="https://github.com/uber/NullAway">NullAway</a> tool is also
  an implementation of this idea (that is, a fast, but incomplete and
  unsound, nullness checker).  NullAway doesn't let the user specify Java
  Generics:  it assumes that every type parameter is <code>@NonNull</code>.
  Does Uber's tool provide users a good
  introduction to the ideas that a user can use to transition to a nullness
  type system later?
</p>



<h2 id="typestate">Stateful type systems</h2>

<p>
This project is to improve support for
<a href="https://checkerframework.org/manual/#typestate-checker">typestate checking</a>
</p>

<p>
Ordinarily, a program variable has
the same type throughout its lifetime from when the variable is declared
until it goes out of scope. “Typestate”
permits the type of an object or variable to <em>change</em> in a controlled way.
Essentially, it is a combination of standard type systems with dataflow
analysis. For instance, a file object changes from unopened, to opened, to
closed; certain operations such as writing to the file are only permitted
when the file is in the opened typestate. Another way of saying this is
that <code>write</code> is permitted after <code>open</code>, but not after <code>close</code>.
Typestate
is applicable to many other types of software properties as well.
</p>

<p>
Two <a href="https://checkerframework.org/manual/">typestate checking frameworks</a>
exist for the Checker Framework.  Neither is being maintained; a new one
needs to be written.
</p>


<h2 id="your-own-new-type-system">Invent your own new type system</h2>

<p>
We also welcome your ideas for new type systems.  For example, any run-time
failure can probably be prevented at compile time with the right
analysis.  Can you come up with a way to fix your pet peeve?
</p>

<p>
It is easiest, but not required, to choose an existing type system from the
literature, since that means you can skip the design stage and go right to
implementation.
</p>

<p>
This task can be simple or very
challenging, depending on how ambitious the type system is.  Remember to
focus on what helps a software developer most!
</p>



<h1 id="cf-other">Type system enhancements and tools</h1>


<h2 id="annotated-jdk">JDK annotations</h2>

<p>
The JDK is the most important library to annotate, and the Checker
Framework ships with partial annotations for it.
These are scattered in multiple locations:  in multiple subdirectories of
<a href="https://github.com/typetools/checker-framework/tree/master/checker/jdk"><code>checker/jdk/</code></a>,
and in files <code>jdk.astub</code> under
<a href="https://github.com/typetools/checker-framework/tree/master/checker/src/org/checkerframework/checker"><code>checker/src/org/checkerframework/checker/</code></a>
</p>

<p>
The goal of this project is to put the annotations in a single place:  a
new clone of the JDK repository.  The effort can be partially annotated
&mdash; say, by using
the <a href="https://checkerframework.org/annotation-file-utilities/">Annotation
File Utilities</a> to move annotations around, or enhancing the Annotation
File Utilities if they are not up to the task) and partially done manually.
</p>


<h2 id="flow-expression-parser">Flow expression parser</h2>

<p>
A number of type annotations take, as an
argument, <a href="https://checkerframework.org/manual/#java-expressions-as-arguments">a
Java expression</a>.  The parser for these is a hack.  The goal of this
project is to replace it by calls
to <a href="https://github.com/javaparser/javaparser">JavaParser</a>.
For example, the <code>FlowExpressions.Receiver</code> class, which
represents an AST, should be replaced by the JavaParser AST.
</p>

<p>
This task
should be straightforward, since JavaParser is already used in other parts
of the Checker Framework.
</p>


<h2 id="asm">Upgrade to a newer version of ASM</h2>

<p>
  The
  <a href="https://checkerframework.org/annotation-file-utilities/">Annotation
  File Utilities</a>, or AFU, insert annotations into, and extract
  annotations from, <code>.java</code> files, <code>.class</code> files,
  and text files.  These programs were written before the
  <a href="https://asm.ow2.org/">ASM</a> bytecode library supported Java 8's
  type annotations.  Therefore, the AFU has its own custom version of ASM
  that supports type annotations.  Now that ASM 6 has been released and it
  supports type annotations, the AFU needs to be slightly changed to use
  the official ASM 6 library instead of its own custom ASM variant.
</p>

<p>
  This project is a good way to learn about <code>.class</code> files and
  Java bytecodes:  how they are stored, and how to manipulate them.
</p>


<h2 id="analysis_diffs">Tool for analysis diffs</h2>
<!--
  This project idea is duplicated at
  ~mernst/public_html/uw-only/research/potential-research-projects.html .
-->

<p>
   Many program analyses are too verbose for a person to read their entire
   output.  However, after a program change, the analysis results may
   change only slightly.  An "analysis diff" tool could show the
   difference between the analysis run on the old code and the analysis run
   on the new code.
</p>
<ul>
  <li>
    The analysis diffs may help the programmer to better understand the
    changes.
  </li>
  <li>
    Bug detection tools. such
    as <a href="http://findbugs.sourceforge.net/">FindBugs</a> or
    the <a href="https://checkerframework.org/">Checker Framework</a>, have
    extremely verbose output when first run on a program.  Programmers
    could examine and fix only the warnings about code they have changed
    (and that they are currently thinking about).
  </li>
  <li>
    Tools that always have large output, such as inference tools, could
    become manageable to users if output is shown in small doses.
  </li>
  <li>
    You can probably think of other uses.
  </li>
</ul>

<p>
  The analysis diff tool would take as input two analysis results (the
  previous and the current one).  It would output only the new parts of its
  second input.  (It could optionally output a complete diff between two
  analysis results.)
</p>

<p>
  One challenge is dealing with changed line numbers and other analysis
  output differences between runs.
</p>

<p>
It would be nice to integrate the tool with git pre-commit hooks or GitHub
pull requests, to enable either of the following functionality (for either
commits to master or for pull requests):
</p>
<ul>
  <li>
    Permit only those commits/pulls that do not add any new analysis warnings.
  </li>
  <li>
    Permit only those commits/pulls that are "clean" &mdash; the analysis
    issues no warnings for any changed line.
  </li>
</ul>

<p>
  A concrete example of an analysis diff tool
  is <a href="https://github.com/plume-lib/checklink/blob/master/checklink-persistent-errors">checklink-persistent-errors</a>;
  see the documentation at the top of the file.  That tool only works for
  one particular analysis, the W3C Link Checker.
  An analysis diff tool also appears to be built into FindBugs.
  The goal of this project is to build a general-purpose tool that is easy
  to apply to new analyses.
</p>


<h2 id="Whole-program_type_inference">Whole-program type inference</h2>

<p>
A type system is useful because it prevents certain errors.  The downside
of a type system is the effort required to write the types.  Type inference
is the process of writing the types for a program.
</p>

<p>
Type-<em>checking</em> is a modular, or local, analysis.  For example, given a
procedure in which types have been written, a type-checker can verify the
procedure's types without examining the implementation of any other
procedure.
</p>

<p>
By contrast, type <em>inference</em> is a non-local, whole-program analysis.  For
example, to determine what type should be written for a procedure's formal
parameter, it is necessary to examine the type of the argument at every
call to that procedure.  At every call, to determine the type of some argument A, it
may be necessary to know the types of the formal parameters to the
procedure that contains A, and so forth.  It is possible to resolve this
seemingly-infinite regress, but only by examining the entire program in the
worst case.
</p>

<p>
The differences between type checking and type inference means that they
are usually written in very different ways.  Type inference is usually done
by first collecting all of the constraints for the entire program, then
passing them to a specialized solver.  Writing a type inference tool is
harder.  Worst of all, it's annoying to encode all the type rules twice in
different ways:  once for the type checker and once for the type inference.
</p>

<p>
As a result, many type systems have a type checker but no type inference
tool.  This makes programmers reluctant to use these type systems, which denies
programmers the benefits of type-checking.
</p>

<p>
The goal of this project is to automatically create type inference tools
from type-checking tools, so that it is not necessary for the type system
designer to implement the type system twice in different ways.
</p>

<p>
A key insight is that the type-checker already encodes all knowledge about
what is a legal, well-typed program.  How can we exploit that for the
purpose of type inference as well as type-checking?  The idea is to
iteratively run the type-checker, multiple times, observing what types are
passed around the program and what errors occur.  Each iteration collects
more information, until there is nothing more to learn.
</p>

<p>
This approach has some disadvantages:  it is theoretically slower, and
theoretically less accurate, than a purpose-built type inference tool for
each type system.  However, it has the major advantage that it requires no
extra work to implement a type inference tool.  Furthermore, maybe it works
well enough in practice.
</p>

<p>
A prototype implementation of this idea already exists, but it needs to be
evaluated in order to discover its flaws, improve its design, and discover
how accurate it is in practice.
</p>

<p>
A valuable project all by itself would be to compare heavy-weight and
light-weight type inference this whole-program inference vs. Checker
Framework Inference vs. Julia, to understand when each one is worth using.
</p>


<h2 id="dataflow">Dataflow enhancements</h2>

<p>
The Checker
Framework's <a href="https://checkerframework.org/manual/#creating-dataflow">dataflow
    framework</a>
(<a href="https://checkerframework.org/manual/checker-framework-dataflow-manual.pdf">manual
    here</a>) implements flow-sensitive type refinement (local type
inference) and other features.  It is used in the Checker
Framework and also in <a href="http://errorprone.info/">Error Prone</a>,
<a href="https://github.com/uber/NullAway">NullAway</a>, and elsewhere.
</p>

<p>
There are a number
of <a href="https://github.com/typetools/checker-framework/issues?q=is%3Aopen+is%3Aissue+label%3ADataflow">open
issues</a> &mdash; both bugs and feature requests &mdash; related to the
dataflow framework.  The goal of this project is to address as many of
those issues as possible, which will directly improve all the tools that
use it.
</p>


<h2 id="Purity_analysis">Purity (side effect) analysis</h2>

<p>
A program analysis technique makes estimates about the current values of
expressions.  When a method call occurs, the analysis has to throw away
most of its estimates, because the method call might change any variable.
If the method is known to have no side effects, then the analysis doesn't
need to throw away its estimates, and the analysis is more precise.
</p>

<p>
For example, the Checker Framework unsoundly trusts but does not check
<a href="https://checkerframework.org/manual/#type-refinement-purity">purity annotations</a>.  This makes
the system vulnerable to programmer mistakes when writing annotations.  The
Checker Framework contains a sound checker for immutability annotations,
but it suffers too many false positive warnings and thus is not usable.  A
better checker is necessary.  It will also incorporate aspects of an escape
analysis.
</p>

<p>
Choosing an algorithm from the literature is the best choice, but there
still might be research work to do:  in the past, when implementing
algorithms from research papers, we have sometimes found that they did not
work as well as claimed, and we have had to enhance them.  One challenge is
that any technique used by pluggable type-checking to verify immutability
must be modular, but many side effect analyses require examining the whole
program.  The system should require few or no method annotations within
method bodies.  I'm not sure whether such a system already exists or we
need to design a new one.
</p>

<p>
Perhaps one of these existing side effect analyses could be used:
 https://github.com/Sable/soot/wiki/Using-Side-Effect-Attributes
 http://www2.informatik.uni-freiburg.de/~geffken/GeffkenST14.pdf
</p>

<!--
For design and implementation ideas, see:
 * $qn/notes-purity
 * ~/prof/grants/2011-09-darpa-apac/phase3-extension-proposal
-->


<h2 id="javadoc">Javadoc support</h2>

<p>
Currently, type annotations are only displayed in Javadoc if they are
explicitly written by the programmer.  However, the Checker Framework
provides flexible defaulting mechanisms, reducing the annotation overhead.
This project will integrate the Checker Framework defaulting phase with
Javadoc, showing the signatures after applying defaulting rules.
</p>

<p>
There are other type-annotation-related improvements to Javadoc that can be
explored, e.g. using JavaScript to show or hide only the type annotations
currently of interest.
</p>


<h2 id="performance">Performance improvements</h2>

<p>
  The Checker Framework runs much slower than the standard javac compiler
  &mdash; often 20 times slower!  This is not acceptable as part of a
  developer's regular process, so we need to speed up the Checker
  Framework.  This project involves determining the cause of slowness in
  the Checker Framework, and correcting those problems.
</p>

<p>
This is a good way to learn about performance tuning for Java applications.
</p>

<p>
  Some concrete tasks include:
</p>

<ul>
  <li>Profile the Checker Framework.  Run a profiler such as
  <a href="https://www.yourkit.com/java/profiler/">YourKit</a> to determine
  which parts of the Checker Framework consume the most CPU time and memory.
  </li>

  <li>Perhaps compare a profile of the Checker Framework against a profile
  of regular javac.  This probably is not necessary because the Checker
    Framework is so much slower than regular javac.
  </li>

  <li>Consider interning string values.  The Checker Framework does a fair
  amount of string manipulation, in part because it reads from resources
  such as stub files that do not produce <code>Element</code>s.  Interning
  could save time when doing comparisons.  You can verify the correctness
  of the optimization by running the
  <a href="https://checkerframework.org/manual/#interning-checker">Interning
    Checker</a> on the Checker Framework code.  Compare the run time of the
  Checker Framework before and after this optimization.
  </li>

  <li> Based on profiling results, devise other optimizations, implement
    them, and evaluate them.
  </li>
</ul>


<h2 id="run-time-checking">Run-time checking</h2>

<p>
Implement run-time checking to complement compile-time checking.  This will
let users combine the power of static checking with that of dynamic
checking.
</p>

<p>
Every type system is too strict: it rejects some programs that never go
wrong at run time. A human must insert a type loophole to make such a
program type-check.  For example, Java takes this approach with its
cast operation (and in some other places).
</p>

<p>
When doing type-checking, it is desirable to automatically insert run-time
checks at each operation that the static checker was unable to verify.
(Again, Java takes exactly this approach.)  This guards against mistakes by
the human who inserted the type loopholes.  A nice property of this
approach is that it enables you to prevent errors in a program
with no type annotations:  whenever the static checker is unable
to verify an operation, it would insert a dynamic check.  Run-time checking
would also be useful in verifying whether the suppressed warnings are
correct &mdash; whether the programmer made a mistake when writing them.
</p>

<p>
The annotation processor (the pluggable type-checker) should automatically
insert the checks, as part of the compilation process.
</p>

<p>
There should be various modes for the run-time checks:
</p>
<ul>
  <li>fail immediately.</li>
  <li>logging, to permit post-mortem debugging without crashing the program.</li>
</ul>

<p>
The run-time penalty should be small:  a run-time check is necessary only
at the location of each cast or suppressed warning.  Everywhere that the
compile-time checker reports no possible error, there is no need to insert a
check.  But, it will be an interesting project to determine how to minimize
the run-time cost.
</p>

<p>
Another interesting, and more challenging, design question is whether you need to add and maintain
a run-time representation of the property being tested.  It's easy to test
whether a particular value is null, but how do you test whether it is
tainted, or should be treated as immutable?  For a more concrete example,
see the discussion of the (not yet implemented)
[Javari run-time checker](http://pag.csail.mit.edu/pubs/ref-immutability-oopsla2005-abstract.html).
Adding this run-time support would be an interesting and challenging project.
</p>

<p>
We developed a prototype for the
<a href="https://ece.uwaterloo.ca/~wdietl/publications/pubs/EnerJ11-abstract.html">EnerJ runtime system</a>.
That code could be used as starting point, or you could start afresh.
</p>

<p>
In the short term, this could be prototyped as a source- or
bytecode-rewriting approach; but integrating it into the type checker is a
better long-term implementation strategy.
</p>



<h2 id="ide-support">IDE and build system support</h2>

<p>
The Checker Framework comes with support for
<a href="https://checkerframework.org/manual/#external-tools">external tools</a>,
including both IDEs (such as an Eclipse plug-in) and build tools
(instructions for Maven, etc.).
</p>

<p>
  These plug-ins and other integration should be improved.
  We have a number of concrete ideas, but you will also probably come up
  with some after a few minutes of using the existing IDE plugins!
</p>

<p>
  This is only a task for someone who is already an expert, such as someone
  who has built IDE plugins before or is very familiar with the build system.
  One reason is that these tools tend to be complex, which can lead to
  subtle problems.
  Another reason is that we don't want to be stuck maintaining code written by
  someone who is just learning how to write an IDE plugin.
</p>

<p>
  Rather than modifying the Checker Framework's existing support or
  building new support from scratch, it may be better to adapt some other
  project's support for build systems and IDEs.  For instance, you might
  make <a href="https://github.com/coala/coala">coala</a> support the
  Checker Framework, or you might adapt the tool integration provided
  by <a href="http://errorprone.info/">Error Prone</a>.
</p>


<!--
Integrate the Checker Framework with an IDE such as Eclipse, IntelliJ, IDEA or NetBeans,
which will make pluggable type-checking easier to use and more attractive to developers.

Some specific projects include:
  * Create an IDE plug-in that invokes the checker and reports any errors to the developer, just as the IDE currently does for type errors.
  * Improve the existing Eclipse plug-in.
  * Add a button to the IDE that hides/shows all annotations of a given variety, to reduce clutter.  This would be useful beyond type annotations.
  * Implement quick fixes for common errors.
  * Integrate type inference with the IDE, to make it easier for a developer to add annotations to code.
  * Improve an IDE's existing refactoring support so that it is aware of, and properly retains, type annotations.
  * Highlight defaulted types and flow-sensitive type refinements, making error messages easier to understand.
  * Highlight the parts of the code that influenced flow-sensitive type refinements, again to make errors easier to comprehend.

IDEs that build on the OpenJDK Java compiler could benefit from even tighter integration with the Checker Framework.

This project may entail the following:

  * familiarity with the IDE plug-in development environment, Eclipse PDT or NetBeans plug-in support:  By the end of the project, the developer should be familiar with building reasonably complex IDE plug-ins.

  * UI/UX design:  The developer would design a UI experience that is appealing to developers and integrates well with the developer's workflow!
-->


<h2 id="exhaustive-testing">Model checking of a type system</h2>

<p>
Design and implement an algorithm to check type soundness of a type system
by exhaustively verifying the type checker on all programs up to a certain
size. The challenge lies in efficient enumeration of all programs and
avoiding redundant checks, and in knowing the expected outcome of the
tests.  This approach is related to bounded exhaustive
testing and model checking; for a reference, see
[Efficient Software Model Checking of Soundness of Type Systems](http://www.eecs.umich.edu/~bchandra/publications/oopsla08.pdf).
</p>



</body>
</html>

<!--  LocalWords:  GSoC uwplse codespecs randoop typetools blogosphere Shi
 -->
<!--  LocalWords:  Marks's Bikesheds ICST Gyori Legunsen Marinov NonDex bc
 -->
<!--  LocalWords:  PossiblyNonDeterministic PossiblyNonDeterministicOrder
 -->
<!--  LocalWords:  DeterministicOrder Bazel PossbilyPropagatable Lazar tex
 -->
<!--  LocalWords:  NotPropagatable JavaParser contravariantly mortem EnerJ
 -->
<!--  LocalWords:  unsoundnesses nondeterministic nondeterministically ASM
 -->
<!--  LocalWords:  deterministically prototyped Stateful plugins plugin
 -->
<!--  LocalWords:  PDFs Stubparser JLint NullnessLight bytecodes YourKit
 -->
<!--  LocalWords:  timeline Uber's NullAway Uber coala BCEL mvn BCEL's AFU
 -->
<!--  LocalWords:  Signedness Jake2 README Lookup ASM's Nayuki CRC mis CWE
 -->
<!--  LocalWords:  BigInteger lockB lockA signedness microbenchmarks pre
 -->
<!--  LocalWords:  checklink subparts UnsignedBytes runtime MyClass jOOU
 -->
<!--  LocalWords:  usePriorityQueue PriorityQueue queueMinPathNode
 -->
<!--  LocalWords:  subchecker IntScope UnsignedLong UnsignedLongs
 -->