From e5afb5ad05407be2f268d79db42ff498be6524f3 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Wed, 8 Jan 2020 17:27:03 -0500 Subject: [PATCH 1/9] update unit inference atf to fix benchmark exceptions --- benchmarks/projects.yml | 5 + src/units/UnitsAnnotatedTypeFactory.java | 14 ++- .../UnitsInferenceAnnotatedTypeFactory.java | 96 +++++++++++++++---- src/units/UnitsLiteralTreeAnnotator.java | 26 ----- 4 files changed, 91 insertions(+), 50 deletions(-) delete mode 100644 src/units/UnitsLiteralTreeAnnotator.java diff --git a/benchmarks/projects.yml b/benchmarks/projects.yml index f311ca0..2aba807 100644 --- a/benchmarks/projects.yml +++ b/benchmarks/projects.yml @@ -22,6 +22,11 @@ projects: build: mvn -B -DskipTests compile clean: mvn -B clean + commons-math: + giturl: https://github.com/txiang61-benchmarks/commons-math.git + build: mvn install -Drat.numUnapprovedLicenses=100 + clean: mvn -B clean + # Converted to use units # TODO: revert to unsat version jblas: diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index cb221c3..704eb06 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -20,6 +20,7 @@ import org.checkerframework.framework.type.DefaultAnnotatedTypeFormatter; import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator; @@ -334,13 +335,18 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { @Override public TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( - new UnitsTypecheckLiteralTreeAnnotator(), new UnitsPropagationTreeAnnotator()); + new UnitsLiteralTreeAnnotator(this), new UnitsPropagationTreeAnnotator()); } - protected final class UnitsTypecheckLiteralTreeAnnotator extends UnitsLiteralTreeAnnotator { + protected final class UnitsLiteralTreeAnnotator extends LiteralTreeAnnotator { // Programmatically set the qualifier implicits - public UnitsTypecheckLiteralTreeAnnotator() { - super(UnitsAnnotatedTypeFactory.this); + public UnitsLiteralTreeAnnotator(AnnotatedTypeFactory atf) { + super(atf); + // set BOTTOM as the literal qualifier for null literals + addLiteralKind(LiteralKind.NULL, unitsRepUtils.BOTTOM); + addLiteralKind(LiteralKind.STRING, unitsRepUtils.DIMENSIONLESS); + addLiteralKind(LiteralKind.CHAR, unitsRepUtils.DIMENSIONLESS); + addLiteralKind(LiteralKind.BOOLEAN, unitsRepUtils.DIMENSIONLESS); // in type checking mode, we also set dimensionless for the number literals addLiteralKind(LiteralKind.INT, unitsRepUtils.DIMENSIONLESS); addLiteralKind(LiteralKind.LONG, unitsRepUtils.DIMENSIONLESS); diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 484ef03..9c8c543 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -2,6 +2,7 @@ import checkers.inference.InferenceAnnotatedTypeFactory; import checkers.inference.InferenceChecker; +import checkers.inference.InferenceMain; import checkers.inference.InferenceQualifierHierarchy; import checkers.inference.InferenceTreeAnnotator; import checkers.inference.InferrableChecker; @@ -12,14 +13,17 @@ import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; +import checkers.inference.qual.VarAnnot; import com.sun.source.tree.BinaryTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.LiteralTree; import com.sun.source.tree.MemberSelectTree; import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; import java.lang.annotation.Annotation; +import java.util.Collection; import java.util.HashSet; import java.util.Map; import java.util.Set; @@ -35,11 +39,10 @@ import org.checkerframework.framework.type.AnnotationClassLoader; import org.checkerframework.framework.type.DefaultAnnotatedTypeFormatter; import org.checkerframework.framework.type.QualifierHierarchy; -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.AnnotationFormatter; import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; +import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.Pair; @@ -212,6 +215,34 @@ protected void finish( bottoms [@checkers.inference.qual.VarAnnot] */ } + + @Override + public Set leastUpperBounds( + Collection annos1, + Collection annos2) { + if (InferenceMain.isHackMode(annos1.size() != annos2.size())) { + 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; + } + + return super.leastUpperBounds(annos1, annos2); + } + } + + @Override + protected Set getDefaultTypeDeclarationBounds() { + Set top = new HashSet<>(); + top.add(unitsRepUtils.TOP); + return top; } @Override @@ -297,23 +328,12 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { } } - @Override - public TreeAnnotator createTreeAnnotator() { - return new ListTreeAnnotator( - new UnitsInferenceLiteralTreeAnnotator(), - new UnitsInferenceTreeAnnotator( - this, realChecker, realTypeFactory, variableAnnotator, slotManager)); - } - - protected final class UnitsInferenceLiteralTreeAnnotator extends UnitsLiteralTreeAnnotator { - // Programmatically set the qualifier implicits - public UnitsInferenceLiteralTreeAnnotator() { - super(UnitsInferenceAnnotatedTypeFactory.this); - // in inference mode, we do not implicitly set dimensionless for the number - // literals as we want to treat them as polymorphic. A "cast" is inferred for - // each literal - } - } + // @Override + // public TreeAnnotator createTreeAnnotator() { + // return new ListTreeAnnotator( + // new UnitsInferenceTreeAnnotator( + // this, realChecker, realTypeFactory, variableAnnotator, slotManager)); + // } private final class UnitsInferenceTreeAnnotator extends InferenceTreeAnnotator { // TODO: per design of InferenceTreeAnnotator, this code should be moved into @@ -388,10 +408,11 @@ private void generateVarSlotForStaticFinalConstants( && AnnotationUtils.areSame( ((ConstantSlot) slot).getValue(), unitsRepUtils.DIMENSIONLESS))) { - // Generate a fresh variable for inference + // Generate a fre sh variable for inference AnnotationLocation loc = VariableAnnotator.treeToLocation(atypeFactory, tree); VariableSlot varSlot = slotManager.createVariableSlot(loc); + atm.clearAnnotations(); atm.replaceAnnotation(slotManager.getAnnotation(varSlot)); } } @@ -518,6 +539,7 @@ public Void visitNewClass(NewClassTree newClassTree, AnnotatedTypeMirror atm) { // Replace the slot/annotation in the atm (callSiteReturnVarSlot) with the // varSlotForPolyReturn for upstream analysis + atm.clearAnnotations(); atm.replaceAnnotation(slotManager.getAnnotation(varSlotForPolyReturn)); } @@ -534,10 +556,44 @@ public Void visitMethodInvocation( variableAnnotator.getOrCreatePolyVar(methodInvocationTree); // disable insertion of polymorphic return variable slot varSlotForPolyReturn.setInsertable(false); + AnnotationBuilder ab = + new AnnotationBuilder(realTypeFactory.getProcessingEnv(), VarAnnot.class); + ab.setValue("value", varSlotForPolyReturn.getId()); + atm.clearAnnotations(); + atm.replaceAnnotation(ab.build()); } return null; } + + @Override + public Void visitLiteral(final LiteralTree tree, AnnotatedTypeMirror type) { + switch (tree.getKind()) { + case NULL_LITERAL: + replaceATM(type, unitsRepUtils.BOTTOM); + return null; + case CHAR_LITERAL: + replaceATM(type, unitsRepUtils.DIMENSIONLESS); + return null; + case BOOLEAN_LITERAL: + replaceATM(type, unitsRepUtils.DIMENSIONLESS); + return null; + case STRING_LITERAL: + replaceATM(type, unitsRepUtils.DIMENSIONLESS); + return null; + default: + return super.visitLiteral(tree, type); + } + } + + private void replaceATM(AnnotatedTypeMirror atm, AnnotationMirror am) { + final ConstantSlot cs = slotManager.createConstantSlot(am); + AnnotationBuilder ab = + new AnnotationBuilder(realTypeFactory.getProcessingEnv(), VarAnnot.class); + ab.setValue("value", cs.getId()); + atm.clearAnnotations(); + atm.replaceAnnotation(ab.build()); + } } // for use in AnnotatedTypeMirror.toString() diff --git a/src/units/UnitsLiteralTreeAnnotator.java b/src/units/UnitsLiteralTreeAnnotator.java deleted file mode 100644 index ef4cbec..0000000 --- a/src/units/UnitsLiteralTreeAnnotator.java +++ /dev/null @@ -1,26 +0,0 @@ -package units; - -import org.checkerframework.framework.qual.LiteralKind; -import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; -import units.representation.UnitsRepresentationUtils; - -/** Common base class for LiteralTreeAnnotator. */ -public abstract class UnitsLiteralTreeAnnotator extends LiteralTreeAnnotator { - - UnitsRepresentationUtils unitsRepUtils = UnitsRepresentationUtils.getInstance(); - - // Programmatically set the qualifier for literals - public UnitsLiteralTreeAnnotator(AnnotatedTypeFactory atf) { - super(atf); - - // set BOTTOM as the literal qualifier for null literals - addLiteralKind(LiteralKind.NULL, unitsRepUtils.BOTTOM); - addLiteralKind(LiteralKind.STRING, unitsRepUtils.DIMENSIONLESS); - addLiteralKind(LiteralKind.CHAR, unitsRepUtils.DIMENSIONLESS); - addLiteralKind(LiteralKind.BOOLEAN, unitsRepUtils.DIMENSIONLESS); - - // TODO: set BOTTOM as the literal qualifier for lower bounds? Its nice to - // infer a bound which is the current mode. - } -} From c8b45090ed6a3a22c1ca844b81b41ff1e4f13cd7 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 14 Apr 2020 23:02:59 -0400 Subject: [PATCH 2/9] add receiver dependent unit to unit checker --- src/units/JavaUtilConcurrent.astub | 17 +++-- src/units/UnitsAnnotatedTypeFactory.java | 19 +++++- .../UnitsInferenceAnnotatedTypeFactory.java | 6 ++ src/units/UnitsInferenceViewpointAdapter.java | 23 +++++++ src/units/UnitsViewpointAdapter.java | 39 ++++++++++++ src/units/qual/RDU.java | 19 ++++++ src/units/representation/TypecheckUnit.java | 12 ++++ .../UnitsRepresentationUtils.java | 7 +++ .../z3smt/UnitsZ3SmtFormatTranslator.java | 8 ++- .../UnitsZ3SmtCombineConstraintEncoder.java | 63 +++++++++++++++++++ .../UnitsZ3SmtConstraintEncoderFactory.java | 2 +- .../z3smt/representation/Z3InferenceUnit.java | 13 ++++ .../inference/JavaUtilConcurrentTimeUnit.java | 28 +++++++++ .../typecheck/JavaUtilConcurrentTimeUnit.java | 25 +++++++- 14 files changed, 267 insertions(+), 14 deletions(-) create mode 100644 src/units/UnitsInferenceViewpointAdapter.java create mode 100644 src/units/UnitsViewpointAdapter.java create mode 100644 src/units/qual/RDU.java create mode 100644 src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java diff --git a/src/units/JavaUtilConcurrent.astub b/src/units/JavaUtilConcurrent.astub index 2e907d9..e1905e9 100644 --- a/src/units/JavaUtilConcurrent.astub +++ b/src/units/JavaUtilConcurrent.astub @@ -14,23 +14,22 @@ enum TimeUnit { // For example, to convert 10 minutes to milliseconds, use: // TimeUnit.MILLISECONDS.convert(10L, TimeUnit.MINUTES) // TODO: enforce source value and unit are equal - @PolyUnit long convert(@PolyUnit TimeUnit this, @UnknownUnits long sourceDuration, - @UnknownUnits TimeUnit sourceUnit); + @RDU long convert(@UnknownUnits TimeUnit this, @UnknownUnits long sourceDuration, @UnknownUnits TimeUnit sourceUnit); // TODO: add dimensional bound on duration to be a time value - @ns long toNanos(@UnknownUnits long duration); + @ns long toNanos(@UnknownUnits TimeUnit this, @RDU long duration); - @us long toMicros(@UnknownUnits long duration); + @us long toMicros(@UnknownUnits TimeUnit this, @RDU long duration); - @ms long toMillis(@UnknownUnits long duration); + @ms long toMillis(@UnknownUnits TimeUnit this, @RDU long duration); - @s long toSeconds(@UnknownUnits long duration); + @s long toSeconds(@UnknownUnits TimeUnit this, @RDU long duration); - long toMinutes(@UnknownUnits long duration); + long toMinutes(@UnknownUnits TimeUnit this, @RDU long duration); - long toHours(@UnknownUnits long duration); + long toHours(@UnknownUnits TimeUnit this, @RDU long duration); - long toDays(@UnknownUnits long duration); + long toDays(@UnknownUnits TimeUnit this, @RDU long duration); // TODO: enforce "this" has same unit as "timeout" void timedWait(@UnknownUnits TimeUnit this, Object obj, @UnknownUnits long timeout); diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index 35600d7..6e2a7b1 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -19,6 +19,7 @@ import org.checkerframework.framework.type.AnnotationClassLoader; import org.checkerframework.framework.type.DefaultAnnotatedTypeFormatter; import org.checkerframework.framework.type.QualifierHierarchy; +import org.checkerframework.framework.type.ViewpointAdapter; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; @@ -79,6 +80,11 @@ protected Set> createSupportedTypeQualifiers() { return qualSet; } + @Override + protected ViewpointAdapter createViewpointAdapter() { + return new UnitsViewpointAdapter(this); + } + @Override public AnnotationMirror canonicalAnnotation(AnnotationMirror anno) { // check to see if it is an internal units annotation @@ -111,7 +117,7 @@ public AnnotationMirror canonicalAnnotation(AnnotationMirror anno) { @Override public boolean isSupportedQualifier(AnnotationMirror anno) { /* - * getQualifierHierarchy().getTypeQualifiers() contains PolyAll, PolyUnit, and the AMs of + * getQualifierHierarchy().getTypeQualifiers() contains PolyUnit, and the AMs of * Top and Bottom. We need to check all other instances of @UnitsRep AMs that are * supported qualifiers here. */ @@ -121,7 +127,7 @@ public boolean isSupportedQualifier(AnnotationMirror anno) { if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) { return unitsRepUtils.hasAllBaseUnits(anno); } - // Anno is PolyAll, PolyUnit + // Anno is PolyUnit return AnnotationUtils.containsSame(this.getQualifierHierarchy().getTypeQualifiers(), anno); } @@ -239,6 +245,7 @@ protected void finish( // Update tops tops.remove(unitsRepUtils.RAWUNITSREP); + tops.remove(unitsRepUtils.RECEIVER_DEPENDANT_UNIT); tops.add(unitsRepUtils.TOP); // System.err.println(" === Typecheck ATF "); @@ -284,6 +291,14 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { return true; } + // Case: @RDU shouldn't appear. throw error? + if (AnnotationUtils.areSame(subAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return isSubtype(unitsRepUtils.TOP, superAnno); + } + if (AnnotationUtils.areSame(superAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return true; + } + // Case: @UnitsRep(x) <: @UnitsRep(y) if (AnnotationUtils.areSameByClass(subAnno, UnitsRep.class) && AnnotationUtils.areSameByClass(superAnno, UnitsRep.class)) { diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 484ef03..ae898e4 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -12,6 +12,7 @@ import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; +import checkers.inference.util.InferenceViewpointAdapter; import com.sun.source.tree.BinaryTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.IdentifierTree; @@ -109,6 +110,11 @@ protected Set> createSupportedTypeQualifiers() { return qualSet; } + @Override + protected InferenceViewpointAdapter createViewpointAdapter() { + return new UnitsInferenceViewpointAdapter(this); + } + // In Inference ATF, this returns the alias for a given real qualifier @Override public AnnotationMirror canonicalAnnotation(AnnotationMirror anno) { diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java new file mode 100644 index 0000000..37f7762 --- /dev/null +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -0,0 +1,23 @@ +package units; + +import checkers.inference.util.InferenceViewpointAdapter; +import javax.lang.model.element.Element; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import units.representation.UnitsRepresentationUtils; + +public class UnitsInferenceViewpointAdapter extends InferenceViewpointAdapter { + + // static reference to the singleton instance + protected static UnitsRepresentationUtils unitsRepUtils; + + public UnitsInferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + unitsRepUtils = UnitsRepresentationUtils.getInstance(); + } + + @Override + protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { + return false; + } +} diff --git a/src/units/UnitsViewpointAdapter.java b/src/units/UnitsViewpointAdapter.java new file mode 100644 index 0000000..dc9076b --- /dev/null +++ b/src/units/UnitsViewpointAdapter.java @@ -0,0 +1,39 @@ +package units; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; +import units.representation.UnitsRepresentationUtils; + +public class UnitsViewpointAdapter extends AbstractViewpointAdapter { + + // static reference to the singleton instance + protected static UnitsRepresentationUtils unitsRepUtils; + + public UnitsViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + unitsRepUtils = UnitsRepresentationUtils.getInstance(); + } + + @Override + protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { + return false; + } + + @Override + protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { + return atm.getAnnotationInHierarchy(unitsRepUtils.TOP); + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + if (AnnotationUtils.areSame(declaredAnnotation, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return receiverAnnotation; + } + return declaredAnnotation; + } +} diff --git a/src/units/qual/RDU.java b/src/units/qual/RDU.java new file mode 100644 index 0000000..6be2671 --- /dev/null +++ b/src/units/qual/RDU.java @@ -0,0 +1,19 @@ +package units.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; + +/** + * UnitReceiverDependant is the top type of the type hierarchy. + * + * @checker_framework.manual #units-checker Units Checker + */ +@Documented +@SubtypeOf(UnitsRep.class) +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) // ElementType.TYPE, +public @interface RDU {} diff --git a/src/units/representation/TypecheckUnit.java b/src/units/representation/TypecheckUnit.java index db35df7..78a9aee 100644 --- a/src/units/representation/TypecheckUnit.java +++ b/src/units/representation/TypecheckUnit.java @@ -11,6 +11,7 @@ public class TypecheckUnit { private boolean uu; private boolean ub; + private boolean rdu; private int prefixExponent; // Tree map maintaining sorted order on base unit names private final Map exponents; @@ -20,6 +21,8 @@ public TypecheckUnit() { uu = false; // default UU value is false ub = false; + // default UU value is false + rdu = false; // default prefixExponent is 0 prefixExponent = 0; // default exponents are 0 @@ -44,6 +47,15 @@ public boolean isUnitsBottom() { return ub; } + public void setRDUnits(boolean val) { + rdu = val; + assert !(uu && ub); + } + + public boolean isRDUnits() { + return rdu; + } + public void setPrefixExponent(int exp) { prefixExponent = exp; } diff --git a/src/units/representation/UnitsRepresentationUtils.java b/src/units/representation/UnitsRepresentationUtils.java index ed02991..e2a6bbe 100644 --- a/src/units/representation/UnitsRepresentationUtils.java +++ b/src/units/representation/UnitsRepresentationUtils.java @@ -26,6 +26,7 @@ import units.qual.BUC; import units.qual.Dimensionless; import units.qual.PolyUnit; +import units.qual.RDU; import units.qual.UnitsAlias; import units.qual.UnitsBottom; import units.qual.UnitsRep; @@ -64,6 +65,8 @@ public class UnitsRepresentationUtils { public AnnotationMirror SURFACE_BOTTOM; + public AnnotationMirror RECEIVER_DEPENDANT_UNIT; + // /** Instance of {@link VarAnnot} for use in UnitsVisitor in infer mode. */ // public AnnotationMirror VARANNOT; @@ -212,6 +215,8 @@ public void postInit() { RAWUNITSREP = AnnotationBuilder.fromClass(elements, UnitsRep.class); + RECEIVER_DEPENDANT_UNIT = AnnotationBuilder.fromClass(elements, RDU.class); + Map zeroBaseDimensions = createZeroFilledBaseUnitsMap(); TOP = createInternalUnit(true, false, 0, zeroBaseDimensions); BOTTOM = createInternalUnit(false, true, 0, zeroBaseDimensions); @@ -494,6 +499,8 @@ public TypecheckUnit createTypecheckUnit(AnnotationMirror anno) { // if it is a polyunit annotation, generate top if (AnnotationUtils.areSameByClass(anno, PolyUnit.class)) { unit.setUnknownUnits(true); + } else if (AnnotationUtils.areSameByClass(anno, RDU.class)) { + unit.setRDUnits(true); } // if it is a units internal annotation, generate the internal unit else if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) { diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index 1208ad7..3d8827a 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java @@ -60,6 +60,7 @@ public String generateZ3SlotDeclaration(VariableSlot slot) { slotDeclaration.add(addZ3BoolDefinition(encodedSlot.getUnknownUnits())); slotDeclaration.add(addZ3BoolDefinition(encodedSlot.getUnitsBottom())); + slotDeclaration.add(addZ3BoolDefinition(encodedSlot.getRDUnits())); if (unitsRepUtils.serializePrefix()) { slotDeclaration.add(addZ3IntDefinition(encodedSlot.getPrefixExponent())); @@ -138,6 +139,8 @@ protected Z3InferenceUnit serializeConstantSlot(ConstantSlot slot) { encodedSlot.setUnknownUnits(true); } else if (unit.isUnitsBottom()) { encodedSlot.setUnitsBottom(true); + } else if (unit.isRDUnits()) { + encodedSlot.setRDUnits(true); } else { encodedSlot.setPrefixExponent(unit.getPrefixExponent()); for (String bu : unitsRepUtils.serializableBaseUnits()) { @@ -166,6 +169,7 @@ public void preAnalyzeSlots(Collection slots) { @Override public BoolExpr encodeSlotWellformnessConstraint(VariableSlot slot) { + Z3InferenceUnit serializedSlot = slot.serialize(this); if (slot instanceof ConstantSlot) { ConstantSlot cs = (ConstantSlot) slot; AnnotationMirror anno = cs.getValue(); @@ -173,9 +177,11 @@ public BoolExpr encodeSlotWellformnessConstraint(VariableSlot slot) { if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { return ctx.mkTrue(); } + if (AnnotationUtils.areSame(anno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return serializedSlot.getRDUnits(); + } } - Z3InferenceUnit serializedSlot = slot.serialize(this); return UnitsZ3SmtEncoderUtils.slotWellformedness(ctx, serializedSlot); } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java new file mode 100644 index 0000000..c578096 --- /dev/null +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java @@ -0,0 +1,63 @@ +package units.solvers.backend.z3smt.encoder; + +import backend.z3smt.Z3SmtFormatTranslator; +import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.VariableSlot; +import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; +import checkers.inference.solver.frontend.Lattice; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import units.representation.TypecheckUnit; +import units.solvers.backend.z3smt.representation.Z3InferenceUnit; + +public class UnitsZ3SmtCombineConstraintEncoder + extends Z3SmtAbstractConstraintEncoder + implements CombineConstraintEncoder { + + public UnitsZ3SmtCombineConstraintEncoder( + Lattice lattice, + Context ctx, + Z3SmtFormatTranslator z3SmtFormatTranslator) { + super(lattice, ctx, z3SmtFormatTranslator); + } + + private BoolExpr receiver_dependent( + VariableSlot target, VariableSlot declared, VariableSlot result) { + Z3InferenceUnit tar = target.serialize(z3SmtFormatTranslator); + Z3InferenceUnit decl = declared.serialize(z3SmtFormatTranslator); + Z3InferenceUnit res = result.serialize(z3SmtFormatTranslator); + + return ctx.mkAnd( + ctx.mkImplies(decl.getRDUnits(), UnitsZ3SmtEncoderUtils.equality(ctx, tar, res)), + ctx.mkImplies( + ctx.mkNot(decl.getRDUnits()), + UnitsZ3SmtEncoderUtils.equality(ctx, decl, res))); + } + + @Override + public BoolExpr encodeVariable_Variable( + VariableSlot target, VariableSlot declared, VariableSlot result) { + return ctx.mkTrue(); + // return receiver_dependent(target, declared, result); + } + + @Override + public BoolExpr encodeVariable_Constant( + VariableSlot target, ConstantSlot declared, VariableSlot result) { + return receiver_dependent(target, declared, result); + } + + @Override + public BoolExpr encodeConstant_Variable( + ConstantSlot target, VariableSlot declared, VariableSlot result) { + return ctx.mkTrue(); + // return receiver_dependent(target, declared, result); + } + + @Override + public BoolExpr encodeConstant_Constant( + ConstantSlot target, ConstantSlot declared, VariableSlot result) { + return receiver_dependent(target, declared, result); + } +} diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java index 83b8acc..2056456 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java @@ -63,7 +63,7 @@ public ExistentialConstraintEncoder createExistentialConstraintEncoder @Override public CombineConstraintEncoder createCombineConstraintEncoder() { - return null; + return new UnitsZ3SmtCombineConstraintEncoder(lattice, ctx, formatTranslator); } @Override diff --git a/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java b/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java index c5890d0..c845293 100644 --- a/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java +++ b/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java @@ -19,6 +19,7 @@ public class Z3InferenceUnit { private BoolExpr uu; private BoolExpr ub; + private BoolExpr rdu; private IntExpr prefixExponent; // Tree map maintaining sorted order on base unit names private final Map exponents; @@ -40,6 +41,8 @@ public static Z3InferenceUnit makeConstantSlot(Context ctx, int slotID) { slot.uu = ctx.mkBool(false); // default UU value is false slot.ub = ctx.mkBool(false); + // default UU value is false + slot.rdu = ctx.mkBool(false); // default prefixExponent is 0 slot.prefixExponent = slot.intZero; @@ -67,6 +70,8 @@ public static Z3InferenceUnit makeVariableSlot(Context ctx, int slotID) { UnitsZ3SmtEncoderUtils.z3VarName( slotID, UnitsZ3SmtEncoderUtils.prefixSlotName)); + slot.rdu = ctx.mkBool(false); + for (String baseUnit : UnitsRepresentationUtils.getInstance().serializableBaseUnits()) { slot.exponents.put( baseUnit, ctx.mkIntConst(UnitsZ3SmtEncoderUtils.z3VarName(slotID, baseUnit))); @@ -91,6 +96,14 @@ public BoolExpr getUnitsBottom() { return ub; } + public void setRDUnits(boolean val) { + rdu = ctx.mkBool(val); + } + + public BoolExpr getRDUnits() { + return rdu; + } + public void setPrefixExponent(int exp) { prefixExponent = ctx.mkInt(exp); } diff --git a/testing/inference/JavaUtilConcurrentTimeUnit.java b/testing/inference/JavaUtilConcurrentTimeUnit.java index c22aa5c..0bfbc06 100644 --- a/testing/inference/JavaUtilConcurrentTimeUnit.java +++ b/testing/inference/JavaUtilConcurrentTimeUnit.java @@ -28,4 +28,32 @@ void test2() { @ns long nanosec = ns.convert(10L, TimeUnit.DAYS); } + + void testParams() { + TimeUnit s_unit = TimeUnit.SECONDS; + TimeUnit ns_unit = NANOSECONDS; + + long ns = 1000; + long s = 1000; + + // :: fixable-error: (argument.type.incompatible) + TimeUnit.SECONDS.toMillis(s); + // :: fixable-error: (argument.type.incompatible) + TimeUnit.NANOSECONDS.toMillis(ns); + + // :: fixable-error: (argument.type.incompatible) + ns_unit.toMillis(ns); + // :: fixable-error: (argument.type.incompatible) + s_unit.toMillis(s); + } + + void testReturn(long s1, long s2) { + TimeUnit s = TimeUnit.SECONDS; + TimeUnit ms = TimeUnit.MILLISECONDS; + + // :: fixable-error: (assignment.type.incompatible) + s1 = s.convert(10L, NANOSECONDS); + // :: fixable-error: (assignment.type.incompatible) + s2 = TimeUnit.SECONDS.convert(10L, NANOSECONDS); + } } diff --git a/testing/typecheck/JavaUtilConcurrentTimeUnit.java b/testing/typecheck/JavaUtilConcurrentTimeUnit.java index d548579..ff62699 100644 --- a/testing/typecheck/JavaUtilConcurrentTimeUnit.java +++ b/testing/typecheck/JavaUtilConcurrentTimeUnit.java @@ -36,10 +36,14 @@ void test2() { // :: error: (assignment.type.incompatible) ms = ns; - // ensure the poly convert works + // ensure RDU convert works @s long seconds = s.convert(10L, NANOSECONDS); + // :: error: (assignment.type.incompatible) + @s long not_seconds = ms.convert(10L, NANOSECONDS); @s long secondsTwo = TimeUnit.SECONDS.convert(10L, NANOSECONDS); + // :: error: (assignment.type.incompatible) + @s long not_secondsTwo = TimeUnit.MILLISECONDS.convert(10L, NANOSECONDS); // convert 10 minutes to milliseconds @ms long milliseconds = TimeUnit.MILLISECONDS.convert(10L, TimeUnit.MINUTES); @@ -59,4 +63,23 @@ void bad() { // :: error: (assignment.type.incompatible) @s TimeUnit s4 = NANOSECONDS; } + + void testParams(@ns long ns, @s long s) { + @s TimeUnit s_unit = TimeUnit.SECONDS; + @ns TimeUnit ns_unit = NANOSECONDS; + + TimeUnit.SECONDS.toMillis(s); + TimeUnit.NANOSECONDS.toMillis(ns); + // :: error: (argument.type.incompatible) + TimeUnit.NANOSECONDS.toMillis(s); + // :: error: (argument.type.incompatible) + TimeUnit.SECONDS.toMillis(ns); + + ns_unit.toMillis(ns); + s_unit.toMillis(s); + // :: error: (argument.type.incompatible) + s_unit.toMillis(ns); + // :: error: (argument.type.incompatible) + ns_unit.toMillis(s); + } } From 855454cf9c9d7cdc6fe854f7f0eeea1ec5bc64f6 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Fri, 17 Apr 2020 00:56:49 -0400 Subject: [PATCH 3/9] add tests and stub files for benchmarks --- default.jaif | 93 +++++++++---------- solutions.txt | 60 ++++++------ src/units/JavaAWT.astub | 8 ++ src/units/JavaAWTGeom.astub | 12 +++ src/units/JavaLang.astub | 11 ++- src/units/JavaText.astub | 10 ++ src/units/UnitsChecker.java | 5 +- src/units/UnitsInferenceViewpointAdapter.java | 22 +++++ .../z3smt/UnitsZ3SmtFormatTranslator.java | 11 ++- .../UnitsZ3SmtCombineConstraintEncoder.java | 6 +- statistics.txt | 28 +++--- testing/typecheck/RDUMethodReceiver.java | 48 ++++++++++ 12 files changed, 203 insertions(+), 111 deletions(-) create mode 100644 src/units/JavaAWT.astub create mode 100644 src/units/JavaAWTGeom.astub create mode 100644 src/units/JavaText.astub create mode 100644 testing/typecheck/RDUMethodReceiver.java diff --git a/default.jaif b/default.jaif index dacd04b..c60ca5d 100644 --- a/default.jaif +++ b/default.jaif @@ -1,97 +1,90 @@ package units.qual: - annotation @us: + annotation @m2: package units.qual: - annotation @RDU: + annotation @ms: package units.qual: annotation @m: package units.qual: - annotation @mPERs: + annotation @BUC: + int exponent + String unit package units.qual: - annotation @m2: + annotation @UnitsRep: + boolean top + boolean bot + int prefixExponent + annotation-field units.qual.BUC[] baseUnitComponents package units.qual: - annotation @ms: + annotation @UnitsBottom: package units.qual: - annotation @Dimensionless: + annotation @us: package units.qual: - annotation @ns: + annotation @PolyUnit: package units.qual: - annotation @PolyUnit: + annotation @mPERs: package units.qual: - annotation @km: + annotation @rad: package units.qual: - annotation @BUC: - int exponent - String unit + annotation @s: package units.qual: - annotation @UnitsRep: - boolean top - boolean bot - int prefixExponent - annotation-field units.qual.BUC[] baseUnitComponents + annotation @km: package units.qual: - annotation @s: + annotation @UnknownUnits: package units.qual: - annotation @rad: + annotation @deg: package units.qual: - annotation @UnitsBottom: + annotation @Dimensionless: package units.qual: - annotation @UnknownUnits: + annotation @RDU: package units.qual: - annotation @deg: + annotation @ns: package : -class JavaUtilConcurrentTimeUnit:@units.qual.Dimensionless -method testReturn(JJ)V: -insert-annotation Method.parameter 1, Variable.type: @units.qual.s +class GenericMethods:@units.qual.Dimensionless +method mStringCatTwo(Ljava/lang/Object;)Ljava/lang/String;: +insert-annotation Method.parameter 0, Variable.type: @units.qual.Dimensionless +insert-annotation Method.typeParameter 0, TypeParameter.bound 0: @units.qual.Dimensionless +insert-annotation Method.typeParameter 0: @units.qual.Dimensionless insert-annotation Method.parameter -1: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 2, ExpressionStatement.expression, Assignment.expression, MethodInvocation.argument 0: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 3, ExpressionStatement.expression, Assignment.expression, MethodInvocation.argument 0: @units.qual.Dimensionless -insert-annotation Method.parameter 0, Variable.type: @units.qual.s -insert-annotation Method.body, Block.statement 0, Variable.type: @units.qual.s -insert-annotation Method.body, Block.statement 1, Variable.type: @units.qual.ms - -method testParams()V: -insert-annotation Method.body, Block.statement 0, Variable.type: @units.qual.s -insert-annotation Method.body, Block.statement 1, Variable.type: @units.qual.ns -insert-annotation Method.body, Block.statement 2, Variable.type: @units.qual.ns -insert-annotation Method.body, Block.statement 3, Variable.type: @units.qual.s +insert-annotation Method.type: @units.qual.Dimensionless + +method mStringCatOne(Ljava/lang/Object;)Ljava/lang/String;: +insert-annotation Method.typeParameter 0, TypeParameter.bound 0: @units.qual.Dimensionless insert-annotation Method.parameter -1: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 2, Variable.initializer: @units.qual.ns -insert-annotation Method.body, Block.statement 3, Variable.initializer: @units.qual.s +insert-annotation Method.typeParameter 0: @units.qual.Dimensionless +insert-annotation Method.parameter 0, Variable.type: @units.qual.Dimensionless +insert-annotation Method.type: @units.qual.Dimensionless method ()V: -method test(JLjava/util/concurrent/TimeUnit;)V: -insert-annotation Method.parameter 1, Variable.type: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 0, Variable.type: @units.qual.ms +method idOne(Ljava/lang/Object;)LT;: insert-annotation Method.parameter 0, Variable.type: @units.qual.Dimensionless +insert-annotation Method.typeParameter 0: @units.qual.Dimensionless insert-annotation Method.parameter -1: @units.qual.Dimensionless +insert-annotation Method.type: @units.qual.Dimensionless +insert-annotation Method.typeParameter 0, TypeParameter.bound 0: @units.qual.Dimensionless -method test2()V: +method idTwo(Ljava/lang/Number;)LT;: +insert-annotation Method.parameter 0, Variable.type: @units.qual.Dimensionless +insert-annotation Method.body, Block.statement 0, Variable.type: @units.qual.Dimensionless insert-annotation Method.parameter -1: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 0, Variable.type: @units.qual.s -insert-annotation Method.body, Block.statement 1, Variable.type: @units.qual.ms -insert-annotation Method.body, Block.statement 2, Variable.type: @units.qual.us -insert-annotation Method.body, Block.statement 3, Variable.type: @units.qual.ns -insert-annotation Method.body, Block.statement 4, Variable.initializer, MethodInvocation.argument 0: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 5, Variable.initializer, MethodInvocation.argument 0: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 6, Variable.initializer, MethodInvocation.argument 0: @units.qual.Dimensionless -insert-annotation Method.body, Block.statement 7, Variable.initializer, MethodInvocation.argument 0: @units.qual.Dimensionless +insert-annotation Method.typeParameter 0, TypeParameter.bound 0: @units.qual.Dimensionless +insert-annotation Method.type: @units.qual.Dimensionless diff --git a/solutions.txt b/solutions.txt index b1d4f79..4061bbb 100644 --- a/solutions.txt +++ b/solutions.txt @@ -3,44 +3,38 @@ SlotID: 5 Annotation: @Dimensionless SlotID: 6 Annotation: @Dimensionless SlotID: 7 Annotation: @Dimensionless SlotID: 9 Annotation: @Dimensionless +SlotID: 10 Annotation: @Dimensionless SlotID: 11 Annotation: @Dimensionless SlotID: 12 Annotation: @Dimensionless -SlotID: 13 Annotation: @ms +SlotID: 13 Annotation: @Dimensionless +SlotID: 14 Annotation: @Dimensionless SlotID: 15 Annotation: @Dimensionless -SlotID: 16 Annotation: @s -SlotID: 18 Annotation: @ms -SlotID: 19 Annotation: @us -SlotID: 21 Annotation: @ns +SlotID: 16 Annotation: @Dimensionless +SlotID: 17 Annotation: @Dimensionless +SlotID: 18 Annotation: @Dimensionless +SlotID: 19 Annotation: @Dimensionless +SlotID: 20 Annotation: @Dimensionless +SlotID: 21 Annotation: @Dimensionless +SlotID: 22 Annotation: @Dimensionless SlotID: 23 Annotation: @Dimensionless -SlotID: 24 Annotation: @s +SlotID: 24 Annotation: @Dimensionless SlotID: 25 Annotation: @Dimensionless -SlotID: 26 Annotation: @ms +SlotID: 26 Annotation: @Dimensionless SlotID: 27 Annotation: @Dimensionless -SlotID: 28 Annotation: @us +SlotID: 28 Annotation: @Dimensionless SlotID: 29 Annotation: @Dimensionless -SlotID: 30 Annotation: @ns -SlotID: 31 Annotation: @s -SlotID: 32 Annotation: @ns -SlotID: 33 Annotation: @ns -SlotID: 34 Annotation: @ns -SlotID: 35 Annotation: @s -SlotID: 36 Annotation: @s -SlotID: 37 Annotation: @s -SlotID: 38 Annotation: @ns -SlotID: 39 Annotation: @ns -SlotID: 40 Annotation: @s -SlotID: 41 Annotation: @s -SlotID: 42 Annotation: @s -SlotID: 43 Annotation: @s -SlotID: 44 Annotation: @ms -SlotID: 45 Annotation: @Dimensionless -SlotID: 46 Annotation: @s -SlotID: 47 Annotation: @s -SlotID: 48 Annotation: @s -SlotID: 49 Annotation: @Dimensionless -SlotID: 50 Annotation: @s -SlotID: 51 Annotation: @Dimensionless -SlotID: 52 Annotation: @Dimensionless -SlotID: 53 Annotation: @Dimensionless -SlotID: 54 Annotation: @Dimensionless +SlotID: 30 Annotation: @Dimensionless +SlotID: 31 Annotation: @Dimensionless +SlotID: 32 Annotation: @Dimensionless +SlotID: 34 Annotation: @Dimensionless +SlotID: 35 Annotation: @Dimensionless +SlotID: 36 Annotation: @Dimensionless +SlotID: 37 Annotation: @Dimensionless +SlotID: 38 Annotation: @Dimensionless +SlotID: 39 Annotation: @Dimensionless +SlotID: 40 Annotation: @Dimensionless +SlotID: 41 Annotation: @Dimensionless +SlotID: 42 Annotation: @Dimensionless +SlotID: 43 Annotation: @Dimensionless +SlotID: 44 Annotation: @Dimensionless ========================================================= diff --git a/src/units/JavaAWT.astub b/src/units/JavaAWT.astub new file mode 100644 index 0000000..143afb9 --- /dev/null +++ b/src/units/JavaAWT.astub @@ -0,0 +1,8 @@ +import units.qual.*; + +package java.awt; + +abstract class Graphics2D { + abstract void rotate(@rad double theta); + abstract void rotate(@rad double theta, double x, double y); +} diff --git a/src/units/JavaAWTGeom.astub b/src/units/JavaAWTGeom.astub new file mode 100644 index 0000000..b43b77d --- /dev/null +++ b/src/units/JavaAWTGeom.astub @@ -0,0 +1,12 @@ +import units.qual.*; + +package java.awt.geom; + +class AffineTransform implements Cloneable, Serializable { + static AffineTransform getRotateInstance(@rad double theta); + static AffineTransform getRotateInstance(@rad double theta, double anchorx, double anchory); + void rotate(@rad double theta); + void rotate(@rad double theta, double x, double y); + void setToRotation(@rad double theta); + void setToRotation(@rad double theta, double anchorx, double anchory); +} diff --git a/src/units/JavaLang.astub b/src/units/JavaLang.astub index 055fe6d..b136e96 100644 --- a/src/units/JavaLang.astub +++ b/src/units/JavaLang.astub @@ -6,14 +6,12 @@ class System { static @ms long currentTimeMillis(); static @ns long nanoTime(); } - // Throwable is implicitly @UnknownUnits class Throwable implements Serializable { void printStackTrace(@UnknownUnits Throwable this); void printStackTrace(@UnknownUnits Throwable this, PrintStream arg0); void printStackTrace(@UnknownUnits Throwable this, PrintWriter arg0); } - class String implements Serializable, Comparable, CharSequence { static String format(String arg0, @UnknownUnits Object[] arg1); static String format(Locale arg0, String arg1, @UnknownUnits Object[] arg2); @@ -22,3 +20,12 @@ class String implements Serializable, Comparable, CharSequence { static String valueOf(@UnknownUnits float arg0); static String valueOf(@UnknownUnits double arg0); } + +class StringBuilder implements Serializable, CharSequence { + StringBuilder append(@UnknownUnits int i); + StringBuilder append(@UnknownUnits long lng); + StringBuilder append(@UnknownUnits float f); + StringBuilder append(@UnknownUnits double b); + StringBuilder append(@UnknownUnits char c); +} + diff --git a/src/units/JavaText.astub b/src/units/JavaText.astub new file mode 100644 index 0000000..039e3d0 --- /dev/null +++ b/src/units/JavaText.astub @@ -0,0 +1,10 @@ +import units.qual.*; + +package java.text; + +class NumberFormat { + String format(@UnknownUnits long number); + abstract StrinBuffer format(@UnknownUnits long number, StringBuffer toAppendTo, FieldPosition pos); + String format(@UnknownUnits double number); + abstract StrinBuffer format(@UnknownUnits double number, StringBuffer toAppendTo, FieldPosition pos); +} diff --git a/src/units/UnitsChecker.java b/src/units/UnitsChecker.java index 7d2e1d7..a30d59c 100644 --- a/src/units/UnitsChecker.java +++ b/src/units/UnitsChecker.java @@ -19,8 +19,11 @@ "JavaMathTrig.astub", "JavaThread.astub", "JavaUtil.astub", + "JavaText.astub", "JavaUtilConcurrent.astub", // for ode4j, not yet annotated for hombucha - "ExperimentsJavaAwtGeomAffineTransform.astub", // for imgscalr experiment + "JavaAWT.astub", // for josm + "JavaAWTGeom.astub", // for josm, imgscalr + // "ExperimentsJavaAwtGeomAffineTransform.astub", // for imgscalr experiment "ExperimentsSunMiscUnsafe.astub", // for JLargeArrays }) public class UnitsChecker extends BaseInferrableChecker { diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java index 37f7762..fb1934f 100644 --- a/src/units/UnitsInferenceViewpointAdapter.java +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -1,9 +1,14 @@ package units; +import checkers.inference.InferenceMain; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.Slot; import checkers.inference.util.InferenceViewpointAdapter; +import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; import units.representation.UnitsRepresentationUtils; public class UnitsInferenceViewpointAdapter extends InferenceViewpointAdapter { @@ -20,4 +25,21 @@ public UnitsInferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) { protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { return false; } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + if (InferenceMain.isHackMode(declaredAnnotation == null)) { + return unitsRepUtils.BOTTOM; + } + Slot declSlot = InferenceMain.getInstance().getSlotManager().getSlot(declaredAnnotation); + if (declSlot.isConstant()) { + ConstantSlot cs = (ConstantSlot) declSlot; + if (AnnotationUtils.areSame(cs.getValue(), unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return super.combineAnnotationWithAnnotation( + receiverAnnotation, declaredAnnotation); + } + } + return declaredAnnotation; + } } diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index 3d8827a..1b7219e 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java @@ -173,7 +173,7 @@ public BoolExpr encodeSlotWellformnessConstraint(VariableSlot slot) { if (slot instanceof ConstantSlot) { ConstantSlot cs = (ConstantSlot) slot; AnnotationMirror anno = cs.getValue(); - // encode PolyAll and PolyUnit as constant trues + // encode PolyUnit as constant trues if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { return ctx.mkTrue(); } @@ -181,22 +181,23 @@ public BoolExpr encodeSlotWellformnessConstraint(VariableSlot slot) { return serializedSlot.getRDUnits(); } } - return UnitsZ3SmtEncoderUtils.slotWellformedness(ctx, serializedSlot); } @Override public BoolExpr encodeSlotPreferenceConstraint(VariableSlot slot) { + Z3InferenceUnit serializedSlot = slot.serialize(this); if (slot instanceof ConstantSlot) { ConstantSlot cs = (ConstantSlot) slot; AnnotationMirror anno = cs.getValue(); - // encode PolyAll and PolyUnit as constant trues + // encode PolyUnit as constant trues if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { return ctx.mkTrue(); } + if (AnnotationUtils.areSame(anno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return serializedSlot.getRDUnits(); + } } - - Z3InferenceUnit serializedSlot = slot.serialize(this); return UnitsZ3SmtEncoderUtils.slotPreference(ctx, serializedSlot); } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java index c578096..f89e204 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java @@ -38,8 +38,7 @@ private BoolExpr receiver_dependent( @Override public BoolExpr encodeVariable_Variable( VariableSlot target, VariableSlot declared, VariableSlot result) { - return ctx.mkTrue(); - // return receiver_dependent(target, declared, result); + return receiver_dependent(target, declared, result); } @Override @@ -51,8 +50,7 @@ public BoolExpr encodeVariable_Constant( @Override public BoolExpr encodeConstant_Variable( ConstantSlot target, VariableSlot declared, VariableSlot result) { - return ctx.mkTrue(); - // return receiver_dependent(target, declared, result); + return receiver_dependent(target, declared, result); } @Override diff --git a/statistics.txt b/statistics.txt index cdd750c..fd30743 100644 --- a/statistics.txt +++ b/statistics.txt @@ -1,18 +1,14 @@ ====================== Statistics ======================= -serialize_prefix: 1 -serialize_baseunits: 1 -smt_serialization_time(millisec): 149 -smt_solving_time(millisec): 351 -total_slots: 54 -total_variable_slots: 44 -constantslot: 10 -variableslot: 30 -existentialvariableslot: 1 -combvariableslot: 10 -refinementvariableslot: 2 -lubvariableslot: 1 -total_constraints: 40 -combineconstraint: 10 -subtypeconstraint: 28 -equalityconstraint: 2 +serialize_prefix: 0 +serialize_baseunits: 0 +smt_serialization_time(millisec): 53 +smt_solving_time(millisec): 21 +total_slots: 44 +total_variable_slots: 38 +constantslot: 6 +variableslot: 23 +existentialvariableslot: 15 +total_constraints: 4 +existentialconstraint: 2 +subtypeconstraint: 2 ========================================================= diff --git a/testing/typecheck/RDUMethodReceiver.java b/testing/typecheck/RDUMethodReceiver.java new file mode 100644 index 0000000..ac51527 --- /dev/null +++ b/testing/typecheck/RDUMethodReceiver.java @@ -0,0 +1,48 @@ +import units.qual.*; + +public class RDUMethodReceiver { + + // :: error: (super.invocation.invalid) + @m public class MeterClass { + @RDU + Object get(@m MeterClass this) { + return null; + } + + Object set(@m MeterClass this, @RDU Object x) { + return null; + } + } + + // :: error: (super.invocation.invalid) + @s public class SecondClass { + @RDU + Object get(@s SecondClass this) { + return null; + } + + Object set(@s SecondClass this, @RDU Object x) { + return null; + } + } + + void invoke() { + MeterClass mc = new MeterClass(); + @m Object x = mc.get(); + mc.set(x); + + SecondClass sc = new SecondClass(); + @s Object y = sc.get(); + sc.set(y); + + // :: error: (assignment.type.incompatible) + @m Object z = sc.get(); + // :: error: (argument.type.incompatible) + sc.set(z); + + // :: error: (assignment.type.incompatible) + @s Object w = mc.get(); + // :: error: (argument.type.incompatible) + mc.set(w); + } +} From 2c4823bb009a1a1839399cd8966234c160bd18a8 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Thu, 7 May 2020 23:02:37 -0400 Subject: [PATCH 4/9] increased UnitsTools and the units signatures for benchmark GasFlow --- .classpath | 22 +- .project | 13 +- .settings/org.eclipse.buildship.core.prefs | 2 + benchmarks/find_replace.sh | 31 +++ benchmarks/projects.yml | 22 +- default.jaif | 90 -------- scripts/run-dljc-infer.sh | 16 +- solutions.txt | 40 ---- src/units/JavaLang.astub | 3 + src/units/JavaNioFile.astub | 8 + src/units/JavaUtil.astub | 10 + src/units/JavolutionMathLib.astub | 89 +++++++ src/units/UnitsAnnotatedTypeFactory.java | 10 +- src/units/UnitsAnnotationFormatter.java | 3 +- src/units/UnitsChecker.java | 2 + .../UnitsInferenceAnnotatedTypeFactory.java | 22 +- src/units/UnitsTools.java | 75 +++++- src/units/UnitsVisitor.java | 12 +- src/units/notusedquals/N.java | 24 ++ src/units/notusedquals/kPa.java | 22 ++ src/units/notusedquals/kmol.java | 23 ++ src/units/qual/C.java | 18 ++ src/units/qual/J.java | 20 ++ src/units/qual/JPERKmol.java | 21 ++ src/units/{notusedquals => qual}/K.java | 3 +- src/units/qual/MJ.java | 20 ++ src/units/qual/MJPERm3.java | 20 ++ src/units/qual/PERm2s2.java | 18 ++ src/units/qual/Pa.java | 20 ++ src/units/qual/Pas.java | 20 ++ src/units/qual/W.java | 20 ++ src/units/qual/WPERm2K.java | 20 ++ src/units/qual/bar.java | 20 ++ src/units/qual/bars3PERm.java | 20 ++ src/units/{notusedquals => qual}/g.java | 3 +- src/units/qual/g8.java | 20 ++ src/units/qual/gPERmol.java | 18 ++ src/units/qual/hr.java | 18 ++ src/units/{notusedquals => qual}/kg.java | 4 +- src/units/qual/kg2PERs2.java | 20 ++ src/units/qual/kgPERm2s.java | 20 ++ src/units/qual/kgPERm3.java | 20 ++ src/units/qual/kgPERmol.java | 20 ++ src/units/qual/kgPERs.java | 20 ++ src/units/qual/m2PERs2.java | 18 ++ src/units/qual/m2PERs2K.java | 18 ++ src/units/qual/m2s2.java | 18 ++ src/units/qual/m3.java | 18 ++ src/units/qual/m3PERhr.java | 18 ++ src/units/qual/mPERs2.java | 18 ++ src/units/qual/mm.java | 20 ++ src/units/qual/mm2.java | 20 ++ src/units/{notusedquals => qual}/mol.java | 3 +- src/units/qual/s2PERm2.java | 18 ++ statistics.txt | 14 -- testing/inference/AbstractEdge.java | 5 + testing/inference/DEdge.java | 21 ++ testing/inference/DNode.java | 18 ++ testing/inference/DynamicNetwork.java | 6 + testing/inference/GSPG.java | 218 ++++++++++++++++++ testing/inference/GasEdge.java | 11 + testing/inference/GasNode.java | 4 + testing/inference/Graph.java | 189 +++++++++++++++ testing/inference/Identifiable.java | 45 ++++ testing/inference/IdentifiableCollection.java | 16 ++ testing/inference/Test.java | 41 ++++ testing/inference/Test2.java | 43 ++++ testing/inference/Test3.java | 11 + testing/typecheck/Arithmetic.java | 9 + 69 files changed, 1561 insertions(+), 201 deletions(-) create mode 100644 .settings/org.eclipse.buildship.core.prefs create mode 100755 benchmarks/find_replace.sh delete mode 100644 default.jaif delete mode 100644 solutions.txt create mode 100644 src/units/JavaNioFile.astub create mode 100644 src/units/JavolutionMathLib.astub create mode 100644 src/units/notusedquals/N.java create mode 100644 src/units/notusedquals/kPa.java create mode 100644 src/units/notusedquals/kmol.java create mode 100644 src/units/qual/C.java create mode 100644 src/units/qual/J.java create mode 100644 src/units/qual/JPERKmol.java rename src/units/{notusedquals => qual}/K.java (88%) create mode 100644 src/units/qual/MJ.java create mode 100644 src/units/qual/MJPERm3.java create mode 100644 src/units/qual/PERm2s2.java create mode 100644 src/units/qual/Pa.java create mode 100644 src/units/qual/Pas.java create mode 100644 src/units/qual/W.java create mode 100644 src/units/qual/WPERm2K.java create mode 100644 src/units/qual/bar.java create mode 100644 src/units/qual/bars3PERm.java rename src/units/{notusedquals => qual}/g.java (88%) create mode 100644 src/units/qual/g8.java create mode 100644 src/units/qual/gPERmol.java create mode 100644 src/units/qual/hr.java rename src/units/{notusedquals => qual}/kg.java (86%) create mode 100644 src/units/qual/kg2PERs2.java create mode 100644 src/units/qual/kgPERm2s.java create mode 100644 src/units/qual/kgPERm3.java create mode 100644 src/units/qual/kgPERmol.java create mode 100644 src/units/qual/kgPERs.java create mode 100644 src/units/qual/m2PERs2.java create mode 100644 src/units/qual/m2PERs2K.java create mode 100644 src/units/qual/m2s2.java create mode 100644 src/units/qual/m3.java create mode 100644 src/units/qual/m3PERhr.java create mode 100644 src/units/qual/mPERs2.java create mode 100644 src/units/qual/mm.java create mode 100644 src/units/qual/mm2.java rename src/units/{notusedquals => qual}/mol.java (88%) create mode 100644 src/units/qual/s2PERm2.java delete mode 100644 statistics.txt create mode 100644 testing/inference/AbstractEdge.java create mode 100644 testing/inference/DEdge.java create mode 100644 testing/inference/DNode.java create mode 100644 testing/inference/DynamicNetwork.java create mode 100644 testing/inference/GSPG.java create mode 100644 testing/inference/GasEdge.java create mode 100644 testing/inference/GasNode.java create mode 100644 testing/inference/Graph.java create mode 100644 testing/inference/Identifiable.java create mode 100644 testing/inference/IdentifiableCollection.java create mode 100644 testing/inference/Test.java create mode 100644 testing/inference/Test2.java create mode 100644 testing/inference/Test3.java create mode 100644 testing/typecheck/Arithmetic.java diff --git a/.classpath b/.classpath index 7c6ac24..81721b0 100644 --- a/.classpath +++ b/.classpath @@ -1,12 +1,20 @@ - - + + + + + + + + + + + + + + - - - - - + diff --git a/.project b/.project index 8ca7972..653f020 100644 --- a/.project +++ b/.project @@ -1,14 +1,23 @@ units-inference - + + + org.eclipse.jdt.core.javabuilder - + + + + + org.eclipse.buildship.core.gradleprojectbuilder + + org.eclipse.jdt.core.javanature + org.eclipse.buildship.core.gradleprojectnature diff --git a/.settings/org.eclipse.buildship.core.prefs b/.settings/org.eclipse.buildship.core.prefs new file mode 100644 index 0000000..e889521 --- /dev/null +++ b/.settings/org.eclipse.buildship.core.prefs @@ -0,0 +1,2 @@ +connection.project.dir= +eclipse.preferences.version=1 diff --git a/benchmarks/find_replace.sh b/benchmarks/find_replace.sh new file mode 100755 index 0000000..9ede210 --- /dev/null +++ b/benchmarks/find_replace.sh @@ -0,0 +1,31 @@ +#!/bin/bash +# find_replace.sh + +# echo "Find and replace in current directory!" +# echo "Existing string?" +# read existing +# echo "Replacement string?" +# read replacement +# echo "Replacing all occurences of $existing with $replacement in files matching $filepattern" + +# find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/$existing/$replacement/g" + +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/import si.uom.SI;/import units.UnitsTools;/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/SI.METRE/UnitsTools.m/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/SI.RADIAN/UnitsTools.rad/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/SI.SECOND/UnitsTools.s/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/SI.KILOMETER/UnitsTools.km/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/SI.DAY/UnitsTools.day/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/SI.YEAR/UnitsTools.year/g" + +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/import si.uom.NonSI;/import units.UnitsTools;/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/NonSI.DEGREE_ANGLE/UnitsTools.deg/g" + +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/import javax.measure.Unit;//g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/Unit/int/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/Unit/int/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/Unit/int/g" +find . -type f -name "*.java" -print0 | xargs -0 sed -i '' -e "s/Unit