Skip to content

Add RLC-only SideEffectFree stubs and tests #7609

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
iamsanjaymalakar wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Add RLC-only SideEffectFree stubs and tests #7609

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
77d5a28
Add RLC-only SideEffectFree stubs and tests
iamsanjaymalakar Apr 3, 2026
e1d5221
Merge branch 'master' into rlc-sideeffect-stub
iamsanjaymalakar Apr 3, 2026
22fac31
Add Logger stubs/tests for Log4j 1.x and 2.x
iamsanjaymalakar Apr 4, 2026
d72e909
Expand RLC Log4j side-effect-free stubs and tests
iamsanjaymalakar Apr 9, 2026
4abfe12
Merge branch 'master' into rlc-sideeffect-stub
iamsanjaymalakar Apr 9, 2026
5d5fd21
Fix Log4j Message import and throwable regression test
iamsanjaymalakar Apr 9, 2026
e8970a4
Addresses PR comments.
iamsanjaymalakar Apr 10, 2026
2806c28
Merge branch 'master' into rlc-sideeffect-stub
iamsanjaymalakar Apr 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .../src/main/java/org/checkerframework/checker/rlccalledmethods/RLCCalledMethodsChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
* CalledMethodsChecker} used as a subchecker in the ResourceLeakChecker, and never independently.
* Runs the MustCallChecker as a subchecker in order to share the CFG.
*/
@StubFiles("IOUtils.astub")
@StubFiles({"IOUtils.astub", "log4j.astub"})
public class RLCCalledMethodsChecker extends CalledMethodsChecker {

/** Creates a RLCCalledMethodsChecker. */
Expand Down
32 changes: 32 additions & 0 deletions checker/src/main/java/org/checkerframework/checker/rlccalledmethods/jdk.astub
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
package java.lang;

import java.io.PrintStream;
import java.io.PrintWriter;
import org.checkerframework.checker.lock.qual.GuardSatisfied;
import org.checkerframework.dataflow.qual.SideEffectFree;

public interface AutoCloseable {
@SideEffectFree
void close(@GuardSatisfied AutoCloseable this) throws Exception;
}

public class Throwable {
@SideEffectFree
public void printStackTrace();

@SideEffectFree
public void printStackTrace(PrintStream s);

@SideEffectFree
public void printStackTrace(PrintWriter s);
}

package java.io;

import org.checkerframework.checker.lock.qual.GuardSatisfied;
import org.checkerframework.dataflow.qual.SideEffectFree;

public interface Closeable extends AutoCloseable {
@SideEffectFree
public void close(@GuardSatisfied Closeable this) throws IOException;
}
212 changes: 212 additions & 0 deletions checker/src/main/java/org/checkerframework/checker/rlccalledmethods/log4j.astub
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,212 @@
import org.checkerframework.dataflow.qual.SideEffectFree;

// Log4j 1.x API stubs (package org.apache.log4j).
package org.apache.log4j;

class Category {
Copy link
Copy Markdown
Contributor

@kelloggm kelloggm Apr 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

https://logging.apache.org/log4j/1.x/apidocs/org/apache/log4j/Category.html says that this class has been deprecated since at least 2003. (!)

If you want to add log4j stubs, at least include the modern versions of the logging functions (i.e., in Logger) too.

Copy link
Copy Markdown
Member Author

@iamsanjaymalakar iamsanjaymalakar Apr 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, that makes sense. I removed the old Category-only coverage and updated the PR to use Logger instead. It now covers both Log4j 1.x and Log4j 2 with separate regression tests.

@SideEffectFree public void debug(Object message);
@SideEffectFree public void debug(Object message, Throwable t);
@SideEffectFree public void info(Object message);
@SideEffectFree public void info(Object message, Throwable t);
@SideEffectFree public void warn(Object message);
@SideEffectFree public void warn(Object message, Throwable t);
@SideEffectFree public void error(Object message);
@SideEffectFree public void error(Object message, Throwable t);
@SideEffectFree public void fatal(Object message);
@SideEffectFree public void fatal(Object message, Throwable t);
@SideEffectFree public void log(Priority priority, Object message);
@SideEffectFree public void log(Priority priority, Object message, Throwable t);
@SideEffectFree public void log(String callerFQCN, Priority level, Object message, Throwable t);
}

class Logger extends Category {
@SideEffectFree public void trace(Object message);
@SideEffectFree public void trace(Object message, Throwable t);
}
Comment on lines +6 to +25
Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot Apr 10, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🧹 Nitpick | 🔵 Trivial

Add regressions for the newly stubbed overload families.

The new tests only hit debug/info/warn/error plus one varargs/throwable path, but this stub file also adds trace, fatal, Category.log(...), and Log4j 2 Message overloads. Right now those extra signatures are unprotected, so a binding typo there would not be caught by checker/tests/resourceleak/sideeffect-free-stubs/Log4j1ObjectCalls.java:10-68 or checker/tests/resourceleak/sideeffect-free-stubs/Log4j2ObjectCalls.java:16-86.

Also applies to: 32-212

🤖 Prompt for AI Agents 
Verify each finding against the current code and only fix it if needed.

In
`@checker/src/main/java/org/checkerframework/checker/rlccalledmethods/log4j.astub`
around lines 6 - 25, The new astub adds extra untested overload families
(Category.log(...), trace(...), fatal(...), and Log4j2 Message overloads) so
regressions or binding typos there won't be caught; update the tests to exercise
these newly stubbed signatures (or add new test cases similar to
checker/tests/resourceleak/sideeffect-free-stubs/Log4j1ObjectCalls.java and
Log4j2ObjectCalls.java) to cover Category.log(Priority,...),
Category.log(String,Priority,...), Logger.trace(...), Category.fatal(...), and
any Message-based overloads so the checker validates the bindings for those
methods as well. Ensure the tests include both object and throwable/varargs
paths for each added overload family to detect binding mistakes.

Copy link
Copy Markdown
Member Author

@iamsanjaymalakar iamsanjaymalakar Apr 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried to cover representative samples from the stubs in the test cases, rather than adding test for every stub.

Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot Apr 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@iamsanjaymalakar, that's a perfectly reasonable approach — testing representative samples is a common and accepted practice for stub files, especially when the overloads follow a consistent pattern. As long as the core binding and annotation mechanism is exercised for each method family, exhaustive per-overload tests would add significant boilerplate without proportional benefit. Thanks for the explanation!


// Log4j 2.x API stubs (package org.apache.logging.log4j).
package org.apache.logging.log4j;

import org.apache.logging.log4j.message.Message;

interface Logger {
@SideEffectFree void trace(CharSequence message);
@SideEffectFree void trace(CharSequence message, Throwable throwable);
@SideEffectFree void trace(Object message);
@SideEffectFree void trace(Object message, Throwable throwable);
@SideEffectFree void trace(String message);
@SideEffectFree void trace(String message, Throwable throwable);
@SideEffectFree void trace(String message, Object p0);
@SideEffectFree void trace(String message, Object p0, Object p1);
@SideEffectFree void trace(String message, Object p0, Object p1, Object p2);
@SideEffectFree void trace(String message, Object p0, Object p1, Object p2, Object p3);
@SideEffectFree void trace(
String message, Object p0, Object p1, Object p2, Object p3, Object p4);
@SideEffectFree void trace(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
@SideEffectFree void trace(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6);
@SideEffectFree void trace(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7);
@SideEffectFree void trace(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8);
@SideEffectFree void trace(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8, Object p9);
@SideEffectFree void trace(String message, Object... params);
@SideEffectFree void trace(Message message);
@SideEffectFree void trace(Message message, Throwable throwable);

@SideEffectFree void debug(CharSequence message);
@SideEffectFree void debug(CharSequence message, Throwable throwable);
@SideEffectFree void debug(Object message);
@SideEffectFree void debug(Object message, Throwable throwable);
@SideEffectFree void debug(String message);
@SideEffectFree void debug(String message, Throwable throwable);
@SideEffectFree void debug(String message, Object p0);
@SideEffectFree void debug(String message, Object p0, Object p1);
@SideEffectFree void debug(String message, Object p0, Object p1, Object p2);
@SideEffectFree void debug(String message, Object p0, Object p1, Object p2, Object p3);
@SideEffectFree void debug(
String message, Object p0, Object p1, Object p2, Object p3, Object p4);
@SideEffectFree void debug(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
@SideEffectFree void debug(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6);
@SideEffectFree void debug(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7);
@SideEffectFree void debug(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8);
@SideEffectFree void debug(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8, Object p9);
@SideEffectFree void debug(String message, Object... params);
@SideEffectFree void debug(Message message);
@SideEffectFree void debug(Message message, Throwable throwable);

@SideEffectFree void info(CharSequence message);
@SideEffectFree void info(CharSequence message, Throwable throwable);
@SideEffectFree void info(Object message);
@SideEffectFree void info(Object message, Throwable throwable);
@SideEffectFree void info(String message);
@SideEffectFree void info(String message, Throwable throwable);
@SideEffectFree void info(String message, Object p0);
@SideEffectFree void info(String message, Object p0, Object p1);
@SideEffectFree void info(String message, Object p0, Object p1, Object p2);
@SideEffectFree void info(String message, Object p0, Object p1, Object p2, Object p3);
@SideEffectFree void info(
String message, Object p0, Object p1, Object p2, Object p3, Object p4);
@SideEffectFree void info(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
@SideEffectFree void info(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6);
@SideEffectFree void info(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7);
@SideEffectFree void info(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8);
@SideEffectFree void info(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8, Object p9);
@SideEffectFree void info(String message, Object... params);
@SideEffectFree void info(Message message);
@SideEffectFree void info(Message message, Throwable throwable);

@SideEffectFree void warn(CharSequence message);
@SideEffectFree void warn(CharSequence message, Throwable throwable);
@SideEffectFree void warn(Object message);
@SideEffectFree void warn(Object message, Throwable throwable);
@SideEffectFree void warn(String message);
@SideEffectFree void warn(String message, Throwable throwable);
@SideEffectFree void warn(String message, Object p0);
@SideEffectFree void warn(String message, Object p0, Object p1);
@SideEffectFree void warn(String message, Object p0, Object p1, Object p2);
@SideEffectFree void warn(String message, Object p0, Object p1, Object p2, Object p3);
@SideEffectFree void warn(
String message, Object p0, Object p1, Object p2, Object p3, Object p4);
@SideEffectFree void warn(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
@SideEffectFree void warn(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6);
@SideEffectFree void warn(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7);
@SideEffectFree void warn(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8);
@SideEffectFree void warn(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8, Object p9);
@SideEffectFree void warn(String message, Object... params);
@SideEffectFree void warn(Message message);
@SideEffectFree void warn(Message message, Throwable throwable);

@SideEffectFree void error(CharSequence message);
@SideEffectFree void error(CharSequence message, Throwable throwable);
@SideEffectFree void error(Object message);
@SideEffectFree void error(Object message, Throwable throwable);
@SideEffectFree void error(String message);
@SideEffectFree void error(String message, Throwable throwable);
@SideEffectFree void error(String message, Object p0);
@SideEffectFree void error(String message, Object p0, Object p1);
@SideEffectFree void error(String message, Object p0, Object p1, Object p2);
@SideEffectFree void error(String message, Object p0, Object p1, Object p2, Object p3);
@SideEffectFree void error(
String message, Object p0, Object p1, Object p2, Object p3, Object p4);
@SideEffectFree void error(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
@SideEffectFree void error(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6);
@SideEffectFree void error(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7);
@SideEffectFree void error(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8);
@SideEffectFree void error(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8, Object p9);
@SideEffectFree void error(String message, Object... params);
@SideEffectFree void error(Message message);
@SideEffectFree void error(Message message, Throwable throwable);

@SideEffectFree void fatal(CharSequence message);
@SideEffectFree void fatal(CharSequence message, Throwable throwable);
@SideEffectFree void fatal(Object message);
@SideEffectFree void fatal(Object message, Throwable throwable);
@SideEffectFree void fatal(String message);
@SideEffectFree void fatal(String message, Throwable throwable);
@SideEffectFree void fatal(String message, Object p0);
@SideEffectFree void fatal(String message, Object p0, Object p1);
@SideEffectFree void fatal(String message, Object p0, Object p1, Object p2);
@SideEffectFree void fatal(String message, Object p0, Object p1, Object p2, Object p3);
@SideEffectFree void fatal(
String message, Object p0, Object p1, Object p2, Object p3, Object p4);
@SideEffectFree void fatal(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5);
@SideEffectFree void fatal(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6);
@SideEffectFree void fatal(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7);
@SideEffectFree void fatal(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8);
@SideEffectFree void fatal(
String message, Object p0, Object p1, Object p2, Object p3, Object p4, Object p5,
Object p6, Object p7, Object p8, Object p9);
@SideEffectFree void fatal(String message, Object... params);
@SideEffectFree void fatal(Message message);
@SideEffectFree void fatal(Message message, Throwable throwable);
}
7 changes: 0 additions & 7 deletions checker/tests/resourceleak/TwoResourcesECM.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,19 +12,12 @@
class TwoResourcesECM {
@Owning Socket s1, s2;

// The contracts.postcondition error below is thrown because s1 is not final,
// and therefore might theoretically be side-effected by the call to s2.close()
// even on the non-exceptional path. See ReplicaInputStreams.java for a variant
// of this test where such an error is not issued. Because this method can leak
// along both regular and exceptional exits, both errors are issued.
//
// The contracts.exceptional.postcondition error is thrown because destructors
// have to close their resources even on exception. If s1.close() throws an
// exception, then s2.close() will not be called.
@EnsuresCalledMethods(
value = {"this.s1", "this.s2"},
methods = {"close"})
// :: error: [contracts.postcondition]
// :: error: [contracts.exceptional.postcondition]
public void dispose() throws IOException {
s1.close();
Expand Down
30 changes: 30 additions & 0 deletions checker/tests/resourceleak/sideeffect-free-stubs/AutoCloseableClose.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
// RLC uses Called Methods facts to remember that a resource has already been closed.
// This test checks that the RLC-specific SideEffectFree stub for AutoCloseable.close()
// preserves those facts across another close call in the same destructor, rather than
// conservatively forgetting them after the first invocation.

import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
import org.checkerframework.checker.mustcall.qual.Owning;

final class TestAutoCloseable implements AutoCloseable {
@Override
public void close() {}
}

class AutoCloseableClose implements AutoCloseable {
private @Owning AutoCloseable first = new TestAutoCloseable();
private @Owning AutoCloseable second = new TestAutoCloseable();

@Override
@EnsuresCalledMethods(
value = {"this.first", "this.second"},
methods = "close")
public void close() {
try {
first.close();
second.close();
} catch (Exception e) {
throw new AssertionError(e);
}
}
}
34 changes: 34 additions & 0 deletions checker/tests/resourceleak/sideeffect-free-stubs/CloseableClose.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
// RLC uses Called Methods facts to remember that a resource has already been closed.
// This test checks that the RLC-specific SideEffectFree stub for Closeable.close()
// preserves those facts across another close call in the same destructor, rather than
// conservatively forgetting them after the first invocation.

import java.io.Closeable;
import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
import org.checkerframework.checker.mustcall.qual.Owning;

final class TestCloseable implements Closeable {
@Override
public void close() {}
}

class CloseableClose implements Closeable {
private @Owning Closeable first = new TestCloseable();
private @Owning Closeable second = new TestCloseable();

@Override
@EnsuresCalledMethods(
value = {"this.first", "this.second"},
methods = "close")
public void close() {
try {
try {
first.close();
} catch (Exception ignored) {
}
second.close();
} catch (Exception e) {
throw new AssertionError(e);
}
}
}
Loading
Loading