From c456d5407c2a835a3e84fe613f33e34adcae8317 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 12 Aug 2026 08:36:12 -0700 Subject: [PATCH 1/6] Retain type refinements across calls to @SideEffectsOnly methods After a call to a method annotated @SideEffectsOnly, discard only what the annotation's expressions could have changed, rather than every refinement. A checker discards what it knows about an expression `e` if `e` contains a listed expression, and also if `e` contains a call through whose receiver or arguments a listed expression is reachable: a @Pure method's result depends on state that no annotation declares, so approximate that state by what is reachable from the call's receiver and arguments. If a listed expression cannot be represented at the call site -- because viewpoint adaptation yields an Unknown, or because it cannot be parsed -- then return null, which makes the caller discard every refinement. Omitting the expression instead would treat the method as side-effecting less than it was declared to. Co-Authored-By: Claude Opus 5 --- .../test/junit/OptionalSideEffectsTest.java | 28 ++++ .../test/junit/SideEffectsOnlyTest.java | 25 ++++ checker/tests/nullness/SetIteratorTest.java | 2 - .../tests/nullness/SideEffectsOnlySuper.java | 33 +++++ .../OptionalSideEffectsLambda.java | 44 ++++++ .../OptionalSideEffectsPrecondition.java | 68 +++++++++ .../PureMethodCallRefinement.java | 101 ++++++++++++++ .../sideeffectsonly/SideEffectsMultiple.java | 24 ++++ .../sideeffectsonly/SideEffectsOnlyField.java | 30 ++++ .../sideeffectsonly/SideEffectsOnlyTest1.java | 34 +++++ .../sideeffectsonly/SideEffectsOnlyTest2.java | 26 ++++ .../sideeffectsonly/SideEffectsTest1.java | 22 +++ .../sideeffectsonly/StaticIteratorSE.java | 28 ++++ .../UnrepresentableArgument.java | 43 ++++++ docs/manual/advanced-features.tex | 36 ++++- docs/manual/called-methods-checker.tex | 8 +- docs/manual/introduction.tex | 17 ++- docs/manual/nullness-checker.tex | 3 +- docs/manual/purity-checker.tex | 12 +- docs/manual/troubleshooting.tex | 1 + .../common/basetype/BaseTypeVisitor.java | 5 + .../framework/flow/CFAbstractAnalysis.java | 105 ++++++++++++++ .../framework/flow/CFAbstractStore.java | 132 ++++++++++++++++-- .../framework/flow/CFAbstractTransfer.java | 2 + .../framework/type/AnnotatedTypeFactory.java | 25 ++++ 25 files changed, 832 insertions(+), 22 deletions(-) create mode 100644 checker/src/test/java/org/checkerframework/checker/test/junit/OptionalSideEffectsTest.java create mode 100644 checker/src/test/java/org/checkerframework/checker/test/junit/SideEffectsOnlyTest.java create mode 100644 checker/tests/nullness/SideEffectsOnlySuper.java create mode 100644 checker/tests/optional-side-effects/OptionalSideEffectsLambda.java create mode 100644 checker/tests/optional-side-effects/OptionalSideEffectsPrecondition.java create mode 100644 checker/tests/sideeffectsonly/PureMethodCallRefinement.java create mode 100644 checker/tests/sideeffectsonly/SideEffectsMultiple.java create mode 100644 checker/tests/sideeffectsonly/SideEffectsOnlyField.java create mode 100644 checker/tests/sideeffectsonly/SideEffectsOnlyTest1.java create mode 100644 checker/tests/sideeffectsonly/SideEffectsOnlyTest2.java create mode 100644 checker/tests/sideeffectsonly/SideEffectsTest1.java create mode 100644 checker/tests/sideeffectsonly/StaticIteratorSE.java create mode 100644 checker/tests/sideeffectsonly/UnrepresentableArgument.java diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalSideEffectsTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalSideEffectsTest.java new file mode 100644 index 000000000000..1d52528336a9 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalSideEffectsTest.java @@ -0,0 +1,28 @@ +package org.checkerframework.checker.test.junit; + +import java.io.File; +import java.util.List; +import org.checkerframework.checker.optional.OptionalChecker; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +/** + * Tests that the Optional Checker retains type refinements across a call to a method that is + * annotated with {@code @SideEffectsOnly}. + */ +public class OptionalSideEffectsTest extends CheckerFrameworkPerDirectoryTest { + + /** + * Create an OptionalSideEffectsTest. + * + * @param testFiles the files containing test code, which will be type-checked + */ + public OptionalSideEffectsTest(List testFiles) { + super(testFiles, OptionalChecker.class, "optional-side-effects", "-AcheckPurityAnnotations"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"optional-side-effects"}; + } +} diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/SideEffectsOnlyTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/SideEffectsOnlyTest.java new file mode 100644 index 000000000000..fcccca136830 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/SideEffectsOnlyTest.java @@ -0,0 +1,25 @@ +package org.checkerframework.checker.test.junit; + +import java.io.File; +import java.util.List; +import org.checkerframework.checker.tainting.TaintingChecker; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +/** Tests {@code @SideEffectsOnly} annotations that are written in the code under test. */ +public class SideEffectsOnlyTest extends CheckerFrameworkPerDirectoryTest { + + /** + * Create a SideEffectsOnlyTest. + * + * @param testFiles the files containing test code, which will be type-checked + */ + public SideEffectsOnlyTest(List testFiles) { + super(testFiles, TaintingChecker.class, "sideeffectsonly", "-AcheckPurityAnnotations"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"sideeffectsonly"}; + } +} diff --git a/checker/tests/nullness/SetIteratorTest.java b/checker/tests/nullness/SetIteratorTest.java index f2801d453ae6..7d6dcdac1a02 100644 --- a/checker/tests/nullness/SetIteratorTest.java +++ b/checker/tests/nullness/SetIteratorTest.java @@ -26,7 +26,6 @@ public String listChildren(String parentNode) { if (edges.get(parentNode) != null) { for (String childNode : edges.get(parentNode).keySet()) { - // :: error: [dereference.of.nullable] edges.get(parentNode).toString(); for (String childNodeEdgeX : edges.get(parentNode).get(childNode)) { childrenString += " " + childNode + "(" + childNodeEdgeX + ")"; @@ -42,7 +41,6 @@ public void listChildren2(String parentNode) { Iterator itor = edges.get(parentNode).keySet().iterator(); edges.get(parentNode).toString(); String s = itor.next(); - // :: error: [dereference.of.nullable] edges.get(parentNode).toString(); } } diff --git a/checker/tests/nullness/SideEffectsOnlySuper.java b/checker/tests/nullness/SideEffectsOnlySuper.java new file mode 100644 index 000000000000..e0e292d1ba92 --- /dev/null +++ b/checker/tests/nullness/SideEffectsOnlySuper.java @@ -0,0 +1,33 @@ +// A `@SideEffectsOnly("this")` method that is called via `super` side-effects the object that the +// caller denotes as `this`, so refinements of that object's fields must be discarded. + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public class SideEffectsOnlySuper { + + static class Super { + @Nullable Object f; + + @SideEffectsOnly("this") + void clear() { + f = null; + } + } + + static class Sub extends Super { + void viaSuper() { + f = new Object(); + super.clear(); + // :: error: (dereference.of.nullable) + f.toString(); + } + + void viaThis() { + f = new Object(); + this.clear(); + // :: error: (dereference.of.nullable) + f.toString(); + } + } +} diff --git a/checker/tests/optional-side-effects/OptionalSideEffectsLambda.java b/checker/tests/optional-side-effects/OptionalSideEffectsLambda.java new file mode 100644 index 000000000000..19cd68d28fdc --- /dev/null +++ b/checker/tests/optional-side-effects/OptionalSideEffectsLambda.java @@ -0,0 +1,44 @@ +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.optional.qual.RequiresPresent; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; + +class OptionalSideEffectsLambda { + + void fooWithEnhancedFor(OptContainer container, List strs) { + if (!container.getOptStr().isPresent()) { + return; + } + for (String s : strs) { + // This should verify because the call to Iterator.next only side effects the iterator. + bar(container); + } + } + + void fooWithForEach(OptContainer container, List strs) { + if (!container.getOptStr().isPresent()) { + return; + } + strs.forEach(s -> bar(container)); + } + + @RequiresPresent("#1.getOptStr()") + @SideEffectFree + void bar(OptContainer container) {} +} + +class OptContainer { + + @SuppressWarnings("optional:field") + private Optional optStr; + + OptContainer(String s) { + this.optStr = Optional.ofNullable(s); + } + + @Pure + public Optional getOptStr() { + return this.optStr; + } +} diff --git a/checker/tests/optional-side-effects/OptionalSideEffectsPrecondition.java b/checker/tests/optional-side-effects/OptionalSideEffectsPrecondition.java new file mode 100644 index 000000000000..3c70fcc27476 --- /dev/null +++ b/checker/tests/optional-side-effects/OptionalSideEffectsPrecondition.java @@ -0,0 +1,68 @@ +import java.util.ArrayList; +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.optional.qual.RequiresPresent; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +class OptionalSideEffectsPrecondition { + + void test1(OptionalContainer optContainer) { + if (!optContainer.getOpt().isPresent()) { + return; + } + List strs = new ArrayList<>(); + methodA(optContainer, strs); + optContainer.getOpt().get(); // OK + bar(optContainer); // OK + } + + void test2(OptionalContainer optContainer) { + if (!optContainer.getOpt().isPresent()) { + return; + } + List strs = new ArrayList<>(); + methodB(optContainer, strs); + + // :: error: (contracts.precondition) + bar(optContainer); + } + + void test3(OptionalContainer optContainer) { + if (!optContainer.getOpt().isPresent()) { + return; + } + List strs = new ArrayList<>(); + havoc(optContainer, strs); + + // :: error: (contracts.precondition) + bar(optContainer); + } + + @RequiresPresent("#1.getOpt()") + void bar(OptionalContainer optContainer) {} + + @SideEffectsOnly("#2") + void methodA(OptionalContainer optContainer, Object param) {} + + @SideEffectsOnly({"#1", "#2"}) + void methodB(OptionalContainer optContainer, Object param) {} + + void havoc(OptionalContainer optContainer, Object param) {} + + class OptionalContainer { + + @SuppressWarnings("optional:field") + private Optional opt; + + @SuppressWarnings("optional:parameter") + OptionalContainer(Optional opt) { + this.opt = opt; + } + + @Pure // Not required if running under -AassumePureGetters + public Optional getOpt() { + return this.opt; + } + } +} diff --git a/checker/tests/sideeffectsonly/PureMethodCallRefinement.java b/checker/tests/sideeffectsonly/PureMethodCallRefinement.java new file mode 100644 index 000000000000..db4267ac5369 --- /dev/null +++ b/checker/tests/sideeffectsonly/PureMethodCallRefinement.java @@ -0,0 +1,101 @@ +// A `@SideEffectsOnly` annotation says what the callee writes, but says nothing about what a +// `@Pure` method reads. A refinement of a `@Pure` method call must therefore be discarded when +// a listed expression is reached through the call's receiver or one of its arguments, even though +// the call is not built out of the listed expression. + +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class PureMethodCallRefinement { + + @Tainted Object f; + + @Pure + Object getF() { + return f; + } + + @EnsuresQualifier(expression = "#1.getF()", qualifier = Untainted.class) + // :: error: contracts.postcondition + void makeUntainted(PureMethodCallRefinement o) {} + + @SideEffectsOnly("#1.f") + void modifyField(PureMethodCallRefinement o) {} + + @SideEffectsOnly("this") + void modifyThis() {} + + void test(PureMethodCallRefinement o) { + makeUntainted(o); + // `modifyField` may write `o.f`, which `getF()` returns. The annotation does not mention + // `o.getF()`, but that expression is not a subexpression of `o.f`, so a rule based only on + // subexpressions would wrongly retain the refinement. + modifyField(o); + // :: error: assignment + @Untainted Object y = o.getF(); + } + + void testNestedCall(PureMethodCallRefinement o) { + makeUntaintedNested(o); + // The stored expression's receiver is itself a call, so the search for the modified location + // must recur through it. + modifyField(o); + // :: error: assignment + @Untainted Object y = o.getSelf().getF(); + } + + @Pure + PureMethodCallRefinement getSelf() { + return this; + } + + @EnsuresQualifier(expression = "#1.getSelf().getF()", qualifier = Untainted.class) + // :: error: contracts.postcondition + void makeUntaintedNested(PureMethodCallRefinement o) {} + + @Tainted Object g; + + @Tainted Object @Tainted [] arr = new @Tainted Object[10]; + + @Pure + Object @Tainted [] getArr() { + return arr; + } + + @EnsuresQualifier(expression = "#1.getSelf().g", qualifier = Untainted.class) + // :: error: contracts.postcondition + void makeUntaintedFieldOfCall(PureMethodCallRefinement o) {} + + @EnsuresQualifier(expression = "#1.getArr()[0]", qualifier = Untainted.class) + // :: error: contracts.postcondition + void makeUntaintedElementOfCall(PureMethodCallRefinement o) {} + + void testFieldOfCall(PureMethodCallRefinement o) { + makeUntaintedFieldOfCall(o); + // The stored expression is a field access, not a call, but its receiver is a call, so the + // search for the modified location must recur through the receiver. + modifyField(o); + // :: error: assignment + @Untainted Object y = o.getSelf().g; + } + + void testElementOfCall(PureMethodCallRefinement o) { + makeUntaintedElementOfCall(o); + // The stored expression is an array access whose array is a call. + modifyField(o); + // :: error: assignment + @Untainted Object y = o.getArr()[0]; + } + + void testUnrelatedReceiver(PureMethodCallRefinement o) { + makeUntainted(o); + // `modifyThis` modifies `this`, which is unrelated to `o` and to `o`'s fields. Like every + // other use of `@SideEffectsOnly` for type refinement, this is unsound if `this` and `o` are + // aliases, or if `o` is reachable from `this`. + modifyThis(); + @Untainted Object y = o.getF(); + } +} diff --git a/checker/tests/sideeffectsonly/SideEffectsMultiple.java b/checker/tests/sideeffectsonly/SideEffectsMultiple.java new file mode 100644 index 000000000000..1d9ab9812152 --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsMultiple.java @@ -0,0 +1,24 @@ +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsMultiple { + @Tainted Object x; + + void test() { + method(x); + method1(x); + // :: error: [argument] + method2(x); + } + + @EnsuresQualifier(expression = "#1", qualifier = Untainted.class) + // :: error: contracts.postcondition + void method(Object x) {} + + @SideEffectsOnly({"this", "#1"}) + void method1(@Untainted Object y) {} + + void method2(@Untainted Object x) {} +} diff --git a/checker/tests/sideeffectsonly/SideEffectsOnlyField.java b/checker/tests/sideeffectsonly/SideEffectsOnlyField.java new file mode 100644 index 000000000000..bb110ca6b3b1 --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsOnlyField.java @@ -0,0 +1,30 @@ +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsOnlyField { + @Tainted Object a; + @Tainted Object b; + + static void test(SideEffectsOnlyField arg) { + method(arg); + method3(arg); + // :: error: argument + method2(arg.a); + method2(arg.b); + } + + @EnsuresQualifier( + expression = {"#1.a", "#1.b"}, + qualifier = Untainted.class) + // :: error: contracts.postcondition + static void method(SideEffectsOnlyField x) {} + + @SideEffectsOnly("#1.a") + static void method3(SideEffectsOnlyField z) {} + + @SideEffectFree + static void method2(@Untainted Object x) {} +} diff --git a/checker/tests/sideeffectsonly/SideEffectsOnlyTest1.java b/checker/tests/sideeffectsonly/SideEffectsOnlyTest1.java new file mode 100644 index 000000000000..10304f2120c1 --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsOnlyTest1.java @@ -0,0 +1,34 @@ +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsOnlyTest1 { + @Tainted Object x; + + void test0() { + method(x); + method1(x); + // The field "this.x" may be modified by a method that side-effects "this". + // :: error: assignment + @Untainted Object y = x; + } + + void test() { + method(x); + method2(x); + // `method2()` is specified to side-effect its argument. + // :: error: assignment + @Untainted Object y = x; + } + + @EnsuresQualifier(expression = "#1", qualifier = Untainted.class) + // :: error: contracts.postcondition + void method(Object x) {} + + @SideEffectsOnly({"this"}) + void method1(@Untainted Object x) {} + + @SideEffectsOnly({"#1"}) + void method2(@Untainted Object x) {} +} diff --git a/checker/tests/sideeffectsonly/SideEffectsOnlyTest2.java b/checker/tests/sideeffectsonly/SideEffectsOnlyTest2.java new file mode 100644 index 000000000000..ff7dcaad7f2c --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsOnlyTest2.java @@ -0,0 +1,26 @@ +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsOnlyTest2 { + @Tainted Object w; + @Tainted Object x; + + void test0() { + method(x); + method1(x); + method3(x); + @Untainted Object y = x; + } + + @EnsuresQualifier(expression = "#1", qualifier = Untainted.class) + // :: error: contracts.postcondition + void method(Object x) {} + + @SideEffectsOnly({"w"}) + void method1(@Untainted Object x) {} + + @SideEffectsOnly({"w"}) + void method3(@Untainted Object z) {} +} diff --git a/checker/tests/sideeffectsonly/SideEffectsTest1.java b/checker/tests/sideeffectsonly/SideEffectsTest1.java new file mode 100644 index 000000000000..978bf45b1916 --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsTest1.java @@ -0,0 +1,22 @@ +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsTest1 { + @Tainted Object x; + + void test() { + method(x); + method1(x); + // :: error: argument + method2(x); + } + + @EnsuresQualifier(expression = "#1", qualifier = Untainted.class) + // :: error: contracts.postcondition + void method(Object x) {} + + void method1(@Untainted Object x) {} + + void method2(@Untainted Object x) {} +} diff --git a/checker/tests/sideeffectsonly/StaticIteratorSE.java b/checker/tests/sideeffectsonly/StaticIteratorSE.java new file mode 100644 index 000000000000..047b3e576d6a --- /dev/null +++ b/checker/tests/sideeffectsonly/StaticIteratorSE.java @@ -0,0 +1,28 @@ +import java.util.Enumeration; +import java.util.Iterator; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public final class StaticIteratorSE implements Iterator { + Enumeration e; + + public StaticIteratorSE(Enumeration e) { + this.e = e; + } + + public boolean hasNext() { + return e.hasMoreElements(); + } + + @SideEffectsOnly("this") + public T next() { + // `Enumeration.nextElement` is `@SideEffectsOnly("this")` in the annotated JDK, which this + // call site adapts to `this.e`. That is reached through `this`, which this method's own + // annotation lists. + return e.nextElement(); + } + + @SideEffectsOnly("this") + public void remove() { + throw new UnsupportedOperationException(); + } +} diff --git a/checker/tests/sideeffectsonly/UnrepresentableArgument.java b/checker/tests/sideeffectsonly/UnrepresentableArgument.java new file mode 100644 index 000000000000..8e788521141b --- /dev/null +++ b/checker/tests/sideeffectsonly/UnrepresentableArgument.java @@ -0,0 +1,43 @@ +// A callee's `@SideEffectsOnly` annotation cannot always be written at a call site: view +// adaptation may yield an expression that the checker cannot represent, as it does when an argument +// is a conditional expression. Then the checker does not know what the call modifies, so it +// discards every refinement. + +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class UnrepresentableArgument { + + @Tainted Object a; + @Tainted Object b; + + @EnsuresQualifier(expression = "#1", qualifier = Untainted.class) + // :: error: contracts.postcondition + void makeUntainted(Object o) {} + + @SideEffectsOnly("#1") + void modifies(Object o) {} + + void representableArgument() { + makeUntainted(a); + modifies(a); + // :: error: assignment + @Untainted Object y = a; + } + + void unrepresentableArgument(boolean cond) { + makeUntainted(a); + modifies(cond ? a : b); + // :: error: assignment + @Untainted Object y = a; + } + + void otherArgumentIsModified() { + makeUntainted(a); + // The call modifies only `this.b`, so the refinement of `this.a` survives. + modifies(b); + @Untainted Object y = a; + } +} diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex index 33f24dc35fee..0b1ddc0bc797 100644 --- a/docs/manual/advanced-features.tex +++ b/docs/manual/advanced-features.tex @@ -1064,6 +1064,25 @@ The \refqualclass{dataflow/qual}{SideEffectFree} annotation indicates that the method has no side effects, so calling it does not invalidate any dataflow facts. +\iffalse +Alternately, the \refqualclass{dataflow/qual}{SideEffectsOnly} +annotation specifies all the expressions that the method might side-effect. + +After a call to a \<@SideEffectsOnly> method, a checker discards what it knows about an +expression \ if \ contains a listed expression: modifying \ can change \, +but not the other way around. If \ is a call to a \<@Pure> method, then a checker also +discards what it knows when a listed expression is reached through the call's receiver or +one of its arguments. A \<@Pure> method's result depends on the state that the method +reads, which no annotation declares, so a checker approximates that state by what is +reachable from the call's receiver and arguments. For example, a call to a +\<@SideEffectsOnly("x.f")> method discards what is known about \, but not what is +known about \. + +Each listed expression is viewpoint-adapted to the call site. If the adaptation yields an +expression that the checker cannot represent --- as when an argument is a conditional +expression or a cast --- then the checker does not know what the call modifies, so it +discards every refinement, exactly as for a method with no side-effect annotation. +\fi Calling a method twice might have different results, so facts known about one call cannot be relied upon at another call. @@ -1103,7 +1122,10 @@ } \end{Verbatim} -There are three ways to express that \ does not set +There are three +%% With @SideEffectsOnly: +% four +ways to express that \ does not set \ to \, and thus to prevent the Nullness Checker from issuing a warning about the call \. @@ -1122,6 +1144,17 @@ the second occurrence of \code{myField} has the same (non-null) value as the one in the test. +\iffalse +\item + If \ has side effects, but they do not affect \, + declare the method as \refqualclass{dataflow/qual}{SideEffectsOnly}: + +\begin{Verbatim} + @SideEffectsOnly({"someOtherVariable1", "someOtherVariable2"}) + int computeValue() { ... } +\end{Verbatim} +\fi + \item If no method resets \ to \ after it has been initialized to a non-null value (even if a method has some other side effect), @@ -1277,6 +1310,7 @@ \item \refqualclass{framework/qual}{RequiresQualifier} \item \refqualclass{framework/qual}{EnsuresQualifier} \item \refqualclass{framework/qual}{EnsuresQualifierIf} +\item \refqualclass{dataflow/qual}{SideEffectsOnly} \item \refqualclass{checker/nullness/qual}{RequiresNonNull} \item \refqualclass{checker/nullness/qual}{EnsuresNonNull} \item \refqualclass{checker/nullness/qual}{EnsuresNonNullIf} diff --git a/docs/manual/called-methods-checker.tex b/docs/manual/called-methods-checker.tex index c33a68f1a375..d28b259889e3 100644 --- a/docs/manual/called-methods-checker.tex +++ b/docs/manual/called-methods-checker.tex @@ -219,7 +219,9 @@ \end{Verbatim} If \ might have side-effects (i.e., it is not annotated as - \refqualclass{dataflow/qual}{SideEffectFree} or \refqualclass{dataflow/qual}{Pure}), + \refqualclass{dataflow/qual}{SideEffectFree}, + \iffalse\refqualclass{dataflow/qual}{SideEffectsOnly},\fi or + \refqualclass{dataflow/qual}{Pure}), then the Called Methods Checker issues an error because it cannot make any assumptions about the call to \, and therefore assumes the worst: that all information it knows about in-scope variables (including @@ -227,7 +229,9 @@ There are two possible fixes: \begin{itemize} - \item add a \<@SideEffectFree> or \<@Pure> annotation to \, if \ is + \item add a \refqualclass{dataflow/qual}{SideEffectFree}, + \iffalse\refqualclass{dataflow/qual}{SideEffectsOnly},\fi or + \refqualclass{dataflow/qual}{Pure} annotation to \, if \ is in fact side-effect free or pure; or \item re-order the calls to \ and \ so that the call to \ appears last in \. diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index ba911e672c9e..238e918da71d 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -619,12 +619,15 @@ More sound (strict) checking: enable errors that are disabled by default \begin{itemize} \item \<-AcheckPurityAnnotations> - Check the bodies of methods marked + Check the bodies of methods and constructors marked \refqualclass{dataflow/qual}{SideEffectFree}, +\iffalse + \refqualclass{dataflow/qual}{SideEffectsOnly}, +\fi \refqualclass{dataflow/qual}{Deterministic}, and \refqualclass{dataflow/qual}{Pure} - to ensure the method satisfies the annotation. By default, - the Checker Framework unsoundly trusts the method annotation. See + to ensure the method or constructor satisfies the annotation. By default, + the Checker Framework unsoundly trusts the annotation. See Section~\ref{type-refinement-purity}. \item \<-AinvariantArrays> Make array subtyping invariant; that is, two arrays are subtypes of one @@ -1577,6 +1580,14 @@ If your proof includes ``method \ has no side effects'', then annotate \'s declaration with \refqualclass{dataflow/qual}{SideEffectFree}. +\iffalse +\item + If your proof includes ``method \ modifies nothing but field \ of + its receiver'', then annotate \'s declaration with + \refqualclasswithparams{dataflow/qual}{SideEffectsOnly}{"this.f"}. The + annotation's required argument lists every expression that \ might + modify. +\fi \item If your proof includes ``each call to method \ returns the same value'', then annotate \'s declaration with diff --git a/docs/manual/nullness-checker.tex b/docs/manual/nullness-checker.tex index 19dd88c128c9..84c4653d35b7 100644 --- a/docs/manual/nullness-checker.tex +++ b/docs/manual/nullness-checker.tex @@ -239,7 +239,8 @@ arbitrary external method calls that have access to the given field. By contrast, for a \<@Nullable> field, the Nullness Checker assumes that most method calls might set it to \. (Exceptions are calls to - methods that are \refqualclass{dataflow/qual}{SideEffectFree} or that + methods that are \refqualclass{dataflow/qual}{SideEffectFree}\iffalse or + (for non-listed expressions) \refqualclass{dataflow/qual}{SideEffectsOnly}\fi, or that have an \refqualclass{checker/nullness/qual}{EnsuresNonNull} or \refqualclass{checker/nullness/qual}{EnsuresNonNullIf} annotation.) \end{sloppypar} diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index fb48ea7d074c..e099a6d81a5c 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -27,6 +27,11 @@ \item[\refqualclass{dataflow/qual}{SideEffectFree}] indicates that the method has no externally-visible side effects. +\iffalse +\item[\refqualclass{dataflow/qual}{SideEffectsOnly}] + indicates that the method has limited externally-visible side effects. +\fi + \item[\refqualclass{dataflow/qual}{Deterministic}] indicates that if the method is called multiple times with identical arguments, then it returns the identical result according to \<==> @@ -45,7 +50,12 @@ mistake % by writing \<\refqualclass{dataflow/qual}{SideEffectFree}> on the -declaration of a method that is not side-effect-free +declaration of a method that is not side-effect-free, +% +\iffalse +by writing \<\refqualclass{dataflow/qual}{SideEffectsOnly}> on the +declaration of a method that side-effects more than the listed expressions, +\fi or % by writing \<\refqualclass{dataflow/qual}{Deterministic}> on the diff --git a/docs/manual/troubleshooting.tex b/docs/manual/troubleshooting.tex index 1206305a3f80..208c6a1e3c28 100644 --- a/docs/manual/troubleshooting.tex +++ b/docs/manual/troubleshooting.tex @@ -347,6 +347,7 @@ \ does not set the field \ to \, you can use \<\refqualclass{dataflow/qual}{Pure}>, \<\refqualclass{dataflow/qual}{SideEffectFree}>, +\iffalse\<\refqualclass{dataflow/qual}{SideEffectsOnly}>,\fi or \<\refqualclass{checker/nullness/qual}{EnsuresNonNull}> on the declaration of \; see Sections~\ref{type-refinement-purity} and~\ref{nullness-method-annotations}. diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 2db4137f2a29..19bd52778759 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -95,6 +95,7 @@ import org.checkerframework.dataflow.qual.Impure; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; import org.checkerframework.dataflow.util.PurityChecker; import org.checkerframework.dataflow.util.PurityChecker.PurityResult; import org.checkerframework.dataflow.util.PurityKind; @@ -242,6 +243,9 @@ public class BaseTypeVisitor>( /** Instance of the types utility. */ protected final Types types; + /** + * Cache for {@link #getSideEffectsOnlyExpressions}, which would otherwise re-parse the + * annotation's expressions once per dataflow iteration per call site. A key that is mapped to + * null stands for the null result, so test membership with {@link Map#containsKey} rather than + * comparing the result of {@link Map#get} to null. + * + *

The keys are nodes of a single control flow graph, so {@link #performAnalysis} clears this. + * + *

This is an {@link IdentityHashMap} because the cached values are viewpoint-adapted to a + * particular call site, but {@link MethodInvocationNode#equals} compares only the target and the + * arguments. Two call sites that are equal in that sense need not adapt to the same expressions, + * so a hash map keyed by {@code equals} could return one call site's expressions for another. The + * same node object is passed on every dataflow iteration, so identity keys still hit. + */ + private final IdentityHashMap> + sideEffectsOnlyExpressionsCache = new IdentityHashMap<>(); + /** * Create a CFAbstractAnalysis. * @@ -129,9 +153,90 @@ protected CFAbstractAnalysis( public void performAnalysis(ControlFlowGraph cfg, List> fieldValues) { this.fieldValues.clear(); this.fieldValues.addAll(fieldValues); + // The cache's keys are nodes of the control flow graph that was analyzed previously. + sideEffectsOnlyExpressionsCache.clear(); super.performAnalysis(cfg); } + /** + * Returns the expressions that the invoked method side-effects (specified as arguments/elements + * of {@code @SideEffectsOnly}), viewpoint-adapted to the given method invocation. Returns null if + * the invoked method has no {@code @SideEffectsOnly} annotation. + * + *

Also returns null if any of the annotation's expressions cannot be parsed at the call site. + * Null means "the method might side-effect anything", which is the conservative result; returning + * a list that omits the unparseable expression would treat the method as side-effecting + * less than it was declared to. + * + *

The result is cached, because dataflow calls this once per iteration per call site and + * parsing an expression is not cheap. Clients should not side-effect the returned value, which is + * aliased to internal state. + * + * @param methodInvocationNode the call site at which the side-effecting expressions will be used + * @return the expressions that the method side-effects, viewpoint-adapted to the given + * invocation; or null if the method has no valid {@code @SideEffectsOnly} annotation + */ + public @Nullable List getSideEffectsOnlyExpressions( + MethodInvocationNode methodInvocationNode) { + if (sideEffectsOnlyExpressionsCache.containsKey(methodInvocationNode)) { + return sideEffectsOnlyExpressionsCache.get(methodInvocationNode); + } + ExecutableElement method = methodInvocationNode.getTarget().getMethod(); + List result = computeSideEffectsOnlyExpressions(method, methodInvocationNode); + sideEffectsOnlyExpressionsCache.put(methodInvocationNode, result); + return result; + } + + /** + * Computes the value that {@link #getSideEffectsOnlyExpressions} caches and returns; see that + * method for the specification. + * + * @param method a method + * @param methodInvocationNode the call site at which the side-effecting expressions will be used + * @return the expressions that the method side-effects, viewpoint-adapted to the given + * invocation, or null + */ + private @Nullable List computeSideEffectsOnlyExpressions( + ExecutableElement method, MethodInvocationNode methodInvocationNode) { + List seOnlyExpressionStrings = atypeFactory.getSideEffectsOnlyExpressionStrings(method); + if (seOnlyExpressionStrings == null) { + return null; + } + + List seOnlyExpressions = new ArrayList<>(); + + for (String seOnlyExpr : seOnlyExpressionStrings) { + try { + // Do not use `StringToJavaExpression.atMethodInvocation(seOnlyExpr, + // methodInvocationNode, checker)`, which obtains the invoked method from + // `methodInvocationNode.getTree()`; that tree is null for a call that corresponds to no + // AST tree, such as the `Iterator.next()` that an enhanced for loop is desugared to. + JavaExpression exprJe = + StringToJavaExpression.atMethodDecl(seOnlyExpr, method, checker) + .atMethodInvocation(methodInvocationNode); + + if (exprJe.containsUnknown()) { + // Nothing in the store can match an `Unknown`, so returning the expression would discard + // no refinement at all. Returning null makes the caller discard every refinement. + return null; + } + + // At a call of the form `super.m()`, viewpoint-adapting the callee's `this` yields + // `super`. + // The caller refers to that same object as `this`, so rewrite it that way; otherwise + // the refinements of `this` and of its fields would not be discarded. + exprJe = JavaExpression.superToThis(exprJe); + seOnlyExpressions.add(exprJe); + } catch (JavaExpressionParseException ex) { + // The expression cannot be represented at the call site, so the caller must assume that + // the call might side-effect anything. A future change will report the parse error. + return null; + } + } + + return seOnlyExpressions; + } + /** * A list of initial abstract values for the fields. * diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index bdafce2045a4..caec1bb3c33f 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -236,25 +236,35 @@ public void updateForMethodCall(MethodInvocationNode methodInvocationNode, V val boolean sideEffectsUnrefineAliases = atypeFactory.sideEffectsUnrefineAliases; Node receiver = methodInvocationNode.getTarget().getReceiver(); - boolean hasDoesNotUnrefineReceiver = atypeFactory.hasDoesNotUnrefineReceiver(method); - - // TODO: Also remove if any element/argument to the annotation is not - // isUnmodifiableByOtherCode. Example: @KeyFor("valueThatCanBeMutated"). + boolean hasDoesNotUnrefineReceiver = atypeFactory.hasDoesNotUnrefineReceiver(method); // This is an expression that is exempted from unrefinement, or null if no expression is // exempted. @Nullable JavaExpression unrefinableReceiverJe = hasDoesNotUnrefineReceiver ? JavaExpression.fromNode(receiver) : null; + @Nullable List seOnlyExpressions = + analysis.getSideEffectsOnlyExpressions(methodInvocationNode); + + // TODO: Also remove if any element/argument to the annotation is not + // isUnmodifiableByOtherCode. Example: @KeyFor("valueThatCanBeMutated"). + // Update local variables. if (sideEffectsUnrefineAliases) { localVariableValues .entrySet() - .removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe)); + .removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe, seOnlyExpressions)); } // Update this value. + // `thisValue` is the abstract value of the expression `this`. A callee with a + // `@SideEffectsOnly` annotation can change it only if the annotation lists `this` itself. + // (At call site `x.m()`, the callee's `this` corresponds to `x`.) + boolean thisIsSideEffected = + seOnlyExpressions == null + || seOnlyExpressions.stream().anyMatch(je -> je instanceof ThisReference); if (sideEffectsUnrefineAliases + && thisIsSideEffected && !(unrefinableReceiverJe instanceof ThisReference) && !(unrefinableReceiverJe instanceof SuperReference)) { thisValue = null; @@ -262,19 +272,23 @@ public void updateForMethodCall(MethodInvocationNode methodInvocationNode, V val // Update field values. if (sideEffectsUnrefineAliases) { - fieldValues.entrySet().removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe)); + fieldValues + .entrySet() + .removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe, seOnlyExpressions)); } else { // Case 2 (unassignable fields) and case 3 (monotonic fields). - updateFieldValuesForMethodCall(atypeFactory, unrefinableReceiverJe); + updateFieldValuesForMethodCall(atypeFactory, unrefinableReceiverJe, seOnlyExpressions); } // Update array values. - arrayValues.entrySet().removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe)); + arrayValues + .entrySet() + .removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe, seOnlyExpressions)); // Update information about method calls. methodCallExpressions .entrySet() - .removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe)); + .removeIf(e -> isSideEffected(e.getKey(), unrefinableReceiverJe, seOnlyExpressions)); } // Store information about method calls if possible. @@ -286,6 +300,12 @@ public void updateForMethodCall(MethodInvocationNode methodInvocationNode, V val * Returns true if a method call might change the abstract value of the given expression, so its * refinement should be discarded. * + *

When {@code sideEffectsOnlyExpressions} is non-null (the method has a + * {@code @SideEffectsOnly} annotation), {@code expr} is side-effected only if {@link + * #mayChangeValue} holds of it and one of those expressions. This is the counterpart of the + * exact-equality test used at the declaration site in {@code DisallowedSideEffects}, which checks + * what the method body actually modifies. + * *

Some side effects are ignored: {@code notSideEffectedExpression} is treated as if it cannot * change. Concretely, the implementation evaluates to false if {@code expr} is strictly equal to * {@code notSideEffectedExpression}. @@ -293,19 +313,101 @@ public void updateForMethodCall(MethodInvocationNode methodInvocationNode, V val * @param expr an expression * @param notSideEffectedExpression an expression that is never considered to be side-effected, or * null + * @param sideEffectsOnlyExpressions if non-null, only these expressions (and expressions whose + * value they may change) are considered to be side-effected * @return true if the abstract value of the expression might have changed */ private boolean isSideEffected( - JavaExpression expr, @Nullable JavaExpression notSideEffectedExpression) { + JavaExpression expr, + @Nullable JavaExpression notSideEffectedExpression, + @Nullable List sideEffectsOnlyExpressions) { if (!expr.isModifiableByOtherCode()) { return false; } if (notSideEffectedExpression != null && expr.equals(notSideEffectedExpression)) { return false; } + if (sideEffectsOnlyExpressions != null) { + return sideEffectsOnlyExpressions.stream().anyMatch(seOnly -> mayChangeValue(expr, seOnly)); + } return true; } + /** + * Returns true if modifying {@code seOnlyExpr}, or anything reached through it, might change the + * value of {@code expr}. + * + *

That is the case when {@code expr} contains {@code seOnlyExpr} as a subexpression: modifying + * {@code x} can change {@code x.f}. + * + *

It is also the case when {@code expr} contains a method call through which {@code + * seOnlyExpr} is reached; see {@link #callMayChangeValue}. + * + * @param expr an expression whose value is stored in this store + * @param seOnlyExpr an expression that may be modified + * @return true if modifying {@code seOnlyExpr} might change the value of {@code expr} + */ + private static boolean mayChangeValue(JavaExpression expr, JavaExpression seOnlyExpr) { + return expr.containsSyntacticEqualJavaExpression(seOnlyExpr) + || callMayChangeValue(expr, seOnlyExpr); + } + + /** + * Returns true if {@code expr} contains a method call such that modifying {@code seOnlyExpr} + * might change the method call's value. + * + *

The value of a call to a {@code @Pure} method depends on the state that the method reads, + * which no annotation declares; this method approximates the read state by what is reachable from + * the call's receiver and arguments. If {@code getF()} returns {@code this.f}, then a call to a + * {@code @SideEffectsOnly("x.f")} method can change the value of {@code x.getF()}, even though + * {@code x.getF()} does not contain {@code x.f}. + * + *

The call need not be {@code expr} itself: the value of {@code x.getF().g} and of {@code + * x.getArr()[0]} also changes when the value of the call within them does. Such an expression + * contains no method call as a subexpression in the sense of {@link + * JavaExpression#containsSyntacticEqualJavaExpression}, because a receiver or array is not + * compared against {@code seOnlyExpr} but is descended into here. + * + * @param expr an expression whose value is stored in this store + * @param seOnlyExpr an expression that may be modified + * @return true if modifying {@code seOnlyExpr} might change the value of expr, by changing the + * value of a call within {@code expr} + */ + private static boolean callMayChangeValue(JavaExpression expr, JavaExpression seOnlyExpr) { + if (expr instanceof MethodCall methodCall) { + if (mayReach(seOnlyExpr, methodCall.getReceiver())) { + return true; + } + for (JavaExpression argument : methodCall.getArguments()) { + if (mayReach(seOnlyExpr, argument)) { + return true; + } + } + return false; + } else if (expr instanceof FieldAccess fieldAccess) { + return callMayChangeValue(fieldAccess.getReceiver(), seOnlyExpr); + } else if (expr instanceof ArrayAccess arrayAccess) { + return callMayChangeValue(arrayAccess.getArray(), seOnlyExpr) + || callMayChangeValue(arrayAccess.getIndex(), seOnlyExpr); + } else { + return false; + } + } + + /** + * Returns true if {@code seOnlyExpr} may be reached through {@code input}. + * + * @param seOnlyExpr an expression that may be modified + * @param input the receiver or an argument of a stored method call + * @return true if {@code seOnlyExpr} may be reached through {@code input} + */ + private static boolean mayReach(JavaExpression seOnlyExpr, JavaExpression input) { + // The recursive call handles a nested call such as `x.getA().getB()`, whose receiver is + // itself a method call. + return seOnlyExpr.containsSyntacticEqualJavaExpression(input) + || mayChangeValue(input, seOnlyExpr); + } + /** * Returns the new value of a field after a method call, or {@code null} if the field should be * removed from the store. @@ -388,18 +490,24 @@ protected V newMonotonicFieldValueAfterMethodCall( *

More specifically, remove all information about fields except for unassignable fields and * fields that have a monotonic annotation. * + *

A non-null {@code sideEffectsOnlyExpressions} indicates that the invoked method has limited + * side effects. In this case, remove information for fields that appear in the list of + * side-effected expressions. + * * @param atypeFactory AnnotatedTypeFactory of the associated checker * @param unrefinableReceiverJe if non-null, the receiver, which should not be unrefined + * @param sideEffectsOnlyExpressions the expressions that are side-effected by a method call */ private void updateFieldValuesForMethodCall( GenericAnnotatedTypeFactory atypeFactory, - @Nullable JavaExpression unrefinableReceiverJe) { + @Nullable JavaExpression unrefinableReceiverJe, + @Nullable List sideEffectsOnlyExpressions) { Map newFieldValues = new HashMap<>(MapsP.mapCapacity(fieldValues)); for (Map.Entry e : fieldValues.entrySet()) { FieldAccess fieldAccess = e.getKey(); V previousValue = e.getValue(); - if (!isSideEffected(fieldAccess, unrefinableReceiverJe)) { + if (!isSideEffected(fieldAccess, unrefinableReceiverJe, sideEffectsOnlyExpressions)) { // If the field hasn't been side-effected, there is no need to compute a new value for it. // For unmodifiable fields, this is safe because they are not assignable by other code. // For the exempt receiver, skipping recomputation is necessary to preserve its value. diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index acb92af2ce33..20f33308418a 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1080,6 +1080,8 @@ public TransferResult visitObjectCreation(ObjectCreationNode n, TransferIn S store = p.getRegularStore(); // add new information based on postcondition processPostconditions(n, store, constructorElt, newClassTree); + // TODO: This does not call `store.updateForMethodCall`, so a constructor's + // `@SideEffectsOnly` annotation has no effect yet on type refinement at a `new` expression. return super.visitObjectCreation(n, p); } diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 4aeccaefc25e..9c9582e48e99 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -95,6 +95,7 @@ import org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.InferredDeclared; import org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenesStorage; import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.DoesNotUnrefineReceiver; import org.checkerframework.framework.qual.EnsuresQualifier; @@ -262,6 +263,9 @@ public class AnnotatedTypeFactory implements AnnotationProvider { /** The RequiresQualifier.List.value field/element. */ protected final ExecutableElement requiresQualifierListValueElement; + /** The SideEffectsOnly.value field/element. */ + protected final ExecutableElement sideEffectsOnlyValueElement; + /** The RequiresQualifier type. */ protected final TypeMirror requiresQualifierTM; @@ -704,6 +708,8 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) { TreeUtils.getMethod(RequiresQualifier.class, "expression", 0, processingEnv); requiresQualifierListValueElement = TreeUtils.getMethod(RequiresQualifier.List.class, "value", 0, processingEnv); + sideEffectsOnlyValueElement = + TreeUtils.getMethod(SideEffectsOnly.class, "value", 0, processingEnv); requiresQualifierTM = ElementUtils.getTypeElement(processingEnv, RequiresQualifier.class).asType(); @@ -4186,6 +4192,25 @@ private void inheritOverriddenDeclAnnos(ExecutableElement elt, AnnotationMirrorS } } + /** + * Returns the expressions written in the {@code @SideEffectsOnly} annotation on {@code method}. + * Returns null if {@code method} has no {@code @SideEffectsOnly} annotation. + * + *

Clients should not side-effect the returned value, which may be aliased to internal state. + * + * @param method a method or constructor + * @return the {@code @SideEffectsOnly} expressions written on {@code method}, or null if {@code + * method} has no {@code @SideEffectsOnly} annotation + */ + public @Nullable List getSideEffectsOnlyExpressionStrings(ExecutableElement method) { + AnnotationMirror sideEffectsOnly = getDeclAnnotation(method, SideEffectsOnly.class); + if (sideEffectsOnly == null) { + return null; + } + return AnnotationUtils.getElementValueArray( + sideEffectsOnly, sideEffectsOnlyValueElement, String.class); + } + private void addOrMerge(AnnotationMirrorSet results, AnnotationMirror annotation) { if (AnnotationUtils.containsSameByName(results, annotation)) { /* From 578a6dce250eb692fbc62bd86cb00e7f601a3075 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 12 Aug 2026 08:36:44 -0700 Subject: [PATCH 2/6] Inherit @SideEffectsOnly from overridden methods @SideEffectsOnly is not inherited as an annotation, because its `value` element is significant, unlike that of the other inherited declaration annotations. A method that overrides methods in two supertypes inherits the union of what they permit it to side-effect, rather than the "first one wins" rule of `addOrMerge`. Each expression is remembered along with the method that declares it, because the expression is parsed in that method's scope: an expression that names a field of the superclass might name a different field, or none at all, in the subclass. A @SideEffectsOnly written on the overriding method itself is authoritative, so in that case nothing is inherited. Co-Authored-By: Claude Opus 5 --- .../SideEffectsOnlyInherit.java | 71 ++++++++++ .../SideEffectsOnlyInheritScope.java | 47 +++++++ .../SideEffectsOnlyOverride.java | 85 +++++++++++ .../framework/flow/CFAbstractAnalysis.java | 60 ++++---- .../framework/type/AnnotatedTypeFactory.java | 133 ++++++++++++++---- 5 files changed, 340 insertions(+), 56 deletions(-) create mode 100644 checker/tests/sideeffectsonly/SideEffectsOnlyInherit.java create mode 100644 checker/tests/sideeffectsonly/SideEffectsOnlyInheritScope.java create mode 100644 checker/tests/sideeffectsonly/SideEffectsOnlyOverride.java diff --git a/checker/tests/sideeffectsonly/SideEffectsOnlyInherit.java b/checker/tests/sideeffectsonly/SideEffectsOnlyInherit.java new file mode 100644 index 000000000000..41766bb54210 --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsOnlyInherit.java @@ -0,0 +1,71 @@ +// A method that overrides methods in two supertypes inherits the union of their +// `@SideEffectsOnly` expressions, not just the first supertype's. The `value` element of +// `@SideEffectsOnly` is significant, unlike that of the other inherited declaration annotations. + +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsOnlyInherit { + + static class Cell { + @Tainted Object f; + @Tainted Object g; + } + + interface I { + @SideEffectsOnly("#1.f") + void m(Cell c); + } + + static class Base { + @SideEffectsOnly("#1.g") + public void m(Cell c) {} + } + + // `C.m` cannot satisfy both supertype specifications; the override errors are suppressed in + // order to test what `C.m` inherits. Whichever supertype `AnnotatedTypes.overriddenMethods` + // yields first, `C.m` is treated as side-effecting both `#1.f` and `#1.g`. + @SuppressWarnings("purity.sideeffectsonly.overriding") + static class C extends Base implements I { + @Override + public void m(Cell c) {} + } + + @EnsuresQualifier(expression = "#1.f", qualifier = Untainted.class) + // :: error: contracts.postcondition + static void makeFUntainted(Cell c) {} + + @EnsuresQualifier(expression = "#1.g", qualifier = Untainted.class) + // :: error: contracts.postcondition + static void makeGUntainted(Cell c) {} + + static void testF(C receiver, Cell c) { + makeFUntainted(c); + receiver.m(c); + // :: error: assignment + @Untainted Object y = c.f; + } + + static void testG(C receiver, Cell c) { + makeGUntainted(c); + receiver.m(c); + // :: error: assignment + @Untainted Object y = c.g; + } + + // A `@SideEffectsOnly` written on the method itself is authoritative: nothing is inherited. + @SuppressWarnings("purity.sideeffectsonly.overriding") + static class D extends Base implements I { + @SideEffectsOnly("#1.f") + @Override + public void m(Cell c) {} + } + + static void testOwnAnnotationWins(D receiver, Cell c) { + makeGUntainted(c); + receiver.m(c); + @Untainted Object y = c.g; + } +} diff --git a/checker/tests/sideeffectsonly/SideEffectsOnlyInheritScope.java b/checker/tests/sideeffectsonly/SideEffectsOnlyInheritScope.java new file mode 100644 index 000000000000..76a37ebdaf72 --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsOnlyInheritScope.java @@ -0,0 +1,47 @@ +// The expressions of an inherited `@SideEffectsOnly` annotation are resolved in the scope of the +// supertype method that declares them, not in the scope of the method that inherits them. + +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsOnlyInheritScope { + + static class Sup { + @Tainted Object f; + + @SideEffectsOnly("this.f") + void m() {} + } + + static class Sub extends Sup { + // Shadows `Sup.f`. `Sub.m` inherits a specification about `Sup.f`, not about `Sub.f`. + @Tainted Object f; + + @Override + void m() {} + } + + @EnsuresQualifier(expression = "#1.f", qualifier = Untainted.class) + // :: error: contracts.postcondition + static void makeSupFUntainted(Sup s) {} + + @EnsuresQualifier(expression = "#1.f", qualifier = Untainted.class) + // :: error: contracts.postcondition + static void makeSubFUntainted(Sub s) {} + + static void testShadowingFieldIsRetained(Sub s) { + makeSubFUntainted(s); + s.m(); + // `Sub.f` is not side-effected, so its refinement is retained. + @Untainted Object y = s.f; + } + + static void testShadowedFieldIsDiscarded(Sub s) { + makeSupFUntainted(s); + s.m(); + // :: error: assignment + @Untainted Object y = ((Sup) s).f; + } +} diff --git a/checker/tests/sideeffectsonly/SideEffectsOnlyOverride.java b/checker/tests/sideeffectsonly/SideEffectsOnlyOverride.java new file mode 100644 index 000000000000..2efc4aca0844 --- /dev/null +++ b/checker/tests/sideeffectsonly/SideEffectsOnlyOverride.java @@ -0,0 +1,85 @@ +// An overriding method must not side-effect more than the overridden method's +// `@SideEffectsOnly` annotation permits. Otherwise a call whose receiver is statically of the +// supertype would retain a refinement that the override invalidates. + +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +public class SideEffectsOnlyOverride { + + static class Cell { + @Tainted Object g; + @Tainted Cell inner; + } + + static class Super { + @SideEffectsOnly("#1.inner") + void m(Cell c) {} + } + + /** Side-effects exactly what the supertype permits. */ + static class SubSame extends Super { + @SideEffectsOnly("#1.inner") + @Override + void m(Cell c) {} + } + + /** Side-effects less than the supertype permits: `#1.inner.g` is reached through `#1.inner`. */ + static class SubDeeper extends Super { + @SideEffectsOnly("#1.inner.g") + @Override + void m(Cell c) {} + } + + /** Side-effects nothing at all. */ + static class SubSideEffectFree extends Super { + @SideEffectFree + @Override + void m(Cell c) {} + } + + /** Side-effects more than the supertype permits. */ + static class SubMore extends Super { + @SideEffectsOnly({"#1.inner", "#1.g"}) + @Override + // TODO :: error: purity.sideeffectsonly.overriding + void m(Cell c) {} + } + + /** `#1` is not reached through `#1.inner`, so side-effecting it is more than permitted. */ + static class SubWhole extends Super { + @SideEffectsOnly("#1") + @Override + // TODO :: error: purity.sideeffectsonly.overriding + void m(Cell c) {} + } + + /** A supertype without `@SideEffectsOnly` constrains nothing. */ + static class Unconstrained { + void m(Cell c) {} + } + + static class SubOfUnconstrained extends Unconstrained { + @SideEffectsOnly("#1.inner") + @Override + void m(Cell c) {} + } + + @EnsuresQualifier(expression = "#1.g", qualifier = Untainted.class) + // :: error: contracts.postcondition + static void makeUntainted(Cell c) {} + + /** + * Without the override check, this refinement would be wrongly retained: the call resolves + * statically to {@code Super.m}, which does not permit side-effecting {@code c.g}, but it may + * execute {@code SubMore.m}, which does. + */ + static void testDynamicDispatch(Super s, Cell c) { + makeUntainted(c); + s.m(c); + @Untainted Object y = c.g; + } +} diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index 29144cd1895b..6b17b842f388 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -198,39 +198,49 @@ public void performAnalysis(ControlFlowGraph cfg, List> fie */ private @Nullable List computeSideEffectsOnlyExpressions( ExecutableElement method, MethodInvocationNode methodInvocationNode) { - List seOnlyExpressionStrings = atypeFactory.getSideEffectsOnlyExpressionStrings(method); + Map> seOnlyExpressionStrings = + atypeFactory.getSideEffectsOnlyExpressionStrings(method); if (seOnlyExpressionStrings == null) { return null; } List seOnlyExpressions = new ArrayList<>(); - for (String seOnlyExpr : seOnlyExpressionStrings) { - try { - // Do not use `StringToJavaExpression.atMethodInvocation(seOnlyExpr, - // methodInvocationNode, checker)`, which obtains the invoked method from - // `methodInvocationNode.getTree()`; that tree is null for a call that corresponds to no - // AST tree, such as the `Iterator.next()` that an enhanced for loop is desugared to. - JavaExpression exprJe = - StringToJavaExpression.atMethodDecl(seOnlyExpr, method, checker) - .atMethodInvocation(methodInvocationNode); - - if (exprJe.containsUnknown()) { - // Nothing in the store can match an `Unknown`, so returning the expression would discard - // no refinement at all. Returning null makes the caller discard every refinement. + for (Map.Entry> entry : seOnlyExpressionStrings.entrySet()) { + // The method whose `@SideEffectsOnly` annotation contains the expressions. It is `method` + // itself, unless `method` inherits the annotation. + ExecutableElement declaringMethod = entry.getKey(); + for (String seOnlyExpr : entry.getValue()) { + try { + // An expression is parsed in the scope of the method that declares it, which is not + // necessarily the scope of `method`: a field that the declaring method's class declares + // might be shadowed or inaccessible in `method`'s class. + // Do not use `StringToJavaExpression.atMethodInvocation(seOnlyExpr, + // methodInvocationNode, checker)`, which obtains the invoked method from + // `methodInvocationNode.getTree()`; that tree is null for a call that corresponds to no + // AST tree, such as the `Iterator.next()` that an enhanced for loop is desugared to. + JavaExpression exprJe = + StringToJavaExpression.atMethodDecl(seOnlyExpr, declaringMethod, checker) + .atMethodInvocation(methodInvocationNode); + + if (exprJe.containsUnknown()) { + // Nothing in the store can match an `Unknown`, so returning the expression would + // discard no refinement at all. Returning null makes the caller discard every + // refinement. + return null; + } + + // At a call of the form `super.m()`, viewpoint-adapting the callee's `this` yields + // `super`. + // The caller refers to that same object as `this`, so rewrite it that way; otherwise + // the refinements of `this` and of its fields would not be discarded. + exprJe = JavaExpression.superToThis(exprJe); + seOnlyExpressions.add(exprJe); + } catch (JavaExpressionParseException ex) { + // The expression cannot be represented at the call site, so the caller must assume that + // the call might side-effect anything. A future change will report the parse error. return null; } - - // At a call of the form `super.m()`, viewpoint-adapting the callee's `this` yields - // `super`. - // The caller refers to that same object as `this`, so rewrite it that way; otherwise - // the refinements of `this` and of its fields would not be discarded. - exprJe = JavaExpression.superToThis(exprJe); - seOnlyExpressions.add(exprJe); - } catch (JavaExpressionParseException ex) { - // The expression cannot be represented at the call site, so the caller must assume that - // the call might side-effect anything. A future change will report the parse error. - return null; } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 9c9582e48e99..5643cb1bd4ba 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -49,6 +49,7 @@ import java.util.HashMap; import java.util.HashSet; import java.util.IdentityHashMap; +import java.util.LinkedHashMap; import java.util.List; import java.util.Map; import java.util.Set; @@ -363,6 +364,23 @@ public class AnnotatedTypeFactory implements AnnotationProvider { */ private final AnnotationMirrorSet inheritedAnnotations = new AnnotationMirrorSet(); + /** + * Maps a method to the {@code @SideEffectsOnly} expressions that it inherits from the methods it + * overrides: a map from a method declaration to the expressions written in the + * {@code @SideEffectsOnly} annotation on that declaration. A method that inherits no such + * expression has no entry. + * + *

The declaring method is retained, rather than just the expression strings, because each + * expression must be parsed in the scope of the method that declares it; see {@link + * #getSideEffectsOnlyExpressionStrings}. + * + *

{@link #inheritOverriddenDeclAnnos} populates this map, in lockstep with {@link + * #cacheDeclAnnos}, so an entry is present only after {@link #getDeclAnnotations} has been called + * on the method. + */ + private final Map>> + inheritedSideEffectsOnlyExpressions = new HashMap<>(); + /** The checker to use for option handling and resource management. */ protected final BaseTypeChecker checker; @@ -811,6 +829,10 @@ protected void postInit( addInheritedAnnotation( AnnotationBuilder.fromClass( elements, org.checkerframework.dataflow.qual.SideEffectFree.class)); + // `@SideEffectsOnly` is not in `inheritedAnnotations`, even though it is inherited, because + // inheriting it as an annotation would lose track of which method declared each of its + // expressions. `inheritOverriddenDeclAnnos` inherits it separately; see + // `getSideEffectsOnlyExpressionStrings`. addInheritedAnnotation( AnnotationBuilder.fromClass( elements, org.checkerframework.dataflow.qual.Deterministic.class)); @@ -4165,50 +4187,99 @@ private void inheritOverriddenDeclAnnos(ExecutableElement elt, AnnotationMirrorS Map overriddenMethods = AnnotatedTypes.overriddenMethods(elements, this, elt); - if (overriddenMethods != null) { - for (ExecutableElement superElt : overriddenMethods.values()) { - AnnotationMirrorSet superAnnos = getDeclAnnotations(superElt); - - for (AnnotationMirror annotation : superAnnos) { - List annotationsOnAnnotation; - try { - annotationsOnAnnotation = - annotation.getAnnotationType().asElement().getAnnotationMirrors(); - } catch (com.sun.tools.javac.code.Symbol.CompletionFailure cf) { - // Fix for Issue 348: If a CompletionFailure occurs, issue a warning. - checker.reportWarning( - annotation.getAnnotationType().asElement(), - "annotation.not.completed", - ElementUtils.getQualifiedName(elt), - annotation); - continue; - } - if (containsSameByClass(annotationsOnAnnotation, InheritedAnnotation.class) - || AnnotationUtils.containsSameByName(inheritedAnnotations, annotation)) { - addOrMerge(results, annotation); + if (overriddenMethods == null) { + return; + } + + // `@SideEffectsOnly` is not inherited as an annotation, because its `value` element is + // significant, unlike that of the other inherited declaration annotations. A method that + // overrides methods in two supertypes inherits the union of what they permit it to + // side-effect, rather than the "first one wins" rule of `addOrMerge`; + // `BaseTypeVisitor.OverrideChecker` reports any override that thereby side-effects more than a + // supertype permits. Furthermore, each expression must be remembered along with the method + // that declares it, because the expression is parsed in that method's scope. A + // `@SideEffectsOnly` written on `elt` itself is authoritative, so in that case nothing is + // inherited. + boolean inheritSideEffectsOnly = !containsSameByClass(results, SideEffectsOnly.class); + // The union of the supertypes' `@SideEffectsOnly` expressions, or null if no supertype has a + // `@SideEffectsOnly` annotation. A `LinkedHashMap` for determinism. + Map> inheritedSideEffectsOnly = null; + + for (ExecutableElement superElt : overriddenMethods.values()) { + if (inheritSideEffectsOnly) { + Map> superSideEffectsOnly = + getSideEffectsOnlyExpressionStrings(superElt); + if (superSideEffectsOnly != null) { + if (inheritedSideEffectsOnly == null) { + inheritedSideEffectsOnly = new LinkedHashMap<>(); } + inheritedSideEffectsOnly.putAll(superSideEffectsOnly); } } + + AnnotationMirrorSet superAnnos = getDeclAnnotations(superElt); + + for (AnnotationMirror annotation : superAnnos) { + List annotationsOnAnnotation; + try { + annotationsOnAnnotation = + annotation.getAnnotationType().asElement().getAnnotationMirrors(); + } catch (com.sun.tools.javac.code.Symbol.CompletionFailure cf) { + // Fix for Issue 348: If a CompletionFailure occurs, issue a warning. + checker.reportWarning( + annotation.getAnnotationType().asElement(), + "annotation.not.completed", + ElementUtils.getQualifiedName(elt), + annotation); + continue; + } + if (containsSameByClass(annotationsOnAnnotation, InheritedAnnotation.class) + || AnnotationUtils.containsSameByName(inheritedAnnotations, annotation)) { + addOrMerge(results, annotation); + } + } + } + + if (inheritedSideEffectsOnly != null) { + inheritedSideEffectsOnlyExpressions.put(elt, inheritedSideEffectsOnly); } } /** - * Returns the expressions written in the {@code @SideEffectsOnly} annotation on {@code method}. - * Returns null if {@code method} has no {@code @SideEffectsOnly} annotation. + * Returns the {@code @SideEffectsOnly} expressions that apply to {@code method}: a map from a + * method declaration to the expressions written in the {@code @SideEffectsOnly} annotation on + * that declaration. Returns null if no {@code @SideEffectsOnly} annotation applies to {@code + * method}. + * + *

The result identifies the method that declares each expression, rather than just the + * expression strings, because an expression is parsed in the scope of the method that declares + * it. That scope differs from {@code method}'s scope when {@code method} inherits the annotation: + * an expression that names a field of the superclass might name a different field, or none at + * all, in the subclass. + * + *

A {@code @SideEffectsOnly} annotation written on {@code method} itself is authoritative. + * Otherwise, {@code method} inherits the union of the annotations on the methods that it + * overrides. * *

Clients should not side-effect the returned value, which may be aliased to internal state. * * @param method a method or constructor - * @return the {@code @SideEffectsOnly} expressions written on {@code method}, or null if {@code - * method} has no {@code @SideEffectsOnly} annotation - */ - public @Nullable List getSideEffectsOnlyExpressionStrings(ExecutableElement method) { + * @return a map from a method declaration to the {@code @SideEffectsOnly} expressions written on + * it, or null if no {@code @SideEffectsOnly} annotation applies to {@code method} + */ + public @Nullable Map> getSideEffectsOnlyExpressionStrings( + ExecutableElement method) { + // This call also populates `inheritedSideEffectsOnlyExpressions` for `method`. Because + // `@SideEffectsOnly` is not inherited as an annotation, the result is non-null only if the + // annotation is written on `method` itself. AnnotationMirror sideEffectsOnly = getDeclAnnotation(method, SideEffectsOnly.class); - if (sideEffectsOnly == null) { - return null; + if (sideEffectsOnly != null) { + return Collections.singletonMap( + method, + AnnotationUtils.getElementValueArray( + sideEffectsOnly, sideEffectsOnlyValueElement, String.class)); } - return AnnotationUtils.getElementValueArray( - sideEffectsOnly, sideEffectsOnlyValueElement, String.class); + return inheritedSideEffectsOnlyExpressions.get(method); } private void addOrMerge(AnnotationMirrorSet results, AnnotationMirror annotation) { From fa14b99e67c61eaa3f9b43ecff94f6a1e1be98fe Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 12 Aug 2026 12:21:41 -0700 Subject: [PATCH 3/6] Javadoc --- .../framework/type/AnnotatedTypeFactory.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 9c9582e48e99..214d16d9e4d2 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -4211,6 +4211,13 @@ private void inheritOverriddenDeclAnnos(ExecutableElement elt, AnnotationMirrorS sideEffectsOnly, sideEffectsOnlyValueElement, String.class); } + /** + * Add the given annotation to the set, or (future feature) merge it with an existing annotation + * in the set. + * + * @param results a set to side-effect + * @param annotation an annotation to add to the set + */ private void addOrMerge(AnnotationMirrorSet results, AnnotationMirror annotation) { if (AnnotationUtils.containsSameByName(results, annotation)) { /* From 5e3a3225e8a01a34213f274a2a4955c244670b44 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 12 Aug 2026 12:40:37 -0700 Subject: [PATCH 4/6] Improve doc --- docs/manual/called-methods-checker.tex | 20 ++++++++++++-------- docs/manual/purity-checker.tex | 6 +++--- docs/manual/troubleshooting.tex | 11 +++++++---- 3 files changed, 22 insertions(+), 15 deletions(-) diff --git a/docs/manual/called-methods-checker.tex b/docs/manual/called-methods-checker.tex index d28b259889e3..c162f27370be 100644 --- a/docs/manual/called-methods-checker.tex +++ b/docs/manual/called-methods-checker.tex @@ -218,21 +218,25 @@ } \end{Verbatim} - If \ might have side-effects (i.e., it is not annotated as - \refqualclass{dataflow/qual}{SideEffectFree}, - \iffalse\refqualclass{dataflow/qual}{SideEffectsOnly},\fi or - \refqualclass{dataflow/qual}{Pure}), + If \ might have side-effects (i.e., it is not annotated + as \refqualclass{dataflow/qual}{SideEffectFree}, + as \refqualclass{dataflow/qual}{Pure}\iffalse, + or as \refqualclass{dataflow/qual}{SideEffectsOnly} with no expression + that can affect the value of \\fi), then the Called Methods Checker issues an error because it cannot make any assumptions about the call to \, and therefore assumes the worst: that all information it knows about in-scope variables (including that \ was called on \) is stale and must be discarded. - There are two possible fixes: + Here are possible fixes: \begin{itemize} - \item add a \refqualclass{dataflow/qual}{SideEffectFree}, - \iffalse\refqualclass{dataflow/qual}{SideEffectsOnly},\fi or + \item add a \refqualclass{dataflow/qual}{SideEffectFree} or \refqualclass{dataflow/qual}{Pure} annotation to \, if \ is - in fact side-effect free or pure; or + in fact side-effect free or pure. + \iffalse + \item add a \refqualclass{dataflow/qual}{SideEffectsOnly} annotation if + \ has side effects but cannot affect the value of \. + \fi \item re-order the calls to \ and \ so that the call to \ appears last in \. \end{itemize} diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index e099a6d81a5c..a334e5f8c365 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -49,16 +49,16 @@ methods affect type-checking of client code. However, you can make a mistake % -by writing \<\refqualclass{dataflow/qual}{SideEffectFree}> on the +by writing \refqualclass{dataflow/qual}{SideEffectFree} on the declaration of a method that is not side-effect-free, % \iffalse -by writing \<\refqualclass{dataflow/qual}{SideEffectsOnly}> on the +by writing \refqualclass{dataflow/qual}{SideEffectsOnly} on the declaration of a method that side-effects more than the listed expressions, \fi or % -by writing \<\refqualclass{dataflow/qual}{Deterministic}> on the +by writing \refqualclass{dataflow/qual}{Deterministic} on the declaration of a method that is not deterministic. To enable diff --git a/docs/manual/troubleshooting.tex b/docs/manual/troubleshooting.tex index 208c6a1e3c28..8dd0265f14bd 100644 --- a/docs/manual/troubleshooting.tex +++ b/docs/manual/troubleshooting.tex @@ -345,10 +345,13 @@ If you want to communicate that \ does not set the field \ to \, you can use -\<\refqualclass{dataflow/qual}{Pure}>, -\<\refqualclass{dataflow/qual}{SideEffectFree}>, -\iffalse\<\refqualclass{dataflow/qual}{SideEffectsOnly}>,\fi -or \<\refqualclass{checker/nullness/qual}{EnsuresNonNull}> on the +\refqualclass{dataflow/qual}{Pure}, +\refqualclass{dataflow/qual}{SideEffectFree}, +\iffalse +\refqualclass{dataflow/qual}{SideEffectsOnly} (with no expression that can +affect \), +\fi +or \refqualclass{checker/nullness/qual}{EnsuresNonNull} on the declaration of \; see Sections~\ref{type-refinement-purity} and~\ref{nullness-method-annotations}. From 98286e9f1d04ca9d43596299b50b9c9aadcfdbe6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 12 Aug 2026 12:49:30 -0700 Subject: [PATCH 5/6] Note a limitation --- .../StaticPureCallRefinement.java | 73 +++++++++++++++++++ .../framework/flow/CFAbstractStore.java | 10 +++ 2 files changed, 83 insertions(+) create mode 100644 checker/tests/sideeffectsonly/StaticPureCallRefinement.java diff --git a/checker/tests/sideeffectsonly/StaticPureCallRefinement.java b/checker/tests/sideeffectsonly/StaticPureCallRefinement.java new file mode 100644 index 000000000000..146dc27c2fe0 --- /dev/null +++ b/checker/tests/sideeffectsonly/StaticPureCallRefinement.java @@ -0,0 +1,73 @@ +// The value of a `@Pure` method call is approximated by the state reachable from the call's +// receiver and arguments. A static call has no receiver, so state that it reads through a class +// name is invisible to that approximation. + +import org.checkerframework.checker.tainting.qual.Tainted; +import org.checkerframework.checker.tainting.qual.Untainted; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; + +class StaticOther { + static @Tainted Object field; +} + +class StaticUtil { + @Pure + static Object get() { + return StaticOther.field; + } + + @Pure + static Object getFrom(StaticPureCallRefinement o) { + return o.f; + } +} + +public class StaticPureCallRefinement { + + @Tainted Object f; + + @EnsuresQualifier(expression = "StaticUtil.get()", qualifier = Untainted.class) + // :: error: contracts.postcondition + void makeUntaintedStatic() {} + + @EnsuresQualifier(expression = "StaticUtil.getFrom(#1)", qualifier = Untainted.class) + // :: error: contracts.postcondition + void makeUntaintedStaticArg(StaticPureCallRefinement o) {} + + @SideEffectsOnly("StaticOther.field") + void modifyStaticField() {} + + @SideEffectsOnly("#1.f") + void modifyField(StaticPureCallRefinement o) {} + + void arbitrary() {} + + void testStaticReceiver() { + makeUntaintedStatic(); + // `modifyStaticField` may write `StaticOther.field`, which `StaticUtil.get()` returns, so the + // refinement of `StaticUtil.get()` is stale. It is nonetheless retained, because + // `StaticUtil.get()` is not modifiable by other code: its receiver is a class name and it has + // no arguments, so no location that a caller could write appears in it. + modifyStaticField(); + @Untainted Object y = StaticUtil.get(); + } + + void testStaticReceiverImpureCall() { + makeUntaintedStatic(); + // The retention above is not specific to `@SideEffectsOnly`: the refinement of a static call + // with no modifiable argument survives an arbitrary impure call too. + arbitrary(); + @Untainted Object y = StaticUtil.get(); + } + + void testStaticArgument(StaticPureCallRefinement o) { + makeUntaintedStaticArg(o); + // By contrast, a static call whose argument reaches the modified location does lose its + // refinement, because arguments are part of the approximation. + modifyField(o); + // :: error: assignment + @Untainted Object y = StaticUtil.getFrom(o); + } +} diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index caec1bb3c33f..8177df8ec08f 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -362,6 +362,16 @@ private static boolean mayChangeValue(JavaExpression expr, JavaExpression seOnly * {@code @SideEffectsOnly("x.f")} method can change the value of {@code x.getF()}, even though * {@code x.getF()} does not contain {@code x.f}. * + *

The approximation misses state that a call reads but does not reach through its receiver or + * arguments. Static state is the main such case: the receiver of a static call is a class name, + * which reaches nothing, so only the arguments contribute. If {@code Util.getField()} returns + * {@code Other.field}, this method returns false for {@code Util.getField()} and {@code + * Other.field}, even though a call to a {@code @SideEffectsOnly("Other.field")} method can change + * the call's value. (For a static call with no modifiable argument, the omission is masked by + * {@link #isSideEffected}, which returns false before reaching this method because such a call is + * not {@link JavaExpression#isModifiableByOtherCode}; its refinement survives every call, not + * just a {@code @SideEffectsOnly} one.) + * *

The call need not be {@code expr} itself: the value of {@code x.getF().g} and of {@code * x.getArr()[0]} also changes when the value of the call within them does. Such an expression * contains no method call as a subexpression in the sense of {@link From 0a51ae2f74550d119d5130ecad98c91f9c7f5a12 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 13 Aug 2026 04:18:24 -0700 Subject: [PATCH 6/6] Consistent argument order, TODO --- .../framework/flow/CFAbstractStore.java | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index 8177df8ec08f..bbaeca474923 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -343,6 +343,12 @@ private boolean isSideEffected( *

It is also the case when {@code expr} contains a method call through which {@code * seOnlyExpr} is reached; see {@link #callMayChangeValue}. * + *

This method is unsound for two array accesses that may denote the same element without + * containing one another. It returns false for {@code a[i]} and {@code a[0]}, so the refinement + * of {@code a[i]} survives a call to a {@code @SideEffectsOnly("a[0]")} method even when {@code + * i} is 0. TODO: return true when both expressions are array accesses on arrays that may be the + * same, unless the two index expressions are known to differ. + * * @param expr an expression whose value is stored in this store * @param seOnlyExpr an expression that may be modified * @return true if modifying {@code seOnlyExpr} might change the value of {@code expr} @@ -385,11 +391,11 @@ private static boolean mayChangeValue(JavaExpression expr, JavaExpression seOnly */ private static boolean callMayChangeValue(JavaExpression expr, JavaExpression seOnlyExpr) { if (expr instanceof MethodCall methodCall) { - if (mayReach(seOnlyExpr, methodCall.getReceiver())) { + if (mayReach(methodCall.getReceiver(), seOnlyExpr)) { return true; } for (JavaExpression argument : methodCall.getArguments()) { - if (mayReach(seOnlyExpr, argument)) { + if (mayReach(argument, seOnlyExpr)) { return true; } } @@ -407,11 +413,11 @@ private static boolean callMayChangeValue(JavaExpression expr, JavaExpression se /** * Returns true if {@code seOnlyExpr} may be reached through {@code input}. * - * @param seOnlyExpr an expression that may be modified * @param input the receiver or an argument of a stored method call + * @param seOnlyExpr an expression that may be modified * @return true if {@code seOnlyExpr} may be reached through {@code input} */ - private static boolean mayReach(JavaExpression seOnlyExpr, JavaExpression input) { + private static boolean mayReach(JavaExpression input, JavaExpression seOnlyExpr) { // The recursive call handles a nested call such as `x.getA().getB()`, whose receiver is // itself a method call. return seOnlyExpr.containsSyntacticEqualJavaExpression(input)