diff --git a/.ci-build.sh b/.ci-build.sh index 0285bd50..6f5e15be 100755 --- a/.ci-build.sh +++ b/.ci-build.sh @@ -92,7 +92,7 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then clone_downstream $SECURITY_GIT $SECURITY_BRANCH test_downstream $SECURITY_GIT $SECURITY_COMMAND fi - + # Universe test if [[ "${GROUP}" == "downstream-universe" ]]; then UNIVERSE_GIT=universe @@ -102,6 +102,18 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then clone_downstream $UNIVERSE_GIT $UNIVERSE_BRANCH test_downstream $UNIVERSE_GIT $UNIVERSE_COMMAND fi + + # Value inference test + if [[ "${GROUP}" == "downstream-value-inference" ]]; then + VALUE_GIT=value-inference + VALUE_BRANCH=master + VALUE_COMMAND="./gradlew build" + + ./gradlew testLibJar + + clone_downstream $VALUE_GIT $VALUE_BRANCH + test_downstream $VALUE_GIT $VALUE_COMMAND + fi fi echo Exiting "$(cd "$(dirname "$0")" && pwd -P)/$(basename "$0")" in `pwd` diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index c84d4cfc..1d518f3d 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -13,7 +13,7 @@ jobs: strategy: fail-fast: false matrix: - group: [ cfi-tests, downstream-ontology, downstream-security-demo, downstream-universe ] + group: [ cfi-tests, downstream-ontology, downstream-security-demo, downstream-universe, downstream-value-inference ] jdk: [ 8, 11 ] runs-on: ubuntu-latest steps: diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index a18e4a37..231c38cf 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -581,10 +581,7 @@ public ExistentialVariableSlot createExistentialVariableSlot(Slot potentialSlot, * @param rhsAtm atm of right operand * @return type kind of the arithmetic operation */ - private TypeKind getArithmeticResultKind(AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm) { - TypeMirror lhsType = lhsAtm.getUnderlyingType(); - TypeMirror rhsType = rhsAtm.getUnderlyingType(); - + private TypeKind getArithmeticResultKind(TypeMirror lhsType, TypeMirror rhsType) { assert (TypesUtils.isPrimitiveOrBoxed(lhsType) && TypesUtils.isPrimitiveOrBoxed(rhsType)); if (TypesUtils.isFloatingPoint(lhsType) || TypesUtils.isFloatingPoint(rhsType)) { @@ -601,7 +598,7 @@ private TypeKind getArithmeticResultKind(AnnotatedTypeMirror lhsAtm, AnnotatedTy @Override public ArithmeticVariableSlot createArithmeticVariableSlot( - AnnotationLocation location, AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm) { + AnnotationLocation location, TypeMirror lhs, TypeMirror rhs) { if (location == null || location.getKind() == AnnotationLocation.Kind.MISSING) { throw new BugInCF( "Cannot create an ArithmeticVariableSlot with a missing annotation location."); @@ -612,7 +609,7 @@ public ArithmeticVariableSlot createArithmeticVariableSlot( } // create the arithmetic var slot if it doesn't exist for the given location - TypeKind kind = getArithmeticResultKind(lhsAtm, rhsAtm); + TypeKind kind = getArithmeticResultKind(lhs, rhs); ArithmeticVariableSlot slot = new ArithmeticVariableSlot(nextId(), location, kind); addToSlots(slot); arithmeticSlotCache.put(location, slot.getId()); diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index 37cea000..65dfd967 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -155,7 +155,7 @@ public interface SlotManager { * @return the ArithmeticVariableSlot for the given location */ ArithmeticVariableSlot createArithmeticVariableSlot( - AnnotationLocation location, AnnotatedTypeMirror lhsAtm, AnnotatedTypeMirror rhsAtm); + AnnotationLocation location, TypeMirror lhsType, TypeMirror rhsType); /** * Create new ComparisonVariableSlot at the given location and return a reference to it if no diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index a13fe465..e686943f 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,95 @@ 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/ArithmeticConstraint.java b/src/checkers/inference/model/ArithmeticConstraint.java index 83074a7e..d38c7179 100644 --- a/src/checkers/inference/model/ArithmeticConstraint.java +++ b/src/checkers/inference/model/ArithmeticConstraint.java @@ -57,6 +57,16 @@ public static ArithmeticOperationKind fromTreeKind(Kind kind) { return OR; case XOR: return XOR; + case PLUS_ASSIGNMENT: + return PLUS; + case MINUS_ASSIGNMENT: + return MINUS; + case MULTIPLY_ASSIGNMENT: + return MULTIPLY; + case DIVIDE_ASSIGNMENT: + return DIVIDE; + case REMAINDER_ASSIGNMENT: + return REMAINDER; default: throw new BugInCF("There are no defined ArithmeticOperationKinds " + "for the given com.sun.source.tree.Tree.Kind: " + kind); 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/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java index 48efee7c..9a9e64bc 100644 --- a/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3smt/encoder/Z3SmtSoftConstraintEncoder.java @@ -1,19 +1,15 @@ package checkers.inference.solver.backend.z3smt.encoder; import java.util.Collection; +import java.util.logging.Logger; +import checkers.inference.InferenceMain; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; -import checkers.inference.model.ArithmeticConstraint; -import checkers.inference.model.CombineConstraint; -import checkers.inference.model.ComparableConstraint; import checkers.inference.model.Constraint; import checkers.inference.model.EqualityConstraint; -import checkers.inference.model.ExistentialConstraint; -import checkers.inference.model.ImplicationConstraint; import checkers.inference.model.InequalityConstraint; -import checkers.inference.model.PreferenceConstraint; import checkers.inference.model.SubtypeConstraint; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -22,6 +18,8 @@ public abstract class Z3SmtSoftConstraintEncoder extends Z3SmtAbstractConstraintEncoder { + private static final Logger logger = Logger.getLogger(Z3SmtSoftConstraintEncoder.class.getName()); + protected final StringBuilder softConstraints; public Z3SmtSoftConstraintEncoder( @@ -60,7 +58,11 @@ public String encodeAndGetSoftConstraints(Collection constraints) { encodeSoftInequalityConstraint((InequalityConstraint) constraint); } else { - throw new BugInCF("Soft constraint for " + constraint.getClass().getName() + " is not supported"); + if (InferenceMain.isHackMode()) { + logger.warning("Soft constraint for " + constraint.getClass().getName() + " is not supported"); + } else { + throw new BugInCF("Soft constraint for " + constraint.getClass().getName() + " is not supported"); + } } } String res = softConstraints.toString(); 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; + } + +} +