diff options
Diffstat (limited to 'third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/util/PurityChecker.java')
| -rw-r--r-- | third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/util/PurityChecker.java | 491 |
1 files changed, 0 insertions, 491 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/util/PurityChecker.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/util/PurityChecker.java deleted file mode 100644 index 0b298f1955..0000000000 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/util/PurityChecker.java +++ /dev/null @@ -1,491 +0,0 @@ -package org.checkerframework.dataflow.util; - -/*>>> -import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; -*/ - -import com.sun.source.tree.ArrayAccessTree; -import com.sun.source.tree.AssertTree; -import com.sun.source.tree.AssignmentTree; -import com.sun.source.tree.BinaryTree; -import com.sun.source.tree.BlockTree; -import com.sun.source.tree.BreakTree; -import com.sun.source.tree.CaseTree; -import com.sun.source.tree.CatchTree; -import com.sun.source.tree.ClassTree; -import com.sun.source.tree.CompoundAssignmentTree; -import com.sun.source.tree.ConditionalExpressionTree; -import com.sun.source.tree.ContinueTree; -import com.sun.source.tree.DoWhileLoopTree; -import com.sun.source.tree.EmptyStatementTree; -import com.sun.source.tree.EnhancedForLoopTree; -import com.sun.source.tree.ExpressionStatementTree; -import com.sun.source.tree.ExpressionTree; -import com.sun.source.tree.ForLoopTree; -import com.sun.source.tree.IdentifierTree; -import com.sun.source.tree.IfTree; -import com.sun.source.tree.InstanceOfTree; -import com.sun.source.tree.LabeledStatementTree; -import com.sun.source.tree.LambdaExpressionTree; -import com.sun.source.tree.LiteralTree; -import com.sun.source.tree.MemberReferenceTree; -import com.sun.source.tree.MemberSelectTree; -import com.sun.source.tree.MethodInvocationTree; -import com.sun.source.tree.NewArrayTree; -import com.sun.source.tree.NewClassTree; -import com.sun.source.tree.ParenthesizedTree; -import com.sun.source.tree.ReturnTree; -import com.sun.source.tree.SwitchTree; -import com.sun.source.tree.SynchronizedTree; -import com.sun.source.tree.ThrowTree; -import com.sun.source.tree.Tree; -import com.sun.source.tree.TryTree; -import com.sun.source.tree.TypeCastTree; -import com.sun.source.tree.UnaryTree; -import com.sun.source.tree.VariableTree; -import com.sun.source.tree.WhileLoopTree; -import com.sun.source.util.SimpleTreeVisitor; -import com.sun.tools.javac.tree.TreeScanner; -import java.util.ArrayList; -import java.util.Collection; -import java.util.EnumSet; -import java.util.List; -import javax.lang.model.element.Element; -import org.checkerframework.dataflow.qual.Deterministic; -import org.checkerframework.dataflow.qual.Pure; -import org.checkerframework.dataflow.qual.Pure.Kind; -import org.checkerframework.dataflow.qual.SideEffectFree; -import org.checkerframework.javacutil.AnnotationProvider; -import org.checkerframework.javacutil.InternalUtils; -import org.checkerframework.javacutil.Pair; -import org.checkerframework.javacutil.TreeUtils; - -/** - * A visitor that determines the purity (as defined by {@link - * org.checkerframework.dataflow.qual.SideEffectFree}, {@link - * org.checkerframework.dataflow.qual.Deterministic}, and {@link - * org.checkerframework.dataflow.qual.Pure}) of a statement or expression. The entry point is method - * {@link #checkPurity}. - * - * @see SideEffectFree - * @see Deterministic - * @see Pure - * @author Stefan Heule - */ -public class PurityChecker { - - /** - * Compute whether the given statement is side-effect-free, deterministic, or both. Returns a - * result that can be queried. - */ - public static PurityResult checkPurity( - Tree statement, AnnotationProvider annoProvider, boolean assumeSideEffectFree) { - PurityCheckerHelper helper = new PurityCheckerHelper(annoProvider, assumeSideEffectFree); - PurityResult res = helper.scan(statement, new PurityResult()); - return res; - } - - /** - * Result of the {@link PurityChecker}. Can be queried regarding whether a given tree was - * side-effect-free, deterministic, or both; also gives reasons if the answer is "no". - */ - public static class PurityResult { - - protected final List<Pair<Tree, String>> notSeFreeReasons; - protected final List<Pair<Tree, String>> notDetReasons; - protected final List<Pair<Tree, String>> notBothReasons; - protected EnumSet<Pure.Kind> types; - - public PurityResult() { - notSeFreeReasons = new ArrayList<>(); - notDetReasons = new ArrayList<>(); - notBothReasons = new ArrayList<>(); - types = EnumSet.allOf(Pure.Kind.class); - } - - public EnumSet<Pure.Kind> getTypes() { - return types; - } - - /** Is the method pure w.r.t. a given set of types? */ - public boolean isPure(Collection<Kind> kinds) { - return types.containsAll(kinds); - } - - /** Get the {@code reason}s why the method is not side-effect-free. */ - public List<Pair<Tree, String>> getNotSeFreeReasons() { - return notSeFreeReasons; - } - - /** Add {@code reason} as a reason why the method is not side-effect free. */ - public void addNotSeFreeReason(Tree t, String msgId) { - notSeFreeReasons.add(Pair.of(t, msgId)); - types.remove(Kind.SIDE_EFFECT_FREE); - } - - /** Get the {@code reason}s why the method is not deterministic. */ - public List<Pair<Tree, String>> getNotDetReasons() { - return notDetReasons; - } - - /** Add {@code reason} as a reason why the method is not deterministic. */ - public void addNotDetReason(Tree t, String msgId) { - notDetReasons.add(Pair.of(t, msgId)); - types.remove(Kind.DETERMINISTIC); - } - - /** - * Get the {@code reason}s why the method is not both side-effect-free and deterministic. - */ - public List<Pair<Tree, String>> getNotBothReasons() { - return notBothReasons; - } - - /** - * Add {@code reason} as a reason why the method is not both side-effect free and - * deterministic. - */ - public void addNotBothReason(Tree t, String msgId) { - notBothReasons.add(Pair.of(t, msgId)); - types.remove(Kind.DETERMINISTIC); - types.remove(Kind.SIDE_EFFECT_FREE); - } - } - - /** - * Helper class to keep {@link PurityChecker}'s interface clean. The implementation is heavily - * based on {@link TreeScanner}, but some parts of the AST are skipped (such as types or - * modifiers). Furthermore, scanning works differently in that the input parameter (usually - * named {@code p}) gets "threaded through", instead of using {@code reduce}. - */ - protected static class PurityCheckerHelper - extends SimpleTreeVisitor<PurityResult, PurityResult> { - - protected final AnnotationProvider annoProvider; - /** - * True if all methods should be assumed to be @SideEffectFree, for the purposes of - * org.checkerframework.dataflow analysis. - */ - private final boolean assumeSideEffectFree; - - protected /*@Nullable*/ List<Element> methodParameter; - - public PurityCheckerHelper(AnnotationProvider annoProvider, boolean assumeSideEffectFree) { - this.annoProvider = annoProvider; - this.assumeSideEffectFree = assumeSideEffectFree; - } - - /** Scan a single node. */ - public PurityResult scan(Tree node, PurityResult p) { - return node == null ? p : node.accept(this, p); - } - - /** Scan a list of nodes. */ - public PurityResult scan(Iterable<? extends Tree> nodes, PurityResult p) { - PurityResult r = p; - if (nodes != null) { - for (Tree node : nodes) { - r = scan(node, r); - } - } - return r; - } - - @Override - protected PurityResult defaultAction(Tree node, PurityResult p) { - assert false : "this type of tree is unexpected here"; - return null; - } - - @Override - public PurityResult visitClass(ClassTree node, PurityResult p) { - return p; - } - - @Override - public PurityResult visitVariable(VariableTree node, PurityResult p) { - return scan(node.getInitializer(), p); - } - - @Override - public PurityResult visitEmptyStatement(EmptyStatementTree node, PurityResult p) { - return p; - } - - @Override - public PurityResult visitBlock(BlockTree node, PurityResult p) { - return scan(node.getStatements(), p); - } - - @Override - public PurityResult visitDoWhileLoop(DoWhileLoopTree node, PurityResult p) { - PurityResult r = scan(node.getStatement(), p); - r = scan(node.getCondition(), r); - return r; - } - - @Override - public PurityResult visitWhileLoop(WhileLoopTree node, PurityResult p) { - PurityResult r = scan(node.getCondition(), p); - r = scan(node.getStatement(), r); - return r; - } - - @Override - public PurityResult visitForLoop(ForLoopTree node, PurityResult p) { - PurityResult r = scan(node.getInitializer(), p); - r = scan(node.getCondition(), r); - r = scan(node.getUpdate(), r); - r = scan(node.getStatement(), r); - return r; - } - - @Override - public PurityResult visitEnhancedForLoop(EnhancedForLoopTree node, PurityResult p) { - PurityResult r = scan(node.getVariable(), p); - r = scan(node.getExpression(), r); - r = scan(node.getStatement(), r); - return r; - } - - @Override - public PurityResult visitLabeledStatement(LabeledStatementTree node, PurityResult p) { - return scan(node.getStatement(), p); - } - - @Override - public PurityResult visitSwitch(SwitchTree node, PurityResult p) { - PurityResult r = scan(node.getExpression(), p); - r = scan(node.getCases(), r); - return r; - } - - @Override - public PurityResult visitCase(CaseTree node, PurityResult p) { - PurityResult r = scan(node.getExpression(), p); - r = scan(node.getStatements(), r); - return r; - } - - @Override - public PurityResult visitSynchronized(SynchronizedTree node, PurityResult p) { - PurityResult r = scan(node.getExpression(), p); - r = scan(node.getBlock(), r); - return r; - } - - @Override - public PurityResult visitTry(TryTree node, PurityResult p) { - PurityResult r = scan(node.getResources(), p); - r = scan(node.getBlock(), r); - r = scan(node.getCatches(), r); - r = scan(node.getFinallyBlock(), r); - return r; - } - - @Override - public PurityResult visitCatch(CatchTree node, PurityResult p) { - p.addNotDetReason(node, "catch"); - PurityResult r = scan(node.getParameter(), p); - r = scan(node.getBlock(), r); - return r; - } - - @Override - public PurityResult visitConditionalExpression( - ConditionalExpressionTree node, PurityResult p) { - PurityResult r = scan(node.getCondition(), p); - r = scan(node.getTrueExpression(), r); - r = scan(node.getFalseExpression(), r); - return r; - } - - @Override - public PurityResult visitIf(IfTree node, PurityResult p) { - PurityResult r = scan(node.getCondition(), p); - r = scan(node.getThenStatement(), r); - r = scan(node.getElseStatement(), r); - return r; - } - - @Override - public PurityResult visitExpressionStatement(ExpressionStatementTree node, PurityResult p) { - return scan(node.getExpression(), p); - } - - @Override - public PurityResult visitBreak(BreakTree node, PurityResult p) { - return p; - } - - @Override - public PurityResult visitContinue(ContinueTree node, PurityResult p) { - return p; - } - - @Override - public PurityResult visitReturn(ReturnTree node, PurityResult p) { - return scan(node.getExpression(), p); - } - - @Override - public PurityResult visitThrow(ThrowTree node, PurityResult p) { - return scan(node.getExpression(), p); - } - - @Override - public PurityResult visitAssert(AssertTree node, PurityResult p) { - PurityResult r = scan(node.getCondition(), p); - r = scan(node.getDetail(), r); - return r; - } - - @Override - public PurityResult visitMethodInvocation(MethodInvocationTree node, PurityResult p) { - Element elt = TreeUtils.elementFromUse(node); - String reason = "call"; - if (!PurityUtils.hasPurityAnnotation(annoProvider, elt)) { - p.addNotBothReason(node, reason); - } else { - boolean det = PurityUtils.isDeterministic(annoProvider, elt); - boolean seFree = - (assumeSideEffectFree || PurityUtils.isSideEffectFree(annoProvider, elt)); - if (!det && !seFree) { - p.addNotBothReason(node, reason); - } else if (!det) { - p.addNotDetReason(node, reason); - } else if (!seFree) { - p.addNotSeFreeReason(node, reason); - } - } - PurityResult r = scan(node.getMethodSelect(), p); - r = scan(node.getArguments(), r); - return r; - } - - @Override - public PurityResult visitNewClass(NewClassTree node, PurityResult p) { - Element methodElement = InternalUtils.symbol(node); - boolean sideEffectFree = - (assumeSideEffectFree - || PurityUtils.isSideEffectFree(annoProvider, methodElement)); - if (sideEffectFree) { - p.addNotDetReason(node, "object.creation"); - } else { - p.addNotBothReason(node, "object.creation"); - } - PurityResult r = scan(node.getEnclosingExpression(), p); - r = scan(node.getArguments(), r); - r = scan(node.getClassBody(), r); - return r; - } - - @Override - public PurityResult visitNewArray(NewArrayTree node, PurityResult p) { - PurityResult r = scan(node.getDimensions(), p); - r = scan(node.getInitializers(), r); - return r; - } - - @Override - public PurityResult visitLambdaExpression(LambdaExpressionTree node, PurityResult p) { - PurityResult r = scan(node.getParameters(), p); - r = scan(node.getBody(), r); - return r; - } - - @Override - public PurityResult visitParenthesized(ParenthesizedTree node, PurityResult p) { - return scan(node.getExpression(), p); - } - - @Override - public PurityResult visitAssignment(AssignmentTree node, PurityResult p) { - ExpressionTree variable = node.getVariable(); - p = assignmentCheck(p, variable); - PurityResult r = scan(variable, p); - r = scan(node.getExpression(), r); - return r; - } - - protected PurityResult assignmentCheck(PurityResult p, ExpressionTree variable) { - if (TreeUtils.isFieldAccess(variable)) { - // rhs is a field access - p.addNotBothReason(variable, "assign.field"); - } else if (variable instanceof ArrayAccessTree) { - // rhs is array access - p.addNotBothReason(variable, "assign.array"); - } else { - // rhs is a local variable - assert isLocalVariable(variable); - } - return p; - } - - protected boolean isLocalVariable(ExpressionTree variable) { - return variable instanceof IdentifierTree && !TreeUtils.isFieldAccess(variable); - } - - @Override - public PurityResult visitCompoundAssignment(CompoundAssignmentTree node, PurityResult p) { - ExpressionTree variable = node.getVariable(); - p = assignmentCheck(p, variable); - PurityResult r = scan(variable, p); - r = scan(node.getExpression(), r); - return r; - } - - @Override - public PurityResult visitUnary(UnaryTree node, PurityResult p) { - return scan(node.getExpression(), p); - } - - @Override - public PurityResult visitBinary(BinaryTree node, PurityResult p) { - PurityResult r = scan(node.getLeftOperand(), p); - r = scan(node.getRightOperand(), r); - return r; - } - - @Override - public PurityResult visitTypeCast(TypeCastTree node, PurityResult p) { - PurityResult r = scan(node.getExpression(), p); - return r; - } - - @Override - public PurityResult visitInstanceOf(InstanceOfTree node, PurityResult p) { - PurityResult r = scan(node.getExpression(), p); - return r; - } - - @Override - public PurityResult visitArrayAccess(ArrayAccessTree node, PurityResult p) { - PurityResult r = scan(node.getExpression(), p); - r = scan(node.getIndex(), r); - return r; - } - - @Override - public PurityResult visitMemberSelect(MemberSelectTree node, PurityResult p) { - return scan(node.getExpression(), p); - } - - @Override - public PurityResult visitMemberReference(MemberReferenceTree node, PurityResult p) { - assert false : "this type of tree is unexpected here"; - return null; - } - - @Override - public PurityResult visitIdentifier(IdentifierTree node, PurityResult p) { - return p; - } - - @Override - public PurityResult visitLiteral(LiteralTree node, PurityResult p) { - return p; - } - } -} |