From b3c2cdacc4d247f8aa0267d61db6e208aad1815a Mon Sep 17 00:00:00 2001 From: zcai Date: Tue, 13 Dec 2022 18:15:38 -0500 Subject: [PATCH 001/215] Add VariableDeclarationNode for binding variable (#374) --- .../dataflow/cfg/builder/CFGTranslationPhaseOne.java | 2 ++ docs/CHANGELOG.md | 3 +++ 2 files changed, 5 insertions(+) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 18f0a43c1a3..d57f4822eae 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -600,6 +600,8 @@ public Node visitBindingPattern17(Tree bindingPatternTree, Void p) { TypeElement classElem = TreeUtils.elementFromDeclaration(enclosingClass); Node receiver = new ImplicitThisNode(classElem.asType()); VariableTree varTree = TreeUtils.bindingPatternTreeGetVariable(bindingPatternTree); + VariableDeclarationNode variableDeclarationNode = new VariableDeclarationNode(varTree); + extendWithNode(variableDeclarationNode); LocalVariableNode varNode = new LocalVariableNode(varTree, receiver); extendWithNode(varNode); return varNode; diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 4eaa8f08b20..33ff3a2fa24 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -5,6 +5,9 @@ Version 3.28.0-eisop2 (December ?, 2022) **Implementation details:** +A `VariableDeclarationNode` is now correctly added to the CFG for the binding variable +in a `BindingPatternTree`. + **Closed issues:** From addcaad6c0600333520f34c03610cd84929e149f Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Tue, 7 Feb 2023 22:17:55 -0500 Subject: [PATCH 002/215] typetools/checker-framework 3.29.0 release (#392) Co-authored-by: Suzanne Millstein Co-authored-by: Michael Ernst Co-authored-by: Martin Kellogg Co-authored-by: Muyeed Ahmed Co-authored-by: Manu Sridharan --- azure-pipelines.yml | 8 +- build.gradle | 205 ++++++------ checker-qual-android/build.gradle | 12 +- checker-qual/build.gradle | 4 +- .../formatter/qual/ConversionCategory.java | 33 +- .../qual/I18nConversionCategory.java | 6 +- .../checker/index/qual/HasSubsequence.java | 4 +- .../checker/index/qual/LessThan.java | 4 +- .../checker/index/qual/LessThanBottom.java | 2 +- .../checker/index/qual/LessThanUnknown.java | 2 +- .../mustcall/qual/CreatesMustCallFor.java | 4 +- .../common/value/qual/MinLen.java | 2 +- checker-util/build.gradle | 2 +- .../i18nformatter/util/I18nFormatUtil.java | 13 +- checker/bin-devel/test-plume-lib.sh | 13 +- .../bin-devel/wpi-plumelib/bcel-util.expected | 6 + checker/build.gradle | 266 +++++++-------- checker/jtreg/nullness/issue3700/Client.out | 2 +- .../CalledMethodsAnnotatedTypeFactory.java | 2 +- .../builder/AutoValueSupport.java | 6 +- .../calledmethods/builder/LombokSupport.java | 2 +- .../fenum/FenumAnnotatedTypeFactory.java | 6 +- .../checker/formatter/FormatterTreeUtil.java | 2 +- .../I18nFormatterAnnotatedTypeFactory.java | 3 +- .../i18nformatter/I18nFormatterTreeUtil.java | 8 +- .../checker/index/IndexMethodIdentifier.java | 45 ++- .../checker/index/IndexRefinementInfo.java | 48 ++- .../LessThanAnnotatedTypeFactory.java | 1 - .../index/lowerbound/LowerBoundChecker.java | 2 +- .../index/lowerbound/LowerBoundTransfer.java | 9 +- .../index/samelen/SameLenTransfer.java | 10 +- .../searchindex/SearchIndexTransfer.java | 9 +- .../index/upperbound/OffsetEquation.java | 16 +- .../UpperBoundAnnotatedTypeFactory.java | 78 ++++- .../index/upperbound/UpperBoundChecker.java | 2 +- .../lock/LockAnnotatedTypeFactory.java | 6 +- .../checker/lock/LockVisitor.java | 5 +- .../checker/mustcall/IOUtils.astub | 14 + .../checker/mustcall/MustCallChecker.java | 1 + .../checker/mustcall/MustCallTransfer.java | 2 +- .../nullness/KeyForAnnotatedTypeFactory.java | 2 +- .../checker/nullness/NullnessVisitor.java | 3 +- ...ction-object-parameters-may-be-null.readme | 6 +- .../permit-nullness-assertion-exception.astub | 40 +++ .../checker/nullness/sometimes-nullable.astub | 13 + .../checker/regex/RegexVisitor.java | 9 +- .../checker/resourceleak/IOUtils.astub | 25 ++ .../MustCallConsistencyAnalyzer.java | 124 ++++--- .../ResourceLeakAnnotatedTypeFactory.java | 32 ++ .../resourceleak/ResourceLeakChecker.java | 5 + .../resourceleak/ResourceLeakVisitor.java | 2 +- .../checker/signature/SignatureTransfer.java | 2 +- .../SignednessAnnotatedTypeFactory.java | 6 +- .../units/UnitsAnnotatedTypeFactory.java | 3 +- .../AinferTestAnnotatedTypeFactory.java | 64 +++- .../ainfer/qual/AinferTreatAsSibling1.java | 15 + .../non-annotated/IShouldBeSibling1.java | 14 + .../non-annotated/OptionGroup.java | 18 + .../non-annotated/Purity.java | 2 +- .../TreatAsSibling1InferenceTest.java | 13 + .../non-annotated/TreatAsSibling1Test.java | 11 + checker/tests/index/Issue5471.java | 22 ++ .../nullness/java17/SwitchTestIssue5412.java | 128 +++++++ .../tests/resourceleak/COAnonymousClass.java | 6 +- checker/tests/resourceleak/IOUtilsTest.java | 17 + checker/tests/resourceleak/JavaEETest.java | 7 + ...MultipleMethodParamsMustCallAliasTest.java | 3 + .../tests/resourceleak/TwoOwningMCATest.java | 38 +++ .../resourceleak/TwoSocketContainer.java | 38 +++ .../resourceleak/TwoSocketContainerSafe.java | 43 +++ checker/tests/tainting/Issue5435.java | 7 + checker/tests/wpi-many/testin.txt | 12 +- dataflow/build.gradle | 16 +- dataflow/manual/content.tex | 265 +++++++-------- dataflow/manual/dataflow.tex | 4 +- .../dataflow/analysis/AbstractAnalysis.java | 2 +- .../dataflow/analysis/TransferResult.java | 2 + .../cfg/block/ExceptionBlockImpl.java | 2 +- .../cfg/block/SingleSuccessorBlockImpl.java | 6 +- .../cfg/builder/CFGTranslationPhaseOne.java | 92 +++++- .../dataflow/cfg/node/ArrayAccessNode.java | 2 + .../dataflow/cfg/node/ImplicitThisNode.java | 4 + .../cfg/node/LambdaResultExpressionNode.java | 2 +- .../cfg/node/MethodInvocationNode.java | 2 + .../dataflow/cfg/node/Node.java | 10 +- .../dataflow/cfg/node/SynchronizedNode.java | 2 +- .../cfg/visualize/AbstractCFGVisualizer.java | 4 +- .../constantpropagation/Constant.java | 2 +- docs/CHANGELOG.md | 23 +- docs/checker-framework-webpage.html | 8 +- docs/developer/gsoc-ideas.html | 312 ++++++++++++------ .../release/README-release-process.html | 33 ++ docs/examples/errorprone/build.gradle | 2 +- docs/examples/lombok/build.gradle | 8 +- docs/manual/contributors.tex | 1 + docs/manual/creating-a-checker.tex | 2 +- docs/manual/external-tools.tex | 16 +- docs/manual/index-checker.tex | 4 +- docs/manual/introduction.tex | 8 +- docs/manual/manual.tex | 4 +- docs/manual/nullness-checker.tex | 56 +++- docs/manual/resource-leak-checker.tex | 9 +- docs/manual/warnings.tex | 53 ++- framework-test/build.gradle | 2 +- .../test/TestConfigurationBuilder.java | 4 +- .../checkerframework/taglet/ManualTaglet.java | 2 +- framework/build.gradle | 26 +- .../accumulation/AccumulationChecker.java | 2 +- .../common/aliasing/AliasingTransfer.java | 8 +- .../common/basetype/BaseTypeChecker.java | 11 +- .../common/basetype/BaseTypeVisitor.java | 38 ++- .../common/basetype/messages.properties | 2 + ...InitializedFieldsAnnotatedTypeFactory.java | 5 +- .../ReturnsReceiverAnnotatedTypeFactory.java | 4 +- .../common/util/TypeVisualizer.java | 7 +- .../util/count/AnnotationStatistics.java | 28 +- .../common/value/RangeOrListOfValues.java | 6 +- .../common/value/ReflectiveEvaluator.java | 43 ++- .../SceneToStubWriter.java | 18 +- .../WholeProgramInference.java | 19 ++ .../WholeProgramInferenceImplementation.java | 30 +- ...holeProgramInferenceJavaParserStorage.java | 206 ++++++++++-- .../WholeProgramInferenceScenesStorage.java | 48 +++ .../WholeProgramInferenceStorage.java | 23 ++ .../scenelib/ASceneWrapper.java | 8 +- .../framework/ajava/AnnotationFileStore.java | 2 +- .../ajava/DoubleJavaParserVisitor.java | 13 +- .../framework/ajava/ExpectedTreesVisitor.java | 7 +- .../ajava/InsertAjavaAnnotations.java | 20 +- .../ajava/JointJavacJavaParserVisitor.java | 10 +- .../framework/ajava/TypeAnnotationMover.java | 4 +- .../framework/flow/CFAbstractStore.java | 6 +- .../framework/flow/CFAbstractTransfer.java | 5 +- .../framework/source/SourceChecker.java | 27 +- .../framework/source/SourceVisitor.java | 8 +- .../framework/stub/AddAnnotatedFor.java | 9 +- .../framework/stub/AnnotationFileParser.java | 105 +++++- .../framework/stub/JavaStubifier.java | 6 +- .../stub/RemoveAnnotationsForInference.java | 20 +- .../framework/stub/StubGenerator.java | 10 +- .../framework/stub/ToIndexFileConverter.java | 3 +- .../framework/type/AnnotatedTypeFactory.java | 17 +- .../framework/type/AnnotatedTypeMirror.java | 17 +- .../framework/type/AnnotatedTypeReplacer.java | 12 +- .../type/ElementQualifierHierarchy.java | 2 +- .../type/GenericAnnotatedTypeFactory.java | 38 ++- .../type/TypeFromExpressionVisitor.java | 11 + .../framework/type/TypeFromTreeVisitor.java | 4 +- .../framework/util/AnnotatedTypes.java | 6 +- .../framework/util/JavaParserUtil.java | 14 +- .../util/defaults/QualifierDefaults.java | 2 +- .../dependenttypes/DependentTypesHelper.java | 3 +- .../util/element/ClassTypeParamApplier.java | 5 +- .../framework/util/element/MethodApplier.java | 66 ++-- .../util/element/MethodTypeParamApplier.java | 58 ++-- .../framework/util/element/ParamApplier.java | 58 ++-- .../util/element/SuperTypeApplier.java | 15 +- .../util/element/TypeDeclarationApplier.java | 43 ++- .../util/element/TypeVarUseApplier.java | 22 +- .../util/element/VariableApplier.java | 46 +-- .../typeinference/solver/SubtypesSolver.java | 2 +- .../all-systems/java8/memberref/Issue946.java | 3 - javacutil/build.gradle | 2 +- .../checkerframework/javacutil/TreeUtils.java | 81 ++++- 164 files changed, 2810 insertions(+), 1063 deletions(-) create mode 100644 checker/src/main/java/org/checkerframework/checker/mustcall/IOUtils.astub create mode 100644 checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub create mode 100644 checker/src/main/java/org/checkerframework/checker/nullness/sometimes-nullable.astub create mode 100644 checker/src/main/java/org/checkerframework/checker/resourceleak/IOUtils.astub create mode 100644 checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/qual/AinferTreatAsSibling1.java create mode 100644 checker/tests/ainfer-testchecker/non-annotated/IShouldBeSibling1.java create mode 100644 checker/tests/ainfer-testchecker/non-annotated/OptionGroup.java create mode 100644 checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1InferenceTest.java create mode 100644 checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1Test.java create mode 100644 checker/tests/index/Issue5471.java create mode 100644 checker/tests/nullness/java17/SwitchTestIssue5412.java create mode 100644 checker/tests/resourceleak/IOUtilsTest.java create mode 100644 checker/tests/resourceleak/JavaEETest.java create mode 100644 checker/tests/resourceleak/TwoOwningMCATest.java create mode 100644 checker/tests/resourceleak/TwoSocketContainer.java create mode 100644 checker/tests/resourceleak/TwoSocketContainerSafe.java create mode 100644 checker/tests/tainting/Issue5435.java diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 3b8722659c7..2481f429510 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -174,7 +174,9 @@ jobs: displayName: test-cftests-inference.sh - job: inference_tests_jdk17 dependsOn: - - canary_jobs +## Improve parallelism by depending only on typecheck, not canary, jobs +# - canary_jobs + - typecheck_jdk17 pool: vmImage: 'ubuntu-latest' container: wmdietl/cf-ubuntu-jdk-latest:latest @@ -243,7 +245,8 @@ jobs: displayName: test-misc.sh - job: misc_jdk19 dependsOn: - - canary_jobs + # - canary_jobs + - misc_jdk17 pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk19-plus:latest @@ -415,7 +418,6 @@ jobs: - bash: ./checker/bin-devel/test-guava.sh displayName: test-guava.sh - job: guava_jdk19 - condition: false dependsOn: - canary_jobs - guava_jdk17 diff --git a/build.gradle b/build.gradle index f1766ecb196..cf9bd0bd484 100644 --- a/build.gradle +++ b/build.gradle @@ -1,7 +1,7 @@ import de.undercouch.gradle.tasks.download.Download plugins { - // https://plugins.gradle.org/plugin/com.github.johnrengelman.shadow (v5 requires Gradle 5) + // https://plugins.gradle.org/plugin/com.github.johnrengelman.shadow id 'com.github.johnrengelman.shadow' version '7.1.2' // https://plugins.gradle.org/plugin/de.undercouch.download id 'de.undercouch.download' version '5.3.0' @@ -13,10 +13,11 @@ plugins { // https://plugins.gradle.org/plugin/org.ajoberstar.grgit id 'org.ajoberstar.grgit' version '4.1.1' apply false - // Code formatting; defines targets "spotlessApply" and "spotlessCheck" + // Code formatting; defines targets "spotlessApply" and "spotlessCheck". + // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/" id 'com.diffplug.spotless' version '6.12.0' } -apply plugin: "de.undercouch.download" +apply plugin: 'de.undercouch.download' import org.ajoberstar.grgit.Grgit @@ -62,7 +63,7 @@ ext { // afu = "${annotationTools}/annotation-file-utilities" stubparser = "${parentDir}/stubparser" - stubparserJar = "${stubparser}/javaparser-core/target/stubparser-3.24.7.jar" + stubparserJar = "${stubparser}/javaparser-core/target/stubparser-3.24.9.jar" jtregHome = "${parentDir}/jtreg" plumeScriptsHome = "${project(':checker').projectDir}/bin-devel/.plume-scripts" @@ -72,7 +73,7 @@ ext { // The local git repository, typically in the .git directory, but not for worktrees. // This value is always overwritten, but Gradle needs the variable to be initialized. - localRepo = ".git" + localRepo = '.git' } // Keep in sync with check in @@ -84,8 +85,8 @@ switch (JavaVersion.current()) { case JavaVersion.VERSION_19: break; // Supported versions default: - logger.info("The Checker Framework has only been tested with JDK 8, 11, 17, and 19." + - " You are using JDK " + JavaVersion.current().majorVersion + "."); + logger.info('The Checker Framework has only been tested with JDK 8, 11, 17, and 19.' + + ' You are using JDK ' + JavaVersion.current().majorVersion + '.'); break; } @@ -94,16 +95,16 @@ task setLocalRepo(type:Exec) { standardOutput = new ByteArrayOutputStream() doLast { String worktreeList = standardOutput.toString() - localRepo = worktreeList.substring(0, worktreeList.indexOf(" ")) + "/.git" + localRepo = worktreeList.substring(0, worktreeList.indexOf(' ')) + '/.git' } } // No group so it does not show up in the output of `gradlew tasks` task installGitHooks(type: Copy, dependsOn: 'setLocalRepo') { description 'Copies git hooks to .git directory' - from files("checker/bin-devel/git.post-merge", "checker/bin-devel/git.pre-commit") + from files('checker/bin-devel/git.post-merge', 'checker/bin-devel/git.pre-commit') rename('git\\.(.*)', '$1') - into localRepo + "/hooks" + into localRepo + '/hooks' } spotless { @@ -115,7 +116,7 @@ spotless { // > Could not create task ':checker-qual:spotlessJavaCheck'. // > Could not create task ':checker-qual:spotlessJava'. // > File signature can only be created for existing regular files, given: - // /Users/smillst/jsr308/checker-framework/checker-qual/build/libs/checker-qual-3.25.1-SNAPSHOT.jar + // .../checker-framework/checker-qual/build/libs/checker-qual-3.25.1-SNAPSHOT.jar predeclareDepsFromBuildscript() } @@ -149,7 +150,7 @@ allprojects { // level (third number) if: // * any new checkers have been added, or // * backward-incompatible changes have been made to APIs or elsewhere. - version '3.28.0-eisop2-SNAPSHOT' + version '3.29.0' repositories { mavenCentral() @@ -196,16 +197,16 @@ allprojects { // These are required in Java 16+ because the --illegal-access option is set to deny // by default. None of these packages are accessed via reflection, so the module // only needs to be exported, but not opened. - "--add-exports", "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", - "--add-exports", "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", - "--add-exports", "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", - "--add-exports", "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", - "--add-exports", "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED", - "--add-exports", "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", - "--add-exports", "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", - "--add-exports", "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", + '--add-exports', 'jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED', + '--add-exports', 'jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED', + '--add-exports', 'jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED', + '--add-exports', 'jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED', + '--add-exports', 'jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED', + '--add-exports', 'jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED', + '--add-exports', 'jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED', + '--add-exports', 'jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED', // Required because the Checker Framework reflectively accesses private members in com.sun.tools.javac.comp. - "--add-opens", "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED", + '--add-opens', 'jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED', ] reflectionUtilVersion = '1.0.5' @@ -265,7 +266,7 @@ allprojects { googleJavaFormat().aosp() importOrder('com', 'jdk', 'lib', 'lombok', 'org', 'java', 'javax') // Remove addTypeAnnotation after the next release of Spotless. - formatAnnotations().addTypeAnnotation("DoesNotMatchRegex") + formatAnnotations().addTypeAnnotation('DoesNotMatchRegex') } } // The Spotless plugin uses the latest version of google-java-format @@ -289,7 +290,7 @@ allprojects { } dependencies { - checkerFatJar(project(path: ":checker", configuration: 'fatJar')) + checkerFatJar(project(path: ':checker', configuration: 'fatJar')) } // Add the fat checker.jar to the classpath of every Javadoc task. This allows Javadoc in @@ -303,7 +304,7 @@ allprojects { dependsOn(":framework-test:${tagletVersion}Classes") doFirst { options.encoding = 'UTF-8' - if (!name.equals("javadocDoclintAll")) { + if (!name.equals('javadocDoclintAll')) { options.memberLevel = javadocMemberLevel } classpath += configurations.getByName('checkerFatJar').asFileTree @@ -353,15 +354,15 @@ allprojects { // When sourceCompatibility or release is changed to 11, then the following will be required. // options.compilerArgs += [ - // "--add-exports", "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", - // "--add-exports", "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED', + // '--add-exports', 'jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED', // ] // This is equivalent to writing "exports jdk.compiler/... to ALL-UNNAMED" in the // module-info.java of jdk.compiler, so corresponding --add-opens are only required for @@ -386,8 +387,8 @@ allprojects { // -fallthrough: Don't check fallthroughs. Instead, use Error Prone. Its // warnings are suppressible with a "// fall through" comment. // -classfile: classgraph jar file and https://bugs.openjdk.org/browse/JDK-8190452 - "-Xlint:-options,-fallthrough,-classfile", - "-Xlint", + '-Xlint:-options,-fallthrough,-classfile', + '-Xlint', ] options.encoding = 'UTF-8' @@ -494,7 +495,7 @@ task maybeCloneAndBuildDependencies() { executable 'ls' ignoreExitValue = true } - throw new RuntimeException("Can't find stubparser jar: " + stubparserJar) + throw new RuntimeException('Can\'t find stubparser jar: ' + stubparserJar) } } } @@ -537,14 +538,14 @@ def createCheckTypeTask(projectName, taskName, checker, args = []) { '-AnoJreVersionCheck', ] options.compilerArgs += args - options.forkOptions.jvmArgs += ["-Xmx2g"] + options.forkOptions.jvmArgs += ['-Xmx2g'] if (isJava8) { options.compilerArgs += [ - "-source", - "8", - "-target", - "8" + '-source', + '8', + '-target', + '8' ] } else { options.fork = true @@ -557,12 +558,12 @@ task htmlValidate(type: Exec, group: 'Format') { description 'Validate that HTML files are well-formed' executable 'html5validator' args = [ - "--ignore", - "/api/", - "/build/", - "/docs/manual/manual.html", - "/docs/manual/plume-bib/docs/index.html", - "/checker/jdk/nullness/src/java/lang/ref/package.html" + '--ignore', + '/api/', + '/build/', + '/docs/manual/manual.html', + '/docs/manual/plume-bib/docs/index.html', + '/checker/jdk/nullness/src/java/lang/ref/package.html' ] } @@ -626,14 +627,14 @@ configurations { } dependencies { - requireJavadoc "org.plumelib:require-javadoc:1.0.5" + requireJavadoc 'org.plumelib:require-javadoc:1.0.6' } task requireJavadoc(type: JavaExec, group: 'Documentation') { description = 'Ensures that Javadoc documentation exists in source code.' - mainClass = "org.plumelib.javadoc.RequireJavadoc" + mainClass = 'org.plumelib.javadoc.RequireJavadoc' classpath = configurations.requireJavadoc - args "checker/src/main/java", "checker-qual/src/main/java", "checker-util/src/main/java", "dataflow/src/main/java", "framework/src/main/java", "framework-test/src/main/java", "javacutil/src/main/java" + args 'checker/src/main/java', 'checker-qual/src/main/java', 'checker-util/src/main/java', 'dataflow/src/main/java', 'framework/src/main/java', 'framework-test/src/main/java', 'javacutil/src/main/java' } @@ -651,7 +652,7 @@ def createJavadocTask(taskName, taskDescription, memberLevel) { destinationDir = file("${rootDir}/docs/tmpapi") destinationDir.mkdirs() subprojects.forEach { - if (!it.name.startsWith("checker-qual-android")) { + if (!it.name.startsWith('checker-qual-android')) { source += it.sourceSets.main.allJava } } @@ -673,7 +674,7 @@ task manual(group: 'Documentation') { description 'Build the manual' doLast { exec { - commandLine "make", "-C", "docs/manual", "all" + commandLine 'make', '-C', 'docs/manual', 'all' } } } @@ -743,9 +744,9 @@ task getHtmlTools() { // No group so it does not show up in the output of `gradlew tasks` task pythonIsInstalled(type: Exec) { - description "Check that the python3 executable is installed." - executable = "python3" - args "--version" + description 'Check that the python3 executable is installed.' + executable = 'python3' + args '--version' } task tags { @@ -753,10 +754,10 @@ task tags { description 'Create Emacs TAGS table' doLast { exec { - commandLine "etags", "-i", "checker/TAGS", "-i", "checker-qual/TAGS", "-i", "checker-util/TAGS", "-i", "dataflow/TAGS", "-i", "framework/TAGS", "-i", "framework-test/TAGS", "-i", "javacutil/TAGS", "-i", "docs/manual/TAGS" + commandLine 'etags', '-i', 'checker/TAGS', '-i', 'checker-qual/TAGS', '-i', 'checker-util/TAGS', '-i', 'dataflow/TAGS', '-i', 'framework/TAGS', '-i', 'framework-test/TAGS', '-i', 'javacutil/TAGS', '-i', 'docs/manual/TAGS' } exec { - commandLine "make", "-C", "docs/manual", "tags" + commandLine 'make', '-C', 'docs/manual', 'tags' } } } @@ -825,7 +826,7 @@ subprojects { if (!project.name.startsWith('checker-qual-android')) { task tags(type: Exec) { description 'Create Emacs TAGS table' - commandLine "bash", "-c", "find . \\( -name build \\) -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" } } @@ -840,7 +841,7 @@ subprojects { // Adds manifest to all Jar files tasks.withType(Jar) { includeEmptyDirs = false - if (archiveFileName.get().startsWith("checker-qual") || archiveFileName.get().startsWith("checker-util")) { + if (archiveFileName.get().startsWith('checker-qual') || archiveFileName.get().startsWith('checker-util')) { metaInf { from './LICENSE.txt' } @@ -850,15 +851,15 @@ subprojects { } } manifest { - attributes("Implementation-Version": "${project.version}") - attributes("Implementation-URL": "https://eisop.github.io/") - if (! archiveFileName.get().endsWith("source.jar")) { - attributes('Automatic-Module-Name': "org.checkerframework." + project.name.replaceAll('-', '.')) + attributes('Implementation-Version': "${project.version}") + attributes('Implementation-URL': 'https://eisop.github.io/') + if (! archiveFileName.get().endsWith('source.jar')) { + attributes('Automatic-Module-Name': 'org.checkerframework.' + project.name.replaceAll('-', '.')) } - if (archiveFileName.get().startsWith("checker-qual") || archiveFileName.get().startsWith("checker-util")) { - attributes("Bundle-License": "MIT") + if (archiveFileName.get().startsWith('checker-qual') || archiveFileName.get().startsWith('checker-util')) { + attributes('Bundle-License': 'MIT') } else { - attributes("Bundle-License": "(GPL-2.0-only WITH Classpath-exception-2.0)") + attributes('Bundle-License': '(GPL-2.0-only WITH Classpath-exception-2.0)') } } } @@ -903,48 +904,48 @@ subprojects { exec { executable "${jtregHome}/bin/jtreg" args = [ - "-dir:${projectDir}/jtreg", - "-workDir:${jtregOutput}/${name}/work", - "-reportDir:${jtregOutput}/${name}/report", - "-verbose:error,fail", - // Don't add debugging information - // "-javacoptions:-g", - "-keywords:!ignore", - "-samevm", - "-javacoptions:-classpath ${tasks.shadowJar.archiveFile.get()}:${sourceSets.test.output.asPath}", - // Required for checker/jtreg/nullness/PersistUtil.java and other tests - "-vmoptions:-classpath ${tasks.shadowJar.archiveFile.get()}:${sourceSets.test.output.asPath}", + "-dir:${projectDir}/jtreg", + "-workDir:${jtregOutput}/${name}/work", + "-reportDir:${jtregOutput}/${name}/report", + '-verbose:error,fail', + // Don't add debugging information + // '-javacoptions:-g', + '-keywords:!ignore', + '-samevm', + "-javacoptions:-classpath ${tasks.shadowJar.archiveFile.get()}:${sourceSets.test.output.asPath}", + // Required for checker/jtreg/nullness/PersistUtil.java and other tests + "-vmoptions:-classpath ${tasks.shadowJar.archiveFile.get()}:${sourceSets.test.output.asPath}", ] if (isJava8) { // Use Error Prone javac and source/target 8 args += [ "-vmoptions:-Xbootclasspath/p:${configurations.javacJar.asPath}", "-javacoptions:-Xbootclasspath/p:${configurations.javacJar.asPath}", - "-javacoptions:-source 8", - "-javacoptions:-target 8" + '-javacoptions:-source 8', + '-javacoptions:-target 8' ] } else { args += [ // checker/jtreg/nullness/defaultsPersist/ReferenceInfoUtil.java // uses the jdk.jdeps module. - "-javacoptions:--add-modules jdk.jdeps", - "-javacoptions:--add-exports=jdk.jdeps/com.sun.tools.classfile=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.jdeps/com.sun.tools.classfile=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", + '-javacoptions:--add-modules jdk.jdeps', + '-javacoptions:--add-exports=jdk.jdeps/com.sun.tools.classfile=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.jdeps/com.sun.tools.classfile=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED', ] } if (project.name.is('framework')) { // Do not check for the annotated JDK args += [ - "-javacoptions:-ApermitMissingJdk" + '-javacoptions:-ApermitMissingJdk' ] } else if (project.name.is('checker')) { args += [ @@ -962,9 +963,9 @@ subprojects { } } catch (Exception ex) { if (ex.getCause() != null && ex.getCause().getCause()!= null) { - String msg = ex.getCause().getLocalizedMessage() + ":\n" - msg += ex.getCause().getCause().getLocalizedMessage() + "\n" - msg += "Have you installed jtreg?" + String msg = ex.getCause().getLocalizedMessage() + ':\n' + msg += ex.getCause().getCause().getLocalizedMessage() + '\n' + msg += 'Have you installed jtreg?' println msg } throw ex @@ -975,7 +976,7 @@ subprojects { // Create a task for each JUnit test class whose name is the same as the JUnit class name. sourceSets.test.allJava.filter { it.path.contains('test/junit') }.forEach { file -> - String junitClassName = file.name.replaceAll(".java", "") + String junitClassName = file.name.replaceAll('.java', '') tasks.create(name: "${junitClassName}", type: Test) { description "Run ${junitClassName} tests." include "**/${name}.class" @@ -997,7 +998,7 @@ subprojects { } if (project.hasProperty('emit.test.debug')) { - systemProperties += ["emit.test.debug": 'true'] + systemProperties += ['emit.test.debug': 'true'] } testLogging { @@ -1006,8 +1007,8 @@ subprojects { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and expected diagnostics not found. - exceptionFormat "full" - events "failed" + exceptionFormat 'full' + events 'failed' // Don't show the uninteresting stack traces from the exceptions. showStackTraces = false @@ -1151,7 +1152,7 @@ task checkBasicStyle(group: 'Format') { if (!it.file.isDirectory()) { boolean blankLineAtEnd = false String fileName = it.file.getName() - boolean checkTabs = !fileName.equals("Makefile") + boolean checkTabs = !fileName.equals('Makefile') it.file.eachLine { line -> if (line.endsWith(' ')) { println("Trailing whitespace: ${it.file.absolutePath}") @@ -1202,7 +1203,7 @@ task checkBasicStyle(group: 'Format') { } } if (failed) { - throw new GradleException("Files do not meet basic style guidelines.") + throw new GradleException('Files do not meet basic style guidelines.') } } } @@ -1241,7 +1242,7 @@ task releaseBuild(group: 'Build') { release = true /* Not sure why typetools enforces build on Java 8. if (!isJava8) { - throw new RuntimeException("You must use Java 8 when making a release. You are using " + JavaVersion.current() + ".") + throw new RuntimeException('You must use Java 8 when making a release. You are using ' + JavaVersion.current() + '.') } */ } diff --git a/checker-qual-android/build.gradle b/checker-qual-android/build.gradle index d767e42091a..f0dfa8e2d0c 100644 --- a/checker-qual-android/build.gradle +++ b/checker-qual-android/build.gradle @@ -1,4 +1,4 @@ -evaluationDependsOn(":checker-qual") +evaluationDependsOn(':checker-qual') task copySources(type: Copy) { description 'Copy checker-qual source to checker-qual-android' @@ -9,8 +9,8 @@ task copySources(type: Copy) { delete file('src') } from files('../checker-qual/src/main') - include "**/*.java" - exclude "**/SignednessUtilExtra.java" + include '**/*.java' + exclude '**/SignednessUtilExtra.java' into file('src/main') // Not read only because "replaceAnnotations" tasks writes to the files. @@ -28,8 +28,8 @@ sourcesJar.dependsOn(copySources) */ task replaceAnnotations { doLast { - fileTree(dir: 'src', include: "**/*.java").each { - it.text = it.text.replaceAll("RetentionPolicy.RUNTIME", "RetentionPolicy.CLASS") + fileTree(dir: 'src', include: '**/*.java').each { + it.text = it.text.replaceAll('RetentionPolicy.RUNTIME', 'RetentionPolicy.CLASS') } } } @@ -42,7 +42,7 @@ clean { delete file('src') } -apply from: rootProject.file("gradle-mvn-push.gradle") +apply from: rootProject.file('gradle-mvn-push.gradle') /** Adds information to the publication for uploading to Maven repositories. */ final checkerQualAndroidPom(publication) { diff --git a/checker-qual/build.gradle b/checker-qual/build.gradle index bf05b97db0f..647394cff11 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:6.3.1" + classpath 'biz.aQute.bnd:biz.aQute.bnd.gradle:6.3.1' // Don't add implementation dependencies; checker-qual.jar should have no dependencies. } } @@ -21,7 +21,7 @@ jar { } } -apply from: rootProject.file("gradle-mvn-push.gradle") +apply from: rootProject.file('gradle-mvn-push.gradle') /** Adds information to the publication for uploading to Maven repositories. */ final checkerQualPom(publication) { diff --git a/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java b/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java index 92ab74f04d5..66e36304463 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java @@ -185,6 +185,13 @@ public enum ConversionCategory { return null; } + /** + * The conversion categories that have a corresponding conversion character. This lacks UNUSED, + * TIME_AND_INT, etc. + */ + private static ConversionCategory[] conversionCategoriesWithChar = + new ConversionCategory[] {GENERAL, CHAR, INT, FLOAT, TIME}; + /** * Converts a conversion character to a category. For example: * @@ -197,7 +204,7 @@ public enum ConversionCategory { */ @SuppressWarnings("nullness:dereference.of.nullable") // `chars` field is non-null for these public static ConversionCategory fromConversionChar(char c) { - for (ConversionCategory v : new ConversionCategory[] {GENERAL, CHAR, INT, FLOAT, TIME}) { + for (ConversionCategory v : conversionCategoriesWithChar) { if (v.chars.contains(String.valueOf(c))) { return v; } @@ -213,6 +220,10 @@ public static boolean isSubsetOf(ConversionCategory a, ConversionCategory b) { return intersect(a, b) == a; } + /** Conversion categories that need to be considered by {@link #intersect}. */ + private static ConversionCategory[] conversionCategoriesForIntersect = + new ConversionCategory[] {CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME, NULL}; + /** * Returns the intersection of two categories. This is seldomly needed. * @@ -251,13 +262,11 @@ public static ConversionCategory intersect(ConversionCategory a, ConversionCateg // GENERAL Set> bs = arrayToSet(b.types); as.retainAll(bs); // intersection - for (ConversionCategory v : - new ConversionCategory[] { - CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME, NULL - }) { + for (ConversionCategory v : conversionCategoriesForIntersect) { @SuppressWarnings( - "nullness:argument.type.incompatible") // `types` field is null only for UNUSED + "nullness:argument.type.incompatible" // `types` field is null only for UNUSED // and GENERAL + ) Set> vs = arrayToSet(v.types); if (vs.equals(as)) { return v; @@ -266,6 +275,10 @@ public static ConversionCategory intersect(ConversionCategory a, ConversionCateg throw new RuntimeException(); } + /** Conversion categories that need to be considered by {@link #union}. */ + private static ConversionCategory[] conversionCategoriesForUnion = + new ConversionCategory[] {NULL, CHAR_AND_INT, INT_AND_TIME, CHAR, INT, FLOAT, TIME}; + /** * Returns the union of two categories. This is seldomly needed. * @@ -304,13 +317,11 @@ public static ConversionCategory union(ConversionCategory a, ConversionCategory // GENERAL Set> bs = arrayToSet(b.types); as.addAll(bs); // union - for (ConversionCategory v : - new ConversionCategory[] { - NULL, CHAR_AND_INT, INT_AND_TIME, CHAR, INT, FLOAT, TIME - }) { + for (ConversionCategory v : conversionCategoriesForUnion) { @SuppressWarnings( - "nullness:argument.type.incompatible") // `types` field is null only for UNUSED + "nullness:argument.type.incompatible" // `types` field is null only for UNUSED // and GENERAL + ) Set> vs = arrayToSet(v.types); if (vs.equals(as)) { return v; diff --git a/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java b/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java index 3ca3a530a41..7ccba9dc9c9 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java @@ -103,6 +103,10 @@ public static boolean isSubsetOf(I18nConversionCategory a, I18nConversionCategor return intersect(a, b) == a; } + /** Conversion categories that need to be considered by {@link #intersect}. */ + private static I18nConversionCategory[] conversionCategoriesForIntersect = + new I18nConversionCategory[] {DATE, NUMBER}; + /** * Returns the intersection of the two given I18nConversionCategories. * @@ -138,7 +142,7 @@ public static I18nConversionCategory intersect( // GENERAL Set> bs = arrayToSet(b.types); as.retainAll(bs); // intersection - for (I18nConversionCategory v : new I18nConversionCategory[] {DATE, NUMBER}) { + for (I18nConversionCategory v : conversionCategoriesForIntersect) { @SuppressWarnings( "nullness:argument.type.incompatible") // in those values, `types` field is // non-null diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/HasSubsequence.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/HasSubsequence.java index 202491c3cb7..85e265a1940 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/HasSubsequence.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/HasSubsequence.java @@ -31,9 +31,9 @@ * annotations: * *
    - *
  • If {@code i} is {@code @IndexFor("this")}, then {@code start + i} is + *
  • If {@code i} is {@code @IndexFor("this")}, then {@code this.start + i} is * {@code @IndexFor("array")}. - *
  • If {@code j} is {@code @IndexFor("array")}, then {@code j - start } is + *
  • If {@code j} is {@code @IndexFor("array")}, then {@code j - this.start } is * {@code @IndexFor("this")}. *
* diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThan.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThan.java index 6e0c544402c..46b87853015 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThan.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThan.java @@ -16,8 +16,6 @@ *

If an expression's type has this annotation, then at run time, the expression evaluates to a * value that is less than the value of the expression in the annotation. * - *

{@code @LessThan("end + 1")} is equivalent to {@code @LessThanOrEqual("end")}. - * *

Subtyping: * *

    @@ -25,7 +23,7 @@ *
  • {@code @LessThan({"a", "b"})} is not related to {@code @LessThan({"a", "c"})}. *
* - * @checker_framework.manual #index-inequalities Index Chceker Inequalities + * @checker_framework.manual #index-inequalities Index Checker Inequalities */ @Documented @Retention(RetentionPolicy.RUNTIME) diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanBottom.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanBottom.java index 65c7829d2ad..3eda6aea692 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanBottom.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanBottom.java @@ -11,7 +11,7 @@ /** * The bottom type in the LessThan type system. Programmers should rarely write this type. * - * @checker_framework.manual #index-inequalities Index Chceker Inequalities + * @checker_framework.manual #index-inequalities Index Checker Inequalities * @checker_framework.manual #bottom-type the bottom type */ @Documented diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java index d962c134f86..ca5b2f1a98f 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java @@ -14,7 +14,7 @@ * The top qualifier for the LessThan type hierarchy. It indicates that no other expression is known * to be larger than the annotated one. * - * @checker_framework.manual #index-inequalities Index Chceker Inequalities + * @checker_framework.manual #index-inequalities Index Checker Inequalities */ @Documented @Retention(RetentionPolicy.RUNTIME) diff --git a/checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/CreatesMustCallFor.java b/checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/CreatesMustCallFor.java index 22b1923c439..b1c71880a61 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/CreatesMustCallFor.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/CreatesMustCallFor.java @@ -27,8 +27,8 @@ * *

Because this annotation can only add obligations, it can be written safely on any method, even * one that does not actually create a new obligation. Writing this annotation on a method that does - * not actually create any new obligations may lead to false positives, but never to false - * negatives. + * not actually create any new obligations may lead to false alarms (warnings at correct code), but + * never to missed alarms (lack of warnings at incorrect code). * *

As an example, consider the following code, which uses a {@code @CreatesMustCallFor} * annotation to indicate that the {@code reset()} method re-assigns the {@code socket} field: diff --git a/checker-qual/src/main/java/org/checkerframework/common/value/qual/MinLen.java b/checker-qual/src/main/java/org/checkerframework/common/value/qual/MinLen.java index 0290b93b321..63a5a04367b 100644 --- a/checker-qual/src/main/java/org/checkerframework/common/value/qual/MinLen.java +++ b/checker-qual/src/main/java/org/checkerframework/common/value/qual/MinLen.java @@ -11,7 +11,7 @@ * elements. An alias for an {@link ArrayLenRange} annotation with a {@code from} field and the * maximum possible value for an array length ({@code Integer.MAX_VALUE}) as its {@code to} field. * - *

This annotation is used extensively by the Index Chcker. + *

This annotation is used extensively by the Index Checker. * * @checker_framework.manual #constant-value-checker Constant Value Checker */ diff --git a/checker-util/build.gradle b/checker-util/build.gradle index 18ea2d6c9ac..c1cde552659 100644 --- a/checker-util/build.gradle +++ b/checker-util/build.gradle @@ -9,7 +9,7 @@ dependencies { testImplementation group: 'junit', name: 'junit', version: '4.13.2' } -apply from: rootProject.file("gradle-mvn-push.gradle") +apply from: rootProject.file('gradle-mvn-push.gradle') /** Adds information to the publication for uploading to Maven repositories. */ final checkerUtilPom(publication) { diff --git a/checker-util/src/main/java/org/checkerframework/checker/i18nformatter/util/I18nFormatUtil.java b/checker-util/src/main/java/org/checkerframework/checker/i18nformatter/util/I18nFormatUtil.java index f65752ab97c..dc002a5021e 100644 --- a/checker-util/src/main/java/org/checkerframework/checker/i18nformatter/util/I18nFormatUtil.java +++ b/checker-util/src/main/java/org/checkerframework/checker/i18nformatter/util/I18nFormatUtil.java @@ -112,10 +112,19 @@ public static boolean isFormat(String format) { return true; } + /** An I18n cenversion directive. */ private static class I18nConversion { - public int index; - public I18nConversionCategory category; + /** The index into the string. */ + public final int index; + /** The conversion category. */ + public final I18nConversionCategory category; + /** + * Creates a new I18nConversion. + * + * @param index the index into the string + * @param category the conversion category + */ public I18nConversion(int index, I18nConversionCategory category) { this.index = index; this.category = category; diff --git a/checker/bin-devel/test-plume-lib.sh b/checker/bin-devel/test-plume-lib.sh index 664cf684d50..4776b44a4a1 100755 --- a/checker/bin-devel/test-plume-lib.sh +++ b/checker/bin-devel/test-plume-lib.sh @@ -9,25 +9,24 @@ echo "SHELLOPTS=${SHELLOPTS}" # Optional argument $1 is the group. GROUPARG=$1 echo "GROUPARG=$GROUPARG" -# These are all the Java projects at https://github.com/eisop-plume-lib +# These are all the Java projects at https://github.com/eisop-plume-lib as of Dec 2022. if [[ "${GROUPARG}" == "bcel-util" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "bibtex-clean" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "html-pretty-print" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "icalavailable" ]]; then PACKAGES=("${GROUPARG}"); fi +if [[ "${GROUPARG}" == "javadoc-lookup" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "lookup" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "multi-version-control" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "options" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "plume-util" ]]; then PACKAGES=("${GROUPARG}"); fi +if [[ "${GROUPARG}" == "reflection-util" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "require-javadoc" ]]; then PACKAGES=("${GROUPARG}"); fi if [[ "${GROUPARG}" == "all" ]] || [[ "${GROUPARG}" == "" ]]; then if java -version 2>&1 | grep version | grep 1.8 ; then - # options does not compile under JDK 8 - PACKAGES=(bcel-util bibtex-clean html-pretty-print icalavailable lookup multi-version-control plume-util require-javadoc) - elif java -version 2>&1 | grep version | grep 17 ; then - # TODO bcel-util does not compile under JDK 17 - PACKAGES=(bibtex-clean html-pretty-print icalavailable lookup multi-version-control options plume-util require-javadoc) + # options master branch does not compile under JDK 8 + PACKAGES=(bcel-util bibtex-clean html-pretty-print icalavailable javadoc-lookup lookup multi-version-control plume-util reflection-util require-javadoc) else - PACKAGES=(bcel-util bibtex-clean html-pretty-print icalavailable lookup multi-version-control options plume-util require-javadoc) + PACKAGES=(bcel-util bibtex-clean html-pretty-print icalavailable javadoc-lookup lookup multi-version-control options plume-util reflection-util require-javadoc) fi fi if [ -z ${PACKAGES+x} ]; then diff --git a/checker/bin-devel/wpi-plumelib/bcel-util.expected b/checker/bin-devel/wpi-plumelib/bcel-util.expected index e69de29bb2d..444a90c7684 100644 --- a/checker/bin-devel/wpi-plumelib/bcel-util.expected +++ b/checker/bin-devel/wpi-plumelib/bcel-util.expected @@ -0,0 +1,6 @@ +BcelUtil.java:771: error: [argument] incompatible argument for parameter typename of parseFqBinaryName. + Signatures.ClassnameAndDimensions.parseFqBinaryName(classname); + ^ + found : @SignatureUnknown String + required: @FqBinaryName String +1 error diff --git a/checker/build.gradle b/checker/build.gradle index 15595699588..ebd9906b7c3 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -59,15 +59,19 @@ dependencies { shadow project(':checker-util') // Called Methods Checker AutoValue + Lombok support - testImplementation "com.google.auto.value:auto-value-annotations:1.7.4" - testImplementation "com.google.auto.value:auto-value:1.7.4" - testImplementation "com.ryanharter.auto.value:auto-value-parcel:0.2.9" - testImplementation "org.projectlombok:lombok:1.18.24" + testImplementation 'com.google.auto.value:auto-value-annotations:1.7.4' + testImplementation 'com.google.auto.value:auto-value:1.7.4' + testImplementation 'com.ryanharter.auto.value:auto-value-parcel:0.2.9' + testImplementation 'org.projectlombok:lombok:1.18.24' // Called Methods Checker support for detecting misuses of AWS APIs - testImplementation "com.amazonaws:aws-java-sdk-ec2" - testImplementation "com.amazonaws:aws-java-sdk-kms" + testImplementation 'com.amazonaws:aws-java-sdk-ec2' + testImplementation 'com.amazonaws:aws-java-sdk-kms' // The AWS SDK is used for testing the Called Methods Checker. - testImplementation platform("com.amazonaws:aws-java-sdk-bom:1.12.293") + testImplementation platform('com.amazonaws:aws-java-sdk-bom:1.12.293') + // For the Resource Leak Checker's support for JavaEE. + testImplementation 'javax.servlet:javax.servlet-api:3.1.0' + // For the Resource Leak Checker's support for IOUtils. + testImplementation 'commons-io:commons-io:2.11.0' // Required for checker/tests/index-initializedfields/RequireJavadoc.java if (JavaVersion.current() == JavaVersion.VERSION_1_8) { @@ -95,7 +99,7 @@ generateGitProperties.dependsOn(':installGitHooks') jar { manifest { - attributes("Main-Class": "org.checkerframework.framework.util.CheckerMain") + attributes('Main-Class': 'org.checkerframework.framework.util.CheckerMain') } } @@ -104,29 +108,29 @@ task copyJarsToDist(dependsOn: shadowJar, group: 'Build') { description 'Builds or downloads jars required by CheckerMain and puts them in checker/dist/.' dependsOn project(':checker-qual').tasks.jar doLast { - def checkerQualJarFile = file(project(':checker-qual').tasks.getByName("jar").archivePath) + def checkerQualJarFile = file(project(':checker-qual').tasks.getByName('jar').archivePath) if (!checkerQualJarFile.exists()) { - throw new GradleException("File not found: " + checkerQualJarFile) + throw new GradleException('File not found: ' + checkerQualJarFile) } copy { from checkerQualJarFile into "${projectDir}/dist" rename { String fileName -> // remove version number on checker-qual.jar - fileName.replace(fileName, "checker-qual.jar") + fileName.replace(fileName, 'checker-qual.jar') } } - def checkerUtilJarFile = file(project(':checker-util').tasks.getByName("jar").archivePath) + def checkerUtilJarFile = file(project(':checker-util').tasks.getByName('jar').archivePath) if (!checkerUtilJarFile.exists()) { - throw new GradleException("File not found: " + checkerUtilJarFile) + throw new GradleException('File not found: ' + checkerUtilJarFile) } copy { from checkerUtilJarFile into "${projectDir}/dist" rename { String fileName -> // remove version number on checker-util.jar - fileName.replace(fileName, "checker-util.jar") + fileName.replace(fileName, 'checker-util.jar') } } @@ -134,7 +138,7 @@ task copyJarsToDist(dependsOn: shadowJar, group: 'Build') { from configurations.javacJar into "${projectDir}/dist" rename { String fileName -> - fileName.replace(fileName, "javac.jar") + fileName.replace(fileName, 'javac.jar') } } } @@ -145,8 +149,8 @@ assemble.dependsOn copyJarsToDist task allSourcesJar(type: Jar, group: 'Build') { description 'Creates a sources jar that includes sources for all Checker Framework classes in checker.jar' destinationDirectory = file("${projectDir}/dist") - archiveFileName = "checker-source.jar" - archiveClassifier = "sources" + archiveFileName = 'checker-source.jar' + archiveClassifier = 'sources' from (sourceSets.main.java, project(':framework').sourceSets.main.allJava, project(':dataflow').sourceSets.main.allJava, project(':javacutil').sourceSets.main.allJava, project(':checker-qual').sourceSets.main.allJava, project(':checker-util').sourceSets.main.allJava) @@ -156,8 +160,8 @@ task allJavadocJar(type: Jar, group: 'Build') { description 'Creates javadoc jar including Javadoc for all of the Checker Framework' dependsOn rootProject.tasks.allJavadoc destinationDirectory = file("${projectDir}/dist") - archiveFileName = "checker-javadoc.jar" - archiveClassifier = "javadoc" + archiveFileName = 'checker-javadoc.jar' + archiveClassifier = 'javadoc' from rootProject.tasks.allJavadoc.destinationDir } @@ -175,7 +179,7 @@ task checkerJar(type: ShadowJar, dependsOn: compileJava, group: 'Build') { // To see what files are incorporated into the shadow jar file: // doLast { println sourceSets.main.runtimeClasspath.asPath } manifest { - attributes("Main-Class": "org.checkerframework.framework.util.CheckerMain") + attributes('Main-Class': 'org.checkerframework.framework.util.CheckerMain') } exclude 'org/checkerframework/**/qual/*' exclude 'org/checkerframework/checker/*/util/*' @@ -217,17 +221,17 @@ artifacts { clean { delete "${projectDir}/dist" - delete "tests/calledmethods-delomboked" - delete("tests/ainfer-testchecker/annotated") - delete("tests/ainfer-testchecker/inference-output") - delete("tests/ainfer-nullness/annotated") - delete("tests/ainfer-nullness/inference-output") - delete("tests/ainfer-index/annotated") - delete("tests/ainfer-index/inference-output") + delete 'tests/calledmethods-delomboked' + delete('tests/ainfer-testchecker/annotated') + delete('tests/ainfer-testchecker/inference-output') + delete('tests/ainfer-nullness/annotated') + delete('tests/ainfer-nullness/inference-output') + delete('tests/ainfer-index/annotated') + delete('tests/ainfer-index/inference-output') } // Add non-junit tests -createCheckTypeTask(project.name, "CompilerMessages", +createCheckTypeTask(project.name, 'CompilerMessages', 'org.checkerframework.checker.compilermsgs.CompilerMessagesChecker') checkCompilerMessages { doFirst { @@ -290,7 +294,7 @@ task demosTests(dependsOn: copyJarsToDist, group: 'Verification') { ant.properties.put('checker.lib', file("${projectDir}/dist/checker.jar").absolutePath) ant.ant(dir: demosDir.toString()) } else { - println("Skipping demosTests because they only work with Java 8.") + println('Skipping demosTests because they only work with Java 8.') } } } @@ -319,7 +323,7 @@ task jtregJdk11Tests(dependsOn: ':downloadJtreg', group: 'Verification') { String name = 'all' doLast { if (isJava8) { - println "This test is only run with JDK 11+." + println 'This test is only run with JDK 11+.' return; } exec { @@ -328,21 +332,21 @@ task jtregJdk11Tests(dependsOn: ':downloadJtreg', group: 'Verification') { "-dir:${projectDir}/jtregJdk11", "-workDir:${jtregOutput}/${name}/work", "-reportDir:${jtregOutput}/${name}/report", - "-verbose:summary", - "-javacoptions:-g", - "-keywords:!ignore", - "-samevm", + '-verbose:summary', + '-javacoptions:-g', + '-keywords:!ignore', + '-samevm', "-javacoptions:-classpath ${tasks.shadowJar.archiveFile.get()}:${sourceSets.test.output.asPath}", "-vmoptions:-classpath ${tasks.shadowJar.archiveFile.get()}:${sourceSets.test.output.asPath}", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", - "-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED', + '-vmoptions:--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED', "-javacoptions:-classpath ${sourceSets.testannotations.output.asPath}", // Location of jtreg tests '.' @@ -385,7 +389,7 @@ task delombok { if (skipDelombok) { delombok.enabled = false } else { - tasks.test.dependsOn("delombok") + tasks.test.dependsOn('delombok') } /// @@ -409,7 +413,7 @@ task ainferTestCheckerGenerateStubs(type: Test) { dependsOn(compileTestJava) doFirst { - delete("tests/ainfer-testchecker/annotated") + delete('tests/ainfer-testchecker/annotated') delete("${buildDir}/ainfer-testchecker/") } outputs.upToDateWhen { false } @@ -419,12 +423,12 @@ task ainferTestCheckerGenerateStubs(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } doLast { - copyNonannotatedToAnnotatedDirectory("ainfer-testchecker") + copyNonannotatedToAnnotatedDirectory('ainfer-testchecker') // The stub file format doesn't support annotations on anonymous inner classes, so // this test also expects errors on these tests that expect annotations to be inferred // inside anonymous classes. @@ -435,7 +439,7 @@ task ainferTestCheckerGenerateStubs(type: Test) { // contains an annotation definition. The stub file parser does not support reading // files that define annotations; this test can be reinstated if the stub parser // is extended to support annotation definitions. - delete("tests/ainfer-testchecker/annotated/all-systems/Issue4083.java") + delete('tests/ainfer-testchecker/annotated/all-systems/Issue4083.java') copy { from file('tests/ainfer-testchecker/non-annotated/UsesAnonymous.java') @@ -455,8 +459,8 @@ task ainferTestCheckerValidateStubs(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } } @@ -465,7 +469,7 @@ task ainferTestCheckerGenerateAjava(type: Test) { dependsOn(compileTestJava) doFirst { - delete("tests/ainfer-testchecker/annotated") + delete('tests/ainfer-testchecker/annotated') delete("${buildDir}/ainfer-testchecker/") } outputs.upToDateWhen { false } @@ -475,54 +479,23 @@ task ainferTestCheckerGenerateAjava(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } doLast { - copyNonannotatedToAnnotatedDirectory("ainfer-testchecker") + copyNonannotatedToAnnotatedDirectory('ainfer-testchecker') - // A crash occurs because of a bug in Java Parser when trying to read the .ajava - // file produced for these tests. Reinstate them when https://github.com/javaparser/javaparser/pull/3527 - // has been merged and released, and we've updated to a JavaParser version with that fix. - delete("tests/ainfer-testchecker/annotated/all-systems/java8/memberref/Issue946.java") - delete("tests/ainfer-testchecker/annotated/all-systems/java8/memberref/Receivers.java") + // AinferTestCheckerAjavaValidationTest fails with "warning: (purity.methodref)", whenever + // there is a user-defined generic interface, and a variable of that type is assigned a + // method reference. + delete('tests/ainfer-testchecker/annotated/all-systems/java8/memberref/Issue946.java') + delete('tests/ainfer-testchecker/annotated/all-systems/java8/memberref/Receivers.java') // This test must be deleted, because otherwise an error about a missing type in an // ajava file is issued. The test itself shouldn't be run as an all-systems test while testing // WPI; see the copy in the non-annotated WPI tests for an explanation. - delete("tests/ainfer-testchecker/annotated/all-systems/java8/memberref/Purity.java") - - // These tests cause an error like the following when their corresponding ajava files are read: - // :0: warning: Annotations-org.checkerframework.common.value.ValueChecker.ajava:(line 3,col 1): Skipping annotation type: Anno - delete("tests/ainfer-testchecker/annotated/all-systems/Annotations.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue4083.java") - - // These tests cause unsuppressable errors from the Annotation File Parser, so they are also - // skipped. The errors are of the form: - // :0: warning: ConditionalExpressions-org.checkerframework.common.value.ValueChecker.ajava:(line 53,col 10): Annotations on intersection types are not yet supported - // These tests can all be reinstated when the Annotation File Parser is enhanced to support - // intersection types. - delete("tests/ainfer-testchecker/annotated/all-systems/ConditionalExpressions.java") - delete("tests/ainfer-testchecker/annotated/all-systems/GenericCrazyBounds.java") - delete("tests/ainfer-testchecker/annotated/all-systems/InferAndIntersection.java") - delete("tests/ainfer-testchecker/annotated/all-systems/IntersectionTypes.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue1102.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue1690.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue2195.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue2198.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue2739.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue3120.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue3302.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue577.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Issue717.java") - delete("tests/ainfer-testchecker/annotated/all-systems/MultipleUnions.java") - // TODO: why does this specific ajava file need to be deleted, even though its corresponding source - // file has already been removed? This problem does not occur for any of the others. - delete("tests/ainfer-testchecker/inference-output/MultipleUnions-org.checkerframework.common.value.ValueChecker.ajava") - delete("tests/ainfer-testchecker/annotated/all-systems/TypeVarPrimitives.java") - delete("tests/ainfer-testchecker/annotated/all-systems/Unions.java") - delete("tests/ainfer-testchecker/annotated/all-systems/WildcardBounds.java") + delete('tests/ainfer-testchecker/annotated/all-systems/java8/memberref/Purity.java') // There is some kind of bad interaction between the purity checker's inference mode // and method references to constructors: every one of them in this test causes a @@ -530,7 +503,7 @@ task ainferTestCheckerGenerateAjava(type: Test) { // inference because the relevant purity annotations that seem to trigger it are on // inner classes, which stubs cannot annotate. // TODO: investigate the cause of this error in the Purity checker, fix it, and then reinstate this test. - delete("tests/ainfer-testchecker/annotated/all-systems/java8/memberref/MemberReferences.java") + delete('tests/ainfer-testchecker/annotated/all-systems/java8/memberref/MemberReferences.java') } } @@ -545,8 +518,8 @@ task ainferTestCheckerValidateAjava(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } } @@ -565,7 +538,7 @@ void copyNonannotatedToAnnotatedDirectory(String testdir) { line.contains('// :: error:') // Don't remove unchecked cast warnings, because they're genuinely expected in some all-systems // tests, such as GenericsCasts.java. - || (line.contains('// :: warning:') && !line.contains("// :: warning: [unchecked]")) + || (line.contains('// :: warning:') && !line.contains('// :: warning: [unchecked]')) ? null : line } } @@ -577,7 +550,7 @@ void copyNonannotatedToAnnotatedDirectory(String testdir) { } delete("tests/${testdir}/inference-output") - file("build/whole-program-inference").renameTo(file("tests/${testdir}/inference-output")) + file('build/whole-program-inference').renameTo(file("tests/${testdir}/inference-output")) } // This task is similar to the ainferTestCheckerJaifTest task below, but it doesn't @@ -602,7 +575,7 @@ task ainferTestCheckerGenerateJaifs(type: Test) { dependsOn(compileTestJava) dependsOn(':checker-qual:jar') // For the Value Checker annotations. doFirst { - delete("tests/ainfer-testchecker/annotated") + delete('tests/ainfer-testchecker/annotated') } outputs.upToDateWhen { false } include '**/AinferTestCheckerJaifsTest.class' @@ -611,12 +584,12 @@ task ainferTestCheckerGenerateJaifs(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } doLast { - copyNonannotatedToAnnotatedDirectory("ainfer-testchecker") + copyNonannotatedToAnnotatedDirectory('ainfer-testchecker') // JAIF-based WPI fails these tests, which were added for stub-based WPI. // See issue here: https://github.com/typetools/checker-framework/issues/3009 @@ -633,14 +606,14 @@ task ainferTestCheckerGenerateJaifs(type: Test) { delete('tests/ainfer-testchecker/annotated/OverriddenMethodsTest.java') // Inserting annotations from .jaif files in-place. - String jaifsDir = "tests/ainfer-testchecker/inference-output"; + String jaifsDir = 'tests/ainfer-testchecker/inference-output'; List jaifs = fileTree(jaifsDir).matching { include '*.jaif' }.asList() if (jaifs.isEmpty()) { throw new GradleException("no .jaif files found in ${jaifsDir}") } - String javasDir = "tests/ainfer-testchecker/annotated/"; + String javasDir = 'tests/ainfer-testchecker/annotated/'; List javas = fileTree(javasDir).matching { include '*.java' }.asList() @@ -652,7 +625,7 @@ task ainferTestCheckerGenerateJaifs(type: Test) { // Script argument -cp must precede Java program argument -i. // checker-qual is needed for Constant Value Checker annotations. // Note that "/" works on Windows as well as on Linux. - args = ['-cp', "${sourceSets.test.output.asPath}:${project(':checker-qual').tasks.jar.archivePath}:" + file("tests/build/testclasses")] + args = ['-cp', "${sourceSets.test.output.asPath}:${project(':checker-qual').tasks.jar.archivePath}:" + file('tests/build/testclasses')] args += ['-i'] for (File jaif : jaifs) { args += [jaif.toString()] @@ -675,8 +648,8 @@ task ainferTestCheckerValidateJaifs(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } } @@ -691,7 +664,7 @@ task ainferIndexGenerateAjava(type: Test) { dependsOn(compileTestJava) doFirst { - delete("tests/ainfer-index/annotated") + delete('tests/ainfer-index/annotated') delete("${buildDir}/ainfer-index/") } outputs.upToDateWhen { false } @@ -701,12 +674,12 @@ task ainferIndexGenerateAjava(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } doLast { - copyNonannotatedToAnnotatedDirectory("ainfer-index") + copyNonannotatedToAnnotatedDirectory('ainfer-index') } } @@ -721,8 +694,8 @@ task ainferIndexValidateAjava(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } } @@ -737,7 +710,7 @@ task ainferNullnessGenerateAjava(type: Test) { dependsOn(compileTestJava) doFirst { - delete("tests/ainfer-nullness/annotated") + delete('tests/ainfer-nullness/annotated') delete("${buildDir}/ainfer-nullness/") } outputs.upToDateWhen { false } @@ -747,12 +720,12 @@ task ainferNullnessGenerateAjava(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } doLast { - copyNonannotatedToAnnotatedDirectory("ainfer-nullness") + copyNonannotatedToAnnotatedDirectory('ainfer-nullness') } } @@ -767,8 +740,8 @@ task ainferNullnessValidateAjava(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and the expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } } @@ -783,7 +756,7 @@ task ainferNullnessGenerateJaifs(type: Test) { dependsOn(compileTestJava) doFirst { - delete("tests/ainfer-nullness/annotated") + delete('tests/ainfer-nullness/annotated') } outputs.upToDateWhen { false } include '**/AinferNullnessJaifsTest.class' @@ -792,12 +765,12 @@ task ainferNullnessGenerateJaifs(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } doLast { - copyNonannotatedToAnnotatedDirectory("ainfer-nullness") + copyNonannotatedToAnnotatedDirectory('ainfer-nullness') // JAIF-based WPI fails these tests, which was added for stub-based WPI. // See issue here: https://github.com/typetools/checker-framework/issues/3009 @@ -805,14 +778,14 @@ task ainferNullnessGenerateJaifs(type: Test) { delete('tests/ainfer-nullness/annotated/MultiDimensionalArrays.java') // Inserting annotations from .jaif files in-place. - String jaifsDir = "tests/ainfer-nullness/inference-output"; + String jaifsDir = 'tests/ainfer-nullness/inference-output'; List jaifs = fileTree(jaifsDir).matching { include '*.jaif' }.asList() if (jaifs.isEmpty()) { throw new GradleException("no .jaif files found in ${jaifsDir}") } - String javasDir = "tests/ainfer-nullness/annotated/"; + String javasDir = 'tests/ainfer-nullness/annotated/'; List javas = fileTree(javasDir).matching { include '*.java' }.asList() @@ -823,7 +796,7 @@ task ainferNullnessGenerateJaifs(type: Test) { executable "${afu}/scripts/insert-annotations-to-source" // Script argument -cp must precede Java program argument -i. // Note that "/" works on Windows as well as on Linux. - args = ['-cp', "${sourceSets.test.output.asPath}:${project(':checker-qual').tasks.jar.archivePath}:" + file("tests/build/testclasses")] + args = ['-cp', "${sourceSets.test.output.asPath}:${project(':checker-qual').tasks.jar.archivePath}:" + file('tests/build/testclasses')] args += ['-i'] for (File jaif : jaifs) { args += [jaif.toString()] @@ -846,8 +819,8 @@ task ainferNullnessValidateJaifs(type: Test) { outputs.upToDateWhen { false } // Show the found unexpected diagnostics and expected diagnostics not found. - exceptionFormat "full" - events "passed", "skipped", "failed" + exceptionFormat 'full' + events 'passed', 'skipped', 'failed' } } @@ -861,7 +834,7 @@ task ainferNullnessJaifTest(dependsOn: 'shadowJar', group: 'Verification') { // Empty task that just runs both the jaif and stub WPI tests. // It is run as part of the inferenceTests task. task ainferTest(group: 'Verification') { - description "Run tests for all whole program inference modes." + description 'Run tests for all whole program inference modes.' dependsOn('ainferTestCheckerJaifTest') dependsOn('ainferTestCheckerStubTest') dependsOn('ainferTestCheckerAjavaTest') @@ -871,7 +844,7 @@ task ainferTest(group: 'Verification') { } // This is run as part of the inferenceTests task. -task wpiManyTest(group: "Verification") { +task wpiManyTest(group: 'Verification') { description 'Tests the wpi-many.sh script (and indirectly the wpi.sh script). Requires an Internet connection.' dependsOn(copyJarsToDist) // This test must always be re-run when requested. @@ -900,7 +873,7 @@ task wpiManyTest(group: "Verification") { '--', '--checker', 'nullness,interning,lock,regex,signature,calledmethods,resourceleak' } } catch (Exception e) { - println("Failure: Running wpi-many.sh failed with a non-zero exit code.") + println('Failure: Running wpi-many.sh failed with a non-zero exit code.') File wpiOut = new File("${typecheckFilesDir}/wpi-out") if (wpiOut.exists()) { println("========= Output from last run of wpi.sh (${typecheckFilesDir}/wpi-out): ========") @@ -913,10 +886,10 @@ task wpiManyTest(group: "Verification") { } // collect the logs from running WPI def typecheckFiles = fileTree(typecheckFilesDir).matching { - include "**/*-typecheck.out" + include '**/*-typecheck.out' } def testinLines = file("${project.projectDir}/tests/wpi-many/testin.txt").text.readLines() - testinLines.removeIf { it.startsWith("#") } + testinLines.removeIf { it.startsWith('#') } def expectedTypecheckFileCount = testinLines.size() def actualTypecheckFileCount = typecheckFiles.size() if (actualTypecheckFileCount != expectedTypecheckFileCount) { @@ -936,7 +909,7 @@ task wpiManyTest(group: "Verification") { } println("========= End of output from last run of wpi.sh (${typecheckFilesDir}/wpi-out): ========") def logFiles = fileTree(typecheckFilesDir).matching { - include "**/*.log" + include '**/*.log' } logFiles.visit { FileVisitDetails details -> def filename = "${typecheckFilesDir}" + details.getName() @@ -948,7 +921,7 @@ task wpiManyTest(group: "Verification") { // message that might indicate what went wrong. Even their presenence, // however, is intereseting (even if they are empty). def cannotRunWpiFiles = fileTree(typecheckFilesDir).matching { - include "**/.cannot-run-wpi" + include '**/.cannot-run-wpi' } cannotRunWpiFiles.visit { FileVisitDetails details -> def filename = "${typecheckFilesDir}" + details.getName() @@ -965,29 +938,30 @@ task wpiManyTest(group: "Verification") { def filename = "${project.projectDir}/build/wpi-many-tests-results/" + details.getName() def file = details.getFile() if (file.length() == 0) { - throw new GradleException("Failure: WPI produced empty typecheck file " + filename) + throw new GradleException('Failure: WPI produced empty typecheck file ' + filename) } file.eachLine { line -> if ( // Ignore the line that WPI echoes with the javac command being run. - line.startsWith("Running ") + line.startsWith('Running ') // Warnings about bad path elements aren't related to WPI and are ignored. - || line.startsWith("warning: [path]") + || line.startsWith('warning: [path]') // Ignore bootstrap classpath warning: - || line.startsWith("warning: [options] bootstrap") + || line.startsWith('warning: [options] bootstrap') // Ignore the warnings about --add-opens arguments to the JVM - || line.contains("warning: [options] --add-opens has no effect at compile time") + || line.contains('warning: [options] --add-opens has no effect at compile time') // Ignore the summary line that reports the total number of warnings (which can be single or plural). - || line.endsWith("warning") - || line.endsWith("warnings")) { + || line.endsWith(' warning') + || line.endsWith(' warnings') + || line.startsWith('warning: No processor claimed any of these annotations: ')) { return; } - if (!line.trim().equals("")) { + if (!line.trim().equals('')) { println("======== printing contents of ${filename} ========") details.getFile().eachLine { l -> println(l) } println("======== end of contents of ${filename} ========") - throw new GradleException("Failure: WPI scripts produced an unexpected output in " + filename + ". " + - "Failing line is the following: " + line) + throw new GradleException('Failure: WPI scripts produced an unexpected output in ' + filename + '. ' + + 'Failing line is the following: ' + line) } } } @@ -995,7 +969,7 @@ task wpiManyTest(group: "Verification") { } // This is run as part of the inferenceTests task. -task wpiPlumeLibTest(group: "Verification") { +task wpiPlumeLibTest(group: 'Verification') { description 'Tests whole-program inference on the plume-lib projects. Requires an Internet connection.' dependsOn(copyJarsToDist) @@ -1010,7 +984,7 @@ task wpiPlumeLibTest(group: "Verification") { } } -apply from: rootProject.file("gradle-mvn-push.gradle") +apply from: rootProject.file('gradle-mvn-push.gradle') /** Adds information to the publication for uploading to Maven repositories. */ final checkerPom(publication) { diff --git a/checker/jtreg/nullness/issue3700/Client.out b/checker/jtreg/nullness/issue3700/Client.out index f0d8acb7579..248618f6aa9 100644 --- a/checker/jtreg/nullness/issue3700/Client.out +++ b/checker/jtreg/nullness/issue3700/Client.out @@ -1,2 +1,2 @@ -warning: TimeUnitRange.astub:(line 3,col 1): TimeUnitRange is an enum, but stub file declared it as class TimeUnitRange {... +warning: TimeUnitRange.astub:(line 3,col 1): TimeUnitRange is an enum, but stub file declared it as class TimeUnitRange { public TimeUnitRange of(@Nullable String endUnit); } 1 warning diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java index 3ddf1dd866e..cb24ab0a6cf 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java @@ -51,7 +51,7 @@ public class CalledMethodsAnnotatedTypeFactory extends AccumulationAnnotatedType * The builder frameworks (such as Lombok and AutoValue) supported by this instance of the * Called Methods Checker. */ - private Collection builderFrameworkSupports; + private final Collection builderFrameworkSupports; /** * Whether to use the Value Checker as a subchecker to reduce false positives when analyzing diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/AutoValueSupport.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/AutoValueSupport.java index 38a92528ffc..10db02993e3 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/AutoValueSupport.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/AutoValueSupport.java @@ -41,7 +41,7 @@ public class AutoValueSupport implements BuilderFrameworkSupport { /** The type factory. */ - private CalledMethodsAnnotatedTypeFactory atypeFactory; + private final CalledMethodsAnnotatedTypeFactory atypeFactory; /** * Create a new AutoValueSupport. @@ -278,7 +278,7 @@ private List getAutoValueRequiredProperties( } /** Method names for {@link #isAutoValueRequiredProperty} to ignore. */ - private Set isAutoValueRequiredPropertyIgnored = + private final Set isAutoValueRequiredPropertyIgnored = new HashSet<>(Arrays.asList("equals", "hashCode", "toString", "", "toBuilder")); /** @@ -329,7 +329,7 @@ private boolean isAutoValueRequiredProperty( } /** - * This list of classes that AutoValue considers "optional" comes from AutoValue's source code. + * Classes that AutoValue considers "optional". This list comes from AutoValue's source code. */ private static final String[] optionalClassNames = new String[] { diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/LombokSupport.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/LombokSupport.java index 7d6eac5fe78..204ec3e5c3b 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/LombokSupport.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/LombokSupport.java @@ -31,7 +31,7 @@ public class LombokSupport implements BuilderFrameworkSupport { /** The type factory. */ - private CalledMethodsAnnotatedTypeFactory atypeFactory; + private final CalledMethodsAnnotatedTypeFactory atypeFactory; /** * Create a new LombokSupport. diff --git a/checker/src/main/java/org/checkerframework/checker/fenum/FenumAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/fenum/FenumAnnotatedTypeFactory.java index 0c9d6de726c..8f451a4cb8d 100644 --- a/checker/src/main/java/org/checkerframework/checker/fenum/FenumAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/fenum/FenumAnnotatedTypeFactory.java @@ -30,11 +30,11 @@ public class FenumAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { /** AnnotationMirror for {@link FenumUnqualified}. */ - protected AnnotationMirror FENUM_UNQUALIFIED; + protected final AnnotationMirror FENUM_UNQUALIFIED; /** AnnotationMirror for {@link FenumBottom}. */ - protected AnnotationMirror FENUM_BOTTOM; + protected final AnnotationMirror FENUM_BOTTOM; /** AnnotationMirror for {@link FenumTop}. */ - protected AnnotationMirror FENUM_TOP; + protected final AnnotationMirror FENUM_TOP; /** * Create a FenumAnnotatedTypeFactory. diff --git a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java index def584e28b6..dbdb66f3d0e 100644 --- a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java +++ b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java @@ -455,7 +455,7 @@ public AnnotationMirror exceptionToInvalidFormatAnnotation(IllegalFormatExceptio * @param invalidFormatString an invalid formatter string * @return an {@link InvalidFormat} annotation with the given string as its value */ - // package-private + /* package-private */ AnnotationMirror stringToInvalidFormatAnnotation(String invalidFormatString) { AnnotationBuilder builder = new AnnotationBuilder(processingEnv, InvalidFormat.class); builder.setValue("value", invalidFormatString); diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterAnnotatedTypeFactory.java index 8ce5efd6ce1..6adba24f194 100644 --- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterAnnotatedTypeFactory.java @@ -83,7 +83,8 @@ public I18nFormatterAnnotatedTypeFactory(BaseTypeChecker checker) { } /** - * Builds a map from a translation file key to its value in the file. + * Builds a map from a translation file key to its value in the file. Builds the map for all + * files in the "-Apropfiles" command-line argument. * * @return a map from a translation file key to its value in the file */ diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java index 0be9c38f7cb..1c8efa5644d 100644 --- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java +++ b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java @@ -106,8 +106,8 @@ public AnnotationMirror exceptionToInvalidFormatAnnotation(IllegalArgumentExcept * @param invalidFormatString an invalid formatter string * @return an {@link I18nInvalidFormat} annotation with the given string as its value */ - /*package-private*/ AnnotationMirror stringToInvalidFormatAnnotation( - String invalidFormatString) { + /* package-private */ + AnnotationMirror stringToInvalidFormatAnnotation(String invalidFormatString) { AnnotationBuilder builder = new AnnotationBuilder(processingEnv, I18nInvalidFormat.class); builder.setValue("value", invalidFormatString); return builder.build(); @@ -119,7 +119,7 @@ public AnnotationMirror exceptionToInvalidFormatAnnotation(IllegalArgumentExcept * @param anno an I18nInvalidFormat annotation * @return its value() element/field, or null if it does not have one */ - /*package-private*/ + /* package-private */ @Nullable String getI18nInvalidFormatValue(AnnotationMirror anno) { return AnnotationUtils.getElementValue( anno, i18nInvalidFormatValueElement, String.class, null); @@ -131,7 +131,7 @@ public AnnotationMirror exceptionToInvalidFormatAnnotation(IllegalArgumentExcept * @param anno an I18NFormatFor annotation * @return its value() element/field */ - /*package-private*/ String getI18nFormatForValue(AnnotationMirror anno) { + /* package-private */ String getI18nFormatForValue(AnnotationMirror anno) { return AnnotationUtils.getElementValue(anno, i18nFormatForValueElement, String.class); } diff --git a/checker/src/main/java/org/checkerframework/checker/index/IndexMethodIdentifier.java b/checker/src/main/java/org/checkerframework/checker/index/IndexMethodIdentifier.java index d0c4dd92b7f..d9b4c0fb33a 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/IndexMethodIdentifier.java +++ b/checker/src/main/java/org/checkerframework/checker/index/IndexMethodIdentifier.java @@ -11,6 +11,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.TreeUtils; +import java.util.ArrayList; import java.util.List; import javax.annotation.processing.ProcessingEnvironment; @@ -40,6 +41,12 @@ public class IndexMethodIdentifier { /** The LengthOf.value argument/element. */ private final ExecutableElement lengthOfValueElement; + /** + * The {@code java.lang.String#indexOf} and {@code #lastIndexOf} methods that take a string as a + * non-receiver parameter. + */ + private final List indexOfStringMethods; + /** The type factory. */ private final AnnotatedTypeFactory factory; @@ -55,10 +62,46 @@ public IndexMethodIdentifier(AnnotatedTypeFactory factory) { mathMinMethods = TreeUtils.getMethods("java.lang.Math", "min", 2, processingEnv); mathMaxMethods = TreeUtils.getMethods("java.lang.Math", "max", 2, processingEnv); + indexOfStringMethods = new ArrayList<>(4); + indexOfStringMethods.add( + TreeUtils.getMethod( + "java.lang.String", "indexOf", processingEnv, "java.lang.String")); + indexOfStringMethods.add( + TreeUtils.getMethod( + "java.lang.String", "indexOf", processingEnv, "java.lang.String", "int")); + indexOfStringMethods.add( + TreeUtils.getMethod( + "java.lang.String", "lastIndexOf", processingEnv, "java.lang.String")); + indexOfStringMethods.add( + TreeUtils.getMethod( + "java.lang.String", + "lastIndexOf", + processingEnv, + "java.lang.String", + "int")); + lengthOfValueElement = TreeUtils.getMethod(LengthOf.class, "value", 0, processingEnv); } - /** Returns true iff the argument is an invocation of Math.min. */ + /** + * Returns true iff the argument is an invocation of String#indexOf or String#lastIndexOf that + * takes a string parameter. + * + * @param methodTree the method invocation tree to be tested + * @return true iff the argument is an invocation of one of String's indexOf or lastIndexOf + * methods that takes another string as a parameter. + */ + public boolean isIndexOfString(Tree methodTree) { + ProcessingEnvironment processingEnv = factory.getProcessingEnv(); + return TreeUtils.isMethodInvocation(methodTree, indexOfStringMethods, processingEnv); + } + + /** + * Returns true iff the argument is an invocation of Math.min. + * + * @param methodTree the method invocation tree to be tested + * @return true iff the argument is an invocation of Math.min() + */ public boolean isMathMin(Tree methodTree) { ProcessingEnvironment processingEnv = factory.getProcessingEnv(); return TreeUtils.isMethodInvocation(methodTree, mathMinMethods, processingEnv); diff --git a/checker/src/main/java/org/checkerframework/checker/index/IndexRefinementInfo.java b/checker/src/main/java/org/checkerframework/checker/index/IndexRefinementInfo.java index 9b73d465164..139bf99d599 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/IndexRefinementInfo.java +++ b/checker/src/main/java/org/checkerframework/checker/index/IndexRefinementInfo.java @@ -1,5 +1,6 @@ package org.checkerframework.checker.index; +import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.ConditionalTransferResult; import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.BinaryOperationNode; @@ -22,24 +23,47 @@ */ public class IndexRefinementInfo { - public Node left, right; + /** The left operand. */ + public final Node left; + /** The right operand. */ + public final Node right; /** - * Annotation for left and right expressions. Might be null if dataflow doesn't have a value for - * the expression. + * Annotation for left expressions. Might be null if dataflow doesn't have a value for the + * expression. */ - public AnnotationMirror leftAnno, rightAnno; + public final @Nullable AnnotationMirror leftAnno; + /** + * Annotation for right expressions. Might be null if dataflow doesn't have a value for the + * expression. + */ + public final @Nullable AnnotationMirror rightAnno; - public CFStore thenStore, elseStore; - public ConditionalTransferResult newResult; + /** The then store. */ + public final CFStore thenStore; + /** The else store. */ + public final CFStore elseStore; + /** The new result, after refinement. */ + public final ConditionalTransferResult newResult; + /** + * Creates a new IndexRefinementInfo. + * + * @param left the left operand + * @param right the right operand + * @param result the new result, after refinement + * @param analysis the CFAbstractAnalysis + */ public IndexRefinementInfo( TransferResult result, CFAbstractAnalysis analysis, - Node r, - Node l) { - right = r; - left = l; + Node right, + Node left) { + this.right = right; + this.left = left; + + thenStore = result.getThenStore(); + elseStore = result.getElseStore(); if (analysis.getValue(right) == null || analysis.getValue(left) == null) { leftAnno = null; @@ -50,10 +74,6 @@ public IndexRefinementInfo( QualifierHierarchy hierarchy = analysis.getTypeFactory().getQualifierHierarchy(); rightAnno = getAnno(analysis.getValue(right).getAnnotations(), hierarchy); leftAnno = getAnno(analysis.getValue(left).getAnnotations(), hierarchy); - - thenStore = result.getThenStore(); - elseStore = result.getElseStore(); - newResult = new ConditionalTransferResult<>(result.getResultValue(), thenStore, elseStore); } diff --git a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java index 92511630d68..f409fb289dd 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java @@ -288,7 +288,6 @@ public boolean isLessThanOrEqual(AnnotationMirror left, String right) { if (expressions.contains(right)) { return true; } - // {@code @LessThan("end + 1")} is equivalent to {@code @LessThanOrEqual("end")}. for (String expression : expressions) { if (expression.endsWith(" + 1") && expression.substring(0, expression.length() - 4).equals(right)) { diff --git a/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundChecker.java b/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundChecker.java index 631f5c75278..6c690b902fb 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundChecker.java @@ -36,7 +36,7 @@ public class LowerBoundChecker extends BaseTypeChecker { * These collection classes have some subtypes whose length can change and some subtypes whose * length cannot change. Lower bound checker warnings are skipped at uses of them. */ - private HashSet collectionBaseTypeNames; + private final HashSet collectionBaseTypeNames; /** * A type-checker for preventing fixed-length sequences such as arrays or strings from being diff --git a/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundTransfer.java b/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundTransfer.java index 3946885d593..ae86a05cb43 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundTransfer.java @@ -171,9 +171,14 @@ public class LowerBoundTransfer extends IndexAbstractTransfer { /** The canonical {@link LowerBoundUnknown} annotation. */ public final AnnotationMirror UNKNOWN; - // The ATF (Annotated Type Factory). - private LowerBoundAnnotatedTypeFactory aTypeFactory; + /** The annotated type factory. */ + private final LowerBoundAnnotatedTypeFactory aTypeFactory; + /** + * Create a new LowerBoundTransfer. + * + * @param analysis the CFAnalysis + */ public LowerBoundTransfer(CFAnalysis analysis) { super(analysis); aTypeFactory = (LowerBoundAnnotatedTypeFactory) analysis.getTypeFactory(); diff --git a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenTransfer.java b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenTransfer.java index dca8c33aadf..4d9b1bd5dd9 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenTransfer.java @@ -46,11 +46,17 @@ */ public class SameLenTransfer extends CFTransfer { - private SameLenAnnotatedTypeFactory aTypeFactory; + /** The annotated type factory. */ + private final SameLenAnnotatedTypeFactory aTypeFactory; /** Shorthand for aTypeFactory.UNKNOWN. */ - private AnnotationMirror UNKNOWN; + private final AnnotationMirror UNKNOWN; + /** + * Create a new SameLenTransfer. + * + * @param analysis the CFAnalysis + */ public SameLenTransfer(CFAnalysis analysis) { super(analysis); this.aTypeFactory = (SameLenAnnotatedTypeFactory) analysis.getTypeFactory(); diff --git a/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexTransfer.java b/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexTransfer.java index 0aeab413065..7fc359b115a 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexTransfer.java @@ -24,9 +24,14 @@ */ public class SearchIndexTransfer extends IndexAbstractTransfer { - // The ATF (Annotated Type Factory). - private SearchIndexAnnotatedTypeFactory aTypeFactory; + /** The annotated type factory. */ + private final SearchIndexAnnotatedTypeFactory aTypeFactory; + /** + * Create a new SearchIndexTransfer. + * + * @param analysis the CFAnalysis + */ public SearchIndexTransfer(CFAnalysis analysis) { super(analysis); aTypeFactory = (SearchIndexAnnotatedTypeFactory) analysis.getTypeFactory(); diff --git a/checker/src/main/java/org/checkerframework/checker/index/upperbound/OffsetEquation.java b/checker/src/main/java/org/checkerframework/checker/index/upperbound/OffsetEquation.java index 308ee689b06..ba2c76e2ad9 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/upperbound/OffsetEquation.java +++ b/checker/src/main/java/org/checkerframework/checker/index/upperbound/OffsetEquation.java @@ -27,18 +27,28 @@ *

An OffsetEquation is mutable. */ public class OffsetEquation { + /** The equation for 0 (zero). */ public static final OffsetEquation ZERO = createOffsetForInt(0); + /** The equation for -1. */ public static final OffsetEquation NEG_1 = createOffsetForInt(-1); + /** The equation for 1. */ public static final OffsetEquation ONE = createOffsetForInt(1); + /** Mutable list of terms that have been added to this. */ private final List addedTerms; + /** Mutable list of terms that have been subtracted from this. */ private final List subtractedTerms; - private int intValue = 0; - private String error = null; + /** The integer offset. */ + private int intValue; + /** Non-null if an error has occurred. */ + private @Nullable String error; + /** Create a new OffsetEquation. */ private OffsetEquation() { addedTerms = new ArrayList<>(1); subtractedTerms = new ArrayList<>(1); + this.intValue = 0; + this.error = null; } /** @@ -49,8 +59,8 @@ private OffsetEquation() { protected OffsetEquation(OffsetEquation other) { this.addedTerms = new ArrayList<>(other.addedTerms); this.subtractedTerms = new ArrayList<>(other.subtractedTerms); - this.error = other.error; this.intValue = other.intValue; + this.error = other.error; } public boolean hasError() { diff --git a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java index 6eef8bcc17f..e60cc479dee 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java @@ -47,6 +47,7 @@ import org.checkerframework.common.value.ValueChecker; import org.checkerframework.common.value.ValueCheckerUtils; import org.checkerframework.common.value.qual.BottomVal; +import org.checkerframework.common.value.util.Range; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.framework.flow.CFAbstractStore; @@ -485,7 +486,7 @@ public UpperBoundTreeAnnotator(UpperBoundAnnotatedTypeFactory factory) { *

    *
  • Math.min has unusual semantics that combines annotations for the UBC. *
  • The return type of Random.nextInt depends on the argument, but is not equal to it, - * so a polymorhpic qualifier is insufficient. + * so a polymorphic qualifier is insufficient. *
* * Other methods should not be special-cased here unless there is a compelling reason to do @@ -509,9 +510,84 @@ public Void visitMethodInvocation(MethodInvocationTree tree, AnnotatedTypeMirror qualifier = qualifier.plusOffset(1); type.replaceAnnotation(convertUBQualifierToAnnotation(qualifier)); } + if (imf.isIndexOfString(tree)) { + // String#indexOf(String) and its variants that also take a String technically + // return + // (and are annotated as) @LTEqLengthOf the receiver. However, the result is always + // @LTLengthOf the receiver unless both the receiver and the target string are + // the empty string: "".indexOf("") returns 0, which isn't an index into "". So, + // this + // special case modifies the return type of these methods if either the parameter or + // the receiver is known (by the Value Checker) to not be the empty string. There + // are + // three ways the Value Checker might have that information: either string could + // have a + // @StringVal annotation whose value doesn't include "", either could have an + // @ArrayLen + // annotation + // whose value doesn't contain zero, or either could have an @ArrayLenRange + // annotation whose + // from + // value is any positive integer. + ValueAnnotatedTypeFactory vatf = + ((UpperBoundAnnotatedTypeFactory) this.atypeFactory) + .getValueAnnotatedTypeFactory(); + AnnotatedTypeMirror argType = vatf.getAnnotatedType(tree.getArguments().get(0)); + AnnotatedTypeMirror receiverType = vatf.getReceiverType(tree); + if (definitelyIsNotTheEmptyString(argType, vatf) + || definitelyIsNotTheEmptyString(receiverType, vatf)) { + String receiverName = JavaExpression.getReceiver(tree).toString(); + UBQualifier ltLengthOfReceiver = + UBQualifier.createUBQualifier(receiverName, "0"); + AnnotationMirror currentReturnAnno = type.getAnnotationInHierarchy(UNKNOWN); + UBQualifier currentUBQualifier = + UBQualifier.createUBQualifier( + currentReturnAnno, (IndexChecker) checker); + UBQualifier result = currentUBQualifier.glb(ltLengthOfReceiver); + type.replaceAnnotation(convertUBQualifierToAnnotation(result)); + } + } return super.visitMethodInvocation(tree, type); } + /** + * Returns true if the given Value Checker annotations guarantee that the annotated element + * is not the empty string. + * + * @param atm an annotated type from the Value Checker + * @param vatf the Value Annotated Type Factory + * @return true iff atm contains a {@code StringVal} annotation whose value doesn't contain + * "", an {@code ArrayLen} annotation whose value doesn't contain 0, or an {@code + * ArrayLenRange} annotation whose from value is greater than 0 + */ + private boolean definitelyIsNotTheEmptyString( + AnnotatedTypeMirror atm, ValueAnnotatedTypeFactory vatf) { + Set annos = atm.getAnnotations(); + for (AnnotationMirror anno : annos) { + switch (AnnotationUtils.annotationName(anno)) { + case ValueAnnotatedTypeFactory.STRINGVAL_NAME: + List strings = vatf.getStringValues(anno); + if (strings != null && !strings.contains("")) { + return true; + } + break; + case ValueAnnotatedTypeFactory.ARRAYLEN_NAME: + List lengths = vatf.getArrayLength(anno); + if (lengths != null && !lengths.contains(0)) { + return true; + } + break; + default: + Range range = vatf.getRange(anno); + if (range != null && range.from > 0) { + return true; + } + break; + } + } + return false; + } + @Override public Void visitLiteral(LiteralTree node, AnnotatedTypeMirror type) { // Could also handle long literals, but array indexes are always ints. diff --git a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundChecker.java b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundChecker.java index 35babd683bf..333daf8d288 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundChecker.java @@ -62,7 +62,7 @@ public class UpperBoundChecker extends BaseTypeChecker { * These collection classes have some subtypes whose length can change and some subtypes whose * length cannot change. Warnings are skipped at uses of them. */ - private HashSet collectionBaseTypeNames; + private final HashSet collectionBaseTypeNames; /** Create a new UpperBoundChecker. */ public UpperBoundChecker() { diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index 98ae5c73351..24897c6101f 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -510,7 +510,7 @@ public static SideEffectAnnotation weakest() { * annotation is present on the method * @return the side effect annotation that is present on the given method */ - // package-private + /* package-private */ SideEffectAnnotation methodSideEffectAnnotation( ExecutableElement methodElement, boolean issueErrorIfMoreThanOnePresent) { if (methodElement == null) { @@ -558,7 +558,7 @@ SideEffectAnnotation methodSideEffectAnnotation( * @param atm an AnnotatedTypeMirror containing a GuardSatisfied annotation * @return the index on the GuardSatisfied annotation */ - // package-private + /* package-private */ int getGuardSatisfiedIndex(AnnotatedTypeMirror atm) { return getGuardSatisfiedIndex(atm.getAnnotation(GuardSatisfied.class)); } @@ -570,7 +570,7 @@ int getGuardSatisfiedIndex(AnnotatedTypeMirror atm) { * @param am an AnnotationMirror for a GuardSatisfied annotation * @return the index on the GuardSatisfied annotation */ - // package-private + /* package-private */ int getGuardSatisfiedIndex(AnnotationMirror am) { return AnnotationUtils.getElementValueInt(am, guardSatisfiedValueElement, -1); } diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java index dc9c126981d..4273bf6cc81 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java @@ -75,9 +75,10 @@ */ public class LockVisitor extends BaseTypeVisitor { /** The class of GuardedBy */ - private final Class checkerGuardedByClass = GuardedBy.class; + private static final Class checkerGuardedByClass = GuardedBy.class; /** The class of GuardSatisfied */ - private final Class checkerGuardSatisfiedClass = GuardSatisfied.class; + private static final Class checkerGuardSatisfiedClass = + GuardSatisfied.class; /** A pattern for spotting self receiver */ protected static final Pattern SELF_RECEIVER_PATTERN = Pattern.compile("^(\\.(.*))?$"); diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/IOUtils.astub b/checker/src/main/java/org/checkerframework/checker/mustcall/IOUtils.astub new file mode 100644 index 00000000000..8f35d8febbd --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/IOUtils.astub @@ -0,0 +1,14 @@ +package org.apache.commons.io; + +import org.checkerframework.checker.mustcall.qual.*; + +class IOUtils { + @NotOwning static InputStream toBufferedInputStream(InputStream arg0) throws IOException; + @NotOwning static BufferedReader toBufferedReader(Reader arg0); + @NotOwning static InputStream toInputStream(CharSequence arg0); + @NotOwning static InputStream toInputStream(CharSequence arg0, Charset arg1); + @NotOwning static InputStream toInputStream(CharSequence arg0, String arg1) throws IOException; + @NotOwning static InputStream toInputStream(String arg0); + @NotOwning static InputStream toInputStream(String arg0, Charset arg1); + @NotOwning static InputStream toInputStream(String arg0, String arg1) throws IOException; +} diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallChecker.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallChecker.java index 7fb4871d369..85265b53d55 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallChecker.java @@ -10,6 +10,7 @@ * another. The Resource Leak Checker verifies that the given methods are actually called. */ @StubFiles({ + "IOUtils.astub", "JavaEE.astub", "JdkCompiler.astub", "Reflection.astub", diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java index 1ba84493e0a..67d1437179c 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -49,7 +49,7 @@ public class MustCallTransfer extends CFTransfer { private final TreeBuilder treeBuilder; /** The type factory. */ - private MustCallAnnotatedTypeFactory atypeFactory; + private final MustCallAnnotatedTypeFactory atypeFactory; /** * A cache for the default type for java.lang.String, to avoid needing to look it up for every diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnnotatedTypeFactory.java index 59a8c938e32..60941c6bedd 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnnotatedTypeFactory.java @@ -48,7 +48,7 @@ public class KeyForAnnotatedTypeFactory AnnotationBuilder.fromClass(elements, KeyForBottom.class); /** The canonical name of the KeyFor class. */ - protected final @CanonicalName String KEYFOR_NAME = KeyFor.class.getCanonicalName(); + protected static final @CanonicalName String KEYFOR_NAME = KeyFor.class.getCanonicalName(); /** The Map.containsKey method. */ private final ExecutableElement mapContainsKey = diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java index af8329736d1..64d91bd96cb 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java @@ -393,7 +393,6 @@ public Void visitAssert(AssertTree node, Void p) { // enabled. boolean doVisitAssert; - if (checker.hasOption("assumeAssertionsAreEnabled") || CFCFGBuilder.assumeAssertionsActivatedForAssertTree(checker, node)) { doVisitAssert = true; @@ -556,7 +555,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) { * @param tree a method invocation whose first formal parameter is of String type * @return the first argument if it is a literal, otherwise null */ - /*package-private*/ static @Nullable String literalFirstArgument(MethodInvocationTree tree) { + /* package-private */ static @Nullable String literalFirstArgument(MethodInvocationTree tree) { List args = tree.getArguments(); assert args.size() > 0; ExpressionTree arg = args.get(0); diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/collection-object-parameters-may-be-null.readme b/checker/src/main/java/org/checkerframework/checker/nullness/collection-object-parameters-may-be-null.readme index 6a5413fcaa9..4f481283286 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/collection-object-parameters-may-be-null.readme +++ b/checker/src/main/java/org/checkerframework/checker/nullness/collection-object-parameters-may-be-null.readme @@ -1,6 +1,6 @@ -# Run the following in both copies of the annotated JDK. For example, in: -cd $t/libraries/jdk-fork-mernst-branch-collection-object-parameters-may-be-null/src/java.base/share/classes -cd $t/checker-framework-fork-mernst-branch-collection-object-parameters-may-be-null/checker/jdk/nullness/src +# This file contains notes about creating file collection-object-parameters-may-be-null.astub . + +# Run the following in src/java.base/share/classes/ in the annotated JDK. rm -f *.txt diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub b/checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub new file mode 100644 index 00000000000..46f0d3c81c8 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub @@ -0,0 +1,40 @@ +// This stub file makes the Nullness Checker not warn about null pointer +// exceptions thrown by nullness assertion methods. There is no longer any +// guarantee that your program will not throw a NullPointerException. + +import org.checkerframework.checker.nullness.qual.EnsuresNonNull; +import org.checkerframework.checker.nullness.qual.Nullable; +import java.util.function.Supplier; + + +package java.util; + +public class Objects { + @EnsuresNonNull("#1") + public static T requireNonNull(@Nullable T obj); + @EnsuresNonNull("#1") + public static T requireNonNull(@Nullable T obj, String message); +} + + +// No annotations for com.google.common.base.Preconditions or +// com.google.common.base.Verify are needed because they are annotated with +// @CheckForNull and the Checker Framework treats @CheckForNull as @Nullable. + + +package org.junit; + +public class Assertions { + public static void assertNotNull(@Nullable Object actual); + public static void assertNotNull(@Nullable Object actual, String message); + public static void assertNotNull(@Nullable Object actual, Supplier messageSupplier); +} + + +package org.junit.jupiter.api; + +public class Assertions { + public static void assertNotNull(@Nullable Object actual); + public static void assertNotNull(@Nullable Object actual, String message); + public static void assertNotNull(@Nullable Object actual, Supplier messageSupplier); +} diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/sometimes-nullable.astub b/checker/src/main/java/org/checkerframework/checker/nullness/sometimes-nullable.astub new file mode 100644 index 00000000000..e9a2ac6ff33 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/nullness/sometimes-nullable.astub @@ -0,0 +1,13 @@ +// This file uses `@Nullable` for methods in the JDK that sometimes, but not always, permit null as +// an argument. For more discussion, see section "Conservative nullness annotations on the JDK" in +// the Checker Framework manual (https://checkerframework.org/manual/#nullness-jdk-conservative). + +// This file is very incomplete and should be expanded. + +package java.lang.ref; + +import org.checkerframework.checker.nullness.qual.Nullable; + +public class WeakReference extends Reference { + public WeakReference(@Nullable T referent, @Nullable ReferenceQueue q); +} diff --git a/checker/src/main/java/org/checkerframework/checker/regex/RegexVisitor.java b/checker/src/main/java/org/checkerframework/checker/regex/RegexVisitor.java index ea51b6f1423..8cd9274c319 100644 --- a/checker/src/main/java/org/checkerframework/checker/regex/RegexVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/regex/RegexVisitor.java @@ -15,7 +15,6 @@ import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.VariableElement; -import javax.lang.model.type.TypeMirror; /** * A type-checking visitor for the Regex type system. @@ -34,15 +33,17 @@ */ public class RegexVisitor extends BaseTypeVisitor { + /** The method java.util.regex.MatchResult.end. */ private final ExecutableElement matchResultEnd; + /** The method java.util.regex.MatchResult.group. */ private final ExecutableElement matchResultGroup; + /** The method java.util.regex.MatchResult.start. */ private final ExecutableElement matchResultStart; + /** The method java.util.regex.Pattern.compile. */ private final ExecutableElement patternCompile; + /** The field java.util.regex.Pattern.LITERAL. */ private final VariableElement patternLiteral; - /** Reference types that may be annotated with @Regex. */ - protected TypeMirror[] legalReferenceTypes; - /** * Create a RegexVisitor. * diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/IOUtils.astub b/checker/src/main/java/org/checkerframework/checker/resourceleak/IOUtils.astub new file mode 100644 index 00000000000..9caed0051ee --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/IOUtils.astub @@ -0,0 +1,25 @@ +package org.apache.commons.io; + +import org.checkerframework.checker.calledmethods.qual.*; + +class IOUtils { + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(Reader arg0); + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(Writer arg0); + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(InputStream arg0); + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(OutputStream arg0); + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(Closeable arg0); + @SuppressWarnings("ensuresvarargs.unverified") + @EnsuresCalledMethodsVarArgs("close") + static void closeQuietly(Closeable... arg0); + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(Socket arg0); + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(Selector arg0); + @EnsuresCalledMethods(value = "#1", methods = "close") + static void closeQuietly(ServerSocket arg0); +} diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java index 628ef2ecc3a..75ea0849202 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -59,7 +59,6 @@ import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypeSystemError; import org.checkerframework.javacutil.TypesUtils; -import org.plumelib.util.StringsPlume; import java.io.UnsupportedEncodingException; import java.util.ArrayDeque; @@ -74,6 +73,7 @@ import java.util.Map; import java.util.Objects; import java.util.Set; +import java.util.StringJoiner; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; @@ -629,12 +629,16 @@ private void checkCreatesMustCallForInvocation( } } - String missingStrs = StringsPlume.join(", ", missing); + StringJoiner missingStrs = new StringJoiner(","); + for (JavaExpression m : missing) { + String s = m.toString(); + missingStrs.add(s.equals("this") ? s + " of type " + m.getType() : s); + } checker.reportError( node.getTree(), "reset.not.owning", node.getTarget().getMethod().getSimpleName().toString(), - missingStrs); + missingStrs.toString()); } /** @@ -642,32 +646,36 @@ private void checkCreatesMustCallForInvocation( * org.checkerframework.checker.mustcall.qual.CreatesMustCallFor} annotation. Helper method for * {@link #checkCreatesMustCallForInvocation(Set, MethodInvocationNode)}. * - *

An expression is valid if one of the following conditions is true: 1) the expression is an - * owning pointer, 2) the expression already has a tracked Obligation (i.e. there is already a - * resource alias in some Obligation's resource alias set that refers to the expression), or 3) - * the method in which the invocation occurs also has an @CreatesMustCallFor annotation, with - * the same expression. + *

An expression is valid if one of the following conditions is true: + * + *

    + *
  • 1) the expression is an owning pointer, + *
  • 2) the expression already has a tracked Obligation (i.e. there is already a resource + * alias in some Obligation's resource alias set that refers to the expression), or + *
  • 3) the method in which the invocation occurs also has an @CreatesMustCallFor + * annotation, with the same expression. + *
