Merge branch 'master' into genetic-maxsat

.github/workflows/main.yml

@@ -14,30 +14,35 @@ jobs:
       fail-fast: false
       matrix:
         group: [ cfi-tests, downstream-ontology, downstream-security-demo, downstream-universe ]
-        jdk: [ 8, 11 ]
+        jdk: [ 8, 11, 17 ]
     runs-on: ubuntu-latest
     steps:
       - name: Install dependencies
         run: |
           sudo apt update
-          sudo apt install ant cpp gradle jq libcurl3-gnutls make maven mercurial python3-requests unzip wget binutils build-essential
+          sudo apt install ant cpp gradle jq libcurl3-gnutls make mercurial python3-requests unzip wget binutils build-essential
+      - name: Set up Maven
+        uses: stCarolas/[email protected]
+        with:
+          maven-version: 3.8.6
       - name: Pull Request Checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         with:
           ref: ${{github.event.pull_request.head.ref}}
           repository: ${{github.event.pull_request.head.repo.full_name}}
         if: github.head_ref != ''
       - name: Push Checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         if: github.head_ref == ''
       - name: Set up Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.8'
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: ${{ matrix.jdk }}
+          distribution: 'temurin'
       - name: Dump GitHub context
         env:
           GITHUB_CONTEXT: ${{ toJson(github) }}

README.md

