diff --git a/build.gradle b/build.gradle index b1eec257bd80..5e0d0e7b3e67 100644 --- a/build.gradle +++ b/build.gradle @@ -2,7 +2,7 @@ import de.undercouch.gradle.tasks.download.Download plugins { // https://plugins.gradle.org/plugin/com.github.johnrengelman.shadow (v5 requires Gradle 5) - id 'com.github.johnrengelman.shadow' version '5.2.0' + id 'com.github.johnrengelman.shadow' version '6.0.0' // https://plugins.gradle.org/plugin/de.undercouch.download id "de.undercouch.download" version "4.0.4" id 'java' @@ -583,7 +583,7 @@ subprojects { if (!project.name.startsWith('checker-qual')) { task tags(type: Exec) { description 'Create Emacs TAGS table' - commandLine "bash", "-c", "find . \\( -name jdk11 \\) -prune -o -name '*.java' -print | sort-directory-order | xargs ctags -e -f TAGS" + commandLine "bash", "-c", "find . \\( -name build \\) -prune -o -name '*.java' -print | sort-directory-order | xargs ctags -e -f TAGS" } } diff --git a/changelog.txt b/changelog.txt index f0408c2294be..1c92eb277550 100644 --- a/changelog.txt +++ b/changelog.txt @@ -1,8 +1,11 @@ Version 3.5.0, July 1, 2020 -The Nullness Checker now treats System.getProperty soundly. Use --Alint=permitClearProperty to disable special treatment of System.getProperty -and to permit undefining built-in system properties. +It is no longer necessary to pass -Astubs=checker.jar/javadoc.astub when +compiling a program that uses Javadoc classes. + +The Nullness Checker now treats `System.getProperty()` soundly. Use +`-Alint=permitClearProperty` to disable special treatment of +`System.getProperty()` and to permit undefining built-in system properties. Implementation details: Changed the types of some fields and methods from array to List: @@ -12,6 +15,9 @@ QualifierDefaults.STANDARD_CLIMB_DEFAULTS_BOTTOM QualifierDefaults.STANDARD_UNCHECKED_DEFAULTS_TOP QualifierDefaults.STANDARD_UNCHECKED_DEFAULTS_BOTTOM +In AbstractQualifierPolymorphism, use AnnotationMirrors instead of sets of +annotation mirrors. + --------------------------------------------------------------------------- Version 3.4.1, June 1, 2020 @@ -25,8 +31,8 @@ New command-line option: -AmergeStubsWithSource If both a stub file and a source file are available, use both. Closed issues: -2893, 3021, 3128, 3160, 3232, 3277, 3285, 3289, 3295, 3302, 3305, 3307, 3310, -3316, 3318, 3329. +#2893, #3021, #3128, #3160, #3232, #3277, #3285, #3289, #3295, #3302, #3305, +#3307, #3310, #3316, #3318, #3329. --------------------------------------------------------------------------- @@ -40,7 +46,7 @@ The Returns Receiver Checker enables documenting and checking that a method returns its receiver (i.e., the `this` parameter). Closed issues: -3267, 3263, 3217, 3212, 3201, 3111, 3010, 2943, 2930. +#3267, #3263, #3217, #3212, #3201, #3111, #3010, #2943, #2930. --------------------------------------------------------------------------- @@ -88,8 +94,8 @@ Implementation details: * AbstractTypeProcessor#typeProcessingOver() always gets called. Closed issues: -1307, 1881, 1929, 2432, 2793, 3040, 3046, 3050, 3056, 3083, 3124, 3126, 3129, -3132, 3139, 3149, 3150, 3167, 3189. +#1307, #1881, #1929, #2432, #2793, #3040, #3046, #3050, #3056, #3083, #3124, +#3126, #3129, #3132, #3139, #3149, #3150, #3167, #3189. --------------------------------------------------------------------------- @@ -100,7 +106,7 @@ contains "initialization". Previously, it suppressed all warnings issued by the Nullness Checker or the Initialization Checker. Closed issues: -2719, 3001, 3020, 3069, 3093, 3120. +#2719, #3001, #3020, #3069, #3093, #3120. --------------------------------------------------------------------------- @@ -126,7 +132,8 @@ Implementation details: * Renamed one overload of SourceChecker.printMessages to printOrStoreMessage. Closed issues: -2181, 2975, 3018, 3022, 3032, 3036, 3037, 3038, 3041, 3049, 3055, 3076. +#2181, #2975, #3018, #3022, #3032, #3036, #3037, #3038, #3041, #3049, #3055, +#3076. --------------------------------------------------------------------------- @@ -145,7 +152,7 @@ Implementation details: * Renamed ConditionalPostcondition#annoResult to ConditionalPostcondition#resultValue. Closed issues: -2867, 2897, 2972. +#2867, #2897, #2972. --------------------------------------------------------------------------- @@ -160,8 +167,8 @@ Implementation details: * Deprecated AnnotatedTypes#isTypeAnnotation and AnnotatedTypes#hasTypeQualifierElementTypes. Closed issues: -945, 1224, 2024, 2744, 2809, 2815, 2818, 2830, 2840, 2853, 2854, 2865, 2873, -2874, 2878, 2880, 2886, 2888, 2900, 2905, 2919, 2923. +#945, #1224, #2024, #2744, #2809, #2815, #2818, #2830, #2840, #2853, #2854, +#2865, #2873, #2874, #2878, #2880, #2886, #2888, #2900, #2905, #2919, #2923. --------------------------------------------------------------------------- @@ -180,8 +187,8 @@ Implementation details: AnnotationMirrors Closed issues: -1169, 1654, 2081, 2703, 2739, 2749, 2779, 2781, 2798, 2820, 2824, 2829, 2842, -2845, 2848. +#1169, #1654, #2081, #2703, #2739, #2749, #2779, #2781, #2798, #2820, #2824, +#2829, #2842, #2845, #2848. --------------------------------------------------------------------------- @@ -190,7 +197,7 @@ Version 2.11.1, October 1, 2019 The manual links to the Object Construction Checker. Closed issues: -1635, 2718, 2767. +#1635, #2718, #2767. --------------------------------------------------------------------------- @@ -205,8 +212,8 @@ Running the Checker Framework on a Java 9 JVM is not yet supported. Version 2.10.1, August 22, 2019 Closed issues: -1152, 1614, 2031, 2482, 2543, 2587, 2678, 2686, 2690, 2712, 2717, 2713, 2721, -2725, 2729. +#1152, #1614, #2031, #2482, #2543, #2587, #2678, #2686, #2690, #2712, #2717, +#2713, #2721, #2725, #2729. --------------------------------------------------------------------------- @@ -215,8 +222,8 @@ Version 2.10.0, August 1, 2019 Removed the NullnessRawnessChecker. Use the NullnessChecker instead. Closed issues: -435, 939, 1430, 1687, 1771, 1902, 2173, 2345, 2470, 2534, 2606, 2613, 2619, -2633, 2638. +#435, #939, #1430, #1687, #1771, #1902, #2173, #2345, #2470, #2534, #2606, +#2613, #2619, #2633, #2638. --------------------------------------------------------------------------- @@ -259,8 +266,8 @@ Implementation details: isSuperConstructorCall and isThisConstructorCall Closed issues: -2247, 2391, 2409, 2434, 2451, 2457, 2468, 2484, 2485, 2493, 2505, 2536, 2537, -2540, 2541, 2564, 2565, 2585. +#2247, #2391, #2409, #2434, #2451, #2457, #2468, #2484, #2485, #2493, #2505, +#2536, #2537, #2540, #2541, #2564, #2565, #2585. --------------------------------------------------------------------------- @@ -277,7 +284,7 @@ Implementation detail: deprecated TreeUtils.skipParens in favor of TreeUtils.withoutParens which has the same specification. Closed issues: -2291, 2406, 2469, 2477, 2479, 2480, 2494, 2499. +#2291, #2406, #2469, #2477, #2479, #2480, #2494, #2499. --------------------------------------------------------------------------- @@ -286,8 +293,8 @@ Version 2.8.1, May 1, 2019 Moved text about the Purity Checker into its own chapter in the manual. Closed issues: -660, 2030, 2223, 2240, 2244, 2375, 2407, 2410, 2415, 2420, 2421, 2446, 2447, -2460, 2462. +#660, #2030, #2223, #2240, #2244, #2375, #2407, #2410, #2415, #2420, #2421, +#2446, #2447, #2460, #2462. --------------------------------------------------------------------------- @@ -323,8 +330,8 @@ Interface changes: AnnotatedTypeFactory#getEnclosingElementForArtificialTree Closed issues: -2159, 2230, 2318, 2324, 2330, 2334, 2343, 2344, 2353, 2366, 2367, 2370, 2371, -2385. +#2159, #2230, #2318, #2324, #2330, #2334, #2343, #2344, #2353, #2366, #2367, +#2370, #2371, #2385. --------------------------------------------------------------------------- @@ -352,7 +359,8 @@ Added missing checks regarding annotations on classes, constructor declarations, and constructor invocations. You may see new warnings. Closed issues: -788, 1751, 2147, 2163, 2186, 2235, 2243, 2263, 2264, 2286, 2302, 2326, 2327. +#788, #1751, #2147, #2163, #2186, #2235, #2243, #2263, #2264, #2286, #2302, +#2326, #2327. --------------------------------------------------------------------------- @@ -369,7 +377,7 @@ such as by adjusting wording or adding additional information. Relevant to type system implementers: Renamed method areSameIgnoringValues to areSameByName. -Closed issues: 2008, 2166, 2185, 2187, 2221, 2224, 2229, 2234, 2248. +Closed issues: #2008, #2166, #2185, #2187, #2221, #2224, #2229, #2234, #2248. Also fixed false negatives in handling of Map.get(). --------------------------------------------------------------------------- @@ -379,7 +387,7 @@ Version 2.5.8, December 5, 2018 The manual now links to the AWS KMS compliance checker, which enforces that calls to AWS KMS only generate 256-bit keys. -Closed issues: 372, 1678, 2207, 2212, 2217. +Closed issues: #372, #1678, #2207, #2212, #2217. --------------------------------------------------------------------------- @@ -392,7 +400,7 @@ The manual links to the Rx Thread & Effect Checker, which enforces UI Thread safety properties for stream-based Android applications. Closed issues: -1014, 2151, 2178, 2180, 2183, 2188, 2190, 2195, 2196, 2198, 2199 +#1014, #2151, #2178, #2180, #2183, #2188, #2190, #2195, #2196, #2198, #2199. --------------------------------------------------------------------------- @@ -407,7 +415,7 @@ which the Checker Framework no longer supports. It remains available on Maven Central, with versions 2.5.5 and earlier. Closed issues: -2135, 2157, 2158, 2164, 2171. +#2135, #2157, #2158, #2164, #2171. --------------------------------------------------------------------------- @@ -423,21 +431,21 @@ Added -AnoPrintErrorStack to disable it (which should be rare). Replaced ErrorReporter class with BugInCF and UserError exceptions. Closed issues: -1999, 2008, 2023, 2029, 2074, 2088, 2098, 2099, 2102, 2107. +#1999, #2008, #2023, #2029, #2074, #2088, #2098, #2099, #2102, #2107. --------------------------------------------------------------------------- Version 2.5.4, August 1, 2018 Closed issues: -2030, 2048, 2052, 2059, 2065, 2067, 2073, 2082. +#2030, #2048, #2052, #2059, #2065, #2067, #2073, #2082. --------------------------------------------------------------------------- Version 2.5.3, July 2, 2018 Closed issues: -266, 1248, 1678, 2010, 2011, 2018, 2020, 2046, 2047, 2054. +#266, #1248, #1678, #2010, #2011, #2018, #2020, #2046, #2047, #2054. --------------------------------------------------------------------------- @@ -447,7 +455,7 @@ In the Map Key Checker, null is now @UnknownKeyFor. See the "Map Key Checker" chapter in the manual for more details. Closed issues: -370, 469, 1701, 1916, 1922, 1959, 1976, 1978, 1981, 1983, 1984, 1991, 1992. +#370, #469, #1701, #1916, #1922, #1959, #1976, #1978, #1981, #1983, #1984, #1991, #1992. --------------------------------------------------------------------------- @@ -456,8 +464,8 @@ Version 2.5.1, May 1, 2018 Added a Maven artifact of the Checker Framework testing library, testlib. Closed issues: -849, 1739, 1838, 1847, 1890, 1901, 1911, 1912, 1913, 1934, 1936, 1941, 1942, -1945, 1946, 1948, 1949, 1952, 1953, 1956, 1958. +#849, #1739, #1838, #1847, #1890, #1901, #1911, #1912, #1913, #1934, #1936, +#1941, #1942, #1945, #1946, #1948, #1949, #1952, #1953, #1956, #1958. --------------------------------------------------------------------------- @@ -472,8 +480,8 @@ annotations in comments" section in the "Handling legacy code" chapter in the manual for instructions on how to remove annotations from comments. Closed issues: -515, 1667, 1739, 1776, 1819, 1863, 1864, 1865, 1866, 1867, 1870, 1876, 1879, -1882, 1898, 1903, 1905, 1906, 1910, 1914, 1915, 1920. +#515, #1667, #1739, #1776, #1819, #1863, #1864, #1865, #1866, #1867, #1870, +#1876, #1879, #1882, #1898, #1903, #1905, #1906, #1910, #1914, #1915, #1920. --------------------------------------------------------------------------- @@ -504,26 +512,26 @@ Simplified the instructions for running the Checker Framework with Gradle. The Checker Framework Eclipse plugin is no longer released nor supported. Closed issues: -65, 66, 100, 108, 175, 184, 190, 194, 209, 239, 260, 270, 274, 293, 302, 303, -306, 321, 325, 341, 356, 360, 361, 371, 383, 385, 391, 397, 398, 410, 423, 424, -431, 430, 432, 548, 1131, 1148, 1213, 1455, 1504, 1642, 1685, 1770, 1796, 1797, -1801, 1809, 1810, 1815, 1817, 1818, 1823, 1831, 1837, 1839, 1850, 1851, 1852, -1861. +#65, #66, #100, #108, #175, #184, #190, #194, #209, #239, #260, #270, #274, +#293, #302, #303, #306, #321, #325, #341, #356, #360, #361, #371, #383, #385, +#391, #397, #398, #410, #423, #424, #431, #430, #432, #548, #1131, #1148, +#1213, #1455, #1504, #1642, #1685, #1770, #1796, #1797, #1801, #1809, #1810, +#1815, #1817, #1818, #1823, #1831, #1837, #1839, #1850, #1851, #1852, #1861. --------------------------------------------------------------------------- Version 2.3.2, February 1, 2018 Closed issues: -946, 1133, 1232, 1319, 1625, 1633, 1696, 1709, 1712, 1734, 1738, 1749, 1754, -1760, 1761, 1768, 1769, 1781. +#946, #1133, #1232, #1319, #1625, #1633, #1696, #1709, #1712, #1734, #1738, +#1749, #1754, #1760, #1761, #1768, #1769, #1781. --------------------------------------------------------------------------- Version 2.3.1, January 2, 2018 Closed issues: -1695, 1696, 1697, 1698, 1705, 1708, 1711, 1714, 1715, 1724. +#1695, #1696, #1697, #1698, #1705, #1708, #1711, #1714, #1715, #1724. --------------------------------------------------------------------------- @@ -535,8 +543,8 @@ TreeUtils or TypesUtils. Adapted a few method names and parameter orders for consistency. Closed issues: -951, 1356, 1495, 1602, 1605, 1623, 1628, 1636, 1641, 1653, 1655, 1664, 1665, -1681, 1684, 1688, 1690. +#951, #1356, #1495, #1602, #1605, #1623, #1628, #1636, #1641, #1653, #1655, +#1664, #1665, #1681, #1684, #1688, #1690. --------------------------------------------------------------------------- @@ -547,12 +555,12 @@ indicates that the value is not equals() to any other value. An annotated version of the Commons IO library appears in checker/lib/ . -Closed issue 1586, which required re-opening issues 293 and 341 until +Closed issue #1586, which required re-opening issues 293 and 341 until proper fixes for those are implemented. Closed issues: -1386, 1389, 1423, 1520, 1529, 1530, 1531, 1546, 1553, 1555, 1565, 1570, 1579, -1580, 1582, 1585, 1586, 1587, 1598, 1609, 1615, 1617. +#1386, #1389, #1423, #1520, #1529, #1530, #1531, #1546, #1553, #1555, #1565, +#1570, #1579, #1580, #1582, #1585, #1586, #1587, #1598, #1609, #1615, #1617. --------------------------------------------------------------------------- @@ -566,8 +574,8 @@ byte code. A new jar, checker-qual7.jar, includes the qualifiers and utility classes compiled to Java 7 byte code. Closed issues: -724, 1431, 1442, 1459, 1464, 1482, 1496, 1499, 1500, 1506, 1507, 1510, 1512, -1522, 1526, 1528, 1532, 1535, 1542, 1543. +#724, #1431, #1442, #1459, #1464, #1482, #1496, #1499, #1500, #1506, #1507, +#1510, #1512, #1522, #1526, #1528, #1532, #1535, #1542, #1543. --------------------------------------------------------------------------- @@ -584,8 +592,9 @@ using standard Java syntax (rather than at the top level using a name that contains "$". You need to update your stub files to conform to the new syntax. Closed issues: -220, 293, 297, 341, 375, 407, 536, 571, 798, 867, 1180, 1214, 1218, 1371, 1411, -1427, 1428, 1435, 1438, 1450, 1456, 1460, 1466, 1473, 1474. +#220, #293, #297, #341, #375, #407, #536, #571, #798, #867, #1180, #1214, #1218, +#1371, #1411, #1427, #1428, #1435, #1438, #1450, #1456, #1460, #1466, #1473, +#1474. --------------------------------------------------------------------------- @@ -603,8 +612,9 @@ Use the option -AconservativeUninferredTypeArguments to see warnings about method calls where the Checker Framework fails to infer type arguments. Closed issues: -753, 804, 961, 1032, 1062, 1066, 1098, 1209, 1280, 1316, 1329, 1355, 1365, -1366, 1367, 1377, 1379, 1382, 1384, 1397, 1398, 1399, 1402, 1404, 1406, 1407. +#753, #804, #961, #1032, #1062, #1066, #1098, #1209, #1280, #1316, #1329, #1355, +#1365, #1366, #1367, #1377, #1379, #1382, #1384, #1397, #1398, #1399, #1402, +#1404, #1406, #1407. --------------------------------------------------------------------------- @@ -617,8 +627,8 @@ The manual explains how to configure Android projects that use Android Studio 3.0 and Android Gradle Plugin 3.0.0, which support type annotations. Closed issues: -146, 1264, 1275, 1290, 1303, 1308, 1310, 1312, 1313, 1315, 1323, 1324, 1331, -1332, 1333, 1334, 1347, 1357, 1372. +#146, #1264, #1275, #1290, #1303, #1308, #1310, #1312, #1313, #1315, #1323, +#1324, #1331, #1332, #1333, #1334, #1347, #1357, #1372. --------------------------------------------------------------------------- @@ -630,8 +640,8 @@ The stubparser license has been updated. You can now use stubparser under either the LGPL or the Apache license, whichever you prefer. Closed issues: -254, 1201, 1229, 1236, 1239, 1240, 1257, 1265, 1270, 1271, 1272, 1274, 1288, -1291, 1299, 1304, 1305. +#254, #1201, #1229, #1236, #1239, #1240, #1257, #1265, #1270, #1271, #1272, +#1274, #1288, #1291, #1299, #1304, #1305. --------------------------------------------------------------------------- @@ -641,7 +651,7 @@ The manual contains new FAQ (frequently asked questions) sections about false positive warnings and about inference for field types. Closed issues: -989, 1096, 1136, 1228. +#989, #1096, #1136, #1228. --------------------------------------------------------------------------- @@ -654,8 +664,9 @@ expression, a statically-known lower and upper bound. Use the new feature. Closed issues: -134, 216, 227, 307, 334, 437, 445, 718, 1044, 1045, 1051, 1052, 1054, 1055, -1059, 1077, 1087, 1102, 1108, 1110, 1111, 1120, 1124, 1127, 1132. +#134, #216, #227, #307, #334, #437, #445, #718, #1044, #1045, #1051, #1052, +#1054, #1055, #1059, #1077, #1087, #1102, #1108, #1110, #1111, #1120, #1124, +#1127, #1132. --------------------------------------------------------------------------- @@ -667,8 +678,8 @@ positives. The new option -AconservativeUninferredTypeArguments can be used to get the conservative behavior. Closed issues: -1006, 1011, 1015, 1027, 1035, 1036, 1037, 1039, 1043, 1046, 1049, 1053, 1072, -1084. +#1006, #1011, #1015, #1027, #1035, #1036, #1037, #1039, #1043, #1046, #1049, +#1053, #1072, #1084. --------------------------------------------------------------------------- @@ -682,7 +693,7 @@ The documentation has been reorganized in the Checker Framework repository. The manual, tutorial, and webpages now appear under checker-framework/docs/. Closed issues: -770, 1003, 1012. +#770, #1003, #1012. --------------------------------------------------------------------------- @@ -694,16 +705,15 @@ Manual improvements: * Better explanation of relationship between Fake Enum and Subtyping Checkers. Closed issues: -154, 322, 402, 404, 433, 531, 578, 720, 795, 916, 953, 973, 974, 975, 976, -980, 988, 1000. +#154, #322, #402, #404, #433, #531, #578, #720, #795, #916, #953, #973, #974, +#975, #976, #980, #988, #1000. --------------------------------------------------------------------------- Version 2.1.6, 1 December 2016 Closed issues: - -412, 475. +#412, #475. --------------------------------------------------------------------------- @@ -723,29 +733,29 @@ The manual describes how to run a checker within the NetBeans IDE. The manual describes two approaches to creating a type alias or typedef. Closed issues: -643, 775, 887, 906, 941. +#643, #775, #887, #906, #941. --------------------------------------------------------------------------- Version 2.1.4, 3 October 2016 Closed issues: -885, 886, 919. +#885, #886, #919. --------------------------------------------------------------------------- Version 2.1.3, 16 September 2016 Closed issues: -122, 488, 495, 580, 618, 647, 713, 764, 818, 872, 893, 894, 901, 902, 903, -905, 913. +#122, #488, #495, #580, #618, #647, #713, #764, #818, #872, #893, #894, #901, +#902, #903, #905, #913. --------------------------------------------------------------------------- Version 2.1.2, 1 September 2016 Closed issues: -182, 367, 712, 811, 846, 857, 858, 863, 870, 871, 878, 883, 888. +#182, #367, #712, #811, #846, #857, #858, #863, #870, #871, #878, #883, #888. --------------------------------------------------------------------------- @@ -758,7 +768,8 @@ AnnotatedTypeFactory#createSupportedTypeQualifiers() must now return a mutable list. Checkers that override this method will have to be changed. Closed issues: -384, 590, 681, 790, 805, 809, 810, 820, 824, 826, 829, 838, 845, 850, 856. +#384, #590, #681, #790, #805, #809, #810, #820, #824, #826, #829, #838, #845, +#850, #856. --------------------------------------------------------------------------- @@ -771,8 +782,8 @@ The Lock Checker expresses the annotated variable as ``; previously it used `itself`, which may conflict with an identifier. Closed issues: -166, 273, 358, 408, 471, 484, 594, 625, 692, 700, 701, 711, 717, 752, 756, -759, 763, 767, 779, 783, 794, 807, 808. +#166, #273, #358, #408, #471, #484, #594, #625, #692, #700, #701, #711, #717, +#752, #756, #759, #763, #767, #779, #783, #794, #807, #808. --------------------------------------------------------------------------- @@ -790,8 +801,8 @@ depends on classes in the Checker Framework, then you should add those classes to the classpath when you run the compiler. Closed issues: -171, 250, 291, 523, 577, 672, 680, 688, 689, 690, 691, 695, 696, 698, 702, -704, 705, 706, 707, 720, 721, 723, 728, 736, 738, 740. +#171, #250, #291, #523, #577, #672, #680, #688, #689, #690, #691, #695, #696, +#698, #702, #704, #705, #706, #707, #720, #721, #723, #728, #736, #738, #740. --------------------------------------------------------------------------- @@ -847,7 +858,8 @@ Tool changes: script that performs type inference. Closed issues: -69, 86, 199, 299, 329, 421, 428, 557, 564, 573, 579, 665, 668, 669, 670, 671. +#69, #86, #199, #299, #329, #421, #428, #557, #564, #573, #579, #665, #668, #669, +#670, #671. --------------------------------------------------------------------------- @@ -857,7 +869,7 @@ Documentation: * Clarified Maven documentation about use of annotations in comments. * Added FAQ about annotating fully-qualified type names. -Closed issues: 438, 572, 579, 607, 624, 631. +Closed issues: #438, #572, #579, #607, #624, #631. --------------------------------------------------------------------------- @@ -882,7 +894,7 @@ added under checker-framework/docs/examples/GradleExamples/. Renamed enum DefaultLocation to TypeUseLocation. -Closed issues: 130, 263, 345, 458, 559, 559, 574, 582, 596. +Closed issues: #130, #263, #345, #458, #559, #559, #574, #582, #596. --------------------------------------------------------------------------- @@ -901,7 +913,7 @@ For type-system developers: explicitly specifies a different one. Previously a type system needed to explicitly request CLIMB-to-top, but now it is the default. -Closed issues: 524, 563, 568. +Closed issues: #524, #563, #568. --------------------------------------------------------------------------- @@ -931,13 +943,13 @@ For type-system developers: org.checkerframework.framework.qual.Default{,Qualifier}ForUnannotatedCode to DefaultInUncheckedCodeFor and DefaultQualifierInHierarchyInUncheckedCode. -Closed issues: 169, 363, 448, 478, 496, 516, 529. +Closed issues: #169, #363, #448, #478, #496, #516, #529. --------------------------------------------------------------------------- Version 1.9.9, 1 December 2015 -Fixed issues: 511, 513, 514, 455, 527. +Fixed issues: #511, #513, #514, #455, #527. Removed the javac_maven script and batch file, which had been previously deprecated. @@ -956,19 +968,19 @@ docs/examples/MavenExample. The javac_maven script (and batch file) are deprecated and will be removed as of December 2015. -Fixed issues: 487, 500, 502. +Fixed issues: #487, #500, #502. --------------------------------------------------------------------------- Version 1.9.7, 24 October 2015 -Fixed issues: 291, 474. +Fixed issues: #291, #474. ---------------------------------------------------------------------- Version 1.9.6, 8 October 2015 -Fixed issue: 460. +Fixed issue: #460. ---------------------------------------------------------------------- @@ -981,7 +993,7 @@ Test Framework Updates: * If a test used methods that were previously found on CheckerTest, you may find them in TestUtilities. -Fixed issues: 438, 457, 459. +Fixed issues: #438, #457, #459. ---------------------------------------------------------------------- @@ -999,7 +1011,7 @@ cloned the old repository, then discard your old clone and create a new one using this command: git clone https://github.com/typetools/checker-framework.git -Fixed issues: 427, 429, 434, 442, 450. +Fixed issues: #427, #429, #434, #442, #450. ---------------------------------------------------------------------- @@ -1016,7 +1028,7 @@ New command-line options: Various bug fixes and documentation improvements. -Fixed issues: 436. +Fixed issues: #436. ---------------------------------------------------------------------- @@ -1026,7 +1038,7 @@ Internationalization Format String Checker: This new type-checker prevents use of incorrect internationalization format strings. -Fixed issues: 434. +Fixed issues: #434. ---------------------------------------------------------------------- @@ -1065,21 +1077,21 @@ false positive warnings caused by reflection. The documentation for the Map Key Checker has been moved into its own chapter in the manual. -Fixed issues: 221, 241, 313, 314, 328, 335, 337, 338, 339, 355, 369, - 376, 378, 386, 388, 389, 393, 403, 404, 413, 414, 415, - 417, 418, 420, 421, 422, 426. +Fixed issues: #221, #241, #313, #314, #328, #335, #337, #338, #339, #355, #369, + #376, #378, #386, #388, #389, #393, #403, #404, #413, #414, #415, + #417, #418, #420, #421, #422, #426. ---------------------------------------------------------------------- Version 1.8.11, 2 March 2015 -Fixed issues: 396, 400, 401. +Fixed issues: #396, #400, #401. ---------------------------------------------------------------------- Version 1.8.10, 30 January 2015 -Fixed issues: 37, 127, 350, 364, 365, 387, 392, 395. +Fixed issues: #37, #127, #350, #364, #365, #387, #392, #395. ---------------------------------------------------------------------- @@ -1088,7 +1100,7 @@ Version 1.8.9, 19 December 2014 Aliasing Checker: This new type-checker ensures that an expression has no aliases. -Fixed issues: 362, 380, 382. +Fixed issues: #362, #380, #382. ---------------------------------------------------------------------- @@ -1108,7 +1120,7 @@ E.g. The Nullness checker supports Android annotations android.support.annotation.NonNull and android.support.annotation.Nullable. -Fixed issues: 366, 379. +Fixed issues: #366, #379. ---------------------------------------------------------------------- @@ -1118,11 +1130,11 @@ Fix performance regression introduced in release 1.8.6. Nullness Checker: * Updated Nullness annotations in the annotated JDK. - See issues: 336, 340, 374. + See issues: #336, #340, #374. * String concatenations with null literals are now @NonNull - rather than @Nullable. See issue 357. + rather than @Nullable. See issue #357. -Fixed issues: 200, 300, 332, 336, 340, 357, 359, 373, 374. +Fixed issues: #200, #300, #332, #336, #340, #357, #359, #373, #374. ---------------------------------------------------------------------- @@ -1160,7 +1172,7 @@ Improved Java 7 compatibility and introduced Java 7 compliant annotations for the Nullness Checker. Please see the section on "Class-file compatibility with Java 7" in the manual for more details. -Fixed issue 347. +Fixed issue #347. ---------------------------------------------------------------------- @@ -1197,7 +1209,7 @@ expressions, but it does issue a lambda.unsupported warning when type-checking code containing lambda expressions. Full support for type-checking lambda expressions will appear in a future release. -Fixed issue 343. +Fixed issue #343. ---------------------------------------------------------------------- @@ -1207,11 +1219,11 @@ Updated the Initialization Checker section in the manual with a new introduction paragraph. Removed the Maven plugin section from the manual as the plugin is -no longer maintained and the final release was on June 2, 2014. +no longer maintained and the final release was on June 2, #2014. The javac_maven script (and batch file) are available to use the Checker Framework from Maven. -Fixed issue 331. +Fixed issue #331. ---------------------------------------------------------------------- @@ -1236,7 +1248,7 @@ to use the script in the Maven section of the manual. The Checker Framework installation instructions in the manual have been updated. -Fixed issues: 312, 315, 316, 318, 319, 324, 326, 327. +Fixed issues: #312, #315, #316, #318, #319, #324, #326, #327. ---------------------------------------------------------------------- @@ -1246,7 +1258,7 @@ Support to directly use the Java 8 javac in addition to jsr308-langtools. Added docs/examples directory to checker-framework.zip. New section in the manual describing the contents of checker-framework.zip. -Fixed issues: 204, 304, 320. +Fixed issues: #204, #304, #320. ---------------------------------------------------------------------- @@ -1289,13 +1301,13 @@ to the final bytecode. Reduce special treatment of checkers.quals.Unqualified. -Fixed issues: 170, 240, 265, 281. +Fixed issues: #170, #240, #265, #281. ---------------------------------------------------------------------- Version 1.7.3, 4 February 2014 -Fixes for Issues 210, 253, 280, 288. +Fixes for Issues #210, #253, #280, #288. Manual: Improved discussion of checker guarantees. @@ -1310,13 +1322,13 @@ Eclipse Plugin: Version 1.7.2, 2 January 2014 -Fixed issues: 289, 292, 295, 296, 298. +Fixed issues: #289, #292, #295, #296, #298. ---------------------------------------------------------------------- Version 1.7.1, 9 December 2013 -Fixes for Issues 141, 145, 257, 261, 269, 267, 275, 278, 282, 283, 284, 285. +Fixes for Issues #141, #145, #257, #261, #269, #267, #275, #278, #282, #283, #284, #285. Implementation details: Renamed AbstractBasicAnnotatedTypeFactory to GenericAnnotatedTypeFactory @@ -1650,7 +1662,7 @@ Code refactoring: which might require changes in downstream code. Internal framework improvements: - Fixed Issues 136, 139, 142, 156. + Fixed Issues #136, #139, #142, #156. Bug fixes and documentation improvements. ---------------------------------------------------------------------- @@ -1778,7 +1790,7 @@ Regex Checker: Internal bug fixes: Improve flow's support of annotations with parameters. - Fix generics corner cases (Issues 131, 132, 133, 135). + Fix generics corner cases (Issues #131, #132, #133, #135). Support type annotations in annotations and type-check annotations. Improve reflective look-up of visitors and factories. Small cleanups. @@ -1905,7 +1917,7 @@ Documentation improvements. Version 1.2.1, 20 Sep 2011 -Fix issues 109, 110, 111 and various other cleanups. +Fix issues #109, #110, #111 and various other cleanups. Improvements to the release process. Documentation improvements. diff --git a/checker-qual/build.gradle b/checker-qual/build.gradle index e2db5b794323..121e0c1067c6 100644 --- a/checker-qual/build.gradle +++ b/checker-qual/build.gradle @@ -4,7 +4,7 @@ buildscript { } dependencies { // Create OSGI bundles - classpath "biz.aQute.bnd:biz.aQute.bnd.gradle:5.1.0" + classpath "biz.aQute.bnd:biz.aQute.bnd.gradle:5.1.1" } } diff --git a/checker/bin-devel/build.sh b/checker/bin-devel/build.sh index 83b6ac8609ca..bc0e8ee14922 100755 --- a/checker/bin-devel/build.sh +++ b/checker/bin-devel/build.sh @@ -21,20 +21,20 @@ fi echo "JAVA_HOME=${JAVA_HOME}" if [ -d "/tmp/$USER/plume-scripts" ] ; then - (cd /tmp/$USER/plume-scripts && git pull -q) + (cd "/tmp/$USER/plume-scripts" && git pull -q) else - mkdir -p /tmp/$USER && (cd /tmp/$USER && (git clone --depth 1 -q https://github.com/plume-lib/plume-scripts.git || git clone --depth 1 -q https://github.com/plume-lib/plume-scripts.git)) + mkdir -p "/tmp/$USER" && (cd "/tmp/$USER" && (git clone --depth 1 -q https://github.com/plume-lib/plume-scripts.git || git clone --depth 1 -q https://github.com/plume-lib/plume-scripts.git)) fi # Clone the annotated JDK into ../jdk . -/tmp/$USER/plume-scripts/git-clone-related typetools jdk +"/tmp/$USER/plume-scripts/git-clone-related" typetools jdk AFU="${AFU:-../annotation-tools/annotation-file-utilities}" # Don't use `AT=${AFU}/..` which causes a git failure. AT=$(dirname "${AFU}") ## Build annotation-tools (Annotation File Utilities) -/tmp/$USER/plume-scripts/git-clone-related typetools annotation-tools "${AT}" +"/tmp/$USER/plume-scripts/git-clone-related" typetools annotation-tools "${AT}" if [ ! -d ../annotation-tools ] ; then ln -s "${AT}" ../annotation-tools fi @@ -45,7 +45,7 @@ echo "... done: (cd ${AT} && ./.travis-build-without-test.sh)" ## Build stubparser -/tmp/$USER/plume-scripts/git-clone-related typetools stubparser +"/tmp/$USER/plume-scripts/git-clone-related" typetools stubparser echo "Running: (cd ../stubparser/ && ./.travis-build-without-test.sh)" (cd ../stubparser/ && ./.travis-build-without-test.sh) echo "... done: (cd ../stubparser/ && ./.travis-build-without-test.sh)" diff --git a/checker/bin-devel/test-daikon-part1.sh b/checker/bin-devel/test-daikon-part1.sh index d35cfc89dc05..671590df1a62 100755 --- a/checker/bin-devel/test-daikon-part1.sh +++ b/checker/bin-devel/test-daikon-part1.sh @@ -13,7 +13,7 @@ source "$SCRIPTDIR"/build.sh # daikon-typecheck: 15 minutes -/tmp/$USER/plume-scripts/git-clone-related codespecs daikon +"/tmp/$USER/plume-scripts/git-clone-related" codespecs daikon cd ../daikon git log | head -n 5 make compile diff --git a/checker/bin-devel/test-daikon-part2.sh b/checker/bin-devel/test-daikon-part2.sh index dcb8967af505..cb2de5bb6bf1 100755 --- a/checker/bin-devel/test-daikon-part2.sh +++ b/checker/bin-devel/test-daikon-part2.sh @@ -13,7 +13,7 @@ source "$SCRIPTDIR"/build.sh # daikon-typecheck: 15 minutes -/tmp/$USER/plume-scripts/git-clone-related codespecs daikon +"/tmp/$USER/plume-scripts/git-clone-related" codespecs daikon cd ../daikon git log | head -n 5 make compile diff --git a/checker/bin-devel/test-daikon.sh b/checker/bin-devel/test-daikon.sh index e6daa60854f0..c5813e0eb70b 100755 --- a/checker/bin-devel/test-daikon.sh +++ b/checker/bin-devel/test-daikon.sh @@ -13,7 +13,7 @@ source "$SCRIPTDIR"/build.sh # daikon-typecheck: 15 minutes -/tmp/$USER/plume-scripts/git-clone-related codespecs daikon +"/tmp/$USER/plume-scripts/git-clone-related" codespecs daikon cd ../daikon git log | head -n 5 make compile diff --git a/checker/bin-devel/test-downstream.sh b/checker/bin-devel/test-downstream.sh index dbf95114e345..902b2399c39a 100755 --- a/checker/bin-devel/test-downstream.sh +++ b/checker/bin-devel/test-downstream.sh @@ -22,5 +22,5 @@ source "$SCRIPTDIR"/build.sh ## * guava is run as a separate CI project # Checker Framework demos -/tmp/$USER/plume-scripts/git-clone-related typetools checker-framework.demos +"/tmp/$USER/plume-scripts/git-clone-related" typetools checker-framework.demos ./gradlew :checker:demosTests --console=plain --warning-mode=all --no-daemon diff --git a/checker/bin-devel/test-guava-formatter.sh b/checker/bin-devel/test-guava-formatter.sh index 07ef3a5d88ed..809f62985943 100755 --- a/checker/bin-devel/test-guava-formatter.sh +++ b/checker/bin-devel/test-guava-formatter.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava ./typecheck.sh formatter diff --git a/checker/bin-devel/test-guava-index.sh b/checker/bin-devel/test-guava-index.sh index c0fc6442008e..45b0cbd66542 100755 --- a/checker/bin-devel/test-guava-index.sh +++ b/checker/bin-devel/test-guava-index.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava if [ "$TRAVIS" = "true" ] ; then diff --git a/checker/bin-devel/test-guava-interning.sh b/checker/bin-devel/test-guava-interning.sh index 7b800163a1a1..6b22f2558feb 100755 --- a/checker/bin-devel/test-guava-interning.sh +++ b/checker/bin-devel/test-guava-interning.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava ./typecheck.sh interning diff --git a/checker/bin-devel/test-guava-lock.sh b/checker/bin-devel/test-guava-lock.sh index 4c5128a567a2..60d94cb21d42 100755 --- a/checker/bin-devel/test-guava-lock.sh +++ b/checker/bin-devel/test-guava-lock.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava ./typecheck.sh lock diff --git a/checker/bin-devel/test-guava-nullness.sh b/checker/bin-devel/test-guava-nullness.sh index ad35d5237704..c0ce6db006c6 100755 --- a/checker/bin-devel/test-guava-nullness.sh +++ b/checker/bin-devel/test-guava-nullness.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava ./typecheck.sh nullness diff --git a/checker/bin-devel/test-guava-regex.sh b/checker/bin-devel/test-guava-regex.sh index cd2f334c01fb..2dc45f93fa38 100755 --- a/checker/bin-devel/test-guava-regex.sh +++ b/checker/bin-devel/test-guava-regex.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava ./typecheck.sh regex diff --git a/checker/bin-devel/test-guava-signature.sh b/checker/bin-devel/test-guava-signature.sh index 8337e74ebf93..b70bae265495 100755 --- a/checker/bin-devel/test-guava-signature.sh +++ b/checker/bin-devel/test-guava-signature.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava ./typecheck.sh signature diff --git a/checker/bin-devel/test-guava.sh b/checker/bin-devel/test-guava.sh index 4be426e1cb92..af376815c8e0 100755 --- a/checker/bin-devel/test-guava.sh +++ b/checker/bin-devel/test-guava.sh @@ -12,7 +12,7 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" source "$SCRIPTDIR"/build.sh -/tmp/$USER/plume-scripts/git-clone-related typetools guava +"/tmp/$USER/plume-scripts/git-clone-related" typetools guava cd ../guava if [ "$TRAVIS" = "true" ] ; then diff --git a/checker/bin-devel/test-plume-lib.sh b/checker/bin-devel/test-plume-lib.sh index acc1a9f2adbd..4edd90dc135b 100755 --- a/checker/bin-devel/test-plume-lib.sh +++ b/checker/bin-devel/test-plume-lib.sh @@ -45,7 +45,7 @@ for PACKAGE in "${PACKAGES[@]}"; do echo "PACKAGE=${PACKAGE}" PACKAGEDIR="/tmp/${PACKAGE}" rm -rf "${PACKAGEDIR}" - /tmp/$USER/plume-scripts/git-clone-related plume-lib "${PACKAGE}" "${PACKAGEDIR}" + "/tmp/$USER/plume-scripts/git-clone-related" plume-lib "${PACKAGE}" "${PACKAGEDIR}" echo "About to call ./gradlew --console=plain -PcfLocal assemble" (cd "${PACKAGEDIR}" && ./gradlew --console=plain -PcfLocal assemble) done diff --git a/checker/bin/infer-and-annotate.sh b/checker/bin/infer-and-annotate.sh index 69798948f05e..53d5108f93c6 100755 --- a/checker/bin/infer-and-annotate.sh +++ b/checker/bin/infer-and-annotate.sh @@ -149,7 +149,8 @@ infer_and_annotate() { if [ ! "$(find $WHOLE_PROGRAM_INFERENCE_DIR -prune -empty)" ] then # Only insert annotations if there is at least one .jaif file. - insert-annotations-to-source "${insert_to_source_args[@]}" -i "$(find $WHOLE_PROGRAM_INFERENCE_DIR -name "*.jaif")" "${java_files[@]}" + # shellcheck disable=SC2046 + insert-annotations-to-source "${insert_to_source_args[@]}" -i $(find $WHOLE_PROGRAM_INFERENCE_DIR -name "*.jaif") "${java_files[@]}" fi # Updates DIFF_JAIF variable. # diff returns exit-value 1 when there are differences between files. diff --git a/checker/build.gradle b/checker/build.gradle index 6d278cad07e3..d41ea45475a4 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -1,11 +1,8 @@ -ext { - annotatedJdkHome = '../../jdk' -} sourceSets { main { resources { // Stub files, message.properties, etc. - srcDirs += ['src/main/java', "${buildDir}/generated/resources"] + srcDirs += ['src/main/java'] } } testannotations @@ -28,74 +25,6 @@ dependencies { testannotationsImplementation project(':checker-qual') } -task cloneTypetoolsJdk() { - description 'Obtain or update the annotated JDK.' - doLast { - if (file(annotatedJdkHome).exists()) { - exec { - workingDir annotatedJdkHome - executable 'git' - args = ['pull', '-q'] - ignoreExitValue = true - } - } else { - println 'Cloning annotated JDK repository.' - exec { - workingDir "${annotatedJdkHome}/../" - executable 'git' - args = ['clone', '-q', '--depth', '1', 'https://github.com/typetools/jdk.git', 'jdk'] - } - } - } -} - -task copyAndMinimizeAnnotatedJdkFiles(dependsOn: cloneTypetoolsJdk, group: 'Build') { - dependsOn ':framework:compileJava' - def inputDir = "${annotatedJdkHome}/src" - def outputDir = "${buildDir}/generated/resources/annotated-jdk/" - - description "Copy annotated JDK files to ${outputDir}. Removes private and package-private methods, method bodies, comments, etc. from the annotated JDK" - - inputs.dir file(inputDir) - outputs.dir file(outputDir) - - doLast { - FileTree tree = fileTree(dir: inputDir) - SortedSet annotatedForFiles = new TreeSet<>(); - tree.visit { FileVisitDetails fvd -> - if (!fvd.file.isDirectory() && fvd.file.name.matches(".*\\.java") - && !fvd.file.path.contains("org/checkerframework") - && !fvd.file.name.matches("module-info.java")) { - // Ignore module-info until this JavaParser bug is fixed (and merged in the StubParser): - // https://github.com/javaparser/javaparser/issues/2615 - fvd.getFile().readLines().any { line -> - if (line.contains("@AnnotatedFor") || line.contains("org.checkerframework")) { - annotatedForFiles.add(fvd.file.absolutePath) - return true; - } - } - } - } - String absolutejdkHome = file(annotatedJdkHome).absolutePath - int jdkDirStringSize = absolutejdkHome.size() - copy { - from(annotatedJdkHome) - into(outputDir) - for (String filename : annotatedForFiles) { - include filename.substring(jdkDirStringSize) - } - } - javaexec { - classpath = sourceSets.main.runtimeClasspath - - main = 'org.checkerframework.framework.stub.JavaStubifier' - args outputDir - } - } -} - -processResources.dependsOn(copyAndMinimizeAnnotatedJdkFiles) - jar { manifest { attributes("Main-Class": "org.checkerframework.framework.util.CheckerMain") diff --git a/checker/src/main/java/org/checkerframework/checker/fenum/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/fenum/jdk8.astub index 0fd9476baa1a..5175fba86eed 100644 --- a/checker/src/main/java/org/checkerframework/checker/fenum/jdk8.astub +++ b/checker/src/main/java/org/checkerframework/checker/fenum/jdk8.astub @@ -1,3 +1,5 @@ +// This file is for classes that appear in JDK 8 but not in JDK 11. + import org.checkerframework.checker.fenum.qual.*; package javax.swing; diff --git a/checker/src/main/java/org/checkerframework/checker/formatter/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/formatter/jdk8.astub deleted file mode 100644 index b9daec2ca38d..000000000000 --- a/checker/src/main/java/org/checkerframework/checker/formatter/jdk8.astub +++ /dev/null @@ -1,50 +0,0 @@ -import org.checkerframework.checker.formatter.qual.*; - -package java.util; - -class Formatter { - @FormatMethod - public Formatter format(String format, Object... args); - @FormatMethod - public Formatter format(Locale l, String format, Object... args); -} - -package java.lang; - -class String { - @FormatMethod - public static String format(Locale l, String format, Object... args); - @FormatMethod - public static String format(String format, Object... args); -} - -package java.io; - -class PrintStream { - @FormatMethod - public PrintStream format(Locale l, String format, Object... args); - @FormatMethod - public PrintStream format(String format, Object... args); - @FormatMethod - public PrintStream printf(Locale l, String format, Object... args); - @FormatMethod - public PrintStream printf(String format, Object... args); -} - -class PrintWriter { - @FormatMethod - public PrintWriter format(Locale l, String format, Object... args); - @FormatMethod - public PrintWriter format(String format, Object... args); - @FormatMethod - public PrintWriter printf(Locale l, String format, Object... args); - @FormatMethod - public PrintWriter printf(String format, Object... args); -} - -class Console { - @FormatMethod - public Console format(String format, Object... args); - @FormatMethod - public Console printf(String format, Object... args); -} diff --git a/checker/src/main/java/org/checkerframework/checker/guieffect/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/guieffect/jdk8.astub index be56551d37af..ae5ba18b5cc9 100644 --- a/checker/src/main/java/org/checkerframework/checker/guieffect/jdk8.astub +++ b/checker/src/main/java/org/checkerframework/checker/guieffect/jdk8.astub @@ -1,97 +1,4 @@ -package java.lang; -import org.checkerframework.checker.guieffect.qual.*; -@PolyUIType class Object { - @SafeEffect Class getClass(@PolyUI Object this) ; -} - -@PolyUIType interface Runnable { - @PolyUIEffect void run(@PolyUI Runnable this); -} - -// These types are polymorphic, but they're basically unusable unless I fix the subtyping among -// differently permissioned interfaces... -//package java.util; -//@PolyUIType interface Observer { -// @PolyUIEffect void update(@PolyUI Observer this, @PolyUI Observable o, Object arg); -//} -//@PolyUIType class Observable { -// @SafeEffect void addObserver(@PolyUI Observable this, @PolyUI Observer o); -// @SafeEffect void deleteObserver(@PolyUI Observable this, @PolyUI Observer o); -// @PolyUIEffect void notifyObservers(@PolyUI Observable this); -// @PolyUIEffect void notifyObservers(@PolyUI Observable this, Object arg); -//} - -@UIPackage -package java.awt; - -@UIType class Component implements ImageObserver, MenuContainer, Serializable { - @SafeEffect void repaint(); - @SafeEffect void repaint(long arg0); - @SafeEffect void repaint(int arg0, int arg1, int arg2, int arg3); - @SafeEffect void repaint(long arg0, int arg1, int arg2, int arg3, int arg4); -} -@UIType class Container extends Component { - @SafeEffect void invalidate(); -} - -class Desktop { - @SafeEffect void browse(URI uri); - @SafeEffect void edit(File file); - @SafeEffect static Desktop getDesktop(); - @SafeEffect static boolean isDesktopSupported(); - @SafeEffect boolean isSupported(Desktop.Action action); - @SafeEffect void mail(); - @SafeEffect void mail(URI mailtoURI); - @SafeEffect void open(File file); - @SafeEffect void print(File file); -} - -@UIType class EventQueue { - @SafeEffect void invokeLater(@UI Runnable arg0); -} - -package java.beans; -@PolyUIType public interface PropertyChangeListener extends EventListener { - @PolyUIEffect void propertyChange(@PolyUI PropertyChangeListener this, PropertyChangeEvent evt); -} -@PolyUIType public class PropertyChangeSupport implements Serializable { - @SafeEffect public PropertyChangeSupport(@PolyUI Object sourceBean); - @PolyUIEffect public void addPropertyChangeListener(@PolyUI PropertyChangeSupport this, @PolyUI PropertyChangeListener listener); - @PolyUIEffect public void removePropertyChangeListener(@PolyUI PropertyChangeSupport this, PropertyChangeListener listener); - @PolyUIEffect public @PolyUI PropertyChangeListener[] getPropertyChangeListeners(@PolyUI PropertyChangeSupport this); - @PolyUIEffect public void addPropertyChangeListener(@PolyUI PropertyChangeSupport this, String propertyName, @PolyUI PropertyChangeListener listener); - @PolyUIEffect public void removePropertyChangeListener(@PolyUI PropertyChangeSupport this, String propertyName, @PolyUI PropertyChangeListener listener); - @PolyUIEffect public @PolyUI PropertyChangeListener[] getPropertyChangeListeners(@PolyUI PropertyChangeSupport this, String propertyName); - @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, Object oldValue, Object newValue); - @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, int oldValue, int newValue); - @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, boolean oldValue, boolean newValue); - @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, PropertyChangeEvent event); - @PolyUIEffect public void fireIndexedPropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, - int index, - Object oldValue, - Object newValue); - @PolyUIEffect public void fireIndexedPropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, - int index, - int oldValue, - int newValue); - @PolyUIEffect public void fireIndexedPropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, - int index, - boolean oldValue, - boolean newValue); - @PolyUIEffect public boolean hasListeners(@PolyUI PropertyChangeSupport this, String propertyName); -} - - -@UIPackage -package java.awt.event; - -import org.checkerframework.checker.guieffect.qual.*; - -@UIType interface ActionListener extends EventListener { - @UIEffect void actionPerformed(ActionEvent e); -} - -@UIPackage package java.awt.dnd; +// This file is for classes that appear in JDK 8 but not in JDK 11. @UIPackage package javax.swing; diff --git a/checker/src/main/java/org/checkerframework/checker/i18n/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/i18n/jdk8.astub deleted file mode 100644 index 8014462e4bad..000000000000 --- a/checker/src/main/java/org/checkerframework/checker/i18n/jdk8.astub +++ /dev/null @@ -1,32 +0,0 @@ -import org.checkerframework.checker.i18n.qual.*; - -package java.util; - -class ResourceBundle { - @Localized Object getObject(@LocalizableKey String key); - @Localized String getString(@LocalizableKey String key); - @Localized String[] getStringArray(@LocalizableKey String key); - Set<@LocalizableKey String> keySet(); -} - -package java.awt; - -class Button { - @Localized String getLabel(); - void setLabel(@Localized String label); -} - -class CheckBox { - @Localized String getLabel(); - void setLabel(@Localized String label); -} - -package java.io; - -class PrintStream { - void println(@Localized String str); -} - -package javax.swing; - -// Lots of methods should be added to this stub file. diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/i18nformatter/jdk8.astub deleted file mode 100644 index dce125aa3f62..000000000000 --- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/jdk8.astub +++ /dev/null @@ -1,17 +0,0 @@ -import org.checkerframework.checker.i18nformatter.qual.*; - -package java.text; - -class MessageFormat { - - public static String format(@I18nFormatFor("#2") String arg0, Object... arg1); - -} - -package java.util; - -class ResourceBundle { - - @I18nMakeFormat - String getString(String key); -} diff --git a/checker/src/main/java/org/checkerframework/checker/interning/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/interning/jdk8.astub index de2be0e18bf2..f4d8b0397529 100644 --- a/checker/src/main/java/org/checkerframework/checker/interning/jdk8.astub +++ b/checker/src/main/java/org/checkerframework/checker/interning/jdk8.astub @@ -1,103 +1,7 @@ -import org.checkerframework.checker.interning.qual.*; - -// This file was generated by running the following commands: -// cd ~/java/jdk/src -// search -i -n '\bintern(|alized?|ed|ing)\b' -// search -n -n 'public static final String[^;]*"' -// and examining the search results. - -package java.io; - -public @UsesObjectEquals class ObjectStreamField - implements Comparable -{ - public @Interned String getTypeString(); -} - -package java.lang; - -// All instances of Class are interned. -@Interned class Class { - // In the Oracle JDK, the result of getName is interned - public @Interned String getName(); -} - -@UsesObjectEquals class ClassValue {} - -class String { - @Interned String intern(); -} - -class Boolean { - @Interned Boolean FALSE; - @Interned Boolean TRUE; - public static @Interned Boolean valueOf(String s); - public static @Interned Boolean valueOf(boolean b); -} - -class Byte { - public static @Interned Byte valueOf(byte b); - public static @Interned Byte valueOf(String s); - public static @Interned Byte valueOf(String s, int radix); -} - -class Character { - @Interned class UnicodeBlock { } -} - -@UsesObjectEquals class Thread implements Runnable {} - -package java.lang.reflect; - -class Field { - public @Interned String getName(); - public void set(Field this, Object obj, @Interned Object value); -} - -class Method { - public @Interned String getName(); -} +// This file is for classes that appear in JDK 8 but not in JDK 11. package java.util; -public final class Locale implements Cloneable, Serializable { - public @Interned String getCountry(); - public @Interned String getVariant(); -} - -public class Arrays{ - public static void sort(@PolyInterned Object[] a1); - public static void sort(@PolyInterned Object[] a1, int a2, int a3); - public static int binarySearch(@PolyInterned Object[] a1, @PolyInterned Object a2); - public static int binarySearch(@PolyInterned Object[] a1, int a2, int a3, @PolyInterned Object a4); - public static boolean equals(@PolyInterned Object [] a1, @PolyInterned Object [] a2); - public static void fill(@PolyInterned Object[] a1, @PolyInterned Object a2); - public static void fill(@PolyInterned Object[] a1, int a2, int a3, @PolyInterned Object a4); - public static int hashCode(@PolyInterned Object [] a1); - public static int deepHashCode(@PolyInterned Object [] a1); - public static boolean deepEquals(@PolyInterned Object [] a1, @PolyInterned Object [] a2); - public static String toString(@PolyInterned Object [] a1); - public static String deepToString(@PolyInterned Object [] a1); -} - -@UsesObjectEquals class ComparableTimSort {} -public final @UsesObjectEquals class Currency implements Serializable {} -final @UsesObjectEquals class DualPivotQuicksort {} -public abstract @UsesObjectEquals class EventListenerProxy - implements EventListener {} -public @UsesObjectEquals class EventObject implements java.io.Serializable {} -public @UsesObjectEquals class FormattableFlags {} -@UsesObjectEquals class LocaleISOData {} -public final @UsesObjectEquals class Objects {} -public @UsesObjectEquals class Observable {} -public @UsesObjectEquals class Random implements java.io.Serializable {} -public final @UsesObjectEquals class Scanner implements Iterator, Closeable {} -public final @UsesObjectEquals class ServiceLoader - implements Iterable {} -public @UsesObjectEquals class StringTokenizer implements Enumeration {} -@UsesObjectEquals class TimSort {} -public @UsesObjectEquals class Timer {} -public abstract @UsesObjectEquals class TimerTask implements Runnable {} @UsesObjectEquals class XMLUtils {} /* @@ -112,11 +16,6 @@ public class Attributes implements Map, Cloneable { } */ -package java.util.regex; - -@UsesObjectEquals class Pattern { -} - package javax.management; public class MBeanServerPermission extends BasicPermission { @@ -146,254 +45,6 @@ public class DefaultTableCellRenderer extends JLabel protected void firePropertyChange(@Interned String propertyName, Object oldValue, Object newValue); } -package java.awt.datatransfer; -public class DataFlavor { - public static final @Interned String javaSerializedObjectMimeType = "application/x-java-serialized-object"; - public static final @Interned String javaJVMLocalObjectMimeType = "application/x-java-jvm-local-objectref"; - public static final @Interned String javaRemoteObjectMimeType = "application/x-java-remote-object"; -} -package java.awt; -public @UsesObjectEquals class BorderLayout { - public static final @Interned String NORTH = "North"; - public static final @Interned String SOUTH = "South"; - public static final @Interned String EAST = "East"; - public static final @Interned String WEST = "West"; - public static final @Interned String CENTER = "Center"; - public static final @Interned String BEFORE_FIRST_LINE = "First"; - public static final @Interned String AFTER_LAST_LINE = "Last"; - public static final @Interned String BEFORE_LINE_BEGINS = "Before"; - public static final @Interned String AFTER_LINE_ENDS = "After"; -} -public class Font { - public static final @Interned String DIALOG = "Dialog"; - public static final @Interned String DIALOG_INPUT = "DialogInput"; - public static final @Interned String SANS_SERIF = "SansSerif"; - public static final @Interned String SERIF = "Serif"; - public static final @Interned String MONOSPACED = "Monospaced"; -} -public @UsesObjectEquals class GradientPaint implements Paint {} -public @UsesObjectEquals class AWTEventMulticaster implements - ComponentListener, ContainerListener, FocusListener, KeyListener, - MouseListener, MouseMotionListener, WindowListener, WindowFocusListener, - WindowStateListener, ActionListener, ItemListener, AdjustmentListener, - TextListener, InputMethodListener, HierarchyListener, - HierarchyBoundsListener, MouseWheelListener {} -abstract @UsesObjectEquals class AttributeValue {} -public @UsesObjectEquals class BufferCapabilities implements Cloneable {} -public @UsesObjectEquals class CardLayout implements LayoutManager2, - Serializable {} -public @UsesObjectEquals class CheckboxGroup implements java.io.Serializable {} -@UsesObjectEquals class ColorPaintContext implements PaintContext {} -public abstract @UsesObjectEquals class Component implements ImageObserver, MenuContainer, - Serializable {} -public final @UsesObjectEquals class ComponentOrientation implements java.io.Serializable {} -public @UsesObjectEquals class Cursor implements java.io.Serializable {} -public @UsesObjectEquals class Desktop {} -public @UsesObjectEquals class Event implements java.io.Serializable {} -public @UsesObjectEquals class EventQueue {} -public abstract @UsesObjectEquals class FocusTraversalPolicy {} -public abstract @UsesObjectEquals class FontMetrics implements java.io.Serializable {} -@UsesObjectEquals class GradientPaintContext implements PaintContext {} -public abstract @UsesObjectEquals class Graphics {} -public abstract @UsesObjectEquals class GraphicsConfigTemplate implements Serializable {} -public abstract @UsesObjectEquals class GraphicsConfiguration {} -public abstract @UsesObjectEquals class GraphicsDevice {} -public abstract @UsesObjectEquals class GraphicsEnvironment {} -public @UsesObjectEquals class GridBagConstraints implements Cloneable, java.io.Serializable {} -public @UsesObjectEquals class GridBagLayout implements LayoutManager2, -java.io.Serializable {} -public @UsesObjectEquals class GridBagLayoutInfo implements java.io.Serializable {} -public @UsesObjectEquals class GridLayout implements LayoutManager, java.io.Serializable {} -public abstract @UsesObjectEquals class Image {} -public @UsesObjectEquals class ImageCapabilities implements Cloneable {} -public abstract @UsesObjectEquals class KeyboardFocusManager - implements KeyEventDispatcher, KeyEventPostProcessor {} -public @UsesObjectEquals class MediaTracker implements java.io.Serializable {} -public abstract @UsesObjectEquals class MenuComponent implements java.io.Serializable {} -abstract @UsesObjectEquals class ModalEventFilter implements EventFilter {} -public @UsesObjectEquals class MouseInfo {} -public abstract @UsesObjectEquals class MultipleGradientPaint implements Paint {} -abstract @UsesObjectEquals class MultipleGradientPaintContext implements PaintContext {} -public @UsesObjectEquals class PointerInfo {} -public @UsesObjectEquals class Polygon implements Shape, java.io.Serializable {} -public abstract @UsesObjectEquals class PrintJob {} -public @UsesObjectEquals class Robot {} -public @UsesObjectEquals class ScrollPaneAdjustable implements Adjustable, Serializable {} -public final @UsesObjectEquals class SplashScreen {} -public @UsesObjectEquals class SystemTray {} -public @UsesObjectEquals class TexturePaint implements Paint {} -abstract @UsesObjectEquals class TexturePaintContext implements PaintContext {} -public @UsesObjectEquals class TrayIcon {} -public abstract @UsesObjectEquals class Toolkit {} -@UsesObjectEquals class WaitDispatchSupport implements SecondaryLoop {} -public abstract @UsesObjectEquals class Image {} - -package java.io; -public class File { - public static final @Interned String separator = "" + separatorChar; - public static final @Interned String pathSeparator = "" + pathSeparatorChar; -} -package java.util.jar; -public class JarFile { - public static final @Interned String MANIFEST_NAME = "META-INF/MANIFEST.MF"; -} -package java.util.logging; -public @UsesObjectEquals class Logger { - public static final @Interned String GLOBAL_LOGGER_NAME = "global"; -} -@Interned class Level { } -package javax.accessibility; -public class AccessibleAction { - public static final @Interned String CLICK = new String("click"); - public static final @Interned String TOGGLE_POPUP = new String("toggle popup"); -} -package javax.accessibility; -public class AccessibleContext { - public static final @Interned String ACCESSIBLE_NAME_PROPERTY = "AccessibleName"; - public static final @Interned String ACCESSIBLE_DESCRIPTION_PROPERTY = "AccessibleDescription"; - public static final @Interned String ACCESSIBLE_STATE_PROPERTY = "AccessibleState"; - public static final @Interned String ACCESSIBLE_VALUE_PROPERTY = "AccessibleValue"; - public static final @Interned String ACCESSIBLE_SELECTION_PROPERTY = "AccessibleSelection"; - public static final @Interned String ACCESSIBLE_CARET_PROPERTY = "AccessibleCaret"; - public static final @Interned String ACCESSIBLE_VISIBLE_DATA_PROPERTY = "AccessibleVisibleData"; - public static final @Interned String ACCESSIBLE_CHILD_PROPERTY = "AccessibleChild"; - public static final @Interned String ACCESSIBLE_ACTIVE_DESCENDANT_PROPERTY = "AccessibleActiveDescendant"; -} -package javax.accessibility; -public class AccessibleRelation { - public static final @Interned String LABEL_FOR = new String("labelFor"); - public static final @Interned String LABELED_BY = new String("labeledBy"); - public static final @Interned String MEMBER_OF = new String("memberOf"); - public static final @Interned String CONTROLLER_FOR = new String("controllerFor"); - public static final @Interned String CONTROLLED_BY = new String("controlledBy"); - public static final @Interned String FLOWS_TO = "flowsTo"; - public static final @Interned String FLOWS_FROM = "flowsFrom"; - public static final @Interned String SUBWINDOW_OF = "subwindowOf"; - public static final @Interned String PARENT_WINDOW_OF = "parentWindowOf"; - public static final @Interned String EMBEDS = "embeds"; - public static final @Interned String EMBEDDED_BY = "embeddedBy"; - public static final @Interned String CHILD_NODE_OF = "childNodeOf"; - public static final @Interned String LABEL_FOR_PROPERTY = "labelForProperty"; - public static final @Interned String LABELED_BY_PROPERTY = "labeledByProperty"; - public static final @Interned String MEMBER_OF_PROPERTY = "memberOfProperty"; - public static final @Interned String CONTROLLER_FOR_PROPERTY = "controllerForProperty"; - public static final @Interned String CONTROLLED_BY_PROPERTY = "controlledByProperty"; - public static final @Interned String FLOWS_TO_PROPERTY = "flowsToProperty"; - public static final @Interned String FLOWS_FROM_PROPERTY = "flowsFromProperty"; - public static final @Interned String SUBWINDOW_OF_PROPERTY = "subwindowOfProperty"; - public static final @Interned String PARENT_WINDOW_OF_PROPERTY = "parentWindowOfProperty"; - public static final @Interned String EMBEDS_PROPERTY = "embedsProperty"; - public static final @Interned String EMBEDDED_BY_PROPERTY = "embeddedByProperty"; - public static final @Interned String CHILD_NODE_OF_PROPERTY = "childNodeOfProperty"; -} -package javax.management.monitor; -public class MonitorNotification { - public static final @Interned String OBSERVED_OBJECT_ERROR = "jmx.monitor.error.mbean"; - public static final @Interned String OBSERVED_ATTRIBUTE_ERROR = "jmx.monitor.error.attribute"; - public static final @Interned String OBSERVED_ATTRIBUTE_TYPE_ERROR = "jmx.monitor.error.type"; - public static final @Interned String THRESHOLD_ERROR = "jmx.monitor.error.threshold"; - public static final @Interned String RUNTIME_ERROR = "jmx.monitor.error.runtime"; - public static final @Interned String THRESHOLD_VALUE_EXCEEDED = "jmx.monitor.counter.threshold"; - public static final @Interned String THRESHOLD_HIGH_VALUE_EXCEEDED = "jmx.monitor.gauge.high"; - public static final @Interned String THRESHOLD_LOW_VALUE_EXCEEDED = "jmx.monitor.gauge.low"; - public static final @Interned String STRING_TO_COMPARE_VALUE_MATCHED = "jmx.monitor.string.matches"; - public static final @Interned String STRING_TO_COMPARE_VALUE_DIFFERED = "jmx.monitor.string.differs"; -} -package javax.management.relation; -public class RelationNotification { - public static final @Interned String RELATION_BASIC_CREATION = "jmx.relation.creation.basic"; - public static final @Interned String RELATION_MBEAN_CREATION = "jmx.relation.creation.mbean"; - public static final @Interned String RELATION_BASIC_UPDATE = "jmx.relation.update.basic"; - public static final @Interned String RELATION_MBEAN_UPDATE = "jmx.relation.update.mbean"; - public static final @Interned String RELATION_BASIC_REMOVAL = "jmx.relation.removal.basic"; - public static final @Interned String RELATION_MBEAN_REMOVAL = "jmx.relation.removal.mbean"; -} -package javax.management.remote; -public class JMXConnectionNotification { - public static final @Interned String OPENED = "jmx.remote.connection.opened"; - public static final @Interned String CLOSED = "jmx.remote.connection.closed"; - public static final @Interned String FAILED = "jmx.remote.connection.failed"; -} -package javax.management; -public class AttributeChangeNotification { - public static final @Interned String ATTRIBUTE_CHANGE = "jmx.attribute.change"; -} -package javax.management; -public class JMX { - public static final @Interned String DEFAULT_VALUE_FIELD = "defaultValue"; - public static final @Interned String IMMUTABLE_INFO_FIELD = "immutableInfo"; - public static final @Interned String INTERFACE_CLASS_NAME_FIELD = "interfaceClassName"; - public static final @Interned String LEGAL_VALUES_FIELD = "legalValues"; - public static final @Interned String MAX_VALUE_FIELD = "maxValue"; - public static final @Interned String MIN_VALUE_FIELD = "minValue"; - public static final @Interned String MXBEAN_FIELD = "mxbean"; - public static final @Interned String OPEN_TYPE_FIELD = "openType"; - public static final @Interned String ORIGINAL_TYPE_FIELD = "originalType"; -} -package javax.naming.ldap; -public class ManageReferralControl { - public static final @Interned String OID = "2.16.840.1.113730.3.4.2"; -} -package javax.naming.ldap; -public class PagedResultsControl { - public static final @Interned String OID = "1.2.840.113556.1.4.319"; -} -package javax.naming.ldap; -public class PagedResultsResponseControl { - public static final @Interned String OID = "1.2.840.113556.1.4.319"; -} -package javax.naming.ldap; -public class SortControl { - public static final @Interned String OID = "1.2.840.113556.1.4.473"; -} -package javax.naming.ldap; -public class SortResponseControl { - public static final @Interned String OID = "1.2.840.113556.1.4.474"; -} -package javax.naming.ldap; -public class StartTlsRequest { - public static final @Interned String OID = "1.3.6.1.4.1.1466.20037"; -} -package javax.naming.ldap; -public class StartTlsResponse { - public static final @Interned String OID = "1.3.6.1.4.1.1466.20037"; -} -package javax.naming.spi; -public class NamingManager { - public static final @Interned String CPE = "java.naming.spi.CannotProceedException"; -} -package javax.print; -public class ServiceUIFactory { - public static final @Interned String JCOMPONENT_UI = "javax.swing.JComponent"; - public static final @Interned String PANEL_UI = "java.awt.Panel"; - public static final @Interned String DIALOG_UI = "java.awt.Dialog"; - public static final @Interned String JDIALOG_UI = "javax.swing.JDialog"; -} -package javax.script; -public class ScriptEngine { - public static final @Interned String ARGV="javax.script.argv"; - public static final @Interned String FILENAME = "javax.script.filename"; - public static final @Interned String ENGINE = "javax.script.engine"; - public static final @Interned String ENGINE_VERSION = "javax.script.engine_version"; - public static final @Interned String NAME = "javax.script.name"; - public static final @Interned String LANGUAGE = "javax.script.language"; - public static final @Interned String LANGUAGE_VERSION ="javax.script.language_version"; -} -package javax.security.auth.x500; -public class X500Principal { - public static final @Interned String RFC1779 = "RFC1779"; - public static final @Interned String RFC2253 = "RFC2253"; - public static final @Interned String CANONICAL = "CANONICAL"; -} -package javax.security.sasl; -public class Sasl { - public static final @Interned String QOP = "javax.security.sasl.qop"; - public static final @Interned String STRENGTH = "javax.security.sasl.strength"; - public static final @Interned String MAX_BUFFER = "javax.security.sasl.maxbuffer"; - public static final @Interned String RAW_SEND_SIZE = "javax.security.sasl.rawsendsize"; - public static final @Interned String REUSE = "javax.security.sasl.reuse"; - public static final @Interned String CREDENTIALS = "javax.security.sasl.credentials"; -} package javax.swing.plaf.basic; public class BasicHTML { public static final @Interned String propertyKey = "html"; @@ -652,487 +303,3 @@ public class SpringLayout { public static final @Interned String WIDTH = "Width"; public static final @Interned String HEIGHT = "Height"; } -package javax.xml.crypto.dsig.spec; -public class ExcC14NParameterSpec { - public static final @Interned String DEFAULT = "#default"; -} - -/////////////////////////////////////////////////////////////////////////// -/// End of: public static final @Interned String (initialized to constant) -/// - -package java.awt.color; - -public abstract @UsesObjectEquals class ColorSpace implements java.io.Serializable {} -public @UsesObjectEquals class ICC_Profile implements Serializable {} - -package java.awt.datatransfer; - -public @UsesObjectEquals class Clipboard {} -public @UsesObjectEquals class StringSelection implements Transferable, ClipboardOwner {} -public final @UsesObjectEquals class SystemFlavorMap implements FlavorMap, FlavorTable {} - -package java.awt.dnd; - -public final @UsesObjectEquals class DnDConstants {} -public abstract @UsesObjectEquals class DragGestureRecognizer implements Serializable {} -public @UsesObjectEquals class DragSource implements Serializable {} -public abstract @UsesObjectEquals class DragSourceAdapter - implements DragSourceListener, DragSourceMotionListener {} -public @UsesObjectEquals class DragSourceContext - implements DragSourceListener, DragSourceMotionListener, Serializable {} -public @UsesObjectEquals class DropTarget implements DropTargetListener, Serializable {} -public abstract @UsesObjectEquals class DropTargetAdapter implements DropTargetListener {} -public @UsesObjectEquals class DropTargetContext implements Serializable {} - -package java.awt.event; - -public abstract @UsesObjectEquals class ComponentAdapter implements ComponentListener {} -public abstract @UsesObjectEquals class ContainerAdapter implements ContainerListener {} -public abstract @UsesObjectEquals class FocusAdapter implements FocusListener {} -public abstract @UsesObjectEquals class HierarchyBoundsAdapter implements HierarchyBoundsListener {} -public abstract @UsesObjectEquals class KeyAdapter implements KeyListener {} -public abstract @UsesObjectEquals class MouseAdapter implements MouseListener, MouseWheelListener, MouseMotionListener {} -public abstract @UsesObjectEquals class MouseMotionAdapter implements MouseMotionListener {} -@UsesObjectEquals class NativeLibLoader {} -public abstract @UsesObjectEquals class WindowAdapter - implements WindowListener, WindowStateListener, WindowFocusListener {} - -package java.awt.font; - -@UsesObjectEquals class CharArrayIterator implements CharacterIterator {} -public final @UsesObjectEquals class GlyphJustificationInfo {} -public final @UsesObjectEquals class GlyphMetrics {} -public abstract @UsesObjectEquals class GlyphVector implements Cloneable {} -public abstract @UsesObjectEquals class LayoutPath {} -public final @UsesObjectEquals class LineBreakMeasurer {} -final @UsesObjectEquals class StyledParagraph {} -@UsesObjectEquals class TextJustifier {} -final @UsesObjectEquals class TextLine {} -public final @UsesObjectEquals class TextMeasurer implements Cloneable {} - -package java.awt.geom; - -@UsesObjectEquals class ArcIterator implements PathIterator {} -public abstract @UsesObjectEquals class CubicCurve2D implements Shape, Cloneable {} -@UsesObjectEquals class CubicIterator implements PathIterator {} -@UsesObjectEquals class EllipseIterator implements PathIterator {} -public @UsesObjectEquals class FlatteningPathIterator implements PathIterator {} -public abstract @UsesObjectEquals class Line2D implements Shape, Cloneable {} -public abstract @UsesObjectEquals class Path2D implements Shape, Cloneable {} -@UsesObjectEquals class LineIterator implements PathIterator {} -public abstract @UsesObjectEquals class QuadCurve2D implements Shape, Cloneable {} -@UsesObjectEquals class QuadIterator implements PathIterator {} -@UsesObjectEquals class RectIterator implements PathIterator {} -@UsesObjectEquals class RoundRectIterator implements PathIterator {} - -package java.awt.im; - -public @UsesObjectEquals class InputContext {} -public @UsesObjectEquals class InputMethodHighlight {} - -package java.awt.image; - -public @UsesObjectEquals class AffineTransformOp implements BufferedImageOp, RasterOp {} -public @UsesObjectEquals class BandCombineOp implements RasterOp {} -public abstract @UsesObjectEquals class BufferStrategy {} -public @UsesObjectEquals class ColorConvertOp implements BufferedImageOp, RasterOp {} -public @UsesObjectEquals class ConvolveOp implements BufferedImageOp, RasterOp {} -public abstract @UsesObjectEquals class DataBuffer {} -public @UsesObjectEquals class FilteredImageSource implements ImageProducer {} -public @UsesObjectEquals class ImageFilter implements ImageConsumer, Cloneable {} -public @UsesObjectEquals class Kernel implements Cloneable {} -public @UsesObjectEquals class LookupOp implements BufferedImageOp, RasterOp {} -public abstract @UsesObjectEquals class LookupTable extends Object{} -public @UsesObjectEquals class MemoryImageSource implements ImageProducer {} -public @UsesObjectEquals class PixelGrabber implements ImageConsumer {} -public @UsesObjectEquals class Raster {} -public @UsesObjectEquals class RescaleOp implements BufferedImageOp, RasterOp {} - -package java.awt.image.renderable; - -public @UsesObjectEquals class ParameterBlock implements Cloneable, Serializable {} -public @UsesObjectEquals class RenderContext implements Cloneable {} -public @UsesObjectEquals class RenderableImageOp implements RenderableImage {} -public @UsesObjectEquals class RenderableImageProducer implements ImageProducer, Runnable {} - -package java.awt.print; - -public @UsesObjectEquals class Book implements Pageable {} -public @UsesObjectEquals class PageFormat implements Cloneable {} -public @UsesObjectEquals class Paper implements Cloneable {} -public abstract @UsesObjectEquals class PrinterJob {} - -package java.beans; - -public @UsesObjectEquals class Beans {} -abstract @UsesObjectEquals class ChangeListenerMap {} -public @UsesObjectEquals class Encoder {} -public @UsesObjectEquals class EventHandler implements InvocationHandler {} -public @UsesObjectEquals class FeatureDescriptor {} -public @UsesObjectEquals class Introspector {} -@UsesObjectEquals class NameGenerator {} -public abstract @UsesObjectEquals class PersistenceDelegate {} -public @UsesObjectEquals class PropertyChangeSupport implements Serializable {} -public @UsesObjectEquals class PropertyEditorSupport implements PropertyEditor {} -public @UsesObjectEquals class SimpleBeanInfo implements BeanInfo {} -public @UsesObjectEquals class Statement {} -public @UsesObjectEquals class VetoableChangeSupport implements Serializable {} -public @UsesObjectEquals class XMLDecoder implements AutoCloseable {} - -package java.beans.beancontext; - -public @UsesObjectEquals class BeanContextChildSupport implements BeanContextChild, BeanContextServicesListener, Serializable {} - -package java.lang.invoke; - -abstract public @UsesObjectEquals class CallSite {} -final @UsesObjectEquals class InvokeDynamic {} -// public @UsesObjectEquals class Linkage {} -public abstract @UsesObjectEquals class MethodHandleImpl {} -public @UsesObjectEquals class MethodHandles {} -public @UsesObjectEquals class SwitchPoint {} - -package java.io; - -@UsesObjectEquals class Bits {} -public final @UsesObjectEquals class Console implements Flushable {} -@UsesObjectEquals class DeleteOnExitHook {} -@UsesObjectEquals class ExpiringCache {} -abstract @UsesObjectEquals class FileSystem {} -// Defined above -// public @UsesObjectEquals class ObjectStreamField -// implements Comparable -// {} -public abstract @UsesObjectEquals class OutputStream implements Closeable, Flushable {} -public @UsesObjectEquals class RandomAccessFile implements DataOutput, DataInput, Closeable {} -public abstract @UsesObjectEquals class Reader implements Readable, Closeable {} -final @UsesObjectEquals class SerialCallbackContext {} -public @UsesObjectEquals class StreamTokenizer {} -public abstract @UsesObjectEquals class Writer implements Appendable, Closeable, Flushable {} - -package java.lang; - -abstract @UsesObjectEquals class AbstractStringBuilder implements Appendable, CharSequence {} -@UsesObjectEquals class ApplicationShutdownHooks {} -@UsesObjectEquals class AssertionStatusDirectives {} -abstract @UsesObjectEquals class CharacterData {} -@UsesObjectEquals class CharacterName {} -public abstract @UsesObjectEquals class ClassLoader {} -public final @UsesObjectEquals class Compiler {} -final @UsesObjectEquals class ConditionalSpecialCasing {} -public final @UsesObjectEquals class Math {} -public @UsesObjectEquals class Package implements java.lang.reflect.AnnotatedElement {} -public abstract @UsesObjectEquals class Process {} -public @UsesObjectEquals class Runtime {} -public @UsesObjectEquals class SecurityManager {} -@UsesObjectEquals class Shutdown {} -public final @UsesObjectEquals class StrictMath {} -@UsesObjectEquals class StringCoding {} -public final @UsesObjectEquals class System {} -public @UsesObjectEquals class ThreadGroup implements Thread.UncaughtExceptionHandler {} -public @UsesObjectEquals class ThreadLocal {} -public @UsesObjectEquals class Throwable implements Serializable {} -public final -@UsesObjectEquals class Void {} - -package java.lang.instrument; - -public final @UsesObjectEquals class ClassDefinition {} - -package java.lang.management; - -public @UsesObjectEquals class LockInfo {} -public @UsesObjectEquals class ManagementFactory {} -public @UsesObjectEquals class MemoryNotificationInfo {} -public @UsesObjectEquals class MemoryUsage {} -public @UsesObjectEquals class ThreadInfo {} - -package java.lang.ref; - -public @UsesObjectEquals class ReferenceQueue {} - -package java.lang.reflect; - -public final -@UsesObjectEquals class Array {} -public @UsesObjectEquals class Modifier {} -@UsesObjectEquals class ReflectAccess implements sun.reflect.LangReflectAccess {} - -package java.math; - -@UsesObjectEquals class BitSieve {} -@UsesObjectEquals class MutableBigInteger {} - -package java.net; - -public abstract -@UsesObjectEquals class Authenticator {} -public abstract @UsesObjectEquals class CacheRequest {} -public abstract @UsesObjectEquals class CacheResponse {} -abstract public @UsesObjectEquals class ContentHandler {} -public abstract @UsesObjectEquals class CookieHandler {} -public final -@UsesObjectEquals class DatagramPacket {} -public @UsesObjectEquals class DatagramSocket implements java.io.Closeable {} -public abstract @UsesObjectEquals class DatagramSocketImpl implements SocketOptions {} -public final @UsesObjectEquals class IDN {} -@UsesObjectEquals class InMemoryCookieStore implements CookieStore {} -@UsesObjectEquals class Inet4AddressImpl implements InetAddressImpl {} -@UsesObjectEquals class Inet6AddressImpl implements InetAddressImpl {} -public final @UsesObjectEquals class PasswordAuthentication {} -public abstract @UsesObjectEquals class ProxySelector {} -public abstract @UsesObjectEquals class ResponseCache {} -public @UsesObjectEquals class ServerSocket implements java.io.Closeable {} -public @UsesObjectEquals class Socket implements java.io.Closeable {} -public abstract @UsesObjectEquals class SocketImpl implements SocketOptions {} -public final @UsesObjectEquals class StandardSocketOption {} -public @UsesObjectEquals class URLDecoder {} -public @UsesObjectEquals class URLEncoder {} -public abstract @UsesObjectEquals class URLStreamHandler {} - -package java.nio; - -@UsesObjectEquals class Bits {} -public final @UsesObjectEquals class ByteOrder {} - -package java.nio.channels; - -public abstract @UsesObjectEquals class AsynchronousChannelGroup {} -public abstract @UsesObjectEquals class AsynchronousFileChannel - implements AsynchronousChannel {} -public abstract @UsesObjectEquals class AsynchronousServerSocketChannel - implements AsynchronousChannel, NetworkChannel {} -public abstract @UsesObjectEquals class AsynchronousSocketChannel - implements AsynchronousByteChannel, NetworkChannel {} -public final @UsesObjectEquals class Channels {} -public abstract @UsesObjectEquals class FileLock implements AutoCloseable {} -public abstract @UsesObjectEquals class MembershipKey {} -public abstract @UsesObjectEquals class Pipe {} -public abstract @UsesObjectEquals class SelectionKey {} -public abstract @UsesObjectEquals class Selector implements Closeable {} - -package java.nio.channels.spi; - -public abstract @UsesObjectEquals class AbstractInterruptibleChannel - implements Channel, InterruptibleChannel {} -public abstract @UsesObjectEquals class AsynchronousChannelProvider {} -public abstract @UsesObjectEquals class SelectorProvider {} - -package java.nio.charset; - -public @UsesObjectEquals class CoderResult {} -public @UsesObjectEquals class CodingErrorAction {} - -package java.nio.charset.spi; - -public abstract @UsesObjectEquals class CharsetProvider {} - -package java.nio.file; - -@UsesObjectEquals class CopyMoveHelper {} -public abstract @UsesObjectEquals class FileStore {} -public abstract @UsesObjectEquals class FileSystem - implements Closeable {} -public final @UsesObjectEquals class FileSystems {} -@UsesObjectEquals class FileTreeWalker {} -public final @UsesObjectEquals class Files {} -public final @UsesObjectEquals class Paths {} -public @UsesObjectEquals class SimpleFileVisitor implements FileVisitor {} -public final @UsesObjectEquals class StandardWatchEventKinds {} -@UsesObjectEquals class TempFileHelper {} - -package java.nio.file.attribute; - -public final @UsesObjectEquals class PosixFilePermissions {} -public abstract @UsesObjectEquals class UserPrincipalLookupService {} - -package java.nio.file.spi; - -public abstract @UsesObjectEquals class FileSystemProvider {} -public abstract @UsesObjectEquals class FileTypeDetector {} - -package java.rmi; - -public final @UsesObjectEquals class Naming {} - -package java.rmi.dgc; - -public final @UsesObjectEquals class Lease implements java.io.Serializable {} - -package java.rmi.registry; - -public final @UsesObjectEquals class LocateRegistry {} - -package java.rmi.server; - -public @UsesObjectEquals class RMIClassLoader {} -public abstract @UsesObjectEquals class RMIClassLoaderSpi {} -public abstract @UsesObjectEquals class RMISocketFactory - implements RMIClientSocketFactory, RMIServerSocketFactory {} - -package java.security; - -public final @UsesObjectEquals class AccessController {} -public @UsesObjectEquals class AlgorithmParameterGenerator {} -public abstract @UsesObjectEquals class AlgorithmParameterGeneratorSpi {} -public @UsesObjectEquals class AlgorithmParameters {} -public abstract @UsesObjectEquals class AlgorithmParametersSpi {} -public @UsesObjectEquals class GuardedObject implements java.io.Serializable {} -public @UsesObjectEquals class KeyFactory {} -public abstract @UsesObjectEquals class KeyFactorySpi {} -public final @UsesObjectEquals class KeyPair implements java.io.Serializable {} -public abstract @UsesObjectEquals class KeyPairGeneratorSpi {} -public @UsesObjectEquals class KeyRep implements Serializable {} -public @UsesObjectEquals class KeyStore {} -public abstract @UsesObjectEquals class KeyStoreSpi {} -public abstract @UsesObjectEquals class MessageDigestSpi {} -public abstract @UsesObjectEquals class PermissionCollection implements java.io.Serializable {} -public abstract @UsesObjectEquals class Policy {} -public abstract @UsesObjectEquals class PolicySpi {} -public @UsesObjectEquals class ProtectionDomain {} -public abstract @UsesObjectEquals class SecureRandomSpi implements java.io.Serializable {} -public final @UsesObjectEquals class Security {} -public abstract @UsesObjectEquals class SignatureSpi {} -public final @UsesObjectEquals class SignedObject implements Serializable {} -public @UsesObjectEquals class URIParameter implements - Policy.Parameters, javax.security.auth.login.Configuration.Parameters {} - -package java.security.cert; - -public @UsesObjectEquals class CertPathBuilder {} -public abstract @UsesObjectEquals class CertPathBuilderSpi {} -public abstract @UsesObjectEquals class CertPathHelper {} -public @UsesObjectEquals class CertPathValidator {} -public abstract @UsesObjectEquals class CertPathValidatorSpi {} -public @UsesObjectEquals class CertStore {} -public @UsesObjectEquals class CertificateFactory {} -public abstract @UsesObjectEquals class CertificateFactorySpi {} -public @UsesObjectEquals class CollectionCertStoreParameters - implements CertStoreParameters {} -public abstract @UsesObjectEquals class PKIXCertPathChecker implements Cloneable {} -public @UsesObjectEquals class PKIXCertPathValidatorResult implements CertPathValidatorResult {} -public @UsesObjectEquals class PKIXParameters implements CertPathParameters {} -public @UsesObjectEquals class PolicyQualifierInfo {} -public @UsesObjectEquals class TrustAnchor {} -public @UsesObjectEquals class X509CRLSelector implements CRLSelector {} -public @UsesObjectEquals class X509CertSelector implements CertSelector {} - -package java.security.spec; - -public @UsesObjectEquals class DSAParameterSpec implements AlgorithmParameterSpec, -java.security.interfaces.DSAParams {} -public @UsesObjectEquals class DSAPrivateKeySpec implements KeySpec {} -public @UsesObjectEquals class DSAPublicKeySpec implements KeySpec {} -public @UsesObjectEquals class ECGenParameterSpec implements AlgorithmParameterSpec {} -public @UsesObjectEquals class ECParameterSpec implements AlgorithmParameterSpec {} -public @UsesObjectEquals class ECPrivateKeySpec implements KeySpec {} -public @UsesObjectEquals class ECPublicKeySpec implements KeySpec {} -public abstract @UsesObjectEquals class EncodedKeySpec implements KeySpec {} -public @UsesObjectEquals class MGF1ParameterSpec implements AlgorithmParameterSpec {} -public @UsesObjectEquals class PSSParameterSpec implements AlgorithmParameterSpec {} -public @UsesObjectEquals class RSAKeyGenParameterSpec implements AlgorithmParameterSpec {} -public @UsesObjectEquals class RSAOtherPrimeInfo {} -public @UsesObjectEquals class RSAPrivateKeySpec implements KeySpec {} -public @UsesObjectEquals class RSAPublicKeySpec implements KeySpec {} - -package java.sql; - -public @UsesObjectEquals class DriverManager {} -public @UsesObjectEquals class DriverPropertyInfo {} -public @UsesObjectEquals class Types {} - -package java.text; - -public @UsesObjectEquals class Annotation {} -public final @UsesObjectEquals class Bidi {} -@UsesObjectEquals class BreakDictionary {} -@UsesObjectEquals class CalendarBuilder {} -@UsesObjectEquals class CharacterIteratorFieldDelegate implements Format.FieldDelegate {} -public final @UsesObjectEquals class CollationElementIterator {} -final @UsesObjectEquals class CollationRules {} -final @UsesObjectEquals class EntryPair {} -final @UsesObjectEquals class MergeCollation {} -public final @UsesObjectEquals class Normalizer {} -final @UsesObjectEquals class RBCollationTables {} -final @UsesObjectEquals class RBTableBuilder {} - -package java.util.concurrent; - -public abstract @UsesObjectEquals class AbstractExecutorService implements ExecutorService {} -public @UsesObjectEquals class CountDownLatch {} -public @UsesObjectEquals class CyclicBarrier {} -public @UsesObjectEquals class Exchanger {} -public @UsesObjectEquals class ExecutorCompletionService implements CompletionService {} -public @UsesObjectEquals class Executors {} -public abstract @UsesObjectEquals class ForkJoinTask implements Future, Serializable {} -public @UsesObjectEquals class FutureTask implements RunnableFuture {} -public @UsesObjectEquals class Phaser {} - -package java.util.concurrent.atomic; - -public @UsesObjectEquals class AtomicBoolean implements java.io.Serializable {} -public @UsesObjectEquals class AtomicIntegerArray implements java.io.Serializable {} -public abstract @UsesObjectEquals class AtomicIntegerFieldUpdater {} -public @UsesObjectEquals class AtomicLongArray implements java.io.Serializable {} -public abstract @UsesObjectEquals class AtomicLongFieldUpdater {} -public @UsesObjectEquals class AtomicMarkableReference {} -public @UsesObjectEquals class AtomicReference implements java.io.Serializable {} -public @UsesObjectEquals class AtomicReferenceArray implements java.io.Serializable {} -public abstract @UsesObjectEquals class AtomicReferenceFieldUpdater {} - -package java.util.concurrent.locks; - -public abstract @UsesObjectEquals class AbstractOwnableSynchronizer - implements java.io.Serializable {} -public @UsesObjectEquals class LockSupport {} - -package java.util.jar; - -@UsesObjectEquals class JavaUtilJarAccessImpl implements JavaUtilJarAccess {} - -package java.util.logging; - -public @UsesObjectEquals class ErrorManager {} -public abstract @UsesObjectEquals class Formatter {} -public abstract @UsesObjectEquals class Handler {} -public @UsesObjectEquals class LogManager {} -public @UsesObjectEquals class LogRecord implements java.io.Serializable {} -// Defined above -// public @UsesObjectEquals class Logger {} -@UsesObjectEquals class Logging implements LoggingMXBean {} -// Commented out because LoggingProxy is in package sun.util.logging, and -// we don't want references to sun.* classes here. (LoggingProxyImpl isn't -// a public class anyway.) -// @UsesObjectEquals class LoggingProxyImpl implements LoggingProxy {} - -package java.util.prefs; - -@UsesObjectEquals class Base64 {} -public abstract @UsesObjectEquals class Preferences {} -@UsesObjectEquals class XmlSupport {} - -package java.util.regex; - -final @UsesObjectEquals class ASCII {} -public final @UsesObjectEquals class Matcher implements MatchResult {} -// Defined above -// public final @UsesObjectEquals class Pattern -// implements java.io.Serializable -// {} - -package java.util.spi; - -public abstract @UsesObjectEquals class LocaleServiceProvider {} - -package java.util.zip; - -public @UsesObjectEquals class Adler32 implements Checksum {} -public @UsesObjectEquals class CRC32 implements Checksum {} -public @UsesObjectEquals class Deflater {} -public @UsesObjectEquals class Inflater {} -@UsesObjectEquals class ZStreamRef {} -final @UsesObjectEquals class ZipCoder {} -@UsesObjectEquals class ZipConstants64 {} -public @UsesObjectEquals class ZipEntry implements ZipConstants, Cloneable {} -public @UsesObjectEquals class ZipFile implements ZipConstants, Closeable {} diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForPropagator.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForPropagator.java index 7157351e5df2..f22bf7fd6087 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForPropagator.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForPropagator.java @@ -13,7 +13,7 @@ import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; -import org.checkerframework.framework.type.visitor.AnnotatedTypeReplacer; +import org.checkerframework.framework.type.AnnotatedTypeReplacer; import org.checkerframework.framework.util.TypeArgumentMapper; import org.checkerframework.framework.util.typeinference.TypeArgInferenceUtil; import org.checkerframework.javacutil.AnnotationBuilder; diff --git a/checker/src/main/java/org/checkerframework/checker/propkey/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/propkey/jdk8.astub deleted file mode 100644 index 7bfe03385ed3..000000000000 --- a/checker/src/main/java/org/checkerframework/checker/propkey/jdk8.astub +++ /dev/null @@ -1,16 +0,0 @@ -import org.checkerframework.checker.propkey.qual.*; - -package java.util; - -class Properties { - String getProperty(@PropertyKey String key); - String getProperty(@PropertyKey String key, String defaultValue); - Object setProperty(@PropertyKey String key, String value); -} - -class ResourceBundle { - Object getObject(@PropertyKey String key); - String getString(@PropertyKey String key); - String[] getStringArray(@PropertyKey String key); - Set<@PropertyKey String> keySet(); -} diff --git a/checker/src/main/java/org/checkerframework/checker/regex/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/regex/jdk8.astub index fd87ccc601f6..0570ebad1ca4 100644 --- a/checker/src/main/java/org/checkerframework/checker/regex/jdk8.astub +++ b/checker/src/main/java/org/checkerframework/checker/regex/jdk8.astub @@ -1,26 +1,6 @@ -import org.checkerframework.checker.regex.qual.*; - -package java.util.regex; - -class Pattern { - @Regex Pattern compile(@Regex String regex); - Pattern compile(@Regex String regex, int flags); - boolean matches(@Regex String regex, CharSequence input); - @PolyRegex Matcher matcher(@PolyRegex Pattern this, CharSequence input); - public static @Regex String quote(String s); -} +// This file is for classes that appear in JDK 8 but not in JDK 11. -package java.lang; - -class String { - public @PolyRegex String intern(@PolyRegex String this); - public boolean matches(@Regex String regex); - public String replaceFirst(@Regex String regex, String replacement); - public String replaceAll(@Regex String regex, String replacement); - public String[] split(@Regex String regex, int limit); - public String[] split(@Regex String regex); - public @PolyRegex String toString(@PolyRegex String this); -} +import org.checkerframework.checker.regex.qual.*; package javax.swing.plaf.synth; diff --git a/checker/src/main/java/org/checkerframework/checker/signature/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/signature/jdk8.astub index 914bd920ef26..c903cf458125 100644 --- a/checker/src/main/java/org/checkerframework/checker/signature/jdk8.astub +++ b/checker/src/main/java/org/checkerframework/checker/signature/jdk8.astub @@ -1,77 +1,6 @@ -import org.checkerframework.checker.signature.qual.*; - -package java.lang; - -class Class implements Serializable, GenericDeclaration, Type, AnnotatedElement { - Class forName(@ClassGetName String className) throws ClassNotFoundException; - Class forName(@ClassGetName String name, boolean initialize, ClassLoader loader) throws ClassNotFoundException; - @ClassGetName String getName(); - @ClassGetName String name; - @ClassGetName String getName0(); - @DotSeparatedIdentifiers String getPackageName(); - @ClassGetSimpleName String getSimpleName(); - @FullyQualifiedName String getCanonicalName(); -} - -class ClassLoader { - protected Class loadClass(@BinaryName String name, boolean resolve) throws ClassNotFoundException; - Class loadClass(@BinaryName String name) throws ClassNotFoundException; - protected Class findClass(@BinaryName String name) throws ClassNotFoundException; - @SuppressWarnings("signature") - protected Class defineClass(byte[] b, int off, int len) throws ClassFormatError; - protected Class defineClass(@BinaryName String name, byte[] b, int off, int len) throws ClassFormatError; - protected Class defineClass(@BinaryName String name, byte[] b, int off, int len, ProtectionDomain protectionDomain) throws ClassFormatError; - protected Class defineClass(@BinaryName String name, ByteBuffer b, ProtectionDomain protectionDomain) throws ClassFormatError; - protected Class findSystemClass(@BinaryName String name) throws ClassNotFoundException; - protected Class findLoadedClass(@BinaryName String name); - protected Package definePackage(@FullyQualifiedName String name, String specTitle, String specVersion, String specVendor, String implTitle, String implVersion, String implVendor, URL sealBase) throws IllegalArgumentException; - - class SystemClassLoaderAction implements PrivilegedExceptionAction { - public ClassLoader run() throws Exception { - @SuppressWarnings("signature") - @BinaryName String cls = System.getProperty("java.system.class.loader"); - if (cls == null) { - return parent; - } +// This file is for classes that appear in JDK 8 but not in JDK 11. - Constructor ctor = Class.forName(cls, true, parent) - .getDeclaredConstructor(new Class[] { ClassLoader.class }); - ClassLoader sys = (ClassLoader) ctor.newInstance( - new Object[] { parent }); - Thread.currentThread().setContextClassLoader(sys); - return sys; - } - } -} - -class Package implements AnnotatedElement { - Package(@DotSeparatedIdentifiers String name, String spectitle, String specversion, String specvendor, String impltitle, String implversion, String implvendor, URL sealbase, ClassLoader loader); - @DotSeparatedIdentifiers String getName(); -} - -class StackTraceElement { - public StackTraceElement(@FullyQualifiedName String declaringClass, String methodName, String fileName, int lineNumber); - public @FullyQualifiedName String getClassName(); -} - -class String { - public @PolySignature String intern(@PolySignature String this); -} - -class TypeNotPresentException extends RuntimeException { - public TypeNotPresentException(@FullyQualifiedName String typeName, Throwable cause); - public @FullyQualifiedName String typeName(); -} - -package java.lang.instrument; - -class ClassFileTransformer { - byte[] transform(ClassLoader loader, - @InternalForm String className, - Class classBeingRedefined, - ProtectionDomain protectionDomain, - byte[] classfileBuffer); -} +import org.checkerframework.checker.signature.qual.*; package java.lang.management; @@ -222,283 +151,9 @@ enum PlatformComponent { @BinaryName String getMXBeanInterfaceName(); } -public class MonitorInfo extends LockInfo { - public MonitorInfo(@BinaryName String className, int identityHashCode, int stackDepth, StackTraceElement stackFrame); - public static MonitorInfo from(CompositeData cd) { - if (cd == null) { - return null; - } - - if (cd instanceof MonitorInfoCompositeData) { - return ((MonitorInfoCompositeData) cd).getMonitorInfo(); - } else { - MonitorInfoCompositeData.validateCompositeData(cd); - /* This might be a potentially bug! I have put the annotation so that everything compiles - however, there is no information in the documentation of MonitorInfoCompositeData - class that getClassName returns a @FullyQualifiedName. */ - // @SuppressWarnings("signature") - /* This comes from sun.management, so I presume it is true. */ - @SuppressWarnings("signature") - @BinaryName String className = MonitorInfoCompositeData.getClassName(cd); - int identityHashCode = MonitorInfoCompositeData.getIdentityHashCode(cd); - int stackDepth = MonitorInfoCompositeData.getLockedStackDepth(cd); - StackTraceElement stackFrame = MonitorInfoCompositeData.getLockedStackFrame(cd); - return new MonitorInfo(className, - identityHashCode, - stackDepth, - stackFrame); - } - } -} - -public class LockInfo { - public LockInfo(@ClassGetName String className, int identityHashCode); - public @ClassGetName String getClassName(); -} - package java.util; -class ResourceBundle { - - ResourceBundle getBundle(@BinaryName String baseName); - ResourceBundle getBundle(@BinaryName String baseName, Control control); - ResourceBundle getBundle(@BinaryName String baseName, Locale locale); - ResourceBundle getBundle(@BinaryName String baseName, Locale targetLocale, Control control); - ResourceBundle getBundle(@BinaryName String baseName, Locale locale, ClassLoader loader); - ResourceBundle getBundle(@BinaryName String baseName, Locale targetLocale, ClassLoader loader, Control control); - - class Control { - public @BinaryName String toBundleName(@BinaryName String baseName, Locale locale) { - if (locale == Locale.ROOT) { - return baseName; - } - - String language = locale.getLanguage(); - String country = locale.getCountry(); - String variant = locale.getVariant(); - - if (language == "" && country == "" && variant == "") { - return baseName; - } - - StringBuilder sb = new StringBuilder(baseName); - sb.append('_'); - if (variant != "") { - sb.append(language).append('_').append(country).append('_').append(variant); - } else if (country != "") { - sb.append(language).append('_').append(country); - } else { - sb.append(language); - } - /* I have to do this to bypass the annotation of toString() method of - StringBuilder (which would be wrong). */ - @SuppressWarnings("signature") - @BinaryName String result = sb.toString(); - return result; - - } - - public ResourceBundle newBundle(@BinaryName String baseName, Locale locale, String format, ClassLoader loader, boolean reload) throws IllegalAccessException, InstantiationException, IOException; - public boolean needsReload(@BinaryName String baseName, Locale locale, String format, ClassLoader loader, ResourceBundle bundle, long loadTime); - } -} - class SecurityManager { protected int classDepth(@FullyQualifiedName String name); protected boolean inClass(@FullyQualifiedName String name); } - -package java.util.logging; - -class Level implements Serializable { - @SuppressWarnings("signature") - protected Level(String name, int value); - protected Level(String name, int value, @BinaryName String resourceBundleName); - @BinaryName String getResourceBundleName(); -} - -class Logger { - - public static Logger getAnonymousLogger() { - /* I have to de it to permit null as binary name. */ - @SuppressWarnings("signature") - @BinaryName String temp = null; - return getAnonymousLogger(temp); - } - - protected Logger(String name, @BinaryName String resourceBundleName); - Logger getLogger(String name, @BinaryName String resourceBundleName); - Logger getAnonymousLogger(@BinaryName String resourceBundleName); - @BinaryName String getResourceBundleName(); - void logrb(Level level, String sourceClass, String sourceMethod, @BinaryName String bundleName, String msg); - void logrb(Level level, String sourceClass, String sourceMethod, @BinaryName String bundleName, String msg, Object param1); - void logrb(Level level, String sourceClass, String sourceMethod, @BinaryName String bundleName, String msg, Object[] params); - void logrb(Level level, String sourceClass, String sourceMethod, @BinaryName String bundleName, String msg, Throwable thrown); -} - -class LogManager { - - static { - AccessController.doPrivileged(new PrivilegedAction() { - public Object run() { - @SuppressWarnings("signature") - @BinaryName String cname = null; - try { - @SuppressWarnings("signature") - @BinaryName String temp = System.getProperty("java.util.logging.manager"); - cname = temp; - if (cname != null) { - try { - Class clz = ClassLoader.getSystemClassLoader().loadClass(cname); - manager = (LogManager) clz.newInstance(); - } catch (ClassNotFoundException ex) { - Class clz = Thread.currentThread().getContextClassLoader().loadClass(cname); - manager = (LogManager) clz.newInstance(); - } - } - } catch (Exception ex) { - System.err.println("Could not load Logmanager \"" + cname + "\""); - ex.printStackTrace(); - } - if (manager == null) { - manager = new LogManager(); - } - - // Create and retain Logger for the root of the namespace. - manager.rootLogger = manager.new RootLogger(); - manager.addLogger(manager.rootLogger); - - // Adding the global Logger. Doing so in the Logger. - // would deadlock with the LogManager.. - Logger.global.setLogManager(manager); - manager.addLogger(Logger.global); - - // We don't call readConfiguration() here, as we may be running - // very early in the JVM startup sequence. Instead readConfiguration - // will be called lazily in getLogManager(). - return null; - } - }); - } - - @SuppressWarnings("signature") - Logger demandLogger(String name); - - public void readConfiguration() throws IOException, SecurityException { - checkAccess(); - - // if a configuration class is specified, load it and use it. - @SuppressWarnings("signature") - @BinaryName String cname = System.getProperty("java.util.logging.config.class"); - if (cname != null) { - try { - // Instantiate the named class. It is its constructor's - // responsibility to initialize the logging configuration, by - // calling readConfiguration(InputStream) with a suitable stream. - try { - Class clz = ClassLoader.getSystemClassLoader().loadClass(cname); - clz.newInstance(); - return; - } catch (ClassNotFoundException ex) { - Class clz = Thread.currentThread().getContextClassLoader().loadClass(cname); - clz.newInstance(); - return; - } - } catch (Exception ex) { - System.err.println("Logging configuration class \"" + cname + "\" failed"); - System.err.println("" + ex); - // keep going and useful config file. - } - } - - String fname = System.getProperty("java.util.logging.config.file"); - if (fname == null) { - fname = System.getProperty("java.home"); - if (fname == null) { - throw new Error("Can't find java.home ??"); - } - File f = new File(fname, "lib"); - f = new File(f, "logging.properties"); - fname = f.getCanonicalPath(); - } - InputStream in = new FileInputStream(fname); - BufferedInputStream bin = new BufferedInputStream(in); - try { - readConfiguration(bin); - } finally { - if (in != null) { - in.close(); - } - } - } - - public void readConfiguration(InputStream ins) throws IOException, SecurityException { - checkAccess(); - reset(); - - // Load the properties - props.load(ins); - // Instantiate new configuration objects. - @SuppressWarnings("signature") - @BinaryName String names[] = parseClassNames("config"); - - for (int i = 0; i < names.length; i++) { - String word = names[i]; - try { - Class clz = ClassLoader.getSystemClassLoader().loadClass(word); - clz.newInstance(); - } catch (Exception ex) { - System.err.println("Can't load config class \"" + word + "\""); - System.err.println("" + ex); - // ex.printStackTrace(); - } - } - - // Set levels on any pre-existing loggers, based on the new properties. - setLevelsOnExistingLoggers(); - - // Notify any interested parties that our properties have changed. - changes.firePropertyChange(null, null, null); - - // Note that we need to reinitialize global handles when - // they are first referenced. - synchronized (this) { - initializedGlobalHandlers = false; - } - } - - @SuppressWarnings("signature") - Filter getFilterProperty(String name, Filter defaultValue); - - @SuppressWarnings("signature") - Formatter getFormatterProperty(String name, Formatter defaultValue); -} - -class MemoryHandler extends Handler { - - public MemoryHandler() { - sealed = false; - configure(); - sealed = true; - - @SuppressWarnings("signature") - @BinaryName String name = "???"; - try { - LogManager manager = LogManager.getLogManager(); - @SuppressWarnings("signature") - @BinaryName String temp = manager.getProperty("java.util.logging.MemoryHandler.target"); - name = temp; - Class clz = ClassLoader.getSystemClassLoader().loadClass(name); - target = (Handler) clz.newInstance(); - } catch (Exception ex) { - throw new RuntimeException("MemoryHandler can't load handler \"" + name + "\"" , ex); - } - init(); - } -} - -package java.io; - -class ObjectStreamClass implements Serializable { - public @BinaryName String getName(); -} diff --git a/checker/src/main/java/org/checkerframework/checker/tainting/jdk8.astub b/checker/src/main/java/org/checkerframework/checker/tainting/jdk8.astub deleted file mode 100644 index 2668c11fd829..000000000000 --- a/checker/src/main/java/org/checkerframework/checker/tainting/jdk8.astub +++ /dev/null @@ -1,15 +0,0 @@ -import org.checkerframework.checker.tainting.qual.*; - -package java.sql; - -interface Statement { - ResultSet executeQuery(@Untainted String sql); - int executeUpdate(@Untainted String sql); - boolean execute(@Untainted String sql); - int executeUpdate(@Untainted String sql, int autoGeneratedKeys); - int executeUpdate(@Untainted String sql, int[] columnIndexes); - int executeUpdate(@Untainted String sql, String[] columnNames); - boolean execute(@Untainted String sql, int autoGeneratedKeys); - boolean execute(@Untainted String sql, int[] columnIndexes); - boolean execute(@Untainted String sql, String[] columnNames); -} diff --git a/checker/src/main/resources/javadoc.astub b/checker/src/main/resources/javadoc.astub deleted file mode 100644 index c576203c546b..000000000000 --- a/checker/src/main/resources/javadoc.astub +++ /dev/null @@ -1,127 +0,0 @@ -// This file, javadoc.astub, models the JavaDoc classes in the JDK 8's -// com.sun.javadoc package, which were renamed/removed in JDK 11 and therefore -// cannot be part of an annotated JDK. -// It is annotated for the Value and Nullness checkers. - -import org.checkerframework.common.value.qual.MinLen; - -import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.dataflow.qual.Pure; -import org.checkerframework.dataflow.qual.SideEffectFree; - -package com.sun.javadoc; - -public interface ClassDoc extends ProgramElementDoc, Type { - @Pure boolean isAbstract(); - @Pure boolean isSerializable(); - @Pure boolean isExternalizable(); - MethodDoc[] serializationMethods(); - FieldDoc[] serializableFields(); - boolean definesSerializableFields(); - ClassDoc superclass(); - Type superclassType(); - boolean subclassOf(ClassDoc cd); - ClassDoc[] interfaces(); - Type[] interfaceTypes(); - TypeVariable[] typeParameters(); - ParamTag[] typeParamTags(); - FieldDoc [] fields(); - FieldDoc[] fields(boolean filter); - FieldDoc[] enumConstants(); - MethodDoc[] methods(); - MethodDoc[] methods(boolean filter); - ConstructorDoc[] constructors(); - ConstructorDoc[] constructors(boolean filter); - ClassDoc[] innerClasses(); - ClassDoc[] innerClasses(boolean filter); - ClassDoc findClass(String className); - @Deprecated ClassDoc[] importedClasses(); - @Deprecated PackageDoc[] importedPackages(); -} - -public interface Doc extends java.lang.Comparable { - public abstract java.lang.String commentText(); - public abstract com.sun.javadoc.Tag [] tags(); - public abstract com.sun.javadoc.Tag [] tags(java.lang.String a1); - public abstract com.sun.javadoc.SeeTag [] seeTags(); - public abstract com.sun.javadoc.Tag [] inlineTags(); - public abstract com.sun.javadoc.Tag [] firstSentenceTags(); - public abstract java.lang.String getRawCommentText(); - public abstract void setRawCommentText(java.lang.String a1); - public abstract java.lang.String name(); - @Pure public abstract int compareTo(java.lang.Object a1); - @Pure public abstract boolean isField(); - @Pure public abstract boolean isEnumConstant(); - @Pure public abstract boolean isConstructor(); - @Pure public abstract boolean isMethod(); - @Pure public abstract boolean isAnnotationTypeElement(); - @Pure public abstract boolean isInterface(); - @Pure public abstract boolean isException(); - @Pure public abstract boolean isError(); - @Pure public abstract boolean isEnum(); - @Pure public abstract boolean isAnnotationType(); - @Pure public abstract boolean isOrdinaryClass(); - @Pure public abstract boolean isClass(); - @Pure public abstract boolean isIncluded(); - public abstract com.sun.javadoc. @Nullable SourcePosition position(); -} - -public interface FieldDoc extends MemberDoc { - public abstract com.sun.javadoc.Type type(); - @Pure public abstract boolean isTransient(); - @Pure public abstract boolean isVolatile(); - public abstract com.sun.javadoc.SerialFieldTag[] serialFieldTags(); - public abstract @Nullable Object constantValue(); - public abstract java.lang. @Nullable String constantValueExpression(); -} - -public interface MemberDoc extends ProgramElementDoc { - @Pure public abstract boolean isSynthetic(); -} - -public interface ProgramElementDoc extends Doc { - public abstract com.sun.javadoc. @Nullable ClassDoc containingClass(); - public abstract com.sun.javadoc.PackageDoc containingPackage(); - public abstract java.lang.String qualifiedName(); - public abstract int modifierSpecifier(); - public abstract java.lang.String modifiers(); - public abstract com.sun.javadoc.AnnotationDesc[] annotations(); - @Pure public abstract boolean isPublic(); - @Pure public abstract boolean isProtected(); - @Pure public abstract boolean isPrivate(); - @Pure public abstract boolean isPackagePrivate(); - @Pure public abstract boolean isStatic(); - @Pure public abstract boolean isFinal(); -} - -public interface ExecutableMemberDoc extends MemberDoc { - ClassDoc[] thrownExceptions(); - Type[] thrownExceptionTypes(); - @Pure boolean isNative(); - @Pure boolean isSynchronized(); - @Pure public boolean isVarArgs(); - Parameter[] parameters(); - @Pure Type receiverType(); - ThrowsTag[] throwsTags(); - ParamTag[] paramTags(); - ParamTag[] typeParamTags(); - String signature(); - String flatSignature(); - TypeVariable[] typeParameters(); -} - -public interface RootDoc extends Doc, DocErrorReporter { - String [] @MinLen(1) [] options(); - PackageDoc[] specifiedPackages(); - ClassDoc[] specifiedClasses(); - ClassDoc @MinLen(1) [] classes(); - PackageDoc packageNamed(String name); - ClassDoc classNamed(String qualifiedName); -} - -public interface SourcePosition { - @SideEffectFree File file(); - @Pure int line(); - @Pure int column(); - @SideEffectFree String toString(); -} diff --git a/checker/src/test/java/tests/NullnessJavadocTest.java b/checker/src/test/java/tests/NullnessJavadocTest.java new file mode 100644 index 000000000000..b1b0ae9a6d1f --- /dev/null +++ b/checker/src/test/java/tests/NullnessJavadocTest.java @@ -0,0 +1,43 @@ +package tests; + +import java.io.File; +import java.util.Collections; +import java.util.List; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.checkerframework.javacutil.SystemUtil; +import org.junit.runners.Parameterized.Parameters; + +/** + * JUnit tests for the Nullness Checker -- testing type-checking of code that uses Javadoc classes. + */ +public class NullnessJavadocTest extends CheckerFrameworkPerDirectoryTest { + + /** @param testFiles the files containing test code, which will be type-checked */ + public NullnessJavadocTest(List testFiles) { + super( + testFiles, + org.checkerframework.checker.nullness.NullnessChecker.class, + "nullness", + toolsJarList(), + "-Anomsgtext"); + } + + /** + * Return a list that contains the pathname to the tools.jar file, if it exists. + * + * @returns a list that contains the pathname to the tools.jar file, if it exists + */ + private static List toolsJarList() { + String toolsJar = SystemUtil.getToolsJar(); + if (toolsJar == null) { + return Collections.emptyList(); + } else { + return Collections.singletonList(toolsJar); + } + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"nullness-javadoc"}; + } +} diff --git a/checker/tests/README b/checker/tests/README index d7c2557cf0bb..7c0b2c1cd052 100644 --- a/checker/tests/README +++ b/checker/tests/README @@ -29,13 +29,13 @@ file to be checked is AssertNonNullTest.java in directory $CHECKERFRAMEWORK/checker/tests/nullness/ and the checker is org.checkerframework.checker.nullness.NullnessChecker. - cd $CHECKERFRAMEWORK/checker/tests/nullness - (cd $CHECKERFRAMEWORK && ./gradlew compileJava) && $CHECKERFRAMEWORK/checker/bin-devel/javac -processor org.checkerframework.checker.nullness.NullnessChecker -implicit:class AssertNonNullTest.java + cd $CHECKERFRAMEWORK + ./gradlew compileJava && checker/bin-devel/javac -processor org.checkerframework.checker.nullness.NullnessChecker -implicit:class checker/tests/nullness/AssertNonNullTest.java or (to build distribution files) - cd $CHECKERFRAMEWORK/checker/tests/nullness - (cd $CHECKERFRAMEWORK && ./gradlew assemble) && $CHECKERFRAMEWORK/checker/bin/javac -processor org.checkerframework.checker.nullness.NullnessChecker -implicit:class AssertNonNullTest.java + cd $CHECKERFRAMEWORK + ./gradlew assemble && checker/bin/javac -processor org.checkerframework.checker.nullness.NullnessChecker -implicit:class checker/tests/nullness/AssertNonNullTest.java where the specific checker and command-line arguments are often clear from the directory name but can also be determined from a file such as diff --git a/checker/tests/nullness-javadoc/JavadocJdkAnnotations.java b/checker/tests/nullness-javadoc/JavadocJdkAnnotations.java new file mode 100644 index 000000000000..e0e24665fb6d --- /dev/null +++ b/checker/tests/nullness-javadoc/JavadocJdkAnnotations.java @@ -0,0 +1,18 @@ +import com.sun.javadoc.Doc; +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +public class JavadocJdkAnnotations { + + @Nullable Object f = null; + + @SuppressWarnings("removal") + void testPureAnnotation(Doc d) { + f = "non-null value"; + d.isIncluded(); + @NonNull Object x = f; + d.tags(); + // :: error: (assignment.type.incompatible) + @NonNull Object y = f; + } +} diff --git a/checker/tests/nullness-stubfile/NullnessStubfileMerge.java b/checker/tests/nullness-stubfile/NullnessStubfileMerge.java index 421d95dcec3f..fc26d492c87c 100644 --- a/checker/tests/nullness-stubfile/NullnessStubfileMerge.java +++ b/checker/tests/nullness-stubfile/NullnessStubfileMerge.java @@ -1,4 +1,4 @@ -// warning: StubParser: Method thisMethodIsNotReal(String) not found in type java.lang.String +// warning: StubParser: Package-private method notReal(String) not found in type java.lang.String // warning: StubParser: Type not found: java.lang.NotARealClass // warning: StubParser: Type not found: not.real.NotARealClassInNotRealPackage diff --git a/checker/tests/nullness-stubfile/stubfile1.astub b/checker/tests/nullness-stubfile/stubfile1.astub index 018d069ce375..66605d18f769 100644 --- a/checker/tests/nullness-stubfile/stubfile1.astub +++ b/checker/tests/nullness-stubfile/stubfile1.astub @@ -13,7 +13,7 @@ public final class String { String(@Nullable String arg0); void getChars(@Nullable int arg0, @NonNull int arg1, @NonNull char @NonNull [] arg2, @NonNull int arg3); // Used to test stub file warnings. - void thisMethodIsNotReal(String s); + void notReal(String s); } // The rest of these are used to test stub file warnings. public class NotARealClass{} diff --git a/checker/tests/signedness/TestPrintln.java b/checker/tests/signedness/TestPrintln.java index 965156c7a8fb..3f36f969f0f5 100644 --- a/checker/tests/signedness/TestPrintln.java +++ b/checker/tests/signedness/TestPrintln.java @@ -6,11 +6,8 @@ public class TestPrintln { public static void main(String[] args) { // The first call produces the intended result, but the next two do not. - // The Signedness Checker conservatively warns about all three, because it does not analyze - // the specific values returned by parseUnsignedInt. @Unsigned int a = Integer.parseUnsignedInt("2147483647"); - // :: error: (argument.type.incompatible) System.out.println(a); @Unsigned int b = Integer.parseUnsignedInt("2147483648"); // :: error: (argument.type.incompatible) diff --git a/checker/tests/signedness/UtilsJava8.java b/checker/tests/signedness/UtilsJava8.java index 27e1d04e4eae..63f7512ef376 100644 --- a/checker/tests/signedness/UtilsJava8.java +++ b/checker/tests/signedness/UtilsJava8.java @@ -1,4 +1,5 @@ -import org.checkerframework.checker.signedness.qual.*; +import org.checkerframework.checker.signedness.qual.Signed; +import org.checkerframework.checker.signedness.qual.Unsigned; // Test Java 8 unsigned utils public class UtilsJava8 { @@ -16,9 +17,9 @@ public void annotatedJDKTests( long resLong; // :: error: (argument.type.incompatible) - resString = Long.toUnsignedString(slong, sint); + resString = Long.toUnsignedString(slong, 10); - resString = Long.toUnsignedString(ulong, sint); + resString = Long.toUnsignedString(ulong, 10); // :: error: (argument.type.incompatible) resString = Long.toUnsignedString(slong); @@ -26,9 +27,9 @@ public void annotatedJDKTests( resString = Long.toUnsignedString(ulong); // :: error: (assignment.type.incompatible) - slong = Long.parseUnsignedLong(s, sint); + slong = Long.parseUnsignedLong(s, 10); - ulong = Long.parseUnsignedLong(s, sint); + ulong = Long.parseUnsignedLong(s, 10); // :: error: (assignment.type.incompatible) slong = Long.parseUnsignedLong(s); @@ -75,9 +76,9 @@ public void annotatedJDKTests( ulong = Long.remainderUnsigned(ulong, ulong); // :: error: (argument.type.incompatible) - resString = Integer.toUnsignedString(sint, sint); + resString = Integer.toUnsignedString(sint, 10); - resString = Integer.toUnsignedString(uint, sint); + resString = Integer.toUnsignedString(uint, 10); // :: error: (argument.type.incompatible) resString = Integer.toUnsignedString(sint); @@ -85,9 +86,9 @@ public void annotatedJDKTests( resString = Integer.toUnsignedString(uint); // :: error: (assignment.type.incompatible) - sint = Integer.parseUnsignedInt(s, sint); + sint = Integer.parseUnsignedInt(s, 10); - uint = Integer.parseUnsignedInt(s, sint); + uint = Integer.parseUnsignedInt(s, 10); // :: error: (assignment.type.incompatible) sint = Integer.parseUnsignedInt(s); diff --git a/checker/tests/tainting/Issue2156.java b/checker/tests/tainting/Issue2156.java index 5e8c03e46d77..2c7fdc07a598 100644 --- a/checker/tests/tainting/Issue2156.java +++ b/checker/tests/tainting/Issue2156.java @@ -3,7 +3,8 @@ // @skip-test until the bug is fixed -import org.checkerframework.checker.tainting.qual.*; +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; enum SampleEnum { @Untainted FIRST, diff --git a/checker/tests/tainting/Issue2159.java b/checker/tests/tainting/Issue2159.java index a9ecb7f3143b..e48020ba73ba 100644 --- a/checker/tests/tainting/Issue2159.java +++ b/checker/tests/tainting/Issue2159.java @@ -1,4 +1,6 @@ -import org.checkerframework.checker.tainting.qual.*; +import org.checkerframework.checker.tainting.qual.PolyTainted; +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; class Issue2159 { Issue2159() {} diff --git a/checker/tests/tainting/Issue2243.java b/checker/tests/tainting/Issue2243.java index 98b498a538a5..722d2a729ecb 100644 --- a/checker/tests/tainting/Issue2243.java +++ b/checker/tests/tainting/Issue2243.java @@ -1,7 +1,8 @@ // Test cases for issue 2243 // https://github.com/typetools/checker-framework/issues/2243 -import org.checkerframework.checker.tainting.qual.*; +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; // :: error: (declaration.inconsistent.with.extends.clause) public @Tainted class Issue2243 extends Y2243 {} diff --git a/checker/tests/tainting/Issue2330.java b/checker/tests/tainting/Issue2330.java index 8a722b0c67f3..eab2937f0c90 100644 --- a/checker/tests/tainting/Issue2330.java +++ b/checker/tests/tainting/Issue2330.java @@ -1,5 +1,6 @@ -import java.util.*; -import org.checkerframework.checker.tainting.qual.*; +import org.checkerframework.checker.tainting.qual.PolyTainted; +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; public class Issue2330 { // Checker can't verify that this creates an untainted Issue2330 diff --git a/docs/manual/accumulation-checker.tex b/docs/manual/accumulation-checker.tex new file mode 100644 index 000000000000..ddb0132e280c --- /dev/null +++ b/docs/manual/accumulation-checker.tex @@ -0,0 +1,79 @@ +\htmlhr +\chapterAndLabel{Building an accumulation checker}{accumulation-checker} + +%% This chapter should appear after the "creating a checker" chapter, or perhaps as part of it, +%% once accumulation support is complete. + +This chapter describes how to build a checker for an accumulation analysis. +If you want to \emph{use} an existing checker, you do not need to read this chapter. + +An \emph{accumulation analysis} is a program analysis where the +analysis abstraction is a monotonically increasing set --- that is, the +analysis learns new facts, and facts are never retracted. +Typically, some operation in code is legal +only when the set is large enough --- that is, the estimate has accumulated +sufficiently many facts. + +Accumulation analysis is a special case of typestate analysis in which +(1) the order in which operations are performed does not affect what is subsequently legal, +and (2) the accumulation does not add restrictions; that is, as +more operations are performed, more operations become legal. +Unlike a traditional typestate analysis, an accumulation analysis does +not require an alias analysis for soundness. It can therefore be implemented +as a flow-sensitive type system. + +The Checker Framework contains a generic accumulation analysis that you can +extend to create your own accumulation checker. + +Before reading the rest of this chapter, you should +read how to create a checker (Chapter~\ref{creating-a-checker}). +The rest of this chapter assumes you have done so. + + +\paragraphAndLabel{Defining type qualifiers}{accumulation-qualifiers} + +The Object Construction Checker (Section~\ref{object-construction-checker}) +is a concrete example of a practical accumulation checker that you may want +to reference. The +\href{https://github.com/typetools/checker-framework/blob/master/framework/src/test/java/testaccumulation/TestAccumulationChecker.java}{Test Accumulation Checker} +is a simplified version of the same that you can also use as a model. + +First, design your analysis. Decide what +your checker will accumulate and how to represent it. The Checker Framework's +support for accumulation analysis requires you to accumulate a string representation +of whatever you are accumulating. For example, when accumulating which methods have +been called on an object, you might choose to accumulate method names. + +Define a type qualifier that has a single argument: a \ named \. +The default value for this argument should be an empty array. The +qualifier should have no supertypes (\<@SubtypeOf({})>) and should +be the default qualifier in the hierarchy (\<@DefaultQualifierInHierarchy>). +An example of such a qualifier can be found in the Checker Framework's tests: +\href{https://github.com/typetools/checker-framework/blob/master/framework/src/test/java/testaccumulation/qual/TestAccumulation.java}{TestAccumulation.java}. + +Also define a bottom type, analogous to +\href{https://github.com/typetools/checker-framework/blob/master/framework/src/test/java/testaccumulation/qual/TestAccumulationBottom.java}{TestAccumulationBottom.java}. +It should take no arguments, and should be a subtype of the accumulator type you defined earlier. + +\paragraphAndLabel{Setting up the checker}{accumulation-setup} + +Define a new class that extends \refclass{common/accumulation}{AccumulationChecker}. +It does not need any content. + +Define a new class that extends \refclass{common/accumulation}{AccumulationAnnotatedTypeFactory}. +You must create a new constructor whose only argument is a \refclass{common/basetype}{BaseTypeChecker}. +Your constructor should call the \ constructor defined in +\refclass{common/accumulation}{AccumulationAnnotatedTypeFactory}. + + +\paragraphAndLabel{Adding accumulation logic}{accumulation-accumulating} + +Define a class that extends \refclass{common/accumulation}{AccumulationTransfer}. +To update the estimate of what has been accumulated, override +\refclass{framework/flow}{CFAbstractTransfer} to call +\refmethodterse{common/accumulation}{AccumulationTransfer}{accumulate}{-org.checkerframework.dataflow.cfg.node.Node-org.checkerframework.dataflow.analysis.TransferResult-java.lang.String...-}. + +For example, when accumulating the names of methods called, you would override +\refmethod{framework/flow}{CFAbstractTransfer}{visitMethodInvocation}{-org.checkerframework.dataflow.cfg.node.MethodInvocationNode-org.checkerframework.dataflow.analysis.TransferInput-}, +call \ to get a \, compute the method name from the \, +and then call \. diff --git a/docs/manual/constant-value-checker.tex b/docs/manual/constant-value-checker.tex index 98fa0c7bd6aa..39e7892bbfde 100644 --- a/docs/manual/constant-value-checker.tex +++ b/docs/manual/constant-value-checker.tex @@ -9,15 +9,10 @@ \begin{itemize} \item Typically, it is automatically run by another type checker. -%% This is an implementation detail that does not belong in the user -%% manual, because users don't have to do anything. -% When using the Constant Value Checker as part of another checker, the -% \code{statically-executable.astub} file in the Constant Value Checker directory must -% be passed as a stub file for the checker. \item Alternately, you can run just the Constant Value Checker, by supplying the following command-line options to javac: -\code{-processor org.checkerframework.common.value.ValueChecker -Astubs=statically-executable.astub} +\code{-processor org.checkerframework.common.value.ValueChecker} \end{itemize} @@ -233,8 +228,6 @@ Additionally, a \<@StaticallyExecutable> method and any method it calls must be on the classpath for the compiler, because they are reflectively called at compile-time to perform the constant value analysis. -% Standard library methods (such as those annotated as \<@StaticallyExecutable> -% in file \) will already be on the classpath. To use \<@StaticallyExecutable> on methods in your own code, you should first compile the code without the Constant Value Checker and then add the location of the resulting \code{.class} files to the @@ -242,7 +235,6 @@ might include: \begin{Verbatim} -processor org.checkerframework.common.value.ValueChecker - -Astubs=statically-executable.astub -classpath $CLASSPATH:MY_PROJECT/build/ \end{Verbatim} diff --git a/docs/manual/creating-a-checker.tex b/docs/manual/creating-a-checker.tex index 9dd3043e1249..8c7579f09f35 100644 --- a/docs/manual/creating-a-checker.tex +++ b/docs/manual/creating-a-checker.tex @@ -240,6 +240,7 @@ \begin{enumerate} \item +\label{creating-tips-write-manual} Write the user manual. Do this before you start coding. The manual explains the type system, what it guarantees, how to use it, etc., from the point of view of a user. Writing the manual will help you flesh out @@ -260,6 +261,7 @@ your design. \item +\label{creating-tips-implement-qualifiers} Implement the type qualifiers and hierarchy (Section~\ref{creating-typequals}). @@ -282,6 +284,7 @@ (\chapterpageref{subtyping-checker}). \item +\label{creating-tips-implement-checker} Write the checker class itself (Section~\ref{creating-compiler-interface}). @@ -294,6 +297,7 @@ \end{Verbatim} \item +\label{creating-tips-test-infrastructure} Test infrastructure. If your checker source code is in a clone of the Checker Framework repository, integrate your checker with the Checker Framework's Gradle diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index 6ae528af2bae..29888e05a328 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -554,16 +554,11 @@ % running your code, you can use either the annotated library or the regular % distributed version of the library --- they behave identically. -There is one special case. -\begin{itemize} -\item -For the Java 8 version of the Javadoc classes in the JDK's \ package, -% are not exposed by ct.sym and therefore cannot be part of an -% annotated JDK -use the stub file \ by using \<-Astubs=checker.jar/javadoc.astub>. +There is one special case. If an \<.astub> file is shipped with the +Checker Framework in \, then you can +use \<-Astubs=checker.jar/\emph{stubfilename.astub}>. The ``\'' should be literal --- don't provide a path. (This special syntax only works for ``\''.) -\end{itemize} \subsectionAndLabel{Summary of command-line options}{checker-options} diff --git a/docs/manual/manual.tex b/docs/manual/manual.tex index 36445b801fd1..c165999a429a 100644 --- a/docs/manual/manual.tex +++ b/docs/manual/manual.tex @@ -86,6 +86,8 @@ \input{inference.tex} \input{annotating-libraries.tex} \input{creating-a-checker.tex} +% The Accumulation Checker is not yet ready to be publicized. +\input{accumulation-checker.tex} \input{external-tools.tex} \input{faq.tex} \input{troubleshooting.tex} diff --git a/docs/manual/warnings.tex b/docs/manual/warnings.tex index 2bfdeff3451a..18e95c698a39 100644 --- a/docs/manual/warnings.tex +++ b/docs/manual/warnings.tex @@ -112,7 +112,7 @@ \code{@SuppressWarnings("mynifty")}. (An exception is the Subtyping Checker, for which you use the annotation name; see Section~\ref{subtyping-using}.) -Sometimes, a checker honors \emph{checkername} arguments; use +Sometimes, a checker honors multiple \emph{checkername} arguments; use the \code{-AshowSuppressWarningKeys} command-line option to see them. Using \code{"all"} as the checkername applies to all checkers; this is not recommended, except for messages common to all checkers such as @@ -121,7 +121,7 @@ The argument \emph{messagekey} is the message key for the error. Each warning message from the compiler gives the most specific suppression key that can be used to suppress that warning. -An example is \ in +An example is ``\'' in %BEGIN LATEX \begin{smaller} @@ -153,9 +153,8 @@ to all messages (it suppresses all warnings from the given checker). With the \code{-ArequirePrefixInWarningSuppressions} command-line -option, a warning is only suppressed if the key is in the -\code{"\emph{checkername}"} or -\code{"\emph{checkername}:\emph{messagekey}"} +option, the Checker Framework only suppresses warnings when the key is in +the \code{"\emph{checkername}"} or \code{"\emph{checkername}:\emph{messagekey}"} format, as in \<@SuppressWarnings("nullness")> or \<@SuppressWarnings("nullness:assignment.type.incompatible")>. diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/CheckerFrameworkPerDirectoryTest.java b/framework-test/src/main/java/org/checkerframework/framework/test/CheckerFrameworkPerDirectoryTest.java index 014c2c9ecbbc..8f63126d1dfa 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/CheckerFrameworkPerDirectoryTest.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/CheckerFrameworkPerDirectoryTest.java @@ -57,6 +57,28 @@ public abstract class CheckerFrameworkPerDirectoryTest { /** Extra options to pass to javac when running the checker. */ protected final List checkerOptions; + /** Extra entries for the classpath. */ + protected final List classpathExtra; + + /** + * Creates a new checker test. + * + *

{@link TestConfigurationBuilder#getDefaultConfigurationBuilder(String, File, String, + * Iterable, Iterable, List, boolean)} adds additional checker options. + * + * @param testFiles the files containing test code, which will be type-checked + * @param checker the class for the checker to use + * @param testDir the path to the directory of test inputs + * @param checkerOptions options to pass to the compiler when running tests + */ + protected CheckerFrameworkPerDirectoryTest( + List testFiles, + Class checker, + String testDir, + String... checkerOptions) { + this(testFiles, checker, testDir, Collections.emptyList(), checkerOptions); + } + /** * Creates a new checker test. * @@ -66,16 +88,19 @@ public abstract class CheckerFrameworkPerDirectoryTest { * @param testFiles the files containing test code, which will be type-checked * @param checker the class for the checker to use * @param testDir the path to the directory of test inputs + * @param classpathExtra extra entries for the classpath * @param checkerOptions options to pass to the compiler when running tests */ protected CheckerFrameworkPerDirectoryTest( List testFiles, Class checker, String testDir, + List classpathExtra, String... checkerOptions) { this.testFiles = testFiles; this.checkerName = checker.getName(); this.testDir = "tests" + File.separator + testDir; + this.classpathExtra = classpathExtra; this.checkerOptions = new ArrayList<>(Arrays.asList(checkerOptions)); } @@ -88,6 +113,7 @@ public void run() { TestConfigurationBuilder.buildDefaultConfiguration( testDir, testFiles, + classpathExtra, Collections.singleton(checkerName), customizedOptions, shouldEmitDebugInfo); diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerDirectoryTest.java b/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerDirectoryTest.java index a03d118d0ab2..bc6259a51e0f 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerDirectoryTest.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerDirectoryTest.java @@ -6,7 +6,8 @@ /** * The same as {@link org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest} except - * the annotated JDK is not required. + * the annotated JDK is not used (because the {@code annotated-jdk} resource is under {@code + * checker/}, not {@code framework/}). */ public abstract class FrameworkPerDirectoryTest extends CheckerFrameworkPerDirectoryTest { @@ -16,7 +17,7 @@ public abstract class FrameworkPerDirectoryTest extends CheckerFrameworkPerDirec *

{@link TestConfigurationBuilder#getDefaultConfigurationBuilder(String, File, String, * Iterable, Iterable, List, boolean)} adds additional checker options. * - *

These tests do not require the annotated JDK. + *

These tests do not use the annotated JDK. * * @param testFiles the files containing test code, which will be type-checked * @param checker the class for the checker to use diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerFileTest.java b/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerFileTest.java index 3dc01eead393..777e2ec8ce18 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerFileTest.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/FrameworkPerFileTest.java @@ -6,7 +6,8 @@ /** * The same as {@link org.checkerframework.framework.test.CheckerFrameworkPerFileTest}, but does not - * require the annotated JDK. + * use the annotated JDK (because the {@code annotated-jdk} resource is under {@code checker/}, not + * {@code framework/}). */ public abstract class FrameworkPerFileTest extends CheckerFrameworkPerFileTest { /** @@ -15,7 +16,7 @@ public abstract class FrameworkPerFileTest extends CheckerFrameworkPerFileTest { *

{@link TestConfigurationBuilder#getDefaultConfigurationBuilder(String, File, String, * Iterable, Iterable, List, boolean)} adds additional checker options. * - *

These tests do not require the annotated JDK. + *

These tests do not use the annotated JDK. * * @param testFile the file containing test code, which will be type-checked * @param checker the class for the checker to use diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/TestConfigurationBuilder.java b/framework-test/src/main/java/org/checkerframework/framework/test/TestConfigurationBuilder.java index f1314bedd3d4..899251c3ce42 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/TestConfigurationBuilder.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/TestConfigurationBuilder.java @@ -3,6 +3,8 @@ import java.io.File; import java.util.ArrayList; import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; import java.util.LinkedHashSet; import java.util.List; import java.util.Map; @@ -93,8 +95,43 @@ public static TestConfiguration buildDefaultConfiguration( Iterable processors, List options, boolean shouldEmitDebugInfo) { + return buildDefaultConfiguration( + testSourcePath, + testSourceFiles, + Collections.emptyList(), + processors, + options, + shouldEmitDebugInfo); + } + + /** + * This is the default configuration used by Checker Framework JUnit tests. + * + * @param testSourcePath the path to the Checker test file sources, usually this is the + * directory of Checker's tests + * @param testSourceFiles the Java files that compose the test + * @param classpathExtra extra entries for the classpath, needed to compile the source files + * @param processors the checkers or other annotation processors to run over the testSourceFiles + * @param options the options to the compiler/processors + * @param shouldEmitDebugInfo whether or not debug information should be emitted + * @return a TestConfiguration with input parameters added plus the normal default options, + * compiler, and file manager used by Checker Framework tests + */ + public static TestConfiguration buildDefaultConfiguration( + String testSourcePath, + Iterable testSourceFiles, + Collection classpathExtra, + Iterable processors, + List options, + boolean shouldEmitDebugInfo) { String classPath = getDefaultClassPath(); + if (!classpathExtra.isEmpty()) { + classPath += + System.getProperty("path.separator") + + String.join(System.getProperty("path.separator"), classpathExtra); + } + File outputDir = getOutputDirFromProperty(); TestConfigurationBuilder builder = @@ -131,7 +168,12 @@ public static TestConfiguration buildDefaultConfiguration( List processors = Arrays.asList(checkerName); return buildDefaultConfiguration( - testSourcePath, javaFiles, processors, options, shouldEmitDebugInfo); + testSourcePath, + javaFiles, + Collections.emptyList(), + processors, + options, + shouldEmitDebugInfo); } /** The list of files that contain Java diagnostics to compare against. */ diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java index fcab9e24c230..a3c91b4bdb50 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java @@ -400,9 +400,16 @@ public static void writeJavacArguments( *

In a checker, we treat a more specific error message as subsumed by a general one. For * example, "new.array.type.invalid" is subsumed by "type.invalid". This is not the case in the * test framework; the exact error key is expected. + * + * @param testResult the result of type-checking */ public static void assertResultsAreValid(TypecheckResult testResult) { if (testResult.didTestFail()) { + if (getShouldEmitDebugInfo()) { + System.out.println("---------------- start of javac ouput ----------------"); + System.out.println(testResult.getCompilationResult().getJavacOutput()); + System.out.println("---------------- end of javac ouput ----------------"); + } Assert.fail(testResult.summarize()); } } diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/TypecheckResult.java b/framework-test/src/main/java/org/checkerframework/framework/test/TypecheckResult.java index 97b08a0114ce..79d31d6e46cc 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/TypecheckResult.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/TypecheckResult.java @@ -169,32 +169,4 @@ public static TypecheckResult fromCompilationResults( missingDiagnostics, new ArrayList<>(unexpectedDiagnostics)); } - - public static TypecheckResult fromCompilationResultsExpectedDiagnostics( - TestConfiguration configuration, - CompilationResult result, - List expectedDiagnostics) { - - boolean usingAnomsgtxt = configuration.getOptions().containsKey("-Anomsgtext"); - final Set actualDiagnostics = - TestDiagnosticUtils.fromJavaxDiagnosticList( - result.getDiagnostics(), usingAnomsgtxt); - - final Set unexpectedDiagnostics = new LinkedHashSet<>(); - unexpectedDiagnostics.addAll(actualDiagnostics); - unexpectedDiagnostics.removeAll(expectedDiagnostics); - - final List missingDiagnostics = new ArrayList<>(expectedDiagnostics); - missingDiagnostics.removeAll(actualDiagnostics); - - boolean testFailed = !unexpectedDiagnostics.isEmpty() || !missingDiagnostics.isEmpty(); - - return new TypecheckResult( - configuration, - result, - expectedDiagnostics, - testFailed, - missingDiagnostics, - new ArrayList<>(unexpectedDiagnostics)); - } } diff --git a/framework/build.gradle b/framework/build.gradle index 02a9c160e27f..767590149e70 100644 --- a/framework/build.gradle +++ b/framework/build.gradle @@ -1,9 +1,11 @@ +ext { + annotatedJdkHome = '../../jdk' +} sourceSets { main { resources { // Stub files, message.properties, etc. - srcDirs = ['src/main/java'] - exclude '**/*.java' + srcDirs += ['src/main/java', "${buildDir}/generated/resources"] } } testannotations @@ -16,7 +18,7 @@ sourceSets { } def versions = [ - autoValue : "1.7.2", + autoValue : "1.7.3", lombok : "1.18.12", ] @@ -28,7 +30,7 @@ dependencies { // AFU is an "includedBuild" imported in checker-framework/settings.gradle, so the version number doesn't matter. // https://docs.gradle.org/current/userguide/composite_builds.html#settings_defined_composite implementation('org.checkerframework:annotation-file-utilities:*') { - exclude group: 'com.google', module: 'javac' + exclude group: 'com.google.errorprone', module: 'javac' } implementation project(':checker-qual') implementation 'org.plumelib:reflection-util:0.2.2' @@ -56,6 +58,75 @@ dependencies { testImplementation "org.projectlombok:lombok:${versions.lombok}" } +task cloneTypetoolsJdk() { + description 'Obtain or update the annotated JDK.' + doLast { + if (file(annotatedJdkHome).exists()) { + exec { + workingDir annotatedJdkHome + executable 'git' + args = ['pull', '-q'] + ignoreExitValue = true + } + } else { + println 'Cloning annotated JDK repository.' + exec { + workingDir "${annotatedJdkHome}/../" + executable 'git' + args = ['clone', '-q', '--depth', '1', 'https://github.com/typetools/jdk.git', 'jdk'] + } + } + } +} + + +task copyAndMinimizeAnnotatedJdkFiles(dependsOn: cloneTypetoolsJdk, group: 'Build') { + dependsOn ':framework:compileJava' + def inputDir = "${annotatedJdkHome}/src" + def outputDir = "${buildDir}/generated/resources/annotated-jdk/" + + description "Copy annotated JDK files to ${outputDir}. Removes private and package-private methods, method bodies, comments, etc. from the annotated JDK" + + inputs.dir file(inputDir) + outputs.dir file(outputDir) + + doLast { + FileTree tree = fileTree(dir: inputDir) + SortedSet annotatedForFiles = new TreeSet<>(); + tree.visit { FileVisitDetails fvd -> + if (!fvd.file.isDirectory() && fvd.file.name.matches(".*\\.java") + && !fvd.file.path.contains("org/checkerframework") + && !fvd.file.name.matches("module-info.java")) { + // Ignore module-info until this JavaParser bug is fixed (and merged in the StubParser): + // https://github.com/javaparser/javaparser/issues/2615 + fvd.getFile().readLines().any { line -> + if (line.contains("@AnnotatedFor") || line.contains("org.checkerframework")) { + annotatedForFiles.add(fvd.file.absolutePath) + return true; + } + } + } + } + String absolutejdkHome = file(annotatedJdkHome).absolutePath + int jdkDirStringSize = absolutejdkHome.size() + copy { + from(annotatedJdkHome) + into(outputDir) + for (String filename : annotatedForFiles) { + include filename.substring(jdkDirStringSize) + } + } + javaexec { + classpath = sourceSets.main.runtimeClasspath + + main = 'org.checkerframework.framework.stub.JavaStubifier' + args outputDir + } + } +} + +processResources.dependsOn(copyAndMinimizeAnnotatedJdkFiles) + task checkDependencies(dependsOn: ':maybeCloneAndBuildDependencies') { doLast { if (!file(stubparserJar).exists()) { @@ -275,6 +346,7 @@ task loaderTests(dependsOn: 'shadowJar', group: 'Verification') { clean { delete("tests/whole-program-inference/annotated") delete("tests/returnsreceiverdelomboked") + delete('dist') } diff --git a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationAnnotatedTypeFactory.java new file mode 100644 index 000000000000..8a556e8de15e --- /dev/null +++ b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationAnnotatedTypeFactory.java @@ -0,0 +1,332 @@ +package org.checkerframework.common.accumulation; + +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodInvocationTree; +import java.lang.annotation.Annotation; +import java.lang.reflect.Method; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.ExecutableElement; +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.returnsreceiver.ReturnsReceiverAnnotatedTypeFactory; +import org.checkerframework.common.returnsreceiver.ReturnsReceiverChecker; +import org.checkerframework.common.returnsreceiver.qual.This; +import org.checkerframework.common.value.ValueCheckerUtils; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.QualifierHierarchy; +import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.TreeAnnotator; +import org.checkerframework.framework.util.MultiGraphQualifierHierarchy; +import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.TreeUtils; + +/** + * An annotated type factory for an accumulation checker. + * + *

New accumulation checkers should extend this class and implement a constructor, which should + * take a {@link BaseTypeChecker} and call both the constructor defined in this class and {@link + * #postInit()}. + */ +public abstract class AccumulationAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { + + /** + * The canonical top annotation for this accumulation checker: an instance of the accumulator + * annotation with no arguments. + */ + public final AnnotationMirror top; + + /** The canonical bottom annotation for this accumulation checker. */ + public final AnnotationMirror bottom; + + /** + * The annotation that accumulates things in this accumulation checker. Must be an annotation + * with exactly one field named "value" whose type is a String array. + */ + private final Class accumulator; + + /** + * Create an annotated type factory for an accumulation checker. + * + * @param checker the checker + * @param accumulator the accumulator type in the hierarchy. Must be an annotation with a single + * argument named "value" whose type is a String array. + * @param bottom the bottom type in the hierarchy, which must be a subtype of {@code + * accumulator}. The bottom type should be an annotation with no arguments. + */ + protected AccumulationAnnotatedTypeFactory( + BaseTypeChecker checker, + Class accumulator, + Class bottom) { + super(checker); + + this.accumulator = accumulator; + + // Check that the requirements of the accumulator are met. + Method[] accDeclaredMethods = accumulator.getDeclaredMethods(); + if (accDeclaredMethods.length != 1) { + rejectMalformedAccumulator("have exactly one element"); + } + Method value = accDeclaredMethods[0]; + if (value.getName() != "value") { // interned + rejectMalformedAccumulator("name its element \"value\""); + } + if (!value.getReturnType().isInstance(new String[0])) { + rejectMalformedAccumulator("have an element of type String[]"); + } + if (((String[]) value.getDefaultValue()).length != 0) { + rejectMalformedAccumulator("have the empty String array {} as its default value"); + } + + this.bottom = AnnotationBuilder.fromClass(elements, bottom); + this.top = createAccumulatorAnnotation(Collections.emptyList()); + + // Every subclass must call postInit! This does not do so for subclasses. + if (this.getClass() == AccumulationAnnotatedTypeFactory.class) { + this.postInit(); + } + } + + /** + * Common error message for malformed accumulator annotation. + * + * @param missing what is missing from the accumulator, suitable for use in this string to + * replace $MISSING$: "The accumulator annotation Foo must $MISSING$." + */ + private void rejectMalformedAccumulator(String missing) { + throw new BugInCF("The accumulator annotation " + accumulator + " must " + missing + "."); + } + + /** + * Creates a new instance of the accumulator annotation that contains the elements of {@code + * values}. + * + * @param values the arguments to the annotation. The values can contain duplicates and can be + * in any order. + * @return an annotation mirror representing the accumulator annotation with {@code values}'s + * arguments; this is top if {@code values} is empty + */ + public AnnotationMirror createAccumulatorAnnotation(List values) { + AnnotationBuilder builder = new AnnotationBuilder(processingEnv, accumulator); + builder.setValue("value", ValueCheckerUtils.removeDuplicates(values)); + return builder.build(); + } + + /** + * Creates a new instance of the accumulator annotation that contains exactly one value. + * + * @param value the argument to the annotation. + * @return an annotation mirror representing the accumulator annotation with {@code value} as + * its argument + */ + public AnnotationMirror createAccumulatorAnnotation(String value) { + AnnotationBuilder builder = new AnnotationBuilder(processingEnv, accumulator); + builder.setValue("value", Collections.singletonList(value)); + return builder.build(); + } + + /** + * Returns true if the return type of the given method invocation tree has an @This annotation + * from the Returns Receiver Checker. + * + * @param tree a method invocation tree + * @return true if the method being invoked returns its receiver + */ + public boolean returnsThis(final MethodInvocationTree tree) { + // Must call `getTypeFactoryOfSubchecker` each time, not store and reuse. + ReturnsReceiverAnnotatedTypeFactory rrATF = + getTypeFactoryOfSubchecker(ReturnsReceiverChecker.class); + ExecutableElement methodEle = TreeUtils.elementFromUse(tree); + AnnotatedTypeMirror methodAtm = rrATF.getAnnotatedType(methodEle); + AnnotatedTypeMirror rrType = + ((AnnotatedTypeMirror.AnnotatedExecutableType) methodAtm).getReturnType(); + return rrType != null && rrType.hasAnnotation(This.class); + } + + /** + * Is the given annotation an accumulator annotation? Returns false if the argument is {@link + * #bottom}. + * + * @param anm an annotation mirror + * @return true if the annotation mirror is an instance of this factory's accumulator annotation + */ + public boolean isAccumulatorAnnotation(AnnotationMirror anm) { + return AnnotationUtils.areSameByClass(anm, accumulator); + } + + @Override + protected TreeAnnotator createTreeAnnotator() { + return new ListTreeAnnotator( + super.createTreeAnnotator(), new AccumulationTreeAnnotator(this)); + } + + /** + * This tree annotator implements the following rule(s): + * + *

+ *
RRA + *
If a method returns its receiver, and the receiver has an accumulation type, then the + * default type of the method's return value is the type of the receiver. + *
+ */ + protected class AccumulationTreeAnnotator extends TreeAnnotator { + + /** + * Creates an instance of this tree annotator for the given type factory. + * + * @param factory the type factory + */ + public AccumulationTreeAnnotator(AccumulationAnnotatedTypeFactory factory) { + super(factory); + } + + /** + * Implements rule RRA. + * + * @param tree a method invocation tree + * @param type the type of {@code tree} (i.e. the return type of the invoked method). Is + * (possibly) side-effected by this method. + * @return nothing, works by side-effect on {@code type} + */ + @Override + public Void visitMethodInvocation(MethodInvocationTree tree, AnnotatedTypeMirror type) { + if (returnsThis(tree)) { + // There is a @This annotation on the return type of the invoked method. + ExpressionTree receiverTree = TreeUtils.getReceiverTree(tree.getMethodSelect()); + AnnotatedTypeMirror receiverType = + receiverTree == null ? null : getAnnotatedType(receiverTree); + // The current type of the receiver, or top if none exists. + AnnotationMirror receiverAnno = + receiverType == null ? top : receiverType.getAnnotationInHierarchy(top); + + AnnotationMirror returnAnno = type.getAnnotationInHierarchy(top); + type.replaceAnnotation(qualHierarchy.greatestLowerBound(returnAnno, receiverAnno)); + } + return super.visitMethodInvocation(tree, type); + } + } + + @Override + public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { + return new AccumulationQualifierHierarchy(factory); + } + + /** + * Returns all the values that anno has accumulated. + * + * @param anno an accumulator annotation; must not be bottom + * @return the list of values the annotation has accumulated; it is a new list, so it is safe + * for clients to side-effect + */ + public List getAccumulatedValues(AnnotationMirror anno) { + if (!isAccumulatorAnnotation(anno)) { + throw new BugInCF(anno + "isn't an accumulator annotation"); + } + List values = ValueCheckerUtils.getValueOfAnnotationWithStringArgument(anno); + if (values == null) { + return new ArrayList<>(0); + } else { + return values; + } + } + + /** + * All accumulation analyses share a similar type hierarchy. This class implements the + * subtyping, LUB, and GLB for that hierarchy. The lattice looks like: + * + *
+     *       acc()
+     *      /   \
+     * acc(x)   acc(y) ...
+     *      \   /
+     *     acc(x,y) ...
+     *        |
+     *      bottom
+     * 
+ */ + protected class AccumulationQualifierHierarchy extends MultiGraphQualifierHierarchy { + + /** + * Create the qualifier hierarchy + * + * @param factory the factory + */ + public AccumulationQualifierHierarchy(MultiGraphFactory factory) { + super(factory); + } + + @Override + public AnnotationMirror getTopAnnotation(final AnnotationMirror start) { + return top; + } + + /** + * GLB in this type system is set union of the arguments of the two annotations, unless one + * of them is bottom, in which case the result is also bottom. + */ + @Override + public AnnotationMirror greatestLowerBound( + final AnnotationMirror a1, final AnnotationMirror a2) { + if (AnnotationUtils.areSame(a1, bottom) || AnnotationUtils.areSame(a2, bottom)) { + return bottom; + } + + List a1Val = getAccumulatedValues(a1); + List a2Val = getAccumulatedValues(a2); + // Avoid creating new annotation objects in the common case. + if (a1Val.containsAll(a2Val)) { + return a1; + } + if (a2Val.containsAll(a1Val)) { + return a2; + } + a1Val.addAll(a2Val); + return createAccumulatorAnnotation(a1Val); + } + + /** + * LUB in this type system is set intersection of the arguments of the two annotations, + * unless one of them is bottom, in which case the result is the other annotation. + */ + @Override + public AnnotationMirror leastUpperBound( + final AnnotationMirror a1, final AnnotationMirror a2) { + if (AnnotationUtils.areSame(a1, bottom)) { + return a2; + } else if (AnnotationUtils.areSame(a2, bottom)) { + return a1; + } + + List a1Val = getAccumulatedValues(a1); + List a2Val = getAccumulatedValues(a2); + // Avoid creating new annotation objects in the common case. + if (a1Val.containsAll(a2Val)) { + return a2; + } + if (a2Val.containsAll(a1Val)) { + return a1; + } + a1Val.retainAll(a2Val); + return createAccumulatorAnnotation(a1Val); + } + + /** isSubtype in this type system is subset. */ + @Override + public boolean isSubtype(final AnnotationMirror subAnno, final AnnotationMirror superAnno) { + if (AnnotationUtils.areSame(subAnno, bottom)) { + return true; + } else if (AnnotationUtils.areSame(superAnno, bottom)) { + return false; + } + + List subVal = getAccumulatedValues(subAnno); + List superVal = getAccumulatedValues(superAnno); + return subVal.containsAll(superVal); + } + } +} diff --git a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationChecker.java b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationChecker.java new file mode 100644 index 000000000000..c4134141abca --- /dev/null +++ b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationChecker.java @@ -0,0 +1,29 @@ +package org.checkerframework.common.accumulation; + +import java.util.LinkedHashSet; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.returnsreceiver.ReturnsReceiverChecker; + +// TODO: This Javadoc comment should reference the Checker Framework manual, once the Accumulation +// Checker chapter is uncommented in the manual's LaTeX source. +/** + * An accumulation checker is one that accumulates some property: method calls, map keys, etc. + * + *

This class provides a basic accumulation analysis that can be extended to implement an + * accumulation type system. This accumulation analysis represents all facts as Strings. It + * automatically includes returns-receiver aliasing to precisely handle fluent APIs, but otherwise + * uses no alias analysis. + * + *

The primary extension point is the constructor of {@link AccumulationAnnotatedTypeFactory}, + * which every subclass should override to provide custom annotations. + */ +public abstract class AccumulationChecker extends BaseTypeChecker { + + @Override + protected LinkedHashSet> getImmediateSubcheckerClasses() { + LinkedHashSet> checkers = + super.getImmediateSubcheckerClasses(); + checkers.add(ReturnsReceiverChecker.class); + return checkers; + } +} diff --git a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java new file mode 100644 index 000000000000..9ba36e587be4 --- /dev/null +++ b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java @@ -0,0 +1,126 @@ +package org.checkerframework.common.accumulation; + +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.Tree.Kind; +import java.util.Arrays; +import java.util.List; +import java.util.Set; +import javax.lang.model.element.AnnotationMirror; +import org.checkerframework.common.value.ValueCheckerUtils; +import org.checkerframework.dataflow.analysis.FlowExpressions; +import org.checkerframework.dataflow.analysis.FlowExpressions.Receiver; +import org.checkerframework.dataflow.analysis.TransferResult; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.framework.flow.CFAnalysis; +import org.checkerframework.framework.flow.CFStore; +import org.checkerframework.framework.flow.CFTransfer; +import org.checkerframework.framework.flow.CFValue; + +/** + * The default transfer function for an accumulation checker. + * + *

Subclasses should call the {@link #accumulate(Node, TransferResult, String...)} accumulate} + * method to add a string to the estimate at a particular program point. + */ +public class AccumulationTransfer extends CFTransfer { + + /** The type factory. */ + protected final AccumulationAnnotatedTypeFactory typeFactory; + + /** + * Build a new AccumulationTransfer for the given analysis. + * + * @param analysis the analysis + */ + public AccumulationTransfer(CFAnalysis analysis) { + super(analysis); + typeFactory = (AccumulationAnnotatedTypeFactory) analysis.getTypeFactory(); + } + + /** + * Updates the estimate of how many things {@code node} has accumulated. + * + *

If the node is an invocation of a method that returns its receiver, then its receiver's + * type will also be updated. In a chain of method calls, this process will continue backward as + * long as each receiver is itself a receiver-returning method invocation. + * + *

For example, suppose {@code node} is the expression {@code a.b().c()}, the new value + * (added by the accumulation analysis because of the {@code .c()} call) is "foo", and b and c + * return their receiver. This method will directly update the estimate of {@code a.b().c()} to + * include "foo". In addition, the estimates for the expressions {@code a.b()} and {@code a} + * would have their estimates updated to include "foo", because c and b (respectively) return + * their receivers. Note that due to what kind of values can be held in the store, this + * information is lost outside the method chain. That is, the returns-receiver propagated + * information is lost outside the expression in which the returns-receiver method invocations + * are nested. + * + *

As a concrete example, consider the Called Methods accumulation checker: if {@code build} + * requires a, b, and c to be called, then {@code foo.a().b().c().build();} will typecheck (they + * are in one fluent method chain), but {@code foo.a().b().c(); foo.build();} will not -- the + * store does not keep the information that a, b, and c have been called outside the chain. + * {@code foo}'s type will be {@code CalledMethods("a")}, because only {@code a()} was called + * directly on {@code foo}. For such code to typecheck, the Called Methods accumulation checker + * uses an additional rule: the return type of a receiver-returning method {@code rr()} is + * {@code CalledMethods("rr")}. This rule is implemented directly in the {@link + * org.checkerframework.framework.type.treeannotator.TreeAnnotator} subclass defined in the + * Called Methods type factory. + * + * @param node the node whose estimate should be expanded + * @param result the transfer result containing the store to be modified + * @param values the new accumulation values + */ + public void accumulate(Node node, TransferResult result, String... values) { + List valuesAsList = Arrays.asList(values); + // If dataflow has already recorded information about the target, fetch it and integrate + // it into the list of values in the new annotation. + CFValue flowValue = result.getResultValue(); + if (flowValue != null) { + Set flowAnnos = flowValue.getAnnotations(); + assert flowAnnos.size() <= 1; + for (AnnotationMirror anno : flowAnnos) { + List oldFlowValues = + ValueCheckerUtils.getValueOfAnnotationWithStringArgument(anno); + if (oldFlowValues != null) { + // valuesAsList cannot have its length changed -- it is backed by an array. + // getValueOfAnnotationWithStringArgument returns a new, modifiable list. + oldFlowValues.addAll(valuesAsList); + valuesAsList = oldFlowValues; + } + } + } + + AnnotationMirror newAnno = typeFactory.createAccumulatorAnnotation(valuesAsList); + insertIntoStores(result, node, newAnno); + + Tree tree = node.getTree(); + if (tree != null && tree.getKind() == Kind.METHOD_INVOCATION) { + Node receiver = ((MethodInvocationNode) node).getTarget().getReceiver(); + if (receiver != null && typeFactory.returnsThis((MethodInvocationTree) tree)) { + accumulate(receiver, result, values); + } + } + } + + /** + * Inserts newAnno as the value into all stores (conditional or not) in the result for node. + * + * @param result the TransferResult holding the stores to modify + * @param node the node whose value should be modified + * @param newAnno the new value + */ + private void insertIntoStores( + TransferResult result, Node node, AnnotationMirror newAnno) { + Receiver receiver = FlowExpressions.internalReprOf(typeFactory, node); + if (result.containsTwoStores()) { + CFStore thenStore = result.getThenStore(); + CFStore elseStore = result.getElseStore(); + thenStore.insertValue(receiver, newAnno); + elseStore.insertValue(receiver, newAnno); + } else { + CFStore store = result.getRegularStore(); + store.insertValue(receiver, newAnno); + } + } +} diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java index e66377df118b..6de18d1d4300 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java @@ -125,20 +125,12 @@ protected boolean shouldCheckTopLevelDeclaredType(AnnotatedTypeMirror type, Tree */ protected List isValidType( QualifierHierarchy qualifierHierarchy, AnnotatedTypeMirror type) { - SimpleAnnotatedTypeScanner, Void> scanner = - new SimpleAnnotatedTypeScanner, Void>() { - @Override - protected List defaultAction( - AnnotatedTypeMirror type, Void aVoid) { - return isTopLevelValidType(qualifierHierarchy, type); - } - - @Override - protected List reduce(List r1, List r2) { - return DiagMessage.mergeLists(r1, r2); - } - }; - return scanner.visit(type); + SimpleAnnotatedTypeScanner, QualifierHierarchy> scanner = + new SimpleAnnotatedTypeScanner<>( + (atm, q) -> isTopLevelValidType(q, atm), + DiagMessage::mergeLists, + Collections.emptyList()); + return scanner.visit(type, qualifierHierarchy); } /** diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index e2e3f09788d1..bffa5347a0e6 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2458,46 +2458,39 @@ private static boolean shouldPrintVerbose( * A scanner that indicates whether any (sub-)types have the same toString but different verbose * toString. */ - private static SimpleAnnotatedTypeScanner checkContainsSameToString = - new SimpleAnnotatedTypeScanner() { - /** Maps from a type's toString to its verbose toString. */ - Map map = new HashMap<>(); - - @Override - protected Boolean reduce(Boolean r1, Boolean r2) { - r1 = r1 == null ? false : r1; - r2 = r2 == null ? false : r2; - return r1 || r2; - } - - @Override - protected Boolean defaultAction(AnnotatedTypeMirror type, Void avoid) { - if (type == null) { - return false; - } - String simple = type.toString(); - String verbose = map.get(simple); - if (verbose == null) { - map.put(simple, type.toString(true)); - return false; - } else { - return !verbose.equals(type.toString(true)); - } - } - }; + private static SimpleAnnotatedTypeScanner> + checkContainsSameToString = + new SimpleAnnotatedTypeScanner<>( + (AnnotatedTypeMirror type, Map map) -> { + if (type == null) { + return false; + } + String simple = type.toString(); + String verbose = map.get(simple); + if (verbose == null) { + map.put(simple, type.toString(true)); + return false; + } else { + return !verbose.equals(type.toString(true)); + } + }, + Boolean::logicalOr, + false); /** * Return true iff there are two annotated types (anywhere in any ATM) such that their toStrings * are the same but their verbose toStrings differ. + * + * @param atms annotated type mirrors to compare + * @return true iff there are two annotated types (anywhere in any ATM) such that their + * toStrings are the same but their verbose toStrings differ. */ private static boolean containsSameToString(AnnotatedTypeMirror... atms) { + Map simpleToVerbose = new HashMap<>(); for (AnnotatedTypeMirror atm : atms) { - Boolean result = checkContainsSameToString.visit(atm); - if (result != null && result) { + if (checkContainsSameToString.visit(atm, simpleToVerbose)) { return true; } - // Call reset to clear the visitor history, but not the map from Strings to types. - checkContainsSameToString.reset(); } return false; diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueChecker.java b/framework/src/main/java/org/checkerframework/common/value/ValueChecker.java index 5bb0c83971d2..7c2a97b997fc 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueChecker.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueChecker.java @@ -4,7 +4,6 @@ import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.common.value.util.Range; -import org.checkerframework.framework.qual.StubFiles; import org.checkerframework.framework.source.SupportedOptions; /** @@ -18,7 +17,6 @@ * * @checker_framework.manual #constant-value-checker Constant Value Checker */ -@StubFiles("statically-executable.astub") @SupportedOptions({ ValueChecker.REPORT_EVAL_WARNS, ValueChecker.IGNORE_RANGE_OVERFLOW, diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java index 40685ee1e117..fde459afb8c4 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java @@ -124,7 +124,7 @@ protected Void scan(AnnotatedTypeMirror type, Void p) { @Override public Void visitDeclared(AnnotatedDeclaredType type, Void p) { - // Skip type arguments. + // Don't call super so that the type arguments are not visited. if (type.getEnclosingType() != null) { scan(type.getEnclosingType(), p); } diff --git a/framework/src/main/java/org/checkerframework/common/value/statically-executable.astub b/framework/src/main/java/org/checkerframework/common/value/statically-executable.astub deleted file mode 100644 index 31ffa1a62f2a..000000000000 --- a/framework/src/main/java/org/checkerframework/common/value/statically-executable.astub +++ /dev/null @@ -1,409 +0,0 @@ -import org.checkerframework.common.value.qual.*; - -package java.lang; - -class Boolean{ - @StaticallyExecutable Boolean(boolean value); - @StaticallyExecutable Boolean(String s); - @StaticallyExecutable boolean booleanValue(); - @StaticallyExecutable static boolean getBoolean(String name); - @StaticallyExecutable static boolean parseBoolean(String s); - @StaticallyExecutable @StringVal({"true", "false"}) String toString(); - @StaticallyExecutable static @StringVal({"true", "false"}) String toString(boolean b); - @StaticallyExecutable static Boolean valueOf(boolean b); - @StaticallyExecutable static Boolean valueOf(String s); -} - -class Byte{ - @StaticallyExecutable Byte(byte value); - @StaticallyExecutable Byte(String s); - - @StaticallyExecutable @PolyValue byte byteValue(@PolyValue Byte this); - @StaticallyExecutable static Byte decode(String nm); - @StaticallyExecutable @PolyValue double doubleValue(@PolyValue Byte this); - @StaticallyExecutable @PolyValue float floatValue(@PolyValue Byte this); - @StaticallyExecutable @PolyValue int intValue(@PolyValue Byte this); - @StaticallyExecutable @PolyValue long longValue(@PolyValue Byte this); - @StaticallyExecutable static byte parseByte(String s); - @StaticallyExecutable static byte parseByte(String s, int radix); - @StaticallyExecutable @PolyValue short shortValue(@PolyValue Byte this); - @StaticallyExecutable @ArrayLen({1,2,3,4}) String toString(); - @StaticallyExecutable static @ArrayLen({1,2,3,4}) String toString(byte b); - @StaticallyExecutable static @PolyValue Byte valueOf(@PolyValue byte b); - @StaticallyExecutable static Byte valueOf(String s); - @StaticallyExecutable static Byte valueOf(String s, int radix); -} - -class Character{ - @StaticallyExecutable Character(char value); - - @StaticallyExecutable static int charCount(int codePoint); - @StaticallyExecutable char charValue(); - @StaticallyExecutable static int codePointAt(char[] a, int index); - @StaticallyExecutable static int codePointAt(char[] a, int index, int limit); - @StaticallyExecutable static int codePointAt(CharSequence seq, int index); - @StaticallyExecutable static int codePointBefore(char[] a, int index); - @StaticallyExecutable static int codePointBefore(char[] a, int index, int start); - @StaticallyExecutable static int codePointBefore(CharSequence seq, int index); - @StaticallyExecutable static int codePointCount(char[] a, int offset, int count); - @StaticallyExecutable static int codePointCount(CharSequence seq, int beginIndex, int endIndex); - @StaticallyExecutable static int digit(char ch, int radix); - @StaticallyExecutable static int digit(int codePoint, int radix); - @StaticallyExecutable static char forDigit(int digit, int radix); - @StaticallyExecutable static byte getDirectionality(char ch); - @StaticallyExecutable static byte getDirectionality(int codePoint); - @StaticallyExecutable static int getNumericValue(char ch); - @StaticallyExecutable static int getNumericValue(int codePoint); - @StaticallyExecutable static int getType(char ch); - @StaticallyExecutable static int getType(int codePoint); - @StaticallyExecutable static boolean isDefined(char ch); - @StaticallyExecutable static boolean isDefined(int codePoint); - @StaticallyExecutable static boolean isDigit(char ch); - @StaticallyExecutable static boolean isDigit(int codePoint); - @StaticallyExecutable static boolean isHighSurrogate(char ch); - @StaticallyExecutable static boolean isIdentifierIgnorable(char ch); - @StaticallyExecutable static boolean isIdentifierIgnorable(int codePoint); - @StaticallyExecutable static boolean isISOControl(char ch); - @StaticallyExecutable static boolean isISOControl(int codePoint); - @StaticallyExecutable static boolean isJavaIdentifierPart(char ch); - @StaticallyExecutable static boolean isJavaIdentifierPart(int codePoint); - @StaticallyExecutable static boolean isJavaIdentifierStart(char ch); - @StaticallyExecutable static boolean isJavaIdentifierStart(int codePoint); - @StaticallyExecutable static boolean isJavaLetter(char ch); - @StaticallyExecutable static boolean isJavaLetterOrDigit(char ch); - @StaticallyExecutable static boolean isLetter(char ch); - @StaticallyExecutable static boolean isLetter(int codePoint); - @StaticallyExecutable static boolean isLetterOrDigit(char ch); - @StaticallyExecutable static boolean isLetterOrDigit(int codePoint); - @StaticallyExecutable static boolean isLowerCase(char ch); - @StaticallyExecutable static boolean isLowerCase(int codePoint); - @StaticallyExecutable static boolean isLowSurrogate(char ch); - @StaticallyExecutable static boolean isMirrored(char ch); - @StaticallyExecutable static boolean isMirrored(int codePoint); - @StaticallyExecutable static boolean isSpace(char ch); - @StaticallyExecutable static boolean isSpaceChar(char ch); - @StaticallyExecutable static boolean isSpaceChar(int codePoint); - @StaticallyExecutable static boolean isSupplementaryCodePoint(int codePoint); - @StaticallyExecutable static boolean isSurrogatePair(char high, char low); - @StaticallyExecutable static boolean isTitleCase(char ch); - @StaticallyExecutable static boolean isTitleCase(int codePoint); - @StaticallyExecutable static boolean isUnicodeIdentifierPart(char ch); - @StaticallyExecutable static boolean isUnicodeIdentifierPart(int codePoint); - @StaticallyExecutable static boolean isUnicodeIdentifierStart(char ch); - @StaticallyExecutable static boolean isUnicodeIdentifierStart(int codePoint); - @StaticallyExecutable static boolean isUpperCase(char ch); - @StaticallyExecutable static boolean isUpperCase(int codePoint); - @StaticallyExecutable static boolean isValidCodePoint(int codePoint); - @StaticallyExecutable static boolean isWhitespace(char ch); - @StaticallyExecutable static boolean isWhitespace(int codePoint); - @StaticallyExecutable static int offsetByCodePoints(char[] a, int start, int count, int index, int codePointOffset); - @StaticallyExecutable static int offsetByCodePoints(CharSequence seq, int index, int codePointOffset); - @StaticallyExecutable static char reverseBytes(char ch); - @StaticallyExecutable static char[] toChars(int codePoint); - @StaticallyExecutable static int toChars(int codePoint, char[] dst, int dstIndex); - @StaticallyExecutable static int toCodePoint(char high, char low); - @StaticallyExecutable static char toLowerCase(char ch); - @StaticallyExecutable static int toLowerCase(int codePoint); - @StaticallyExecutable @ArrayLen(1) String toString(); - @StaticallyExecutable static @ArrayLen(1) String toString(char c); - @StaticallyExecutable static char toTitleCase(char ch); - @StaticallyExecutable static int toTitleCase(int codePoint); - @StaticallyExecutable static char toUpperCase(char ch); - @StaticallyExecutable static int toUpperCase(int codePoint); - @StaticallyExecutable static @PolyValue Character valueOf(@PolyValue char c); -} - -class Double{ - @StaticallyExecutable Double(double value); - @StaticallyExecutable Double(String s); - - @StaticallyExecutable @PolyValue byte byteValue(@PolyValue Double this); - @StaticallyExecutable static int compare(double d1, double d2); - @StaticallyExecutable static long doubleToLongBits(double value); - @StaticallyExecutable static long doubleToRawLongBits(double value); - @StaticallyExecutable @PolyValue double doubleValue(@PolyValue Double this); - @StaticallyExecutable @PolyValue float floatValue(@PolyValue Double this); - @StaticallyExecutable @PolyValue int intValue(@PolyValue Double this); - @StaticallyExecutable boolean isInfinite(); - @StaticallyExecutable static boolean isInfinite(double v); - @StaticallyExecutable boolean isNaN(); - @StaticallyExecutable static boolean isNaN(double v); - @StaticallyExecutable static double longBitsToDouble(long bits); - @StaticallyExecutable @PolyValue long longValue(@PolyValue Double this); - @StaticallyExecutable static double parseDouble(String s); - @StaticallyExecutable @PolyValue short shortValue(@PolyValue Double this); - @StaticallyExecutable static String toHexString(double d); - @StaticallyExecutable String toString(); - @StaticallyExecutable static String toString(double d); - @StaticallyExecutable static @PolyValue Double valueOf(@PolyValue double d); - @StaticallyExecutable static Double valueOf(String s); -} -class Float{ - @StaticallyExecutable Float(double value); - @StaticallyExecutable Float(float value); - @StaticallyExecutable Float(String s); - - @StaticallyExecutable @PolyValue byte byteValue(@PolyValue Float this); - @StaticallyExecutable static int compare(float f1, float f2); - @StaticallyExecutable @PolyValue double doubleValue(@PolyValue Float this); - @StaticallyExecutable static int floatToIntBits(float value); - @StaticallyExecutable static int floatToRawIntBits(float value); - @StaticallyExecutable @PolyValue float floatValue(@PolyValue Float this); - @StaticallyExecutable static float intBitsToFloat(int bits); - @StaticallyExecutable @PolyValue int intValue(@PolyValue Float this); - @StaticallyExecutable boolean isInfinite(); - @StaticallyExecutable static boolean isInfinite(float v); - @StaticallyExecutable boolean isNaN(); - @StaticallyExecutable static boolean isNaN(float v); - @StaticallyExecutable @PolyValue long longValue(@PolyValue Float this); - @StaticallyExecutable static float parseFloat(String s); - @StaticallyExecutable @PolyValue short shortValue(@PolyValue Float this); - @StaticallyExecutable static String toHexString(float f); - @StaticallyExecutable String toString(); - @StaticallyExecutable static String toString(float f); - @StaticallyExecutable static @PolyValue Float valueOf(@PolyValue float f); - @StaticallyExecutable static Float valueOf(String s); -} - -class Integer{ - @StaticallyExecutable Integer(int value); - @StaticallyExecutable Integer(String s); - - @StaticallyExecutable static int bitCount(int i); - @StaticallyExecutable @PolyValue byte byteValue(@PolyValue Integer this); - @StaticallyExecutable static Integer decode(String nm); - @StaticallyExecutable @PolyValue double doubleValue(@PolyValue Integer this); - @StaticallyExecutable @PolyValue float floatValue(@PolyValue Integer this); - @StaticallyExecutable static Integer getInteger(String nm); - @StaticallyExecutable static Integer getInteger(String nm, int val); - @StaticallyExecutable static Integer getInteger(String nm, Integer val); - @StaticallyExecutable static int highestOneBit(int i); - @StaticallyExecutable @PolyValue int intValue(@PolyValue Integer this); - @StaticallyExecutable @PolyValue long longValue(@PolyValue Integer this); - @StaticallyExecutable static int lowestOneBit(int i); - @StaticallyExecutable static @IntRange(from = 0, to = 32) int numberOfLeadingZeros(int i); - @StaticallyExecutable static @IntRange(from = 0, to = 32) int numberOfTrailingZeros(int i); - @StaticallyExecutable static int parseInt(String s); - @StaticallyExecutable static int parseInt(String s, int radix); - @StaticallyExecutable static int reverse(int i); - @StaticallyExecutable static int reverseBytes(int i); - @StaticallyExecutable static int rotateLeft(int i, int distance); - @StaticallyExecutable static int rotateRight(int i, int distance); - @StaticallyExecutable short shortValue(); - @StaticallyExecutable static int signum(int i); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 32) String toBinaryString(int i); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 8) String toHexString(int i); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 11) String toOctalString(int i); - @StaticallyExecutable @ArrayLenRange(from = 1, to = 11) String toString(); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 11) String toString(int i); - @StaticallyExecutable static @ArrayLenRange(from = 1) String toString(int i, int radix); - @StaticallyExecutable static @PolyValue Integer valueOf(@PolyValue int i); - @StaticallyExecutable static Integer valueOf(String s); - @StaticallyExecutable static Integer valueOf(String s, int radix); -} - -class Long{ - @StaticallyExecutable Long(long value); - @StaticallyExecutable Long(String s); - - @StaticallyExecutable static int bitCount(long i); - @StaticallyExecutable @PolyValue byte byteValue(@PolyValue Long this); - @StaticallyExecutable static Long decode(String nm); - @StaticallyExecutable @PolyValue double doubleValue(@PolyValue Long this); - @StaticallyExecutable @PolyValue float floatValue(@PolyValue Long this); - @StaticallyExecutable static Long getLong(String nm); - @StaticallyExecutable static Long getLong(String nm, long val); - @StaticallyExecutable static Long getLong(String nm, Long val); - @StaticallyExecutable static long highestOneBit(long i); - @StaticallyExecutable @PolyValue int intValue(@PolyValue Long this); - @StaticallyExecutable @PolyValue long longValue(@PolyValue Long this); - @StaticallyExecutable static long lowestOneBit(long i); - @StaticallyExecutable static @IntRange(from = 0, to = 64) int numberOfLeadingZeros(long i); - @StaticallyExecutable static @IntRange(from = 0, to = 64) int numberOfTrailingZeros(long i); - @StaticallyExecutable static long parseLong(String s); - @StaticallyExecutable static long parseLong(String s, int radix); - @StaticallyExecutable static long reverse(long i); - @StaticallyExecutable static long reverseBytes(long i); - @StaticallyExecutable static long rotateLeft(long i, int distance); - @StaticallyExecutable static long rotateRight(long i, int distance); - @StaticallyExecutable @PolyValue short shortValue(@PolyValue Long this); - @StaticallyExecutable static int signum(long i); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 64) String toBinaryString(long i); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 16) String toHexString(long i); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 22) String toOctalString(long i); - @StaticallyExecutable @ArrayLenRange(from = 1, to = 20) String toString(); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 20) String toString(long i); - @StaticallyExecutable static @ArrayLenRange(from = 1) String toString(long i, int radix); - @StaticallyExecutable static @PolyValue Long valueOf(@PolyValue long l); - @StaticallyExecutable static Long valueOf(String s); - @StaticallyExecutable static Long valueOf(String s, int radix); -} - -class Short{ - @StaticallyExecutable Short(short value); - @StaticallyExecutable Short(String s); - - @StaticallyExecutable @PolyValue byte byteValue(@PolyValue Short this); - @StaticallyExecutable static Short decode(String nm); - @StaticallyExecutable @PolyValue double doubleValue(@PolyValue Short this); - @StaticallyExecutable @PolyValue float floatValue(@PolyValue Short this); - @StaticallyExecutable @PolyValue int intValue(@PolyValue Short this); - @StaticallyExecutable @PolyValue long longValue(@PolyValue Short this); - @StaticallyExecutable static short parseShort(String s); - @StaticallyExecutable static short parseShort(String s, int radix); - @StaticallyExecutable static short reverseBytes(short i); - @StaticallyExecutable @PolyValue short shortValue(@PolyValue Short this); - @StaticallyExecutable @ArrayLen({1, 2, 3, 4, 5, 6}) String toString(); - @StaticallyExecutable static @ArrayLen({1, 2, 3, 4, 5, 6}) String toString(short s); - @StaticallyExecutable static @PolyValue Short valueOf(@PolyValue short s); - @StaticallyExecutable static Short valueOf(String s); - @StaticallyExecutable static Short valueOf(String s, int radix); -} - -class String{ - @StaticallyExecutable String(); - @StaticallyExecutable @PolyValue String(@PolyValue String original); - @StaticallyExecutable String(StringBuffer buffer); - @StaticallyExecutable String(StringBuilder builder); - @StaticallyExecutable @PolyValue String(char @PolyValue[] value); - @StaticallyExecutable String(char[] value, int offset, int count); - @StaticallyExecutable String(int[] codePoints, int offset, int count); - - @StaticallyExecutable char charAt(int index); - @StaticallyExecutable int codePointAt(int index); - @StaticallyExecutable int codePointBefore(int index); - @StaticallyExecutable int codePointCount(int beginIndex, int endIndex); - @StaticallyExecutable int compareTo(String anotherString); - @StaticallyExecutable int compareToIgnoreCase(String str); - @StaticallyExecutable String concat(String str); - @StaticallyExecutable boolean contains(CharSequence s); - @StaticallyExecutable boolean contentEquals(CharSequence cs); - @StaticallyExecutable boolean contentEquals(StringBuffer sb); - @StaticallyExecutable static @PolyValue String copyValueOf(char @PolyValue[] data); - @StaticallyExecutable static String copyValueOf(char[] data, int offset, int count); - @StaticallyExecutable boolean endsWith(String suffix); - @StaticallyExecutable boolean equalsIgnoreCase(String anotherString); - @StaticallyExecutable static String format(Locale l, String format, Object... args); - @StaticallyExecutable static String format(String format, Object... args); - byte[] getBytes(); - byte[] getBytes(Charset charset); - void getBytes(int srcBegin, int srcEnd, byte[] dst, int dstBegin); - byte[] getBytes(String charsetName); - void getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin); - @StaticallyExecutable int indexOf(int ch); - @StaticallyExecutable int indexOf(int ch, int fromIndex); - @StaticallyExecutable int indexOf(String str); - @StaticallyExecutable int indexOf(String str, int fromIndex); - @StaticallyExecutable @PolyValue String intern(@PolyValue String this); - @StaticallyExecutable @EnsuresMinLenIf(expression="this", result=false, targetValue=1) boolean isEmpty(); - @StaticallyExecutable int lastIndexOf(int ch); - @StaticallyExecutable int lastIndexOf(int ch, int fromIndex); - @StaticallyExecutable int lastIndexOf(String str); - @StaticallyExecutable int lastIndexOf(String str, int fromIndex); - @StaticallyExecutable int length(); - @StaticallyExecutable boolean matches(String regex); - @StaticallyExecutable int offsetByCodePoints(int index, int codePointOffset); - @StaticallyExecutable boolean regionMatches(boolean ignoreCase, int toffset, String other, int ooffset, int len); - @StaticallyExecutable boolean regionMatches(int toffset, String other, int ooffset, int len); - @StaticallyExecutable String replace(char oldChar, char newChar); - @StaticallyExecutable String replace(CharSequence target, CharSequence replacement); - @StaticallyExecutable String replaceAll(String regex, String replacement); - @StaticallyExecutable String replaceFirst(String regex, String replacement); - String @MinLen(1) [] split(String regex); - String @MinLen(1) [] split(String regex, int limit); - @StaticallyExecutable boolean startsWith(String prefix); - @StaticallyExecutable boolean startsWith(String prefix, int toffset); - @StaticallyExecutable CharSequence subSequence(int beginIndex, int endIndex); - @StaticallyExecutable String substring(int beginIndex); - @StaticallyExecutable String substring(int beginIndex, int endIndex); - @StaticallyExecutable char @PolyValue[] toCharArray(@PolyValue String this); - @StaticallyExecutable String toLowerCase(); - @StaticallyExecutable String toLowerCase(Locale locale); - @StaticallyExecutable @PolyValue String toString(@PolyValue String this); - @StaticallyExecutable String toUpperCase(); - @StaticallyExecutable String toUpperCase(Locale locale); - @StaticallyExecutable String trim(); - @StaticallyExecutable static @StringVal({"true", "false"}) String valueOf(boolean b); - @StaticallyExecutable static @ArrayLen(1) String valueOf(char c); - @StaticallyExecutable static @PolyValue String valueOf(char @PolyValue[] data); - @StaticallyExecutable static String valueOf(char[] data, int offset, int count); - @StaticallyExecutable static String valueOf(double d); - @StaticallyExecutable static String valueOf(float f); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 11) String valueOf(int i); - @StaticallyExecutable static @ArrayLenRange(from = 1, to = 20) String valueOf(long l); - @StaticallyExecutable static String valueOf(Object obj) ; -} - -package java.math; - -class BigInteger { - BigInteger(@IntRange(from = -1, to = 1) int signum, byte[] magnitude); - BigInteger(String val, @IntRange(from = 2, to = 36) int radix); - - @IntRange(from = -1, to = 1) int compareTo(BigInteger val); - @PolyValue double doubleValue(@PolyValue BigInteger this); - @PolyValue float floatValue(@PolyValue BigInteger this); - @PolyValue int intValue(@PolyValue BigInteger this); - @PolyValue long longValue(@PolyValue BigInteger this); - @IntRange(from = -1, to = 1) int signum(); -} - -package java.util.regex; - -class Pattern { - String @MinLen(1) [] split(CharSequence input, int limit) ; - String @MinLen(1) [] split(CharSequence input) ; -} - -package java.util; - -class StringTokenizer { - @MinLen(1) String nextToken(); - @MinLen(1) String nextToken(String delim); -} - -class Arrays { - static @MinLen(2) String toString(long[] a); - static @MinLen(2) String toString(int[] a); - static @MinLen(2) String toString(short[] a); - static @MinLen(2) String toString(char[] a); - static @MinLen(2) String toString(byte[] a); - static @MinLen(2) String toString(boolean[] a); - static @MinLen(2) String toString(float[] a); - static @MinLen(2) String toString(double[] a); - static @MinLen(2) String toString(Object[] a); - static @MinLen(2) String deepToString(Object[] a); -} - -class Calendar { - public @IntRange(from = 1, to = 7) int getFirstDayOfWeek(); - public void setFirstDayOfWeek(@IntRange(from = 1, to = 7) int value); - public @IntRange(from = 1, to = 7) int getMinimalDaysInFirstWeek(); - public void setMinimalDaysInFirstWeek(@IntRange(from = 1, to = 7) int value); -} - -package java.awt.image; - -class ColorModel { - public int @PolyValue [] getComponents(int pixel, int @PolyValue [] components, int offset); - public int @PolyValue [] getComponents(Object pixel, int @PolyValue [] components, int offset); -} - -package java.text; - -class DateFormatSymbols { - public String @ArrayLen(2) [] getEras(); - public void setEras(String @ArrayLen(2) [] newEras); - public String @ArrayLen(13) [] getMonths(); - public void setMonths(String @ArrayLen(13) [] newMonths); - public String @ArrayLen(13) [] getShortMonths(); - public void setShortMonths(String @ArrayLen(13) [] newShortMonths); - public String @ArrayLen(8) [] getWeekdays(); - public void setWeekdays(String @ArrayLen(8) [] newWeekdays); - public String @ArrayLen(8) [] getShortWeekdays(); - public void setShortWeekdays(String @ArrayLen(8) [] newShortWeekdays); - public String @ArrayLen(2) [] getAmPmStrings(); - public void setAmPmStrings(String @ArrayLen(2) [] newAmpms); - public String @ArrayLen(2) [] @MinLen(5) [] getZoneStrings(); - public void setZoneStrings(String @ArrayLen(2) [] @MinLen(5) [] newZoneStrings); -} diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java index 7035f8cd9a4b..6b730a89e2f9 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java @@ -50,7 +50,7 @@ *

This class populates the initial Scenes by reading existing .jaif files on the {@link * #JAIF_FILES_PATH} directory (regardless of output format). Having more information in those * initial .jaif files means that the precision achieved by the whole-program inference analysis - * will be better. {@code writeScenes()} rewrites the initial .jaif files, and may create new ones. + * will be better. {@link #writeScenes} rewrites the initial .jaif files, and may create new ones. */ public class WholeProgramInferenceScenesStorage { diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index b91eeb8cf2d9..48e01d835f9a 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -2042,12 +2042,7 @@ public boolean shouldSuppressWarnings(Tree tree, String errKey) { } // trees.getPath might be slow, but this is only used in error reporting - // TODO: #1586 this might return null within a cloned finally block and - // then a warning that should be suppressed isn't. Fix this when fixing #1586. @Nullable TreePath path = trees.getPath(this.currentRoot, tree); - if (path == null) { - return false; - } @Nullable VariableTree var = TreeUtils.enclosingVariable(path); if (var != null && shouldSuppressWarnings(TreeUtils.elementFromTree(var), errKey)) { diff --git a/framework/src/main/java/org/checkerframework/framework/stub/StubParser.java b/framework/src/main/java/org/checkerframework/framework/stub/StubParser.java index 999c0a5d0f73..bad0dbd60261 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/StubParser.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/StubParser.java @@ -3,6 +3,7 @@ import com.github.javaparser.ParseProblemException; import com.github.javaparser.Problem; import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.AccessSpecifier; import com.github.javaparser.ast.CompilationUnit; import com.github.javaparser.ast.ImportDeclaration; import com.github.javaparser.ast.Modifier; @@ -75,7 +76,7 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; -import org.checkerframework.framework.type.visitor.AnnotatedTypeReplacer; +import org.checkerframework.framework.type.AnnotatedTypeReplacer; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; @@ -898,8 +899,8 @@ private void clearAnnotations(AnnotatedTypeMirror atype, Type typeDef) { /** * Add the annotations from {@code type} to {@code atype}. Type annotations that parsed as - * declaration annotations (ie those in {@code declAnnos} are applied to the innermost component - * type. + * declaration annotations (i.e., type annotations in {@code declAnnos} are applied to the + * innermost component type. * * @param atype annotated type to which to add annotations * @param type parsed type @@ -941,8 +942,8 @@ private ClassOrInterfaceType unwrapDeclaredType(Type type) { * *

    *
  1. the annotations from {@code typeDef}, and - *
  2. any type annotations that parsed as declaration annotations (ie those in {@code - * declAnnos}). + *
  3. any type annotations that parsed as declaration annotations (i.e., type annotations in + * {@code declAnnos}). *
* * @param atype annotated type to which to add annotations @@ -1425,7 +1426,8 @@ private VariableElement findElement( /** * Looks for method element in the typeElt and returns it if the element has the same signature - * as provided method declaration. In case method element is not found it returns null. + * as provided method declaration. Returns null, and possibly issues a warning, if method + * element is not found. * * @param typeElt type element where method element should be looked for * @param methodDecl method declaration with signature that should be found among methods in the @@ -1451,12 +1453,22 @@ private ExecutableElement findElement(TypeElement typeElt, MethodDeclaration met return method; } } - stubWarnNotFound("Method " + wantedMethodString + " not found in type " + typeElt); - if (debugStubParser) { - stubDebug(String.format(" Here are the methods of %s:", typeElt)); - for (ExecutableElement method : - ElementFilter.methodsIn(typeElt.getEnclosedElements())) { - stubDebug(String.format(" %s", method)); + if (methodDecl.getAccessSpecifier() == AccessSpecifier.PACKAGE_PRIVATE) { + // This might be a false positive warning. The stub parser permits a stub file to omit + // the access specifier, but package-private methods aren't in the TypeElement. + stubWarnNotFound( + "Package-private method " + + wantedMethodString + + " not found in type " + + typeElt); + } else { + stubWarnNotFound("Method " + wantedMethodString + " not found in type " + typeElt); + if (debugStubParser) { + stubDebug(String.format(" Here are the methods of %s:", typeElt)); + for (ExecutableElement method : + ElementFilter.methodsIn(typeElt.getEnclosedElements())) { + stubDebug(String.format(" %s", method)); + } } } return null; @@ -1741,9 +1753,11 @@ private Object getValueOfExpressionInAnnotation( /** * Converts {@code number} to {@code expectedKind}. - *

- * {@code @interface Anno { long value();}) - * {@code @Anno(1)} + * + *


+     *   @interface Anno { long value(); }
+     *   @Anno(1)
+     * 
* * To properly build @Anno, the IntegerLiteralExpr "1" must be converted from an int to a long. */ diff --git a/framework/src/main/java/org/checkerframework/framework/stub/StubTypes.java b/framework/src/main/java/org/checkerframework/framework/stub/StubTypes.java index f365ba8a823d..4b723d5e050a 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/StubTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/StubTypes.java @@ -512,7 +512,7 @@ private void prepJdkFromFile(URL resourceURL) { jdkStubFiles.put(s, path); } } catch (IOException e) { - throw new BugInCF("File Not Found", e); + throw new BugInCF("prepJdkFromFile(" + resourceURL + ")", e); } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index 5c07e0c276fc..38f22deb2548 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -99,12 +99,13 @@ public void viewpointAdaptConstructor( ExecutableElement constructorElt, AnnotatedExecutableType constructorType) { - AnnotatedExecutableType declConstructorType = atypeFactory.getAnnotatedType(constructorElt); + // constructorType's typevar are not substituted when calling viewpointAdaptConstructor + AnnotatedExecutableType unsubstitutedConstructorType = constructorType.deepCopy(); // For constructors, we adapt parameter types, return type and type parameters - List parameterTypes = declConstructorType.getParameterTypes(); - List typeVariables = declConstructorType.getTypeVariables(); - AnnotatedTypeMirror constructorReturn = declConstructorType.getReturnType(); + List parameterTypes = unsubstitutedConstructorType.getParameterTypes(); + List typeVariables = unsubstitutedConstructorType.getTypeVariables(); + AnnotatedTypeMirror constructorReturn = unsubstitutedConstructorType.getReturnType(); Map mappings = new IdentityHashMap<>(); for (AnnotatedTypeMirror parameterType : parameterTypes) { @@ -118,13 +119,14 @@ public void viewpointAdaptConstructor( AnnotatedTypeMirror cr = combineTypeWithType(receiverType, constructorReturn); mappings.put(constructorReturn, cr); - declConstructorType = + unsubstitutedConstructorType = (AnnotatedExecutableType) - AnnotatedTypeCopierWithReplacement.replace(declConstructorType, mappings); + AnnotatedTypeCopierWithReplacement.replace( + unsubstitutedConstructorType, mappings); - constructorType.setParameterTypes(declConstructorType.getParameterTypes()); - constructorType.setTypeVariables(declConstructorType.getTypeVariables()); - constructorType.setReturnType(declConstructorType.getReturnType()); + constructorType.setParameterTypes(unsubstitutedConstructorType.getParameterTypes()); + constructorType.setTypeVariables(unsubstitutedConstructorType.getTypeVariables()); + constructorType.setReturnType(unsubstitutedConstructorType.getReturnType()); } @Override @@ -136,13 +138,14 @@ public void viewpointAdaptMethod( return; } - AnnotatedExecutableType declMethodType = atypeFactory.getAnnotatedType(methodElt); + // methodType's typevar are not substituted when calling viewpointAdaptMethod + AnnotatedExecutableType unsubstitutedMethodType = methodType.deepCopy(); // For methods, we additionally adapt method receiver compared to constructors - List parameterTypes = declMethodType.getParameterTypes(); - List typeVariables = declMethodType.getTypeVariables(); - AnnotatedTypeMirror returnType = declMethodType.getReturnType(); - AnnotatedTypeMirror methodReceiver = declMethodType.getReceiverType(); + List parameterTypes = unsubstitutedMethodType.getParameterTypes(); + List typeVariables = unsubstitutedMethodType.getTypeVariables(); + AnnotatedTypeMirror returnType = unsubstitutedMethodType.getReturnType(); + AnnotatedTypeMirror methodReceiver = unsubstitutedMethodType.getReceiverType(); Map mappings = new IdentityHashMap<>(); @@ -166,16 +169,17 @@ public void viewpointAdaptMethod( mappings.put(methodReceiver, mr); } - declMethodType = + unsubstitutedMethodType = (AnnotatedExecutableType) - AnnotatedTypeCopierWithReplacement.replace(declMethodType, mappings); + AnnotatedTypeCopierWithReplacement.replace( + unsubstitutedMethodType, mappings); // Because we can't viewpoint adapt asMemberOf result, we adapt the declared method first, // and sets the corresponding parts to asMemberOf result - methodType.setReturnType(declMethodType.getReturnType()); - methodType.setReceiverType(declMethodType.getReceiverType()); - methodType.setParameterTypes(declMethodType.getParameterTypes()); - methodType.setTypeVariables(declMethodType.getTypeVariables()); + methodType.setReturnType(unsubstitutedMethodType.getReturnType()); + methodType.setReceiverType(unsubstitutedMethodType.getReceiverType()); + methodType.setParameterTypes(unsubstitutedMethodType.getParameterTypes()); + methodType.setTypeVariables(unsubstitutedMethodType.getTypeVariables()); } /** Check if the method invocation should be adapted. */ diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 9d5e35a570fa..ed0a0ab0655f 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -797,9 +797,9 @@ protected ViewpointAdapter createViewpointAdapter() { } /** - * Get {@code viewpointAdapter}. + * Get {@link #viewpointAdapter}. * - * @return {@code viewpointAdapter} + * @return {@link #viewpointAdapter} */ public ViewpointAdapter getViewpointAdapter() { return viewpointAdapter; @@ -2101,14 +2101,17 @@ public ParameterizedExecutableType methodFromUse( ExpressionTree tree, ExecutableElement methodElt, AnnotatedTypeMirror receiverType) { AnnotatedExecutableType memberType = getAnnotatedType(methodElt); // get unsubstituted type + + // since viewpoint adaption may introduce new poly annotation which should not be resolved, + // firstly do poly resolution methodFromUsePreSubstitution(tree, memberType); + if (viewpointAdapter != null) { + viewpointAdapter.viewpointAdaptMethod(receiverType, methodElt, memberType); + } AnnotatedExecutableType methodType = AnnotatedTypes.asMemberOf(types, this, receiverType, methodElt, memberType); List typeargs = new ArrayList<>(methodType.getTypeVariables().size()); - if (viewpointAdapter != null) { - viewpointAdapter.viewpointAdaptMethod(receiverType, methodElt, methodType); - } Map typeVarMapping = AnnotatedTypes.findTypeArguments(processingEnv, this, tree, methodElt, methodType); @@ -2241,8 +2244,13 @@ public ParameterizedExecutableType constructorFromUse(NewClassTree tree) { ExecutableElement ctor = TreeUtils.constructor(tree); AnnotatedTypeMirror type = fromNewClass(tree); addComputedTypeAnnotations(tree, type); + AnnotatedExecutableType con = getAnnotatedType(ctor); // get unsubstituted type + constructorFromUsePreSubstitution(tree, con); + if (viewpointAdapter != null) { + viewpointAdapter.viewpointAdaptConstructor(type, ctor, con); + } con = AnnotatedTypes.asMemberOf(types, this, type, ctor, con); @@ -2256,9 +2264,6 @@ && isSyntheticArgument(tree.getArguments().get(0))) { } List typeargs = new ArrayList<>(con.getTypeVariables().size()); - if (viewpointAdapter != null) { - viewpointAdapter.viewpointAdaptConstructor(type, ctor, con); - } Map typeVarMapping = AnnotatedTypes.findTypeArguments(processingEnv, this, tree, ctor, con); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java index 213e9278d1db..dc5c7974ff0d 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java @@ -771,28 +771,12 @@ public boolean containsUninferredTypeArguments() { /** The implementation of the visitor for #containsUninferredTypeArguments. */ private final SimpleAnnotatedTypeScanner uninferredTypeArgumentScanner = - new SimpleAnnotatedTypeScanner() { - @Override - protected Boolean defaultAction(AnnotatedTypeMirror type, Void aVoid) { - if (type.getKind() == TypeKind.WILDCARD) { - return ((AnnotatedWildcardType) type).isUninferredTypeArgument(); - } - return false; - } - - @Override - public Boolean reduce(Boolean r1, Boolean r2) { - if (r1 == null && r2 == null) { - return false; - } else if (r1 == null) { - return r2; - } else if (r2 == null) { - return r1; - } else { - return r1 || r2; - } - } - }; + new SimpleAnnotatedTypeScanner<>( + (type, p) -> + type.getKind() == TypeKind.WILDCARD + && ((AnnotatedWildcardType) type).isUninferredTypeArgument(), + Boolean::logicalOr, + false); /** * Create an {@link AnnotatedDeclaredType} with the underlying type of {@link Object}. It diff --git a/framework/src/main/java/org/checkerframework/framework/type/visitor/AnnotatedTypeReplacer.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeReplacer.java similarity index 97% rename from framework/src/main/java/org/checkerframework/framework/type/visitor/AnnotatedTypeReplacer.java rename to framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeReplacer.java index 0a51a2737d86..59cf98351ec3 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/visitor/AnnotatedTypeReplacer.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeReplacer.java @@ -1,10 +1,10 @@ -package org.checkerframework.framework.type.visitor; +package org.checkerframework.framework.type; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeKind; -import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; +import org.checkerframework.framework.type.visitor.AnnotatedTypeComparer; import org.checkerframework.javacutil.BugInCF; /** diff --git a/framework/src/main/java/org/checkerframework/framework/type/HashcodeAtmVisitor.java b/framework/src/main/java/org/checkerframework/framework/type/HashcodeAtmVisitor.java index 8b200a562215..e1f4fd696f30 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/HashcodeAtmVisitor.java +++ b/framework/src/main/java/org/checkerframework/framework/type/HashcodeAtmVisitor.java @@ -1,6 +1,6 @@ package org.checkerframework.framework.type; -import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner; +import org.checkerframework.framework.type.visitor.SimpleAnnotatedTypeScanner; /** * Computes the hashcode of an AnnotatedTypeMirror using the underlying type and primary annotations @@ -11,29 +11,11 @@ * @see org.checkerframework.framework.type.EqualityAtmComparer for more details. *

This is used by AnnotatedTypeMirror.hashcode. */ -public class HashcodeAtmVisitor extends AnnotatedTypeScanner { +public class HashcodeAtmVisitor extends SimpleAnnotatedTypeScanner { - /** - * Generates the hashcode of type and combines it with the hashcode of its component types (if - * any). - */ - @Override - protected Integer scan(AnnotatedTypeMirror type, Void v) { - return reduce(super.scan(type, null), generateHashcode(type)); - } - - /** Used to combine the hashcodes of component types or a type and its component types. */ - @Override - protected Integer reduce(Integer hashcode1, Integer hashcode2) { - if (hashcode1 == null) { - return hashcode2; - } - - if (hashcode2 == null) { - return hashcode1; - } - - return hashcode1 + hashcode2; + /** Creates a {@link HashcodeAtmVisitor}. */ + public HashcodeAtmVisitor() { + super(Integer::sum, 0); } /** @@ -42,11 +24,12 @@ protected Integer reduce(Integer hashcode1, Integer hashcode2) { * * @param type the type */ - private Integer generateHashcode(AnnotatedTypeMirror type) { + @Override + protected Integer defaultAction(AnnotatedTypeMirror type, Void v) { // To differentiate between partially initialized type's (which may have null components) // and fully initialized types, null values are allowed if (type == null) { - return null; + return 0; } return type.getAnnotations().toString().hashCode() * 17 diff --git a/framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java b/framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java index a3786ad8eebb..5ab445c456be 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java +++ b/framework/src/main/java/org/checkerframework/framework/type/TypeFromExpressionVisitor.java @@ -34,7 +34,6 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; -import org.checkerframework.framework.type.visitor.AnnotatedTypeReplacer; import org.checkerframework.framework.util.AnnotatedTypes; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.Pair; diff --git a/framework/src/main/java/org/checkerframework/framework/type/TypeFromTypeTreeVisitor.java b/framework/src/main/java/org/checkerframework/framework/type/TypeFromTypeTreeVisitor.java index 4f74b66438b3..7d609363c81f 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/TypeFromTypeTreeVisitor.java +++ b/framework/src/main/java/org/checkerframework/framework/type/TypeFromTypeTreeVisitor.java @@ -183,7 +183,8 @@ public AnnotatedTypeMirror visitPrimitiveType(PrimitiveTypeTree node, AnnotatedT } @Override - public AnnotatedTypeMirror visitTypeParameter(TypeParameterTree node, AnnotatedTypeFactory f) { + public AnnotatedTypeVariable visitTypeParameter( + TypeParameterTree node, AnnotatedTypeFactory f) { List bounds = new ArrayList<>(node.getBounds().size()); for (Tree t : node.getBounds()) { @@ -243,68 +244,57 @@ public AnnotatedTypeMirror visitWildcard(WildcardTree node, AnnotatedTypeFactory } /** - * Returns an AnnotatedTypeMirror for uses of type variables with annotations written explicitly - * on the type parameter declaration and/or its upper bound. + * If a tree is can be found for the declaration of the type variable {@code type}, then a + * {@link AnnotatedTypeVariable} is returned with explicit annotations from the type variables + * declared bounds. If a tree cannot be found, then {@code type}, converted to a use, is + * returned. * - *

Note for type variable uses in method signatures, explicit annotations on the declaration - * are added by {@link TypeFromMemberVisitor#typeVarAnnotator}. + * @param type type variable used to find declaration tree + * @param f annotated type factory + * @return the AnnotatedTypeVariable from the declaration of {@code type} or {@code type} if no + * tree is found. */ - private AnnotatedTypeMirror forTypeVariable(AnnotatedTypeMirror type, AnnotatedTypeFactory f) { - if (type.getKind() != TypeKind.TYPEVAR) { - throw new BugInCF( - "TypeFromTree.forTypeVariable: should only be called on type variables"); - } - TypeVariable typeVar = (TypeVariable) type.getUnderlyingType(); + private AnnotatedTypeVariable getTypeVariableFromDeclaration( + AnnotatedTypeVariable type, AnnotatedTypeFactory f) { + TypeVariable typeVar = type.getUnderlyingType(); TypeParameterElement tpe = (TypeParameterElement) typeVar.asElement(); Element elt = tpe.getGenericElement(); if (elt instanceof TypeElement) { TypeElement typeElt = (TypeElement) elt; int idx = typeElt.getTypeParameters().indexOf(tpe); ClassTree cls = (ClassTree) f.declarationFromElement(typeElt); - if (cls != null) { - // `forTypeVariable` is called for Identifier, MemberSelect and UnionType trees, - // none of which are declarations. But `cls.getTypeParameters()` returns a list - // of type parameter declarations (`TypeParameterTree`), so this recursive call - // to `visit` will return a declaration ATV. So we must copy the result and set - // its `isDeclaration` field to `false`. - if (cls.getTypeParameters().isEmpty()) { - // The type parameters in the source tree were already erased. - // The element already contains all necessary information and we can return - // that. - return type; - } - AnnotatedTypeMirror result = - visit(cls.getTypeParameters().get(idx), f).shallowCopy(); - ((AnnotatedTypeVariable) result).setDeclaration(false); - return result; - } else { - // We already have all info from the element -> nothing to do. - return type; + if (cls == null || cls.getTypeParameters().isEmpty()) { + // The type parameters in the source tree were already erased. The element already + // contains all necessary information and we can return that. + return type.asUse(); } + + // `forTypeVariable` is called for Identifier, MemberSelect and UnionType trees, + // none of which are declarations. But `cls.getTypeParameters()` returns a list + // of type parameter declarations (`TypeParameterTree`), so this call + // will return a declaration ATV. So change it to a use. + return visitTypeParameter(cls.getTypeParameters().get(idx), f).asUse(); } else if (elt instanceof ExecutableElement) { ExecutableElement exElt = (ExecutableElement) elt; int idx = exElt.getTypeParameters().indexOf(tpe); MethodTree meth = (MethodTree) f.declarationFromElement(exElt); - if (meth != null) { - // This works the same as the case above. Even though `meth` itself is not a - // type declaration tree, the elements of `meth.getTypeParameters()` still are. - AnnotatedTypeMirror result = - visit(meth.getTypeParameters().get(idx), f).shallowCopy(); - ((AnnotatedTypeVariable) result).setDeclaration(false); - return result; - } else { + if (meth == null) { // throw new BugInCF("TypeFromTree.forTypeVariable: did not find source for: " // + elt); - return type; + return type.asUse(); } - } else { + // This works the same as the case above. Even though `meth` itself is not a + // type declaration tree, the elements of `meth.getTypeParameters()` still are. + AnnotatedTypeVariable result = + visitTypeParameter(meth.getTypeParameters().get(idx), f).shallowCopy(); + result.setDeclaration(false); + return result; + } else if (TypesUtils.isCaptured(typeVar)) { // Captured types can have a generic element (owner) that is // not an element at all, namely Symtab.noSymbol. - if (TypesUtils.isCaptured(typeVar)) { - return type; - } else { - throw new BugInCF("TypeFromTree.forTypeVariable: not a supported element: " + elt); - } + return type.asUse(); + } else { + throw new BugInCF("TypeFromTree.forTypeVariable: not a supported element: " + elt); } } @@ -314,7 +304,7 @@ public AnnotatedTypeMirror visitIdentifier(IdentifierTree node, AnnotatedTypeFac AnnotatedTypeMirror type = f.type(node); if (type.getKind() == TypeKind.TYPEVAR) { - return forTypeVariable(type, f).asUse(); + return getTypeVariableFromDeclaration((AnnotatedTypeVariable) type, f); } return type; @@ -326,7 +316,7 @@ public AnnotatedTypeMirror visitMemberSelect(MemberSelectTree node, AnnotatedTyp AnnotatedTypeMirror type = f.type(node); if (type.getKind() == TypeKind.TYPEVAR) { - return forTypeVariable(type, f).asUse(); + return getTypeVariableFromDeclaration((AnnotatedTypeVariable) type, f); } return type; @@ -337,7 +327,7 @@ public AnnotatedTypeMirror visitUnionType(UnionTypeTree node, AnnotatedTypeFacto AnnotatedTypeMirror type = f.type(node); if (type.getKind() == TypeKind.TYPEVAR) { - return forTypeVariable(type, f).asUse(); + return getTypeVariableFromDeclaration((AnnotatedTypeVariable) type, f); } return type; @@ -349,7 +339,7 @@ public AnnotatedTypeMirror visitIntersectionType( AnnotatedTypeMirror type = f.type(node); if (type.getKind() == TypeKind.TYPEVAR) { - return forTypeVariable(type, f).asUse(); + return getTypeVariableFromDeclaration((AnnotatedTypeVariable) type, f); } return type; diff --git a/framework/src/main/java/org/checkerframework/framework/type/TypeHierarchy.java b/framework/src/main/java/org/checkerframework/framework/type/TypeHierarchy.java index 6787074d68ba..027485fa3c75 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/TypeHierarchy.java +++ b/framework/src/main/java/org/checkerframework/framework/type/TypeHierarchy.java @@ -69,8 +69,8 @@ public interface TypeHierarchy { * @param supertype possible supertype * @param top the qualifier at the top of the hierarchy for which the subtype check should be * preformed - * @return returns true if {@code subtype} is a subtype of {@code supertype} in the qualifier - * hierarchy whose top is {@code top} + * @return true if {@code subtype} is a subtype of {@code supertype} in the qualifier hierarchy + * whose top is {@code top} */ boolean isSubtype( AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype, AnnotationMirror top); diff --git a/framework/src/main/java/org/checkerframework/framework/type/TypesIntoElements.java b/framework/src/main/java/org/checkerframework/framework/type/TypesIntoElements.java index 51ca0eb6c16b..d3216f193d92 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/TypesIntoElements.java +++ b/framework/src/main/java/org/checkerframework/framework/type/TypesIntoElements.java @@ -25,8 +25,6 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedIntersectionType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedNoType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedNullType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedUnionType; @@ -304,9 +302,16 @@ private static List generateTypeCompounds( private static class TCConvert extends AnnotatedTypeScanner, TypeAnnotationPosition> { + /** ProcessEnvironment */ private final ProcessingEnvironment processingEnv; + /** + * Creates a {@link TCConvert}. + * + * @param processingEnv ProcessEnvironment + */ TCConvert(ProcessingEnvironment processingEnv) { + super(List.nil()); this.processingEnv = processingEnv; } @@ -319,15 +324,6 @@ public List scan(AnnotatedTypeMirror type, TypeAnnotationPosition return res; } - @Override - protected List scan( - Iterable types, TypeAnnotationPosition pos) { - if (types == null) { - return List.nil(); - } - return super.scan(types, pos); - } - @Override public List reduce(List r1, List r2) { if (r1 == null) { @@ -521,15 +517,5 @@ public List visitWildcard( visitedNodes.put(type, res); return res; } - - @Override - public List visitNoType(AnnotatedNoType type, TypeAnnotationPosition tapos) { - return List.nil(); - } - - @Override - public List visitNull(AnnotatedNullType type, TypeAnnotationPosition tapos) { - return List.nil(); - } } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java b/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java index b1310c3bb898..e02c00e7ff23 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java +++ b/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java @@ -3,6 +3,7 @@ import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.NewClassTree; import com.sun.source.util.TreePath; +import com.sun.tools.javac.code.Type; import java.util.ArrayList; import java.util.Collections; import java.util.IdentityHashMap; @@ -13,6 +14,7 @@ import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; @@ -25,8 +27,8 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedUnionType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; import org.checkerframework.framework.type.QualifierHierarchy; -import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner; import org.checkerframework.framework.type.visitor.EquivalentAtmComboScanner; +import org.checkerframework.framework.type.visitor.SimpleAnnotatedTypeScanner; import org.checkerframework.framework.util.AnnotatedTypes; import org.checkerframework.framework.util.AnnotationMirrorMap; import org.checkerframework.framework.util.AnnotationMirrorSet; @@ -78,14 +80,13 @@ public abstract class AbstractQualifierPolymorphism implements QualifierPolymorp private PolyCollector collector = new PolyCollector(); /** Resolves each polymorphic qualifier by replacing it with its instantiation. */ - private AnnotatedTypeScanner> replacer = - new Replacer(); + private final SimpleAnnotatedTypeScanner> replacer; /** * Completes a type by removing any unresolved polymorphic qualifiers, replacing them with the * bottom qualifiers. */ - private Completer completer = new Completer(); + private final SimpleAnnotatedTypeScanner completer; /** * Creates an {@link AbstractQualifierPolymorphism} instance that uses the given checker for @@ -100,6 +101,34 @@ protected AbstractQualifierPolymorphism( this.atypeFactory = factory; this.qualHierarchy = factory.getQualifierHierarchy(); this.topQuals = new AnnotationMirrorSet(qualHierarchy.getTopAnnotations()); + + this.completer = + new SimpleAnnotatedTypeScanner<>( + (type, p) -> { + for (Map.Entry entry : + polyQuals.entrySet()) { + AnnotationMirror poly = entry.getKey(); + AnnotationMirror top = entry.getValue(); + if (type.hasAnnotation(poly)) { + type.removeAnnotation(poly); + if (type.getKind() != TypeKind.TYPEVAR + && type.getKind() != TypeKind.WILDCARD) { + // Do not add qualifiers to type variables and + // wildcards + type.addAnnotation( + this.qualHierarchy.getBottomAnnotation(top)); + } + } + } + return null; + }); + + this.replacer = + new SimpleAnnotatedTypeScanner<>( + (type, map) -> { + replace(type, map); + return null; + }); } /** @@ -137,7 +166,7 @@ public void resolve(MethodInvocationTree tree, AnnotatedExecutableType type) { List arguments = AnnotatedTypes.getAnnotatedTypes(atypeFactory, parameters, tree.getArguments()); - AnnotationMirrorMap instantiationMapping = + AnnotationMirrorMap instantiationMapping = collector.visit(arguments, parameters); // For super() and this() method calls, getReceiverType(tree) does not return the correct @@ -153,18 +182,38 @@ public void resolve(MethodInvocationTree tree, AnnotatedExecutableType type) { atypeFactory.getReceiverType(tree), type.getReceiverType())); } + // receiver-sensitive poly resolution: resolve return value with assignment context l-value TreePath path = atypeFactory.getPath(tree); if (path != null) { AnnotatedTypeMirror assignmentContext = QualifierPolymorphismUtil.assignedTo(atypeFactory, path); if (assignmentContext != null) { - instantiationMapping = - collector.reduceWithUpperBounds( - instantiationMapping, - collector.visit( - // Actual assignment lhs type - assignmentContext, type.getReturnType(), true)); + // get erased subtype relation + TypeMirror javaLhstype = + atypeFactory.types.erasure(assignmentContext.getUnderlyingType()); + TypeMirror javaReturntype = + atypeFactory.types.erasure(type.getReturnType().getUnderlyingType()); + // primitive types need special care + boolean polyIsSub = + javaReturntype instanceof Type.JCPrimitiveType + || atypeFactory.types.isSubtype(javaReturntype, javaLhstype); + + boolean polyIsSuper = + !(javaReturntype instanceof Type.ArrayType) + && // isSubtype cannot handle this + atypeFactory.types.isSubtype(javaLhstype, javaReturntype); + + // only perform receiver-sensitive poly resolution when return type is erased + // subtype of lhs + if (polyIsSub || polyIsSuper) { // lhs and return type are comparable + instantiationMapping = + collector.reduceWithUpperBounds( + instantiationMapping, + collector.visit( + // Actual assignment lhs type + assignmentContext, type.getReturnType(), polyIsSub)); + } } } @@ -186,7 +235,7 @@ public void resolve(NewClassTree tree, AnnotatedExecutableType type) { List arguments = AnnotatedTypes.getAnnotatedTypes(atypeFactory, parameters, tree.getArguments()); - AnnotationMirrorMap instantiationMapping = + AnnotationMirrorMap instantiationMapping = collector.visit(arguments, parameters); // TODO: poly on receiver for constructors? // instantiationMapping = collector.reduce(instantiationMapping, @@ -210,7 +259,7 @@ public void resolve( return; } } - AnnotationMirrorMap instantiationMapping; + AnnotationMirrorMap instantiationMapping; List parameters = memberReference.getParameterTypes(); List args = functionalInterface.getParameterTypes(); @@ -252,21 +301,26 @@ public void resolve( } /** - * If the primary annotation of {@code actualType} is a polymorphic qualifier, then it is mapped + * If the primary annotation of {@code polyType} is a polymorphic qualifier, then it is mapped * to the primary annotation of {@code type} and the map is returned. Otherwise, an empty map is * returned. + * + * @param type type with qualifier to us in the map + * @param polyType type that may have polymorphic qualifiers + * @return a mapping from the polymorphic qualifiers in {@code polyType} to the qualifiers in + * {@code type} */ - private AnnotationMirrorMap mapQualifierToPoly( - AnnotatedTypeMirror type, AnnotatedTypeMirror actualType) { - AnnotationMirrorMap result = new AnnotationMirrorMap<>(); + private AnnotationMirrorMap mapQualifierToPoly( + AnnotatedTypeMirror type, AnnotatedTypeMirror polyType) { + AnnotationMirrorMap result = new AnnotationMirrorMap<>(); for (Map.Entry kv : polyQuals.entrySet()) { AnnotationMirror top = kv.getValue(); AnnotationMirror poly = kv.getKey(); - if (actualType.hasAnnotation(poly)) { + if (polyType.hasAnnotation(poly)) { AnnotationMirror typeQual = type.getAnnotationInHierarchy(top); if (typeQual != null) { - result.put(poly, AnnotationMirrorSet.singleElementSet(typeQual)); + result.put(poly, typeQual); } } } @@ -274,20 +328,19 @@ private AnnotationMirrorMap mapQualifierToPoly( } /** - * Returns an annotation set that is the merge of the two sets of annotations. The sets are + * Returns annotation that is the combination of the two annotations. The annotations are * instantiations for {@code polyQual}. * *

The combination is typically their least upper bound. (It could be the GLB in the case * that all arguments to a polymorphic method must have the same annotation.) * - * @param polyQual polymorphic qualifier for which {@code a1Annos} and {@code a2Annos} are - * instantiations - * @param a1Annos a set that is an instantiation of {@code polyQual} - * @param a2Annos a set that is an instantiation of {@code polyQual} - * @return the merge of the two sets + * @param polyQual polymorphic qualifier for which {@code a1} and {@code a2} are instantiations + * @param a1 an annotation that is an instantiation of {@code polyQual} + * @param a2 an annotation that is an instantiation of {@code polyQual} + * @return an annotation that is the combination of the two annotations */ - protected abstract AnnotationMirrorSet combine( - AnnotationMirror polyQual, AnnotationMirrorSet a1Annos, AnnotationMirrorSet a2Annos); + protected abstract AnnotationMirror combine( + AnnotationMirror polyQual, AnnotationMirror a1, AnnotationMirror a2); /** * Replaces the top-level polymorphic annotations in {@code type} with the instantiations in @@ -300,48 +353,14 @@ protected abstract AnnotationMirrorSet combine( * @param replacements mapping from polymorphic annotation to instantiation */ protected abstract void replace( - AnnotatedTypeMirror type, AnnotationMirrorMap replacements); - - /** Replaces each polymorphic qualifier with its instantiation. */ - class Replacer extends AnnotatedTypeScanner> { - @Override - public Void scan( - AnnotatedTypeMirror type, AnnotationMirrorMap replacements) { - replace(type, replacements); - return super.scan(type, replacements); - } - } - - /** - * Completes a type by removing any unresolved polymorphic qualifiers, replacing them with the - * top qualifiers. - */ - class Completer extends AnnotatedTypeScanner { - @Override - protected Void scan(AnnotatedTypeMirror type, Void p) { - for (Map.Entry pqentry : polyQuals.entrySet()) { - AnnotationMirror top = pqentry.getValue(); - AnnotationMirror poly = pqentry.getKey(); - - if (type.hasAnnotation(poly)) { - type.removeAnnotation(poly); - if (type.getKind() != TypeKind.TYPEVAR && type.getKind() != TypeKind.WILDCARD) { - // Do not add qualifiers to type variables and wildcards - type.addAnnotation(qualHierarchy.getBottomAnnotation(top)); - } - } - } - return super.scan(type, p); - } - } + AnnotatedTypeMirror type, AnnotationMirrorMap replacements); /** * A helper class that resolves the polymorphic qualifiers with the most restrictive qualifier. - * It returns a mapping from the polymorphic qualifier to the substitution for that qualifier, - * which is a set of qualifiers. For most polymorphic qualifiers this will be a singleton set. + * It returns a mapping from the polymorphic qualifier to the substitution for that qualifier. */ private class PolyCollector - extends EquivalentAtmComboScanner, Void> { + extends EquivalentAtmComboScanner, Void> { /** * Set of {@link AnnotatedTypeVariable} or {@link AnnotatedWildcardType} that have been @@ -349,7 +368,7 @@ private class PolyCollector * *

Uses reference equality rather than equals because the visitor may visit two types * that are structurally equal, but not actually the same. For example, the wildcards in - * Pair may be equal, but they both should be visited. + * {@code Pair} may be equal, but they both should be visited. */ private final Set visitedTypes = Collections.newSetFromMap(new IdentityHashMap<>()); @@ -363,15 +382,15 @@ private boolean visited(AnnotatedTypeMirror atm) { } @Override - protected AnnotationMirrorMap scanWithNull( + protected AnnotationMirrorMap scanWithNull( AnnotatedTypeMirror type1, AnnotatedTypeMirror type2, Void aVoid) { return new AnnotationMirrorMap<>(); } @Override - public AnnotationMirrorMap reduce( - AnnotationMirrorMap r1, - AnnotationMirrorMap r2) { + public AnnotationMirrorMap reduce( + AnnotationMirrorMap r1, + AnnotationMirrorMap r2) { if (r1 == null || r1.isEmpty()) { return r2; @@ -380,15 +399,15 @@ public AnnotationMirrorMap reduce( return r1; } - AnnotationMirrorMap res = new AnnotationMirrorMap<>(); + AnnotationMirrorMap res = new AnnotationMirrorMap<>(); // Ensure that all qualifiers from r1 and r2 are visited. AnnotationMirrorSet r2remain = new AnnotationMirrorSet(); r2remain.addAll(r2.keySet()); - for (Map.Entry entry : r1.entrySet()) { + for (Map.Entry entry : r1.entrySet()) { AnnotationMirror polyQual = entry.getKey(); - AnnotationMirrorSet a1Annos = entry.getValue(); - AnnotationMirrorSet a2Annos = r2.get(polyQual); - if (a2Annos == null || a2Annos.isEmpty()) { + AnnotationMirror a1Annos = entry.getValue(); + AnnotationMirror a2Annos = r2.get(polyQual); + if (a2Annos == null) { res.put(polyQual, a1Annos); } else { res.put(polyQual, combine(polyQual, a1Annos, a2Annos)); @@ -404,13 +423,13 @@ public AnnotationMirrorMap reduce( /** * Reduces lower bounds r1 with upper bounds r2. * - * @param r1 a map from {@link AnnotationMirror} to {@link AnnotationMirrorSet} - * @param r2 a map from {@link AnnotationMirror} to {@link AnnotationMirrorSet} + * @param r1 a map from {@link AnnotationMirror} to {@link AnnotationMirror} + * @param r2 a map from {@link AnnotationMirror} to {@link AnnotationMirror} * @return the reduced {@link AnnotationMirrorMap} */ - private AnnotationMirrorMap reduceWithUpperBounds( - AnnotationMirrorMap r1, - AnnotationMirrorMap r2) { + private AnnotationMirrorMap reduceWithUpperBounds( + AnnotationMirrorMap r1, + AnnotationMirrorMap r2) { if (r1 == null || r1.isEmpty()) { return r2; @@ -419,29 +438,27 @@ private AnnotationMirrorMap reduceWithUpperBounds( return r1; } - AnnotationMirrorMap res = new AnnotationMirrorMap<>(); + AnnotationMirrorMap res = new AnnotationMirrorMap<>(); // Ensure that all qualifiers from r1 and r2 are visited. AnnotationMirrorSet r2remain = new AnnotationMirrorSet(); r2remain.addAll(r2.keySet()); - for (Map.Entry kv1 : r1.entrySet()) { + for (Map.Entry kv1 : r1.entrySet()) { AnnotationMirror key1 = kv1.getKey(); - AnnotationMirrorSet a1Annos = kv1.getValue(); - AnnotationMirrorSet a2Annos = r2.get(key1); - if (a2Annos != null && !a2Annos.isEmpty()) { + AnnotationMirror a1Anno = kv1.getValue(); + AnnotationMirror a2Anno = r2.get(key1); + if (a2Anno != null) { r2remain.remove(key1); - AnnotationMirrorSet subres = new AnnotationMirrorSet(); + AnnotationMirror subres = null; for (AnnotationMirror top : topQuals) { - AnnotationMirror a1 = qualHierarchy.findAnnotationInHierarchy(a1Annos, top); - AnnotationMirror a2 = qualHierarchy.findAnnotationInHierarchy(a2Annos, top); - if (a1 != null) { - subres.add(a1); - } else if (a2 != null) { - subres.add(a2); + if (qualHierarchy.isSubtype(a1Anno, top)) { + subres = a1Anno; + } else if (qualHierarchy.isSubtype(a2Anno, top)) { + subres = a2Anno; } } res.put(key1, subres); } else { - res.put(key1, a1Annos); + res.put(key1, a1Anno); } } for (AnnotationMirror key2 : r2remain) { @@ -453,11 +470,15 @@ private AnnotationMirrorMap reduceWithUpperBounds( /** * Calls {@link #visit(AnnotatedTypeMirror, AnnotatedTypeMirror)} for each type in {@code * types}. + * + * @param types AnnotateTypeMirrors used to find instantiations + * @param polyTypes AnnotatedTypeMirrors that may have polymorphic qualifiers + * @return a mapping of polymorphic qualifiers to their instantiations */ - private AnnotationMirrorMap visit( + private AnnotationMirrorMap visit( Iterable types, Iterable polyTypes) { - AnnotationMirrorMap result = new AnnotationMirrorMap<>(); + AnnotationMirrorMap result = new AnnotationMirrorMap<>(); Iterator itert = types.iterator(); Iterator itera = polyTypes.iterator(); @@ -490,7 +511,7 @@ private AnnotationMirrorMap visit( * type} * @return a mapping of polymorphic qualifiers to their instantiations */ - private AnnotationMirrorMap visit( + private AnnotationMirrorMap visit( AnnotatedTypeMirror type, AnnotatedTypeMirror polyType, boolean polyIsSub) { if (type.getKind() == TypeKind.NULL) { return mapQualifierToPoly(type, polyType); @@ -537,7 +558,7 @@ private AnnotationMirrorMap visit( * @param polyType AnnotatedTypeMirror that may have polymorphic qualifiers * @return {@code visit(type, polyType, false)} */ - private AnnotationMirrorMap visit( + private AnnotationMirrorMap visit( AnnotatedTypeMirror type, AnnotatedTypeMirror polyType) { return visit(type, polyType, false); } @@ -551,21 +572,21 @@ protected String defaultErrorMessage( } @Override - public AnnotationMirrorMap visitArray_Array( + public AnnotationMirrorMap visitArray_Array( AnnotatedArrayType type1, AnnotatedArrayType type2, Void aVoid) { - AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); + AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); return reduce(result, super.visitArray_Array(type1, type2, aVoid)); } @Override - public AnnotationMirrorMap visitDeclared_Declared( + public AnnotationMirrorMap visitDeclared_Declared( AnnotatedDeclaredType type1, AnnotatedDeclaredType type2, Void aVoid) { // Don't call super because asSuper has to be called on each type argument. if (visited(type2)) { return new AnnotationMirrorMap<>(); } - AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); + AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); Iterator type2Args = type2.getTypeArguments().iterator(); for (AnnotatedTypeMirror type1Arg : type1.getTypeArguments()) { @@ -582,48 +603,48 @@ public AnnotationMirrorMap visitDeclared_Declared( } @Override - public AnnotationMirrorMap visitIntersection_Intersection( + public AnnotationMirrorMap visitIntersection_Intersection( AnnotatedIntersectionType type1, AnnotatedIntersectionType type2, Void aVoid) { - AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); + AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); return reduce(result, super.visitIntersection_Intersection(type1, type2, aVoid)); } @Override - public AnnotationMirrorMap visitNull_Null( + public AnnotationMirrorMap visitNull_Null( AnnotatedNullType type1, AnnotatedNullType type2, Void aVoid) { return mapQualifierToPoly(type1, type2); } @Override - public AnnotationMirrorMap visitPrimitive_Primitive( + public AnnotationMirrorMap visitPrimitive_Primitive( AnnotatedPrimitiveType type1, AnnotatedPrimitiveType type2, Void aVoid) { return mapQualifierToPoly(type1, type2); } @Override - public AnnotationMirrorMap visitTypevar_Typevar( + public AnnotationMirrorMap visitTypevar_Typevar( AnnotatedTypeVariable type1, AnnotatedTypeVariable type2, Void aVoid) { if (visited(type2)) { return new AnnotationMirrorMap<>(); } - AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); + AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); return reduce(result, super.visitTypevar_Typevar(type1, type2, aVoid)); } @Override - public AnnotationMirrorMap visitUnion_Union( + public AnnotationMirrorMap visitUnion_Union( AnnotatedUnionType type1, AnnotatedUnionType type2, Void aVoid) { - AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); + AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); return reduce(result, super.visitUnion_Union(type1, type2, aVoid)); } @Override - public AnnotationMirrorMap visitWildcard_Wildcard( + public AnnotationMirrorMap visitWildcard_Wildcard( AnnotatedWildcardType type1, AnnotatedWildcardType type2, Void aVoid) { if (visited(type2)) { return new AnnotationMirrorMap<>(); } - AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); + AnnotationMirrorMap result = mapQualifierToPoly(type1, type2); return reduce(result, super.visitWildcard_Wildcard(type1, type2, aVoid)); } diff --git a/framework/src/main/java/org/checkerframework/framework/type/poly/DefaultQualifierPolymorphism.java b/framework/src/main/java/org/checkerframework/framework/type/poly/DefaultQualifierPolymorphism.java index 37a4faef09aa..9c992b3de9b2 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/poly/DefaultQualifierPolymorphism.java +++ b/framework/src/main/java/org/checkerframework/framework/type/poly/DefaultQualifierPolymorphism.java @@ -6,7 +6,6 @@ import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.util.AnnotationMirrorMap; -import org.checkerframework.framework.util.AnnotationMirrorSet; /** * Default implementation of {@link AbstractQualifierPolymorphism}. The polymorphic qualifiers for a @@ -35,47 +34,26 @@ public DefaultQualifierPolymorphism(ProcessingEnvironment env, AnnotatedTypeFact @Override protected void replace( - AnnotatedTypeMirror type, AnnotationMirrorMap replacements) { - for (Map.Entry pqentry : replacements.entrySet()) { + AnnotatedTypeMirror type, AnnotationMirrorMap replacements) { + for (Map.Entry pqentry : replacements.entrySet()) { AnnotationMirror poly = pqentry.getKey(); if (type.hasAnnotation(poly)) { type.removeAnnotation(poly); - AnnotationMirrorSet quals = pqentry.getValue(); - type.replaceAnnotations(quals); + AnnotationMirror quals = pqentry.getValue(); + type.replaceAnnotation(quals); } } } - /** - * Returns the lub of the two sets. - * - * @param polyQual polymorphic qualifier for which {@code a1Annos} and {@code a2Annos} are - * instantiations - * @param a1Annos a set that is an instantiation of {@code polyQual}, or null - * @param a2Annos a set that is an instantiation of {@code polyQual}, or null - * @return the lub of the two sets - */ + /** Combines the two annotations using the least upper bound. */ @Override - protected AnnotationMirrorSet combine( - AnnotationMirror polyQual, AnnotationMirrorSet a1Annos, AnnotationMirrorSet a2Annos) { - if (a1Annos == null) { - if (a2Annos == null) { - return new AnnotationMirrorSet(); - } - return a2Annos; - } else if (a2Annos == null) { - return a1Annos; - } - - AnnotationMirrorSet lubSet = new AnnotationMirrorSet(); - for (AnnotationMirror top : topQuals) { - AnnotationMirror a1 = qualHierarchy.findAnnotationInHierarchy(a1Annos, top); - AnnotationMirror a2 = qualHierarchy.findAnnotationInHierarchy(a2Annos, top); - AnnotationMirror lub = qualHierarchy.leastUpperBoundTypeVariable(a1, a2); - if (lub != null) { - lubSet.add(lub); - } + protected AnnotationMirror combine( + AnnotationMirror polyQual, AnnotationMirror a1, AnnotationMirror a2) { + if (a1 == null) { + return a2; + } else if (a2 == null) { + return a1; } - return lubSet; + return qualHierarchy.leastUpperBoundTypeVariable(a1, a2); } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/visitor/AnnotatedTypeScanner.java b/framework/src/main/java/org/checkerframework/framework/type/visitor/AnnotatedTypeScanner.java index f67a7e5f6e87..4d1766d05c31 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/visitor/AnnotatedTypeScanner.java +++ b/framework/src/main/java/org/checkerframework/framework/type/visitor/AnnotatedTypeScanner.java @@ -2,6 +2,7 @@ import java.util.IdentityHashMap; import java.util.Map; +import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; @@ -15,38 +16,60 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; /** - * A TypeVisitor that visits all the child tree nodes. To visit types of a particular type, just - * override the corresponding visitXYZ method. Inside your method, call super.visitXYZ to visit - * descendant nodes. + * An {@code AnnotatedTypeScanner} visits an {@link AnnotatedTypeMirror} and all of its child {@link + * AnnotatedTypeMirror} and preforms some function depending on the kind of type. A {@link + * SimpleAnnotatedTypeScanner} scans an {@link AnnotatedTypeMirror} and preforms the same function + * regardless of the kind of type. The function returns some value with type {@link R} and takes an + * argument of type {@link P}. If the function does not return any value, then {@code R} should be + * {@link Void}. If the function takes not arguments, then {@code P} should be {@link Void}. * - *

The default implementation of the visitXYZ methods will determine a result as follows: + *

The default implementation of the visitAnnotatedTypeMirror methods will determine a result as + * follows: * *

    - *
  • If the node being visited has no children, the result will be null. - *
  • If the node being visited has one child, the result will be the result of calling scan on - * that child. The child may be a simple node or itself a list of nodes. - *
  • If the node being visited has more than one child, the result will be determined by calling - * scan each child in turn, and then combining the result of each scan after the first with - * the cumulative result so far, as determined by the reduce(R, R) method. Each child may be - * either a simple node or a list of nodes. The default behavior of the reduce method is such - * that the result of the visitXYZ method will be the result of the last child scanned. + *
  • If the type being visited has no children, the {@link #defaultResult} is returned. + *
  • If the type being visited has one child, the result of visiting the child type is returned. + *
  • If the type being visited has more than one child, the result is determined by visiting + * each child in turn, and then combining the result of each with the cumulative result so + * far, as determined by the {@link #reduce} method. *
* - * Here is an example to count the parameter types number of nodes in a tree: + * The {@link #reduce} method combines the results of visiting child types. It can be specified by + * passing an {@link Reduce} object to one of the constructors or by overriding the method directly. + * If it is not otherwise specified, the reduce returns the first result if it is not null; + * otherwise, the second result is returned. If the default result is nonnull and reduce never + * returns null, then both parameters passed to reduce will be nonnull. * - *

- * class CountTypeVariable extends TreeScanner {
+ * 

When overriding a visitAnnotatedTypeMirror method, the returned expression should be {@code + * reduce(super.visitAnnotatedTypeMirror(type, parameter), result)} so that the whole type is + * scanned. * - * {@literal @}Override - * public Integer visitTypeVariable(ATypeVariable node, Void p) { - * return 1; - * } + *

To begin scanning a type call {@link #visit(AnnotatedTypeMirror, Object)} or to pass {@code + * null} as the last parameter, call {@link #visit(AnnotatedTypeMirror)}. Both methods call {@link + * #reset()}. + * + *

Here is an example of a scanner that counts the number of {@link AnnotatedTypeVariable} in an + * AnnotatedTypeMirror. + * + *

+ * {@code class CountTypeVariable extends AnnotatedTypeScanner} {
+ *    public CountTypeVariable() {
+ *        super(Integer::sum, 0);
+ *    }
  *
  *    {@literal @}Override
- *     public Integer reduce(Integer r1, Integer r2) {
- *         return (r1 == null ? 0 : r1) + (r2 == null ? 0 : r2);
+ *     public Integer visitTypeVariable(AnnotatedTypeVariable type, Void p) {
+ *         return reduce(super.visitTypeVariable(type, p), 1);
  *     }
  * }
+ * 
+ * + * Below is an example of how to use {@code CountTypeVariable} + * + *

+ * void method(AnnotatedTypeMirror type) {
+ *     int count = new CountTypeVariable().visit(type);
+ * }
  * 
* * @param the return type of this visitor's methods. Use Void for visitors that do not need to @@ -54,7 +77,79 @@ * @param

the type of the additional parameter to this visitor's methods. Use Void for visitors * that do not need an additional parameter. */ -public class AnnotatedTypeScanner implements AnnotatedTypeVisitor { +public abstract class AnnotatedTypeScanner implements AnnotatedTypeVisitor { + + /** + * Reduces two results into a single result. + * + * @param the result type + */ + @FunctionalInterface + public interface Reduce { + + /** + * Returns the combination of two results. + * + * @param r1 the first result + * @param r2 the second result + * @return the combination of the two results + */ + R reduce(R r1, R r2); + } + + /** The reduce function to use. */ + protected final Reduce reduceFunction; + + /** The result to return if no other result is provided. It should be immutable. */ + protected final R defaultResult; + + /** + * Constructs an AnnotatedTypeScanner with the given reduce function. If {@code reduceFunction} + * is null, then the reduce function returns the first result if it is nonnull; otherwise the + * second result is returned. + * + * @param reduceFunction function used to combine two results + * @param defaultResult the result to return if a visit type method is not overridden; it should + * be immutable. + */ + protected AnnotatedTypeScanner(@Nullable Reduce reduceFunction, R defaultResult) { + if (reduceFunction == null) { + this.reduceFunction = (r1, r2) -> r1 == null ? r2 : r1; + } else { + this.reduceFunction = reduceFunction; + } + this.defaultResult = defaultResult; + } + + /** + * Constructs an AnnotatedTypeScanner with the given reduce function. If {@code reduceFunction} + * is null, then the reduce function returns the first result if it is nonnull; otherwise the + * second result is returned. The default result is {@code null} + * + * @param reduceFunction function used to combine two results + */ + protected AnnotatedTypeScanner(@Nullable Reduce reduceFunction) { + this(reduceFunction, null); + } + + /** + * Constructs an AnnotatedTypeScanner where the reduce function returns the first result if it + * is nonnull; otherwise the second result is returned. + * + * @param defaultResult the result to return if a visit type method is not overridden; it should + * be immutable. + */ + protected AnnotatedTypeScanner(R defaultResult) { + this(null, defaultResult); + } + + /** + * Constructs an AnnotatedTypeScanner where the reduce function returns the first result if it + * is nonnull; otherwise the second result is returned. The default result is {@code null}. + */ + protected AnnotatedTypeScanner() { + this(null, null); + } // To prevent infinite loops protected final Map visitedNodes = new IdentityHashMap<>(); @@ -110,11 +205,11 @@ protected R scan(AnnotatedTypeMirror type, P p) { * @param p the parameter to use * @return the reduced result of scanning all the types */ - protected R scan(Iterable types, P p) { + protected R scan(@Nullable Iterable types, P p) { if (types == null) { - return null; + return defaultResult; } - R r = null; + R r = defaultResult; boolean first = true; for (AnnotatedTypeMirror type : types) { r = (first ? scan(type, p) : scanAndReduce(type, p, r)); @@ -143,31 +238,38 @@ protected R scanAndReduce(AnnotatedTypeMirror type, P p, R r) { * Combines {@code r1} and {@code r2} and returns the result. The default implementation returns * {@code r1} if it is not null; otherwise, it returns {@code r2}. * - * @param r1 a result of scan - * @param r2 a result of scan + * @param r1 a result of scan, nonnull if {@link #defaultResult} is nonnull and this method + * never returns null + * @param r2 a result of scan, nonnull if {@link #defaultResult} is nonnull and this method + * never returns null * @return the combination of {@code r1} and {@code r2} */ protected R reduce(R r1, R r2) { - if (r1 == null) { - return r2; - } - return r1; + return reduceFunction.reduce(r1, r2); } @Override public R visitDeclared(AnnotatedDeclaredType type, P p) { - if (!type.getTypeArguments().isEmpty()) { - // Only declared types with type arguments might be recursive. - if (visitedNodes.containsKey(type)) { - return visitedNodes.get(type); - } - visitedNodes.put(type, null); + // Only declared types with type arguments might be recursive, + // so only store those. + boolean shouldStoreType = !type.getTypeArguments().isEmpty(); + if (shouldStoreType && visitedNodes.containsKey(type)) { + return visitedNodes.get(type); } - R r = null; + if (shouldStoreType) { + visitedNodes.put(type, defaultResult); + } + R r = defaultResult; if (type.getEnclosingType() != null) { - scan(type.getEnclosingType(), p); + r = scan(type.getEnclosingType(), p); + if (shouldStoreType) { + visitedNodes.put(type, r); + } } r = scanAndReduce(type.getTypeArguments(), p, r); + if (shouldStoreType) { + visitedNodes.put(type, r); + } return r; } @@ -176,8 +278,9 @@ public R visitIntersection(AnnotatedIntersectionType type, P p) { if (visitedNodes.containsKey(type)) { return visitedNodes.get(type); } - visitedNodes.put(type, null); + visitedNodes.put(type, defaultResult); R r = scan(type.directSuperTypes(), p); + visitedNodes.put(type, r); return r; } @@ -186,8 +289,9 @@ public R visitUnion(AnnotatedUnionType type, P p) { if (visitedNodes.containsKey(type)) { return visitedNodes.get(type); } - visitedNodes.put(type, null); + visitedNodes.put(type, defaultResult); R r = scan(type.getAlternatives(), p); + visitedNodes.put(type, r); return r; } @@ -214,7 +318,7 @@ public R visitTypeVariable(AnnotatedTypeVariable type, P p) { if (visitedNodes.containsKey(type)) { return visitedNodes.get(type); } - visitedNodes.put(type, null); + visitedNodes.put(type, defaultResult); R r = scan(type.getLowerBound(), p); visitedNodes.put(type, r); r = scanAndReduce(type.getUpperBound(), p, r); @@ -224,17 +328,17 @@ public R visitTypeVariable(AnnotatedTypeVariable type, P p) { @Override public R visitNoType(AnnotatedNoType type, P p) { - return null; + return defaultResult; } @Override public R visitNull(AnnotatedNullType type, P p) { - return null; + return defaultResult; } @Override public R visitPrimitive(AnnotatedPrimitiveType type, P p) { - return null; + return defaultResult; } @Override @@ -242,7 +346,7 @@ public R visitWildcard(AnnotatedWildcardType type, P p) { if (visitedNodes.containsKey(type)) { return visitedNodes.get(type); } - visitedNodes.put(type, null); + visitedNodes.put(type, defaultResult); R r = scan(type.getExtendsBound(), p); visitedNodes.put(type, r); r = scanAndReduce(type.getSuperBound(), p, r); diff --git a/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeScanner.java b/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeScanner.java index 346152ea777a..20097e462a5c 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeScanner.java +++ b/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeScanner.java @@ -9,9 +9,92 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; +import org.checkerframework.javacutil.BugInCF; +/** + * An {@link AnnotatedTypeScanner} that scans an {@link AnnotatedTypeMirror} and performs some + * {@link #defaultAction} on each type. The defaultAction can be passed to the constructor {@link + * #SimpleAnnotatedTypeScanner(DefaultAction)} or this class can be extended and {@link + * #defaultAction} can be overridden. + * + *

If the default action does not return a result, then {@code R} should be {@link Void}. If the + * default action returns a result, then specify a {@link #reduce} function. + * + * @param the return type of this visitor's methods. Use Void for visitors that do not need to + * return results. + * @param

the type of the additional parameter to this visitor's methods. Use Void for visitors + * that do not need an additional parameter. + */ public class SimpleAnnotatedTypeScanner extends AnnotatedTypeScanner { + /** + * Represents an action to perform on every type. + * + * @param the type of the result of the action + * @param

the type of the parameter of action + */ + @FunctionalInterface + public interface DefaultAction { + + /** + * The action to perform on every type. + * + * @param type AnnotatedTypeMirror on which to perform some action + * @param p argument to pass to the action + * @return result of the action + */ + R defaultAction(AnnotatedTypeMirror type, P p); + } + + /** The action to perform on every type. */ + protected final DefaultAction defaultAction; + + /** + * Creates a scanner that performs {@code defaultAction} on every type. + * + *

Use this constructor if the type of result of the default action is {@link Void}. + * + * @param defaultAction action to perform on every type + */ + public SimpleAnnotatedTypeScanner(DefaultAction defaultAction) { + this(defaultAction, null, null); + } + + /** + * Creates a scanner that performs {@code defaultAction} on every type and use {@code reduce} to + * combine the results. + * + *

Use this constructor if the default action returns a result. + * + * @param defaultAction action to perform on every type + * @param reduce function used to combine results + * @param defaultResult result to use by default + */ + public SimpleAnnotatedTypeScanner( + DefaultAction defaultAction, Reduce reduce, R defaultResult) { + super(reduce, defaultResult); + this.defaultAction = defaultAction; + } + + /** + * Creates a scanner without specifing the default action. Subclasses may only use this + * constructor if they also override {@link #defaultAction(AnnotatedTypeMirror, Object)}. + */ + protected SimpleAnnotatedTypeScanner() { + this(null, null, null); + } + + /** + * Creates a scanner without specifing the default action. Subclasses may only use this + * constructor if they also override {@link #defaultAction(AnnotatedTypeMirror, Object)}. + * + * @param reduce function used to combine results + * @param defaultResult result to use by default + */ + protected SimpleAnnotatedTypeScanner(Reduce reduce, R defaultResult) { + this(null, reduce, defaultResult); + } + /** * Called by default for any visit method that is not overridden. * @@ -20,8 +103,13 @@ public class SimpleAnnotatedTypeScanner extends AnnotatedTypeScanner * @return a visitor-specified result */ protected R defaultAction(AnnotatedTypeMirror type, P p) { - // Do nothing - return null; + if (defaultAction == null) { + // The no argument constructor sets default action to null. + throw new BugInCF( + "%s did not provide a default action. Please override #defaultAction", + this.getClass()); + } + return defaultAction.defaultAction(type, p); } /** diff --git a/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeVisitor.java b/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeVisitor.java index fffce7d7e72f..ef2f396f6a23 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/framework/type/visitor/SimpleAnnotatedTypeVisitor.java @@ -20,7 +20,7 @@ * @param

the type of the additional parameter to this visitor's methods. Use {@link Void} for * visitors that do not need an additional parameter. */ -public class SimpleAnnotatedTypeVisitor implements AnnotatedTypeVisitor { +public abstract class SimpleAnnotatedTypeVisitor implements AnnotatedTypeVisitor { /** The default value to return as a default action. */ protected final R DEFAULT_VALUE; @@ -29,7 +29,7 @@ public class SimpleAnnotatedTypeVisitor implements AnnotatedTypeVisitor, Void> { - - @Override - protected List scan(AnnotatedTypeMirror type, Void aVoid) { - List errors = new ArrayList<>(); - for (AnnotationMirror am : type.getAnnotations()) { - if (isExpressionAnno(am)) { - errors.addAll(checkForError(am)); - } - } - List superList = super.scan(type, aVoid); - if (superList != null) { - errors.addAll(superList); - } - return errors; - } - - @Override - protected List reduce( - List r1, List r2) { - if (r1 != null && r2 != null) { - r1.addAll(r2); - return r1; - } else if (r1 != null) { - return r1; - } else if (r2 != null) { - return r2; - } else { - return null; - } + extends SimpleAnnotatedTypeScanner, Void> { + + /** Create ExpressionErrorChecker. */ + private ExpressionErrorChecker() { + super( + (AnnotatedTypeMirror type, Void aVoid) -> { + List errors = new ArrayList<>(); + for (AnnotationMirror am : type.getAnnotations()) { + if (isExpressionAnno(am)) { + errors.addAll(checkForError(am)); + } + } + return errors; + }, + (r1, r2) -> { + List newList = new ArrayList<>(r1); + newList.addAll(r2); + return newList; + }, + Collections.emptyList()); } } @@ -918,40 +909,17 @@ private boolean hasDependentType(AnnotatedTypeMirror atm) { if (atm == null) { return false; } - Boolean b = new ContainsDependentType().visit(atm); - if (b == null) { - return false; - } + boolean b = + new SimpleAnnotatedTypeScanner<>( + (type, p) -> + type.getAnnotations().stream() + .anyMatch(this::isExpressionAnno), + Boolean::logicalOr, + false) + .visit(atm); return b; } - /** Checks whether or not an annotated type contains an dependent type annotation. */ - private class ContainsDependentType extends AnnotatedTypeScanner { - @Override - protected Boolean scan(AnnotatedTypeMirror type, Void aVoid) { - for (AnnotationMirror am : type.getAnnotations()) { - if (isExpressionAnno(am)) { - return true; - } - } - return super.scan(type, aVoid); - } - - @Override - protected Boolean reduce(Boolean r1, Boolean r2) { - if (r1 != null && r2 != null) { - // if either have an expression anno, return true; - return r1 || r2; - } else if (r1 != null) { - return r1; - } else if (r2 != null) { - return r2; - } else { - return false; - } - } - } - /** * Returns the list of elements of the annotation that are Java expressions, or the empty list * if there aren't any. diff --git a/framework/src/main/java/org/checkerframework/framework/util/typeinference/DefaultTypeArgumentInference.java b/framework/src/main/java/org/checkerframework/framework/util/typeinference/DefaultTypeArgumentInference.java index 35688f17eae2..3950bba76bdb 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/typeinference/DefaultTypeArgumentInference.java +++ b/framework/src/main/java/org/checkerframework/framework/util/typeinference/DefaultTypeArgumentInference.java @@ -139,7 +139,7 @@ public Map inferTypeArgs( if (TreeUtils.enclosingNonParen(pathToExpression).first.getKind() == Tree.Kind.LAMBDA_EXPRESSION || (assignedTo == null - && TreeUtils.getAssignmentContext(pathToExpression) != null)) { + && TreeUtils.getAssignmentContext(pathToExpression, true) != null)) { // If the type of the assignment context isn't found, but the expression is assigned, // then don't attempt to infer type arguments, because the Java type inferred will be // incorrect. The assignment type is null when it includes uninferred type arguments. diff --git a/framework/src/main/java/org/checkerframework/framework/util/typeinference/TypeArgInferenceUtil.java b/framework/src/main/java/org/checkerframework/framework/util/typeinference/TypeArgInferenceUtil.java index beb9785fb1eb..8718ceecdd44 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/typeinference/TypeArgInferenceUtil.java +++ b/framework/src/main/java/org/checkerframework/framework/util/typeinference/TypeArgInferenceUtil.java @@ -417,31 +417,9 @@ public static void checkForUninferredTypes(AnnotatedTypeMirror type) { private static class TypeVariableFinder extends AnnotatedTypeScanner> { - @Override - protected Boolean scan( - Iterable types, Collection typeVars) { - if (types == null) { - return false; - } - Boolean result = false; - boolean first = true; - for (AnnotatedTypeMirror type : types) { - result = (first ? scan(type, typeVars) : scanAndReduce(type, typeVars, result)); - first = false; - } - return result; - } - - @Override - protected Boolean reduce(Boolean r1, Boolean r2) { - if (r1 == null) { - return r2 != null && r2; - - } else if (r2 == null) { - return r1; - } - - return r1 || r2; + /** Create TypeVariableFinder. */ + protected TypeVariableFinder() { + super(Boolean::logicalOr, false); } @Override diff --git a/framework/src/test/java/testaccumulation/TestAccumulationAnnotatedTypeFactory.java b/framework/src/test/java/testaccumulation/TestAccumulationAnnotatedTypeFactory.java new file mode 100644 index 000000000000..76fc374c37d9 --- /dev/null +++ b/framework/src/test/java/testaccumulation/TestAccumulationAnnotatedTypeFactory.java @@ -0,0 +1,72 @@ +package testaccumulation; + +import com.sun.source.tree.MethodInvocationTree; +import javax.lang.model.element.AnnotationMirror; +import org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.TreeAnnotator; +import org.checkerframework.javacutil.TreeUtils; +import testaccumulation.qual.TestAccumulation; +import testaccumulation.qual.TestAccumulationBottom; + +/** + * The annotated type factory for a test accumulation checker, which implements a basic called + * methods checker. + */ +public class TestAccumulationAnnotatedTypeFactory extends AccumulationAnnotatedTypeFactory { + /** + * Create a new accumulation checker's annotated type factory. + * + * @param checker the checker + */ + public TestAccumulationAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker, TestAccumulation.class, TestAccumulationBottom.class); + this.postInit(); + } + + @Override + protected TreeAnnotator createTreeAnnotator() { + return new ListTreeAnnotator( + super.createTreeAnnotator(), new TestAccumulationTreeAnnotator(this)); + } + + /** + * Necessary for the type rule for called methods described below. A new accumulation analysis + * might have other type rules here, or none at all. + */ + private class TestAccumulationTreeAnnotator extends AccumulationTreeAnnotator { + /** + * Creates an instance of this tree annotator for the given type factory. + * + * @param factory the type factory + */ + public TestAccumulationTreeAnnotator(AccumulationAnnotatedTypeFactory factory) { + super(factory); + } + + @Override + public Void visitMethodInvocation(MethodInvocationTree tree, AnnotatedTypeMirror type) { + // CalledMethods requires special treatment of the return values of methods that return + // their receiver: the default return type must include the method being invoked. + // + // The basic accumulation analysis cannot handle this case - it can use the RR checker + // to transfer an annotation from the receiver to the return type, but because + // accumulation + // (has to) happen in dataflow, the correct annotation may not yet be available. The + // basic + // accumulation analysis therefore only supports "pass-through" returns receiver + // methods; + // it does not support automatically accumulating at the same time. + if (returnsThis(tree)) { + String methodName = TreeUtils.getMethodName(tree.getMethodSelect()); + AnnotationMirror oldAnno = type.getAnnotationInHierarchy(top); + type.replaceAnnotation( + qualHierarchy.greatestLowerBound( + oldAnno, createAccumulatorAnnotation(methodName))); + } + return super.visitMethodInvocation(tree, type); + } + } +} diff --git a/framework/src/test/java/testaccumulation/TestAccumulationChecker.java b/framework/src/test/java/testaccumulation/TestAccumulationChecker.java new file mode 100644 index 000000000000..b2d4ba8139d5 --- /dev/null +++ b/framework/src/test/java/testaccumulation/TestAccumulationChecker.java @@ -0,0 +1,6 @@ +package testaccumulation; + +import org.checkerframework.common.accumulation.AccumulationChecker; + +/** A test accumulation checker that implements a basic version of called-methods accumulation. */ +public class TestAccumulationChecker extends AccumulationChecker {} diff --git a/framework/src/test/java/testaccumulation/TestAccumulationTransfer.java b/framework/src/test/java/testaccumulation/TestAccumulationTransfer.java new file mode 100644 index 000000000000..39bd44bc0c89 --- /dev/null +++ b/framework/src/test/java/testaccumulation/TestAccumulationTransfer.java @@ -0,0 +1,35 @@ +package testaccumulation; + +import org.checkerframework.common.accumulation.AccumulationTransfer; +import org.checkerframework.dataflow.analysis.TransferInput; +import org.checkerframework.dataflow.analysis.TransferResult; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.framework.flow.CFAnalysis; +import org.checkerframework.framework.flow.CFStore; +import org.checkerframework.framework.flow.CFValue; + +/** A basic transfer function that accumulates the names of methods called. */ +public class TestAccumulationTransfer extends AccumulationTransfer { + + /** + * default constructor + * + * @param analysis the analysis + */ + public TestAccumulationTransfer(final CFAnalysis analysis) { + super(analysis); + } + + @Override + public TransferResult visitMethodInvocation( + final MethodInvocationNode node, final TransferInput input) { + TransferResult result = super.visitMethodInvocation(node, input); + String methodName = node.getTarget().getMethod().getSimpleName().toString(); + Node receiver = node.getTarget().getReceiver(); + if (!"".equals(methodName) && receiver != null) { + accumulate(receiver, result, methodName); + } + return result; + } +} diff --git a/framework/src/test/java/testaccumulation/qual/TestAccumulation.java b/framework/src/test/java/testaccumulation/qual/TestAccumulation.java new file mode 100644 index 000000000000..141ca8fee59f --- /dev/null +++ b/framework/src/test/java/testaccumulation/qual/TestAccumulation.java @@ -0,0 +1,22 @@ +package testaccumulation.qual; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.SubtypeOf; + +/** A test accumulation analysis qualifier. It accumulates generic strings. */ +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({}) +@DefaultQualifierInHierarchy +public @interface TestAccumulation { + /** + * Accumulated strings. + * + * @return the strings + */ + public String[] value() default {}; +} diff --git a/framework/src/test/java/testaccumulation/qual/TestAccumulationBottom.java b/framework/src/test/java/testaccumulation/qual/TestAccumulationBottom.java new file mode 100644 index 000000000000..46eadffed139 --- /dev/null +++ b/framework/src/test/java/testaccumulation/qual/TestAccumulationBottom.java @@ -0,0 +1,16 @@ +package testaccumulation.qual; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; +import org.checkerframework.framework.qual.TargetLocations; +import org.checkerframework.framework.qual.TypeUseLocation; + +/** A test bottom type for an accumulation type system. */ +@SubtypeOf({TestAccumulation.class}) +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND}) +public @interface TestAccumulationBottom {} diff --git a/framework/src/test/java/tests/AccumulationTest.java b/framework/src/test/java/tests/AccumulationTest.java new file mode 100644 index 000000000000..40d01c426650 --- /dev/null +++ b/framework/src/test/java/tests/AccumulationTest.java @@ -0,0 +1,24 @@ +package tests; + +import java.io.File; +import java.util.List; +import org.checkerframework.framework.test.FrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; +import testaccumulation.TestAccumulationChecker; + +/** + * A test that the accumulation abstract checker is working correctly, using a simple accumulation + * checker. + */ +public class AccumulationTest extends FrameworkPerDirectoryTest { + + /** @param testFiles the files containing test code, which will be type-checked */ + public AccumulationTest(List testFiles) { + super(testFiles, TestAccumulationChecker.class, "accumulation", "-Anomsgtext"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"accumulation", "all-systems"}; + } +} diff --git a/framework/src/test/java/tests/ValueIgnoreRangeOverflowTest.java b/framework/src/test/java/tests/ValueIgnoreRangeOverflowTest.java index 08da143cb583..093684ab3797 100644 --- a/framework/src/test/java/tests/ValueIgnoreRangeOverflowTest.java +++ b/framework/src/test/java/tests/ValueIgnoreRangeOverflowTest.java @@ -16,7 +16,6 @@ public ValueIgnoreRangeOverflowTest(List testFiles) { org.checkerframework.common.value.ValueChecker.class, "value", "-Anomsgtext", - "-Astubs=statically-executable.astub", "-A" + ValueChecker.REPORT_EVAL_WARNS, "-A" + ValueChecker.IGNORE_RANGE_OVERFLOW); } diff --git a/framework/src/test/java/tests/ValueNonNullStringsConcatenationTest.java b/framework/src/test/java/tests/ValueNonNullStringsConcatenationTest.java index 48b188f3cfd7..47f560ee05be 100644 --- a/framework/src/test/java/tests/ValueNonNullStringsConcatenationTest.java +++ b/framework/src/test/java/tests/ValueNonNullStringsConcatenationTest.java @@ -15,7 +15,6 @@ public ValueNonNullStringsConcatenationTest(List testFiles) { org.checkerframework.common.value.ValueChecker.class, "value-non-null-strings-concatenation", "-Anomsgtext", - "-Astubs=statically-executable.astub", "-A" + ValueChecker.REPORT_EVAL_WARNS, "-A" + ValueChecker.NON_NULL_STRINGS_CONCATENATION); } diff --git a/framework/src/test/java/tests/ValueTest.java b/framework/src/test/java/tests/ValueTest.java index 34655f34df1c..38cac432432c 100644 --- a/framework/src/test/java/tests/ValueTest.java +++ b/framework/src/test/java/tests/ValueTest.java @@ -22,7 +22,7 @@ public ValueTest(List testFiles) { org.checkerframework.common.value.ValueChecker.class, "value", "-Anomsgtext", - "-Astubs=statically-executable.astub:tests/value/minints-stub.astub:tests/value/lowercase.astub", + "-Astubs=tests/value/minints-stub.astub:tests/value/lowercase.astub", "-A" + ValueChecker.REPORT_EVAL_WARNS); } diff --git a/framework/src/test/java/tests/ValueUncheckedDefaultsTest.java b/framework/src/test/java/tests/ValueUncheckedDefaultsTest.java index d001ff46dbdd..6cc64ec12618 100644 --- a/framework/src/test/java/tests/ValueUncheckedDefaultsTest.java +++ b/framework/src/test/java/tests/ValueUncheckedDefaultsTest.java @@ -16,7 +16,6 @@ public ValueUncheckedDefaultsTest(List testFiles) { ValueChecker.class, "value", "-Anomsgtext", - "-Astubs=statically-executable.astub", "-AuseConservativeDefaultsForUncheckedCode=btyecode", "-A" + ValueChecker.REPORT_EVAL_WARNS); } diff --git a/framework/src/test/java/tests/ViewpointTestCheckerTest.java b/framework/src/test/java/tests/ViewpointTestCheckerTest.java new file mode 100644 index 000000000000..fe2032e2cf07 --- /dev/null +++ b/framework/src/test/java/tests/ViewpointTestCheckerTest.java @@ -0,0 +1,19 @@ +package tests; + +import java.io.File; +import java.util.List; +import org.checkerframework.framework.test.FrameworkPerDirectoryTest; +import org.junit.runners.Parameterized; + +public class ViewpointTestCheckerTest extends FrameworkPerDirectoryTest { + + /** @param testFiles the files containing test code, which will be type-checked */ + public ViewpointTestCheckerTest(List testFiles) { + super(testFiles, viewpointtest.ViewpointTestChecker.class, "viewpointtest", "-Anomsgtext"); + } + + @Parameterized.Parameters + public static String[] getTestDirs() { + return new String[] {"viewpointtest"}; + } +} diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java new file mode 100644 index 000000000000..68bae4fc8469 --- /dev/null +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -0,0 +1,37 @@ +package viewpointtest; + +import java.lang.annotation.Annotation; +import java.util.Set; +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import viewpointtest.quals.A; +import viewpointtest.quals.B; +import viewpointtest.quals.Bottom; +import viewpointtest.quals.PolyVP; +import viewpointtest.quals.ReceiverDependantQual; +import viewpointtest.quals.Top; + +public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { + + public ViewpointTestAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker); + this.postInit(); + } + + @Override + protected Set> createSupportedTypeQualifiers() { + return getBundledTypeQualifiers( + A.class, + B.class, + Bottom.class, + PolyVP.class, + ReceiverDependantQual.class, + Top.class); + } + + @Override + protected AbstractViewpointAdapter createViewpointAdapter() { + return new ViewpointTestViewpointAdapter(this); + } +} diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotationHolder.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotationHolder.java new file mode 100644 index 000000000000..db0aaf84e54d --- /dev/null +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotationHolder.java @@ -0,0 +1,26 @@ +package viewpointtest; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.util.Elements; +import org.checkerframework.framework.source.SourceChecker; +import org.checkerframework.javacutil.AnnotationBuilder; +import viewpointtest.quals.A; +import viewpointtest.quals.B; +import viewpointtest.quals.Bottom; +import viewpointtest.quals.PolyVP; +import viewpointtest.quals.ReceiverDependantQual; +import viewpointtest.quals.Top; + +public class ViewpointTestAnnotationHolder { + /* package-private */ static AnnotationMirror A, B, BOTTOM, POLYVP, RECEIVERDEPENDANTQUAL, TOP; + + public static void init(SourceChecker checker) { + Elements elements = checker.getElementUtils(); + A = AnnotationBuilder.fromClass(elements, viewpointtest.quals.A.class); + B = AnnotationBuilder.fromClass(elements, viewpointtest.quals.B.class); + BOTTOM = AnnotationBuilder.fromClass(elements, Bottom.class); + POLYVP = AnnotationBuilder.fromClass(elements, PolyVP.class); + RECEIVERDEPENDANTQUAL = AnnotationBuilder.fromClass(elements, ReceiverDependantQual.class); + TOP = AnnotationBuilder.fromClass(elements, Top.class); + } +} diff --git a/framework/src/test/java/viewpointtest/ViewpointTestChecker.java b/framework/src/test/java/viewpointtest/ViewpointTestChecker.java new file mode 100644 index 000000000000..f7d2f228cadf --- /dev/null +++ b/framework/src/test/java/viewpointtest/ViewpointTestChecker.java @@ -0,0 +1,12 @@ +package viewpointtest; + +import org.checkerframework.common.basetype.BaseTypeChecker; + +public class ViewpointTestChecker extends BaseTypeChecker { + + @Override + public void initChecker() { + super.initChecker(); + ViewpointTestAnnotationHolder.init(this); + } +} diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java new file mode 100644 index 000000000000..3eafc34e95df --- /dev/null +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -0,0 +1,48 @@ +package viewpointtest; + +import static viewpointtest.ViewpointTestAnnotationHolder.RECEIVERDEPENDANTQUAL; +import static viewpointtest.ViewpointTestAnnotationHolder.TOP; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeKind; +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; + +public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { + + /** + * The class constructor. + * + * @param atypeFactory + */ + public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + } + + @Override + protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { + return atm.getAnnotationInHierarchy(TOP); + } + + @Override + protected AnnotatedTypeMirror combineTypeWithType( + AnnotatedTypeMirror receiver, AnnotatedTypeMirror declared) { + // skip method decl + if (declared.getKind() == TypeKind.EXECUTABLE) { + return declared; + } + return super.combineTypeWithType(receiver, declared); + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + + if (AnnotationUtils.areSame(declaredAnnotation, RECEIVERDEPENDANTQUAL)) { + return receiverAnnotation; + } + return declaredAnnotation; + } +} diff --git a/framework/src/test/java/viewpointtest/quals/A.java b/framework/src/test/java/viewpointtest/quals/A.java new file mode 100644 index 000000000000..60b3696fa03f --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/A.java @@ -0,0 +1,14 @@ +package viewpointtest.quals; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({Top.class}) +public @interface A {} diff --git a/framework/src/test/java/viewpointtest/quals/B.java b/framework/src/test/java/viewpointtest/quals/B.java new file mode 100644 index 000000000000..ed90c9d5b02d --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/B.java @@ -0,0 +1,14 @@ +package viewpointtest.quals; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({Top.class}) +public @interface B {} diff --git a/framework/src/test/java/viewpointtest/quals/Bottom.java b/framework/src/test/java/viewpointtest/quals/Bottom.java new file mode 100644 index 000000000000..bc76203bf7d7 --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/Bottom.java @@ -0,0 +1,17 @@ +package viewpointtest.quals; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.DefaultFor; +import org.checkerframework.framework.qual.SubtypeOf; +import org.checkerframework.framework.qual.TypeUseLocation; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({A.class, B.class, ReceiverDependantQual.class}) +@DefaultFor(TypeUseLocation.LOWER_BOUND) +public @interface Bottom {} diff --git a/framework/src/test/java/viewpointtest/quals/PolyVP.java b/framework/src/test/java/viewpointtest/quals/PolyVP.java new file mode 100644 index 000000000000..8d4659e72977 --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/PolyVP.java @@ -0,0 +1,14 @@ +package viewpointtest.quals; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.PolymorphicQualifier; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@PolymorphicQualifier(Top.class) +public @interface PolyVP {} diff --git a/framework/src/test/java/viewpointtest/quals/ReceiverDependantQual.java b/framework/src/test/java/viewpointtest/quals/ReceiverDependantQual.java new file mode 100644 index 000000000000..a1873716a6dc --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/ReceiverDependantQual.java @@ -0,0 +1,14 @@ +package viewpointtest.quals; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({Top.class}) +public @interface ReceiverDependantQual {} diff --git a/framework/src/test/java/viewpointtest/quals/Top.java b/framework/src/test/java/viewpointtest/quals/Top.java new file mode 100644 index 000000000000..96d52a309988 --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/Top.java @@ -0,0 +1,16 @@ +package viewpointtest.quals; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.SubtypeOf; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({}) +@DefaultQualifierInHierarchy +public @interface Top {} diff --git a/framework/tests/accumulation/Generics.java b/framework/tests/accumulation/Generics.java new file mode 100644 index 000000000000..6791c4506b6d --- /dev/null +++ b/framework/tests/accumulation/Generics.java @@ -0,0 +1,43 @@ +import java.util.ArrayList; +import java.util.List; +import org.checkerframework.common.returnsreceiver.qual.*; +import testaccumulation.qual.*; + +class Generics { + + static interface Symbol { + + boolean isStatic(); + + void finalize(@TestAccumulation("foo") Symbol this); + } + + static List<@TestAccumulation("foo") Symbol> makeList(@TestAccumulation("foo") Symbol s) { + ArrayList<@TestAccumulation("foo") Symbol> l = new ArrayList<>(); + l.add(s); + return l; + } + + static void useList() { + Symbol s = null; + for (Symbol t : makeList(s)) { + t.finalize(); + } + } + + // reduced from real-world code + private <@TestAccumulation() T extends Symbol> T getMember(Class type, boolean b) { + if (b) { + T sym = getMember(type, !b); + if (sym != null && sym.isStatic()) { + return sym; + } + } else { + T sym = getMember(type, b); + if (sym != null) { + return sym; + } + } + return null; + } +} diff --git a/framework/tests/accumulation/ObjectConstructionIssue20.java b/framework/tests/accumulation/ObjectConstructionIssue20.java new file mode 100644 index 000000000000..b7ff7e0fcf64 --- /dev/null +++ b/framework/tests/accumulation/ObjectConstructionIssue20.java @@ -0,0 +1,36 @@ +// test case for issue 20: https://github.com/kelloggm/object-construction-checker/issues/20 + +import java.util.Map; + +public class ObjectConstructionIssue20 { + + private boolean enableProtoAnnotations; + + @SuppressWarnings({"unchecked"}) + private T getProtoExtension( + E element, GeneratedExtension extension) { + // Use this method as the chokepoint for all field annotations processing, so we can + // toggle on/off annotations processing in one place. + if (!enableProtoAnnotations) { + return null; + } + return (T) element.getOptionFields().get(extension.getDescriptor()); + } + + // stubs of relevant classes + private class Message {} + + private class ProtoElement { + public Map getOptionFields() { + return null; + } + } + + private class FieldDescriptor {} + + private class GeneratedExtension { + public FieldDescriptor getDescriptor() { + return null; + } + } +} diff --git a/framework/tests/accumulation/Parens.java b/framework/tests/accumulation/Parens.java new file mode 100644 index 000000000000..2e896cf9d2f9 --- /dev/null +++ b/framework/tests/accumulation/Parens.java @@ -0,0 +1,5 @@ +public class Parens { + public synchronized void incrementPushed(long[] pushed, int operationType) { + ++(pushed[operationType]); + } +} diff --git a/framework/tests/accumulation/SimpleFluent.java b/framework/tests/accumulation/SimpleFluent.java new file mode 100644 index 000000000000..598d22bf60c4 --- /dev/null +++ b/framework/tests/accumulation/SimpleFluent.java @@ -0,0 +1,109 @@ +// A simple test that the fluent API logic in the Accumulation Checker works. + +import org.checkerframework.common.returnsreceiver.qual.*; +import testaccumulation.qual.*; + +/* Simple inference of a fluent builder. */ +class SimpleFluent { + SimpleFluent build(@TestAccumulation({"a", "b"}) SimpleFluent this) { + return this; + } + + @This SimpleFluent build2(@TestAccumulation({"a", "b"}) SimpleFluent this) { + return this; + } + + @This SimpleFluent a() { + return this; + } + + @This SimpleFluent b() { + return this; + } + + // intentionally does not have an @This annotation + SimpleFluent c() { + return this; + } + + static void doStuffCorrect(@TestAccumulation({"a", "b"}) SimpleFluent s) { + s.a().b().build(); + } + + static void doStuffWrong(@TestAccumulation({"a"}) SimpleFluent s) { + s.a() + // :: error: method.invocation.invalid + .build(); + } + + static void noReturnsReceiverAnno(@TestAccumulation({"a", "b"}) SimpleFluent s) { + s.a().b() + .c() + // :: error: method.invocation.invalid + .build(); + } + + static void mixFluentAndNonFluent(SimpleFluent s1) { + s1.a().b(); + s1.build(); + } + + static void mixFluentAndNonFluentWrong(SimpleFluent s) { + s.a(); // .b() + // :: error: method.invocation.invalid + s.build(); + } + + static void fluentLoop(SimpleFluent t) { + SimpleFluent s = t.a(); + int i = 10; + while (i > 0) { + // :: error: method.invocation.invalid + s.b().build(); + i--; + s = new SimpleFluent(); + } + } + + static void m1(SimpleFluent s) { + s.c().a().b().build(); + } + + static void m2(SimpleFluent s) { + s.c().a().b(); + // :: error: method.invocation.invalid + s.c().build(); + } + + static void m3(SimpleFluent s) { + s.c().a().b().build(); + // :: error: method.invocation.invalid + s.c().a().build(); + } + + static void m4(SimpleFluent s) { + s.c().a().b().build2().build(); + } + + static void m5(SimpleFluent s) { + s.a().c(); + s.b().build(); + } + + static void m6(SimpleFluent s) { + // :: error: method.invocation.invalid + s.a().c().b().build(); + } + + static void m7(SimpleFluent s) { + // :: error: method.invocation.invalid + s.a().b().build().c().b().build(); + } + + static void m8(SimpleFluent s) { + // :: error: method.invocation.invalid + s.a().build().c().a().b().build(); + // :: error: method.invocation.invalid + s.build(); + } +} diff --git a/framework/tests/accumulation/SimpleInference.java b/framework/tests/accumulation/SimpleInference.java new file mode 100644 index 000000000000..cb4f9bf5aa24 --- /dev/null +++ b/framework/tests/accumulation/SimpleInference.java @@ -0,0 +1,19 @@ +import testaccumulation.qual.*; + +class SimpleInference { + void build(@TestAccumulation({"a"}) SimpleInference this) {} + + void a() {} + + static void doStuffCorrect() { + SimpleInference s = new SimpleInference(); + s.a(); + s.build(); + } + + static void doStuffWrong() { + SimpleInference s = new SimpleInference(); + // :: error: method.invocation.invalid + s.build(); + } +} diff --git a/framework/tests/accumulation/Subtyping.java b/framework/tests/accumulation/Subtyping.java new file mode 100644 index 000000000000..023beb01f3e1 --- /dev/null +++ b/framework/tests/accumulation/Subtyping.java @@ -0,0 +1,86 @@ +// A basic test that subtyping between accumulation annotations +// works as expected. Note that GJF botches the formatting +// in this file, so the comments for error messages are in weird +// places. + +import testaccumulation.qual.*; + +class Subtyping { + void top(@TestAccumulation() Object o1) { + @TestAccumulation() Object o2 = o1; + @TestAccumulation("foo") + // :: error: assignment.type.incompatible + Object o3 = o1; + @TestAccumulation("bar") + // :: error: assignment.type.incompatible + Object o4 = o1; + @TestAccumulation({"foo", "bar"}) + // :: error: assignment.type.incompatible + Object o5 = o1; + // :: error: assignment.type.incompatible + @TestAccumulationBottom Object o6 = o1; + } + + void foo(@TestAccumulation("foo") Object o1) { + @TestAccumulation() Object o2 = o1; + @TestAccumulation("foo") + Object o3 = o1; + @TestAccumulation("bar") + // :: error: assignment.type.incompatible + Object o4 = o1; + @TestAccumulation({"foo", "bar"}) + // :: error: assignment.type.incompatible + Object o5 = o1; + // :: error: assignment.type.incompatible + @TestAccumulationBottom Object o6 = o1; + } + + void bar(@TestAccumulation("bar") Object o1) { + @TestAccumulation() Object o2 = o1; + @TestAccumulation("foo") + // :: error: assignment.type.incompatible + Object o3 = o1; + @TestAccumulation("bar") + Object o4 = o1; + @TestAccumulation({"foo", "bar"}) + // :: error: assignment.type.incompatible + Object o5 = o1; + // :: error: assignment.type.incompatible + @TestAccumulationBottom Object o6 = o1; + } + + void foobar(@TestAccumulation({"foo", "bar"}) Object o1) { + @TestAccumulation() Object o2 = o1; + @TestAccumulation("foo") + Object o3 = o1; + @TestAccumulation("bar") + Object o4 = o1; + @TestAccumulation({"foo", "bar"}) + Object o5 = o1; + // :: error: assignment.type.incompatible + @TestAccumulationBottom Object o6 = o1; + } + + void barfoo(@TestAccumulation({"bar", "foo"}) Object o1) { + @TestAccumulation() Object o2 = o1; + @TestAccumulation("foo") + Object o3 = o1; + @TestAccumulation("bar") + Object o4 = o1; + @TestAccumulation({"foo", "bar"}) + Object o5 = o1; + // :: error: assignment.type.incompatible + @TestAccumulationBottom Object o6 = o1; + } + + void bot(@TestAccumulationBottom Object o1) { + @TestAccumulation() Object o2 = o1; + @TestAccumulation("foo") + Object o3 = o1; + @TestAccumulation("bar") + Object o4 = o1; + @TestAccumulation({"foo", "bar"}) + Object o5 = o1; + @TestAccumulationBottom Object o6 = o1; + } +} diff --git a/framework/tests/value/MyTree.java b/framework/tests/value/MyTree.java index 53e95b36442a..97645eb83ed1 100644 --- a/framework/tests/value/MyTree.java +++ b/framework/tests/value/MyTree.java @@ -20,6 +20,7 @@ void uses() { newTree("hello").put("bye"); MyTree<@UnknownVal String> myTree1 = newTree("hello").put("bye"); + // :: error: (assignment.type.incompatible) MyTree<@StringVal("hello") String> myTree2 = newTree("hello").put("hello"); MyTree<@StringVal("hello") String> myTree2b = MyTree.<@StringVal("hello") String>newTree("hello").put("hello"); diff --git a/framework/tests/value/StringLenMethods.java b/framework/tests/value/StringLenMethods.java index 23b071e449e1..8ba8dbc01dfd 100644 --- a/framework/tests/value/StringLenMethods.java +++ b/framework/tests/value/StringLenMethods.java @@ -1,5 +1,6 @@ import org.checkerframework.common.value.qual.ArrayLen; import org.checkerframework.common.value.qual.ArrayLenRange; +import org.checkerframework.common.value.qual.IntRange; import org.checkerframework.common.value.qual.StringVal; class StringLenMethods { @@ -29,7 +30,7 @@ void toString(boolean b, char c, byte y, short s, int i, long l) { @ArrayLenRange(from = 1, to = 20) String sls = String.valueOf(l); } - void toStringRadix(int i, long l, int radix) { + void toStringRadix(int i, long l, @IntRange(from = 2, to = 36) int radix) { @ArrayLenRange(from = 1) String is = Integer.toString(i, radix); @ArrayLenRange(from = 1) String ls = Long.toString(l, radix); diff --git a/framework/tests/viewpointtest/PolyWithVPA.java b/framework/tests/viewpointtest/PolyWithVPA.java new file mode 100644 index 000000000000..04f73ca91c04 --- /dev/null +++ b/framework/tests/viewpointtest/PolyWithVPA.java @@ -0,0 +1,21 @@ +import viewpointtest.quals.*; + +public class PolyWithVPA { + static class PolyClass { + @ReceiverDependantQual + Object foo(@PolyVP Object o) { + return null; + } + } + + static void test1(@A PolyClass a, @B Object bObj) { + @A Object aObj = a.foo(bObj); + } + + // only poly annos in decl are resolved + static void test2(@PolyVP PolyClass poly, @B Object bObj) { + @PolyVP Object polyObj = poly.foo(bObj); + // :: error: (assignment.type.incompatible) + @B Object anotherBObj = poly.foo(bObj); + } +} diff --git a/framework/tests/viewpointtest/VPAExamples.java b/framework/tests/viewpointtest/VPAExamples.java new file mode 100644 index 000000000000..f59887f31b47 --- /dev/null +++ b/framework/tests/viewpointtest/VPAExamples.java @@ -0,0 +1,36 @@ +import viewpointtest.quals.*; + +public class VPAExamples { + + static class RDContainer { + @ReceiverDependantQual + Object get() { + return null; + } + + void set(@ReceiverDependantQual Object o) {} + + @ReceiverDependantQual Object field; + } + + void tests(@A RDContainer a, @B RDContainer b, @Top RDContainer top) { + @A Object aObj = a.get(); + @B Object bObj = b.get(); + @Top Object tObj = top.get(); + // :: error: (assignment.type.incompatible) + bObj = a.get(); + // :: error: (assignment.type.incompatible) + aObj = top.get(); + // :: error: (assignment.type.incompatible) + bObj = top.get(); + + a.set(aObj); + // :: error: (argument.type.incompatible) + a.set(bObj); + // :: error: (argument.type.incompatible) + b.set(aObj); + b.set(bObj); + top.set(aObj); + top.set(bObj); + } +} diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java index 87ae2f68e2f2..0adfe74e9a96 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java @@ -749,7 +749,8 @@ public static > T getElementValueEnum( * @param expectedType the expected type used to cast the return type * @param the class of the expected type * @param useDefaults whether to apply default values to the element - * @return the value of the element with the given name + * @return the value of the element with the given name; it is a new list, so it is safe for + * clients to side-effect */ public static List getElementValueArray( AnnotationMirror anno, diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java index a28ed29ebcd9..b0bf27b9558f 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java @@ -193,4 +193,36 @@ public static int getJreVersion() { Options options = Options.instance(ctx); return options.get(Option.RELEASE); } + + /** + * Returns the pathname to the tools.jar file, or null if it does not exist. Returns null on + * Java 9 and later. + * + * @return the pathname to the tools.jar file, or null + */ + public static @Nullable String getToolsJar() { + + if (getJreVersion() > 8) { + return null; + } + + String javaHome = System.getenv("JAVA_HOME"); + if (javaHome == null) { + String javaHomeProperty = System.getProperty("java.home"); + if (javaHomeProperty.endsWith(File.separator + "jre")) { + javaHome = javaHomeProperty.substring(javaHomeProperty.length() - 4); + } else { + // Could also determine the location of javac on the path... + throw new Error("Can't infer Java home; java.home=" + javaHomeProperty); + } + } + String toolsJarFilename = javaHome + File.separator + "lib" + File.separator + "tools.jar"; + if (!new File(toolsJarFilename).exists()) { + throw new Error( + String.format( + "File does not exist: %s ; JAVA_HOME=%s ; java.home=%s", + toolsJarFilename, javaHome, System.getProperty("java.home"))); + } + return javaHome + File.separator + "lib" + File.separator + "tools.jar"; + } } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index 36e3bbb3ac1e..979db8ab3fa6 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -53,7 +53,6 @@ import java.util.Collections; import java.util.EnumSet; import java.util.List; -import java.util.Objects; import java.util.Set; import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; @@ -393,9 +392,13 @@ public static Pair enclosingNonParen(final TreePath path) { * *

Otherwise, null is returned. * + * @param treePath the tree path + * @param conservative if conservative result is needed. Conservative result does not include + * pseudo assignment of method invocation receiver * @return the assignment context as described, {@code null} otherwise */ - public static @Nullable Tree getAssignmentContext(final TreePath treePath) { + public static @Nullable Tree getAssignmentContext( + final TreePath treePath, boolean conservative) { TreePath parentPath = treePath.getParentPath(); if (parentPath == null) { @@ -423,8 +426,12 @@ public static Pair enclosingNonParen(final TreePath path) { case VARIABLE: return parent; case MEMBER_SELECT: + // since :javacutil:checkWorkingNullness seems not support assertion and living + // variable inference, assign to a local variable to pass the test + Element parentEle = TreeUtils.elementFromTree(parent); + // Don't process method().field - if (Objects.requireNonNull(TreeUtils.elementFromTree(parent)).getKind().isField()) { + if (parentEle != null && parentEle.getKind().isField()) { return null; } // Also check case when treepath's leaf tree is used as method @@ -434,6 +441,20 @@ public static Pair enclosingNonParen(final TreePath path) { TreePath grandParentPath = parentPath.getParentPath(); if (grandParentPath != null && grandParentPath.getLeaf() instanceof MethodInvocationTree) { + + // do not use foo().bar() scheme as assignment context when conservative, since + // assignedTo for that is not implemented yet + if (conservative) { + MethodInvocationTree grandTree = + (MethodInvocationTree) grandParentPath.getLeaf(); + + // adapted from TypeArgInferenceUtil#assignedTo to be consistent + if (grandTree.getMethodSelect() instanceof MemberSelectTree + && ((MemberSelectTree) grandTree.getMethodSelect()).getExpression() + == treePath.getLeaf()) { + return null; + } + } return grandParentPath.getLeaf(); } else { return null; @@ -449,6 +470,16 @@ public static Pair enclosingNonParen(final TreePath path) { } } + /** + * See {@code getAssignmentContext}. Not using extended result. + * + * @param treePath the tree path + * @return the assignment context as described, {@code null} otherwise + */ + public static @Nullable Tree getAssignmentContext(final TreePath treePath) { + return getAssignmentContext(treePath, false); + } + /** * Gets the {@link Element} for the given Tree API node. For an object instantiation returns the * value of the {@link JCNewClass#constructor} field. Note that this result might differ from