-
Notifications
You must be signed in to change notification settings - Fork 2
Impurity annotation #83
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
mernst
wants to merge
38
commits into
randoop:main
Choose a base branch
from
mernst:impurity-annotation
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
38 commits
Select commit
Hold shift + click to select a range
7793d51
Add checker-qual for running impurity obj fuzzing
776styjsu 8f604c2
Move all subject program jars into jars/
776styjsu c69ea5d
Add the jars back
776styjsu 8eda5bd
Remove version number for CF to reduce potential future refactor effort
776styjsu a7485fe
Less indentation for comments
mernst 3ea8f45
Add annotated jars; use them when GRT_FUZZING is on
776styjsu 2d08e1f
Merge branch 'impurity-annotation' of github.com:776styjsu/grt-testin…
776styjsu 3d1d11a
Add annotated jars; use them when GRT_FUZZING is on; Merge
776styjsu 5905a5a
Add missing separator
776styjsu ea2a440
Fix jdom dependencies path
776styjsu 37bbb96
Update slf4j jar namespace; remove binders
776styjsu 8b7c211
Merge branch 'randoop:main' into main
776styjsu cde99c4
Merge ../grt-testing-branch-main into impurity-annotation
mernst 12cea4d
Merge branch 'main' into impurity-annotation
776styjsu 5e6cc7d
Merge ../grt-testing-branch-main into impurity-annotation
mernst 5e6e92e
Merge ../grt-testing-branch-main into impurity-annotation
mernst c5c5f91
Abstract out version number
mernst a35c932
Merge ../grt-testing-branch-main into impurity-annotation
mernst 41297e7
Fix make issues
776styjsu 0e3f50e
Fix make
776styjsu a9f0f73
Update scripts/Makefile
mernst 659177e
Remove stray command-line arguments
mernst dd22826
Merge ../grt-testing-branch-main into impurity-annotation
mernst 353d40c
Merge branch 'randoop:main' into impurity-annotation
776styjsu 260ce15
Add README.md on building annotated subject-program jars
776styjsu 79545fd
Update README.md
776styjsu 4c6a19f
Update README.md
776styjsu ceb5b82
Update README.md
776styjsu 5cc6053
Merge ../grt-testing-branch-main into impurity-annotation
mernst cc23b13
Merge ../grt-testing-branch-main into impurity-annotation
mernst 7672dd7
Merge main into impurity-annotation
035b0c1
Fix linter
be4b6c6
Fix bug in grt fuzzing check
fab2301
Fix last linter
66b6429
Merge ../grt-testing-branch-main into impurity-annotation
mernst 4635465
Only `sh` is needed, not full `bash`
mernst 9fa1783
Fill paragraph
mernst a26c382
Brevity, fix `CHECKERFRAMEWORK` environment variable
mernst File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Some comments aren't visible on the classic Files Changed page.
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file not shown.
Binary file not shown.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,66 @@ | ||
| # Annotated Subject Program JARs | ||
|
|
||
| This folder holds subject JARs with purity annotations: `@Pure`, | ||
| `@SideEffectFree`, `@Impure`, and related qualifiers from | ||
| `org.checkerframework.framework.qual` Compared to `subject-programs/jars/`, the | ||
| compiled bytecode here is the same, but the class files have purity | ||
| annotations. No other code or resources are altered. | ||
|
|
||
| The annotations are produced by the Checker Framework whole-program inference. | ||
|
|
||
| ## Why the annotations matter | ||
|
|
||
| The `GRT_FUZZING` feature in `scripts/mutation-randoop.sh` prioritizes impure | ||
| calls to mutate an object's state before exercising additional API entry points. | ||
| The annotations provide the information it needs. | ||
|
|
||
| ## Rebuilding an annotated JAR | ||
|
|
||
| 1. **Fetch sources**: Run `scripts/get-all-subject-src.sh` to populate | ||
| `subject-programs/src/<subject-program>/`. | ||
| 2. **Build the plain JAR**: In the subject directory, run the build command | ||
| found in `subject-programs/README.build`. The result lands in | ||
| `subject-programs/jars/` or the subject's usual build folder. | ||
| 3. **Set up inference tooling**: Point your environment at the local Checker | ||
| Framework build: | ||
|
|
||
| ```sh | ||
| export CHECKERFRAMEWORK=/path/to/grt-testing/scripts/build/checker-framework | ||
| export PATH="$CHECKERFRAMEWORK/annotation-file-utilities/bin:$PATH" | ||
| export JAVAC_JAR="$CHECKERFRAMEWORK/checker/dist/javac.jar" | ||
| ``` | ||
|
|
||
| 4. **Set the classpath**: Start with the JAR you just built, then | ||
| append any dependencies: | ||
| - Ant projects usually ship extra JARs in a local `jars/` or `lib/` folder. | ||
| - Maven projects can generate a classpath with | ||
| `mvn -q dependency:build-classpath -Dmdep.outputFile=target/wpi-classpath.txt`. | ||
| 5. **Run inference**: From the subject directory, execute: | ||
|
|
||
| ```sh | ||
| $CHECKERFRAMEWORK/checker/bin/infer-and-annotate.sh \ | ||
| "org.checkerframework.framework.util.PurityChecker" \ | ||
| "$RUNTIME_CLASSPATH" \ | ||
| $(find src -name "*.java") | ||
| ``` | ||
|
|
||
| The script rewrites the sources in place with the inferred annotations. | ||
| 6. **Rebuild**: Repeat the command from step 2 to produce an annotated JAR. | ||
| Copy it to this folder. | ||
|
|
||
| ### Worked example (a4j-1.0b) | ||
|
|
||
| ```sh | ||
| cd subject-programs/src/a4j-1.0b | ||
| ant createJar # build the baseline JAR | ||
| export CHECKERFRAMEWORK=... # reuse the env vars above | ||
| export PATH="$CHECKERFRAMEWORK/annotation-file-utilities/bin:$PATH" | ||
| export JAVAC_JAR="$CHECKERFRAMEWORK/checker/dist/javac.jar" | ||
| RUNTIME_CLASSPATH="../../jars/a4j-1.0b.jar:jars/jox116.jar:jars/log4j-1.2.4.jar" | ||
| $CHECKERFRAMEWORK/checker/bin/infer-and-annotate.sh \ | ||
| "org.checkerframework.framework.util.PurityChecker" \ | ||
| "$RUNTIME_CLASSPATH" \ | ||
| $(find src -name "*.java") | ||
| ant createJar # rebuild with annotations | ||
| cp dist/a4j.jar ../../annotated-jars/a4j-1.0b.jar | ||
| ``` |
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.