PICO-local-pull-in

.github/workflows/main.yml

@@ -49,18 +49,10 @@ jobs:
         if: ${{ steps.build.outcome == 'success' }}
         run: ./gradlew ImmutabilityTypecheckExtendedTest
 
-      - name: PICO Glacier TypeCheck Test
-        if: ${{ steps.build.outcome == 'success' }}
-        run: ./gradlew ImmutabilityTypecheckGlacierTest
-
-      - name: PICO Inference Initial Typecheck Test
-        if: ${{ steps.build.outcome == 'success' }}
-        run: ./gradlew ImmutabilityInferenceInitialTypecheckTest
-
-      - name: PICO Inference Test
-        if: ${{ steps.build.outcome == 'success' }}
-        run: ./gradlew ImmutabilityInferenceTest
-
-      - name: PICO ReIm Inference Test
-        if: ${{ steps.build.outcome == 'success' }}
-        run: ./gradlew ImmutabilityReImInferenceTest
+#      - name: PICO Inference Initial Typecheck Test
+#        if: ${{ steps.build.outcome == 'success' }}
+#        run: ./gradlew ImmutabilityInferenceInitialTypecheckTest
+#
+#      - name: PICO Inference Test
+#        if: ${{ steps.build.outcome == 'success' }}
+#        run: ./gradlew ImmutabilityInferenceTest

build.gradle