* * @param obligations the currently-tracked Obligations; this value is side-effected if there is * an Obligation in it which tracks {@code expression} as one of its resource aliases * @param expression an element of a method's @CreatesMustCallFor annotation - * @param path the path to the invocation of the method from whose @CreateMustCallFor annotation - * {@code expression} came + * @param invocationPath the path to the invocation of the method from whose @CreateMustCallFor + * annotation {@code expression} came * @return true iff the expression is valid, as defined above */ private boolean isValidCreatesMustCallForExpression( - Set obligations, JavaExpression expression, TreePath path) { + Set obligations, JavaExpression expression, TreePath invocationPath) { if (expression instanceof FieldAccess) { Element elt = ((FieldAccess) expression).getField(); if (!checker.hasOption(MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP) - && typeFactory.getDeclAnnotation(elt, Owning.class) != null) { + && typeFactory.hasOwning(elt)) { // The expression is an Owning field. This satisfies case 1. return true; } } else if (expression instanceof LocalVariable) { Element elt = ((LocalVariable) expression).getElement(); if (!checker.hasOption(MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP) - && typeFactory.getDeclAnnotation(elt, Owning.class) != null) { + && typeFactory.hasOwning(elt)) { // The expression is an Owning formal parameter. Note that this cannot actually // be a local variable (despite expressions's type being LocalVariable) because // the @Owning annotation can only be written on methods, parameters, and fields; @@ -702,34 +710,33 @@ private boolean isValidCreatesMustCallForExpression( // TODO: Getting this every time is inefficient if a method has many @CreatesMustCallFor // annotations, but that should be rare. - MethodTree enclosingMethodTree = TreePathUtil.enclosingMethod(path); - if (enclosingMethodTree == null) { + MethodTree callerMethodTree = TreePathUtil.enclosingMethod(invocationPath); + if (callerMethodTree == null) { return false; } - ExecutableElement enclosingMethodElt = - TreeUtils.elementFromDeclaration(enclosingMethodTree); + ExecutableElement callerMethodElt = TreeUtils.elementFromDeclaration(callerMethodTree); MustCallAnnotatedTypeFactory mcAtf = typeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class); - List enclosingCmcfValues = + List callerCmcfValues = ResourceLeakVisitor.getCreatesMustCallForValues( - enclosingMethodElt, mcAtf, typeFactory); - if (enclosingCmcfValues.isEmpty()) { + callerMethodElt, mcAtf, typeFactory); + if (callerCmcfValues.isEmpty()) { return false; } - for (String enclosingCmcfValue : enclosingCmcfValues) { - JavaExpression enclosingTarget; + for (String callerCmcfValue : callerCmcfValues) { + JavaExpression callerTarget; try { - enclosingTarget = + callerTarget = StringToJavaExpression.atMethodBody( - enclosingCmcfValue, enclosingMethodTree, checker); + callerCmcfValue, callerMethodTree, checker); } catch (JavaExpressionParseException e) { // Do not issue an error here, because it would be a duplicate. // The error will be issued by the Transfer class of the checker, // via the CreatesMustCallForElementSupplier interface. - enclosingTarget = null; + callerTarget = null; } - if (areSame(expression, enclosingTarget)) { + if (areSame(expression, callerTarget)) { // This satisfies case 3. return true; } @@ -989,20 +996,14 @@ private void removeObligationsAtOwnershipTransferToParameters( // check if parameter has an @Owning annotation VariableElement parameter = parameters.get(i); - Set annotationMirrors = - typeFactory.getDeclAnnotations(parameter); - for (AnnotationMirror anno : annotationMirrors) { - if (AnnotationUtils.areSameByName( - anno, "org.checkerframework.checker.mustcall.qual.Owning")) { - Obligation localObligation = getObligationForVar(obligations, local); - // Passing to an owning parameter is not sufficient to resolve the - // obligation created from a MustCallAlias parameter, because the - // containing method must actually return the value. - if (!localObligation.derivedFromMustCallAlias()) { - // Transfer ownership! - obligations.remove(localObligation); - break; - } + if (typeFactory.hasOwning(parameter)) { + Obligation localObligation = getObligationForVar(obligations, local); + // Passing to an owning parameter is not sufficient to resolve the + // obligation created from a MustCallAlias parameter, because the containing + // method must actually return the value. + if (!localObligation.derivedFromMustCallAlias()) { + // Transfer ownership! + obligations.remove(localObligation); } } } @@ -1066,7 +1067,7 @@ private boolean isTransferOwnershipAtReturn(ControlFlowGraph cfg) { // not be transferred. MethodTree method = ((UnderlyingAST.CFGMethod) underlyingAST).getMethod(); ExecutableElement executableElement = TreeUtils.elementFromDeclaration(method); - return typeFactory.getDeclAnnotation(executableElement, NotOwning.class) == null; + return !typeFactory.hasNotOwning(executableElement); } return false; } @@ -1095,7 +1096,7 @@ private void updateObligationsForAssignment( if (lhsElement.getKind() == ElementKind.FIELD) { boolean isOwningField = !checker.hasOption(MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP) - && typeFactory.getDeclAnnotation(lhsElement, Owning.class) != null; + && typeFactory.hasOwning(lhsElement); // Check that the must-call obligations of the lhs have been satisfied, if the field is // non-final and owning. if (isOwningField @@ -1109,9 +1110,18 @@ private void updateObligationsForAssignment( && rhs instanceof LocalVariableNode && (typeFactory.canCreateObligations() || ElementUtils.isFinal(lhsElement))) { // Assigning to an owning field is sufficient to clear a must-call alias obligation - // in a constructor. + // in + // a constructor, if the enclosing class has at most one @Owning field. If the class + // had multiple owning fields, then a soundness bug would occur: the must call alias + // relationship would allow the whole class' obligation to be fulfilled by closing + // only one of the parameters passed to the constructor (but the other owning fields + // might not actually have had their obligations fulfilled). See test case + // checker/tests/resourceleak/TwoOwningMCATest.java for an example. Element enclosingCtr = lhsElement.getEnclosingElement(); - if (enclosingCtr != null && enclosingCtr.getKind() != ElementKind.CONSTRUCTOR) { + if (enclosingCtr != null + && enclosingCtr.getKind() != ElementKind.CONSTRUCTOR + && hasAtMostOneOwningField( + ElementUtils.enclosingTypeElement(enclosingCtr))) { removeObligationsContainingVar(obligations, (LocalVariableNode) rhs); } else { removeObligationsContainingVarIfNotDerivedFromMustCallAlias( @@ -1131,6 +1141,30 @@ private void updateObligationsForAssignment( } } + /** + * Returns true iff the given type element has 0 or 1 @Owning fields. + * + * @param element an element for a class + * @return true iff element has no more than 1 owning field + */ + private boolean hasAtMostOneOwningField(TypeElement element) { + List fields = + ElementUtils.getAllFieldsIn(element, typeFactory.getElementUtils()); + // Has an owning field already been encountered? + boolean hasOwningField = false; + for (VariableElement field : fields) { + if (typeFactory.hasOwning(field)) { + if (hasOwningField) { + return false; + } else { + hasOwningField = true; + } + } + } + // We haven't seen two owning fields, so there must be 1 or 0. + return true; + } + /** * Returns true if must-call type of node only contains close. This is a helper method for * handling try-with-resources statements. @@ -1652,7 +1686,7 @@ private boolean shouldTrackReturnType(MethodInvocationNode node) { return false; } // check for absence of @NotOwning annotation - return (typeFactory.getDeclAnnotation(executableElement, NotOwning.class) == null); + return !typeFactory.hasNotOwning(executableElement); } /** diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java index f97f9a5a385..2498a0967be 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -16,6 +16,8 @@ import org.checkerframework.checker.mustcall.qual.CreatesMustCallFor; import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.checker.mustcall.qual.MustCallAlias; +import org.checkerframework.checker.mustcall.qual.NotOwning; +import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.cfg.ControlFlowGraph; @@ -361,4 +363,34 @@ public ExecutableElement getCreatesMustCallForValueElement() { public ExecutableElement getCreatesMustCallForListValueElement() { return createsMustCallForListValueElement; } + + /** + * Does the given element have an {@code @NotOwning} annotation (including in stub files)? + * + *

