diff --git a/checker/tests/nullness/Issue406.java b/checker/tests/nullness/Issue406.java new file mode 100644 index 00000000000..edf32da8327 --- /dev/null +++ b/checker/tests/nullness/Issue406.java @@ -0,0 +1,58 @@ +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +public class Issue406 { + static class LocalDate {} + + private void testFails1(@Nullable LocalDate x1, @Nullable LocalDate x2) { + boolean eitherIsNull = x1 == null || x2 == null; + if (eitherIsNull) return; + delegate(x1, x2); + } + + private void testFails1b(@Nullable LocalDate x1, @Nullable LocalDate x2) { + boolean eitherIsNull = x1 == null || x2 == null; + if (!eitherIsNull) { + delegate(x1, x2); + } + } + + private void testFails2(@Nullable LocalDate x1, @Nullable LocalDate x2) { + boolean firstIsNull = x1 == null; + boolean secondIsNull = x2 == null; + if (firstIsNull || secondIsNull) return; + delegate(x1, x2); + } + + private void testFails2b(@Nullable LocalDate x1, @Nullable LocalDate x2) { + boolean firstIsNull = x1 == null; + boolean secondIsNull = x2 == null; + if (!firstIsNull) { + @NonNull LocalDate z = x1; + } + + if (firstIsNull || secondIsNull) return; + delegate(x1, x2); + } + + private void test3(@Nullable LocalDate x1, @Nullable LocalDate x2) { + boolean firstIsNull = x1 != null; + boolean secondIsNull = x2 != null; + if (!firstIsNull || !secondIsNull) { + // :: error: (argument) + delegate( + x1, + // :: error: (argument) + x2); + } + } + + private void testWorks(@Nullable LocalDate x1, @Nullable LocalDate x2) { + if (x1 == null || x2 == null) return; + delegate(x1, x2); + } + + private void delegate(LocalDate x1, LocalDate x2) { + // do something + } +} diff --git a/checker/tests/optional/OptionalBooleanVariableFlowRefinement.java b/checker/tests/optional/OptionalBooleanVariableFlowRefinement.java new file mode 100644 index 00000000000..2efd81b1975 --- /dev/null +++ b/checker/tests/optional/OptionalBooleanVariableFlowRefinement.java @@ -0,0 +1,36 @@ +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.optional.qual.*; +import org.checkerframework.dataflow.qual.*; + +@SuppressWarnings({"optional:parameter", "optional:field", "optional:collection"}) +class OptionalBooleanVariableFlowRefinement { + + void validRefinementTest(Optional opt) { + boolean optIsPresent = opt.isPresent(); + if (optIsPresent) { + opt.get(); // Legal + } + } + + void otherValidRefinement(OptContainer container) { + boolean isGetLegal = + container.getOptStrs().isPresent() && !container.getOptStrs().get().isEmpty(); + if (isGetLegal) { + container.getOptStrs().get(); // Legal + } + } + + class OptContainer { + private Optional> strs; + + public OptContainer(List strs) { + this.strs = Optional.ofNullable(strs); + } + + @Pure + public Optional> getOptStrs() { + return this.strs; + } + } +} diff --git a/checker/tests/resourceleak/DaikonFail.java b/checker/tests/resourceleak/DaikonFail.java new file mode 100644 index 00000000000..d9cbea8257b --- /dev/null +++ b/checker/tests/resourceleak/DaikonFail.java @@ -0,0 +1,37 @@ +import java.io.File; +import java.io.PrintStream; +import org.checkerframework.checker.nullness.qual.Nullable; + +public class DaikonFail { + + public static @Nullable File generate_goals = null; + public static File diff_file = new File("InvariantFormatTest.diffs"); + + private boolean execute() { + + boolean result = performTest(); + + if (generate_goals != null) { + try { + PrintStream out_fp = new PrintStream(generate_goals); + out_fp.close(); + } catch (Exception e) { + throw new RuntimeException(); + } + } else { + if (!result) { + try { + PrintStream diff_fp = new PrintStream(diff_file); + diff_fp.close(); + } catch (Exception e) { + } + return false; + } + } + return true; + } + + private boolean performTest() { + return false; + } +} 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 54fb7004d4c..1ab11ccaabf 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -9,7 +9,9 @@ import java.util.Objects; import java.util.StringJoiner; import java.util.concurrent.atomic.AtomicLong; +import java.util.function.BiFunction; import java.util.function.BinaryOperator; +import java.util.function.Consumer; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.Name; @@ -72,6 +74,71 @@ public abstract class CFAbstractStore, S extends CF /** Information collected about local variables (including method parameters). */ protected final Map localVariableValues; + /** Stores after boolean variable assignment. */ + protected final Map> booleanVarStores; + + /** + * An object that contains the then and else store after a boolean variable assignment. + * + * @param value + * @param store + */ + protected static class BooleanVarStore< + V extends CFAbstractValue, S extends CFAbstractStore> { + + /** Then store. */ + S thenStore; + + /** Else store. */ + S elseStore; + + /** + * Create a BooleanVarStore with copies of the provided {@code thenStore} and {@code elseStore}. + * + * @param thenStore thenStore + * @param elseStore elseStore + */ + BooleanVarStore(S thenStore, S elseStore) { + this.thenStore = thenStore.copy(); + this.elseStore = elseStore.copy(); + thenStore.booleanVarStores.clear(); + elseStore.booleanVarStores.clear(); + } + + /** + * Copy this. + * + * @return a copy of this + */ + public BooleanVarStore copy() { + return new BooleanVarStore<>(thenStore, elseStore); + } + + /** + * Applies {@code function} to both stores. + * + * @param function that takes a store and performs some action + */ + public void applyToStores(Consumer> function) { + function.accept(thenStore); + function.accept(elseStore); + } + + /** + * Merges this's then stores with {@code other}'s then store using {@code function}, and + * likewise for the else stores. A new {@code BooleanVarStore} is returned with the result from + * both merges. + * + * @param function a function that takes two stores and returns a store + * @param other another {@code BooleanVarStore} + * @return the merge of this and {@code other} + */ + public BooleanVarStore merge(BiFunction function, BooleanVarStore other) { + return new BooleanVarStore<>( + function.apply(thenStore, other.thenStore), function.apply(elseStore, other.elseStore)); + } + } + /** Information collected about the current object. */ protected V thisValue; @@ -142,6 +209,7 @@ public long getUid() { protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { this.analysis = analysis; this.localVariableValues = new HashMap<>(); + this.booleanVarStores = new HashMap<>(); this.thisValue = null; this.fieldValues = new HashMap<>(); this.methodCallExpressions = new HashMap<>(); @@ -162,6 +230,8 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti protected CFAbstractStore(CFAbstractStore other) { this.analysis = other.analysis; this.localVariableValues = new HashMap<>(other.localVariableValues); + this.booleanVarStores = new HashMap<>(other.booleanVarStores.size()); + other.booleanVarStores.forEach((var, store) -> this.booleanVarStores.put(var, store.copy())); this.thisValue = other.thisValue; this.fieldValues = new HashMap<>(other.fieldValues); this.methodCallExpressions = new HashMap<>(other.methodCallExpressions); @@ -258,6 +328,7 @@ public void updateForMethodCall( // isUnmodifiableByOtherCode. Example: @KeyFor("valueThatCanBeMutated"). if (sideEffectsUnrefineAliases) { localVariableValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode()); + booleanVarStores.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode()); } // update this value @@ -623,6 +694,10 @@ protected void computeNewValueAndInsert( if (!shouldInsert(expr, value, permitNondeterministic)) { return; } + for (BooleanVarStore booleanVarStore : booleanVarStores.values()) { + booleanVarStore.applyToStores( + s -> s.computeNewValueAndInsert(expr, value, merger, permitNondeterministic)); + } if (expr instanceof LocalVariable) { LocalVariable localVar = (LocalVariable) expr; @@ -761,6 +836,7 @@ public void clearValue(JavaExpression expr) { if (expr instanceof LocalVariable) { LocalVariable localVar = (LocalVariable) expr; localVariableValues.remove(localVar); + booleanVarStores.remove(localVar); } else if (expr instanceof FieldAccess) { FieldAccess fieldAcc = (FieldAccess) expr; fieldValues.remove(fieldAcc); @@ -886,10 +962,20 @@ public void updateForAssignment(Node n, @Nullable V val) { JavaExpression je = JavaExpression.fromNode(n); if (je instanceof ArrayAccess) { updateForArrayAssignment((ArrayAccess) je, val); + booleanVarStores.forEach( + (var, store) -> + store.applyToStores(s -> s.updateForArrayAssignment((ArrayAccess) je, val))); } else if (je instanceof FieldAccess) { updateForFieldAccessAssignment((FieldAccess) je, val); + booleanVarStores.forEach( + (var, store) -> + store.applyToStores(s -> s.updateForFieldAccessAssignment((FieldAccess) je, val))); } else if (je instanceof LocalVariable) { updateForLocalVariableAssignment((LocalVariable) je, val); + booleanVarStores.forEach( + (var, store) -> + store.applyToStores( + s -> s.updateForLocalVariableAssignment((LocalVariable) je, val))); } else { throw new BugInCF("Unexpected je of class " + je.getClass()); } @@ -1135,6 +1221,20 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { return localVariableValues.get(new LocalVariable(el)); } + protected void insertBooleanVarStore(LocalVariable lhsExpr, BooleanVarStore other) { + booleanVarStores.put(lhsExpr, other); + } + + protected void swapBooleanVarStore() { + Map> newBooleanVarStores = + new HashMap<>(booleanVarStores.size()); + booleanVarStores.forEach( + (var, store) -> + newBooleanVarStores.put(var, new BooleanVarStore<>(store.elseStore, store.thenStore))); + booleanVarStores.clear(); + booleanVarStores.putAll(newBooleanVarStores); + } + /* --------------------------------------------------------- */ /* Handling of the current object */ /* --------------------------------------------------------- */ @@ -1175,8 +1275,8 @@ private S upperBound(S other, boolean shouldWiden) { S newStore = analysis.createEmptyStore(sequentialSemantics); for (Map.Entry e : other.localVariableValues.entrySet()) { - // local variables that are only part of one store, but not the other are discarded, as - // one of store implicitly contains 'top' for that variable. + // If a local variable appears in just one store, then the other store implicitly contains + // 'top' for that variable. Remove the variable. LocalVariable localVar = e.getKey(); V thisVal = localVariableValues.get(localVar); if (thisVal != null) { @@ -1189,6 +1289,24 @@ private S upperBound(S other, boolean shouldWiden) { } } + for (Map.Entry> e : other.booleanVarStores.entrySet()) { + // If a local variable appears in just one store, then the other store implicitly contains + // 'top' for that variable. Remove the variable. + LocalVariable localVar = e.getKey(); + BooleanVarStore store = booleanVarStores.get(localVar); + if (store != null) { + BooleanVarStore otherStore = e.getValue(); + BooleanVarStore mergedStore = + shouldWiden + ? store.merge(CFAbstractStore::widenedUpperBound, otherStore) + : store.merge(CFAbstractStore::leastUpperBound, otherStore); + + if (mergedStore != null) { + newStore.booleanVarStores.put(localVar, mergedStore); + } + } + } + // information about the current object { V otherVal = other.thisValue; @@ -1257,6 +1375,35 @@ private V upperBoundOfValues(V otherVal, V thisVal, boolean shouldWiden) { return shouldWiden ? thisVal.widenUpperBound(otherVal) : thisVal.leastUpperBound(otherVal); } + /** + * Creates a new store the has all the values from both {@code this} and {@code other}. If a node + * have a value in both stores, then the most specific one is used. + * + * @param other another store + * @return a new store with values from {@code this} and {@code other} + */ + public S mostSpecific(S other) { + S newStore = this.copy(); + other.booleanVarStores.forEach(newStore::insertBooleanVarStore); + // booleanVarStores.computeIfPresent(lhsExpr, (key, booleanVarStore) -> + // booleanVarStore.merge( + // CFAbstractStore::mostSpecific, other)); + other.localVariableValues.forEach(newStore::insertValue); + if (other.thisValue != null) { + if (newStore.thisValue == null) { + newStore.thisValue = other.thisValue; + } else { + newStore.thisValue = thisValue.mostSpecific(other.thisValue, null); + } + } + other.fieldValues.forEach(newStore::insertValue); + other.arrayValues.forEach(newStore::insertValue); + other.methodCallExpressions.forEach(newStore::insertValue); + other.classValues.forEach(newStore::insertValue); + + return newStore; + } + /** * Returns true iff this {@link CFAbstractStore} contains a superset of the map entries of the * argument {@link CFAbstractStore}. Note that we test the entry keys and values by Java equality, 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 49c56aacdec..90ff8b35b87 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -71,6 +71,7 @@ import org.checkerframework.dataflow.util.NodeUtils; import org.checkerframework.dataflow.util.PurityChecker; import org.checkerframework.framework.flow.CFAbstractAnalysis.FieldInitialValue; +import org.checkerframework.framework.flow.CFAbstractStore.BooleanVarStore; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; @@ -89,6 +90,7 @@ import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; /** * The default analysis transfer function for the Checker Framework. It propagates information @@ -777,6 +779,14 @@ public TransferResult visitLocalVariable(LocalVariableNode n, TransferInpu V valueFromStore = store.getValue(n); V valueFromFactory = getValueFromFactory(n.getTree(), n); V value = moreSpecificValue(valueFromFactory, valueFromStore); + BooleanVarStore booleanVarStore = + store.booleanVarStores.get(new LocalVariable(n.getElement())); + if (booleanVarStore != null) { + S thenStore = in.getThenStore().mostSpecific(booleanVarStore.thenStore); + S elseStore = in.getElseStore().mostSpecific(booleanVarStore.elseStore); + return new ConditionalTransferResult<>( + finishValue(value, thenStore, elseStore), thenStore, elseStore); + } return new RegularTransferResult<>(finishValue(value, store), store); } @@ -835,7 +845,10 @@ public TransferResult visitSwitchExpressionNode( public TransferResult visitConditionalNot(ConditionalNotNode n, TransferInput p) { TransferResult result = super.visitConditionalNot(n, p); S thenStore = result.getThenStore(); + thenStore.swapBooleanVarStore(); S elseStore = result.getElseStore(); + elseStore.swapBooleanVarStore(); + return new ConditionalTransferResult<>(result.getResultValue(), elseStore, thenStore); } @@ -988,7 +1001,16 @@ public TransferResult visitAssignment(AssignmentNode n, TransferInput booleanVarStore = + new BooleanVarStore<>(in.getThenStore(), in.getElseStore()); + in.getThenStore().insertBooleanVarStore(lhsExpr, booleanVarStore); + in.getElseStore().insertBooleanVarStore(lhsExpr, booleanVarStore); + } if (n.isSynthetic() && in.containsTwoStores()) { // This is a synthetic assignment node created for a ternary expression. In this case // the `then` and `else` store are not merged.