Skip to content

Commit

Permalink
PICO-local-pull-in (#1)
Browse files Browse the repository at this point in the history
* adapt pico to CF and CFI master

* fix pico per changes in upstream CF and CFI

* remove incorrect aliasing and unnecessary method check

* remove wrong test diagnostic

* adapt to upstream changes

* fix extends and implements check

* tweak travis build script

* Remove useless separators.

* Unify the name of test files.

* Fix typo.

* Fix typo.

* Fix typo.

* Complete the messages.

* Use all dirs and jar file to fix the issue that "messages.properties" cannot be found. (#1)

* Tweaks.

* Use the correct error key.

* Fix typo (CompatabilityBEI2.java -> CompatibilityBEI2.java) and make CompatibilityBEI2.java pass. (opprop#8)

Make CompatibilityBEI2.java pass.

* Update.

* Update.

* api updates

* typo

* default-for annotator, default bottom on null, allow readonly as upper bound

* Implement super constructor call check.
Replace the error key "super.constructor.invocation.incompatible" with "super.invocation.invalid".
Tweaks test files to pass the test.

* Improve code and javadoc.

* clean debug messages and comment

* fixed HashCodeSafetyExample, addMissingAnnotations->replaceAnnotation

* fixed CompatibilityBEI2 + ReceiverTypeOutsideConstructor: pull default annotation for extends and implements clauses

* milestone: all typecheck tests passed

* add anno invalid check in local variables; add RDM extends/implements rules

* override cf default extends/implements checks

* fix anonymous type of new clause and test case
milestone: no INITIAL_TYPECHECK error in inference tests

* reuse test cases for typecheck and infer initial typecheck

* fix a accidentally disabled test case

* fix additional tests' errors

* test vpa over imp

* TODO: resolve path issues, remove this when fixed

* default class bound and super clause

* default class bound and super clause enhanced

* implicit immutable class bound + cast.unsafe

* remove wrong cast.unsafe keys

* bound of array fixed to READONLY. VPA not needed here because any type is permitted.
Note: how does PICO prevent changes on immutable arrays?

* bottom workaround + vpa interface

* enum default immutable. TODO: fix constructor check in mutable enum decl

* fix enum default in inference

* doc

* relocate common interface and annotator

* bound

* enum & super clause

* test case update

* tweaks on generic

* fix anno

* poly workaround

* update test cases (typecheck 100%, inference-init-tc 100%)

* API update: report

* API update: remove @DefaultInUncheckedCodeFor

* remove @spm

* Revert "remove @spm"

This reverts commit fe280a96

* @spm for static moved to new api

* exclude decl when checking static RDM (TC: 100%, INF: 6 fail)

* small tweaks

* tc cast.unsafe (TC: 100%, INF: 4 fail)

* inf-> workaround for anonymous class

* a small tweak

* update test cases (TC all pass)

* re-remove @spm

* add CF all-systems test

* small tweaks on test drivers

* interface

* isSubtype use native api

* infer atf + get bound

* tweaks

* checker.report update

* checker.report update

* tc

* tc

* ignore rdm on fields

* rdm field logic + tc

* VPA post check

* vpa post check

* field rdm default

* check anno

* tc update

* transitive (needs fix)

* class bound != PM

* receiver != BOTTOM

* stop assign immutable constant slot to enum usage. enum could be mutable

* PICO does not need existential slot on class decl anno

* use constant slot for explicit class decl anno

* update init bound extraction function

* update call to init bound extraction function

* prevent poly infer

* bound handling for anonymous class

* anonymous class method receiver workaround

* workarounds for anonymous class for getTypeOfExtendsImplements

* extract method

* do not apply real anno to atm during infer

* not apply immutable constant to enum during infer-typecheck

* add init bound extraction function

* update tc

* array bound -> RDM (TC)

* exclude static inner class decl from static scope

* don't check with default during inference

* add immutable alias for real type factory

* array decl method

* implicit shallow immutable warning (TC)

* tune up vpa

* better logic to check anonymous

* enum heck

* enforce check without refinement

* workaround for implicit lib type param

* disable alias

* workaround: vpa decl w/o anno

* consistency infer and tc

* ext and imp clause logic

* override base ext/imp clause check

* override base check on ext/imp clauses

* anonymous class logic

* receiver cannot infer to poly

* allow explicit poly on receiver

* class bound for infer

* allow factory to get class decl slot

* annotator: handle decl bound

* annotator: skip null

* annotator: replace real anno

* annotator: not infer to poly

* annotator: drop super decl constraints

* visitor: skip uses w/o slot

* rdm-field: field uses be both rdm or mutable

* comments

* notes

* tweaks

* stubs

* reim test cases

* glacier test cases

* temp ignore all systems test

* stub path problem

* +useOptimisticUncheckedDefaults

* import issue

* import issue

* update pico, fix CF api rename, update gradle version

* commits for fixing PICO-TypeCheck and part of PICO-Infer

* resolve new array problems

* add inference component back to gradle test

* E on line 5 extends readonly, but the declared on line 3 extends immutable

* use valueof static method

* use smaller case local variable

* add imports to the testfile

* change implicit.shallow.immutable from warning to error

* make the testcase more clear

* Clarify the purpose of the junit test; make default annotations explicitly for one junit test

* refactor and fix bugs causing test failures

* fix typecheck error

* Adapt PICO to opprop

* Delete glacier and reminfer test for merge

* Delete reminfer test for merge

* Add HoldsForDefaultValue for quals

* Delete old PICO files

* Add new line at the end of files

* Fix compile test errors

* Delete reim and glacier related tests

* Add error to test case

* Handle initialization block

* Add a new line at the end of file

* Update build.gradle

* Wrap up type check

* Add a new line at the end

* Further clean up the code

* Simplify the code

* Further clean up

* New line at the end

---------

Co-authored-by: Baorui Zhou <b42zhou@uwaterloo.ca>
Co-authored-by: xingweitian <13183370+xingweitian@users.noreply.github.com>
Co-authored-by: Werner Dietl <wdietl@gmail.com>
Co-authored-by: xingweitian <xingweitian@gmail.com>
Co-authored-by: lnsun <lnsun@noreply.github.com>
Co-authored-by: lnsun <57457122+lnsun@users.noreply.github.com>
Co-authored-by: Haifeng Shi <h223shi@uwaterloo.ca>
Co-authored-by: Haifeng Shi <shihaifeng1998@gmail.com>
  • Loading branch information
9 people authored May 30, 2024
1 parent d9665fe commit 848e463
Show file tree
Hide file tree
Showing 101 changed files with 3,515 additions and 2,163 deletions.
22 changes: 7 additions & 15 deletions .github/workflows/main.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
18 changes: 9 additions & 9 deletions build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -82,6 +81,7 @@ sourceSets {
compileJava {
options.compilerArgs = [
'-implicit:class',
'-Xlint:deprecation',
'-Awarns',
'-Xmaxwarns', '10000',
]
Expand All @@ -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 {
Expand Down
11 changes: 6 additions & 5 deletions check.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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=""
Expand All @@ -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

Expand All @@ -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"
2 changes: 1 addition & 1 deletion gradle/wrapper/gradle-wrapper.properties
Original file line number Diff line number Diff line change
Expand Up @@ -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
12 changes: 9 additions & 3 deletions infer.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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[@]}"
5 changes: 3 additions & 2 deletions run-dljc.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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
Expand Down
11 changes: 11 additions & 0 deletions src/main/java/pico/common/ExtendedViewpointAdapter.java
Original file line number Diff line number Diff line change
@@ -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);
}
Loading

0 comments on commit 848e463

Please sign in to comment.