Skip to content

Commit

Permalink
Merge pull request #317 from njit-jerse/dev-docs
Browse files Browse the repository at this point in the history
Developer docs
  • Loading branch information
LoiNguyenCS authored Jul 7, 2024
2 parents da5996d + bce1052 commit 335dad0
Show file tree
Hide file tree
Showing 2 changed files with 103 additions and 0 deletions.
94 changes: 94 additions & 0 deletions DEVELOPERS.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,94 @@
## Developer documentation

This document contains information that might be useful if you want to
contribute to Specimin. We welcome improvements, bug fixes, new test
cases, and any other contributions that you'd like to make. To suggest
a change to Specimin, please open a [GitHub pull request](https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/creating-a-pull-request).

### Development Environment

Specimin's testing infrasture relies on the presence of a `bash` interpreter
and the availability of the standard Unix `diff` command, so the Specimin tests
don't natively run on Windows. To work on Specimin, you should either do your work
on a Unix machine or install [WSL](https://en.wikipedia.org/wiki/Windows_Subsystem_for_Linux).

### Testing infrastructure

Even Specimin's "unit tests" are actually full system tests: each
runs Specimin on a (small) input program and checks that it produces
an expected output program; note that the test cases themselves are
also Java programs (this sometimes confuses IDEs).

Each test case has a name (e.g., "onefilesimple") and three parts:
* the test runner, which is a JUnit test stored under
`src/test/java/org/checkerframework/specimin`. The name of a new
test runner should always be the test name in CamelCase plus the word
"Test" (e.g., `OneFileSimpleTest.java`).
* the test input. This is the program that Specimin should minimize.
It is stored under `src/test/resources/$testname/input`, where `$testname`
is the name of the test. Note that this must be a Java program,
and therefore must also respect the usual Java conventions - for example,
if the test input is in a package, there must be a corresponding file structure
here.
* the expected test output. It is stored in `src/test/resources/$testname/expected`.
It must be an independently-compilable Java program; our CI system checks this requirement
by running the `./gradlew expectedTestOutputsMustCompile` command.

You can run all of the tests via `./gradlew test`. When debugging a specific
test, I usually use a command like this one (replacing `MethodRef2Test` with the
name of the test runner for the test of interest):
```
./gradlew test -PskipCheckerFramework --tests "MethodRef2Test"
```

The `-PskipCheckerFramework` is useful to keep the edit-test-debug cycle
short: re-running the Checker Framework to test each small code change
is too time-consuming.

### Continuous Integration

To pass a CI build, a PR must meet the following requirements:
* the code must be properly formatted; `./gradlew spotlessJava` should
pass with no errors. You can fix formatting errors by running
`./gradlew spotlessApply` and then committing the result. Watch out
for the formatter adding ugly line breaks in code comments!
* the code must typecheck with the Checker Framework's Nullness,
Resource Leak, Interning, and Signature checkers. See
[the Checker Framework manual](https://checkerframework.org/manual/)
for more information about these checkers and how to use them.
* the code must not trigger any warnings from [ErrorProne](https://errorprone.info/)
* all expected test outputs must compile
* all tests must pass
* the [specimin-evaluation integration tests](https://github.com/njit-jerse/specimin-evaluation)
must have the expected outcomes (which may not always be passing). More on this below.

### Integration Tests

Specimin's integration tests come from a set of 20 historical typechecker
bugs from the javac and Checker Framework issue trackers. Ideally,
Specimin would reproduce the typechecker's output on all 20 of these bugs.
However, due to Specimin's approximation, that isn't true for all of the historical
bugs. The repo therefore has a set of files that indicate the expected status for
each of these bugs along three axes:
* `./src/main/resources/target_status.json` records which bugs do and do not
trigger a crash in Specimin
* `./src/main/resources/min_program_compile_status.json` records for which bugs
Specimin produces an independently-compilable program
* `./src/main/resources/min_program_compile_status.json` records for which bugs
Specimin successfully preserves the typechecker's behavior

If you fix a bug in Specimin, and CI fails because one of these changes from
"FAIL" to "PASS", then congratulations---the bug you fixed also fixed that
integration test! Just change the appropriate `.json` file(s) to record the new
status and re-run CI.

If you make a PR and one of these changes from "PASS" to "FAIL", you won't be
able to merge the PR until that integration test is fixed. You can reproduce the
failure locally by checking out the [specimin-evaluation repo](https://github.com/njit-jerse/specimin-evaluation)
and running a command like this:
```
export SPECIMIN=/path/to/your/copy/of/specimin/with/your/changes
python3 main.py --debug cf-691
```

(Replace "cf-691" above with the name of the failing integration test.)
9 changes: 9 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -257,3 +257,12 @@ In cases like these, Specimin chooses the latter: it assumes that the JDK
is available. If you want to target part of the JDK itself with Specimin,
this means that it's necessary to *relocate* JDK classes (into a non `java.*`
package); see the CF-577 test in the integration tests for an example.

### Reporting issues and contributing

We welcome bug reports. Please make a GitHub issue with the command
that you used to run Specimin and describe what went wrong, and we'll
look into it as soon as we can.

If you'd like to contribute to Specimin, we have a separate document
with [developer documentation](https://github.com/njit-jerse/specimin/DEVELOPERS.md).

0 comments on commit 335dad0

Please sign in to comment.