Move CI to github action

.github/workflows/main.yml

@@ -0,0 +1,39 @@
+name: CI
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+  workflow_dispatch:
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        jdk: [ 8, 11 ]
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Set up JDK
+        uses: actions/setup-java@v1
+        with:
+          java-version: ${{matrix.jdk}}
+      - name: Set up Python 3
+        uses: actions/setup-python@v2
+        with:
+          python-version: 3.8
+      - name: Install Python dependencies
+        run: |
+          python -m pip install --upgrade pip
+          pip install --user  -r ./.travis-requirements.txt
+      - name: Github Environment Setup
+        run: |
+          owner=${{ github.repository_owner }}
+          echo "REPO_SITE=${owner}" >> $GITHUB_ENV
+      - name: Units Inference Dependency Setup & Build
+        run: ./dependency-setup.sh
+      - name: Units Inference Tests
+        run: ./test-units.sh

build.gradle

@@ -90,12 +90,17 @@ afterEvaluate {
         group 'Verification'
 
         systemProperties 'path.afu.scripts': "${afu}/scripts",
-                'path.inference.script': "${cfi}/scripts/inference",
-                JDK_JAR: "${cf}/checker/dist/jdk8.jar"
+                'path.inference.script': "${cfi}/scripts/inference"
+
+        if (JavaVersion.current() == JavaVersion.VERSION_1_8) {
+            systemProperties += [JDK_JAR: "${cf}/checker/dist/jdk8.jar"]
+        }
 
         environment "external_checker_classpath", "${units}/build/classes/java/main:${units}/build/resources/main"
 
-        jvmArgs "-Xbootclasspath/p:${cfi}/dist/javac.jar"
+        if (JavaVersion.current() == JavaVersion.VERSION_1_8) {
+            jvmArgs "-Xbootclasspath/p:${cfi}/dist/javac.jar"
+        }
 
         testLogging {
             // Always run the tests
@@ -179,7 +184,7 @@ task getCodeFormatScripts() {
 
 task pythonIsInstalled(type: Exec) {
   description "Check that the python executable is installed."
-  executable = "python"
+  executable = "python3"
   args "--version"
 }
 
@@ -221,7 +226,7 @@ List<String> getJavaFilesToFormat() {
 
 task checkFormat(type: Exec, dependsOn: [getCodeFormatScripts, pythonIsInstalled], group: 'Format') {
     description 'Check whether the source code is properly formatted'
-    executable 'python'
+    executable 'python3'
     doFirst {
         args += "${formatScripts}/check-google-java-format.py"
         args += "--aosp" // 4 space indentation
@@ -238,12 +243,17 @@ task checkFormat(type: Exec, dependsOn: [getCodeFormatScripts, pythonIsInstalled
 task reformat(type: Exec, dependsOn: [getCodeFormatScripts, pythonIsInstalled], group: 'Format') {
     description 'Format the Java source code'
     // jdk8 and checker-qual have no source, so skip
-    executable 'python'
+    executable 'python3'
     doFirst {
         args += "${formatScripts}/run-google-java-format.py"
         args += "--aosp" // 4 space indentation
         args += getJavaFilesToFormat()
     }
 }
 
-tasks.test.dependsOn 'checkFormat'
+//tasks.test.dependsOn 'checkFormat'
+tasks.test {
+    if (JavaVersion.current() == JavaVersion.VERSION_11) {
+        dependsOn 'checkFormat'
+    }
+}

dependency-setup.sh

@@ -33,7 +33,7 @@ else
 fi
 
 ## Build checker-framework-inference
-(cd $JSR308/checker-framework-inference && ./.travis-build-without-test.sh)
+(cd $JSR308/checker-framework-inference && ./.ci-build-without-test.sh)
 
 ## Build units-inference without testing
 (cd $JSR308/units-inference && ./gradlew build -x test)

src/backend/z3smt/Z3SmtFormatTranslator.java

@@ -1,11 +1,13 @@
 package backend.z3smt;
 
+import checkers.inference.model.ArithmeticVariableSlot;
 import checkers.inference.model.CombVariableSlot;
 import checkers.inference.model.ConstantSlot;
 import checkers.inference.model.ExistentialVariableSlot;
 import checkers.inference.model.LubVariableSlot;
 import checkers.inference.model.RefinementVariableSlot;
 import checkers.inference.model.Slot;
+import checkers.inference.model.SourceVariableSlot;
 import checkers.inference.model.VariableSlot;
 import checkers.inference.solver.backend.AbstractFormatTranslator;
 import checkers.inference.solver.frontend.Lattice;
@@ -40,13 +42,13 @@ public final void init(Context ctx) {
         finishInitializingEncoders();
     }
 
-    protected abstract SlotEncodingT serializeVarSlot(VariableSlot slot);
+    protected abstract SlotEncodingT serializeVariableSlot(VariableSlot slot);
 
     protected abstract SlotEncodingT serializeConstantSlot(ConstantSlot slot);
 
     @Override
-    public SlotEncodingT serialize(VariableSlot slot) {
-        return serializeVarSlot(slot);
+    public SlotEncodingT serialize(SourceVariableSlot slot) {
+        return serializeVariableSlot(slot);
     }
 
     @Override
@@ -56,22 +58,27 @@ public SlotEncodingT serialize(ConstantSlot slot) {
 
     @Override
     public SlotEncodingT serialize(ExistentialVariableSlot slot) {
-        return serializeVarSlot(slot);
+        return serializeVariableSlot(slot);
     }
 
     @Override
     public SlotEncodingT serialize(RefinementVariableSlot slot) {
-        return serializeVarSlot(slot);
+        return serializeVariableSlot(slot);
     }
 
     @Override
     public SlotEncodingT serialize(CombVariableSlot slot) {
-        return serializeVarSlot(slot);
+        return serializeVariableSlot(slot);
     }
 
     @Override
     public SlotEncodingT serialize(LubVariableSlot slot) {
-        return serializeVarSlot(slot);
+        return serializeVariableSlot(slot);
+    }
+
+    @Override
+    public SlotEncodingT serialize(ArithmeticVariableSlot slot) {
+        return serializeVariableSlot(slot);
     }
 
     /**

src/backend/z3smt/Z3SmtSolver.java

@@ -345,7 +345,7 @@ protected void encodeAllSlots() {
 
         // generate slot constraints
         for (Slot slot : slots) {
-            if (slot.isVariable()) {
+            if (slot instanceof VariableSlot) {
                 VariableSlot varSlot = (VariableSlot) slot;
 
                 BoolExpr wfConstraint = formatTranslator.encodeSlotWellformnessConstraint(varSlot);

src/units/UnitsAnnotatedTypeFactory.java

@@ -1,9 +1,10 @@
 package units;
 
+import checkers.inference.BaseInferenceRealTypeFactory;
+
 import com.sun.source.tree.BinaryTree;
 import com.sun.source.tree.Tree.Kind;
 
-import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.qual.LiteralKind;
 import org.checkerframework.framework.qual.TypeUseLocation;
@@ -23,9 +24,11 @@
 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;
 import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory;
 import org.checkerframework.framework.util.defaults.QualifierDefaults;
 import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.UserError;
 
@@ -48,12 +51,12 @@
 
 import javax.lang.model.element.AnnotationMirror;
 
-public class UnitsAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+public class UnitsAnnotatedTypeFactory extends BaseInferenceRealTypeFactory {
     // static reference to the singleton instance
     protected static UnitsRepresentationUtils unitsRepUtils;
 
-    public UnitsAnnotatedTypeFactory(BaseTypeChecker checker) {
-        super(checker, true);
+    public UnitsAnnotatedTypeFactory(BaseTypeChecker checker, boolean isInfer) {
+        super(checker, isInfer);
         unitsRepUtils = UnitsRepresentationUtils.getInstance(processingEnv, elements);
         postInit();
     }
@@ -93,7 +96,7 @@ public AnnotationMirror canonicalAnnotation(AnnotationMirror anno) {
         // check to see if it is an internal units annotation
         if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) {
             // fill in missing base units
-            return anno; // unitsRepUtils.fillMissingBaseUnits(anno);
+            return unitsRepUtils.fillMissingBaseUnits(anno);
         }
 
         // check to see if it's a surface annotation such as @m or @UnknownUnits
@@ -128,7 +131,7 @@ public boolean isSupportedQualifier(AnnotationMirror anno) {
             return false;
         }
         if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) {
-            return true;
+            return unitsRepUtils.hasAllBaseUnits(anno);
         }
         if (AnnotationUtils.areSameByClass(anno, PolyUnit.class)) {
             return true;
@@ -161,7 +164,13 @@ protected void addCheckedCodeDefaults(QualifierDefaults defs) {
     }
 
     @Override
-    public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) {
+    public QualifierHierarchy createQualifierHierarchy() {
+        return MultiGraphQualifierHierarchy.createMultiGraphQualifierHierarchy(this);
+    }
+
+    @Override
+    public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory(
+            MultiGraphFactory factory) {
         return new UnitsQualifierHierarchy(factory);
     }
 
@@ -272,6 +281,22 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) {
                 return true;
             }
 
+            // 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)) {
@@ -289,7 +314,12 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) {
                 // return result;
             }
 
-            return true;
+            throw new BugInCF(
+                    "Uncaught subtype check case:"
+                            + "\n    subtype:   "
+                            + getAnnotationFormatter().formatAnnotationMirror(subAnno)
+                            + "\n    supertype: "
+                            + getAnnotationFormatter().formatAnnotationMirror(superAnno));
         }
     }
 

src/units/UnitsChecker.java

@@ -52,8 +52,8 @@ public UnitsVisitor createVisitor(
     }
 
     @Override
-    public UnitsAnnotatedTypeFactory createRealTypeFactory() {
-        return new UnitsAnnotatedTypeFactory(this);
+    public UnitsAnnotatedTypeFactory createRealTypeFactory(boolean infer) {
+        return new UnitsAnnotatedTypeFactory(this, infer);
     }
 
     @Override