Adaptations to work upon opprop CF&CFI

.travis.yml

@@ -1,9 +1,10 @@
 language: java
+python: 3.6
 dist: trusty
 jdk:
   - oraclejdk8
 
 install:
-  - pip install --user  -r ./.travis-requirements.txt
+  - pip3 install --user  -r ./.travis-requirements.txt
 
 script: ./.travis-build.sh

build.gradle

@@ -91,12 +91,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
@@ -180,7 +185,7 @@ task getCodeFormatScripts() {
 
 task pythonIsInstalled(type: Exec) {
   description "Check that the python executable is installed."
-  executable = "python"
+  executable = "python3"
   args "--version"
 }
 
@@ -222,7 +227,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
@@ -239,7 +244,7 @@ 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

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
+distributionUrl=https\://services.gradle.org/distributions/gradle-6.1.1-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

src/backend/z3smt/Z3SmtFormatTranslator.java

@@ -6,6 +6,7 @@
 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 +41,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 +57,22 @@ 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);
     }
 
     /**

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,6 +24,7 @@
 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;
@@ -48,7 +50,7 @@
 
 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;
 
@@ -160,8 +162,16 @@ protected void addCheckedCodeDefaults(QualifierDefaults defs) {
         defs.addCheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.LOCAL_VARIABLE);
     }
 
+    @SuppressWarnings("deprecation")
+    @Override
+    public QualifierHierarchy createQualifierHierarchy() {
+        return MultiGraphQualifierHierarchy.createMultiGraphQualifierHierarchy(this);
+    }
+
+    @SuppressWarnings("deprecation")
     @Override
-    public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) {
+    public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory(
+            MultiGraphFactory factory) {
         return new UnitsQualifierHierarchy(factory);
     }
 

src/units/UnitsChecker.java

@@ -1,5 +1,6 @@
 package units;
 
+import checkers.inference.BaseInferenceRealTypeFactory;
 import checkers.inference.BaseInferrableChecker;
 import checkers.inference.InferenceChecker;
 import checkers.inference.InferrableChecker;
@@ -52,7 +53,7 @@ public UnitsVisitor createVisitor(
     }
 
     @Override
-    public UnitsAnnotatedTypeFactory createRealTypeFactory() {
+    public BaseInferenceRealTypeFactory createRealTypeFactory(boolean infer) {
         return new UnitsAnnotatedTypeFactory(this);
     }