From 14a54a40d56302f17acd415b20386e5352f35232 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sat, 5 Jun 2021 23:35:41 -0400 Subject: [PATCH 01/10] work on top of opprop/checker-framework-inference --- .../ValueInferenceAnnotatedTypeFactory.java | 10 ++++---- src/value/ValueInferenceTransfer.java | 2 +- src/value/ValueVisitor.java | 12 ++++----- src/value/solver/ValueFormatTranslator.java | 25 ++++++------------- .../ValueArithmeticConstraintEncoder.java | 19 +++++++------- .../ValueComparableConstraintEncoder.java | 7 +++--- .../ValueComparisonConstraintEncoder.java | 9 ++++--- .../ValueEqualityConstraintEncoder.java | 7 +++--- .../ValueSubtypeConstraintEncoder.java | 7 +++--- .../ValueZ3SmtSoftConstraintEncoder.java | 4 +-- 10 files changed, 48 insertions(+), 54 deletions(-) diff --git a/src/value/ValueInferenceAnnotatedTypeFactory.java b/src/value/ValueInferenceAnnotatedTypeFactory.java index eedad2d..2249a8f 100644 --- a/src/value/ValueInferenceAnnotatedTypeFactory.java +++ b/src/value/ValueInferenceAnnotatedTypeFactory.java @@ -171,7 +171,7 @@ public Void visitNewClass(NewClassTree newClassTree, AnnotatedTypeMirror atm) { Slot varSlotForPolyReturn = variableAnnotator.getOrCreatePolyVar(newClassTree); // 2) the call site return type: "@m" in "new @m Clazz(...)" - Slot callSiteReturnVarSlot = slotManager.getVariableSlot(atm); + Slot callSiteReturnVarSlot = slotManager.getSlot(atm); // Create a subtype constraint: callSiteReturnVarSlot <: varSlotForPolyReturn // since after annotation insertion, the varSlotForPolyReturn is conceptually a @@ -210,7 +210,7 @@ private void replaceATM(AnnotatedTypeMirror atm, AnnotationMirror am) { // see if given annotation mirror is the VarAnnot versions of @PolyVal private boolean isPolyAnnotation(AnnotationMirror annot) { Slot slot = slotManager.getSlot(annot); - if (slot.isConstant()) { + if (slot instanceof ConstantSlot) { AnnotationMirror constant = ((ConstantSlot) slot).getValue(); return InferenceQualifierHierarchy.isPolymorphic(constant); } @@ -382,8 +382,8 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { AnnotationMirror lhsAM = lhsATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); AnnotationMirror rhsAM = rhsATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); // grab slots for the component (only for lub slot) - Slot lhs = slotManager.getVariableSlot(lhsATM); - Slot rhs = slotManager.getVariableSlot(rhsATM); + Slot lhs = slotManager.getSlot(lhsATM); + Slot rhs = slotManager.getSlot(rhsATM); Slot result; Kind kind = binaryTree.getKind(); @@ -648,7 +648,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { Set resultSet = AnnotationUtils.createAnnotationSet(); resultSet.add(resultAM); final Pair> varATMPair = - Pair.of(slotManager.getVariableSlot(atm), resultSet); + Pair.of(slotManager.getSlot(atm), resultSet); treeToVarAnnoPair.put(binaryTree, varATMPair); } } diff --git a/src/value/ValueInferenceTransfer.java b/src/value/ValueInferenceTransfer.java index 32d4ee6..220f5b5 100644 --- a/src/value/ValueInferenceTransfer.java +++ b/src/value/ValueInferenceTransfer.java @@ -62,7 +62,7 @@ private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore Tree tree = var.getTree(); ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(tree); - Slot slotToRefine = getInferenceAnalysis().getSlotManager().getVariableSlot(atm); + Slot slotToRefine = getInferenceAnalysis().getSlotManager().getSlot(atm); // TODO: Understand why there are null slots if (slotToRefine == null) { return; diff --git a/src/value/ValueVisitor.java b/src/value/ValueVisitor.java index 9f2a50c..c1abbdc 100644 --- a/src/value/ValueVisitor.java +++ b/src/value/ValueVisitor.java @@ -283,9 +283,9 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { AnnotatedTypeMirror varATM = iatf.getAnnotatedTypeLhs(tree.getVariable()); AnnotationMirror exprAMVal = exprATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); AnnotationMirror varAMVal = varATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); - Slot lhs = slotManager.getVariableSlot(exprATM); - Slot rhs = slotManager.getVariableSlot(varATM); - Slot res = slotManager.getVariableSlot(resATM); + Slot lhs = slotManager.getSlot(exprATM); + Slot rhs = slotManager.getSlot(varATM); + Slot res = slotManager.getSlot(resATM); Kind kind = tree.getKind(); switch (kind) { @@ -314,7 +314,7 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { break; } // Create LUB constraint by default default: - Slot lubSlot = slotManager.getVariableSlot(atypeFactory.getAnnotatedType(tree)); + Slot lubSlot = slotManager.getSlot(atypeFactory.getAnnotatedType(tree)); // Create LUB constraint by default constraintManager.addSubtypeConstraint(lhs, lubSlot); constraintManager.addSubtypeConstraint(rhs, lubSlot); @@ -339,7 +339,7 @@ public Void visitUnary(UnaryTree tree, Void p) { Kind kind = tree.getKind(); AnnotatedTypeMirror resType = atypeFactory.getAnnotatedType(tree.getExpression()); AnnotationMirror exprAMVal = resType.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); - Slot var = slotManager.getVariableSlot(resType); + Slot var = slotManager.getSlot(resType); switch (kind) { case UNARY_MINUS: @@ -385,7 +385,7 @@ public Void visitUnary(UnaryTree tree, Void p) { } default: // Create LUB constraint by default - Slot lubSlot = slotManager.getVariableSlot(atypeFactory.getAnnotatedType(tree)); + Slot lubSlot = slotManager.getSlot(atypeFactory.getAnnotatedType(tree)); constraintManager.addSubtypeConstraint(var, lubSlot); break; } diff --git a/src/value/solver/ValueFormatTranslator.java b/src/value/solver/ValueFormatTranslator.java index b2fd189..3a6cb61 100644 --- a/src/value/solver/ValueFormatTranslator.java +++ b/src/value/solver/ValueFormatTranslator.java @@ -2,6 +2,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; +import checkers.inference.model.SourceVariableSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; @@ -71,7 +72,7 @@ public AnnotationMirror decodeSolution( } @Override - protected Z3InferenceValue serializeVarSlot(Slot slot) { + protected Z3InferenceValue serializeVariableSlot(VariableSlot slot) { int slotID = slot.getId(); if (serializedSlots.containsKey(slotID)) { return serializedSlots.get(slotID); @@ -120,23 +121,14 @@ protected Z3InferenceValue serializeConstantSlot(ConstantSlot slot) { } @Override - public BoolExpr encodeSlotWellformnessConstraint(Slot slot) { - if (slot instanceof ConstantSlot) { - ConstantSlot cs = (ConstantSlot) slot; - AnnotationMirror anno = cs.getValue(); - // encode poly as constant trues - if (AnnotationUtils.areSameByClass(anno, PolyVal.class)) { - return ctx.mkTrue(); - } - } + public BoolExpr encodeSlotWellformednessConstraint(VariableSlot slot) { Z3InferenceValue value = slot.serialize(this); BoolExpr range = ctx.mkAnd( ctx.mkGe(value.getIntRangeLower(), ctx.mkInt(Long.MIN_VALUE)), ctx.mkLe(value.getIntRangeUpper(), ctx.mkInt(Long.MAX_VALUE))); - if (slot instanceof VariableSlot) { - VariableSlot vslot = (VariableSlot) slot; - TypeMirror type = vslot.getUnderlyingType(); + if (slot instanceof SourceVariableSlot) { + TypeMirror type = ((SourceVariableSlot) slot).getUnderlyingType(); if (type == null) { return ctx.mkAnd( // one hot @@ -300,11 +292,10 @@ public BoolExpr encodeSlotWellformnessConstraint(Slot slot) { } @Override - public BoolExpr encodeSlotPreferenceConstraint(Slot slot) { + public BoolExpr encodeSlotPreferenceConstraint(VariableSlot slot) { Z3InferenceValue value = slot.serialize(this); - if (slot instanceof VariableSlot) { - VariableSlot vslot = (VariableSlot) slot; - TypeMirror type = vslot.getUnderlyingType(); + if (slot instanceof SourceVariableSlot) { + TypeMirror type = ((SourceVariableSlot) slot).getUnderlyingType(); if (type == null) { return value.getBottomVal(); } diff --git a/src/value/solver/encoder/ValueArithmeticConstraintEncoder.java b/src/value/solver/encoder/ValueArithmeticConstraintEncoder.java index 0812ff8..e22fcd9 100644 --- a/src/value/solver/encoder/ValueArithmeticConstraintEncoder.java +++ b/src/value/solver/encoder/ValueArithmeticConstraintEncoder.java @@ -4,6 +4,7 @@ import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; +import checkers.inference.model.SourceVariableSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; @@ -66,16 +67,14 @@ protected BoolExpr encode( // Unless variable type is long, all arithmetic operations in Java are widened to int first, IntNum maxRange = ctx.mkInt(Integer.MAX_VALUE); IntNum minRange = ctx.mkInt(Integer.MIN_VALUE); - if (leftOperand instanceof VariableSlot) { - VariableSlot vslot = (VariableSlot) leftOperand; - TypeMirror type = vslot.getUnderlyingType(); + if (leftOperand instanceof SourceVariableSlot) { + TypeMirror type = ((SourceVariableSlot) leftOperand).getUnderlyingType(); if (type.getKind() == TypeKind.LONG) { maxRange = ctx.mkInt(Long.MAX_VALUE); minRange = ctx.mkInt(Long.MIN_VALUE); } - } else if (rightOperand instanceof VariableSlot) { - VariableSlot vslot = (VariableSlot) rightOperand; - TypeMirror type = vslot.getUnderlyingType(); + } else if (rightOperand instanceof SourceVariableSlot) { + TypeMirror type = ((SourceVariableSlot) rightOperand).getUnderlyingType(); if (type.getKind() == TypeKind.LONG) { maxRange = ctx.mkInt(Long.MAX_VALUE); minRange = ctx.mkInt(Long.MIN_VALUE); @@ -867,8 +866,8 @@ protected BoolExpr encode( @Override public BoolExpr encodeVariable_Variable( ArithmeticOperationKind operation, - Slot leftOperand, - Slot rightOperand, + VariableSlot leftOperand, + VariableSlot rightOperand, ArithmeticVariableSlot result) { return encode(operation, leftOperand, rightOperand, result); } @@ -876,7 +875,7 @@ public BoolExpr encodeVariable_Variable( @Override public BoolExpr encodeVariable_Constant( ArithmeticOperationKind operation, - Slot leftOperand, + VariableSlot leftOperand, ConstantSlot rightOperand, ArithmeticVariableSlot result) { return encode(operation, leftOperand, rightOperand, result); @@ -886,7 +885,7 @@ public BoolExpr encodeVariable_Constant( public BoolExpr encodeConstant_Variable( ArithmeticOperationKind operation, ConstantSlot leftOperand, - Slot rightOperand, + VariableSlot rightOperand, ArithmeticVariableSlot result) { return encode(operation, leftOperand, rightOperand, result); } diff --git a/src/value/solver/encoder/ValueComparableConstraintEncoder.java b/src/value/solver/encoder/ValueComparableConstraintEncoder.java index 21e2a0b..623476c 100644 --- a/src/value/solver/encoder/ValueComparableConstraintEncoder.java +++ b/src/value/solver/encoder/ValueComparableConstraintEncoder.java @@ -2,6 +2,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; +import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -30,17 +31,17 @@ protected BoolExpr encode(Slot fst, Slot snd) { } @Override - public BoolExpr encodeVariable_Variable(Slot fst, Slot snd) { + public BoolExpr encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { return encode(fst, snd); } @Override - public BoolExpr encodeVariable_Constant(Slot fst, ConstantSlot snd) { + public BoolExpr encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { return encode(fst, snd); } @Override - public BoolExpr encodeConstant_Variable(ConstantSlot fst, Slot snd) { + public BoolExpr encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { return encode(fst, snd); } } diff --git a/src/value/solver/encoder/ValueComparisonConstraintEncoder.java b/src/value/solver/encoder/ValueComparisonConstraintEncoder.java index 11cdf0d..53751c0 100644 --- a/src/value/solver/encoder/ValueComparisonConstraintEncoder.java +++ b/src/value/solver/encoder/ValueComparisonConstraintEncoder.java @@ -4,6 +4,7 @@ import checkers.inference.model.ComparisonVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; +import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ComparisonConstraintEncoder; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -424,8 +425,8 @@ protected BoolExpr encode( @Override public BoolExpr encodeVariable_Variable( ComparisonOperationKind operation, - Slot left, - Slot right, + VariableSlot left, + VariableSlot right, ComparisonVariableSlot result) { return encode(operation, left, right, result); } @@ -433,7 +434,7 @@ public BoolExpr encodeVariable_Variable( @Override public BoolExpr encodeVariable_Constant( ComparisonOperationKind operation, - Slot left, + VariableSlot left, ConstantSlot right, ComparisonVariableSlot result) { return encode(operation, left, right, result); @@ -443,7 +444,7 @@ public BoolExpr encodeVariable_Constant( public BoolExpr encodeConstant_Variable( ComparisonOperationKind operation, ConstantSlot left, - Slot right, + VariableSlot right, ComparisonVariableSlot result) { return ctx.mkTrue(); } diff --git a/src/value/solver/encoder/ValueEqualityConstraintEncoder.java b/src/value/solver/encoder/ValueEqualityConstraintEncoder.java index 9dd7baf..7a3578a 100644 --- a/src/value/solver/encoder/ValueEqualityConstraintEncoder.java +++ b/src/value/solver/encoder/ValueEqualityConstraintEncoder.java @@ -3,6 +3,7 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; +import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -29,12 +30,12 @@ protected BoolExpr encode(Slot fst, Slot snd) { } @Override - public BoolExpr encodeVariable_Variable(Slot fst, Slot snd) { + public BoolExpr encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { return encode(fst, snd); } @Override - public BoolExpr encodeVariable_Constant(Slot fst, ConstantSlot snd) { + public BoolExpr encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { if (fst.getLocation() == AnnotationLocation.MISSING_LOCATION) { return ctx.mkTrue(); } @@ -42,7 +43,7 @@ public BoolExpr encodeVariable_Constant(Slot fst, ConstantSlot snd) { } @Override - public BoolExpr encodeConstant_Variable(ConstantSlot fst, Slot snd) { + public BoolExpr encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { if (snd.getLocation() == AnnotationLocation.MISSING_LOCATION) { return ctx.mkTrue(); } diff --git a/src/value/solver/encoder/ValueSubtypeConstraintEncoder.java b/src/value/solver/encoder/ValueSubtypeConstraintEncoder.java index 764a08d..10c731c 100644 --- a/src/value/solver/encoder/ValueSubtypeConstraintEncoder.java +++ b/src/value/solver/encoder/ValueSubtypeConstraintEncoder.java @@ -2,6 +2,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; +import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -28,17 +29,17 @@ protected BoolExpr encode(Slot subtype, Slot supertype) { } @Override - public BoolExpr encodeVariable_Variable(Slot fst, Slot snd) { + public BoolExpr encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { return encode(fst, snd); } @Override - public BoolExpr encodeVariable_Constant(Slot fst, ConstantSlot snd) { + public BoolExpr encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { return encode(fst, snd); } @Override - public BoolExpr encodeConstant_Variable(ConstantSlot fst, Slot snd) { + public BoolExpr encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { return encode(fst, snd); } } diff --git a/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java b/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java index 411aaa0..091ca35 100644 --- a/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java +++ b/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java @@ -48,8 +48,8 @@ protected void encodeSoftSubtypeConstraint(SubtypeConstraint stc) { } private void subtypeEqPreference(SubtypeConstraint stc, int prefenceVal) { - Z3InferenceValue sub = stc.getFirst().serialize(formatTranslator); - Z3InferenceValue sup = stc.getSecond().serialize(formatTranslator); + Z3InferenceValue sub = stc.getFirst().serialize(z3SmtFormatTranslator); + Z3InferenceValue sup = stc.getSecond().serialize(z3SmtFormatTranslator); // Prefer same upper bound BoolExpr lowerBoundEq = From d1acf4b2076c302bc5f9c09ee404c938f5438b35 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 9 Jun 2021 22:11:19 -0400 Subject: [PATCH 02/10] fix bug to pass the unit tests --- src/value/ValueInferenceAnnotatedTypeFactory.java | 7 ------- tests/value/ValueInferenceTest.java | 2 ++ 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/value/ValueInferenceAnnotatedTypeFactory.java b/src/value/ValueInferenceAnnotatedTypeFactory.java index 2249a8f..e0a1980 100644 --- a/src/value/ValueInferenceAnnotatedTypeFactory.java +++ b/src/value/ValueInferenceAnnotatedTypeFactory.java @@ -302,13 +302,6 @@ public Set leastUpperBounds( } } - @Override - protected Set getDefaultTypeDeclarationBounds() { - Set top = new HashSet<>(); - top.add(UNKNOWNVAL); - return top; - } - /** * The domain of the Constant Value Checker: the types for which it estimates possible values. */ diff --git a/tests/value/ValueInferenceTest.java b/tests/value/ValueInferenceTest.java index e228bec..eeb69d0 100644 --- a/tests/value/ValueInferenceTest.java +++ b/tests/value/ValueInferenceTest.java @@ -1,3 +1,5 @@ +package value; + import checkers.inference.test.CFInferenceTest; import java.io.File; import java.util.ArrayList; From a04531fb6d5bec516adf91175b602e5538d791ae Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 2 Sep 2021 04:08:04 -0400 Subject: [PATCH 03/10] support eisop updates on CF&CFI --- src/value/ValueAnnotatedTypeFactory.java | 114 ++++++++-- src/value/ValueChecker.java | 4 +- .../ValueInferenceAnnotatedTypeFactory.java | 50 +++-- src/value/ValueInferenceTransfer.java | 10 +- src/value/ValueTransfer.java | 5 +- src/value/ValueUtils.java | 195 ++++++++++++++++++ 6 files changed, 335 insertions(+), 43 deletions(-) create mode 100644 src/value/ValueUtils.java diff --git a/src/value/ValueAnnotatedTypeFactory.java b/src/value/ValueAnnotatedTypeFactory.java index 3d51847..0885df3 100644 --- a/src/value/ValueAnnotatedTypeFactory.java +++ b/src/value/ValueAnnotatedTypeFactory.java @@ -1,5 +1,6 @@ package value; +import checkers.inference.BaseInferenceRealTypeFactory; import com.sun.source.tree.LiteralTree; import com.sun.source.tree.NewArrayTree; import com.sun.source.tree.Tree; @@ -14,13 +15,23 @@ import java.util.List; import java.util.Set; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.ExecutableElement; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.common.value.ValueCheckerUtils; +import org.checkerframework.common.value.qual.ArrayLen; +import org.checkerframework.common.value.qual.ArrayLenRange; +import org.checkerframework.common.value.qual.DoubleVal; +import org.checkerframework.common.value.qual.IntRangeFromGTENegativeOne; +import org.checkerframework.common.value.qual.IntRangeFromNonNegative; +import org.checkerframework.common.value.qual.IntRangeFromPositive; import org.checkerframework.common.value.qual.IntVal; +import org.checkerframework.common.value.qual.MatchesRegex; +import org.checkerframework.common.value.qual.MinLen; +import org.checkerframework.common.value.qual.MinLenFieldInvariant; +import org.checkerframework.common.value.qual.PolyValue; import org.checkerframework.common.value.util.NumberUtils; import org.checkerframework.common.value.util.Range; import org.checkerframework.framework.flow.CFAbstractAnalysis; @@ -45,6 +56,7 @@ import org.checkerframework.framework.util.defaults.QualifierDefaults; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypesUtils; import value.qual.BoolVal; import value.qual.BottomVal; @@ -53,7 +65,9 @@ import value.qual.StringVal; import value.qual.UnknownVal; -public class ValueAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { +import org.plumelib.util.CollectionsPlume; + +public class ValueAnnotatedTypeFactory extends BaseInferenceRealTypeFactory { /** The maximum number of values allowed in an annotation's array. */ protected static final int MAX_VALUES = 10; @@ -73,8 +87,31 @@ public class ValueAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { /** The polymorphic type for this hierarchy. */ protected final AnnotationMirror POLYVAL = AnnotationBuilder.fromClass(elements, PolyVal.class); - public ValueAnnotatedTypeFactory(BaseTypeChecker checker) { - super(checker); + /** Fully-qualified class name of {@link org.checkerframework.common.value.qual.BottomVal}. */ + public static final String BOTTOMVAL_NAME = "org.checkerframework.common.value.qual.BottomVal"; + /** Fully-qualified class name of {@link org.checkerframework.common.value.qual.BoolVal}. */ + public static final String BOOLVAL_NAME = "org.checkerframework.common.value.qual.BoolVal"; + /** Fully-qualified class name of {@link IntVal}. */ + public static final String INTVAL_NAME = "org.checkerframework.common.value.qual.IntVal"; + /** Fully-qualified class name of {@link org.checkerframework.common.value.qual.StringVal}. */ + public static final String STRINGVAL_NAME = "org.checkerframework.common.value.qual.StringVal"; + /** Fully-qualified class name of {@link org.checkerframework.common.value.qual.IntRange}. */ + public static final String INTRANGE_NAME = "org.checkerframework.common.value.qual.IntRange"; + + + /** The value() element/field of a @BoolVal annotation. */ + protected final ExecutableElement boolValValueElement = + TreeUtils.getMethod(org.checkerframework.common.value.qual.BoolVal.class, "value", 0, processingEnv); + /** The value() element/field of a @IntVal annotation. */ + protected final ExecutableElement intValValueElement = + TreeUtils.getMethod(IntVal.class, "value", 0, processingEnv); + /** The value() element/field of a @StringVal annotation. */ + public final ExecutableElement stringValValueElement = + TreeUtils.getMethod(org.checkerframework.common.value.qual.StringVal.class, "value", 0, processingEnv); + + + public ValueAnnotatedTypeFactory(BaseTypeChecker checker, boolean isInfer) { + super(checker, isInfer); postInit(); } @@ -132,8 +169,17 @@ public AnnotationMirror canonicalAnnotation(AnnotationMirror anno) { return super.canonicalAnnotation(anno); } + @SuppressWarnings("deprecation") @Override - public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { + public QualifierHierarchy createQualifierHierarchy() { + return MultiGraphQualifierHierarchy + .createMultiGraphQualifierHierarchy(this); + } + + @SuppressWarnings("deprecation") + @Override + public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory( + MultiGraphFactory factory) { return new ValueQualifierHierarchy(factory); } @@ -177,7 +223,7 @@ public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2 if (AnnotationUtils.areSameByName(a1, a2)) { // If both are the same type, determine the type and merge - if (AnnotationUtils.areSameByClass(a1, IntRange.class)) { + if (areSameByClass(a1, IntRange.class)) { // special handling for IntRange long from1 = AnnotationUtils.getElementValue(a1, "from", Long.class, true); long to1 = AnnotationUtils.getElementValue(a1, "to", Long.class, true); @@ -223,7 +269,7 @@ else if (AnnotationUtils.areSame(subAnno, POLYVAL)) { return true; } else if (AnnotationUtils.areSameByName(superAnno, subAnno)) { // Same type, so might be subtype - if (AnnotationUtils.areSameByClass(subAnno, IntRange.class)) { + if (areSameByClass(subAnno, IntRange.class)) { // Special case for range-based annotations Range sub = getRange(subAnno); Range sup = getRange(superAnno); @@ -239,7 +285,7 @@ else if (AnnotationUtils.areSame(subAnno, POLYVAL)) { public AnnotationMirror widenedUpperBound( AnnotationMirror newQualifier, AnnotationMirror previousQualifier) { AnnotationMirror lub = leastUpperBound(newQualifier, previousQualifier); - if (AnnotationUtils.areSameByClass(lub, IntRange.class)) { + if (areSameByClass(lub, IntRange.class)) { Range lubRange = getRange(lub); Range newRange = getRange(newQualifier); Range oldRange = getRange(previousQualifier); @@ -626,7 +672,7 @@ public Void visitTypeCast(TypeCastTree tree, AnnotatedTypeMirror atm) { newAnno = oldAnno; } else if (AnnotationUtils.areSameByClass(oldAnno, IntRange.class) && (range = getRange(oldAnno)).isWiderThan(MAX_VALUES)) { - Class newClass = ValueCheckerUtils.getClassFromType(newType); + Class newClass = TypesUtils.getClassFromType(newType); if (newClass == String.class) { newAnno = UNKNOWNVAL; } else if (newClass == Boolean.class || newClass == boolean.class) { @@ -636,7 +682,7 @@ public Void visitTypeCast(TypeCastTree tree, AnnotatedTypeMirror atm) { newAnno = createIntRangeAnnotation(NumberUtils.castRange(newType, range)); } } else { - List values = ValueCheckerUtils.getValuesCastedToType(oldAnno, newType); + List values = ValueUtils.getValuesCastedToType(oldAnno, newType, ValueAnnotatedTypeFactory.this); newAnno = createResultingAnnotation(atm.getUnderlyingType(), values); } atm.addMissingAnnotations(Collections.singleton(newAnno)); @@ -680,7 +726,7 @@ AnnotationMirror createResultingAnnotation(TypeMirror resultType, List values stringVals.add((String) o); } return createStringAnnotation(stringVals); - } else if (ValueCheckerUtils.getClassFromType(resultType) == char[].class) { + } else if (TypesUtils.getClassFromType(resultType) == char[].class) { List stringVals = new ArrayList<>(values.size()); for (Object o : values) { if (o instanceof char[]) { @@ -857,7 +903,7 @@ public AnnotationMirror createIntRangeAnnotation(Range range) { } else if (range.isWiderThan(MAX_VALUES)) { return createIntRangeAnnotation(range.from, range.to); } else { - List newValues = ValueCheckerUtils.getValuesFromRange(range, Long.class); + List newValues = ValueUtils.getValuesFromRange(range, Long.class); return createIntValAnnotation(newValues); } } @@ -879,7 +925,7 @@ private AnnotationMirror createIntRangeAnnotation(long from, long to) { * anno}. */ private AnnotationMirror convertToUnknown(AnnotationMirror anno) { - if (AnnotationUtils.areSameByClass(anno, IntRange.class)) { + if (areSameByClass(anno, IntRange.class)) { long from = AnnotationUtils.getElementValue(anno, "from", Long.class, true); long to = AnnotationUtils.getElementValue(anno, "to", Long.class, true); if (from == Long.MIN_VALUE && to == Long.MAX_VALUE) { @@ -888,4 +934,46 @@ private AnnotationMirror convertToUnknown(AnnotationMirror anno) { } return anno; } + + /** + * Returns the set of possible values as a sorted list with no duplicate values. Returns the + * empty list if no values are possible (for dead code). Returns null if any value is possible + * -- that is, if no estimate can be made -- and this includes when there is no constant-value + * annotation so the argument is null. + * + *

The method returns a list of {@code Long} but is named {@code getIntValues} because it + * supports the {@code @IntVal} annotation. + * + * @param intAnno an {@code @IntVal} annotation, or null + * @return the possible values, deduplicated and sorted + */ + public List getIntValues(AnnotationMirror intAnno) { + if (intAnno == null) { + return null; + } + List list = + AnnotationUtils.getElementValueArray(intAnno, intValValueElement, Long.class); + list = CollectionsPlume.withoutDuplicates(list); + return list; + } + + /** + * Returns the set of possible values as a sorted list with no duplicate values. Returns the + * empty list if no values are possible (for dead code). Returns null if any value is possible + * -- that is, if no estimate can be made -- and this includes when there is no constant-value + * annotation so the argument is null. + * + * @param stringAnno a {@code @StringVal} annotation, or null + * @return the possible values, deduplicated and sorted + */ + public List getStringValues(AnnotationMirror stringAnno) { + if (stringAnno == null) { + return null; + } + List list = + AnnotationUtils.getElementValueArray( + stringAnno, stringValValueElement, String.class); + list = CollectionsPlume.withoutDuplicates(list); + return list; + } } diff --git a/src/value/ValueChecker.java b/src/value/ValueChecker.java index 896d703..b510c60 100644 --- a/src/value/ValueChecker.java +++ b/src/value/ValueChecker.java @@ -32,8 +32,8 @@ public ValueVisitor createVisitor( } @Override - public ValueAnnotatedTypeFactory createRealTypeFactory() { - return new ValueAnnotatedTypeFactory(this); + public ValueAnnotatedTypeFactory createRealTypeFactory(boolean infer) { + return new ValueAnnotatedTypeFactory(this, infer); } @Override diff --git a/src/value/ValueInferenceAnnotatedTypeFactory.java b/src/value/ValueInferenceAnnotatedTypeFactory.java index e0a1980..7a3f56c 100644 --- a/src/value/ValueInferenceAnnotatedTypeFactory.java +++ b/src/value/ValueInferenceAnnotatedTypeFactory.java @@ -36,7 +36,6 @@ import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.common.value.ValueCheckerUtils; import org.checkerframework.common.value.util.Range; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -45,6 +44,7 @@ import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.framework.util.MultiGraphQualifierHierarchy; import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; @@ -212,7 +212,7 @@ private boolean isPolyAnnotation(AnnotationMirror annot) { Slot slot = slotManager.getSlot(annot); if (slot instanceof ConstantSlot) { AnnotationMirror constant = ((ConstantSlot) slot).getValue(); - return InferenceQualifierHierarchy.isPolymorphic(constant); + return getQualifierHierarchy().isPolymorphicQualifier(constant); } return false; } @@ -274,14 +274,23 @@ private boolean isMethodDeclaredWithPolymorphicReturn( } } + @SuppressWarnings("deprecation") @Override - public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { + public QualifierHierarchy createQualifierHierarchy() { + return MultiGraphQualifierHierarchy + .createMultiGraphQualifierHierarchy(this); + } + + @SuppressWarnings("deprecation") + @Override + public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory( + MultiGraphFactory factory) { return new ValueInferenceQualifierHierarchy(factory); } private final class ValueInferenceQualifierHierarchy extends InferenceQualifierHierarchy { - public ValueInferenceQualifierHierarchy(MultiGraphFactory multiGraphFactory) { - super(multiGraphFactory); + public ValueInferenceQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory multiGraphFactory) { + super(getSupportedTypeQualifiers(), elements); } @Override @@ -352,8 +361,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { // create varslot for the result of the binary tree computation // note: constraints for binary ops are added in Visitor if (this.treeToVarAnnoPair.containsKey(binaryTree)) { - atm.replaceAnnotations( - (Iterable) ((Pair) this.treeToVarAnnoPair.get(binaryTree)).second); + atm.replaceAnnotations(treeToVarAnnoPair.get(binaryTree).second); } else { // TODO: find out why there are missing location AnnotationLocation location = @@ -408,7 +416,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case MINUS: if (lhsAM == null || rhsAM == null) { @@ -429,7 +437,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case MULTIPLY: if (lhsAM == null || rhsAM == null) { @@ -450,7 +458,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case DIVIDE: if (lhsAM == null || rhsAM == null) { @@ -471,7 +479,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case REMAINDER: if (lhsAM == null || rhsAM == null) { @@ -492,7 +500,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case LEFT_SHIFT: if (lhsAM == null || rhsAM == null) { @@ -513,7 +521,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case RIGHT_SHIFT: if (lhsAM == null || rhsAM == null) { @@ -534,7 +542,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case UNSIGNED_RIGHT_SHIFT: if (lhsAM == null || rhsAM == null) { @@ -555,7 +563,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case AND: if (lhsAM == null || rhsAM == null) { @@ -576,7 +584,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case OR: if (lhsAM == null || rhsAM == null) { @@ -597,7 +605,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case XOR: if (lhsAM == null || rhsAM == null) { @@ -618,7 +626,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { slotManager.createConstantSlot(createIntRangeAnnotation(range)); break; } - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; case GREATER_THAN: case GREATER_THAN_EQUAL: @@ -629,13 +637,13 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { result = slotManager.createConstantSlot(UNKNOWNVAL); break; default: - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; } // insert varAnnot of the slot into the ATM AnnotationMirror resultAM = slotManager.getAnnotation(result); - atm.clearAnnotations(); + atm.clearPrimaryAnnotations(); atm.replaceAnnotation(resultAM); Set resultSet = AnnotationUtils.createAnnotationSet(); @@ -678,7 +686,7 @@ AnnotationMirror createResultingAnnotation(TypeMirror resultType, List values stringVals.add((String) o); } return createStringAnnotation(stringVals); - } else if (ValueCheckerUtils.getClassFromType(resultType) == char[].class) { + } else if (TypesUtils.getClassFromType(resultType) == char[].class) { List stringVals = new ArrayList<>(values.size()); for (Object o : values) { if (o instanceof char[]) { diff --git a/src/value/ValueInferenceTransfer.java b/src/value/ValueInferenceTransfer.java index 220f5b5..aa9ed35 100644 --- a/src/value/ValueInferenceTransfer.java +++ b/src/value/ValueInferenceTransfer.java @@ -16,8 +16,7 @@ import java.util.Set; import javax.lang.model.element.AnnotationMirror; import org.checkerframework.dataflow.analysis.ConditionalTransferResult; -import org.checkerframework.dataflow.analysis.FlowExpressions; -import org.checkerframework.dataflow.analysis.FlowExpressions.Receiver; +import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.analysis.RegularTransferResult; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; @@ -31,6 +30,7 @@ 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.expression.JavaExpression; import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFValue; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -94,8 +94,8 @@ private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore AnnotationMirror elseAm = getInferenceAnalysis().getSlotManager().getAnnotation(elseSlot); // If node is assignment, iterate over lhs; otherwise, just node. - Receiver rec; - rec = FlowExpressions.internalReprOf(getInferenceAnalysis().getTypeFactory(), var); + JavaExpression rec; + rec = JavaExpression.fromNode(var); thenStore.clearValue(rec); thenStore.insertValue(rec, thenAm); elseStore.clearValue(rec); @@ -198,7 +198,7 @@ public TransferResult visitLocalVariable( LocalVariableNode n, TransferInput in) { TransferResult result = super.visitLocalVariable(n, in); CFStore store = result.getRegularStore(); - Receiver rec = FlowExpressions.internalReprOf(getInferenceAnalysis().getTypeFactory(), n); + JavaExpression rec = JavaExpression.fromNode(n); CFValue value = store.getValue(rec); if (value == null) { diff --git a/src/value/ValueTransfer.java b/src/value/ValueTransfer.java index d80b9f2..949e6c1 100644 --- a/src/value/ValueTransfer.java +++ b/src/value/ValueTransfer.java @@ -17,6 +17,7 @@ import org.checkerframework.framework.flow.CFValue; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.TypeKindUtils; import org.checkerframework.javacutil.TypesUtils; /** Transfer function for value inference. Please also check {@link ValueInferenceTransfer}. */ @@ -127,8 +128,8 @@ private Range calculateRangeBinaryOp( Node rightNode, NumericalBinaryOps op, TransferInput p) { - if (TypesUtils.isIntegral(leftNode.getType()) - && TypesUtils.isIntegral(rightNode.getType())) { + if (TypeKindUtils.isIntegral(leftNode.getType().getKind()) + && TypeKindUtils.isIntegral(rightNode.getType().getKind())) { Range leftRange = getIntRange(leftNode, p); Range rightRange = getIntRange(rightNode, p); Range resultRange; diff --git a/src/value/ValueUtils.java b/src/value/ValueUtils.java new file mode 100644 index 0000000..e54290c --- /dev/null +++ b/src/value/ValueUtils.java @@ -0,0 +1,195 @@ +package value; + +import com.sun.source.tree.Tree; +import org.checkerframework.common.value.JavaExpressionOptimizer; +import org.checkerframework.common.value.ValueChecker; +import org.checkerframework.common.value.qual.IntRange; +import org.checkerframework.common.value.qual.IntVal; +import org.checkerframework.common.value.qual.StringVal; +import org.checkerframework.common.value.util.NumberUtils; +import org.checkerframework.common.value.util.Range; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.TypeSystemError; +import org.checkerframework.javacutil.TypesUtils; +import org.plumelib.util.CollectionsPlume; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.type.TypeMirror; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +/** Utility methods for the Value Checker. */ +public class ValueUtils { + + /** Do not instantiate. */ + private ValueUtils() { + throw new TypeSystemError("do not instantiate"); + } + + /** + * Get a list of values of annotation, and then cast them to a given type. + * + * @param anno the annotation that contains values + * @param castTo the type that is casted to + * @param atypeFactory the type factory + * @return a list of values after the casting + */ + public static List getValuesCastedToType( + AnnotationMirror anno, TypeMirror castTo, ValueAnnotatedTypeFactory atypeFactory) { + Class castType = TypesUtils.getClassFromType(castTo); + List values; + switch (AnnotationUtils.annotationName(anno)) { + case ValueAnnotatedTypeFactory.INTVAL_NAME: + List longs = atypeFactory.getIntValues(anno); + values = convertIntVal(longs, castType, castTo); + break; + case ValueAnnotatedTypeFactory.INTRANGE_NAME: + Range range = atypeFactory.getRange(anno); + List rangeValues = getValuesFromRange(range, Long.class); + values = convertIntVal(rangeValues, castType, castTo); + break; + case ValueAnnotatedTypeFactory.STRINGVAL_NAME: + values = convertStringVal(anno, castType, atypeFactory); + break; + case ValueAnnotatedTypeFactory.BOOLVAL_NAME: + values = convertBoolVal(anno, castType, atypeFactory); + break; + case ValueAnnotatedTypeFactory.BOTTOMVAL_NAME: + default: + values = null; + } + return values; + } + + /** + * Converts a long value to a boxed numeric type. + * + * @param value a long value + * @param expectedType the boxed numeric type of the result + * @return {@code value} converted to {@code expectedType} using standard conversion rules + */ + private static T convertLongToType(long value, Class expectedType) { + Object convertedValue; + if (expectedType == Integer.class) { + convertedValue = (int) value; + } else if (expectedType == Short.class) { + convertedValue = (short) value; + } else if (expectedType == Byte.class) { + convertedValue = (byte) value; + } else if (expectedType == Long.class) { + convertedValue = value; + } else if (expectedType == Double.class) { + convertedValue = (double) value; + } else if (expectedType == Float.class) { + convertedValue = (float) value; + } else if (expectedType == Character.class) { + convertedValue = (char) value; + } else { + throw new UnsupportedOperationException( + "ValueCheckerUtils: unexpected class: " + expectedType); + } + return expectedType.cast(convertedValue); + } + + /** + * Get all possible values from the given type and cast them into a boxed primitive type. + * + *

{@code expectedType} must be a boxed type, not a primitive type, because primitive types + * cannot be stored in a list. + * + * @param range the given range + * @param expectedType the expected type + * @return a list of all the values in the range + */ + public static List getValuesFromRange(Range range, Class expectedType) { + if (range == null || range.isWiderThan(ValueAnnotatedTypeFactory.MAX_VALUES)) { + return null; + } + if (range.isNothing()) { + return Collections.emptyList(); + } + + // The subtraction does not overflow, because the width has already been checked, so the + // bound difference is less than ValueAnnotatedTypeFactory.MAX_VALUES. + long boundDifference = range.to - range.from; + + // Each value is computed as a sum of the first value and an offset within the range, + // to avoid having range.to as an upper bound of the loop. range.to can be Long.MAX_VALUE, + // in which case a comparison value <= range.to would be always true. + // boundDifference is always much smaller than Long.MAX_VALUE + List values = new ArrayList<>((int) boundDifference + 1); + for (long offset = 0; offset <= boundDifference; offset++) { + long value = range.from + offset; + values.add(convertLongToType(value, expectedType)); + } + return values; + } + + private static List convertToStringVal(List origValues) { + if (origValues == null) { + return null; + } + return CollectionsPlume.mapList(Object::toString, origValues); + } + + /** + * Convert the {@code value} argument/element of a @BoolVal annotation into a list. + * + * @param anno a @BoolVal annotation + * @param newClass if String.class, the returned list is a {@code List} + * @param atypeFactory the type factory, used for obtaining fields/elements from annotations + * @return the {@code value} of a @BoolVal annotation, as a {@code List} or a {@code + * List} + */ + private static List convertBoolVal( + AnnotationMirror anno, Class newClass, ValueAnnotatedTypeFactory atypeFactory) { + List bools = + AnnotationUtils.getElementValueArray( + anno, atypeFactory.boolValValueElement, Boolean.class); + + if (newClass == String.class) { + return convertToStringVal(bools); + } + return bools; + } + + /** + * Convert the {@code value} argument/element of a {@code @StringVal} annotation into a list. + * + * @param anno a {@code @StringVal} annotation + * @param newClass if char[].class, the returned list is a {@code List} + * @param atypeFactory the type factory, used for obtaining fields/elements from annotations + * @return the {@code value} of a {@code @StringVal} annotation, as a {@code List} or a + * {@code List} + */ + private static List convertStringVal( + AnnotationMirror anno, Class newClass, ValueAnnotatedTypeFactory atypeFactory) { + List strings = atypeFactory.getStringValues(anno); + if (newClass == char[].class) { + return CollectionsPlume.mapList(String::toCharArray, strings); + } + return strings; + } + + private static List convertIntVal(List longs, Class newClass, TypeMirror newType) { + if (longs == null) { + return null; + } + if (newClass == String.class) { + return convertToStringVal(longs); + } else if (newClass == Character.class || newClass == char.class) { + return CollectionsPlume.mapList((Long l) -> (char) l.longValue(), longs); + } else if (newClass == Boolean.class) { + throw new UnsupportedOperationException( + "ValueAnnotatedTypeFactory: can't convert int to boolean"); + } + return NumberUtils.castNumbers(newType, longs); + } + +} From 04172b7db75e4b92f5316c5f4eb54d3347b0a361 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 2 Sep 2021 04:57:41 -0400 Subject: [PATCH 04/10] remove ValueInferenceQualifierHierarchy --- .../ValueInferenceAnnotatedTypeFactory.java | 37 ------------------- 1 file changed, 37 deletions(-) diff --git a/src/value/ValueInferenceAnnotatedTypeFactory.java b/src/value/ValueInferenceAnnotatedTypeFactory.java index 7a3f56c..e0355e4 100644 --- a/src/value/ValueInferenceAnnotatedTypeFactory.java +++ b/src/value/ValueInferenceAnnotatedTypeFactory.java @@ -274,43 +274,6 @@ private boolean isMethodDeclaredWithPolymorphicReturn( } } - @SuppressWarnings("deprecation") - @Override - public QualifierHierarchy createQualifierHierarchy() { - return MultiGraphQualifierHierarchy - .createMultiGraphQualifierHierarchy(this); - } - - @SuppressWarnings("deprecation") - @Override - public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory( - MultiGraphFactory factory) { - return new ValueInferenceQualifierHierarchy(factory); - } - - private final class ValueInferenceQualifierHierarchy extends InferenceQualifierHierarchy { - public ValueInferenceQualifierHierarchy(MultiGraphQualifierHierarchy.MultiGraphFactory multiGraphFactory) { - super(getSupportedTypeQualifiers(), elements); - } - - @Override - public Set leastUpperBounds( - Collection annos1, - Collection annos2) { - // TODO: remove hack - Set result = AnnotationUtils.createAnnotationSet(); - for (AnnotationMirror a1 : annos1) { - for (AnnotationMirror a2 : annos2) { - AnnotationMirror lub = leastUpperBound(a1, a2); - if (lub != null) { - result.add(lub); - } - } - } - return result; - } - } - /** * The domain of the Constant Value Checker: the types for which it estimates possible values. */ From fbc160602132d86d3de95b194bfaf724e3deb872 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 2 Sep 2021 05:22:45 -0400 Subject: [PATCH 05/10] update github action workflow --- .github/workflows/main.yml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index fac65ef..a257411 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -12,11 +12,19 @@ jobs: build: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - name: Pull Request Checkout + uses: actions/checkout@v2 + with: + ref: ${{github.event.pull_request.head.ref}} + repository: ${{github.event.pull_request.head.repo.full_name}} + if: github.head_ref != '' + - name: Push Checkout + uses: actions/checkout@v2 + if: github.head_ref == '' - name: Set up Python 3 uses: actions/setup-python@v2 with: - python-version: 3.6 + python-version: 3.8 - name: Install Python dependencies run: | python -m pip install --upgrade pip From 9b9886786d597e273bea7772041e6f77d1d87661 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 2 Sep 2021 09:30:18 -0400 Subject: [PATCH 06/10] run git-clone-related instead of hardcoding repo in setup.sh --- setup.sh | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/setup.sh b/setup.sh index c7a4310..e0a8121 100755 --- a/setup.sh +++ b/setup.sh @@ -12,7 +12,7 @@ else fi # Default value is opprop. REPO_SITE may be set to other value for travis test purpose. -export REPO_SITE="${REPO_SITE:-txiang61}" +export REPO_SITE="${REPO_SITE:-opprop}" echo "------ Downloading everything from REPO_SITE: $REPO_SITE ------" @@ -20,16 +20,14 @@ echo "------ Downloading everything from REPO_SITE: $REPO_SITE ------" if [ -d $JSR308/checker-framework ] ; then (cd $JSR308/checker-framework && git pull) else - BRANCH=master - (cd $JSR308 && git clone -b $BRANCH --depth 1 https://github.com/"$REPO_SITE"/checker-framework.git) + /tmp/plume-scripts/git-clone-related $REPO_SITE checker-framework $JSR308/checker-framework fi # Build checker-framework-inference if [ -d $JSR308/checker-framework-inference ] ; then (cd $JSR308/checker-framework-inference && git pull) else - BRANCH=master - (cd $JSR308 && git clone -b $BRANCH --depth 1 https://github.com/"$REPO_SITE"/checker-framework-inference.git) + /tmp/plume-scripts/git-clone-related $REPO_SITE checker-framework-inference $JSR308/checker-framework-inference fi # This also builds annotation-tools @@ -42,8 +40,7 @@ echo "Fetching DLJC" if [ -d $JSR308/do-like-javac ] ; then (cd $JSR308/do-like-javac && git pull) else - BRANCH=master - (cd $JSR308 && git clone -b $BRANCH --depth 1 https://github.com/"$REPO_SITE"/do-like-javac.git) + /tmp/plume-scripts/git-clone-related $REPO_SITE do-like-javac $JSR308/do-like-javac fi echo "Building value-inference without testing" From 6d7a5f6b6a9c2ed569fd8788c9746a9fdc60f757 Mon Sep 17 00:00:00 2001 From: d367wang <55197967+d367wang@users.noreply.github.com> Date: Thu, 2 Sep 2021 11:20:12 -0400 Subject: [PATCH 07/10] Update setup.sh: download plume-lib first --- setup.sh | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/setup.sh b/setup.sh index e0a8121..2efa1f8 100755 --- a/setup.sh +++ b/setup.sh @@ -11,6 +11,12 @@ else export JAVA_HOME=${JAVA_HOME:-$(dirname $(dirname $(readlink -f $(which javac))))} fi +if [ -d "/tmp/plume-scripts" ] ; then + git -C /tmp/plume-scripts pull -q +else + git -C /tmp clone --depth 1 -q https://github.com/plume-lib/plume-scripts.git +fi + # Default value is opprop. REPO_SITE may be set to other value for travis test purpose. export REPO_SITE="${REPO_SITE:-opprop}" From 257d7d965d219571d764f92b780da5ec025edd0f Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 17 Dec 2021 11:29:14 -0500 Subject: [PATCH 08/10] fix compile error --- src/value/ValueInferenceAnnotatedTypeFactory.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/value/ValueInferenceAnnotatedTypeFactory.java b/src/value/ValueInferenceAnnotatedTypeFactory.java index e0355e4..6620a2d 100644 --- a/src/value/ValueInferenceAnnotatedTypeFactory.java +++ b/src/value/ValueInferenceAnnotatedTypeFactory.java @@ -606,7 +606,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { // insert varAnnot of the slot into the ATM AnnotationMirror resultAM = slotManager.getAnnotation(result); - atm.clearPrimaryAnnotations(); + atm.clearAnnotations(); atm.replaceAnnotation(resultAM); Set resultSet = AnnotationUtils.createAnnotationSet(); From 8588764be60d4f9cfee49217b7c8cdf3a52cc479 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 14 Jan 2022 07:44:09 -0500 Subject: [PATCH 09/10] adapt to the change of ArithmeticVariableSlot constructor --- .../ValueInferenceAnnotatedTypeFactory.java | 22 +-- .../ValueZ3SmtSoftConstraintEncoder.java | 184 ++++++++---------- 2 files changed, 96 insertions(+), 110 deletions(-) diff --git a/src/value/ValueInferenceAnnotatedTypeFactory.java b/src/value/ValueInferenceAnnotatedTypeFactory.java index 6620a2d..0a1501d 100644 --- a/src/value/ValueInferenceAnnotatedTypeFactory.java +++ b/src/value/ValueInferenceAnnotatedTypeFactory.java @@ -362,7 +362,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; } if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -383,7 +383,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case MINUS: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -404,7 +404,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case MULTIPLY: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -425,7 +425,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case DIVIDE: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -446,7 +446,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case REMAINDER: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -467,7 +467,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case LEFT_SHIFT: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -488,7 +488,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case RIGHT_SHIFT: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -509,7 +509,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case UNSIGNED_RIGHT_SHIFT: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -530,7 +530,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case AND: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -551,7 +551,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case OR: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( @@ -572,7 +572,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { break; case XOR: if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location); + result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); constraintManager.addArithmeticConstraint( diff --git a/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java b/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java index 091ca35..5129643 100644 --- a/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java +++ b/src/value/solver/encoder/ValueZ3SmtSoftConstraintEncoder.java @@ -71,94 +71,91 @@ private void subtypeEqPreference(SubtypeConstraint stc, int prefenceVal) { } } - @Override - protected void encodeSoftComparisonConstraint(ComparisonConstraint cc) { - // switch (cc.getOperation()) { - // case EQUAL_TO: - // Constraint cst = - // InferenceMain.getInstance() - // .getConstraintManager() - // .createEqualityConstraint(cc.getResult(), cc.getRight()); - // Expr simplified = cst.serialize(formatTranslator).simplify(); - // if (!simplified.isTrue()) { - // addSoftConstraint(simplified, 15); - // } - // default: - // break; - // } - } - - @Override - protected void encodeSoftComparableConstraint(ComparableConstraint constraint) { - // Z3InferenceValue fst = cc.getFirst().serialize(formatTranslator); - // Z3InferenceValue snd = cc.getSecond().serialize(formatTranslator); - // switch(cc.getOperation()) { - // case EQUAL_TO: - // Constraint eqc = - // InferenceMain.getInstance() - // .getConstraintManager() - // .createEqualityConstraint(cc.getFirst(), cc.getSecond()); - // Expr simplifiedEQC = eqc.serialize(formatTranslator).simplify(); - // if (!simplifiedEQC.isTrue()) { - // addSoftConstraint(simplifiedEQC, 1); - // } - // break; - // case GREATER_THAN: - // BoolExpr gt = ctx.mkOr( - // ctx.mkAnd( - // fst.getIntRange(), - // ctx.mkGt(fst.getIntRangeLower(), snd.getIntRangeLower()), - // ctx.mkGt( - // fst.getIntRangeUpper(), snd.getIntRangeUpper())), - // ctx.mkNot(fst.getIntRange())); - // if (!gt.isTrue()) { - // addSoftConstraint(ctx.mkNot(gt), 1); - // } - // break; - // case LESS_THAN: - // BoolExpr lt = ctx.mkOr( - // ctx.mkAnd( - // fst.getIntRange(), - // ctx.mkLt(fst.getIntRangeLower(), snd.getIntRangeLower()), - // ctx.mkLt( - // fst.getIntRangeUpper(), snd.getIntRangeUpper())), - // ctx.mkNot(fst.getIntRange())); - // if (!lt.isTrue()) { - // addSoftConstraint(ctx.mkNot(lt), 1); - // } - // break; - // case GREATER_THAN_EQUAL: - // BoolExpr gteq = ctx.mkOr( - // ctx.mkAnd( - // fst.getIntRange(), - // ctx.mkGe(fst.getIntRangeLower(), snd.getIntRangeLower()), - // ctx.mkGe( - // fst.getIntRangeUpper(), snd.getIntRangeUpper())), - // ctx.mkNot(fst.getIntRange())); - // if (!gteq.isTrue()) { - // addSoftConstraint(ctx.mkNot(gteq), 1); - // } - // break; - // case LESS_THAN_EQUAL: - // BoolExpr lteq = ctx.mkOr( - // ctx.mkAnd( - // fst.getIntRange(), - // ctx.mkLe(fst.getIntRangeLower(), snd.getIntRangeLower()), - // ctx.mkLe( - // fst.getIntRangeUpper(), snd.getIntRangeUpper())), - // ctx.mkNot(fst.getIntRange())); - // if (!lteq.isTrue()) { - // addSoftConstraint(ctx.mkNot(lteq), 1); - // } - // break; - // default: - // break; - // - // } - } - - @Override - protected void encodeSoftArithmeticConstraint(ArithmeticConstraint constraint) {} +// @Override +// protected void encodeSoftComparisonConstraint(ComparisonConstraint cc) { +// switch (cc.getOperation()) { +// case EQUAL_TO: +// Constraint cst = +// InferenceMain.getInstance() +// .getConstraintManager() +// .createEqualityConstraint(cc.getResult(), cc.getRight()); +// Expr simplified = cst.serialize(formatTranslator).simplify(); +// if (!simplified.isTrue()) { +// addSoftConstraint(simplified, 15); +// } +// default: +// break; +// } +// } + +// @Override +// protected void encodeSoftComparableConstraint(ComparableConstraint constraint) { +// Z3InferenceValue fst = cc.getFirst().serialize(formatTranslator); +// Z3InferenceValue snd = cc.getSecond().serialize(formatTranslator); +// switch(cc.getOperation()) { +// case EQUAL_TO: +// Constraint eqc = +// InferenceMain.getInstance() +// .getConstraintManager() +// .createEqualityConstraint(cc.getFirst(), cc.getSecond()); +// Expr simplifiedEQC = eqc.serialize(formatTranslator).simplify(); +// if (!simplifiedEQC.isTrue()) { +// addSoftConstraint(simplifiedEQC, 1); +// } +// break; +// case GREATER_THAN: +// BoolExpr gt = ctx.mkOr( +// ctx.mkAnd( +// fst.getIntRange(), +// ctx.mkGt(fst.getIntRangeLower(), snd.getIntRangeLower()), +// ctx.mkGt( +// fst.getIntRangeUpper(), snd.getIntRangeUpper())), +// ctx.mkNot(fst.getIntRange())); +// if (!gt.isTrue()) { +// addSoftConstraint(ctx.mkNot(gt), 1); +// } +// break; +// case LESS_THAN: +// BoolExpr lt = ctx.mkOr( +// ctx.mkAnd( +// fst.getIntRange(), +// ctx.mkLt(fst.getIntRangeLower(), snd.getIntRangeLower()), +// ctx.mkLt( +// fst.getIntRangeUpper(), snd.getIntRangeUpper())), +// ctx.mkNot(fst.getIntRange())); +// if (!lt.isTrue()) { +// addSoftConstraint(ctx.mkNot(lt), 1); +// } +// break; +// case GREATER_THAN_EQUAL: +// BoolExpr gteq = ctx.mkOr( +// ctx.mkAnd( +// fst.getIntRange(), +// ctx.mkGe(fst.getIntRangeLower(), snd.getIntRangeLower()), +// ctx.mkGe( +// fst.getIntRangeUpper(), snd.getIntRangeUpper())), +// ctx.mkNot(fst.getIntRange())); +// if (!gteq.isTrue()) { +// addSoftConstraint(ctx.mkNot(gteq), 1); +// } +// break; +// case LESS_THAN_EQUAL: +// BoolExpr lteq = ctx.mkOr( +// ctx.mkAnd( +// fst.getIntRange(), +// ctx.mkLe(fst.getIntRangeLower(), snd.getIntRangeLower()), +// ctx.mkLe( +// fst.getIntRangeUpper(), snd.getIntRangeUpper())), +// ctx.mkNot(fst.getIntRange())); +// if (!lteq.isTrue()) { +// addSoftConstraint(ctx.mkNot(lteq), 1); +// } +// break; +// default: +// break; +// +// } +// } @Override protected void encodeSoftEqualityConstraint(EqualityConstraint constraint) {} @@ -166,15 +163,4 @@ protected void encodeSoftEqualityConstraint(EqualityConstraint constraint) {} @Override protected void encodeSoftInequalityConstraint(InequalityConstraint constraint) {} - @Override - protected void encodeSoftImplicationConstraint(ImplicationConstraint constraint) {} - - @Override - protected void encodeSoftExistentialConstraint(ExistentialConstraint constraint) {} - - @Override - protected void encodeSoftCombineConstraint(CombineConstraint constraint) {} - - @Override - protected void encodeSoftPreferenceConstraint(PreferenceConstraint constraint) {} } From 37e5221a00ebaff6ed4e225ffbe8040420bf52c4 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sat, 5 Feb 2022 22:45:02 -0500 Subject: [PATCH 10/10] adapt handling of binary tree in terms of arithmetic/comparison --- .../ValueInferenceAnnotatedTypeFactory.java | 242 ++---------------- src/value/ValueVisitor.java | 177 +++++-------- 2 files changed, 87 insertions(+), 332 deletions(-) diff --git a/src/value/ValueInferenceAnnotatedTypeFactory.java b/src/value/ValueInferenceAnnotatedTypeFactory.java index 0a1501d..05d0642 100644 --- a/src/value/ValueInferenceAnnotatedTypeFactory.java +++ b/src/value/ValueInferenceAnnotatedTypeFactory.java @@ -343,261 +343,51 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { AnnotatedTypeMirror rhsATM = this.inferenceTypeFactory.getAnnotatedType(binaryTree.getRightOperand()); - AnnotationMirror lhsAM = lhsATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); - AnnotationMirror rhsAM = rhsATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); // grab slots for the component (only for lub slot) Slot lhs = slotManager.getSlot(lhsATM); Slot rhs = slotManager.getSlot(rhsATM); + TypeMirror lhsTM = lhsATM.getUnderlyingType(); + TypeMirror rhsTM = rhsATM.getUnderlyingType(); + Slot result; Kind kind = binaryTree.getKind(); switch (kind) { case PLUS: if (TreeUtils.isStringConcatenation(binaryTree)) { - result = slotManager.createConstantSlot(UNKNOWNVAL); - // result = - // slotManager.createConstantSlot( - // - // AnnotationBuilder.fromClass(elements, StringVal.class)); - break; - } - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).plus(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); + result = slotManager.getSlot(UNKNOWNVAL); + // result = slotManager.createConstantSlot( + // AnnotationBuilder.fromClass(elements, StringVal.class)); break; } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); + result = slotManager.createArithmeticVariableSlot(location, lhsTM, rhsTM); + ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); + constraintManager.addArithmeticConstraint( + opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); break; case MINUS: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).minus(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case MULTIPLY: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).times(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case DIVIDE: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).divide(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case REMAINDER: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).remainder(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case LEFT_SHIFT: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).shiftLeft(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case RIGHT_SHIFT: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).signedShiftRight(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case UNSIGNED_RIGHT_SHIFT: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).unsignedShiftRight(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case AND: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).bitwiseAnd(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case OR: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).bitwiseOr(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); - break; case XOR: - if (lhsAM == null || rhsAM == null) { - result = slotManager.createArithmeticVariableSlot(location, lhsATM, rhsATM); - ArithmeticOperationKind opKindplus = - ArithmeticOperationKind.fromTreeKind(kind); - constraintManager.addArithmeticConstraint( - opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); - break; - } - if (AnnotationUtils.areSameByClass(lhsAM, IntRange.class) - && AnnotationUtils.areSameByClass(rhsAM, IntRange.class)) { - Range range = getRange(lhsAM).bitwiseXor(getRange(rhsAM)); - if (range.isLongEverything() && atm.getKind() == TypeKind.INT) { - range = Range.INT_EVERYTHING; - } - result = - slotManager.createConstantSlot(createIntRangeAnnotation(range)); - break; - } - result = slotManager.createLubMergeVariableSlot(lhs, rhs); + result = slotManager.createArithmeticVariableSlot(location, lhsTM, rhsTM); + opKindplus = ArithmeticOperationKind.fromTreeKind(kind); + constraintManager.addArithmeticConstraint( + opKindplus, lhs, rhs, (ArithmeticVariableSlot) result); break; + case GREATER_THAN: case GREATER_THAN_EQUAL: case LESS_THAN: case LESS_THAN_EQUAL: case EQUAL_TO: case NOT_EQUAL_TO: - result = slotManager.createConstantSlot(UNKNOWNVAL); + result = slotManager.getSlot(UNKNOWNVAL); break; default: result = slotManager.createLubMergeVariableSlot(lhs, rhs); diff --git a/src/value/ValueVisitor.java b/src/value/ValueVisitor.java index c1abbdc..116a590 100644 --- a/src/value/ValueVisitor.java +++ b/src/value/ValueVisitor.java @@ -14,6 +14,7 @@ import checkers.inference.model.ConstraintManager; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Slot; +import checkers.inference.qual.VarAnnot; import com.sun.source.tree.AssignmentTree; import com.sun.source.tree.BinaryTree; import com.sun.source.tree.CompoundAssignmentTree; @@ -31,6 +32,13 @@ import value.qual.IntRange; import value.qual.UnknownVal; +import static checkers.inference.model.ComparisonConstraint.ComparisonOperationKind.EQUAL_TO; +import static checkers.inference.model.ComparisonConstraint.ComparisonOperationKind.GREATER_THAN; +import static checkers.inference.model.ComparisonConstraint.ComparisonOperationKind.GREATER_THAN_EQUAL; +import static checkers.inference.model.ComparisonConstraint.ComparisonOperationKind.LESS_THAN; +import static checkers.inference.model.ComparisonConstraint.ComparisonOperationKind.LESS_THAN_EQUAL; +import static checkers.inference.model.ComparisonConstraint.ComparisonOperationKind.NOT_EQUAL_TO; + public class ValueVisitor extends InferenceVisitor { /** The top type for this hierarchy. */ @@ -163,106 +171,62 @@ public Void visitBinary(BinaryTree binaryTree, Void p) { } Kind kind = binaryTree.getKind(); + ComparisonVariableSlot compThenRes, compElseRes; + + if (!(leftTree instanceof IdentifierTree)) { + return super.visitBinary(binaryTree, p); + } + switch (kind) { - case EQUAL_TO: // == - if (leftTree instanceof IdentifierTree) { - ComparisonVariableSlot compThenRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - true); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.EQUAL_TO, lhs, rhs, compThenRes); - ComparisonVariableSlot compElseRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - false); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.NOT_EQUAL_TO, lhs, rhs, compElseRes); - } + case EQUAL_TO: + case NOT_EQUAL_TO: + case GREATER_THAN: + case GREATER_THAN_EQUAL: + case LESS_THAN: + case LESS_THAN_EQUAL: + compThenRes = slotManager.createComparisonVariableSlot( + VariableAnnotator.treeToLocation(atypeFactory, leftTree), + null, + true); + compElseRes = slotManager.createComparisonVariableSlot( + VariableAnnotator.treeToLocation(atypeFactory, leftTree), + null, + false); + break; + default: + return super.visitBinary(binaryTree, p); + } + + // initialize the comparison relation as for "==" comparison + ComparisonOperationKind thenRelation = EQUAL_TO; + ComparisonOperationKind elseRelation = NOT_EQUAL_TO; + switch (kind) { case NOT_EQUAL_TO: // != - if (leftTree instanceof IdentifierTree) { - ComparisonVariableSlot compThenRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - true); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.NOT_EQUAL_TO, lhs, rhs, compThenRes); - ComparisonVariableSlot compElseRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - false); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.EQUAL_TO, lhs, rhs, compElseRes); - } + thenRelation = NOT_EQUAL_TO; + elseRelation = EQUAL_TO; break; case GREATER_THAN: // > - if (leftTree instanceof IdentifierTree) { - ComparisonVariableSlot compThenRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - true); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.GREATER_THAN, lhs, rhs, compThenRes); - ComparisonVariableSlot compElseRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - false); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.LESS_THAN_EQUAL, lhs, rhs, compElseRes); - } + thenRelation = GREATER_THAN; + elseRelation = LESS_THAN_EQUAL; break; case GREATER_THAN_EQUAL: // >= - if (leftTree instanceof IdentifierTree) { - ComparisonVariableSlot compThenRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - true); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.GREATER_THAN_EQUAL, lhs, rhs, compThenRes); - ComparisonVariableSlot compElseRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - false); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.LESS_THAN, lhs, rhs, compElseRes); - } + thenRelation = GREATER_THAN_EQUAL; + elseRelation = LESS_THAN; break; case LESS_THAN: // < - if (leftTree instanceof IdentifierTree) { - ComparisonVariableSlot compThenRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - true); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.LESS_THAN, lhs, rhs, compThenRes); - ComparisonVariableSlot compElseRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - false); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.GREATER_THAN_EQUAL, lhs, rhs, compElseRes); - } + thenRelation = LESS_THAN; + elseRelation = GREATER_THAN_EQUAL; break; case LESS_THAN_EQUAL: // <= - if (leftTree instanceof IdentifierTree) { - ComparisonVariableSlot compThenRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - true); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.LESS_THAN_EQUAL, lhs, rhs, compThenRes); - ComparisonVariableSlot compElseRes = - slotManager.getComparisonVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, leftTree), - false); - constraintManager.addComparisonConstraint( - ComparisonOperationKind.GREATER_THAN, lhs, rhs, compElseRes); - } + thenRelation = LESS_THAN_EQUAL; + elseRelation = GREATER_THAN; break; default: break; } + constraintManager.addComparisonConstraint(thenRelation, lhs, rhs, compThenRes); + constraintManager.addComparisonConstraint(elseRelation, lhs, rhs, compElseRes); } return super.visitBinary(binaryTree, p); @@ -278,11 +242,14 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { InferenceAnnotatedTypeFactory iatf = (InferenceAnnotatedTypeFactory) atypeFactory; + // The ATM of the compound assignment expression AnnotatedTypeMirror resATM = atypeFactory.getAnnotatedType(tree); + // The ATM of the right operand of the compound assignment expression AnnotatedTypeMirror exprATM = iatf.getAnnotatedType(tree.getExpression()); - AnnotatedTypeMirror varATM = iatf.getAnnotatedTypeLhs(tree.getVariable()); - AnnotationMirror exprAMVal = exprATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); - AnnotationMirror varAMVal = varATM.getEffectiveAnnotationInHierarchy(UNKNOWNVAL); + // The ATM of the left operand of the compound assignment expression +// AnnotatedTypeMirror varATM = iatf.getAnnotatedTypeLhs(tree.getVariable()); + AnnotatedTypeMirror varATM = iatf.getAnnotatedType(tree.getVariable()); + Slot lhs = slotManager.getSlot(exprATM); Slot rhs = slotManager.getSlot(varATM); Slot res = slotManager.getSlot(resATM); @@ -297,22 +264,20 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { case MULTIPLY_ASSIGNMENT: case DIVIDE_ASSIGNMENT: case REMAINDER_ASSIGNMENT: - if (exprAMVal == null || varAMVal == null) { - ArithmeticVariableSlot avsResplus = - slotManager.getArithmeticVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, tree)); - // TODO: slot is null because location is missing. Find out why location is - // missing. - if (avsResplus == null) { - break; - } - constraintManager.addEqualityConstraint(avsResplus, res); + ArithmeticVariableSlot avsResplus = + slotManager.createArithmeticVariableSlot( + VariableAnnotator.treeToLocation(atypeFactory, tree), + varATM.getUnderlyingType(), + exprATM.getUnderlyingType()); + ArithmeticOperationKind opKindplus = ArithmeticOperationKind.fromTreeKind(kind); + constraintManager.addArithmeticConstraint(opKindplus, lhs, rhs, avsResplus); + // TODO: slot is null because location is missing. Find out why location is + // missing. + if (avsResplus == null) { break; } - if (AnnotationUtils.areSameByClass(exprAMVal, IntRange.class) - && AnnotationUtils.areSameByClass(varAMVal, IntRange.class)) { - break; - } // Create LUB constraint by default + constraintManager.addEqualityConstraint(avsResplus, res); + break; default: Slot lubSlot = slotManager.getSlot(atypeFactory.getAnnotatedType(tree)); // Create LUB constraint by default @@ -345,8 +310,8 @@ public Void visitUnary(UnaryTree tree, Void p) { case UNARY_MINUS: if (exprAMVal == null) { ArithmeticVariableSlot avsResplus = - slotManager.getArithmeticVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, tree)); + slotManager.createArithmeticVariableSlot( + VariableAnnotator.treeToLocation(atypeFactory, tree), null, null); // TODO: slot is null because location is missing. if (avsResplus == null) { break; @@ -367,8 +332,8 @@ public Void visitUnary(UnaryTree tree, Void p) { case POSTFIX_DECREMENT: if (exprAMVal == null) { ArithmeticVariableSlot avsResplus = - slotManager.getArithmeticVariableSlot( - VariableAnnotator.treeToLocation(atypeFactory, tree)); + slotManager.createArithmeticVariableSlot( + VariableAnnotator.treeToLocation(atypeFactory, tree), null, null); // TODO: slot is null because location is missing. if (avsResplus == null) { break;