@@ -46,17 +46,16 @@ repositories {
 }
 
 dependencies {
-    compile fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar")
-    compile fileTree(dir: "${cfiPath}/dist", include: "checker-framework-inference.jar")
+    implementation fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar")
+    implementation fileTree(dir: "${cfiPath}/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'
+    implementation 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.6'
+    implementation 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.6'
     // The production code uses the SLF4J logging API at compile time
-    compile 'org.slf4j:slf4j-api:1.7.30'
-
+    implementation 'org.slf4j:slf4j-api:1.7.29'
     // CF test lib dependency
-    testCompile fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar")
-    testCompile 'junit:junit:4.13.2'
+    testImplementation fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar")
+    testImplementation 'junit:junit:4.13.2'
 }
 
 sourceSets {
@@ -82,6 +81,7 @@ sourceSets {
 compileJava {
     options.compilerArgs = [
             '-implicit:class',
+            '-Xlint:deprecation',
             '-Awarns',
             '-Xmaxwarns', '10000',
     ]
@@ -107,7 +107,7 @@ afterEvaluate {
                 JDK_JAR: "${cfPath}/checker/dist/jdk8.jar"
 
         environment "external_checker_classpath", "${picoPath}/build/classes/java/main:${picoPath}/build/resources/main"
-
+        maxHeapSize = "1024m"
         if (isJava8) {
             jvmArgs "-Xbootclasspath/p:${cfiPath}/dist/javac.jar"
         } else {

check.sh

@@ -10,7 +10,8 @@ export JAVAC=$CF/checker/bin/javac
 export PICO=$(cd $(dirname "$0") && pwd)
 
 # Dependencies
-export CLASSPATH=$PICO/build/classes/java/main:$CFI/dist/checker-framework-inference.jar
+export CLASSPATH=$PICO/build/classes/java/main:$PICO/build/resources/main:\
+$PICO/build/libs/immutability.jar:$CFI/dist/checker-framework-inference.jar
 
 # Command
 DEBUG=""
@@ -19,8 +20,8 @@ CHECKER="pico.typecheck.PICOChecker"
 declare -a ARGS
 for i in "$@" ; do
     if [[ $i == "-d" ]] ; then
-        echo "Typecheck using debug mode. Listening at port 5050. Waiting for connection...."
-        DEBUG="-J-Xdebug -J-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=5050"
+        echo "Typecheck using debug mode. Listening at port 5005. Waiting for connection...."
+        DEBUG="-J-Xdebug -J-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=5005"
         continue
     fi
 
@@ -35,9 +36,9 @@ done
 cmd=""
 
 if [ "$DEBUG" == "" ]; then
-	cmd="$JAVAC -cp "${CLASSPATH}" -processor "${CHECKER}" "${ARGS[@]}""
+    cmd="$JAVAC -cp "${CLASSPATH}" -processor "${CHECKER}" "${ARGS[@]}""
 else
-	cmd="$JAVAC "$DEBUG" -cp "${CLASSPATH}" -processor "${CHECKER}" -AatfDoNotCache "${ARGS[@]}""
+    cmd="$JAVAC "$DEBUG" -cp "${CLASSPATH}" -processor "${CHECKER}" -AatfDoNotCache "${ARGS[@]}""
 fi
 
 eval "$cmd"

gradle/wrapper/gradle-wrapper.properties

@@ -2,4 +2,4 @@ distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-4.5-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-7.3.3-bin.zip

infer.sh

@@ -8,7 +8,9 @@ export CFI=$JSR308/checker-framework-inference
 export PICO=$(cd $(dirname "$0") && pwd)
 
 # Dependencies
-export CLASSPATH=$PICO/build/classes/java/main:$CFI/dist/checker-framework-inference.jar
+export CLASSPATH=$PICO/build/classes/java/main:$PICO/build/resources/main:\
+$PICO/build/libs/immutability.jar:$CFI/dist/checker-framework-inference.jar
+
 export external_checker_classpath=$PICO/build/classes/java/main:$PICO/build/resources/main
 
 export AFU=$JSR308/annotation-tools/annotation-file-utilities
@@ -18,6 +20,9 @@ export JDK_JAR=$CF/checker/dist/jdk8.jar
 CHECKER=pico.inference.PICOInferenceChecker
 
 SOLVER=pico.inference.solver.PICOSolverEngine
+#SOLVER=checkers.inference.solver.DebugSolver
+
+STUBS="src/main/java/pico/inference/jdk.astub"
 
 declare -a ARGS
 for i in "$@" ; do
@@ -31,11 +36,12 @@ done
 
 SOLVER_ARGS=useGraph=false,collectStatistic=true
 
-IS_HACK=true
+TRUE=true
 
 # echo "${ARGS[@]}"
 
 # Start the inference
 $CFI/scripts/inference-dev -m ROUNDTRIP --checker "$CHECKER" --solver "$SOLVER" \
-    --solverArgs="useGraph=false,collectStatistic=true" --hacks="$IS_HACK" \
+    --solverArgs="useGraph=false,collectStatistic=true" --hacks="$TRUE" \
+    --cfArgs="-Astubs=$STUBS" --makeDefaultsExplicit="$TRUE" \
     -afud ./annotated "${ARGS[@]}"

run-dljc.sh

@@ -9,7 +9,7 @@ export AFU="$JSR308"/annotation-tools/annotation-file-utilities
 export PATH="$PATH":"$AFU"/scripts
 export CFI="$JSR308"/checker-framework-inference
 
-export CLASSPATH="$JSR308"/immutability/build/classes/main:$CHECKERFRAMEWORK/dataflow/build:$CHECKERFRAMEWORK/javacutil/build:$CHECKERFRAMEWORK/stubparser/build:$CHECKERFRAMEWORK/framework/build:$CHECKERFRAMEWORK/checker/build:$SOLVER/bin:$CHECKERFRAMEWORK/framework/tests/junit-4.12.jar:$CHECKERFRAMEWORK/framework/tests/hamcrest-core-1.3.jar:$CFI/dist/checker-framework-inference.jar:$CFI/dist/org.ow2.sat4j.core-2.3.4.jar:$CFI/dist/commons-logging-1.2.jar:$CFI/dist/log4j-1.2.16.jar:$JSR308/jsr308-langtools/build/classes:$CLASSPATH
+export CLASSPATH="$JSR308"/immutability/build/classes/java/main:$CHECKERFRAMEWORK/dataflow/build:$CHECKERFRAMEWORK/javacutil/build:$CHECKERFRAMEWORK/stubparser/build:$CHECKERFRAMEWORK/framework/build:$CHECKERFRAMEWORK/checker/build:$SOLVER/bin:$CHECKERFRAMEWORK/framework/tests/junit-4.12.jar:$CHECKERFRAMEWORK/framework/tests/hamcrest-core-1.3.jar:$CFI/dist/checker-framework-inference.jar:$CFI/dist/org.ow2.sat4j.core-2.3.4.jar:$CFI/dist/commons-logging-1.2.jar:$CFI/dist/log4j-1.2.16.jar:$JSR308/jsr308-langtools/build/classes:$CLASSPATH
 
 #parsing build command of the target program
 build_cmd="$2"
@@ -30,8 +30,9 @@ elif [[ "$1" = "-i" ]] ; then
     rm -rf logs annotated
     echo "Cleaning Done."
     CHECKER="pico.inference.PICOInferenceChecker"
+#    SOLVER="checkers.inference.solver.DebugSolver"
     SOLVER="pico.inference.solver.PICOSolverEngine"
-    running_cmd="python $DLJC/dljc -t inference --checker "${CHECKER}" --cfArgs=\"-AoptimalSolution\" --solver "${SOLVER}" --solverArgs=\"collectStatistic=true,useGraph=false\" --mode ROUNDTRIP -afud $WORKING_DIR/annotated -o logs -- $build_cmd "
+    running_cmd="python $DLJC/dljc -t inference --checker "${CHECKER}" --cfArgs=\"-AoptimalSolution -Astubs=/home/l82sun/workspace/opprop/immutability/src/main/java/pico/inference/jdk.astub\" --solver "${SOLVER}" --solverArgs=\"collectStatistic=true,useGraph=false\"  --guess --stubs="/home/l82sun/workspace/opprop/immutability/src/main/java/pico/inference/jdk.astub" --mode ROUNDTRIP -afud $WORKING_DIR/annotated -o logs -- $build_cmd "
 else
     echo "Unknown tool: should be either -t|-i but found: ${1}"
     exit 1

src/main/java/pico/common/ExtendedViewpointAdapter.java

@@ -0,0 +1,11 @@
+package pico.common;
+
+import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.type.ViewpointAdapter;
+
+import javax.lang.model.element.AnnotationMirror;
+
+public interface ExtendedViewpointAdapter extends ViewpointAdapter {
+    AnnotatedTypeMirror rawCombineAnnotationWithType(AnnotationMirror anno, AnnotatedTypeMirror type);
+    AnnotationMirror rawCombineAnnotationWithAnnotation(AnnotationMirror anno, AnnotationMirror type);
+}