Added a receiver dependent qualifier

.classpath

@@ -4,8 +4,9 @@
 	<classpathentry kind="src" output="build/classes/java/test" path="tests"/>
 	<classpathentry kind="src" path="/checker"/>
 	<classpathentry kind="src" path="/checker-framework-inference"/>
-    <classpathentry kind="lib" path="/checker-framework-inference/lib/com.microsoft.z3.jar"/>
+	<classpathentry kind="lib" path="/checker-framework-inference/lib/com.microsoft.z3.jar"/>
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8/"/>
 	<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
+	<classpathentry kind="lib" path="/checker-framework-inference/dist/checker-framework-inference.jar"/>
 	<classpathentry kind="output" path="build/classes/java"/>
 </classpath>

.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*

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:

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

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

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

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);
+}
+

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);
+}

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<String>, 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);
+}
+

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);
+}

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);

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<Class<? extends Annotation>> createSupportedTypeQualifiers() {
         // get all the loaded annotations
         Set<Class<? extends Annotation>> qualSet = new HashSet<Class<? extends Annotation>>();
-        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<AnnotationMirror, Set<AnnotationMirror>> e : supertypesMap.entrySet()) {
-                if (AnnotationUtils.areSame(e.getKey(), unitsRepUtils.POLYALL)) {
-                    Set<AnnotationMirror> 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<AnnotationMirror, Set<AnnotationMirror>> 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() {

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 {