Typecheck Fix

build.gradle

@@ -46,23 +46,24 @@ 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.5'
+    implementation 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.5'
     // 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.12'
 }
 
 sourceSets {
     main {
         java {
             srcDirs = ["src/main/java"]
+            exclude "pico/inference/**"
+
         }
 
         resources {
@@ -75,6 +76,8 @@ sourceSets {
         java {
             // TODO: we shouldn't need source level dependency on CFITest
             srcDirs = ["src/test/java", "${cfiPath}/tests/checkers/inference/test"]
+            exclude "pico/ImmutabilityInferenceInitialTypecheckTest.java","pico/ImmutabilityReImInferenceTest.java",
+            "pico/ImmutabilityInferenceTest.java"
         }
     }
 }

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=""
@@ -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

@@ -19,6 +19,8 @@ CHECKER=pico.inference.PICOInferenceChecker
 
 SOLVER=pico.inference.solver.PICOSolverEngine
 
+STUBS="src/main/java/pico/inference/jdk.astub"
+
 declare -a ARGS
 for i in "$@" ; do
     if [[ $i == "-ds" ]] ; then
@@ -38,4 +40,5 @@ IS_HACK=true
 # Start the inference
 $CFI/scripts/inference-dev -m ROUNDTRIP --checker "$CHECKER" --solver "$SOLVER" \
     --solverArgs="useGraph=false,collectStatistic=true" --hacks="$IS_HACK" \
+    --cfArgs="-Astubs=$STUBS" \
     -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);
+}