Skip to content

Commit

Permalink
resolve soundness bug in RLC, fix typetools#5453
Browse files Browse the repository at this point in the history
  • Loading branch information
kelloggm committed Dec 20, 2022
1 parent ff50d49 commit ef30ddb
Show file tree
Hide file tree
Showing 5 changed files with 42 additions and 4 deletions.
Expand Up @@ -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(
Expand All @@ -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<VariableElement> 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.
Expand Down
Expand Up @@ -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;
Expand Down
4 changes: 3 additions & 1 deletion 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.*;

Expand All @@ -9,6 +11,7 @@ class TwoOwningMCATest {
@Owning private final Foo f2;

@MustCallAlias
// :: error: mustcallalias.out.of.scope
TwoOwningMCATest(@MustCallAlias Foo g) {
this.f2 = g;
}
Expand All @@ -29,7 +32,6 @@ void a() {}
}

public static void test(Foo f) {
// :: error: required.method.not.called
TwoOwningMCATest t = new TwoOwningMCATest(f);
f.a();
}
Expand Down
1 change: 1 addition & 0 deletions checker/tests/resourceleak/TwoSocketContainer.java
Expand Up @@ -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;
Expand Down
3 changes: 2 additions & 1 deletion docs/manual/resource-leak-checker.tex
Expand Up @@ -289,7 +289,8 @@
\begin{enumerate}
\item \<p> is passed to another method or constructor (including \<super>) in a
\<@MustCallAlias> position, and \<m> returns that method's result, or
\item \<p> is stored in an \<@Owning> field of the enclosing class.
\item \<p> 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}


Expand Down

0 comments on commit ef30ddb

Please sign in to comment.