diff --git a/.classpath b/.classpath index 5c45723..7c6ac24 100644 --- a/.classpath +++ b/.classpath @@ -4,8 +4,9 @@ - + + 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/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/dependency-setup.sh b/dependency-setup.sh index e9af5c9..96d4a78 100755 --- a/dependency-setup.sh +++ b/dependency-setup.sh @@ -18,7 +18,7 @@ echo "------ Downloading everthing from REPO_SITE: $REPO_SITE ------" if [ -d $JSR308/checker-framework-inference ] ; then (cd $JSR308/checker-framework-inference && git pull) else - BRANCH=upstream_update_mar_5_2019 + BRANCH=master echo "Cloning from branch" $BRANCH (cd $JSR308 && git clone -b $BRANCH --depth 1 https://github.com/"$REPO_SITE"/checker-framework-inference.git) fi diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar index a5fe1cb..1948b90 100644 Binary files a/gradle/wrapper/gradle-wrapper.jar and b/gradle/wrapper/gradle-wrapper.jar differ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index be280be..838e6bc 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists +distributionUrl=https\://services.gradle.org/distributions/gradle-5.3-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-4.5-bin.zip diff --git a/scripts/run-units-infer.sh b/scripts/run-units-infer.sh index 78cc508..e4c164c 100755 --- a/scripts/run-units-infer.sh +++ b/scripts/run-units-infer.sh @@ -14,6 +14,9 @@ export PATH=$AFU/scripts:$PATH CHECKER=units.UnitsChecker SOLVER=units.solvers.backend.UnitsSolverEngine +DEBUG_SOLVER=checkers.inference.solver.DebugSolver +# SOLVER="$DEBUG_SOLVER" + if [ -n "$1" ] && [ $1 = "GJE" ]; then SOLVERARGS=solver=GJE,collectStatistics=true,writeSolutions=true,noAppend=true elif [ -n "$1" ] && [ $1 = "true" ]; then 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/JavaLang.astub b/src/units/JavaLang.astub index 055fe6d..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(); @@ -22,3 +25,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..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, @@ -14,23 +15,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 f94f770..4764ccc 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -13,14 +13,20 @@ import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.TypeUseLocation; +import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeFormatter; import org.checkerframework.framework.type.AnnotatedTypeMirror; 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; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; +import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; +import org.checkerframework.framework.type.typeannotator.TypeAnnotator; import org.checkerframework.framework.util.AnnotationFormatter; import org.checkerframework.framework.util.GraphQualifierHierarchy; import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; @@ -43,11 +49,6 @@ public UnitsAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker, true); unitsRepUtils = UnitsRepresentationUtils.getInstance(processingEnv, elements); postInit(); - - // add implicits for exceptions - addTypeNameImplicit(java.lang.Exception.class, unitsRepUtils.DIMENSIONLESS); - addTypeNameImplicit(java.lang.Throwable.class, unitsRepUtils.DIMENSIONLESS); - addTypeNameImplicit(java.lang.Void.class, unitsRepUtils.BOTTOM); } @Override @@ -56,15 +57,19 @@ protected AnnotationClassLoader createAnnotationClassLoader() { return new UnitsAnnotationClassLoader(checker); } + @Override + protected ViewpointAdapter createViewpointAdapter() { + return new UnitsViewpointAdapter(this); + } + @Override protected Set> createSupportedTypeQualifiers() { // get all the loaded annotations Set> qualSet = new HashSet>(); - qualSet.addAll(getBundledTypeQualifiersWithPolyAll()); + qualSet.addAll(getBundledTypeQualifiers()); // // load all the external units // loadAllExternalUnits(); - // // // copy all loaded external Units to qual set // qualSet.addAll(externalQualsMap.values()); @@ -122,7 +127,7 @@ public boolean isSupportedQualifier(AnnotationMirror anno) { if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) { return unitsRepUtils.hasAllBaseUnits(anno); } - // Anno is PolyAll, PolyUnit + // Anno is PolyUnit return AnnotationUtils.containsSame(this.getQualifierHierarchy().getTypeQualifiers(), anno); } @@ -146,28 +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); @@ -226,19 +209,6 @@ protected void finish( } } - // Set direct supertypes of PolyAll - // replace raw @UnitsRep with UnitsTop in super of PolyAll - for (Entry> e : supertypesMap.entrySet()) { - if (AnnotationUtils.areSame(e.getKey(), unitsRepUtils.POLYALL)) { - Set polyAllSupers = AnnotationUtils.createAnnotationSet(); - polyAllSupers.addAll(e.getValue()); - polyAllSupers.add(unitsRepUtils.TOP); - polyAllSupers.remove(unitsRepUtils.RAWUNITSREP); - supertypesMap.put(e.getKey(), polyAllSupers); - break; - } - } - // Set direct supertypes of PolyUnit // replace raw @UnitsRep with UnitsTop in super of PolyUnit for (Entry> e : supertypesMap.entrySet()) { @@ -275,6 +245,7 @@ protected void finish( // Update tops tops.remove(unitsRepUtils.RAWUNITSREP); + tops.remove(unitsRepUtils.RECEIVER_DEPENDANT_UNIT); tops.add(unitsRepUtils.TOP); // System.err.println(" === Typecheck ATF "); @@ -312,13 +283,19 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { return true; } - // Case: @PolyAll and @PolyUnit are treated as @UnknownUnits - if (AnnotationUtils.areSame(subAnno, unitsRepUtils.POLYALL) - || AnnotationUtils.areSame(subAnno, unitsRepUtils.POLYUNIT)) { + // Case: @PolyUnit are treated as @UnknownUnits + if (AnnotationUtils.areSame(subAnno, unitsRepUtils.POLYUNIT)) { return isSubtype(unitsRepUtils.TOP, superAnno); } - if (AnnotationUtils.areSame(superAnno, unitsRepUtils.POLYALL) - || AnnotationUtils.areSame(superAnno, unitsRepUtils.POLYUNIT)) { + if (AnnotationUtils.areSame(superAnno, unitsRepUtils.POLYUNIT)) { + return true; + } + + // Case: @RDU shouldn't appear. throw error? + if (AnnotationUtils.areSame(subAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return isSubtype(unitsRepUtils.TOP, superAnno); + } + if (AnnotationUtils.areSame(superAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { return true; } @@ -350,13 +327,18 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { @Override public TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( - new UnitsTypecheckImplicitsTreeAnnotator(), new UnitsPropagationTreeAnnotator()); + new UnitsLiteralTreeAnnotator(this), new UnitsPropagationTreeAnnotator()); } - protected final class UnitsTypecheckImplicitsTreeAnnotator extends UnitsImplicitsTreeAnnotator { + protected final class UnitsLiteralTreeAnnotator extends LiteralTreeAnnotator { // Programmatically set the qualifier implicits - public UnitsTypecheckImplicitsTreeAnnotator() { - 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); @@ -434,6 +416,24 @@ public Void visitBinary(BinaryTree binaryTree, AnnotatedTypeMirror type) { } } + @Override + protected TypeAnnotator createTypeAnnotator() { + return new ListTypeAnnotator( + new UnitsDefaultForTypeAnnotator(this), super.createTypeAnnotator()); + } + + protected class UnitsDefaultForTypeAnnotator extends DefaultForTypeAnnotator { + // Programmatically set the qualifier + public UnitsDefaultForTypeAnnotator(AnnotatedTypeFactory atf) { + super(atf); + + // add defaults for exceptions + addTypes(java.lang.Exception.class, unitsRepUtils.DIMENSIONLESS); + addTypes(java.lang.Throwable.class, unitsRepUtils.DIMENSIONLESS); + addTypes(java.lang.Void.class, unitsRepUtils.BOTTOM); + } + } + // for use in AnnotatedTypeMirror.toString() @Override protected AnnotatedTypeFormatter createAnnotatedTypeFormatter() { diff --git a/src/units/UnitsChecker.java b/src/units/UnitsChecker.java index 7d2e1d7..44b2c2e 100644 --- a/src/units/UnitsChecker.java +++ b/src/units/UnitsChecker.java @@ -19,8 +19,10 @@ "JavaMathTrig.astub", "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/UnitsImplicitsTreeAnnotator.java b/src/units/UnitsImplicitsTreeAnnotator.java deleted file mode 100644 index c09524c..0000000 --- a/src/units/UnitsImplicitsTreeAnnotator.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.ImplicitsTreeAnnotator; -import units.representation.UnitsRepresentationUtils; - -/** Common base class for ImplicitsTreeAnnotator. */ -public abstract class UnitsImplicitsTreeAnnotator extends ImplicitsTreeAnnotator { - - UnitsRepresentationUtils unitsRepUtils = UnitsRepresentationUtils.getInstance(); - - // Programmatically set the qualifier implicits - public UnitsImplicitsTreeAnnotator(AnnotatedTypeFactory atf) { - super(atf); - - // set BOTTOM as the implicit 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 implicit qualifier for lower bounds? Its nice to - // infer a bound which is the current mode. - } -} diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index b652d17..af531cc 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,18 @@ import checkers.inference.model.ConstraintManager; 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; +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; @@ -40,7 +45,9 @@ 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.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; @@ -89,6 +96,11 @@ protected AnnotationClassLoader createAnnotationClassLoader() { return new UnitsAnnotationClassLoader(checker); } + @Override + protected InferenceViewpointAdapter createViewpointAdapter() { + return new UnitsInferenceViewpointAdapter(this); + } + // In Inference ATF, this returns the set of real qualifiers @Override protected Set> createSupportedTypeQualifiers() { @@ -212,6 +224,71 @@ 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; + } + + if (annos1.isEmpty() || annos2.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); + } + } + } + + return result; + } + + // @Override + // public boolean isSubtype(AnnotationMirror subtype, AnnotationMirror supertype) { + // if (!isVarAnnot(subtype) && !isVarAnnot(supertype)) { + // // Case: All units <: Top + // if (AnnotationUtils.areSame(supertype, unitsRepUtils.TOP)) { + // return true; + // } + // // Case: Bottom <: All units + // if (AnnotationUtils.areSame(subtype, unitsRepUtils.BOTTOM)) { + // return true; + // } + // + // // Case: @UnitsRep(x) <: @UnitsRep(y) + // if (AnnotationUtils.areSameByClass(subtype, UnitsRep.class) + // && AnnotationUtils.areSameByClass(supertype, UnitsRep.class)) { + // return UnitsTypecheckUtils.unitsEqual(subtype, supertype); + // } + // } + // + // return super.isSubtype(subtype, supertype); + // } + } + + @Override + protected Set getDefaultTypeDeclarationBounds() { + Set top = new HashSet<>(); + top.add(unitsRepUtils.TOP); + return top; } @Override @@ -300,21 +377,10 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { @Override public TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( - new UnitsInferenceImplicitsTreeAnnotator(), new UnitsInferenceTreeAnnotator( this, realChecker, realTypeFactory, variableAnnotator, slotManager)); } - protected final class UnitsInferenceImplicitsTreeAnnotator extends UnitsImplicitsTreeAnnotator { - // Programmatically set the qualifier implicits - public UnitsInferenceImplicitsTreeAnnotator() { - 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 - } - } - private final class UnitsInferenceTreeAnnotator extends InferenceTreeAnnotator { // TODO: per design of InferenceTreeAnnotator, this code should be moved into // UnitsVariableAnnotator if it performs deep traversal @@ -388,10 +454,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 +585,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 +602,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/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java new file mode 100644 index 0000000..fb1934f --- /dev/null +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -0,0 +1,45 @@ +package units; + +import checkers.inference.InferenceMain; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.Slot; +import checkers.inference.util.InferenceViewpointAdapter; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; +import units.representation.UnitsRepresentationUtils; + +public class UnitsInferenceViewpointAdapter extends InferenceViewpointAdapter { + + // static reference to the singleton instance + protected static UnitsRepresentationUtils unitsRepUtils; + + public UnitsInferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + unitsRepUtils = UnitsRepresentationUtils.getInstance(); + } + + @Override + protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { + return false; + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + if (InferenceMain.isHackMode(declaredAnnotation == null)) { + return unitsRepUtils.BOTTOM; + } + Slot declSlot = InferenceMain.getInstance().getSlotManager().getSlot(declaredAnnotation); + if (declSlot.isConstant()) { + ConstantSlot cs = (ConstantSlot) declSlot; + if (AnnotationUtils.areSame(cs.getValue(), unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return super.combineAnnotationWithAnnotation( + receiverAnnotation, declaredAnnotation); + } + } + return declaredAnnotation; + } +} diff --git a/src/units/UnitsViewpointAdapter.java b/src/units/UnitsViewpointAdapter.java new file mode 100644 index 0000000..dc9076b --- /dev/null +++ b/src/units/UnitsViewpointAdapter.java @@ -0,0 +1,39 @@ +package units; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; +import units.representation.UnitsRepresentationUtils; + +public class UnitsViewpointAdapter extends AbstractViewpointAdapter { + + // static reference to the singleton instance + protected static UnitsRepresentationUtils unitsRepUtils; + + public UnitsViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + unitsRepUtils = UnitsRepresentationUtils.getInstance(); + } + + @Override + protected boolean shouldAdaptMember(AnnotatedTypeMirror type, Element element) { + return false; + } + + @Override + protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { + return atm.getAnnotationInHierarchy(unitsRepUtils.TOP); + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation( + AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { + if (AnnotationUtils.areSame(declaredAnnotation, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return receiverAnnotation; + } + return declaredAnnotation; + } +} diff --git a/src/units/qual/RDU.java b/src/units/qual/RDU.java new file mode 100644 index 0000000..6be2671 --- /dev/null +++ b/src/units/qual/RDU.java @@ -0,0 +1,19 @@ +package units.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; + +/** + * UnitReceiverDependant is the top type of the type hierarchy. + * + * @checker_framework.manual #units-checker Units Checker + */ +@Documented +@SubtypeOf(UnitsRep.class) +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) // ElementType.TYPE, +public @interface RDU {} diff --git a/src/units/representation/TypecheckUnit.java b/src/units/representation/TypecheckUnit.java index db35df7..6a45a05 100644 --- a/src/units/representation/TypecheckUnit.java +++ b/src/units/representation/TypecheckUnit.java @@ -11,6 +11,7 @@ public class TypecheckUnit { private boolean uu; private boolean ub; + private boolean rdu; private int prefixExponent; // Tree map maintaining sorted order on base unit names private final Map exponents; @@ -20,6 +21,8 @@ public TypecheckUnit() { uu = false; // default UU value is false ub = false; + // default RDU value is false + rdu = false; // default prefixExponent is 0 prefixExponent = 0; // default exponents are 0 @@ -35,6 +38,15 @@ public boolean isUnknownUnits() { return uu; } + public void setRDUnits(boolean val) { + rdu = val; + assert !(uu && ub); + } + + public boolean isRDUnits() { + return rdu; + } + public void setUnitsBottom(boolean val) { ub = val; assert !(uu && ub); diff --git a/src/units/representation/UnitsRepresentationUtils.java b/src/units/representation/UnitsRepresentationUtils.java index 15bdc33..a85e4f1 100644 --- a/src/units/representation/UnitsRepresentationUtils.java +++ b/src/units/representation/UnitsRepresentationUtils.java @@ -19,7 +19,6 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.util.Elements; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.framework.qual.PolyAll; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; @@ -27,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; @@ -43,9 +43,6 @@ public class UnitsRepresentationUtils { private static ProcessingEnvironment processingEnv; private static Elements elements; - /** An instance of {@link PolyAll} as an {@link AnnotationMirror} */ - public AnnotationMirror POLYALL; - /** An instance of {@link PolyUnit} as an {@link AnnotationMirror} */ public AnnotationMirror POLYUNIT; @@ -68,6 +65,8 @@ public class UnitsRepresentationUtils { public AnnotationMirror SURFACE_BOTTOM; + public AnnotationMirror RECEIVER_DEPENDANT_UNIT; + // /** Instance of {@link VarAnnot} for use in UnitsVisitor in infer mode. */ // public AnnotationMirror VARANNOT; @@ -212,8 +211,8 @@ protected Map createZeroFilledBaseUnitsMap() { // postInit() is called after performing annotation loading to obtain the full list of base // units public void postInit() { - POLYALL = AnnotationBuilder.fromClass(elements, PolyAll.class); POLYUNIT = AnnotationBuilder.fromClass(elements, PolyUnit.class); + RECEIVER_DEPENDANT_UNIT = AnnotationBuilder.fromClass(elements, RDU.class); RAWUNITSREP = AnnotationBuilder.fromClass(elements, UnitsRep.class); @@ -497,9 +496,10 @@ public TypecheckUnit createTypecheckUnit(AnnotationMirror anno) { TypecheckUnit unit = new TypecheckUnit(); // if it is a polyunit annotation, generate top - if (AnnotationUtils.areSameByClass(anno, PolyUnit.class) - || AnnotationUtils.areSameByClass(anno, PolyAll.class)) { + if (AnnotationUtils.areSameByClass(anno, PolyUnit.class)) { unit.setUnknownUnits(true); + } else if (AnnotationUtils.areSameByClass(anno, RDU.class)) { + unit.setRDUnits(true); } // if it is a units internal annotation, generate the internal unit else if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) { @@ -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/gje/UnitsGJEFormatTranslator.java b/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java index 6b82e68..27ce4a6 100644 --- a/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java +++ b/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java @@ -98,8 +98,7 @@ protected GJEInferenceUnit serializeConstantSlot(ConstantSlot slot) { // Temp Hack: forcefully encode constant slot for poly qualifiers as // unknownunits - if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT) - || AnnotationUtils.areSame(anno, unitsRepUtils.POLYALL)) { + if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { anno = unitsRepUtils.TOP; } diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index d0c3245..292e443 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())); @@ -115,8 +116,7 @@ protected Z3InferenceUnit serializeConstantSlot(ConstantSlot slot) { // Temp Hack: forcefully encode constant slot for poly qualifiers as // unknownunits - if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT) - || AnnotationUtils.areSame(anno, unitsRepUtils.POLYALL)) { + if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { anno = unitsRepUtils.TOP; } @@ -139,6 +139,8 @@ protected Z3InferenceUnit serializeConstantSlot(ConstantSlot slot) { encodedSlot.setUnknownUnits(true); } else if (unit.isUnitsBottom()) { encodedSlot.setUnitsBottom(true); + } else if (unit.isRDUnits()) { + encodedSlot.setRDUnits(true); } else { encodedSlot.setPrefixExponent(unit.getPrefixExponent()); for (String bu : unitsRepUtils.serializableBaseUnits()) { @@ -167,17 +169,18 @@ 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(); - // encode PolyAll and PolyUnit as constant trues - if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYALL) - || AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { + // encode PolyUnit as constant trues + if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { return ctx.mkTrue(); } + if (AnnotationUtils.areSame(anno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { + return serializedSlot.getRDUnits(); + } } - - Z3InferenceUnit serializedSlot = slot.serialize(this); return UnitsZ3SmtEncoderUtils.slotWellformedness(ctx, serializedSlot); } @@ -186,9 +189,8 @@ public BoolExpr encodeSlotPreferenceConstraint(VariableSlot slot) { if (slot instanceof ConstantSlot) { ConstantSlot cs = (ConstantSlot) slot; AnnotationMirror anno = cs.getValue(); - // encode PolyAll and PolyUnit as constant trues - if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYALL) - || AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { + // encode PolyUnit as constant trues + if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { return ctx.mkTrue(); } } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java new file mode 100644 index 0000000..c578096 --- /dev/null +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java @@ -0,0 +1,63 @@ +package units.solvers.backend.z3smt.encoder; + +import backend.z3smt.Z3SmtFormatTranslator; +import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.VariableSlot; +import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; +import checkers.inference.solver.frontend.Lattice; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import units.representation.TypecheckUnit; +import units.solvers.backend.z3smt.representation.Z3InferenceUnit; + +public class UnitsZ3SmtCombineConstraintEncoder + extends Z3SmtAbstractConstraintEncoder + implements CombineConstraintEncoder { + + public UnitsZ3SmtCombineConstraintEncoder( + Lattice lattice, + Context ctx, + Z3SmtFormatTranslator z3SmtFormatTranslator) { + super(lattice, ctx, z3SmtFormatTranslator); + } + + private BoolExpr receiver_dependent( + VariableSlot target, VariableSlot declared, VariableSlot result) { + Z3InferenceUnit tar = target.serialize(z3SmtFormatTranslator); + Z3InferenceUnit decl = declared.serialize(z3SmtFormatTranslator); + Z3InferenceUnit res = result.serialize(z3SmtFormatTranslator); + + return ctx.mkAnd( + ctx.mkImplies(decl.getRDUnits(), UnitsZ3SmtEncoderUtils.equality(ctx, tar, res)), + ctx.mkImplies( + ctx.mkNot(decl.getRDUnits()), + UnitsZ3SmtEncoderUtils.equality(ctx, decl, res))); + } + + @Override + public BoolExpr encodeVariable_Variable( + VariableSlot target, VariableSlot declared, VariableSlot result) { + return ctx.mkTrue(); + // return receiver_dependent(target, declared, result); + } + + @Override + public BoolExpr encodeVariable_Constant( + VariableSlot target, ConstantSlot declared, VariableSlot result) { + return receiver_dependent(target, declared, result); + } + + @Override + public BoolExpr encodeConstant_Variable( + ConstantSlot target, VariableSlot declared, VariableSlot result) { + return ctx.mkTrue(); + // return receiver_dependent(target, declared, result); + } + + @Override + public BoolExpr encodeConstant_Constant( + ConstantSlot target, ConstantSlot declared, VariableSlot result) { + return receiver_dependent(target, declared, result); + } +} diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java index 83b8acc..2056456 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java @@ -63,7 +63,7 @@ public ExistentialConstraintEncoder createExistentialConstraintEncoder @Override public CombineConstraintEncoder createCombineConstraintEncoder() { - return null; + return new UnitsZ3SmtCombineConstraintEncoder(lattice, ctx, formatTranslator); } @Override diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java index 7465a71..c044504 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java @@ -91,11 +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 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) @@ -127,6 +131,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); @@ -141,6 +146,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 c5890d0..633c1a9 100644 --- a/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java +++ b/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java @@ -20,6 +20,7 @@ public class Z3InferenceUnit { private BoolExpr uu; private BoolExpr ub; private IntExpr prefixExponent; + private BoolExpr rdu; // Tree map maintaining sorted order on base unit names private final Map exponents; @@ -40,6 +41,8 @@ public static Z3InferenceUnit makeConstantSlot(Context ctx, int slotID) { slot.uu = ctx.mkBool(false); // default UU value is false slot.ub = ctx.mkBool(false); + // default RDU value is false; + slot.rdu = ctx.mkBool(false); // default prefixExponent is 0 slot.prefixExponent = slot.intZero; @@ -62,6 +65,9 @@ public static Z3InferenceUnit makeVariableSlot(Context ctx, int slotID) { ctx.mkBoolConst( UnitsZ3SmtEncoderUtils.z3VarName( slotID, UnitsZ3SmtEncoderUtils.ubSlotName)); + + slot.rdu = ctx.mkBool(false); + slot.prefixExponent = ctx.mkIntConst( UnitsZ3SmtEncoderUtils.z3VarName( @@ -91,6 +97,14 @@ public BoolExpr getUnitsBottom() { return ub; } + public void setRDUnits(boolean val) { + rdu = ctx.mkBool(val); + } + + public BoolExpr getRDUnits() { + return rdu; + } + public void setPrefixExponent(int exp) { prefixExponent = ctx.mkInt(exp); } diff --git a/testing/inference/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 3ef7d74..928200d 100644 --- a/testing/inference/Constructors.java +++ b/testing/inference/Constructors.java @@ -1,15 +1,8 @@ -import org.checkerframework.framework.qual.PolyAll; import units.UnitsTools; import units.qual.*; -@UnknownUnits class PolyAllClass { - @PolyAll PolyAllClass(@PolyAll int x) {} - // @PolyAll PolyAllClass(@PolyAll PolyAllClass x) {} -} - class PolyUnitClass { @PolyUnit PolyUnitClass(@PolyUnit int x) {} - // @PolyUnit PolyUnitClass(@PolyUnit PolyUnitClass x) {} } class MeterClass { @@ -22,28 +15,6 @@ class NoAnnotClass { class Constructors { // TODO: return check isn't quite correct for inner declared classes - // class PolyAllClass { - // @PolyAll PolyAllClass(@PolyAll int x) {} - // } - - void polyAllConstructorTest() { - // propagate @m from assignment context - // :: fixable-error: (assignment.type.incompatible) - @m PolyAllClass pac1 = new PolyAllClass(5); - - // progagate @m from constructor arg - PolyAllClass pac2 = new PolyAllClass(5 * UnitsTools.m); - - // propagate @m from constructor return type - // :: fixable-error: (constructor.invocation.invalid) - PolyAllClass pac3 = new @m PolyAllClass(5); - - // :: fixable-error: (constructor.invocation.invalid) - @m PolyAllClass pac4 = new @m PolyAllClass(5); - - // :: fixable-error: (constructor.invocation.invalid) - PolyAllClass pac5 = new @m PolyAllClass(5 * UnitsTools.s); - } void polyUnitConstructorTest() { // propagate @m from assignment context @@ -54,44 +25,22 @@ 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: (argument.type.incompatible) :: fixable-error: - // (constructor.invocation.invalid) :: fixable-error: - // (assignment.type.incompatible) + // :: 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); } - - // if polymorphic var slots are inserted then this test fails as there are - // missing pairs of round brackets - // void chainPolyConstructorTest() { - // // propagate @m from assignment context - // // :: fixable-error: (assignment.type.incompatible) - // @m PolyAllClass pacc1 = new PolyAllClass(new PolyAllClass(5)); - // - // // progagate @m from constructor arg - // PolyAllClass pacc2 = new PolyAllClass(new PolyAllClass(5 * - // UnitsTools.m)); - // - // // propagate @m from constructor return type - // // :: fixable-error: (constructor.invocation.invalid) - // PolyAllClass pacc3 = new @m PolyAllClass(new PolyAllClass(5)); - // - // // propagate @m from constructor return type - // // :: fixable-error: (constructor.invocation.invalid) - // PolyAllClass pacc4 = new PolyAllClass(new @m PolyAllClass(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 c22aa5c..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); } @@ -28,4 +29,32 @@ void test2() { @ns long nanosec = ns.convert(10L, TimeUnit.DAYS); } + + void testParams() { + TimeUnit s_unit = TimeUnit.SECONDS; + TimeUnit ns_unit = NANOSECONDS; + + long ns = 1000; + long s = 1000; + + // :: fixable-error: (argument.type.incompatible) + TimeUnit.SECONDS.toMillis(s); + // :: fixable-error: (argument.type.incompatible) + TimeUnit.NANOSECONDS.toMillis(ns); + + // :: fixable-error: (argument.type.incompatible) + ns_unit.toMillis(ns); + // :: fixable-error: (argument.type.incompatible) + s_unit.toMillis(s); + } + + void testReturn(long s1, long s2) { + TimeUnit s = TimeUnit.SECONDS; + TimeUnit ms = TimeUnit.MILLISECONDS; + + // :: fixable-error: (assignment.type.incompatible) + s1 = s.convert(10L, NANOSECONDS); + // :: fixable-error: (assignment.type.incompatible) + s2 = TimeUnit.SECONDS.convert(10L, NANOSECONDS); + } } diff --git a/testing/inference/Methods.java b/testing/inference/Methods.java index 5e781b8..655a2cb 100644 --- a/testing/inference/Methods.java +++ b/testing/inference/Methods.java @@ -1,12 +1,7 @@ -import org.checkerframework.framework.qual.PolyAll; import units.UnitsTools; import units.qual.*; class Methods { - @PolyAll int polyAllMethod(@PolyAll int x) { - return x; - } - @PolyUnit int polyUnitMethod(@PolyUnit int x) { return x; } @@ -19,11 +14,13 @@ class Methods { return x; } - void polyAllMethodTest() { - // :: fixable-error: (assignment.type.incompatible) - @m int pam1 = polyAllMethod(5); + int method(int x) { + return x; + } - int pam2 = polyAllMethod(5 * UnitsTools.m); + void testMethod() { + // :: fixable-error: (assignment.type.incompatible) + @m int num = method(5); } void polyUnitMethodTest() { @@ -41,13 +38,6 @@ void normalMethodTest() { int nm1 = meterMethod(5); } - void chainPolyAllMethodTest() { - // :: fixable-error: (assignment.type.incompatible) - @m int cpam1 = polyAllMethod(polyAllMethod(5)); - - int cpam2 = polyAllMethod(polyAllMethod(5 * UnitsTools.m)); - } - void chainPolyUnitMethodTest() { // :: fixable-error: (assignment.type.incompatible) @m int cpum1 = polyUnitMethod(polyUnitMethod(5)); 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/inference/Variables.java b/testing/inference/Variables.java index 13b0cdf..899770e 100644 --- a/testing/inference/Variables.java +++ b/testing/inference/Variables.java @@ -48,8 +48,6 @@ void boxedConstructorCalls() { @m Integer explicitValueOfCall = Integer.valueOf(10); // :: fixable-error: (constructor.invocation.invalid) @m Integer omittingConstructorArgType = new @m Integer(10); - // :: fixable-error: (assignment.type.incompatible) - // :: fixable-error: (constructor.invocation.invalid) @m Integer omittingConstructorReturnType = new Integer(10 * UnitsTools.m); // :: fixable-error: (assignment.type.incompatible) @m Integer omittingConstructorArgAndReturnType = new Integer(10); @@ -61,7 +59,6 @@ void boxedMethodCalls() { } void customUnitForInsertion() { - // :: fixable-error: (assignment.type.incompatible) @UnitsRep( top = false, bot = false, @@ -70,6 +67,7 @@ void customUnitForInsertion() { @BUC(unit = "m", exponent = 12), @BUC(unit = "s", exponent = -34) }) + // :: fixable-error: (assignment.type.incompatible) Integer x = 50; } } diff --git a/testing/typecheck/Constructors.java b/testing/typecheck/Constructors.java index 11140c2..d8c4293 100644 --- a/testing/typecheck/Constructors.java +++ b/testing/typecheck/Constructors.java @@ -1,11 +1,6 @@ -import org.checkerframework.framework.qual.PolyAll; import units.UnitsTools; import units.qual.*; -@UnknownUnits class PolyAllClass { - @PolyAll PolyAllClass(@PolyAll int x) {} -} - class PolyUnitClass { @PolyUnit PolyUnitClass(@PolyUnit int x) {} } @@ -19,42 +14,24 @@ class NoAnnotClass { } class Constructors { - void polyAllConstructorTest() { - // :: error: (assignment.type.incompatible) - @m PolyAllClass pac1 = new PolyAllClass(5); - - PolyAllClass pac2 = new PolyAllClass(5 * UnitsTools.m); - - // :: error: (constructor.invocation.invalid) - PolyAllClass pac3 = new @m PolyAllClass(5); - - // :: error: (constructor.invocation.invalid) - @m PolyAllClass pac4 = new @m PolyAllClass(5); - - // :: error: (constructor.invocation.invalid) - PolyAllClass pac5 = new @m PolyAllClass(5 * UnitsTools.s); - } - void polyUnitConstructorTest() { // :: error: (assignment.type.incompatible) @m PolyUnitClass puc1 = new PolyUnitClass(5); 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); } void nonPolyConstructorTest() { // :: error: (argument.type.incompatible) - // :: error: (constructor.invocation.invalid) - // :: error: (assignment.type.incompatible) @m MeterClass mc1 = new MeterClass(5); // :: error: (argument.type.incompatible) @m MeterClass mc2 = new @m MeterClass(5); diff --git a/testing/typecheck/JavaUtilConcurrentTimeUnit.java b/testing/typecheck/JavaUtilConcurrentTimeUnit.java index d548579..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); } @@ -36,10 +37,14 @@ void test2() { // :: error: (assignment.type.incompatible) ms = ns; - // ensure the poly convert works + // ensure RDU convert works @s long seconds = s.convert(10L, NANOSECONDS); + // :: error: (assignment.type.incompatible) + @s long not_seconds = ms.convert(10L, NANOSECONDS); @s long secondsTwo = TimeUnit.SECONDS.convert(10L, NANOSECONDS); + // :: error: (assignment.type.incompatible) + @s long not_secondsTwo = TimeUnit.MILLISECONDS.convert(10L, NANOSECONDS); // convert 10 minutes to milliseconds @ms long milliseconds = TimeUnit.MILLISECONDS.convert(10L, TimeUnit.MINUTES); @@ -59,4 +64,23 @@ void bad() { // :: error: (assignment.type.incompatible) @s TimeUnit s4 = NANOSECONDS; } + + void testParams(@ns long ns, @s long s) { + @s TimeUnit s_unit = TimeUnit.SECONDS; + @ns TimeUnit ns_unit = NANOSECONDS; + + TimeUnit.SECONDS.toMillis(s); + TimeUnit.NANOSECONDS.toMillis(ns); + // :: error: (argument.type.incompatible) + TimeUnit.NANOSECONDS.toMillis(s); + // :: error: (argument.type.incompatible) + TimeUnit.SECONDS.toMillis(ns); + + ns_unit.toMillis(ns); + s_unit.toMillis(s); + // :: error: (argument.type.incompatible) + s_unit.toMillis(ns); + // :: error: (argument.type.incompatible) + ns_unit.toMillis(s); + } } diff --git a/testing/typecheck/Methods.java b/testing/typecheck/Methods.java index 3a0524d..363bd49 100644 --- a/testing/typecheck/Methods.java +++ b/testing/typecheck/Methods.java @@ -1,12 +1,7 @@ -import org.checkerframework.framework.qual.PolyAll; import units.UnitsTools; import units.qual.*; class Methods { - @PolyAll int polyAllMethod(@PolyAll int x) { - return x; - } - @PolyUnit int polyUnitMethod(@PolyUnit int x) { return x; } @@ -19,13 +14,6 @@ class Methods { return x; } - void polyAllMethodTest() { - // :: error: (assignment.type.incompatible) - @m int pam1 = polyAllMethod(5); - - int pam2 = polyAllMethod(5 * UnitsTools.m); - } - void polyUnitMethodTest() { // :: error: (assignment.type.incompatible) @m int pum1 = polyUnitMethod(5); @@ -35,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); @@ -46,13 +34,6 @@ void normalMethodTest() { int nm1 = meterMethod(5); } - void chainPolyAllMethodTest() { - // :: error: (assignment.type.incompatible) - @m int cpam1 = polyAllMethod(polyAllMethod(5)); - - int cpam2 = polyAllMethod(polyAllMethod(5 * UnitsTools.m)); - } - void chainPolyUnitMethodTest() { // :: error: (assignment.type.incompatible) @m int cpum1 = polyUnitMethod(polyUnitMethod(5)); diff --git a/testing/typecheck/RDUMethodReceiver.java b/testing/typecheck/RDUMethodReceiver.java new file mode 100644 index 0000000..2d29c90 --- /dev/null +++ b/testing/typecheck/RDUMethodReceiver.java @@ -0,0 +1,46 @@ +import units.qual.*; + +public class RDUMethodReceiver { + + @m public class MeterClass { + @RDU + Object get(@m MeterClass this) { + return null; + } + + Object set(@m MeterClass 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() { + 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); + } +} 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); + } +} diff --git a/testing/typecheck/Subtyping.java b/testing/typecheck/Subtyping.java index 06d9925..d59a234 100644 --- a/testing/typecheck/Subtyping.java +++ b/testing/typecheck/Subtyping.java @@ -1,4 +1,3 @@ -import org.checkerframework.framework.qual.PolyAll; import units.qual.*; class Subtyping { @@ -41,22 +40,4 @@ void test() { m = m; s = s; } - - @PolyAll Integer polyall; - @PolyUnit Integer polyunit; - @UnitsRep Integer raw; - - void oddCases() { - // For directly testing the subtyping relations defined between poly and unit types - // these are not expected to be in source code - polyall = raw; - raw = polyall; - polyunit = raw; - raw = polyunit; - - polyall = polyunit; - polyunit = polyall; - polyall = m; - m = polyall; - } }