Run github-action CI on punit-artifact

.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

@@ -1,7 +1,7 @@
 /// Why doesn't this work on Travis under Java 7?
 /// The same text does in Randoop's build.gradle file.
 plugins {
-    id 'com.github.johnrengelman.shadow' version '6.1.0'
+    id 'com.github.johnrengelman.shadow' version '2.0.4'
 }
 
 apply plugin: 'java'
@@ -37,15 +37,15 @@ dependencies {
     compile fileTree(dir: "${cf}/checker/dist", include: "checker.jar")
     compile fileTree(dir: "${cfi}/dist", include: "checker-framework-inference.jar")
     // sat4j solver dependency
-    compile 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.6'
-    compile 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.6'
+    compile 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.5'
+    compile 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.5'
     // z3 solver dependency
     compile fileTree(dir: "${cfi}/lib", include: "com.microsoft.z3.jar")
 
     // CF test lib dependency
     testCompile fileTree(dir: "${cf}/framework-test/build/libs", include: "framework-test-*.jar")
     testCompile fileTree(dir: "${cfi}/dist", include: "inference-framework-test-lib.jar")
-    testCompile 'junit:junit:4.13.2'
+    testCompile 'junit:junit:4.13'
 }
 
 sourceSets {
@@ -180,7 +180,7 @@ task getCodeFormatScripts() {
 
 task pythonIsInstalled(type: Exec) {
   description "Check that the python executable is installed."
-  executable = "python"
+  executable = "python3"
   args "--version"
 }
 
@@ -222,7 +222,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,12 +239,16 @@ 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 {
+    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)

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

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