From e5afb5ad05407be2f268d79db42ff498be6524f3 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Wed, 8 Jan 2020 17:27:03 -0500 Subject: [PATCH 01/11] 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 9f7cf936ce2b3d117589b315afe1b09af8ef7be1 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Mon, 9 Mar 2020 14:10:57 -0400 Subject: [PATCH 02/11] added view point adaption for receiver dependent units --- src/units/JavaLang.astub | 9 +++ src/units/JavaText.astub | 10 ++++ src/units/JavaUtilConcurrent.astub | 14 ++--- src/units/UnitsAnnotatedTypeFactory.java | 17 +++++- src/units/UnitsChecker.java | 1 + .../UnitsInferenceAnnotatedTypeFactory.java | 35 +++++++++++- src/units/UnitsInferenceViewpointAdapter.java | 35 ++++++++++++ src/units/UnitsViewpointAdapter.java | 57 +++++++++++++++++++ src/units/qual/RDU.java | 21 +++++++ .../UnitsRepresentationUtils.java | 6 +- 10 files changed, 195 insertions(+), 10 deletions(-) create mode 100644 src/units/JavaText.astub create mode 100644 src/units/UnitsInferenceViewpointAdapter.java create mode 100644 src/units/UnitsViewpointAdapter.java create mode 100644 src/units/qual/RDU.java diff --git a/src/units/JavaLang.astub b/src/units/JavaLang.astub index 055fe6d..684908d 100644 --- a/src/units/JavaLang.astub +++ b/src/units/JavaLang.astub @@ -22,3 +22,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/JavaUtilConcurrent.astub b/src/units/JavaUtilConcurrent.astub index 2e907d9..ac5c7df 100644 --- a/src/units/JavaUtilConcurrent.astub +++ b/src/units/JavaUtilConcurrent.astub @@ -18,19 +18,19 @@ enum TimeUnit { @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, @UnknownUnits long duration); - @us long toMicros(@UnknownUnits long duration); + @us long toMicros(@UnknownUnits TimeUnit this, @UnknownUnits 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, @UnknownUnits long duration); - long toMinutes(@UnknownUnits long duration); + long toMinutes(@UnknownUnits TimeUnit this, @UnknownUnits long duration); - long toHours(@UnknownUnits long duration); + long toHours(@UnknownUnits TimeUnit this, @UnknownUnits long duration); - long toDays(@UnknownUnits long duration); + long toDays(@UnknownUnits TimeUnit this, @UnknownUnits 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 704eb06..aafabea 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.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; @@ -55,6 +56,11 @@ protected AnnotationClassLoader createAnnotationClassLoader() { // Use the Units Annotated Type Loader instead of the default one return new UnitsAnnotationClassLoader(checker); } + + @Override + protected ViewpointAdapter createViewpointAdapter() { + return new UnitsViewpointAdapter(this); + } @Override protected Set> createSupportedTypeQualifiers() { @@ -262,6 +268,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 "); @@ -299,13 +306,21 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { return true; } - // Case: @PolyAll and @PolyUnit are treated as @UnknownUnits + // Case: @PolyUnit are treated as @UnknownUnits if (AnnotationUtils.areSame(subAnno, unitsRepUtils.POLYUNIT)) { return isSubtype(unitsRepUtils.TOP, superAnno); } if (AnnotationUtils.areSame(superAnno, unitsRepUtils.POLYUNIT)) { return true; } + + // Case: @RDU are treated as @UnknownUnits + 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) diff --git a/src/units/UnitsChecker.java b/src/units/UnitsChecker.java index 7d2e1d7..69b5b59 100644 --- a/src/units/UnitsChecker.java +++ b/src/units/UnitsChecker.java @@ -19,6 +19,7 @@ "JavaMathTrig.astub", "JavaThread.astub", "JavaUtil.astub", + "JavaText.astub", "JavaUtilConcurrent.astub", // for ode4j, not yet annotated for hombucha "ExperimentsJavaAwtGeomAffineTransform.astub", // for imgscalr experiment "ExperimentsSunMiscUnsafe.astub", // for JLargeArrays diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 9c8c543..2a2c2b4 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -14,6 +14,8 @@ import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.qual.VarAnnot; +import checkers.inference.util.InferenceViewpointAdapter; + import com.sun.source.tree.BinaryTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.IdentifierTree; @@ -44,6 +46,7 @@ import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; @@ -91,6 +94,11 @@ protected AnnotationClassLoader createAnnotationClassLoader() { // Use the Units Annotated Type Loader instead of the default one return new UnitsAnnotationClassLoader(checker); } + + @Override + protected InferenceViewpointAdapter createViewpointAdapter() { + return new UnitsInferenceViewpointAdapter(this); + } // In Inference ATF, this returns the set of real qualifiers @Override @@ -234,7 +242,32 @@ public Set leastUpperBounds( return result; } - return super.leastUpperBounds(annos1, annos2); + if (annos1.isEmpty()) { + throw new BugInCF( + "QualifierHierarchy.leastUpperBounds: tried to determine LUB with empty sets"); + } + + Set result = AnnotationUtils.createAnnotationSet(); + for (AnnotationMirror a1 : annos1) { + for (AnnotationMirror a2 : annos2) { + AnnotationMirror lub = leastUpperBound(a1, a2); + if (lub != null) { + result.add(lub); + } + } + } + + if (annos1.size() == result.size() || annos2.size() == result.size()) { + return result; + } else { + throw new BugInCF("QualifierHierarchy.leastUpperBounds: resulting set has incorrect number of annotations.\n" + + " Set 1: " + + annos1 + + " Set 2: " + + annos2 + + " LUB: " + + result); + } } } diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java new file mode 100644 index 0000000..37a5cea --- /dev/null +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -0,0 +1,35 @@ +package units; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.type.TypeKind; + +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; + +import checkers.inference.util.InferenceViewpointAdapter; +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) { + if (!(type.getKind() == TypeKind.DECLARED || type.getKind() == TypeKind.ARRAY)) { + return false; + } + return super.shouldAdaptMember(type, element); + } + + @Override + protected AnnotatedTypeMirror combineAnnotationWithType(AnnotationMirror receiverAnnotation, AnnotatedTypeMirror declared) { + return super.combineAnnotationWithType(receiverAnnotation, declared); + } +} diff --git a/src/units/UnitsViewpointAdapter.java b/src/units/UnitsViewpointAdapter.java new file mode 100644 index 0000000..90dc9b0 --- /dev/null +++ b/src/units/UnitsViewpointAdapter.java @@ -0,0 +1,57 @@ +package units; + +import java.util.ArrayList; +import java.util.IdentityHashMap; +import java.util.List; +import java.util.Map; + +import javax.lang.model.element.AnnotationMirror; + +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; +import org.checkerframework.framework.type.AnnotatedTypeReplacer; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; +import org.checkerframework.javacutil.AnnotationUtils; + +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.type.TypeKind; + +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) { + if (!(type.getKind() == TypeKind.DECLARED || type.getKind() == TypeKind.ARRAY)) { + return false; + } + return super.shouldAdaptMember(type, element); + } + + + @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..d5fc8cb --- /dev/null +++ b/src/units/qual/RDU.java @@ -0,0 +1,21 @@ +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(UnknownUnits.class) +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) // ElementType.TYPE, +public @interface RDU {} diff --git a/src/units/representation/UnitsRepresentationUtils.java b/src/units/representation/UnitsRepresentationUtils.java index ed02991..f5ead4f 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; @@ -63,6 +64,8 @@ public class UnitsRepresentationUtils { public AnnotationMirror SURFACE_TOP; public AnnotationMirror SURFACE_BOTTOM; + + public AnnotationMirror RECEIVER_DEPENDANT_UNIT; // /** Instance of {@link VarAnnot} for use in UnitsVisitor in infer mode. */ // public AnnotationMirror VARANNOT; @@ -209,6 +212,7 @@ protected Map createZeroFilledBaseUnitsMap() { // units public void postInit() { POLYUNIT = AnnotationBuilder.fromClass(elements, PolyUnit.class); + RECEIVER_DEPENDANT_UNIT = AnnotationBuilder.fromClass(elements, RDU.class); RAWUNITSREP = AnnotationBuilder.fromClass(elements, UnitsRep.class); @@ -492,7 +496,7 @@ public TypecheckUnit createTypecheckUnit(AnnotationMirror anno) { TypecheckUnit unit = new TypecheckUnit(); // if it is a polyunit annotation, generate top - if (AnnotationUtils.areSameByClass(anno, PolyUnit.class)) { + if (AnnotationUtils.areSameByClass(anno, PolyUnit.class) || AnnotationUtils.areSameByClass(anno, RDU.class)) { unit.setUnknownUnits(true); } // if it is a units internal annotation, generate the internal unit From 4de729ddf1137570590e6e10c1720c8e9b246cc2 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Mon, 9 Mar 2020 14:10:57 -0400 Subject: [PATCH 03/11] added view point adaption for receiver dependent units --- src/units/JavaLang.astub | 9 +++ src/units/JavaText.astub | 10 ++++ src/units/JavaUtilConcurrent.astub | 16 +++--- src/units/UnitsAnnotatedTypeFactory.java | 52 +++++++++++------ src/units/UnitsChecker.java | 1 + .../UnitsInferenceAnnotatedTypeFactory.java | 35 +++++++++++- src/units/UnitsInferenceViewpointAdapter.java | 35 ++++++++++++ src/units/UnitsViewpointAdapter.java | 57 +++++++++++++++++++ src/units/qual/RDU.java | 21 +++++++ .../UnitsRepresentationUtils.java | 6 +- 10 files changed, 214 insertions(+), 28 deletions(-) create mode 100644 src/units/JavaText.astub create mode 100644 src/units/UnitsInferenceViewpointAdapter.java create mode 100644 src/units/UnitsViewpointAdapter.java create mode 100644 src/units/qual/RDU.java diff --git a/src/units/JavaLang.astub b/src/units/JavaLang.astub index 055fe6d..684908d 100644 --- a/src/units/JavaLang.astub +++ b/src/units/JavaLang.astub @@ -22,3 +22,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/JavaUtilConcurrent.astub b/src/units/JavaUtilConcurrent.astub index 2e907d9..e733293 100644 --- a/src/units/JavaUtilConcurrent.astub +++ b/src/units/JavaUtilConcurrent.astub @@ -14,23 +14,23 @@ 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, + @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 704eb06..2001ee5 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.LiteralTreeAnnotator; import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; @@ -35,6 +36,7 @@ import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.UserError; import units.qual.BaseUnit; +import units.qual.RDU; import units.qual.UnitsAlias; import units.qual.UnitsRep; import units.representation.UnitsRepresentationUtils; @@ -55,6 +57,11 @@ protected AnnotationClassLoader createAnnotationClassLoader() { // Use the Units Annotated Type Loader instead of the default one return new UnitsAnnotationClassLoader(checker); } + + @Override + protected ViewpointAdapter createViewpointAdapter() { + return new UnitsViewpointAdapter(this); + } @Override protected Set> createSupportedTypeQualifiers() { @@ -122,7 +129,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); } @@ -151,22 +158,22 @@ protected void addCheckedCodeDefaults(QualifierDefaults defs) { // -AuseDefaultsForUncheckedCode=bytecode // uses those defaults in byte code // -AuseDefaultsForUncheckedCode=source,bytecode // also uses those defaults in // source code - @Override - protected void addUncheckedCodeDefaults(QualifierDefaults defs) { - super.addUncheckedCodeDefaults(defs); - - // experiment with: - // This seems to have no effect thus far in the constraints generated in inference - // top param, receiver, bot return for inference, explain unsat - defs.addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.RECEIVER); - defs.addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.PARAMETER); - defs.addUncheckedCodeDefault(unitsRepUtils.BOTTOM, TypeUseLocation.RETURN); - - // bot param, top return for tightest api restriction?? - - // dimensionless is default for all other locations - // defs.addUncheckedCodeDefault(unitsRepUtils.DIMENSIONLESS, TypeUseLocation.OTHERWISE); - } +// @Override +// protected void addUncheckedCodeDefaults(QualifierDefaults defs) { +// super.addUncheckedCodeDefaults(defs); +// +// // experiment with: +// // This seems to have no effect thus far in the constraints generated in inference +// // top param, receiver, bot return for inference, explain unsat +// defs.addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.RECEIVER); +// defs.addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.PARAMETER); +// defs.addUncheckedCodeDefault(unitsRepUtils.BOTTOM, TypeUseLocation.RETURN); +// +// // bot param, top return for tightest api restriction?? +// +// // dimensionless is default for all other locations +// // defs.addUncheckedCodeDefault(unitsRepUtils.DIMENSIONLESS, TypeUseLocation.OTHERWISE); +// } @Override public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { @@ -262,6 +269,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 "); @@ -299,13 +307,21 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { return true; } - // Case: @PolyAll and @PolyUnit are treated as @UnknownUnits + // Case: @PolyUnit are treated as @UnknownUnits if (AnnotationUtils.areSame(subAnno, unitsRepUtils.POLYUNIT)) { return isSubtype(unitsRepUtils.TOP, superAnno); } if (AnnotationUtils.areSame(superAnno, unitsRepUtils.POLYUNIT)) { return true; } + + // Case: @RDU are treated as @UnknownUnits + 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) diff --git a/src/units/UnitsChecker.java b/src/units/UnitsChecker.java index 7d2e1d7..69b5b59 100644 --- a/src/units/UnitsChecker.java +++ b/src/units/UnitsChecker.java @@ -19,6 +19,7 @@ "JavaMathTrig.astub", "JavaThread.astub", "JavaUtil.astub", + "JavaText.astub", "JavaUtilConcurrent.astub", // for ode4j, not yet annotated for hombucha "ExperimentsJavaAwtGeomAffineTransform.astub", // for imgscalr experiment "ExperimentsSunMiscUnsafe.astub", // for JLargeArrays diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 9c8c543..2a2c2b4 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -14,6 +14,8 @@ import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.qual.VarAnnot; +import checkers.inference.util.InferenceViewpointAdapter; + import com.sun.source.tree.BinaryTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.IdentifierTree; @@ -44,6 +46,7 @@ import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; @@ -91,6 +94,11 @@ protected AnnotationClassLoader createAnnotationClassLoader() { // Use the Units Annotated Type Loader instead of the default one return new UnitsAnnotationClassLoader(checker); } + + @Override + protected InferenceViewpointAdapter createViewpointAdapter() { + return new UnitsInferenceViewpointAdapter(this); + } // In Inference ATF, this returns the set of real qualifiers @Override @@ -234,7 +242,32 @@ public Set leastUpperBounds( return result; } - return super.leastUpperBounds(annos1, annos2); + if (annos1.isEmpty()) { + throw new BugInCF( + "QualifierHierarchy.leastUpperBounds: tried to determine LUB with empty sets"); + } + + Set result = AnnotationUtils.createAnnotationSet(); + for (AnnotationMirror a1 : annos1) { + for (AnnotationMirror a2 : annos2) { + AnnotationMirror lub = leastUpperBound(a1, a2); + if (lub != null) { + result.add(lub); + } + } + } + + if (annos1.size() == result.size() || annos2.size() == result.size()) { + return result; + } else { + throw new BugInCF("QualifierHierarchy.leastUpperBounds: resulting set has incorrect number of annotations.\n" + + " Set 1: " + + annos1 + + " Set 2: " + + annos2 + + " LUB: " + + result); + } } } diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java new file mode 100644 index 0000000..37a5cea --- /dev/null +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -0,0 +1,35 @@ +package units; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.type.TypeKind; + +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; + +import checkers.inference.util.InferenceViewpointAdapter; +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) { + if (!(type.getKind() == TypeKind.DECLARED || type.getKind() == TypeKind.ARRAY)) { + return false; + } + return super.shouldAdaptMember(type, element); + } + + @Override + protected AnnotatedTypeMirror combineAnnotationWithType(AnnotationMirror receiverAnnotation, AnnotatedTypeMirror declared) { + return super.combineAnnotationWithType(receiverAnnotation, declared); + } +} diff --git a/src/units/UnitsViewpointAdapter.java b/src/units/UnitsViewpointAdapter.java new file mode 100644 index 0000000..90dc9b0 --- /dev/null +++ b/src/units/UnitsViewpointAdapter.java @@ -0,0 +1,57 @@ +package units; + +import java.util.ArrayList; +import java.util.IdentityHashMap; +import java.util.List; +import java.util.Map; + +import javax.lang.model.element.AnnotationMirror; + +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; +import org.checkerframework.framework.type.AnnotatedTypeReplacer; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; +import org.checkerframework.javacutil.AnnotationUtils; + +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.type.TypeKind; + +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) { + if (!(type.getKind() == TypeKind.DECLARED || type.getKind() == TypeKind.ARRAY)) { + return false; + } + return super.shouldAdaptMember(type, element); + } + + + @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..d5fc8cb --- /dev/null +++ b/src/units/qual/RDU.java @@ -0,0 +1,21 @@ +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(UnknownUnits.class) +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) // ElementType.TYPE, +public @interface RDU {} diff --git a/src/units/representation/UnitsRepresentationUtils.java b/src/units/representation/UnitsRepresentationUtils.java index ed02991..f5ead4f 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; @@ -63,6 +64,8 @@ public class UnitsRepresentationUtils { public AnnotationMirror SURFACE_TOP; public AnnotationMirror SURFACE_BOTTOM; + + public AnnotationMirror RECEIVER_DEPENDANT_UNIT; // /** Instance of {@link VarAnnot} for use in UnitsVisitor in infer mode. */ // public AnnotationMirror VARANNOT; @@ -209,6 +212,7 @@ protected Map createZeroFilledBaseUnitsMap() { // units public void postInit() { POLYUNIT = AnnotationBuilder.fromClass(elements, PolyUnit.class); + RECEIVER_DEPENDANT_UNIT = AnnotationBuilder.fromClass(elements, RDU.class); RAWUNITSREP = AnnotationBuilder.fromClass(elements, UnitsRep.class); @@ -492,7 +496,7 @@ public TypecheckUnit createTypecheckUnit(AnnotationMirror anno) { TypecheckUnit unit = new TypecheckUnit(); // if it is a polyunit annotation, generate top - if (AnnotationUtils.areSameByClass(anno, PolyUnit.class)) { + if (AnnotationUtils.areSameByClass(anno, PolyUnit.class) || AnnotationUtils.areSameByClass(anno, RDU.class)) { unit.setUnknownUnits(true); } // if it is a units internal annotation, generate the internal unit From 340deae87865a92d0c552c3f8ae1cbb239d10684 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Thu, 26 Mar 2020 22:57:37 -0400 Subject: [PATCH 04/11] add tests for rdu --- src/units/UnitsAnnotatedTypeFactory.java | 4 +-- src/units/UnitsViewpointAdapter.java | 9 ----- src/units/qual/RDU.java | 1 - .../inference/JavaUtilConcurrentTimeUnit.java | 36 +++++++++---------- .../typecheck/JavaUtilConcurrentTimeUnit.java | 28 +++++++-------- 5 files changed, 33 insertions(+), 45 deletions(-) diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index ded586d..44e497a 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -36,10 +36,8 @@ import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.UserError; import units.qual.BaseUnit; -import units.qual.RDU; import units.qual.UnitsAlias; import units.qual.UnitsRep; -import units.qual.UnknownUnits; import units.representation.UnitsRepresentationUtils; import units.util.UnitsTypecheckUtils; @@ -63,7 +61,7 @@ protected AnnotationClassLoader createAnnotationClassLoader() { protected ViewpointAdapter createViewpointAdapter() { return new UnitsViewpointAdapter(this); } - + @Override protected Set> createSupportedTypeQualifiers() { // get all the loaded annotations diff --git a/src/units/UnitsViewpointAdapter.java b/src/units/UnitsViewpointAdapter.java index ccd2e1e..f3a9438 100644 --- a/src/units/UnitsViewpointAdapter.java +++ b/src/units/UnitsViewpointAdapter.java @@ -1,20 +1,11 @@ package units; -import java.util.ArrayList; -import java.util.IdentityHashMap; -import java.util.List; -import java.util.Map; - import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; -import javax.lang.model.element.ExecutableElement; import javax.lang.model.type.TypeKind; import org.checkerframework.framework.type.AbstractViewpointAdapter; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.type.AnnotatedTypeReplacer; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.javacutil.AnnotationUtils; import units.representation.UnitsRepresentationUtils; diff --git a/src/units/qual/RDU.java b/src/units/qual/RDU.java index 01f2a6a..6be2671 100644 --- a/src/units/qual/RDU.java +++ b/src/units/qual/RDU.java @@ -5,7 +5,6 @@ import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; - import org.checkerframework.framework.qual.SubtypeOf; /** diff --git a/testing/inference/JavaUtilConcurrentTimeUnit.java b/testing/inference/JavaUtilConcurrentTimeUnit.java index 990ec34..0bfbc06 100644 --- a/testing/inference/JavaUtilConcurrentTimeUnit.java +++ b/testing/inference/JavaUtilConcurrentTimeUnit.java @@ -28,30 +28,30 @@ 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 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); - } - + 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) + + // :: 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 3cd922b..ff62699 100644 --- a/testing/typecheck/JavaUtilConcurrentTimeUnit.java +++ b/testing/typecheck/JavaUtilConcurrentTimeUnit.java @@ -63,23 +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); + @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); + TimeUnit.NANOSECONDS.toMillis(s); // :: error: (argument.type.incompatible) - TimeUnit.SECONDS.toMillis(ns); - - ns_unit.toMillis(ns); - s_unit.toMillis(s); + 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); - } + s_unit.toMillis(ns); + // :: error: (argument.type.incompatible) + ns_unit.toMillis(s); + } } From dc063140fd559a3e5679aed15f6f8922f9ad550b Mon Sep 17 00:00:00 2001 From: txiang61 Date: Sat, 28 Mar 2020 08:05:19 -0400 Subject: [PATCH 05/11] fixed all failed test with the new added rdu --- .gitignore | 4 +++ src/units/UnitsAnnotatedTypeFactory.java | 26 ++----------------- .../UnitsInferenceAnnotatedTypeFactory.java | 14 +++++----- src/units/UnitsInferenceViewpointAdapter.java | 25 +++++++++++++----- src/units/UnitsViewpointAdapter.java | 8 +----- src/units/representation/TypecheckUnit.java | 2 ++ .../UnitsRepresentationUtils.java | 4 +++ .../z3smt/UnitsZ3SmtFormatTranslator.java | 6 ++--- .../UnitsZ3SmtCombineConstraintEncoder.java | 6 +++-- .../z3smt/encoder/UnitsZ3SmtEncoderUtils.java | 3 ++- .../z3smt/representation/Z3InferenceUnit.java | 5 +--- testing/inference/Casting.java | 11 ++++++-- testing/inference/Constructors.java | 13 +++------- testing/inference/Methods.java | 11 +++++++- testing/inference/StaticFinalConstants.java | 14 ---------- testing/typecheck/StaticFinalConstants.java | 20 ++++++++++++++ 16 files changed, 92 insertions(+), 80 deletions(-) create mode 100644 testing/typecheck/StaticFinalConstants.java diff --git a/.gitignore b/.gitignore index 57d0bc5..f3ca3f0 100644 --- a/.gitignore +++ b/.gitignore @@ -37,6 +37,10 @@ manual-tests/annotated manual-tests/inference manual-tests/typecheck manual-tests/insertionTest +annotated/ +unsatConstraints.txt +statistics.txt +solutions.txt # temp files manual-tests/unused* diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index 44e497a..47e9da9 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -151,29 +151,6 @@ protected void addCheckedCodeDefaults(QualifierDefaults defs) { defs.addCheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.LOCAL_VARIABLE); } - // Note: remember to use - // --cfArgs="-AuseDefaultsForUncheckedCode=source,bytecode" in cmd line option - // -AuseDefaultsForUncheckedCode=bytecode // uses those defaults in byte code - // -AuseDefaultsForUncheckedCode=source,bytecode // also uses those defaults in - // source code - // @Override - // protected void addUncheckedCodeDefaults(QualifierDefaults defs) { - // super.addUncheckedCodeDefaults(defs); - // - // // experiment with: - // // This seems to have no effect thus far in the constraints generated in inference - // // top param, receiver, bot return for inference, explain unsat - // defs.addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.RECEIVER); - // defs.addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.PARAMETER); - // defs.addUncheckedCodeDefault(unitsRepUtils.BOTTOM, TypeUseLocation.RETURN); - // - // // bot param, top return for tightest api restriction?? - // - // // dimensionless is default for all other locations - // // defs.addUncheckedCodeDefault(unitsRepUtils.DIMENSIONLESS, - // TypeUseLocation.OTHERWISE); - // } - @Override public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { return new UnitsQualifierHierarchy(factory); @@ -314,7 +291,8 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { return true; } - // Case: @RDU are treated as @UnknownUnits + // Case: @RDU shouldn't appear. + // TODO: throw error? if (AnnotationUtils.areSame(subAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { return isSubtype(unitsRepUtils.TOP, superAnno); } diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index cb7b76d..8b90cae 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -40,6 +40,8 @@ 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; @@ -383,12 +385,12 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { } } - // @Override - // public TreeAnnotator createTreeAnnotator() { - // return new ListTreeAnnotator( - // new UnitsInferenceTreeAnnotator( - // this, realChecker, realTypeFactory, variableAnnotator, slotManager)); - // } + @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 diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java index 8f2943e..5fbeaab 100644 --- a/src/units/UnitsInferenceViewpointAdapter.java +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -1,10 +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 javax.lang.model.type.TypeKind; 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 { @@ -19,11 +23,20 @@ public UnitsInferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) { @Override protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { - if (!(type.getKind() == TypeKind.DECLARED - || type.getKind() == TypeKind.ARRAY - || type.getKind().isPrimitive())) { - return false; + return false; + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + 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 super.shouldAdaptMember(type, element); + return declaredAnnotation; } } diff --git a/src/units/UnitsViewpointAdapter.java b/src/units/UnitsViewpointAdapter.java index f3a9438..dc9076b 100644 --- a/src/units/UnitsViewpointAdapter.java +++ b/src/units/UnitsViewpointAdapter.java @@ -2,7 +2,6 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; -import javax.lang.model.type.TypeKind; import org.checkerframework.framework.type.AbstractViewpointAdapter; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -21,12 +20,7 @@ public UnitsViewpointAdapter(AnnotatedTypeFactory atypeFactory) { @Override protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { - if (!(type.getKind() == TypeKind.DECLARED - || type.getKind() == TypeKind.ARRAY - || type.getKind().isPrimitive())) { - return false; - } - return super.shouldAdaptMember(type, element); + return false; } @Override diff --git a/src/units/representation/TypecheckUnit.java b/src/units/representation/TypecheckUnit.java index ec2ac06..6a45a05 100644 --- a/src/units/representation/TypecheckUnit.java +++ b/src/units/representation/TypecheckUnit.java @@ -21,6 +21,8 @@ public TypecheckUnit() { uu = false; // default UU value is false ub = false; + // default RDU value is false + rdu = false; // default prefixExponent is 0 prefixExponent = 0; // default exponents are 0 diff --git a/src/units/representation/UnitsRepresentationUtils.java b/src/units/representation/UnitsRepresentationUtils.java index 1e460b2..a85e4f1 100644 --- a/src/units/representation/UnitsRepresentationUtils.java +++ b/src/units/representation/UnitsRepresentationUtils.java @@ -584,6 +584,10 @@ public void setSerializedBaseUnits(Set constantSlots) { TypecheckUnit unit = createTypecheckUnit(slot.getValue()); // System.err.println(unit); + if (unit.isRDUnits()) { + continue; + } + serializePrefix = serializePrefix || (unit.getPrefixExponent() != 0); for (Entry baseUnitExponents : unit.getExponents().entrySet()) { diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index 98645e8..ca6d47e 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,8 +139,7 @@ protected Z3InferenceUnit serializeConstantSlot(ConstantSlot slot) { encodedSlot.setUnknownUnits(true); } else if (unit.isUnitsBottom()) { encodedSlot.setUnitsBottom(true); - } - if (unit.isRDUnits()) { + } else if (unit.isRDUnits()) { encodedSlot.setRDUnits(true); } else { encodedSlot.setPrefixExponent(unit.getPrefixExponent()); @@ -229,8 +229,6 @@ public Map decodeSolution( z3Slot.setUnknownUnits(Boolean.parseBoolean(value)); } else if (component.contentEquals(UnitsZ3SmtEncoderUtils.ubSlotName)) { z3Slot.setUnitsBottom(Boolean.parseBoolean(value)); - } else if (component.contentEquals(UnitsZ3SmtEncoderUtils.rduSlotName)) { - z3Slot.setRDUnits(Boolean.parseBoolean(value)); } else if (component.contentEquals(UnitsZ3SmtEncoderUtils.prefixSlotName)) { z3Slot.setPrefixExponent(Integer.parseInt(value)); } else { diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java index f89e204..c578096 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java @@ -38,7 +38,8 @@ private BoolExpr receiver_dependent( @Override public BoolExpr encodeVariable_Variable( VariableSlot target, VariableSlot declared, VariableSlot result) { - return receiver_dependent(target, declared, result); + return ctx.mkTrue(); + // return receiver_dependent(target, declared, result); } @Override @@ -50,7 +51,8 @@ public BoolExpr encodeVariable_Constant( @Override public BoolExpr encodeConstant_Variable( ConstantSlot target, VariableSlot declared, VariableSlot result) { - return receiver_dependent(target, declared, result); + return ctx.mkTrue(); + // return receiver_dependent(target, declared, result); } @Override diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java index c3b3560..dc3457d 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java @@ -16,7 +16,6 @@ public class UnitsZ3SmtEncoderUtils { private static final char idComponentSeparator = '-'; public static final String uuSlotName = "TOP"; public static final String ubSlotName = "BOT"; - public static final String rduSlotName = "RDU"; public static final String prefixSlotName = "PREFIX"; public static String z3VarName(int slotID, String component) { @@ -128,6 +127,7 @@ private static BoolExpr mustBeDimensionless(Context ctx, Z3InferenceUnit unit) { BoolExpr allExponentsAreZero = allExponentsAreZero(ctx, unit); /* @formatter:off // this is for eclipse formatter */ return ctx.mkAnd( + ctx.mkNot(unit.getRDUnits()), ctx.mkNot(unit.getUnknownUnits()), ctx.mkNot(unit.getUnitsBottom()), allExponentsAreZero); @@ -142,6 +142,7 @@ public static BoolExpr equality(Context ctx, Z3InferenceUnit fst, Z3InferenceUni /* @formatter:off // this is for eclipse formatter */ BoolExpr equalityEncoding = ctx.mkAnd( + ctx.mkEq(fst.getRDUnits(), snd.getRDUnits()), ctx.mkEq(fst.getUnknownUnits(), snd.getUnknownUnits()), ctx.mkEq(fst.getUnitsBottom(), snd.getUnitsBottom())); if (UnitsRepresentationUtils.getInstance().serializePrefix()) { diff --git a/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java b/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java index 27a0611..633c1a9 100644 --- a/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java +++ b/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java @@ -66,10 +66,7 @@ public static Z3InferenceUnit makeVariableSlot(Context ctx, int slotID) { UnitsZ3SmtEncoderUtils.z3VarName( slotID, UnitsZ3SmtEncoderUtils.ubSlotName)); - slot.rdu = - ctx.mkBoolConst( - UnitsZ3SmtEncoderUtils.z3VarName( - slotID, UnitsZ3SmtEncoderUtils.rduSlotName)); + slot.rdu = ctx.mkBool(false); slot.prefixExponent = ctx.mkIntConst( diff --git a/testing/inference/Casting.java b/testing/inference/Casting.java index 5bf3284..6d7dbd5 100644 --- a/testing/inference/Casting.java +++ b/testing/inference/Casting.java @@ -8,7 +8,14 @@ class Casting { int primDim = (int) 20.0f; - Integer boxDim = 20; + int boxDim = 20; + @m int boxM = (@m int) boxDim; - @m Integer boxM = (@m Integer) boxDim; + void cast() { + int x = 20; + @m int y = (@m int) x; + + Integer boxX = 20; + @m Integer boxY = (@m Integer) boxX; + } } diff --git a/testing/inference/Constructors.java b/testing/inference/Constructors.java index 07f26f4..afafce5 100644 --- a/testing/inference/Constructors.java +++ b/testing/inference/Constructors.java @@ -5,11 +5,6 @@ class PolyUnitClass { @PolyUnit PolyUnitClass(@PolyUnit int x) {} } -class MeterClass { - // :: error: (super.invocation.invalid) - @m MeterClass(@m int x) {} -} - class NoAnnotClass { NoAnnotClass(int x) {} } @@ -37,10 +32,10 @@ void polyUnitConstructorTest() { } void nonPolyConstructorTest() { - // :: fixable-error: (argument.type.incompatible) - @m MeterClass mc1 = new MeterClass(5); - // :: fixable-error: (argument.type.incompatible) - @m MeterClass mc2 = new @m MeterClass(5); + // :: fixable-error: (assignment.type.incompatible) + @m Integer mc1 = new Integer(5); + // :: fixable-error: (constructor.invocation.invalid) + @m Integer mc2 = new @m Integer(5); @Dimensionless NoAnnotClass na1 = new NoAnnotClass(5); } diff --git a/testing/inference/Methods.java b/testing/inference/Methods.java index 8dad62d..277cdbf 100644 --- a/testing/inference/Methods.java +++ b/testing/inference/Methods.java @@ -14,11 +14,20 @@ class Methods { return x; } + int method(int x) { + return x; + } + + void testMethod() { + // :: fixable-error: (assignment.type.incompatible) + @m int num = method(5); + } + void polyUnitMethodTest() { // :: fixable-error: (assignment.type.incompatible) @m int pum1 = polyUnitMethod(5); - int pum2 = polyUnitMethod(5 * UnitsTools.m); + @m int pum2 = polyUnitMethod(5 * UnitsTools.m); // :: fixable-error: (assignment.type.incompatible) @m int pum3 = polyUnitMethod(5, 6); diff --git a/testing/inference/StaticFinalConstants.java b/testing/inference/StaticFinalConstants.java index dcfa473..5477cde 100644 --- a/testing/inference/StaticFinalConstants.java +++ b/testing/inference/StaticFinalConstants.java @@ -5,20 +5,6 @@ class StaticFinalConstants { - void inferRadians() { - // :: fixable-error: (argument.type.incompatible) - Math.sin(Math.E); - - // :: fixable-error: (argument.type.incompatible) - Math.cos(Math.PI); - - // :: fixable-error: (argument.type.incompatible) - sin(E); - - // :: fixable-error: (argument.type.incompatible) - cos(PI); - } - static class MyConstants { public static final double X = 10; public static final Integer Y = Integer.MAX_VALUE; diff --git a/testing/typecheck/StaticFinalConstants.java b/testing/typecheck/StaticFinalConstants.java new file mode 100644 index 0000000..49ba5c8 --- /dev/null +++ b/testing/typecheck/StaticFinalConstants.java @@ -0,0 +1,20 @@ +import static java.lang.Math.*; + +import units.qual.*; + +class StaticFinalConstants { + + void inferRadians() { + // :: error: (argument.type.incompatible) + Math.sin(Math.E); + + // :: error: (argument.type.incompatible) + Math.cos(Math.PI); + + // :: error: (argument.type.incompatible) + sin(E); + + // :: error: (argument.type.incompatible) + cos(PI); + } +} From 6e152c5f7607f900f019e92d4ec9e6d96a51054c Mon Sep 17 00:00:00 2001 From: txiang61 Date: Mon, 30 Mar 2020 16:20:41 -0400 Subject: [PATCH 06/11] comments and edges cases --- src/units/UnitsAnnotatedTypeFactory.java | 3 +-- src/units/UnitsInferenceViewpointAdapter.java | 3 +++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index 47e9da9..4764ccc 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -291,8 +291,7 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { return true; } - // Case: @RDU shouldn't appear. - // TODO: throw error? + // Case: @RDU shouldn't appear. throw error? if (AnnotationUtils.areSame(subAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { return isSubtype(unitsRepUtils.TOP, superAnno); } diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java index 5fbeaab..f2acfa2 100644 --- a/src/units/UnitsInferenceViewpointAdapter.java +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -29,6 +29,9 @@ protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { @Override protected AnnotationMirror combineAnnotationWithAnnotation( AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + if (InferenceMain.isHackMode(declaredAnnotation == null)) { + return declaredAnnotation; + } Slot declSlot = InferenceMain.getInstance().getSlotManager().getSlot(declaredAnnotation); if (declSlot.isConstant()) { ConstantSlot cs = (ConstantSlot) declSlot; From d0c53083372b5b8aa4ff5e822889a88ed0c9edd2 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Mon, 30 Mar 2020 17:30:35 -0400 Subject: [PATCH 07/11] added more test on RDU --- testing/typecheck/RDUMethodReceiver.java | 34 ++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 testing/typecheck/RDUMethodReceiver.java diff --git a/testing/typecheck/RDUMethodReceiver.java b/testing/typecheck/RDUMethodReceiver.java new file mode 100644 index 0000000..72bf1f8 --- /dev/null +++ b/testing/typecheck/RDUMethodReceiver.java @@ -0,0 +1,34 @@ +import units.qual.*; + +public class RDUMethodReceiver { + + public class MeterClass { + @RDU Object get(@m MeterClass this) { return null; } + Object set(@m MeterClass this, @RDU Object x) { return null; } + } + + 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); + } +} \ No newline at end of file From 941c11de38d8f52d24fd7ae7a062fbd746595d14 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Mon, 13 Apr 2020 14:00:23 -0400 Subject: [PATCH 08/11] default Object class to UnitsBottom --- src/units/JavaLang.astub | 3 + src/units/JavaUtilConcurrent.astub | 1 + .../UnitsInferenceAnnotatedTypeFactory.java | 28 ++++----- src/units/UnitsInferenceViewpointAdapter.java | 2 +- testing/typecheck/RDUMethodReceiver.java | 30 +++++++--- testing/typecheck/TimeUnits.java | 58 +++++++++++++++++++ 6 files changed, 99 insertions(+), 23 deletions(-) create mode 100644 testing/typecheck/TimeUnits.java diff --git a/src/units/JavaLang.astub b/src/units/JavaLang.astub index 684908d..41eb062 100644 --- a/src/units/JavaLang.astub +++ b/src/units/JavaLang.astub @@ -2,6 +2,9 @@ import units.qual.*; package java.lang; +@UnitsBottom class Object{ +} + class System { static @ms long currentTimeMillis(); static @ns long nanoTime(); diff --git a/src/units/JavaUtilConcurrent.astub b/src/units/JavaUtilConcurrent.astub index e733293..d80a05d 100644 --- a/src/units/JavaUtilConcurrent.astub +++ b/src/units/JavaUtilConcurrent.astub @@ -2,6 +2,7 @@ import units.qual.*; package java.util.concurrent; +@UnitsBottom enum TimeUnit { @ns NANOSECONDS, @us MICROSECONDS, diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 8b90cae..81c94a1 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -257,19 +257,21 @@ public Set leastUpperBounds( } } } - - if (annos1.size() == result.size() || annos2.size() == result.size()) { - return result; - } else { - throw new BugInCF( - "QualifierHierarchy.leastUpperBounds: resulting set has incorrect number of annotations.\n" - + " Set 1: " - + annos1 - + " Set 2: " - + annos2 - + " LUB: " - + result); - } + + return result; + +// if (annos1.size() == result.size() || annos2.size() == result.size()) { +// return result; +// } else { +// throw new BugInCF( +// "QualifierHierarchy.leastUpperBounds: resulting set has incorrect number of annotations.\n" +// + " Set 1: " +// + annos1 +// + " Set 2: " +// + annos2 +// + " LUB: " +// + result); +// } } // @Override diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java index f2acfa2..fb1934f 100644 --- a/src/units/UnitsInferenceViewpointAdapter.java +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -30,7 +30,7 @@ protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { protected AnnotationMirror combineAnnotationWithAnnotation( AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { if (InferenceMain.isHackMode(declaredAnnotation == null)) { - return declaredAnnotation; + return unitsRepUtils.BOTTOM; } Slot declSlot = InferenceMain.getInstance().getSlotManager().getSlot(declaredAnnotation); if (declSlot.isConstant()) { diff --git a/testing/typecheck/RDUMethodReceiver.java b/testing/typecheck/RDUMethodReceiver.java index 72bf1f8..2d29c90 100644 --- a/testing/typecheck/RDUMethodReceiver.java +++ b/testing/typecheck/RDUMethodReceiver.java @@ -2,14 +2,26 @@ public class RDUMethodReceiver { - public class MeterClass { - @RDU Object get(@m MeterClass this) { return null; } - Object set(@m MeterClass this, @RDU Object x) { return null; } + @m public class MeterClass { + @RDU + Object get(@m MeterClass this) { + return null; + } + + Object set(@m MeterClass this, @RDU Object x) { + return null; + } } - public class SecondClass { - @RDU Object get(@s SecondClass this) { return null; } - Object set(@s SecondClass this, @RDU Object x) { return null; } + @s public class SecondClass { + @RDU + Object get(@s SecondClass this) { + return null; + } + + Object set(@s SecondClass this, @RDU Object x) { + return null; + } } void invoke() { @@ -21,14 +33,14 @@ void invoke() { @s Object y = sc.get(); sc.set(y); - // :: error: (assignment.type.incompatible) + // :: error: (assignment.type.incompatible) @m Object z = sc.get(); // :: error: (argument.type.incompatible) sc.set(z); - // :: error: (assignment.type.incompatible) + // :: error: (assignment.type.incompatible) @s Object w = mc.get(); // :: error: (argument.type.incompatible) mc.set(w); } -} \ No newline at end of file +} diff --git a/testing/typecheck/TimeUnits.java b/testing/typecheck/TimeUnits.java new file mode 100644 index 0000000..ec9cfda --- /dev/null +++ b/testing/typecheck/TimeUnits.java @@ -0,0 +1,58 @@ +import units.qual.*; + +@UnknownUnits +enum TimeUnit { + @ns NANOSECONDS, + @us MICROSECONDS, + @ms MILLISECONDS, + @s SECONDS; + + // For example, to convert 10 minutes to milliseconds, use: + // TimeUnit.MILLISECONDS.convert(10L, TimeUnit.MINUTES) + // TODO: enforce source value and unit are equal + @RDU long convert(@UnknownUnits TimeUnit this, @UnknownUnits long sourceDuration, + @UnknownUnits TimeUnit sourceUnit) { + return 0; + } + + // TODO: add dimensional bound on duration to be a time value + @ns long toNanos(@UnknownUnits TimeUnit this, @RDU long duration) { + return (@ns long) 0; + } + + @us long toMicros(@UnknownUnits TimeUnit this, @RDU long duration) { + return (@us long) 0; + } + + @ms long toMillis(@UnknownUnits TimeUnit this, @RDU long duration) { + return (@ms long) 0; + } + + @s long toSeconds(@UnknownUnits TimeUnit this, @RDU long duration) { + return (@s long) 0; + } + + + void test() { + @s + TimeUnit s = TimeUnit.SECONDS; + + @ms + TimeUnit ms = TimeUnit.MILLISECONDS; + + @us + TimeUnit us = TimeUnit.MICROSECONDS; + + @ns + TimeUnit ns = TimeUnit.NANOSECONDS; + + @s long seconds = s.convert(10, NANOSECONDS); + + // convert 10 minutes to milliseconds + @ms long milliseconds = ms.convert(10, TimeUnit.SECONDS); + + @us long microsec = us.convert(10, TimeUnit.SECONDS); + + @ns long nanosec = ns.convert(10, TimeUnit.SECONDS); + } +} \ No newline at end of file From cefde9605f6b66e77b5ca2faae64780d64ad3654 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Mon, 13 Apr 2020 22:41:27 -0400 Subject: [PATCH 09/11] modify constraints --- .../solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java | 6 ++++-- .../backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java | 5 +++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index ca6d47e..292e443 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java @@ -169,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(); @@ -176,9 +177,10 @@ 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/UnitsZ3SmtEncoderUtils.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java index dc3457d..40290ec 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java @@ -91,11 +91,12 @@ public static BoolExpr slotWellformedness(Context ctx, Z3InferenceUnit unit) { // variable declarations outputted for the z3 files BoolExpr allExponentsAreZero = allExponentsAreZero(ctx, unit); /* @formatter:off // this is for eclipse formatter */ - return UnitsZ3SmtEncoderUtils.mkOneHot( + return ctx.mkAnd(ctx.mkNot(unit.getRDUnits()), + UnitsZ3SmtEncoderUtils.mkOneHot( ctx, ctx.mkAnd(ctx.mkNot(unit.getUnknownUnits()), ctx.mkNot(unit.getUnitsBottom())), ctx.mkAnd(unit.getUnknownUnits(), allExponentsAreZero), - ctx.mkAnd(unit.getUnitsBottom(), allExponentsAreZero)); + ctx.mkAnd(unit.getUnitsBottom(), allExponentsAreZero))); /* @formatter:on // this is for eclipse formatter */ // simplify xor (xor ((not x and not y), x), y) From 37f1efb8e245f0af09c53abdc1a85c0ab64a4117 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Mon, 13 Apr 2020 22:43:06 -0400 Subject: [PATCH 10/11] added astub file for java awt library --- src/units/JavaAWT.astub | 9 ++++++ src/units/JavaAWTGeom.astub | 12 +++++++ src/units/UnitsAnnotatedTypeFactory.java | 29 +++++++++++++++++ src/units/UnitsChecker.java | 3 +- src/units/UnitsInferenceViewpointAdapter.java | 2 +- testing/typecheck/RDUMethodReceiver.java | 32 +++++++++++++++---- 6 files changed, 78 insertions(+), 9 deletions(-) create mode 100644 src/units/JavaAWT.astub create mode 100644 src/units/JavaAWTGeom.astub diff --git a/src/units/JavaAWT.astub b/src/units/JavaAWT.astub new file mode 100644 index 0000000..93a1cb2 --- /dev/null +++ b/src/units/JavaAWT.astub @@ -0,0 +1,9 @@ +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..014f982 --- /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); +} \ No newline at end of file diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index 4764ccc..b836d8a 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -9,6 +9,7 @@ import java.util.Map.Entry; import java.util.Set; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.util.Elements; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.LiteralKind; @@ -151,6 +152,34 @@ protected void addCheckedCodeDefaults(QualifierDefaults defs) { defs.addCheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.LOCAL_VARIABLE); } + @Override + protected QualifierDefaults createQualifierDefaults() { + return new UnitsQualifierDefaults(elements, this); + } + + private class UnitsQualifierDefaults extends QualifierDefaults { + + public UnitsQualifierDefaults(Elements elements, AnnotatedTypeFactory atypeFactory) { + super(elements, atypeFactory); + } + + public void addUncheckedStandardDefaults() { + super.addUncheckedStandardDefaults(); + + // experiment with: + // This seems to have no effect thus far in the constraints generated in inference + // top param, receiver, bot return for inference, explain unsat + addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.RECEIVER); + addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.PARAMETER); + addUncheckedCodeDefault(unitsRepUtils.BOTTOM, TypeUseLocation.RETURN); + + // bot param, top return for tightest api restriction?? + + // dimensionless is default for all other locations + // addUncheckedCodeDefault(unitsRepUtils.DIMENSIONLESS, TypeUseLocation.OTHERWISE); + } + } + @Override public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { return new UnitsQualifierHierarchy(factory); diff --git a/src/units/UnitsChecker.java b/src/units/UnitsChecker.java index 69b5b59..44b2c2e 100644 --- a/src/units/UnitsChecker.java +++ b/src/units/UnitsChecker.java @@ -20,8 +20,9 @@ "JavaThread.astub", "JavaUtil.astub", "JavaText.astub", + "JavaAWT.astub", // for josm "JavaUtilConcurrent.astub", // for ode4j, not yet annotated for hombucha - "ExperimentsJavaAwtGeomAffineTransform.astub", // for imgscalr experiment + // "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 f2acfa2..8da8033 100644 --- a/src/units/UnitsInferenceViewpointAdapter.java +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -30,7 +30,7 @@ protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { protected AnnotationMirror combineAnnotationWithAnnotation( AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { if (InferenceMain.isHackMode(declaredAnnotation == null)) { - return declaredAnnotation; + return unitsRepUtils.DIMENSIONLESS; } Slot declSlot = InferenceMain.getInstance().getSlotManager().getSlot(declaredAnnotation); if (declSlot.isConstant()) { diff --git a/testing/typecheck/RDUMethodReceiver.java b/testing/typecheck/RDUMethodReceiver.java index 72bf1f8..d93876b 100644 --- a/testing/typecheck/RDUMethodReceiver.java +++ b/testing/typecheck/RDUMethodReceiver.java @@ -3,13 +3,31 @@ public class RDUMethodReceiver { 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) + public @m MeterClass() {} + + @RDU + Object get(@m MeterClass this) { + return null; + } + + Object set(@m MeterClass this, @RDU Object x) { + return null; + } } public class SecondClass { - @RDU Object get(@s SecondClass this) { return null; } - Object set(@s SecondClass this, @RDU Object x) { return null; } + // :: error: (super.invocation.invalid) + public @s SecondClass() {} + + @RDU + Object get(@s SecondClass this) { + return null; + } + + Object set(@s SecondClass this, @RDU Object x) { + return null; + } } void invoke() { @@ -21,14 +39,14 @@ void invoke() { @s Object y = sc.get(); sc.set(y); - // :: error: (assignment.type.incompatible) + // :: error: (assignment.type.incompatible) @m Object z = sc.get(); // :: error: (argument.type.incompatible) sc.set(z); - // :: error: (assignment.type.incompatible) + // :: error: (assignment.type.incompatible) @s Object w = mc.get(); // :: error: (argument.type.incompatible) mc.set(w); } -} \ No newline at end of file +} From 483bec30b4884a08c219a5ec6f272623fb54fa0c Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Mon, 13 Apr 2020 22:45:17 -0400 Subject: [PATCH 11/11] corrected tests file --- src/units/UnitsAnnotatedTypeFactory.java | 29 ---------- .../UnitsInferenceAnnotatedTypeFactory.java | 17 +----- .../z3smt/encoder/UnitsZ3SmtEncoderUtils.java | 15 +++-- testing/inference/Constructors.java | 18 +++--- testing/inference/GenericMethods.java | 1 - .../inference/JavaUtilConcurrentTimeUnit.java | 1 + testing/inference/Methods.java | 2 +- testing/typecheck/Constructors.java | 7 +-- .../typecheck/JavaUtilConcurrentTimeUnit.java | 1 + testing/typecheck/Methods.java | 2 +- testing/typecheck/TimeUnits.java | 58 ------------------- 11 files changed, 29 insertions(+), 122 deletions(-) delete mode 100644 testing/typecheck/TimeUnits.java diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index b836d8a..4764ccc 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -9,7 +9,6 @@ import java.util.Map.Entry; import java.util.Set; import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.util.Elements; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.LiteralKind; @@ -152,34 +151,6 @@ protected void addCheckedCodeDefaults(QualifierDefaults defs) { defs.addCheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.LOCAL_VARIABLE); } - @Override - protected QualifierDefaults createQualifierDefaults() { - return new UnitsQualifierDefaults(elements, this); - } - - private class UnitsQualifierDefaults extends QualifierDefaults { - - public UnitsQualifierDefaults(Elements elements, AnnotatedTypeFactory atypeFactory) { - super(elements, atypeFactory); - } - - public void addUncheckedStandardDefaults() { - super.addUncheckedStandardDefaults(); - - // experiment with: - // This seems to have no effect thus far in the constraints generated in inference - // top param, receiver, bot return for inference, explain unsat - addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.RECEIVER); - addUncheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.PARAMETER); - addUncheckedCodeDefault(unitsRepUtils.BOTTOM, TypeUseLocation.RETURN); - - // bot param, top return for tightest api restriction?? - - // dimensionless is default for all other locations - // addUncheckedCodeDefault(unitsRepUtils.DIMENSIONLESS, TypeUseLocation.OTHERWISE); - } - } - @Override public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { return new UnitsQualifierHierarchy(factory); diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 81c94a1..af531cc 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -243,7 +243,7 @@ public Set leastUpperBounds( return result; } - if (annos1.isEmpty()) { + if (annos1.isEmpty() || annos2.isEmpty()) { throw new BugInCF( "QualifierHierarchy.leastUpperBounds: tried to determine LUB with empty sets"); } @@ -257,21 +257,8 @@ public Set leastUpperBounds( } } } - - return result; -// if (annos1.size() == result.size() || annos2.size() == result.size()) { -// return result; -// } else { -// throw new BugInCF( -// "QualifierHierarchy.leastUpperBounds: resulting set has incorrect number of annotations.\n" -// + " Set 1: " -// + annos1 -// + " Set 2: " -// + annos2 -// + " LUB: " -// + result); -// } + return result; } // @Override diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java index 40290ec..c044504 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java @@ -91,12 +91,15 @@ public static BoolExpr slotWellformedness(Context ctx, Z3InferenceUnit unit) { // variable declarations outputted for the z3 files BoolExpr allExponentsAreZero = allExponentsAreZero(ctx, unit); /* @formatter:off // this is for eclipse formatter */ - return ctx.mkAnd(ctx.mkNot(unit.getRDUnits()), - UnitsZ3SmtEncoderUtils.mkOneHot( - ctx, - ctx.mkAnd(ctx.mkNot(unit.getUnknownUnits()), ctx.mkNot(unit.getUnitsBottom())), - ctx.mkAnd(unit.getUnknownUnits(), allExponentsAreZero), - ctx.mkAnd(unit.getUnitsBottom(), allExponentsAreZero))); + return ctx.mkAnd( + ctx.mkNot(unit.getRDUnits()), + UnitsZ3SmtEncoderUtils.mkOneHot( + ctx, + ctx.mkAnd( + ctx.mkNot(unit.getUnknownUnits()), + ctx.mkNot(unit.getUnitsBottom())), + ctx.mkAnd(unit.getUnknownUnits(), allExponentsAreZero), + ctx.mkAnd(unit.getUnitsBottom(), allExponentsAreZero))); /* @formatter:on // this is for eclipse formatter */ // simplify xor (xor ((not x and not y), x), y) diff --git a/testing/inference/Constructors.java b/testing/inference/Constructors.java index afafce5..928200d 100644 --- a/testing/inference/Constructors.java +++ b/testing/inference/Constructors.java @@ -5,6 +5,10 @@ class PolyUnitClass { @PolyUnit PolyUnitClass(@PolyUnit int x) {} } +class MeterClass { + @m MeterClass(@m int x) {} +} + class NoAnnotClass { NoAnnotClass(int x) {} } @@ -21,21 +25,21 @@ void polyUnitConstructorTest() { PolyUnitClass puc2 = new PolyUnitClass(5 * UnitsTools.m); // propagate @m from constructor return type - // :: fixable-error: (constructor.invocation.invalid) + // :: fixable-warning: (cast.unsafe.constructor.invocation) PolyUnitClass puc3 = new @m PolyUnitClass(5); - // :: fixable-error: (constructor.invocation.invalid) + // :: fixable-warning: (cast.unsafe.constructor.invocation) @m PolyUnitClass puc4 = new @m PolyUnitClass(5); - // :: fixable-error: (constructor.invocation.invalid) + // :: fixable-warning: (cast.unsafe.constructor.invocation) PolyUnitClass puc5 = new @m PolyUnitClass(5 * UnitsTools.s); } void nonPolyConstructorTest() { - // :: fixable-error: (assignment.type.incompatible) - @m Integer mc1 = new Integer(5); - // :: fixable-error: (constructor.invocation.invalid) - @m Integer mc2 = new @m Integer(5); + // :: fixable-error: (argument.type.incompatible) + @m MeterClass mc1 = new MeterClass(5); + // :: fixable-error: (argument.type.incompatible) + @m MeterClass mc2 = new @m MeterClass(5); @Dimensionless NoAnnotClass na1 = new NoAnnotClass(5); } diff --git a/testing/inference/GenericMethods.java b/testing/inference/GenericMethods.java index 43bdaf0..caed357 100644 --- a/testing/inference/GenericMethods.java +++ b/testing/inference/GenericMethods.java @@ -12,7 +12,6 @@ public T idOne(T param) { } public String mStringCatOne(T param) { - // :: fixable-error: (method.invocation.invalid) return param.toString() + param; } diff --git a/testing/inference/JavaUtilConcurrentTimeUnit.java b/testing/inference/JavaUtilConcurrentTimeUnit.java index 0bfbc06..66301a2 100644 --- a/testing/inference/JavaUtilConcurrentTimeUnit.java +++ b/testing/inference/JavaUtilConcurrentTimeUnit.java @@ -6,6 +6,7 @@ class JavaUtilConcurrentTimeUnit { void test(long time, TimeUnit unit) throws Exception { + // :: fixable-error: (argument.type.incompatible) long milliseconds = unit.toMillis(time); Thread.sleep(milliseconds); } diff --git a/testing/inference/Methods.java b/testing/inference/Methods.java index 277cdbf..655a2cb 100644 --- a/testing/inference/Methods.java +++ b/testing/inference/Methods.java @@ -27,7 +27,7 @@ void polyUnitMethodTest() { // :: fixable-error: (assignment.type.incompatible) @m int pum1 = polyUnitMethod(5); - @m int pum2 = polyUnitMethod(5 * UnitsTools.m); + int pum2 = polyUnitMethod(5 * UnitsTools.m); // :: fixable-error: (assignment.type.incompatible) @m int pum3 = polyUnitMethod(5, 6); diff --git a/testing/typecheck/Constructors.java b/testing/typecheck/Constructors.java index d496bb4..d8c4293 100644 --- a/testing/typecheck/Constructors.java +++ b/testing/typecheck/Constructors.java @@ -6,7 +6,6 @@ class PolyUnitClass { } class MeterClass { - // :: error: (super.invocation.invalid) @m MeterClass(@m int x) {} } @@ -21,13 +20,13 @@ void polyUnitConstructorTest() { PolyUnitClass puc2 = new PolyUnitClass(5 * UnitsTools.m); - // :: error: (constructor.invocation.invalid) + // :: warning: (cast.unsafe.constructor.invocation) PolyUnitClass puc3 = new @m PolyUnitClass(5); - // :: error: (constructor.invocation.invalid) + // :: warning: (cast.unsafe.constructor.invocation) @m PolyUnitClass puc4 = new @m PolyUnitClass(5); - // :: error: (constructor.invocation.invalid) + // :: warning: (cast.unsafe.constructor.invocation) PolyUnitClass puc5 = new @m PolyUnitClass(5 * UnitsTools.s); } diff --git a/testing/typecheck/JavaUtilConcurrentTimeUnit.java b/testing/typecheck/JavaUtilConcurrentTimeUnit.java index ff62699..7a6da7c 100644 --- a/testing/typecheck/JavaUtilConcurrentTimeUnit.java +++ b/testing/typecheck/JavaUtilConcurrentTimeUnit.java @@ -23,6 +23,7 @@ void readFromEnumInSource() { } void test(long time, TimeUnit unit) throws Exception { + // :: error: (argument.type.incompatible) @ms long milliseconds = unit.toMillis(time); Thread.sleep(milliseconds); } diff --git a/testing/typecheck/Methods.java b/testing/typecheck/Methods.java index da23277..363bd49 100644 --- a/testing/typecheck/Methods.java +++ b/testing/typecheck/Methods.java @@ -23,7 +23,7 @@ void polyUnitMethodTest() { // :: error: (assignment.type.incompatible) @m int pum3 = polyUnitMethod(5, 6); - @m int pum4 = polyUnitMethod(UnitsTools.m, UnitsTools.m); + int pum4 = polyUnitMethod(UnitsTools.m, UnitsTools.m); // :: error: (assignment.type.incompatible) @m int pum5 = polyUnitMethod(UnitsTools.m, UnitsTools.s); diff --git a/testing/typecheck/TimeUnits.java b/testing/typecheck/TimeUnits.java deleted file mode 100644 index ec9cfda..0000000 --- a/testing/typecheck/TimeUnits.java +++ /dev/null @@ -1,58 +0,0 @@ -import units.qual.*; - -@UnknownUnits -enum TimeUnit { - @ns NANOSECONDS, - @us MICROSECONDS, - @ms MILLISECONDS, - @s SECONDS; - - // For example, to convert 10 minutes to milliseconds, use: - // TimeUnit.MILLISECONDS.convert(10L, TimeUnit.MINUTES) - // TODO: enforce source value and unit are equal - @RDU long convert(@UnknownUnits TimeUnit this, @UnknownUnits long sourceDuration, - @UnknownUnits TimeUnit sourceUnit) { - return 0; - } - - // TODO: add dimensional bound on duration to be a time value - @ns long toNanos(@UnknownUnits TimeUnit this, @RDU long duration) { - return (@ns long) 0; - } - - @us long toMicros(@UnknownUnits TimeUnit this, @RDU long duration) { - return (@us long) 0; - } - - @ms long toMillis(@UnknownUnits TimeUnit this, @RDU long duration) { - return (@ms long) 0; - } - - @s long toSeconds(@UnknownUnits TimeUnit this, @RDU long duration) { - return (@s long) 0; - } - - - void test() { - @s - TimeUnit s = TimeUnit.SECONDS; - - @ms - TimeUnit ms = TimeUnit.MILLISECONDS; - - @us - TimeUnit us = TimeUnit.MICROSECONDS; - - @ns - TimeUnit ns = TimeUnit.NANOSECONDS; - - @s long seconds = s.convert(10, NANOSECONDS); - - // convert 10 minutes to milliseconds - @ms long milliseconds = ms.convert(10, TimeUnit.SECONDS); - - @us long microsec = us.convert(10, TimeUnit.SECONDS); - - @ns long nanosec = ns.convert(10, TimeUnit.SECONDS); - } -} \ No newline at end of file