From ef30ddb127bdfd167ddd06f6c6abc7d513050880 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Tue, 20 Dec 2022 12:56:27 -0500 Subject: [PATCH] resolve soundness bug in RLC, fix #5453 --- .../MustCallConsistencyAnalyzer.java | 35 +++++++++++++++++-- ...MultipleMethodParamsMustCallAliasTest.java | 3 ++ .../tests/resourceleak/TwoOwningMCATest.java | 4 ++- .../resourceleak/TwoSocketContainer.java | 1 + docs/manual/resource-leak-checker.tex | 3 +- 5 files changed, 42 insertions(+), 4 deletions(-) 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 df152ad5fc4..4fc175813b3 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -1075,9 +1075,16 @@ 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. + // 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( @@ -1097,6 +1104,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.getDeclAnnotation(field, Owning.class) != null) { + 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. diff --git a/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java b/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java index 153a10698d8..66c6e17ae02 100644 --- a/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java +++ b/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java @@ -70,6 +70,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 index a79391ef201..43870bd7a96 100644 --- a/checker/tests/resourceleak/TwoOwningMCATest.java +++ b/checker/tests/resourceleak/TwoOwningMCATest.java @@ -1,3 +1,5 @@ +// Test case for issue 5453: https://github.com/typetools/checker-framework/issues/5453 + import org.checkerframework.checker.mustcall.qual.*; import org.checkerframework.checker.calledmethods.qual.*; @@ -9,6 +11,7 @@ class TwoOwningMCATest { @Owning private final Foo f2; @MustCallAlias + // :: error: mustcallalias.out.of.scope TwoOwningMCATest(@MustCallAlias Foo g) { this.f2 = g; } @@ -29,7 +32,6 @@ void a() {} } public static void test(Foo f) { - // :: error: required.method.not.called TwoOwningMCATest t = new TwoOwningMCATest(f); f.a(); } diff --git a/checker/tests/resourceleak/TwoSocketContainer.java b/checker/tests/resourceleak/TwoSocketContainer.java index 0e313888377..0c3ad3c9c0d 100644 --- a/checker/tests/resourceleak/TwoSocketContainer.java +++ b/checker/tests/resourceleak/TwoSocketContainer.java @@ -9,6 +9,7 @@ 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; diff --git a/docs/manual/resource-leak-checker.tex b/docs/manual/resource-leak-checker.tex index b70da0af1d8..007b46a8b1a 100644 --- a/docs/manual/resource-leak-checker.tex +++ b/docs/manual/resource-leak-checker.tex @@ -289,7 +289,8 @@ \begin{enumerate} \item \

is passed to another method or constructor (including \) in a \<@MustCallAlias> position, and \ returns that method's result, or -\item \

is stored in an \<@Owning> field of the enclosing class. +\item \

is stored in the only \<@Owning> field of the enclosing class (a class with more than one + \<@Owning> field cannot have a resource alias relationship). \end{enumerate}