From 2b01a930038cbef86e84373abd6fd9a68146a7fc Mon Sep 17 00:00:00 2001 From: d367wang Date: Sat, 19 Feb 2022 19:41:18 -0500 Subject: [PATCH 1/4] support refinement for conditions of comparisons --- .../inference/dataflow/InferenceTransfer.java | 97 +++++++++++++++++++ .../inference/dataflow/InferenceValue.java | 14 ++- .../inference/model/VariableSlot.java | 4 +- .../ostrusted-inferrable-test/Comparison.java | 19 ++++ 4 files changed, 130 insertions(+), 4 deletions(-) create mode 100644 testdata/ostrusted-inferrable-test/Comparison.java diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index a13fe465..bca599d1 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -1,14 +1,18 @@ package checkers.inference.dataflow; +import org.checkerframework.dataflow.analysis.ConditionalTransferResult; import org.checkerframework.dataflow.analysis.RegularTransferResult; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.EqualToNode; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.NotEqualNode; import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode; import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode; +import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFTransfer; import org.checkerframework.framework.flow.CFValue; @@ -21,6 +25,7 @@ import java.util.Map; import java.util.logging.Logger; +import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeKind; import com.sun.source.tree.Tree; @@ -31,6 +36,8 @@ import checkers.inference.SlotManager; import checkers.inference.VariableAnnotator; import checkers.inference.model.AnnotationLocation; +import checkers.inference.model.ComparisonVariableSlot; +import checkers.inference.model.ConstraintManager; import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Slot; @@ -401,4 +408,94 @@ private TransferResult storeDeclaration(Node lhs, private boolean isDeclarationWithInitializer(AssignmentNode assignmentNode) { return (assignmentNode.getTree().getKind() == Tree.Kind.VARIABLE); } + + private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore elseStore) { + // Only create refinement comparison slot for variables + // TODO: deal with comparison between more complex expressions + Node var = node; + if (node instanceof AssignmentNode) { + AssignmentNode a = (AssignmentNode) node; + var = a.getTarget(); + } + if (!(var instanceof LocalVariableNode) && !(var instanceof FieldAccessNode)) { + return; + } + Tree tree = var.getTree(); + ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + SlotManager slotManager = getInferenceAnalysis().getSlotManager(); + + AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(tree); + Slot slotToRefine = slotManager.getSlot(atm); + + // TODO: Understand why there are null slots + if (InferenceMain.isHackMode(slotToRefine == null)) { + logger.fine("HackMode: slotToRefine is null !"); + return; + } + + if (slotToRefine instanceof RefinementVariableSlot) { + slotToRefine = ((RefinementVariableSlot) slotToRefine).getRefined(); + assert !(slotToRefine instanceof RefinementVariableSlot); + } + + AnnotationLocation location = + VariableAnnotator.treeToLocation(analysis.getTypeFactory(), tree); + // TODO: find out why there are missing location + if (InferenceMain.isHackMode(location == AnnotationLocation.MISSING_LOCATION)) { + logger.fine("HackMode: create ComparisonVariableSlot on MISSING_LOCATION !"); + return; + } + ComparisonVariableSlot thenSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, true); + constraintManager.addSubtypeConstraint(thenSlot, slotToRefine); + ComparisonVariableSlot elseSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, false); + constraintManager.addSubtypeConstraint(elseSlot, slotToRefine); + + if (slotToRefine instanceof VariableSlot) { + // ComparisonVariableSlots stores the refined value after comparison, so add it to the "refinedTo" list + ((VariableSlot) slotToRefine).getRefinedToSlots().add(thenSlot); + ((VariableSlot) slotToRefine).getRefinedToSlots().add(elseSlot); + } + + AnnotationMirror thenAm = slotManager.getAnnotation(thenSlot); + AnnotationMirror elseAm = slotManager.getAnnotation(elseSlot); + + // If node is assignment, iterate over lhs; otherwise, just node. + JavaExpression rec; + rec = JavaExpression.fromNode(var); + thenStore.clearValue(rec); + thenStore.insertValue(rec, thenAm); + elseStore.clearValue(rec); + elseStore.insertValue(rec, elseAm); + } + + @Override + public TransferResult visitEqualTo( + EqualToNode n, TransferInput in) { + TransferResult result = super.visitEqualTo(n, in); + CFStore thenStore = result.getThenStore(); + CFStore elseStore = result.getElseStore(); + + createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore); + createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore); + + CFValue newResultValue = + getInferenceAnalysis() + .createAbstractValue(typeFactory.getAnnotatedType(n.getTree())); + return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore); + } + + @Override + public TransferResult visitNotEqual( + NotEqualNode n, TransferInput in) { + TransferResult result = super.visitNotEqual(n, in); + CFStore thenStore = result.getThenStore(); + CFStore elseStore = result.getElseStore(); + + createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore); + createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore); + + CFValue newResultValue = + analysis.createAbstractValue(typeFactory.getAnnotatedType(n.getTree())); + return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore); + } } diff --git a/src/checkers/inference/dataflow/InferenceValue.java b/src/checkers/inference/dataflow/InferenceValue.java index 96e98572..16c5b1fb 100644 --- a/src/checkers/inference/dataflow/InferenceValue.java +++ b/src/checkers/inference/dataflow/InferenceValue.java @@ -1,5 +1,6 @@ package checkers.inference.dataflow; +import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.util.InferenceUtil; import javax.lang.model.type.TypeVariable; import org.checkerframework.framework.flow.CFValue; @@ -153,9 +154,18 @@ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, f return other; } + if (thisSlot instanceof ComparisonVariableSlot + && ((ComparisonVariableSlot) thisSlot).getRefined().equals(otherSlot)) { + return this; + } + if (otherSlot instanceof ComparisonVariableSlot + && ((ComparisonVariableSlot) otherSlot).getRefined().equals(thisSlot)) { + return other; + } + if (thisSlot instanceof VariableSlot) { // Check if one of these has refinement variables that were merged to the other. - for (RefinementVariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) { + for (VariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) { if (slot.isMergedTo(otherSlot)) { return other; } @@ -164,7 +174,7 @@ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, f if (otherSlot instanceof VariableSlot) { // Same as above - for (RefinementVariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) { + for (VariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) { if (slot.isMergedTo(thisSlot)) { return this; } diff --git a/src/checkers/inference/model/VariableSlot.java b/src/checkers/inference/model/VariableSlot.java index 2c7e0b0a..31f6a27d 100644 --- a/src/checkers/inference/model/VariableSlot.java +++ b/src/checkers/inference/model/VariableSlot.java @@ -31,7 +31,7 @@ public abstract class VariableSlot extends Slot { private AnnotationLocation location; /** Refinement variables that refine this slot. */ - private final Set refinedToSlots = new HashSet<>(); + private final Set refinedToSlots = new HashSet<>(); /** * Create a Slot with the given annotation location. @@ -53,7 +53,7 @@ public void setLocation(AnnotationLocation location) { this.location = location; } - public Set getRefinedToSlots() { + public Set getRefinedToSlots() { return refinedToSlots; } diff --git a/testdata/ostrusted-inferrable-test/Comparison.java b/testdata/ostrusted-inferrable-test/Comparison.java new file mode 100644 index 00000000..3168440a --- /dev/null +++ b/testdata/ostrusted-inferrable-test/Comparison.java @@ -0,0 +1,19 @@ +import ostrusted.qual.OsTrusted; +import ostrusted.qual.OsUntrusted; + +public class Comparison { + + void foo(@OsUntrusted Object o) { + if (o == null) { + bar(o); + } + } + + @OsTrusted + Object bar(Object o) { + // :: fixable-error: (return.type.incompatible) + return o; + } + +} + From 5ebcb2af1062773a1f0cc38fb7e63ca2cb4a2984 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sun, 6 Mar 2022 19:53:54 -0500 Subject: [PATCH 2/4] add doc; small refactor --- .../inference/dataflow/InferenceTransfer.java | 27 ++++++++++++------- .../inference/model/VariableSlot.java | 3 ++- 2 files changed, 19 insertions(+), 11 deletions(-) diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index bca599d1..5865310f 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -409,18 +409,25 @@ private boolean isDeclarationWithInitializer(AssignmentNode assignmentNode) { return (assignmentNode.getTree().getKind() == Tree.Kind.VARIABLE); } + /** + * Create one {@link ComparisonVariableSlot} for one operand of a comparison for each of the then store + * and else store separately. + * @param node a CFG node representing one operand of a comparison + * @param thenStore the then store in which the value of the given node is updated + * @param elseStore the else store in which the value of the given node is updated + */ private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore elseStore) { // Only create refinement comparison slot for variables // TODO: deal with comparison between more complex expressions - Node var = node; + Node targetNode = node; if (node instanceof AssignmentNode) { AssignmentNode a = (AssignmentNode) node; - var = a.getTarget(); + targetNode = a.getTarget(); } - if (!(var instanceof LocalVariableNode) && !(var instanceof FieldAccessNode)) { + if (!(targetNode instanceof LocalVariableNode) && !(targetNode instanceof FieldAccessNode)) { return; } - Tree tree = var.getTree(); + Tree tree = targetNode.getTree(); ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); SlotManager slotManager = getInferenceAnalysis().getSlotManager(); @@ -460,12 +467,12 @@ private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore AnnotationMirror elseAm = slotManager.getAnnotation(elseSlot); // If node is assignment, iterate over lhs; otherwise, just node. - JavaExpression rec; - rec = JavaExpression.fromNode(var); - thenStore.clearValue(rec); - thenStore.insertValue(rec, thenAm); - elseStore.clearValue(rec); - elseStore.insertValue(rec, elseAm); + JavaExpression receiver; + receiver = JavaExpression.fromNode(targetNode); + thenStore.clearValue(receiver); + thenStore.insertValue(receiver, thenAm); + elseStore.clearValue(receiver); + elseStore.insertValue(receiver, elseAm); } @Override diff --git a/src/checkers/inference/model/VariableSlot.java b/src/checkers/inference/model/VariableSlot.java index 31f6a27d..7e6891f0 100644 --- a/src/checkers/inference/model/VariableSlot.java +++ b/src/checkers/inference/model/VariableSlot.java @@ -30,7 +30,8 @@ public abstract class VariableSlot extends Slot { */ private AnnotationLocation location; - /** Refinement variables that refine this slot. */ + /** Variable slots that refine this slot, which can be {@link RefinementVariableSlot} in an assignment + * and {@link ComparisonVariableSlot} in a comparison. */ private final Set refinedToSlots = new HashSet<>(); /** From 23f12b4e393a7cceb1f595b01fa083b634878e5d Mon Sep 17 00:00:00 2001 From: d367wang Date: Sun, 20 Mar 2022 16:49:38 -0400 Subject: [PATCH 3/4] add comment --- testdata/ostrusted-inferrable-test/Comparison.java | 1 + 1 file changed, 1 insertion(+) diff --git a/testdata/ostrusted-inferrable-test/Comparison.java b/testdata/ostrusted-inferrable-test/Comparison.java index 3168440a..453b3271 100644 --- a/testdata/ostrusted-inferrable-test/Comparison.java +++ b/testdata/ostrusted-inferrable-test/Comparison.java @@ -5,6 +5,7 @@ public class Comparison { void foo(@OsUntrusted Object o) { if (o == null) { + // Literal null is @OsTrusted. By creating bar(o); } } From 1d59b435ffe2af948df8e3ef46465bb96e89703e Mon Sep 17 00:00:00 2001 From: d367wang Date: Sun, 20 Mar 2022 16:49:38 -0400 Subject: [PATCH 4/4] add comment --- testdata/ostrusted-inferrable-test/Comparison.java | 1 + 1 file changed, 1 insertion(+) diff --git a/testdata/ostrusted-inferrable-test/Comparison.java b/testdata/ostrusted-inferrable-test/Comparison.java index 3168440a..616b1f9c 100644 --- a/testdata/ostrusted-inferrable-test/Comparison.java +++ b/testdata/ostrusted-inferrable-test/Comparison.java @@ -5,6 +5,7 @@ public class Comparison { void foo(@OsUntrusted Object o) { if (o == null) { + // Literal null is @OsTrusted. `o` is refined to @OsTrusted through ComparisonConstraint. bar(o); } }