Prefer this method to calling {@link #getDeclAnnotation(Element, Class)} on the type + * factory directly, which won't find this annotation in stub files (it only considers stub + * files loaded by this checker, not subcheckers). + * + * @param elt an element + * @return whether there is a NotOwning annotation on the given element + */ + public boolean hasNotOwning(Element elt) { + MustCallAnnotatedTypeFactory mcatf = getTypeFactoryOfSubchecker(MustCallChecker.class); + return mcatf.getDeclAnnotation(elt, NotOwning.class) != null; + } + + /** + * Does the given element have an {@code @Owning} annotation (including in stub files)? + * + *

Prefer this method to calling {@link #getDeclAnnotation(Element, Class)} on the type + * factory directly, which won't find this annotation in stub files (it only considers stub + * files loaded by this checker, not subcheckers). + * + * @param elt an element + * @return whether there is an Owning annotation on the given element + */ + public boolean hasOwning(Element elt) { + MustCallAnnotatedTypeFactory mcatf = getTypeFactoryOfSubchecker(MustCallChecker.class); + return mcatf.getDeclAnnotation(elt, Owning.class) != null; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java index bfb4e979b78..cb50d55fbbf 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java @@ -6,6 +6,7 @@ import org.checkerframework.checker.mustcall.MustCallNoCreatesMustCallForChecker; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.framework.qual.StubFiles; import org.checkerframework.framework.source.SupportedOptions; import java.util.LinkedHashSet; @@ -25,8 +26,12 @@ MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP, MustCallChecker.NO_RESOURCE_ALIASES }) +@StubFiles("IOUtils.astub") public class ResourceLeakChecker extends CalledMethodsChecker { + /** Creates a ResourceLeakChecker. */ + public ResourceLeakChecker() {} + /** * Command-line option for counting how many must-call obligations were checked by the Resource * Leak Checker, and emitting the number after processing all files. Used for generating tables diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java index 70df7eb5c80..e656514c44e 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -247,7 +247,7 @@ private static String getCreatesMustCallForValue( * iff there are no @CreatesMustCallFor annotations on elt. The returned list is always * modifiable if it is non-empty. */ - /*package-private*/ static List getCreatesMustCallForValues( + /* package-private */ static List getCreatesMustCallForValues( ExecutableElement elt, MustCallAnnotatedTypeFactory mcAtf, ResourceLeakAnnotatedTypeFactory atypeFactory) { diff --git a/checker/src/main/java/org/checkerframework/checker/signature/SignatureTransfer.java b/checker/src/main/java/org/checkerframework/checker/signature/SignatureTransfer.java index 588e5ef72f3..c270bd85fd6 100644 --- a/checker/src/main/java/org/checkerframework/checker/signature/SignatureTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/signature/SignatureTransfer.java @@ -22,7 +22,7 @@ public class SignatureTransfer extends CFTransfer { /** The annotated type factory for this transfer function. */ - private SignatureAnnotatedTypeFactory aTypeFactory; + private final SignatureAnnotatedTypeFactory aTypeFactory; /** * Create a new SignatureTransfer. diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java index 6dc1fd425ed..d94833f9100 100644 --- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java @@ -612,7 +612,8 @@ private boolean castIgnoresMSB( * @return true iff the right shift is masked such that a signed or unsigned right shift has the * same effect */ - /*package-private*/ boolean isMaskedShiftEitherSignedness(BinaryTree shiftExpr, TreePath path) { + /* package-private */ boolean isMaskedShiftEitherSignedness( + BinaryTree shiftExpr, TreePath path) { Pair enclosingPair = TreePathUtil.enclosingNonParen(path); // enclosing immediately contains shiftExpr or a parenthesized version of shiftExpr Tree enclosing = enclosingPair.first; @@ -660,7 +661,8 @@ private boolean castIgnoresMSB( * @return true iff the right shift is type casted such that a signed or unsigned right shift * has the same effect */ - /*package-private*/ boolean isCastedShiftEitherSignedness(BinaryTree shiftExpr, TreePath path) { + /* package-private */ boolean isCastedShiftEitherSignedness( + BinaryTree shiftExpr, TreePath path) { // enclosing immediately contains shiftExpr or a parenthesized version of shiftExpr Tree enclosing = TreePathUtil.enclosingNonParen(path).first; diff --git a/checker/src/main/java/org/checkerframework/checker/units/UnitsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/units/UnitsAnnotatedTypeFactory.java index b8bbf6fc548..2593d337e8c 100644 --- a/checker/src/main/java/org/checkerframework/checker/units/UnitsAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/units/UnitsAnnotatedTypeFactory.java @@ -6,6 +6,7 @@ import com.sun.source.tree.Tree; import org.checkerframework.checker.initialization.qual.UnderInitialization; +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; import org.checkerframework.checker.nullness.qual.NonNull; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.nullness.qual.RequiresNonNull; @@ -95,7 +96,7 @@ public class UnitsAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { * Map from canonical class name to the corresponding UnitsRelations instance. We use the string * to prevent instantiating the UnitsRelations multiple times. */ - private Map<@CanonicalName String, UnitsRelations> unitsRel; + private @MonotonicNonNull Map<@CanonicalName String, UnitsRelations> unitsRel; /** Map from canonical name of external qualifiers, to their Class. */ private static final Map<@CanonicalName String, Class> externalQualsMap = diff --git a/checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/AinferTestAnnotatedTypeFactory.java b/checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/AinferTestAnnotatedTypeFactory.java index 681fc4ccbc9..478e8a51012 100644 --- a/checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/AinferTestAnnotatedTypeFactory.java +++ b/checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/AinferTestAnnotatedTypeFactory.java @@ -1,5 +1,8 @@ package org.checkerframework.checker.testchecker.ainfer; +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.MethodTree; + import org.checkerframework.checker.testchecker.ainfer.qual.AinferBottom; import org.checkerframework.checker.testchecker.ainfer.qual.AinferDefaultType; import org.checkerframework.checker.testchecker.ainfer.qual.AinferImplicitAnno; @@ -8,9 +11,12 @@ import org.checkerframework.checker.testchecker.ainfer.qual.AinferSibling2; import org.checkerframework.checker.testchecker.ainfer.qual.AinferSiblingWithFields; import org.checkerframework.checker.testchecker.ainfer.qual.AinferTop; +import org.checkerframework.checker.testchecker.ainfer.qual.AinferTreatAsSibling1; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.LiteralKind; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.MostlyNoElementQualifierHierarchy; import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; @@ -49,6 +55,12 @@ public class AinferTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { private final AnnotationMirror IMPLICIT_ANNO = new AnnotationBuilder(processingEnv, AinferImplicitAnno.class).build(); + private final AnnotationMirror SIBLING1 = + new AnnotationBuilder(processingEnv, AinferSibling1.class).build(); + + private final AnnotationMirror TREAT_AS_SIBLING1 = + new AnnotationBuilder(processingEnv, AinferTreatAsSibling1.class).build(); + /** The AinferSiblingWithFields.value field/element. */ private final ExecutableElement siblingWithFieldsValueElement = TreeUtils.getMethod(AinferSiblingWithFields.class, "value", 0, processingEnv); @@ -58,6 +70,10 @@ public class AinferTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { public AinferTestAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker); + // Support a declaration annotation that can be written on parameters, to test that the + // WPI feature allowing inference of declaration annotations on parameters works as + // intended. + addAliasedTypeAnnotation(AinferTreatAsSibling1.class, SIBLING1); postInit(); } @@ -81,7 +97,51 @@ public TreeAnnotator createTreeAnnotator() { literalTreeAnnotator.addLiteralKind(LiteralKind.INT, BOTTOM); literalTreeAnnotator.addStandardLiteralQualifiers(); - return new ListTreeAnnotator(new PropagationTreeAnnotator(this), literalTreeAnnotator); + return new ListTreeAnnotator( + new PropagationTreeAnnotator(this), + literalTreeAnnotator, + new AinferTestTreeAnnotator(this)); + } + + protected class AinferTestTreeAnnotator extends TreeAnnotator { + + /** + * Create a new AinferTestTreeAnnotator. + * + * @param atypeFactory the type factory + */ + protected AinferTestTreeAnnotator(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + } + + @Override + public Void visitClass(ClassTree classTree, AnnotatedTypeMirror type) { + /* NO-AFU + WholeProgramInference wpi = atypeFactory.getWholeProgramInference(); + TypeElement classElt = TreeUtils.elementFromDeclaration(classTree); + if (wpi != null && classElt.getSimpleName().contentEquals("IShouldBeSibling1")) { + wpi.addClassDeclarationAnnotation(classElt, SIBLING1); + } + */ + return super.visitClass(classTree, type); + } + + @Override + public Void visitMethod(MethodTree methodTree, AnnotatedTypeMirror type) { + /* NO-AFU + WholeProgramInference wpi = atypeFactory.getWholeProgramInference(); + if (wpi != null) { + ExecutableElement execElt = TreeUtils.elementFromDeclaration(methodTree); + for (int i = 0; i < execElt.getParameters().size(); ++i) { + VariableElement param = execElt.getParameters().get(i); + if (param.getSimpleName().contentEquals("iShouldBeTreatedAsSibling1")) { + wpi.addDeclarationAnnotationToFormalParameter(execElt, i, TREAT_AS_SIBLING1); + } + } + } + */ + return super.visitMethod(methodTree, type); + } } @Override @@ -92,7 +152,7 @@ protected QualifierHierarchy createQualifierHierarchy() { /** * Using a MultiGraphQualifierHierarchy to enable tests with Annotations that contain fields. * - * @see AinferSiblingWithFields. + * @see AinferSiblingWithFields */ protected class AinferTestQualifierHierarchy extends MostlyNoElementQualifierHierarchy { diff --git a/checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/qual/AinferTreatAsSibling1.java b/checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/qual/AinferTreatAsSibling1.java new file mode 100644 index 00000000000..ba569a924d5 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/testchecker/ainfer/qual/AinferTreatAsSibling1.java @@ -0,0 +1,15 @@ +package org.checkerframework.checker.testchecker.ainfer.qual; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * A declaration annotation used to test that the API for inferring declaration annotations on + * parameters works properly. The presence of this annotation indicates that the checker should + * treat the annotated element as if it were annotated as {@link AinferSibling1}. + */ +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.PARAMETER}) +public @interface AinferTreatAsSibling1 {} diff --git a/checker/tests/ainfer-testchecker/non-annotated/IShouldBeSibling1.java b/checker/tests/ainfer-testchecker/non-annotated/IShouldBeSibling1.java new file mode 100644 index 00000000000..a44b4ca243f --- /dev/null +++ b/checker/tests/ainfer-testchecker/non-annotated/IShouldBeSibling1.java @@ -0,0 +1,14 @@ +// Tests the feature that allows checkers to add annotations onto a class +// declaration, which is used for custom inference logic. There is custom +// logic in the AinferTestChecker specifically for classes with the name +// "IShouldBeSibling1" that infers an @Sibling1 annotation for them. + +import org.checkerframework.checker.testchecker.ainfer.qual.AinferSibling1; + +@SuppressWarnings("super.invocation") // Intentional. +public class IShouldBeSibling1 { + public static void test(IShouldBeSibling1 s1) { + // :: warning: assignment + @AinferSibling1 IShouldBeSibling1 s = s1; + } +} diff --git a/checker/tests/ainfer-testchecker/non-annotated/OptionGroup.java b/checker/tests/ainfer-testchecker/non-annotated/OptionGroup.java new file mode 100644 index 00000000000..14d4870e2e5 --- /dev/null +++ b/checker/tests/ainfer-testchecker/non-annotated/OptionGroup.java @@ -0,0 +1,18 @@ +// This annotation from plume-lib options caused an error in +// a version of ajava-based WPI. The problem was that annotation +// declarations weren't considered possible declarations when checking +// whether a location can store a declaration annotation. + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +@Retention(RetentionPolicy.RUNTIME) +@Target(ElementType.FIELD) +public @interface OptionGroup { + + String value(); + + boolean unpublicized() default false; +} diff --git a/checker/tests/ainfer-testchecker/non-annotated/Purity.java b/checker/tests/ainfer-testchecker/non-annotated/Purity.java index f3b723f0fb3..4d6b6851f8a 100644 --- a/checker/tests/ainfer-testchecker/non-annotated/Purity.java +++ b/checker/tests/ainfer-testchecker/non-annotated/Purity.java @@ -1,5 +1,5 @@ // Copied from the all-systems tests, because of the expected error -// on line 23. During the first round of WPI, errors are warnings: so the test fails. +// on line 26. During the first round of WPI, errors are warnings: so the test fails. // The class has been renamed so that an -AskipDefs=TestPure command-line argument // can suppress the original errors. diff --git a/checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1InferenceTest.java b/checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1InferenceTest.java new file mode 100644 index 00000000000..5da4f414535 --- /dev/null +++ b/checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1InferenceTest.java @@ -0,0 +1,13 @@ +// A simple test that the @AinferTreatAsSibling1 can be inferred. +// This test does actually test inference: the AinferTestChecker's TreeAnnotator +// has logic to add the @AinferTreatAsSibling1 annotation to parameters with +// the name "iShouldBeTreatedAsSibling1". + +import org.checkerframework.checker.testchecker.ainfer.qual.AinferSibling1; + +public class TreatAsSibling1InferenceTest { + public void test(Object iShouldBeTreatedAsSibling1) { + // :: warning: assignment + @AinferSibling1 Object x = iShouldBeTreatedAsSibling1; + } +} diff --git a/checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1Test.java b/checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1Test.java new file mode 100644 index 00000000000..eef11cac87e --- /dev/null +++ b/checker/tests/ainfer-testchecker/non-annotated/TreatAsSibling1Test.java @@ -0,0 +1,11 @@ +// A simple test that the @AinferTreatAsSibling1 annotation works as intended. +// This test doesn't actually test inference: it's a test for the AinferTestChecker. + +import org.checkerframework.checker.testchecker.ainfer.qual.AinferSibling1; +import org.checkerframework.checker.testchecker.ainfer.qual.AinferTreatAsSibling1; + +public class TreatAsSibling1Test { + public void test(@AinferTreatAsSibling1 Object y) { + @AinferSibling1 Object x = y; + } +} diff --git a/checker/tests/index/Issue5471.java b/checker/tests/index/Issue5471.java new file mode 100644 index 00000000000..9f28c2c9150 --- /dev/null +++ b/checker/tests/index/Issue5471.java @@ -0,0 +1,22 @@ +// Test case for https://github.com/typetools/checker-framework/issues/5471. + +import org.checkerframework.checker.index.qual.IndexFor; + +public class Issue5471 { + private static boolean atTheBeginning(@IndexFor("#2") int index, String line) { + return (index == 0); + } + + private static boolean hasDoubleQuestionMarkAtTheBeginning(String line) { + int i = line.indexOf("??"); + if (i != -1) { + return (atTheBeginning(i, line)); + } + return false; + } + + public static void main(String[] args) { + String x = "Hello?World, this is our new program"; + if (hasDoubleQuestionMarkAtTheBeginning(x)) System.out.println("TRUE"); + } +} diff --git a/checker/tests/nullness/java17/SwitchTestIssue5412.java b/checker/tests/nullness/java17/SwitchTestIssue5412.java new file mode 100644 index 00000000000..65f6ab40af5 --- /dev/null +++ b/checker/tests/nullness/java17/SwitchTestIssue5412.java @@ -0,0 +1,128 @@ +// Test case for https://github.com/typetools/checker-framework/issues/5412 + +// @below-java17-jdk-skip-test + +import org.checkerframework.checker.nullness.qual.NonNull; + +enum MyEnum { + VAL1, + VAL2, + VAL3 +} + +class SwitchTestExhaustive { + public String foo1(MyEnum b) { + final var s = + switch (b) { + case VAL1 -> "1"; + case VAL2 -> "2"; + case VAL3 -> "3"; + }; + return s; + } + + public String foo1a(MyEnum b) { + final var s = + switch (b) { + case VAL1 -> "1"; + case VAL2 -> "2"; + case VAL3 -> "3"; + // The default case is dead code, so it would be possible for type-checking to skip it + // and not issue this warning. But giving the warning is also good. + // :: error: (switch.expression) + default -> null; + }; + return s; + } + + public String foo2(MyEnum b) { + final var s = + switch (b) { + case VAL1 -> "1"; + case VAL2 -> "2"; + case VAL3 -> "3"; + default -> throw new RuntimeException(); + }; + return s; + } + + public String foo3(MyEnum b) { + return switch (b) { + case VAL1 -> "1"; + case VAL2 -> "2"; + case VAL3 -> "3"; + }; + } + + public String foo4(MyEnum b) { + String aString = "foo"; + switch (b) { + case VAL1: + return "a"; + case VAL2: + return "b"; + case VAL3: + return "c"; + default: + System.out.println(aString.hashCode()); + throw new Error(); + } + } + + public String foo4a(MyEnum b) { + String aString = null; + switch (b) { + case VAL1: + aString = "a"; + break; + case VAL2: + aString = "b"; + break; + case VAL3: + aString = "c"; + break; + // The `default:` case is dead code, so it is acceptable for this method to compile + // without nullness errors. + default: + break; + } + // :: error: (return) + return aString; + } + + public String foo4b(MyEnum b) { + String aString; + switch (b) { + case VAL1: + aString = "a"; + break; + case VAL2: + aString = "b"; + break; + case VAL3: + aString = "c"; + break; + // The `default:` case is dead code, so it is acceptable for this method to compile + // without nullness errors. + default: + aString = null; + break; + } + // :: error: (return) + return aString; + } + + // TODO: test fallthrough to the default: case. + public @NonNull String foo5(MyEnum b) { + String aString = "foo"; + switch (b) { + case VAL1: + return aString; + case VAL2: + return aString; + case VAL3: + default: + return aString; + } + } +} diff --git a/checker/tests/resourceleak/COAnonymousClass.java b/checker/tests/resourceleak/COAnonymousClass.java index ec8c6b2cf6a..c360606b8a3 100644 --- a/checker/tests/resourceleak/COAnonymousClass.java +++ b/checker/tests/resourceleak/COAnonymousClass.java @@ -20,8 +20,12 @@ void other() { // :: error: creates.mustcall.for.invalid.target // :: error: creates.mustcall.for.override.invalid public void run() { + // [The following explanation is incorrect. The problem is a bug in + // creating + // implicit "this" expressions.] // Ideally, we would not issue the following error. However, the Checker - // Framework's JavaExpression support + // Framework's + // JavaExpression support // (https://checkerframework.org/manual/#java-expressions-as-arguments) // treats all versions of "this" (including "Foo.this") as referring to // the object that directly contains the annotation, so we treat this diff --git a/checker/tests/resourceleak/IOUtilsTest.java b/checker/tests/resourceleak/IOUtilsTest.java new file mode 100644 index 00000000000..eaa1721c8fa --- /dev/null +++ b/checker/tests/resourceleak/IOUtilsTest.java @@ -0,0 +1,17 @@ +import org.checkerframework.checker.mustcall.qual.*; + +import java.io.*; + +class IOUtilsTest { + static void test1(@Owning InputStream inputStream) { + org.apache.commons.io.IOUtils.closeQuietly(inputStream); + } + + static void test2(@Owning InputStream inputStream) throws IOException { + try { + InputStream other = org.apache.commons.io.IOUtils.toBufferedInputStream(inputStream); + } finally { + inputStream.close(); + } + } +} diff --git a/checker/tests/resourceleak/JavaEETest.java b/checker/tests/resourceleak/JavaEETest.java new file mode 100644 index 00000000000..b4fc459de04 --- /dev/null +++ b/checker/tests/resourceleak/JavaEETest.java @@ -0,0 +1,7 @@ +// Test for https://github.com/typetools/checker-framework/issues/5472 + +class JavaEETest { + static void foo(javax.servlet.ServletResponse s) throws java.io.IOException { + s.getWriter(); + } +} diff --git a/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java b/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java index dc3d76ea6ea..2cfd9ef0611 100644 --- a/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java +++ b/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java @@ -71,6 +71,9 @@ class ReplicaInputStreams implements Closeable { private final @Owning InputStream in2; public @MustCallAlias ReplicaInputStreams( + // This class is unsafe: calling close on i1 doesn't result in calling close on i2, + // so this MustCallAlias relationship shouldn't be verified. + // :: error: mustcallalias.out.of.scope @MustCallAlias InputStream i1, @MustCallAlias InputStream i2) { this.in1 = i1; this.in2 = i2; diff --git a/checker/tests/resourceleak/TwoOwningMCATest.java b/checker/tests/resourceleak/TwoOwningMCATest.java new file mode 100644 index 00000000000..5166c73253d --- /dev/null +++ b/checker/tests/resourceleak/TwoOwningMCATest.java @@ -0,0 +1,38 @@ +// Test case for issue 5453: https://github.com/typetools/checker-framework/issues/5453 + +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +@InheritableMustCall({"finish1", "finish2"}) +class TwoOwningMCATest { + + @Owning private final Foo f1 = new Foo(); + + @Owning private final Foo f2; + + @MustCallAlias + // :: error: mustcallalias.out.of.scope + TwoOwningMCATest(@MustCallAlias Foo g) { + this.f2 = g; + } + + @EnsuresCalledMethods(value = "this.f1", methods = "a") + void finish1() { + this.f1.a(); + } + + @EnsuresCalledMethods(value = "this.f2", methods = "a") + void finish2() { + this.f2.a(); + } + + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + public static void test(Foo f) { + TwoOwningMCATest t = new TwoOwningMCATest(f); + f.a(); + } +} diff --git a/checker/tests/resourceleak/TwoSocketContainer.java b/checker/tests/resourceleak/TwoSocketContainer.java new file mode 100644 index 00000000000..f290e89aaf0 --- /dev/null +++ b/checker/tests/resourceleak/TwoSocketContainer.java @@ -0,0 +1,38 @@ +// A test that a class with two owned sockets cannot be @MustCallAliased with both of them. + +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +import java.net.Socket; + +@InheritableMustCall({"close1", "close2"}) +public class TwoSocketContainer { + @Owning private final Socket s1, s2; + + // :: error: mustcallalias.out.of.scope + public @MustCallAlias TwoSocketContainer(@MustCallAlias Socket s1, @MustCallAlias Socket s2) { + this.s1 = s1; + this.s2 = s2; + } + + @EnsuresCalledMethods( + value = "this.s1", + methods = {"close"}) + public void close1() throws java.io.IOException { + s1.close(); + } + + @EnsuresCalledMethods( + value = "this.s2", + methods = {"close"}) + public void close2() throws java.io.IOException { + s2.close(); + } + + // The following error should be thrown about at least sock2 + // :: error: required.method.not.called + public static void test(@Owning Socket sock1, @Owning Socket sock2) throws java.io.IOException { + TwoSocketContainer tsc = new TwoSocketContainer(sock1, sock2); + sock1.close(); + } +} diff --git a/checker/tests/resourceleak/TwoSocketContainerSafe.java b/checker/tests/resourceleak/TwoSocketContainerSafe.java new file mode 100644 index 00000000000..6e1482a1e76 --- /dev/null +++ b/checker/tests/resourceleak/TwoSocketContainerSafe.java @@ -0,0 +1,43 @@ +// This is the safe version of TwoSocketContainer.java. + +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +import java.net.Socket; + +@InheritableMustCall({"close1", "close2"}) +public class TwoSocketContainerSafe { + @Owning private final Socket s1, s2; + + public TwoSocketContainerSafe(@Owning Socket s1, @Owning Socket s2) { + this.s1 = s1; + this.s2 = s2; + } + + @EnsuresCalledMethods( + value = "this.s1", + methods = {"close"}) + public void close1() throws java.io.IOException { + s1.close(); + } + + @EnsuresCalledMethods( + value = "this.s2", + methods = {"close"}) + public void close2() throws java.io.IOException { + s2.close(); + } + + public static void test(@Owning Socket sock1, @Owning Socket sock2) throws java.io.IOException { + TwoSocketContainerSafe tsc = new TwoSocketContainerSafe(sock1, sock2); + try { + tsc.close1(); + } catch (Exception io) { + } finally { + try { + tsc.close2(); + } catch (Exception io2) { + } + } + } +} diff --git a/checker/tests/tainting/Issue5435.java b/checker/tests/tainting/Issue5435.java new file mode 100644 index 00000000000..61140363fc0 --- /dev/null +++ b/checker/tests/tainting/Issue5435.java @@ -0,0 +1,7 @@ +class Issue5435 { + public @interface A1 {} + + public @interface A2 { + A1[] m() default {@A1()}; + } +} diff --git a/checker/tests/wpi-many/testin.txt b/checker/tests/wpi-many/testin.txt index b4aacc4b055..4d9bfff67d0 100644 --- a/checker/tests/wpi-many/testin.txt +++ b/checker/tests/wpi-many/testin.txt @@ -1,7 +1,7 @@ -https://github.com/kelloggm/wpi-many-tests-bcel-util 74be0b18f893077223850d5ffb117e496c4b833a -https://github.com/kelloggm/wpi-many-tests-bibtex-clean b7ac872c9323a0944015cd79014e45fb7a5d1c93 -https://github.com/kelloggm/wpi-many-tests-ensures-called-methods db816432c95a3d047a1e3f7966fefb1515cba7c9 -https://github.com/kelloggm/wpi-many-tests-html-pretty-print 1c4f2da82407e21eb89a9196f06d613a64af211a -https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 7a70d58b9fdaedd71c4af4a9dfca7d5fda9268dc +https://github.com/kelloggm/wpi-many-tests-bcel-util a3826a2663c73f0c5f87c1bfcb36e7a156d05ec4 +https://github.com/kelloggm/wpi-many-tests-bibtex-clean c65dec43f346b4c89fdc5636c1ac719f49726f86 +https://github.com/kelloggm/wpi-many-tests-ensures-called-methods 9a07424a21d2c3248c50049aa041d905225f76ae +https://github.com/kelloggm/wpi-many-tests-html-pretty-print 9ae8cc4eca139ac58a4d8da5f7f00ada759730da +https://github.com/kelloggm/-wpi-many-tests-bibtex-clean dcc3bff57c1d977004cf9526773f179f51f62559 # This comment line tests that the commenting feature works (if it doesn't, then this line will be read and fail, as it's not a URL). -https://github.com/Nargeshdb/wpi-many-tests-owning-field 6accab941bdae0274862ab414d729851851670ea +https://github.com/Nargeshdb/wpi-many-tests-owning-field e73696ffffc090935c9dd44a6770bbf9e43043ad diff --git a/dataflow/build.gradle b/dataflow/build.gradle index 01d3c2397a9..3e9b43613de 100644 --- a/dataflow/build.gradle +++ b/dataflow/build.gradle @@ -97,13 +97,13 @@ def testDataflowAnalysis(taskName, dirName, className, diff) { } else if (JavaVersion.current() > JavaVersion.VERSION_11) { jvmArgs += [ - "--add-opens", "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", - "--add-opens", "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED", - "--add-opens", "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", - "--add-opens", "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", - "--add-opens", "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", - "--add-opens", "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", - "--add-opens", "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", + '--add-opens', 'jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED', + '--add-opens', 'jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED', + '--add-opens', 'jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED', + '--add-opens', 'jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED', + '--add-opens', 'jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED', + '--add-opens', 'jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED', + '--add-opens', 'jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED', ] } @@ -131,7 +131,7 @@ testDataflowAnalysis("liveVariableTest", "live-variable", "livevar.LiveVariable" testDataflowAnalysis("issue3447Test", "issue3447", "livevar.LiveVariable", false) testDataflowAnalysis("reachingDefinitionTest", "reachingdef", "reachingdef.ReachingDefinition", true) -apply from: rootProject.file("gradle-mvn-push.gradle") +apply from: rootProject.file('gradle-mvn-push.gradle') /** Adds information to the publication for uploading the dataflow artifacts to Maven repositories. */ final dataflowPom(publication) { diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex index 40078bdc1cb..86269fc79fc 100644 --- a/dataflow/manual/content.tex +++ b/dataflow/manual/content.tex @@ -1,12 +1,19 @@ +% -*- mode: latex; TeX-master: "dataflow"; TeX-command-default: "PDF"; -*- +%% Put local variables at beginning of file because Emacs function +%% `hack-local-variables` only looks backwards 3000 characters for the "Local +%% Variables" block, that number is hardcoded, and the "LocalWords" part of this +%% file is longer than that. + \section{Introduction} This document describes a \emph{Dataflow Framework} for the Java -programming language. The Dataflow Framework is used in the +programming language. This is an industrial-strength framework. +The Dataflow Framework is used in the \href{https://checkerframework.org/}{Checker Framework}, -\href{http://errorprone.info/}{Error Prone}, -\href{https://github.com/uber/NullAway}{NullAway}, -at Facebook, +Google's \href{http://errorprone.info/}{Error Prone}, +Uber's \href{https://github.com/uber/NullAway}{NullAway}, +Facebook's \href{https://engineering.fb.com/2022/11/22/developer-tools/meta-java-nullsafe/}{Nullsafe}, and in other contexts. The primary purpose of the Dataflow Framework is to estimate values: @@ -60,11 +67,11 @@ \section{Introduction} gives an introduction to customizing dataflow to add checker-specific enhancements. -\begin{workinprogress} - Paragraphs colored in gray with a gray bar on the left side (just - like this one) contain questions, additional comments or indicate - missing parts. Eventually, these paragraphs will be removed. -\end{workinprogress} +% \begin{workinprogress} +% Paragraphs colored in gray with a gray bar on the left side (just +% like this one) contain questions, additional comments or indicate +% missing parts. Eventually, these paragraphs will be removed. +% \end{workinprogress} \subsection{Potential version conflicts if you export the Dataflow Framework} @@ -303,9 +310,9 @@ \subsubsection{AbstractValue} For the Nullness Checker, abstract values additionally track the meaning of PolyNull, which may be either Nullable or NonNull. The meaning of PolyNull can change when a PolyNull value is compared to -the null literal, which is specific to the NullnessChecker. Other +the null literal, which is specific to the Nullness Checker. Other checkers often also support a Poly* qualifier, but only the -NullnessChecker tracks the meaning of its poly qualifier using the +Nullness Checker tracks the meaning of its poly qualifier using the dataflow analysis. \begin{verbatim} @@ -642,7 +649,7 @@ \subsection{Formal Definition of the Control-Flow Graph} \item \textbf{Regular basic block.} A \emph{regular basic block} contains any non-empty sequence of nodes and has exactly one successor. None of the nodes in the block can - throw an exception at runtime. + throw an exception at run time. \item \textbf{Special basic blocks.} A \emph{special basic block} contains the empty sequence of nodes (i.e., is empty) @@ -664,7 +671,7 @@ \subsection{Formal Definition of the Control-Flow Graph} \item \textbf{Exception basic block.} An \emph{exception basic block} contains exactly one node that \emph{might} throw an - exception at runtime (e.g., a method call). There are zero + exception at run time (e.g., a method call). There are zero or one non-exceptional successors (only a basic block containing a \code{throw} statement does not have a non-exceptional successor). There are one or more @@ -765,11 +772,14 @@ \subsection{Formal Definition of the Control-Flow Graph} to see what expressions are summed up and because we don't create internal names for expression results. -\autoref{tab:nodes} lists all node types in the framework. We use the -Java class name of the implementation, but leave out the suffix -\code{Node}, which is present for every type. +\autoref{tab:nodes} lists all node types in the framework. All classes are in package \code{org.checkerframework.dataflow.cfg.node}. +% Defining a command for node types makes it easier to determine all the +% node types that the manual discusses. One can compare this list with the +% source code to ensure that every node type is listed. +\newcommand{\nodetype}[1]{\code{#1}} + \begin{longtable}{lp{0.4\linewidth}l} \midrule \multicolumn{3}{c}{\autoref{tab:nodes}: All node types in the Dataflow Framework.} \\ \\ @@ -779,122 +789,136 @@ \subsection{Formal Definition of the Control-Flow Graph} \hline \multicolumn{3}{|c|}{{Continued on next page}} \\ \hline \endfoot \endlastfoot - \code{Node} & The base class of all nodes. & \\ + \nodetype{Node} & The base class of all nodes. & \\ \midrule - \code{ValueLiteral} & The base class of literal value nodes. & \\ - \code{BooleanLiteral} & & \code{true} \\ - \code{CharacterLiteral} & & \code{'c'} \\ - \code{DoubleLiteral} & & \code{3.14159} \\ - \code{FloatLiteral} & & \code{1.414f} \\ - \code{IntegerLiteral} & & \code{42} \\ - \code{LongLiteral} & & \code{1024L} \\ - \code{NullLiteral} & & \code{null} \\ - \code{ShortLiteral} & & \code{512} \\ - \code{StringLiteral} & & \code{"memo"} \\ + \nodetype{ValueLiteralNode} & The base class of literal value nodes. & \\ + \nodetype{BooleanLiteralNode} & & \code{true} \\ + \nodetype{CharacterLiteralNode} & & \code{'c'} \\ + \nodetype{DoubleLiteralNode} & & \code{3.14159} \\ + \nodetype{FloatLiteralNode} & & \code{1.414f} \\ + \nodetype{IntegerLiteralNode} & & \code{42} \\ + \nodetype{LongLiteralNode} & & \code{1024L} \\ + \nodetype{NullLiteralNode} & & \code{null} \\ + \nodetype{ShortLiteralNode} & & \code{512} \\ + \nodetype{StringLiteralNode} & & \code{"memo"} \\ \midrule & Accessor expressions & \\ - \code{ArrayAccess} & & \code{args[i]} \\ - \code{FieldAccess} & & \code{f}, \code{obj.f} \\ - \code{MethodAccess} & & \code{obj.hashCode} \\ - \code{This} & Base class of references to \code{this} & \\ - \code{ExplicitThis} & Explicit use of \code{this} in an expression & \\ - \code{ImplicitThis} & Implicit use of \code{this} in an expression & \\ - \code{Super} & Explicit use of \code{super} in expression. & \code{super(x, y)} \\ - \code{LocalVariable} & Use of a local variable, either as l-value or r-value & \\ + \nodetype{ArrayAccessNode} & & \code{args[i]} \\ + \nodetype{FieldAccessNode} & & \code{f}, \code{obj.f} \\ + \nodetype{MethodAccessNode} & & \code{obj.hashCode} \\ + \nodetype{LocalVariableNode} & Use of a local variable, either as l-value or r-value & \\ + \nodetype{ThisNode} & Base class of references to \code{this} & \\ + \nodetype{ExplicitThisNode} & Explicit use of \code{this} in an expression & \\ + \nodetype{ImplicitThisNode} & Implicit use of \code{this} in an expression & \\ + \nodetype{SuperNode} & Explicit use of \code{super} in expression. & \code{super(x, y)} \\ \midrule - \code{MethodInvocation} & Note that access and invocation are distinct. & \code{hashCode()} \\ + \nodetype{MethodInvocationNode} & Note that access and invocation are distinct. & \code{hashCode()} \\ \midrule - & Arithmetic and logical operations & \\ - \code{BitwiseAnd} & & a \& \code{b} \\ - \code{BitwiseComplement} & & \verb|~b| \\ - \code{BitwiseOr} & & \code{a | b} \\ - \code{BitwiseXor} & & \code{a ^ b} \\ - \code{ConditionalAnd} & Short-circuiting. & a \&\& \code{b} \\ - \code{ConditionalNot} & & \code{!a} \\ - \code{ConditionalOr} & Short-circuiting. & \code{a || b} \\ - \code{FloatingDivision} & & \code{1.0 / 2.0} \\ - \code{FloatingRemainder} & & \code{13.0 \% 4.0} \\ - \code{LeftShift} & & \code{x << 3} \\ - \code{IntegerDivision} & & \code{3 / 2} \\ - \code{IntegerRemainder} & & \code{13 \% 4} \\ - \code{NumericalAddition} & & \code{x + y} \\ - \code{NumericalMinus} & & \code{-x} \\ - \code{NumericalMultiplication} & & \code{x * y} \\ - \code{NumericalPlus} & & \code{+x} \\ - \code{NumericalSubtraction} & & \code{x - y} \\ - \code{SignedRightShift} & & \code{x >> 3} \\ - \code{StringConcatenate} & & \code{s + ".txt"} \\ - \code{TernaryExpression} & & \code{c ? t : f} \\ - \code{UnsignedRightShift} & & \code{x >>> 5} \\ + & Expression supertypes. & \\ + \nodetype{BinaryOperationNode} & Base class of binary expression nodes & \\ + \nodetype{UnaryOperationNode} & Base class of unary expression nodes & \\ + + & Arithmetic and logical operations. & \\ + \nodetype{BitwiseAndNode} & & a \& \code{b} \\ + \nodetype{BitwiseComplementNode} & & \verb|~b| \\ + \nodetype{BitwiseOrNode} & & \code{a | b} \\ + \nodetype{BitwiseXorNode} & & \code{a ^ b} \\ + \nodetype{ConditionalAndNode} & Short-circuiting. & a \&\& \code{b} \\ + \nodetype{ConditionalNotNode} & & \code{!a} \\ + \nodetype{ConditionalOrNode} & Short-circuiting. & \code{a || b} \\ + \nodetype{FloatingDivisionNode} & & \code{1.0 / 2.0} \\ + \nodetype{FloatingRemainderNode} & & \code{13.0 \% 4.0} \\ + \nodetype{LeftShiftNode} & & \code{x << 3} \\ + \nodetype{IntegerDivisionNode} & & \code{3 / 2} \\ + \nodetype{IntegerRemainderNode} & & \code{13 \% 4} \\ + \nodetype{NumericalAdditionNode} & & \code{x + y} \\ + \nodetype{NumericalMinusNode} & & \code{-x} \\ + \nodetype{NumericalMultiplicationNode} & & \code{x * y} \\ + \nodetype{NumericalPlusNode} & & \code{+x} \\ + \nodetype{NumericalSubtractionNode} & & \code{x - y} \\ + \nodetype{SignedRightShiftNode} & & \code{x >> 3} \\ + \nodetype{StringConcatenateNode} & & \code{s + ".txt"} \\ + \nodetype{SwitchExpressionNode} & & \\ + \nodetype{TernaryExpressionNode} & & \code{c ? t : f} \\ + \nodetype{UnsignedRightShiftNode} & & \code{x >>> 5} \\ \midrule & Relational operations & \\ - \code{EqualTo} & & \code{x == y} \\ - \code{NotEqual} & & \code{x != y} \\ - \code{GreaterThan} & & \code{x > y} \\ - \code{GreaterThanOrEqual} & & \code{x >= y} \\ - \code{LessThan} & & \code{x < y} \\ - \code{LessThanOrEqual} & & \code{x <= y} \\ + \nodetype{EqualToNode} & & \code{x == y} \\ + \nodetype{NotEqualNode} & & \code{x != y} \\ + \nodetype{GreaterThanNode} & & \code{x > y} \\ + \nodetype{GreaterThanOrEqualNode} & & \code{x >= y} \\ + \nodetype{LessThanNode} & & \code{x < y} \\ + \nodetype{LessThanOrEqualNode} & & \code{x <= y} \\ + + \nodetype{CaseNode} & Case of a switch. Acts as an equality test. & \\ \midrule - \code{SwitchExpression} & A switch expression (not statement!) & \\ - \code{Case} & Case of a switch. Acts as an equality test. & \\ + \nodetype{AssignmentNode} & & \code{x = 1} \\ +% \midrule + + \nodetype{StringConcatenateAssignmentNode} & A compound \code{String} assignment. & \code{s += ".txt"} \\ \midrule - \code{Assignment} & & \code{x = 1} \\ + \nodetype{ArrayCreationNode} & & \code{new double[]} \\ + \nodetype{ObjectCreationNode} & & \code{new Object()} \\ \midrule - \code{ArrayCreation} & & \code{new double[]} \\ - \code{ObjectCreation} & & \code{new Object()} \\ + \nodetype{FunctionalInterfaceNode} & A member reference or lambda & \\ \midrule - \code{TypeCast} & & \code{(float) 42} \\ - \code{InstanceOf} & & \code{x instanceof Float} \\ + \nodetype{TypeCastNode} & & \code{(float) 42} \\ + \nodetype{InstanceOfNode} & & \code{x instanceof Float} \\ \midrule - & Conversion nodes & \\ - \code{NarrowingConversion} & Implicit conversion. & \\ - \code{StringConversion} & Might be implicit. & \code{obj.toString()} \\ - \code{WideningConversion} & Implicit conversion. & \\ + & Conversion nodes. & \\ + \nodetype{NarrowingConversionNode} & Implicit conversion. & \\ + \nodetype{StringConversionNode} & Might be implicit. & \code{obj.toString()} \\ + \nodetype{WideningConversionNode} & Implicit conversion. & \\ \midrule \midrule & \textbf{Non-value nodes} & \\ & Types appearing in expressions, such as \code{MyType.class} & \\ - \code{ArrayType} & & \\ - \code{ParameterizedType} & & \\ - \code{PrimitiveType} & & \\ + \nodetype{ArrayTypeNode} & & \\ + \nodetype{ParameterizedTypeNode} & & \\ + \nodetype{PrimitiveTypeNode} & & \\ \midrule - \code{ClassName} & Identifier referring to Java class or interface. & \code{java.util.HashMap} \\ - \code{PackageName} & Identifier referring to Java package. & \code{java.util} \\ + \nodetype{ClassNameNode} & Identifier referring to Java class or interface. & \code{java.util.HashMap} \\ + \nodetype{PackageNameNode} & Identifier referring to Java package. & \code{java.util} \\ \midrule - \code{Throw} & Throw an exception. & \\ - \code{Return} & Return from a method. & \\ + \nodetype{ThrowNode} & Throw an exception. & \\ + \nodetype{ReturnNode} & Return from a method. & \\ \midrule - \code{AssertionError} & & \code{assert x != null : "Hey"} \\ + \nodetype{AssertionErrorNode} & & \code{assert x != null : "Hey"} \\ \midrule - \code{ExpressionStatement} & An expression that is used as a statement. & \code{m();} \\ + \nodetype{ExpressionStatementNode} & An expression that is used as a statement. & \code{m();} \\ \midrule - \code{Marker} & No-op nodes used to annotate a CFG with + \nodetype{SynchronizedNode} & Start or end of a synchronized code block. & \\ + \nodetype{MarkerNode} & No-op node used to annotate a CFG with information of the underlying Java source code. Mostly useful for debugging and visualization. An example is indicating the start/end of switch statements. & \\ \midrule - \code{NullChk} & Null checks inserted by javac & \\ + \nodetype{NullChkNode} & Null checks inserted by javac & \\ + \midrule + + \nodetype{VariableDeclarationNode} & Declaration of a local variable & \\ + \nodetype{ClassDeclarationNode} & Declaration of a class & \\ \midrule - \code{VariableDeclaration} & Declaration of a local variable & \\ + \nodetype{LambdaResultExpressionNode} & Body of a single-expression lambda & \\ \midrule \caption{All node types in the Dataflow Framework.} @@ -935,31 +959,10 @@ \subsection{Formal Definition of the Control-Flow Graph} \label{tab:nodesWithException} \end{table} -\begin{workinprogress} -Can \code{StringConversion} be implicit? I think so, but in any event discuss. -\end{workinprogress} - -\begin{workinprogress} -For each non-expression, explain its purpose, just like the explanation for -Marker that still needs to be fleshed out. -\end{workinprogress} - -\begin{workinprogress} -``Could be desugared'' on ``Conversion -nodes'' was confusing. What is the design rationale for -desugaring in the Dataflow Framework? Discuss that. Here, at least -forward-reference to \autoref{sec:desugaring}, if that's relevant. \\ -More generally, for any cases that will be discussed in the text, add a -forward reference to the section with the discussion. -\end{workinprogress} +Other AST constructs are desugared into the above nodes (see \autoref{sec:desugaring}). \begin{workinprogress} -When we added Java~8 support, did we add additional nodes that are not -listed here? Cross-check with implementation. -\end{workinprogress} - -\begin{workinprogress} -Why is it \code{AssertionErrorNode} instead of \code{AssertNode}? +Can \code{StringConversionNode} be implicit? I think so, but in any event discuss. \end{workinprogress} @@ -1236,7 +1239,7 @@ \subsection{AST to CFG Translation} as defined in Definition~\ref{def:node}. \item \textbf{Exception extended node.} Similar to a simple node, an exception extended node contains a node, but this - node might throw an exception at runtime. + node might throw an exception at run time. \item \textbf{Unconditional jump.} An unconditional jump indicates that control flow proceeds non-sequentially to a location indicated by a target label. @@ -1429,14 +1432,10 @@ \subsubsection{Conversions and node-tree mapping} apply to the conversions with no special work on the part of a checker developer. -Widening and narrowing conversions are still represented as special +Widening and narrowing conversions are represented as special node types, although it would be more consistent to change them into type casts. -\begin{workinprogress} -Is the last point a to-do item? -\end{workinprogress} - We maintain the invariant that a CFG node maps to zero or one AST tree and almost all of them map to a single tree. But we can't maintain a unique inverse mapping because some trees have both pre- and @@ -1465,7 +1464,7 @@ \section{Dataflow Analysis} algorithm is used to compute a fix-point, by iteratively applying a set of transfer functions to the nodes in the CFG\@. These transfer functions are specific to the particular analysis and are used to -approximate the runtime behavior of different statements and expressions. +approximate the run-time behavior of different statements and expressions. \subsection{Managing Intermediate Results of the Analysis} @@ -1871,14 +1870,6 @@ \subsection{Interaction of the Checker Framework and the Dataflow Analysis} type for the tree node was inferred by the analysis. This is the first type of query described in \autoref{sec:answering-questions}. -\begin{workinprogress} -I found the below section confusing. I had a hard time putting my finger -on it, but perhaps you could re-read the section. As one minor issue, -``very similar'': similar to what? ``intermediary nodes'': what are -those? ``we'': is that the analysis writer or the framework implementor -(or the runtime system)? -\end{workinprogress} - Dataflow itself uses the type factory to get the initial \code{AnnotatedTypeMirror} for a tree node in the following way. @@ -2066,17 +2057,6 @@ \subsubsubsection{Alias Information} and $<:$ denotes standard Java subtyping. -%% Problem: Emacs function `hack-local-variables` only looks backwards 3000 -%% characters for the "Local Variables" block, that number is hardcoded, -%% and the "LocalWords" part of this file is longer than that if its lines -%% are only (say) 100 characters long. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "dataflow" -%%% TeX-command-default: "PDF" -%%% End: - % LocalWords: pre cfg javacutils InternalUtils DivideByZero BlockImpl se SingleSuccessorBlock RegularBlock SingleSuccessorBlockImpl ExceptionBlock SpecialBlock ConditionalBlock SpecialBlocks % LocalWords: ControlFlowGraph ControlFlowGraphs CFGBuilder ast CFValue JavaExpressions AbstractValue AbstractValues PolyNull Poly AnnotatedTypeMirrors CFAbstractValue NullnessValue CFStore % LocalWords: NullnessCheckers CFAbstractStore InitializationStore Regex NullnessStore TransferInput TransferResult TransferInputs ConditionalTransferResult RegularTransferResult CFTransfer @@ -2086,9 +2066,20 @@ \subsubsubsection{Alias Information} % LocalWords: IntegerLiteral LongLiteral NullLiteral ShortLiteral args StringLiteral Accessor ArrayAccess FieldAccess This MethodAccess ExplicitThis ImplicitThis NullAway % LocalWords: LocalVariable MethodInvocation BitwiseAnd BitwiseOr MyType BitwiseComplement BitwiseXor ConditionalAnd ConditionalNot ConditionalOr FloatingDivision FloatingRemainder LeftShift % LocalWords: IntegerDivision IntegerRemainder NumericalAddition EqualTo NumericalMinus NumericalMultiplication NumericalPlus util NumericalSubtraction SignedRightShift StringConcatenate -% LocalWords: TernaryExpression UnsignedRightShift NotEqual GreaterThan GreaterThanOrEqual LessThan LessThanOrEqual ArrayCreation StringConcatenateAssignment ObjectCreation TypeCast cond +% LocalWords: TernaryExpression UnsignedRightShift NotEqual GreaterThan GreaterThanOrEqual LessThan ArrayCreation StringConcatenateAssignment ObjectCreation TypeCast cond % LocalWords: InstanceOf NarrowingConversion StringConversion WideningConversion ArrayType ParameterizedType ClassName PrimitiveType PackageName AssertionError NullChk accessor % LocalWords: VariableDeclaration FieldAssignment CFGFieldAssignment getRegularStore CFGConditionalOr fnc CFGConditionalOr2 ConditionalOrNode ConditionalOr2 valueOf % LocalWords: IdentifierTree FieldAccessNode ImplicitThisNode unboxing TreePath pathHack MethodTree VarSymbol DetachedVarSymbols DeclarationFromElement BoxedClass treeLookup getValue % LocalWords: nodeValues AdditionNode postconversion treelookup LocalVariableNode AconcurrentSemantics MonotonicNonNull MonotonicQualifier IntegerLiteralNode EqualToNode unshaded % LocalWords: ConstSimple SelfReference PureMethodCall javacutil stubparser TreeParser TreeBuilder DetachedVarSymbol LiveSimple +% LocalWords: Uber's Nullsafe CFGVisualizeLauncher intra boolean subparts ValueLiteralNode c' lang BooleanLiteralNode CharacterLiteralNode DoubleLiteralNode FloatLiteralNode ThisNode +% LocalWords: LongLiteralNode NullLiteralNode ShortLiteralNode StringLiteralNode ArrayAccessNode MethodAccessNode ExplicitThisNode SuperNode MethodInvocationNode BinaryOperationNode +% LocalWords: UnaryOperationNode BitwiseAndNode BitwiseComplementNode BitwiseOrNode BitwiseXorNode ConditionalAndNode ConditionalNotNode FloatingDivisionNode FloatingRemainderNode b1 +% LocalWords: LeftShiftNode IntegerDivisionNode IntegerRemainderNode NumericalAdditionNode b2 b3 NumericalMinusNode NumericalMultiplicationNode NumericalPlusNode NotEqualNode num0 +% LocalWords: NumericalSubtractionNode SignedRightShiftNode StringConcatenateNode GreaterThanNode SwitchExpressionNode TernaryExpressionNode UnsignedRightShiftNode LessThanNode +% LocalWords: GreaterThanOrEqualNode LessThanOrEqualNode CaseNode AssignmentNode ArrayCreationNode StringConcatenateAssignmentNode ObjectCreationNode FunctionalInterfaceNode ThrowNode +% LocalWords: TypeCastNode InstanceOfNode instanceof NarrowingConversionNode StringConversionNode WideningConversionNode ArrayTypeNode ParameterizedTypeNode PrimitiveTypeNode Varargs +% LocalWords: ClassNameNode PackageNameNode ReturnNode AssertionErrorNode SynchronizedNode varargs MarkerNode NullChkNode VariableDeclarationNode ClassDeclarationNode NoSuchFieldError +% LocalWords: LambdaResultExpressionNode ArrayIndexOutOfBoundsException Throwable ClassFormatError ArithmeticException NegativeArraySizeException ClassCircularityError CFGIfStatement +% LocalWords: NoClassDefFoundError unaryAssignNodeLookup assertionsEnabled CFGAssert CFGSwitch +% LocalWords: intValue diff --git a/dataflow/manual/dataflow.tex b/dataflow/manual/dataflow.tex index cfae694830a..2c789faff20 100644 --- a/dataflow/manual/dataflow.tex +++ b/dataflow/manual/dataflow.tex @@ -15,6 +15,8 @@ \usepackage{ucs} \usepackage{longtable} +\usepackage{relsize} + % At least 80% of every float page must be taken up by % floats; there will be no page with more than 20% white space. \def\topfraction{.95} @@ -57,7 +59,7 @@ commentstyle=\color{gray}, captionpos=b } -\newcommand{\code}[1]{\lstinline{#1}} +\newcommand{\code}[1]{{\smaller\lstinline{#1}}} \usepackage{fullpage} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java index 6dec6dc02e6..78bb24a4699 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java @@ -221,7 +221,7 @@ public IdentityHashMap getNodeValues() { * * @param in the current node values */ - /*package-private*/ void setNodeValues(IdentityHashMap in) { + /* package-private */ void setNodeValues(IdentityHashMap in) { assert !isRunning; nodeValues.clear(); nodeValues.putAll(in); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferResult.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferResult.java index 0f4d3b639e9..938a01a43ad 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferResult.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferResult.java @@ -23,6 +23,8 @@ public abstract class TransferResult, S extends Store /** * The abstract value of the {@link org.checkerframework.dataflow.cfg.node.Node} associated with * this {@link TransferResult}, or {@code null} if no value has been produced. + * + *

Is set by {@link #setResultValue}. */ protected @Nullable V resultValue; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ExceptionBlockImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ExceptionBlockImpl.java index fa97695ce7f..14ac2c21b0c 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ExceptionBlockImpl.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ExceptionBlockImpl.java @@ -13,7 +13,7 @@ import javax.lang.model.type.TypeMirror; -/** Base class of the {@link Block} implementation hierarchy. */ +/** Implementation of {@link ExceptionBlock}. */ public class ExceptionBlockImpl extends SingleSuccessorBlockImpl implements ExceptionBlock { /** The node of this block. */ diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java index 5fdfe07ced1..429a17c14ce 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java @@ -12,7 +12,11 @@ */ public abstract class SingleSuccessorBlockImpl extends BlockImpl implements SingleSuccessorBlock { - /** Internal representation of the successor. */ + /** + * Internal representation of the successor. + * + *

Is set by {@link #setSuccessor}. + */ protected @Nullable BlockImpl successor; /** diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index d57f4822eae..6e748c089c3 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -844,8 +844,15 @@ protected void addLabelForNextNode(Label l) { /* Utility Methods */ /* --------------------------------------------------------- */ + /** The UID for the next unique name. */ protected long uid = 0; + /** + * Returns a unique name starting with {@code prefix}. + * + * @param prefix the prefix of the unique name + * @return a unique name starting with {@code prefix} + */ protected String uniqueName(String prefix) { return prefix + "#num" + uid++; } @@ -2332,7 +2339,8 @@ public Node visitBreak(BreakTree tree, Void p) { return null; } - // This visits a switch statement, not a switch expression. + // This visits a switch statement. + // Switch expressions are visited by visitSwitchExpression17. @Override public Node visitSwitch(SwitchTree tree, Void p) { SwitchBuilder builder = new SwitchBuilder(tree); @@ -2434,16 +2442,31 @@ private SwitchBuilder(Tree switchTree) { for (int i = 0; i < numCases; ++i) { CaseTree caseTree = caseTrees.get(i); if (TreeUtils.isDefaultCaseTree(caseTree)) { + // Per the Java Language Specification, the checks of all cases must happen + // before the + // default case, no matter where `default:` is written. Therefore, build the + // default + // case last. defaultIndex = i; } else { - buildCase(caseTree, i); + boolean isLastExceptDefault = + i == numCases - 1 + || (i == numCases - 2 + && TreeUtils.isDefaultCaseTree(caseTrees.get(i + 1))); + // This can be extended to handle case statements as well as case rules. + boolean noFallthroughToHere = TreeUtils.isCaseRule(caseTree); + boolean isLastOfExhaustive = + isLastExceptDefault && casesAreExhaustive() && noFallthroughToHere; + buildCase(caseTree, i, isLastOfExhaustive); } } + if (defaultIndex != -1) { // The checks of all cases must happen before the default case, therefore we build - // the default case last. + // the + // default case last. // Fallthrough is still handled correctly with the caseBodyLabels. - buildCase(caseTrees.get(defaultIndex), defaultIndex); + buildCase(caseTrees.get(defaultIndex), defaultIndex, false); } addLabelForNextNode(breakTargetLC.peekLabel()); @@ -2540,17 +2563,28 @@ private void buildSwitchExpressionVar() { * * @param tree a case tree whose CFG to build * @param index the index of the case tree in {@link #caseBodyLabels} + * @param isLastOfExhaustive true if this is the last case of an exhaustive switch + * statement, with no fallthrough to it. In other words, no test of the labels is + * necessary. */ - private void buildCase(CaseTree tree, int index) { + private void buildCase(CaseTree tree, int index, boolean isLastOfExhaustive) { boolean isDefaultCase = TreeUtils.isDefaultCaseTree(tree); + // If true, no test of labels is necessary. + // Unfortunately, if isLastOfExhaustive==TRUE, no flow-sensitive refinement occurs + // within the + // body of the CaseNode. In the future, that can be performed, but it requires addition + // of + // InfeasibleExitBlock, a new SpecialBlock in the CFG. + boolean isTerminalCase = isDefaultCase || isLastOfExhaustive; final Label thisBodyLabel = caseBodyLabels[index]; final Label nextBodyLabel = caseBodyLabels[index + 1]; + // `nextCaseLabel` is not used if isTerminalCase==FALSE. final Label nextCaseLabel = new Label(); // Handle the case expressions - if (!isDefaultCase) { - // non-default cases: a case expression exists + if (!isTerminalCase) { + // A case expression exists, and it needs to be tested. ArrayList exprs = new ArrayList<>(); for (ExpressionTree exprTree : TreeUtils.caseTreeGetExpressions(tree)) { exprs.add(scan(exprTree, null)); @@ -2571,7 +2605,7 @@ private void buildCase(CaseTree tree, int index) { scan(stmt, null); } // Handle possible fallthrough by adding jump to next body. - if (!isDefaultCase) { + if (!isTerminalCase) { extendWithExtendedNode(new UnconditionalJump(nextBodyLabel)); } } else { @@ -2590,7 +2624,7 @@ private void buildCase(CaseTree tree, int index) { } } - if (!isDefaultCase) { + if (!isTerminalCase) { addLabelForNextNode(nextCaseLabel); } } @@ -2632,6 +2666,44 @@ private void buildCase(CaseTree tree, int index) { assert breakTargetLC != null : "no target for case statement"; extendWithExtendedNode(new UnconditionalJump(breakTargetLC.accessLabel())); } + + /** + * Returns true if the cases are exhaustive -- exactly one is executed. There might or might + * not be a `default` case label; if there is, it is never used. + * + * @return true if the cases are exhaustive + */ + boolean casesAreExhaustive() { + TypeMirror selectorTypeMirror = TreeUtils.typeOf(selectorExprTree); + + switch (selectorTypeMirror.getKind()) { + case BOOLEAN: + // TODO + break; + case DECLARED: + DeclaredType declaredType = (DeclaredType) selectorTypeMirror; + TypeElement declaredTypeElement = (TypeElement) declaredType.asElement(); + if (declaredTypeElement.getKind() == ElementKind.ENUM) { + // It's an enumerated type. + List enumConstants = + ElementUtils.getEnumConstants(declaredTypeElement); + List caseLabels = new ArrayList<>(enumConstants.size()); + for (CaseTree caseTree : caseTrees) { + for (ExpressionTree caseEnumConstant : + TreeUtils.caseTreeGetExpressions(caseTree)) { + caseLabels.add(((IdentifierTree) caseEnumConstant).getName()); + } + } + // Could also check that the values match. + boolean result = enumConstants.size() == caseLabels.size(); + return result; + } + break; + default: + break; + } + return false; + } } @Override @@ -3409,7 +3481,7 @@ public Node visitNewClass(NewClassTree tree, Void p) { convertCallArguments(constructor, TreeUtils.typeFromUse(tree), actualExprs); // TODO: for anonymous classes, don't use the identifier alone. - // See Issue 890. + // See https://github.com/typetools/checker-framework/issues/890 . Node constructorNode = scan(tree.getIdentifier(), p); // Handle anonymous classes in visitClass. diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ArrayAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ArrayAccessNode.java index 9f910bccc51..71f813a5887 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ArrayAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ArrayAccessNode.java @@ -35,6 +35,8 @@ public class ArrayAccessNode extends Node { * If this ArrayAccessNode is a node for an array desugared from an enhanced for loop, then the * {@code arrayExpression} field is the expression in the for loop, e.g., {@code arr} in {@code * for(Object o: arr}. + * + *

Is set by {@link #setArrayExpression}. */ protected @Nullable ExpressionTree arrayExpression; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java index ee1be3bd940..b85f22bee43 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java @@ -23,6 +23,10 @@ public R accept(NodeVisitor visitor, P p) { return visitor.visitImplicitThis(this, p); } + // In an inner class context, an implicit this may need to be represented as "Outer.this" rather + // than just as "this". This is context-dependent, and toString doesn't know if it is being + // used + // in an inner class context. @Override public String toString() { return "(this)"; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/LambdaResultExpressionNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/LambdaResultExpressionNode.java index 46f391b5bf7..62b85bbfd83 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/LambdaResultExpressionNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/LambdaResultExpressionNode.java @@ -9,7 +9,7 @@ import java.util.Collections; import java.util.Objects; -/** A node for the single expression body of a single expression lambda. */ +/** A node for the single expression body of a single-expression lambda. */ public class LambdaResultExpressionNode extends Node { /** Tree for the lambda expression body. */ diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodInvocationNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodInvocationNode.java index 3ad2226d709..412d0ae7876 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodInvocationNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/MethodInvocationNode.java @@ -46,6 +46,8 @@ public class MethodInvocationNode extends Node { * If this MethodInvocationNode is a node for an {@link Iterator#next()} desugared from an * enhanced for loop, then the {@code iterExpression} field is the expression in the for loop, * e.g., {@code iter} in {@code for(Object o: iter}. + * + *

Is set by {@link #setIterableExpression}. */ protected @Nullable ExpressionTree iterableExpression; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java index f6202437852..cf334fc3718 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java @@ -42,15 +42,23 @@ public abstract class Node implements UniqueId { /** * The basic block this node belongs to. If null, this object represents a method formal * parameter. + * + *

Is set by {@link #setBlock}. */ protected @Nullable Block block; - /** Is this node an l-value? */ + /** + * Is this node an l-value? + * + *

Is set by {@link #setLValue}. + */ protected boolean lvalue = false; /** * Does this node represent a tree that appears in the source code (true) or one that the CFG * builder added while desugaring (false). + * + *

Is set by {@link #setInSource}. */ protected boolean inSource = true; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SynchronizedNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SynchronizedNode.java index cd33c21badf..13a1ef3f609 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SynchronizedNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SynchronizedNode.java @@ -12,7 +12,7 @@ import javax.lang.model.util.Types; /** - * This represents the start and end of synchronized code block. If startOfBlock == true it is the + * This represents the start and end of a synchronized code block. If startOfBlock == true it is the * node preceding a synchronized code block. Otherwise it is the node immediately after a * synchronized code block. */ diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/AbstractCFGVisualizer.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/AbstractCFGVisualizer.java index dc8a2a35945..11b4910a18e 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/AbstractCFGVisualizer.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/AbstractCFGVisualizer.java @@ -54,10 +54,10 @@ public abstract class AbstractCFGVisualizer< protected boolean verbose; /** The line separator. */ - protected final String lineSeparator = System.lineSeparator(); + protected static final String lineSeparator = System.lineSeparator(); /** The indentation for elements of the store. */ - protected final String storeEntryIndent = " "; + protected static final String storeEntryIndent = " "; @Override public void init(Map args) { diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/Constant.java b/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/Constant.java index 85410cae077..02b5e969ec9 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/Constant.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/Constant.java @@ -10,7 +10,7 @@ public class Constant implements AbstractValue { /** What kind of abstract value is this? */ - protected Type type; + protected final Type type; /** The value of this abstract value (or null). */ protected @Nullable Integer value; diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 33ff3a2fa24..f93950d8d80 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -1,4 +1,4 @@ -Version 3.28.0-eisop2 (December ?, 2022) +Version 3.30.0-eisop1 (February ?, 2023) ---------------------------------------- **User-visible changes:** @@ -11,6 +11,25 @@ in a `BindingPatternTree`. **Closed issues:** +Version 3.29.0 (January 4, 2023) +--------------------------------- + +**User-visible changes:** + +Dropped support for `-ApermitUnsupportedJdkVersion` command-line argument. +You can now run the Checker Framework under any JDK version, without a warning. + +Pass `-Astubs=permit-nullness-assertion-exception.astub` to not be warned about null +pointer exceptions within nullness assertion methods like `Objects.requireNonNull`. + +Pass `-Astubs=sometimes-nullable.astub` to unsoundly permit passing null to +calls if null is sometimes but not always permitted. + +**Closed issues:** + +#5412, #5431, #5435, #5438, #5447, #5450, #5453, #5471, #5472, #5487. + + Version 3.28.0-eisop1 (December 7, 2022) ---------------------------------------- @@ -22,6 +41,8 @@ Support JSpecify annotations in the `org.jspecify.annotations` package. Remove duplicate code in `AnnotatedTypeFactory` and `javacutil`. +**Closed issues:** + Version 3.28.0 (December 1, 2022) --------------------------------- diff --git a/docs/checker-framework-webpage.html b/docs/checker-framework-webpage.html index 4c13b10bf63..7ea02ff70de 100644 --- a/docs/checker-framework-webpage.html +++ b/docs/checker-framework-webpage.html @@ -30,8 +30,8 @@

The Checker Framework

Installation instructions and tutorial.
  • - Download: checker-framework-3.28.0-eisop1.zip - (7 Dec 2022); + Download: checker-framework-3.29.0.zip + (5 Jan 2023); includes source, platform-independent binary, tests, and documentation.
    Then, see the installation @@ -93,7 +93,7 @@

    The Checker Framework

    the .class file. The tools support both Java 5 declaration annotations and Java 8 type annotations.
  • Evaluate a type system or a Checker Framework feature @@ -359,7 +359,7 @@

    Types of projects

    -

    How to apply

    +

    How to apply to GSoC (relevant to GSoC students only)

    (This section is relevant only to Google Summer of Code Students. @@ -542,47 +542,125 @@

    Signature strings

    -

    Java's Optional class

    +

    Detecting errors in use of the Optional class

    + +

    Java 8 introduced the Optional class, a container that is either empty or contains a non-null value. It is intended to solve the problem of null -pointer exceptions. However, Optional has its own problems. +pointer exceptions. However, Optional +has its + own problems, leading +to extensive + advice on when and how to use Optional. It is difficult for +programmers to remember all these rules.

    -Because of Optional's problems, many commentators advise programmers to use -Optional only in limited ways. +The goal of this project is to build a tool to check uses of Optional and run it on open-source projects. The research questions are:

    +
      +
    • Is it possible to build a tool that enforces good style in using Optional? +
      • +
    • How much effort is is for programmers to use such a tool? +
      • +
    • Does real-world code obey the rules about use of Optional, or not? +
      • +

    -The goal of this project is to evaluate -the Optional - Checker, which warns programmers who -have misused Optional. -Another goal is to extend the Optional Checker to make it more precise or -to detect other misuses of Optional. +We have +a prototype + verification tool that checks some but not all rules about use of +Optional (https://checkerframework.org/manual/#optional-checker). This +project will do case studies of it and extend it.

    +

    +The methodology is to find open-source projects that use Optional(you can +do this by searching GitHub, for example), run the tool on them, and read +the tool's warnings. Each warning will lead to either a bug report against +an open-source project or an improvement to the verification tool. +

    + + + + +

    Preventing mixed signed/unsigned computations

    + +

    - The Signedness - Checker ensures that you do not misuse unsigned values, such as - by mixing signed and unsigned values in a computation or by performing a - meaningless operation. +An unsigned integer's bits are interpreted differently than a signed +integer's bits. It is meaningless to add a signed and an unsigned integer +— the result will be nonsense bits. The same is true of printing and +of other numeric operators such as multiplication and comparison.

    - Perform a case study of the Signedness Checker, in order to detect errors - or guarantee that code is correct. +We have +a prototype + compile-time verification tool that detects and prevents these +errors. The goal of this project is to perform case studies to determine +how often programmers make signedness errors (our initial investigation +suggests that this is common!) and to improve the verification tool.

    - A good way to find projects that use unsigned arithmetic is to find a library that supports unsigned +The research questions are: +

    +
      +
    • How often do programmers make signedness errors? +
      • +
    • Is it feasible to automatically detect signedness errors? What techniques are useful? +
      • +
    • What is the false positive rate of a signedness verification tool — that is, false alarms from the tool? +
      • +
    • How much effort is required from a programmer? +
      • +
    + +

    +The methodology is: +

    +
      +
    • find open-source projects that use unsigned arithmetic +
      • +
    • run the verification tool on them +
      • +
    • for each tool warning, determine whether it is a defect in the + project or a limitation of the verification tool. For example, the Signedness + Checker does not currently handle boxed integers and BigInteger; these + haven't yet come up in case studies but could be worthwhile enhancements. + You may also need to write more annotations for libraries such as the + JDK. +
      • +
    • submit bug reports against the project, or improve the verification tool +
      • +
    + +

    + A good way to find projects that use unsigned arithmetic is to find a + library that supports unsigned arithmetic, then search on GitHub for projects that use that library.

    @@ -609,9 +687,9 @@

    Signed and unsigned numbers

    In Guava, see its unsigned support, such - as UnsignedBytes, - UnsignedLong, - UnsignedLongs, + as UnsignedBytes, + UnsignedLong, + UnsignedLongs, etc. Guava is already annotated; search for @Unsigned within https://github.com/typetools/guava. @@ -635,16 +713,6 @@

    Signed and unsigned numbers

  • Jake2
    • --> -

    - Your case studies will detect defects in open-source programs (thus - showing the value of the Signedness Checker), or they will show the need - for enhancements to the Signedness Checker. For example, the Signedness - Checker does not currently handle boxed integers and BigInteger; these - haven't yet come up in case studies but could be worthwhile enhancements. - You may also need to write more annotations for libraries such as the - JDK. -

    -

    Whole-program type inference

    @@ -950,13 +1018,30 @@

    Non-Empty Checker for precise handling of Queue.peek(

    -

    Custom tainting checking

    +

    Preventing injection vulnerabilities via specialized taint analysis

    + + + +

    +Many security vulnerabilities result from use of untrusted data without sanitizing it first. +Examples include SQL injection, cross-site scripting, command injection, and many more. +Other vulnerabilities result from leaking private data, such as credit card numbers. +

    + +

    +We have built a generalized taint analysis that can address any of these problems. However, because it is so general, it is not very useful. A user must customize it for each particular problem. +

    + +

    +The goal of this project is to make those customizations, and to evaluate their usefulness. +A specific research question is: "To what extent is a general taint analysis useful in eliminating a wide variety of security vulnerabilities? How much customization, if any, is needed?" +

    -The Checker Framework comes with +The generalized taint analysis is the Checker Framework's a Tainting - Checker that is so general that it is not good for much of anything. -In order to be useful in a particular domain, a user must customize it: + Checker. It requires customization to a particular domain: