Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

[WIP] Add support for Preconditions.checkArgument(...) #607

Closed
wants to merge 3 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -248,6 +248,7 @@ public TransferResult<Nullness, NullnessStore> visitCharacterLiteral(
@Override
public TransferResult<Nullness, NullnessStore> visitStringLiteral(
StringLiteralNode stringLiteralNode, TransferInput<Nullness, NullnessStore> input) {
handler.ondataflowVisitStringLiteral(stringLiteralNode, input);
return noStoreChanges(NONNULL, input);
}

Expand Down Expand Up @@ -897,7 +898,7 @@ public TransferResult<Nullness, NullnessStore> visitMethodInvocation(
state.getTypes(),
state.context,
apContext,
values(input),
input,
thenUpdates,
elseUpdates,
bothUpdates);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,13 @@
import com.uber.nullaway.Nullness;
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import java.util.Objects;
import java.util.Optional;
import javax.annotation.Nullable;
import javax.lang.model.element.Element;
import javax.lang.model.element.ElementKind;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.Node;

Expand Down Expand Up @@ -71,7 +73,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,12 @@
import com.sun.tools.javac.code.Symbol;
import com.sun.tools.javac.code.Types;
import com.sun.tools.javac.util.Context;
import com.uber.nullaway.Nullness;
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import java.util.List;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.Node;

Expand All @@ -49,7 +52,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -36,15 +36,18 @@
import com.sun.tools.javac.util.Context;
import com.uber.nullaway.ErrorMessage;
import com.uber.nullaway.NullAway;
import com.uber.nullaway.Nullness;
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessAnalysis;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import java.util.List;
import java.util.Optional;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.UnderlyingAST;
import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.StringLiteralNode;

/**
* Provides a default (No-Op) implementation of every method defined by the Handler interface.
Expand Down Expand Up @@ -152,7 +155,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
Expand Down Expand Up @@ -193,4 +196,10 @@ public void onNonNullFieldAssignment(
Symbol field, AccessPathNullnessAnalysis analysis, VisitorState state) {
// NoOp
}

@Override
public void ondataflowVisitStringLiteral(
StringLiteralNode node, TransferInput<Nullness, NullnessStore> input) {
// NoOp
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -37,15 +37,18 @@
import com.sun.tools.javac.util.Context;
import com.uber.nullaway.ErrorMessage;
import com.uber.nullaway.NullAway;
import com.uber.nullaway.Nullness;
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessAnalysis;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import java.util.List;
import java.util.Optional;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.UnderlyingAST;
import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.StringLiteralNode;

/**
* Registry of all handlers registered on our analysis.
Expand Down Expand Up @@ -183,15 +186,15 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
NullnessHint nullnessHint = NullnessHint.UNKNOWN;
for (Handler h : handlers) {
NullnessHint n =
h.onDataflowVisitMethodInvocation(
node, types, context, apContext, inputs, thenUpdates, elseUpdates, bothUpdates);
node, types, context, apContext, input, thenUpdates, elseUpdates, bothUpdates);
nullnessHint = nullnessHint.merge(n);
}
return nullnessHint;
Expand Down Expand Up @@ -251,4 +254,12 @@ public void onNonNullFieldAssignment(
h.onNonNullFieldAssignment(field, analysis, state);
}
}

@Override
public void ondataflowVisitStringLiteral(
StringLiteralNode node, TransferInput<Nullness, NullnessStore> input) {
for (Handler h : handlers) {
h.ondataflowVisitStringLiteral(node, input);
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -39,13 +39,15 @@
import com.uber.nullaway.Nullness;
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
import javax.annotation.Nullable;
import javax.lang.model.element.Element;
import javax.lang.model.element.ElementKind;
import javax.lang.model.type.TypeKind;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.Node;

Expand Down Expand Up @@ -83,7 +85,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,11 @@
import com.uber.nullaway.dataflow.NullnessStore;
import java.util.List;
import java.util.Optional;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.UnderlyingAST;
import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.StringLiteralNode;

/**
* The general interface representing a handler.
Expand Down Expand Up @@ -224,7 +226,7 @@ NullnessStore.Builder onDataflowInitialStore(
* @param types {@link Types} for the current compilation
* @param apContext the current access path context information (see {@link
* AccessPath.AccessPathContext}).
* @param inputs NullnessStore information known before the method invocation.
* @param input Nullness and NullnessStore information known before the method invocation.
* @param thenUpdates NullnessStore updates to be added along the then path, handlers can add via
* the set() method.
* @param elseUpdates NullnessStore updates to be added along the else path, handlers can add via
Expand All @@ -240,7 +242,7 @@ NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates);
Expand Down Expand Up @@ -325,6 +327,9 @@ Optional<ErrorMessage> onExpressionDereference(
void onNonNullFieldAssignment(
Symbol field, AccessPathNullnessAnalysis analysis, VisitorState state);

void ondataflowVisitStringLiteral(
StringLiteralNode node, TransferInput<Nullness, NullnessStore> input);

/**
* A three value enum for handlers implementing onDataflowVisitMethodInvocation to communicate
* their knowledge of the method return nullability to the the rest of NullAway.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ public static Handler buildDefault(Config config) {
handlerListBuilder.add(new GrpcHandler());
handlerListBuilder.add(new RequiresNonNullHandler());
handlerListBuilder.add(new EnsuresNonNullHandler());
handlerListBuilder.add(new PreconditionsHandler());
if (config.serializationIsActive() && config.getSerializationConfig().fieldInitInfoEnabled) {
handlerListBuilder.add(
new FieldInitializationSerializationHandler(config.getSerializationConfig()));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,10 @@
import com.sun.tools.javac.util.Context;
import com.uber.nullaway.Config;
import com.uber.nullaway.NullAway;
import com.uber.nullaway.Nullness;
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import com.uber.nullaway.jarinfer.JarInferStubxProvider;
import java.io.DataInputStream;
import java.io.IOException;
Expand All @@ -51,6 +53,7 @@
import javax.annotation.Nullable;
import javax.lang.model.element.Modifier;
import javax.lang.model.type.TypeKind;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;

/** This handler loads inferred nullability model from stubs for methods in unannotated packages. */
Expand Down Expand Up @@ -169,7 +172,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -43,16 +43,20 @@
import com.uber.nullaway.LibraryModels;
import com.uber.nullaway.LibraryModels.MethodRef;
import com.uber.nullaway.NullAway;
import com.uber.nullaway.Nullness;
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import java.util.ArrayList;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.ServiceLoader;
import java.util.Set;
import java.util.function.Function;
import javax.annotation.Nullable;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.Node;

Expand Down Expand Up @@ -138,7 +142,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
Expand All @@ -160,7 +164,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
// arguments is null, then the return should be non-null.
boolean anyNull = false;
for (int idx : nullImpliesNullIndexes) {
if (!inputs.valueOfSubNode(node.getArgument(idx)).equals(NONNULL)) {
if (!Objects.equals(input.getValueOfSubNode(node.getArgument(idx)), NONNULL)) {
anyNull = true;
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@
import com.uber.nullaway.dataflow.AccessPath;
import com.uber.nullaway.dataflow.AccessPathNullnessAnalysis;
import com.uber.nullaway.dataflow.AccessPathNullnessPropagation;
import com.uber.nullaway.dataflow.NullnessStore;
import java.lang.annotation.Annotation;
import java.util.List;
import java.util.Objects;
Expand All @@ -54,6 +55,7 @@
import javax.lang.model.element.Name;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeMirror;
import org.checkerframework.nullaway.dataflow.analysis.TransferInput;
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.nullaway.dataflow.cfg.node.Node;

Expand Down Expand Up @@ -108,7 +110,7 @@ public NullnessHint onDataflowVisitMethodInvocation(
Types types,
Context context,
AccessPath.AccessPathContext apContext,
AccessPathNullnessPropagation.SubNodeValues inputs,
TransferInput<Nullness, NullnessStore> input,
AccessPathNullnessPropagation.Updates thenUpdates,
AccessPathNullnessPropagation.Updates elseUpdates,
AccessPathNullnessPropagation.Updates bothUpdates) {
Expand Down
Loading