From 0bfdaf81dddc58a1333b169b1789cd064a7986b7 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 1 Nov 2023 10:16:53 -0400 Subject: [PATCH 1/6] failing test --- .../OwningFieldStringComparison.java | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 checker/tests/resourceleak/OwningFieldStringComparison.java diff --git a/checker/tests/resourceleak/OwningFieldStringComparison.java b/checker/tests/resourceleak/OwningFieldStringComparison.java new file mode 100644 index 00000000000..92d9822f589 --- /dev/null +++ b/checker/tests/resourceleak/OwningFieldStringComparison.java @@ -0,0 +1,32 @@ +// Test case for + +import org.checkerframework.checker.mustcall.qual.*; +import org.checkerframework.checker.calledmethods.qual.*; +import java.net.Socket; + +@InheritableMustCall("a") +public class OwningFieldStringComparison { + + // :: error: required.method.not.called + @Owning Socket s; + + // important to the bug: the name of this field must contain + // the name of the owning socket + /* @NotOwning */ Socket s2; + + // Note this "destructor" closes the wrong socket + @EnsuresCalledMethods(value="this.s2", methods="close") + public void a() { + try { + this.s2.close(); + } catch(Exception e) { + + } finally { + try { + this.s2.close(); + } catch (Exception e) { + + } + } + } +} From 7becc3c19f12fa1bbdebafceec4f96b6e1dd290b Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 1 Nov 2023 10:17:26 -0400 Subject: [PATCH 2/6] add issue URL --- .../resourceleak/OwningFieldStringComparison.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/checker/tests/resourceleak/OwningFieldStringComparison.java b/checker/tests/resourceleak/OwningFieldStringComparison.java index 92d9822f589..c89fe62351f 100644 --- a/checker/tests/resourceleak/OwningFieldStringComparison.java +++ b/checker/tests/resourceleak/OwningFieldStringComparison.java @@ -1,8 +1,8 @@ -// Test case for +// Test case for https://github.com/typetools/checker-framework/issues/6276 -import org.checkerframework.checker.mustcall.qual.*; -import org.checkerframework.checker.calledmethods.qual.*; import java.net.Socket; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; @InheritableMustCall("a") public class OwningFieldStringComparison { @@ -15,11 +15,11 @@ public class OwningFieldStringComparison { /* @NotOwning */ Socket s2; // Note this "destructor" closes the wrong socket - @EnsuresCalledMethods(value="this.s2", methods="close") + @EnsuresCalledMethods(value = "this.s2", methods = "close") public void a() { try { this.s2.close(); - } catch(Exception e) { + } catch (Exception e) { } finally { try { From d997555cf69f58eb669d7d7433e1cda80b3e0104 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 1 Nov 2023 10:21:19 -0400 Subject: [PATCH 3/6] port Calvin's extraction of the relevant code into a method --- .../checker/resourceleak/ResourceLeakVisitor.java | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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 be36474ea9a..c19d35b3a17 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -429,7 +429,7 @@ private void checkOwningField(Element field) { rlTypeFactory.ensuresCalledMethodsValueElement, String.class); for (String value : values) { - if (value.contains(field.getSimpleName().toString())) { + if (expressionEqualsField(value, field)) { List methods = AnnotationUtils.getElementValueArray( ensuresCalledMethodsAnno, @@ -467,6 +467,18 @@ private void checkOwningField(Element field) { } } + /** + * Determine if the given expression e refers to this.field. + * + * @param e the expression + * @param field the field + * @return true if e refers to this.field + */ + private boolean expressionEqualsField(String e, Element field) { + // TODO: this is very wrong + return e.contains(field.getSimpleName().toString()); + } + /** * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. From 9860ce4a3849858c8debb22a5b63a44c641d48d2 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 1 Nov 2023 10:26:34 -0400 Subject: [PATCH 4/6] fix bug --- .../resourceleak/ResourceLeakVisitor.java | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) 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 c19d35b3a17..0383576492c 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -11,6 +11,7 @@ import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.Modifier; import javax.lang.model.element.TypeElement; +import javax.lang.model.element.VariableElement; import org.checkerframework.checker.calledmethods.CalledMethodsVisitor; import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; import org.checkerframework.checker.mustcall.CreatesMustCallForToJavaExpression; @@ -20,10 +21,13 @@ import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.dataflow.expression.FieldAccess; import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.framework.flow.CFAbstractStore; import org.checkerframework.framework.flow.CFAbstractValue; +import org.checkerframework.framework.util.JavaExpressionParseUtil; +import org.checkerframework.framework.util.StringToJavaExpression; import org.checkerframework.javacutil.AnnotationMirrorSet; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; @@ -355,7 +359,7 @@ private static AnnotationMirrorSet getEnsuresCalledMethodsAnnotations( @Override public Void visitVariable(VariableTree tree, Void p) { - Element varElement = TreeUtils.elementFromDeclaration(tree); + VariableElement varElement = TreeUtils.elementFromDeclaration(tree); if (varElement.getKind().isField() && !noLightweightOwnership @@ -375,7 +379,7 @@ public Void visitVariable(VariableTree tree, Void p) { * * @param field the declaration of the field to check */ - private void checkOwningField(Element field) { + private void checkOwningField(VariableElement field) { if (checker.shouldSkipUses(field)) { return; @@ -474,9 +478,13 @@ private void checkOwningField(Element field) { * @param field the field * @return true if e refers to this.field */ - private boolean expressionEqualsField(String e, Element field) { - // TODO: this is very wrong - return e.contains(field.getSimpleName().toString()); + private boolean expressionEqualsField(String e, VariableElement field) { + try { + JavaExpression je = StringToJavaExpression.atFieldDecl(e, field, this.checker); + return je instanceof FieldAccess && ((FieldAccess) je).getField().equals(field); + } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) { + return false; + } } /** From d01ffc61b489f84a77cb185b55c56d73d9064c5f Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 1 Nov 2023 10:30:53 -0400 Subject: [PATCH 5/6] add a note --- .../checker/resourceleak/ResourceLeakVisitor.java | 1 + 1 file changed, 1 insertion(+) 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 0383576492c..ccd756c2b8f 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -483,6 +483,7 @@ private boolean expressionEqualsField(String e, VariableElement field) { JavaExpression je = StringToJavaExpression.atFieldDecl(e, field, this.checker); return je instanceof FieldAccess && ((FieldAccess) je).getField().equals(field); } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) { + // The parsing error will be reported elsewhere, assuming e was derived from an annotation. return false; } } From c12e7585e3578cae55c9633734b6cfac42400ae8 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 1 Nov 2023 16:35:19 -0400 Subject: [PATCH 6/6] test case --- .../tests/resourceleak/SneakyDestructor.java | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 checker/tests/resourceleak/SneakyDestructor.java diff --git a/checker/tests/resourceleak/SneakyDestructor.java b/checker/tests/resourceleak/SneakyDestructor.java new file mode 100644 index 00000000000..586646ae600 --- /dev/null +++ b/checker/tests/resourceleak/SneakyDestructor.java @@ -0,0 +1,25 @@ +// Test case that shows that the fix for +// https://github.com/typetools/checker-framework/issues/6276 +// is not fooled by a must-call method that closes the owned field +// of another instance of the class. + +import java.io.*; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +@InheritableMustCall("close") +public class SneakyDestructor { + // :: error: required.method.not.called + private final @Owning Closeable resource; + + public SneakyDestructor(Closeable r) { + this.resource = r; + } + + // ... + + @EnsuresCalledMethods(value = "#1.resource", methods = "close") + public void close(SneakyDestructor other) throws IOException { + other.resource.close(); + } +}