@@ -1,11 +1,8 @@
-Continuous integration status of master:
-![CFI status](https://github.com/opprop/checker-framework-inference/workflows/CI/badge.svg)
-
-Checker Framework Inference
+Checker Framework Inference [![Build Status](https://github.com/opprop/checker-framework-inference/workflows/CI/badge.svg)](https://github.com/opprop/checker-framework-inference/actions/workflows/main.yml)
 ===========================
 
 This project is a general type inference framework,
-built upon the [Checker Framework](https://checkerframework.org/).
+built upon the [EISOP Checker Framework](https://eisop.github.io/).
 
 Given a program with no type annotations, Checker Framework Inference produces a program with type annotations.
 
@@ -31,7 +28,7 @@ Configure Eclipse to edit Checker Framework Inference
 
 The instructions here assumes you have cloned this project into a folder called `checker-framework-inference`.
 
-1) Follow the instructions in the [Checker Framework Manual](https://checkerframework.org/manual/#building-eclipse)
+1) Follow the instructions in the [EISOP Checker Framework Manual](https://eisop.github.io/cf/manual/manual.html#eclipse)
 to download, build, and configure Eclipse to edit the Checker Framework. The Checker Framework Inference Eclipse
 project depends on the eclipse projects from Checker Framework.
 
@@ -95,7 +92,7 @@ To test the build:
 Execution
 ---------
 
-Verify you have all of the requirements.
+Verify you have all the requirements.
 
 ````
 ./scripts/inference
@@ -119,7 +116,7 @@ Available options are [INFER, TYPECHECK, ROUNDTRIP, ROUNDTRIP_TYPECHECK]
     Generates and solves the constraints and writes the results to default.jaif file
 
   * `TYPECHECK`:
-    Typechecks the existin code
+    Typechecks the existing code
 
   * `ROUNDTRIP`:
     Generates and solves the constraints and then inserts the results
@@ -146,10 +143,10 @@ The classpath that is required by target program.
 `checkers.inference.solver.PropagationSolver` and `checkers.inference.solver.SolverEngine` are real solvers
 at the moment.
 
-Omiting the solver will create an output that numbers all of the
+Omitting the solver will create an output that numbers all the
 annotation positions in the program.
 
-`checkers.inference.solver.DebugSolver` will output all of the
+`checkers.inference.solver.DebugSolver` will output all the
 constraints generated.
 
 
@@ -178,7 +175,7 @@ Specifies what concrete solver is going to use.
 
   * `LogiQL`: Encodes constraints as statements of LogiQL language and use LogicBlox to solve.
 
-  * `Z3` with bit vector theory: Encodes constraints as Max-SMT problem with bit vectory theory, and use Z3 library to solve.
+  * `Z3` with bit vector theory: Encodes constraints as Max-SMT problem with bit vector theory, and use Z3 library to solve.
 
 
   `MaxSat` solver is used by default.
@@ -187,7 +184,7 @@ Specifies what concrete solver is going to use.
 Specifies whether to separate constraints into multiple components through constraint graph and solve them respectively. The default value is true.
 
 * `solveInParallel`
-If constraints are separated by constraint graph, this arguments indicates whether to solve the components in parallel (multithreading). The default value is true.
+If constraints are separated by constraint graph, this argument indicates whether to solve the components in parallel (multithreading). The default value is true.
 
 * `collectStatistics`
 Specifies whether to collect statistic with respect to timing, size of constraints, size of encoding, etc. The default value is false.

build.gradle

@@ -13,7 +13,6 @@ ext {
     checkerFrameworkPath = System.getenv('CHECKERFRAMEWORK') ?: "${jsr308}/checker-framework"
     checkerJar = "${checkerFrameworkPath}/checker/dist/checker.jar"
     afu = "${jsr308}/annotation-tools/annotation-file-utilities"
-    z3Jar = "${projectDir}/lib/com.microsoft.z3.jar"
     lingelingTar = "${projectDir}/lib/lingeling.tar.gz"
     dljcScript = "${jsr308}/do-like-javac/dljc"
 
@@ -22,6 +21,20 @@ ext {
     isJava8 = JavaVersion.current() == JavaVersion.VERSION_1_8
 
     errorproneJavacVersion = '9+181-r4173-1'
+
+    // Keep in sync with checker-framework/build.gradle.
+    // TODO: find a way to directly use that variable.
+    compilerArgsForRunningCF = [
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
+            "--add-exports", "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
+            "--add-opens", "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED",
+    ]
 }
 
 println '===================================='
@@ -57,24 +70,25 @@ dependencies {
     }
 
     implementation 'org.plumelib:options:1.0.5'
-    implementation 'org.plumelib:plume-util:1.5.8'
+    implementation 'org.plumelib:plume-util:1.5.9'
 
-    implementation 'com.google.guava:guava:31.0.1-jre'
+    implementation 'com.google.guava:guava:31.1-jre'
 
     // AFU is an "includedBuild" imported in settings.gradle, so the version number doesn't matter.
     // https://docs.gradle.org/current/userguide/composite_builds.html#settings_defined_composite
-    implementation('org.checkerframework:annotation-file-utilities:*') {
+    implementation('io.github.eisop:annotation-file-utilities:*') {
         exclude group: 'com.google.errorprone', module: 'javac'
     }
 
     // Serialize constraints
     implementation 'com.googlecode.json-simple:json-simple:1.1.1'
     // Pretty print serialized constraints
-    implementation 'com.google.code.gson:gson:2.9.0'
+    implementation 'com.google.code.gson:gson:2.9.1'
 
     implementation 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.6'
     implementation 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.6'
-    implementation files(z3Jar)
+
+    implementation 'tools.aqua:z3-turnkey:4.11.2'
 
     testImplementation fileTree(dir: "${checkerFrameworkPath}/framework-test/build/libs", include: "framework-test-*.jar")
     // Mocking library. Used in a couple tests
@@ -101,13 +115,6 @@ sourceSets {
     }
 }
 
-task buildZ3(type: Exec) {
-    description 'Build Z3 solver'
-    onlyIf { !(new File(z3Jar).exists()) }
-    workingDir './scripts'
-    commandLine './buildZ3'
-}
-
 task buildLingeling(type: Exec) {
     description 'Build Lingeling solver'
     onlyIf { !(new File(lingelingTar).exists()) }
@@ -141,6 +148,7 @@ test {
         // Without this, the test throw "java.lang.OutOfMemoryError: Java heap space"
         // Corresponding pull request: https://github.com/opprop/checker-framework-inference/pull/263
         forkEvery(1)
+        jvmArgs += compilerArgsForRunningCF
     }
 
     testLogging {
@@ -170,7 +178,6 @@ test {
 }
 
 compileJava {
-    dependsOn(buildZ3)
     dependsOn(buildLingeling)
     dependsOn(buildDLJC)
     options.compilerArgs = [
@@ -210,7 +217,6 @@ task dist(dependsOn: shadowJar, type: Copy) {
             "will build checker-framework-inference.jar, copy all the relevant runtime jars into " +
             "the dist directory."
     from files(
-            "${checkerFrameworkPath}/checker/dist/jdk8.jar",
             "${checkerFrameworkPath}/checker/dist/checker.jar",
             "${checkerFrameworkPath}/checker/dist/checker-qual.jar",
             "${checkerFrameworkPath}/checker/dist/checker-util.jar",

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-7.3.3-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
+networkTimeout=10000
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

gradlew

@@ -55,7 +55,7 @@
 #       Darwin, MinGW, and NonStop.
 #
 #   (3) This script is generated from the Groovy template
-#       https://github.com/gradle/gradle/blob/master/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt
+#       https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt
 #       within the Gradle project.
 #
 #       You can find Gradle at https://github.com/gradle/gradle/.
@@ -80,13 +80,10 @@ do
     esac
 done
 
-APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
-
-APP_NAME="Gradle"
+# This is normally unused
+# shellcheck disable=SC2034
 APP_BASE_NAME=${0##*/}
-
-# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
-DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
 
 # Use the maximum available, or set MAX_FD != -1 to use that value.
 MAX_FD=maximum
@@ -143,12 +140,16 @@ fi
 if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then
     case $MAX_FD in #(
       max*)
+        # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked.
+        # shellcheck disable=SC3045
         MAX_FD=$( ulimit -H -n ) ||
             warn "Could not query maximum file descriptor limit"
     esac
     case $MAX_FD in  #(
       '' | soft) :;; #(
       *)
+        # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked.
+        # shellcheck disable=SC3045
         ulimit -n "$MAX_FD" ||
             warn "Could not set maximum file descriptor limit to $MAX_FD"
     esac
@@ -193,6 +194,10 @@ if "$cygwin" || "$msys" ; then
     done
 fi
 
+
+# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
+DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+
 # Collect all arguments for the java command;
 #   * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of
 #     shell script including quotes and variable substitutions, so put them in
@@ -205,6 +210,12 @@ set -- \
         org.gradle.wrapper.GradleWrapperMain \
         "$@"
 
+# Stop when "xargs" is not available.
+if ! command -v xargs >/dev/null 2>&1
+then
+    die "xargs is not available"
+fi
+
 # Use "xargs" to parse quoted args.
 #
 # With -n1 it outputs one arg per line, with the quotes and backslashes removed.

gradlew.bat

@@ -14,7 +14,7 @@
 @rem limitations under the License.
 @rem
 
-@if "%DEBUG%" == "" @echo off
+@if "%DEBUG%"=="" @echo off
 @rem ##########################################################################
 @rem
 @rem  Gradle startup script for Windows
@@ -25,7 +25,8 @@
 if "%OS%"=="Windows_NT" setlocal
 
 set DIRNAME=%~dp0
-if "%DIRNAME%" == "" set DIRNAME=.
+if "%DIRNAME%"=="" set DIRNAME=.
+@rem This is normally unused
 set APP_BASE_NAME=%~n0
 set APP_HOME=%DIRNAME%
 
@@ -40,7 +41,7 @@ if defined JAVA_HOME goto findJavaFromJavaHome
 
 set JAVA_EXE=java.exe
 %JAVA_EXE% -version >NUL 2>&1
-if "%ERRORLEVEL%" == "0" goto execute
+if %ERRORLEVEL% equ 0 goto execute
 
 echo.
 echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
@@ -75,13 +76,15 @@ set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
 
 :end
 @rem End local scope for the variables with windows NT shell
-if "%ERRORLEVEL%"=="0" goto mainEnd
+if %ERRORLEVEL% equ 0 goto mainEnd
 
 :fail
 rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
 rem the _cmd.exe /c_ return code!
-if  not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
-exit /b 1
+set EXIT_CODE=%ERRORLEVEL%
+if %EXIT_CODE% equ 0 set EXIT_CODE=1
+if not ""=="%GRADLE_EXIT_CONSOLE%" exit %EXIT_CODE%
+exit /b %EXIT_CODE%
 
 :mainEnd
 if "%OS%"=="Windows_NT" endlocal