Rdu

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

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

@@ -19,7 +19,9 @@
 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;
@@ -55,6 +57,11 @@ 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
@@ -63,7 +70,6 @@ protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
 
         // // load all the external units
         // loadAllExternalUnits();
-        //
         // // copy all loaded external Units to qual set
         // qualSet.addAll(externalQualsMap.values());
 
@@ -121,7 +127,7 @@ public boolean isSupportedQualifier(AnnotationMirror anno) {
         if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) {
             return unitsRepUtils.hasAllBaseUnits(anno);
         }
-        // Anno is PolyAll, PolyUnit
+        // Anno is PolyUnit
         return AnnotationUtils.containsSame(this.getQualifierHierarchy().getTypeQualifiers(), anno);
     }
 
@@ -145,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);
@@ -261,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 ");
@@ -298,14 +283,22 @@ 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 shouldn't appear. throw error?
+            if (AnnotationUtils.areSame(subAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) {
+                return isSubtype(unitsRepUtils.TOP, superAnno);
+            }
+            if (AnnotationUtils.areSame(superAnno, unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) {
+                return true;
+            }
+
             // Case: @UnitsRep(x) <: @UnitsRep(y)
             if (AnnotationUtils.areSameByClass(subAnno, UnitsRep.class)
                     && AnnotationUtils.areSameByClass(superAnno, UnitsRep.class)) {
@@ -334,13 +327,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);

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 {