-
Notifications
You must be signed in to change notification settings - Fork 0
Cross-tool oracle comparison (Infer#/CodeQL) + related-work positioning #21
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
Merged
Merged
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,156 @@ | ||
| name: oracle (cross-tool) | ||
|
|
||
| # On-demand cross-tool validation: run Own.NET's leak check, Infer#, and CodeQL | ||
| # over the SAME public C# repo and diff their leak-class findings into an | ||
| # agreement report (scripts/oracle_compare.py). Evaluation tooling — the mature | ||
| # detectors are both a recall bar and an oracle. See docs/notes/oracle.md. | ||
| # | ||
| # Trigger from the Actions tab ("Run workflow") or the API. Inputs reach the | ||
| # shell via env (never interpolated into a `run:` script) to avoid injection. | ||
| # | ||
| # Honest notes: | ||
| # * Own.NET needs no build (error-tolerant SemanticModel). The two oracles do: | ||
| # CodeQL builds a database (build-mode: none, from source); Infer# analyses | ||
| # compiled .dll+.pdb, so the target must `dotnet build`. Each oracle step is | ||
| # continue-on-error, so a build failure still yields a partial report. | ||
| # * The diff core (oracle_compare.py) is unit-tested (--selftest, run first); | ||
| # this orchestration is validated on dispatch, like mine.yml. | ||
|
|
||
| on: | ||
| workflow_dispatch: | ||
| inputs: | ||
| repo: | ||
| description: "Target: owner/repo (e.g. DapperLib/Dapper) or a git URL" | ||
| required: true | ||
| ref: | ||
| description: "Branch / tag / sha to analyse (optional, default: repo HEAD)" | ||
| required: false | ||
| default: "" | ||
| paths: | ||
| description: "Subdir to scan with own-check (optional, default: whole repo)" | ||
| required: false | ||
| default: "" | ||
| build: | ||
| description: "Project/solution under the target to `dotnet build` for Infer# (optional, default: repo root)" | ||
| required: false | ||
| default: "" | ||
|
|
||
| permissions: | ||
| contents: read | ||
| security-events: write # required by the CodeQL action internals (upload is off) | ||
|
|
||
| jobs: | ||
| oracle: | ||
| name: oracle ${{ inputs.repo }} | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| - uses: actions/setup-python@v5 | ||
| with: | ||
| python-version: "3.13" | ||
| - uses: actions/setup-dotnet@v4 | ||
| with: | ||
| dotnet-version: "8.0.x" | ||
|
|
||
| # Fast fail: the diff logic is unit-tested before we clone/build anything. | ||
| - name: Comparator selftest | ||
| run: python scripts/oracle_compare.py --selftest | ||
|
|
||
| - name: Clone the target | ||
| env: | ||
| REPO: ${{ inputs.repo }} | ||
| REF: ${{ inputs.ref }} | ||
| run: | | ||
| case "$REPO" in | ||
| http://*|https://*|git@*) url="$REPO" ;; | ||
| *) url="https://github.com/${REPO}.git" ;; | ||
| esac | ||
| git clone --depth 1 --quiet "$url" target | ||
| if [[ -n "$REF" ]]; then | ||
| # --branch only accepts a branch/tag; fetch+checkout also takes a raw SHA. | ||
| git -C target fetch --depth 1 --quiet origin "$REF" | ||
| git -C target checkout --quiet --detach FETCH_HEAD | ||
| fi | ||
| echo "COMMIT=$(git -C target rev-parse HEAD)" >> "$GITHUB_ENV" | ||
|
|
||
| # Own.NET — no build needed; scans .cs directly. | ||
| - name: Own.NET own-check | ||
| env: | ||
| PATHS: ${{ inputs.paths }} | ||
| run: | | ||
| scan="target"; [[ -n "$PATHS" ]] && scan="target/$PATHS" | ||
| set +e | ||
| scripts/own-check.sh --format human -- "$scan" > own.txt 2> own-extract.log | ||
| echo "own-check rc=$? ; $(wc -l < own.txt) finding line(s)" | ||
|
|
||
| # CodeQL — database from source (no build), default queries; we filter to | ||
| # the dispose/leak family in the comparator. | ||
| - name: CodeQL init | ||
| uses: github/codeql-action/init@v3 | ||
| continue-on-error: true | ||
| with: | ||
| languages: csharp | ||
| build-mode: none | ||
| source-root: target | ||
| - name: CodeQL analyze | ||
| uses: github/codeql-action/analyze@v3 | ||
| continue-on-error: true | ||
| with: | ||
| category: ownnet-oracle | ||
| output: codeql-out | ||
| upload: false | ||
|
|
||
| # Infer# — needs compiled binaries; build the target into one output dir. | ||
| - name: Build the target (for Infer#) | ||
| env: | ||
| BUILD: ${{ inputs.build }} | ||
| continue-on-error: true | ||
| run: | | ||
| tgt="target"; [[ -n "$BUILD" ]] && tgt="target/$BUILD" | ||
| if dotnet build "$tgt" -c Release -o _bin -v quiet; then | ||
| echo "BUILD_OK=1" >> "$GITHUB_ENV" | ||
| else | ||
| echo "target build failed — Infer# will be skipped, report stays partial" | ||
| fi | ||
| - name: Run Infer# | ||
| if: env.BUILD_OK == '1' | ||
| uses: microsoft/infersharpaction@v1.5 | ||
| continue-on-error: true | ||
| with: | ||
| binary-path: _bin | ||
|
|
||
| - name: Diff Own.NET vs the oracles | ||
| if: always() | ||
| env: | ||
| REPO: ${{ inputs.repo }} | ||
| run: | | ||
| args=(--own own.txt --target "$REPO" --commit "${COMMIT:-}" | ||
| --strip "$GITHUB_WORKSPACE/target" --strip target | ||
| --json report.json) | ||
| [[ -f infer-out/report.sarif ]] && args+=(--infersharp infer-out/report.sarif) | ||
| cq=$(find codeql-out -name '*.sarif' -type f 2>/dev/null | head -1 || true) | ||
| [[ -n "$cq" ]] && args+=(--codeql "$cq") | ||
| python scripts/oracle_compare.py "${args[@]}" > report.md | ||
| cat report.md | ||
|
|
||
| - name: Publish the report to the run summary | ||
| if: always() | ||
| run: | | ||
| if [[ -s report.md ]]; then | ||
| cat report.md >> "$GITHUB_STEP_SUMMARY" | ||
| else | ||
| echo "no report produced (see the Diff step log)" >> "$GITHUB_STEP_SUMMARY" | ||
| fi | ||
| - name: Upload the report and raw outputs | ||
| if: always() | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: oracle-report | ||
| path: | | ||
| report.md | ||
| report.json | ||
| own.txt | ||
| own-extract.log | ||
| infer-out/report.sarif | ||
| codeql-out/*.sarif | ||
| if-no-files-found: warn | ||
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,101 @@ | ||
| # Oracle comparison — validating the leak check against Infer# and CodeQL | ||
|
|
||
| We are **not** the first resource-leak detector for C#. Infer# (Microsoft, on | ||
| Facebook Infer) and CodeQL (`cs/local-not-disposed`) are mature, interprocedural, | ||
| battle-tested. That is precisely what makes them useful here: run all three over | ||
| the **same** repo and diff the leak-class findings. Cross-tool agreement is a | ||
| strong correctness signal; disagreement points straight at our precision or | ||
| recall gaps. This is evaluation tooling — a companion to corpus mining | ||
| ([`mining.md`](mining.md)), with an external reference instead of just our own | ||
| verdict. | ||
|
|
||
| ## The three buckets | ||
|
|
||
| Restricted to the comparable class — *resource leak / not disposed* (OWN001 vs | ||
| Infer#'s `DOTNET_RESOURCE_LEAK` vs CodeQL's `cs/local-not-disposed` & friends): | ||
|
|
||
| | bucket | meaning | what to do | | ||
| |---|---|---| | ||
| | **agree** | a `(file, line)` flagged by Own.NET **and** an oracle | high confidence — nothing, this is the win | | ||
| | **own-only** | flagged by us, by no oracle | triage: a candidate **false positive** to harden, *or* a real catch the oracle's leak query can't express | | ||
| | **oracle-only** | flagged by an oracle, not by us | our **recall gap** — reduce to a minimal `.cs`, then model it or record it as a known limitation | | ||
|
|
||
| Two classes sit **outside** the three-way diff and are reported separately: | ||
|
|
||
| - **Own.NET-only defect classes** — `OWN002` (use-after-dispose) and `OWN003` | ||
| (double-dispose). The oracle *leak* queries have no equivalent, so counting | ||
| them as "own-only leaks" would be misleading. They are a feature, not noise. | ||
| - **Oracle findings outside our scope** — Infer#'s `NULL_DEREFERENCE`, | ||
| thread-safety, taint, etc. Listed as context (counts by rule), not a gap. | ||
|
|
||
| ## Why this is a fair-but-honest comparison | ||
|
|
||
| - **Own.NET needs no build.** The Roslyn extractor reads a best-effort | ||
| `SemanticModel` without `dotnet restore`/build (unresolved externals become an | ||
| honest `OWN050`, not a guess). **Both oracles need the target to build**: | ||
| CodeQL constructs a database (here via `build-mode: none`, from source), Infer# | ||
| analyses compiled `.dll`+`.pdb`. So the oracle run can fail where ours doesn't | ||
| — that asymmetry is the point, and each oracle step is `continue-on-error` so a | ||
| build failure still yields a partial report. | ||
| - **Path/line matching is deliberately loose.** Tools disagree on the exact line | ||
| (allocation site vs declaration) and on path prefixes. The comparator matches | ||
| on **basename + a line window** (`--line-tol`, default 3). Robust to prefixes; | ||
| same-named files in different dirs can theoretically collide (rare — the line | ||
| disambiguates). The file-level overlap is the most robust signal. | ||
|
|
||
| ## Run it | ||
|
|
||
| In CI (no local Infer#/CodeQL/Docker needed) — Actions tab → **oracle | ||
| (cross-tool)** → *Run workflow*. The report lands in the run summary and as an | ||
| artifact (`report.md`, `report.json`, plus each tool's raw output): | ||
|
|
||
| ```text | ||
| inputs: repo = DapperLib/Dapper ref = (optional) | ||
| paths = (optional own-check subdir) build = (optional proj/sln for Infer#) | ||
| ``` | ||
|
|
||
| The diff core runs anywhere on already-produced outputs (this is what `--selftest` | ||
| exercises, and it gates CI): | ||
|
|
||
| ```sh | ||
| python scripts/oracle_compare.py \ | ||
| --own own.txt \ | ||
| --infersharp infer-out/report.sarif \ | ||
| --codeql codeql-out/csharp.sarif \ | ||
| --strip "$PWD/target" \ | ||
| --target DapperLib/Dapper --commit "$SHA" --json report.json | ||
| ``` | ||
|
|
||
| `--own` is `own-check`'s human output (same format the miner reads). The two | ||
| oracle inputs are SARIF — Infer# and CodeQL both emit it, so one parser handles | ||
| both. Extra SARIF oracles can be added with `--sarif tool=path`. | ||
|
|
||
| ## What "agree" buys us, concretely | ||
|
|
||
| The first mine of Dapper found **zero** real leaks (a well-disciplined library). | ||
| A clean run is a precision signal — but on its own it can't tell "we correctly | ||
| found nothing" from "we silently skipped everything". The oracle closes that: | ||
|
|
||
| - if the oracles also find ~nothing → genuine agreement, the codebase is clean; | ||
| - if the oracles find leaks we missed → **oracle-only**, a concrete recall target | ||
| (likely interprocedural, a field, or a `for`/`do`/`try` shape we honestly skip); | ||
| - if we flag something they don't → **own-only**, either a precision bug to fix or | ||
| a defect class (double-dispose) they don't model. | ||
|
|
||
| Pair this with the extractor's planned `--stats` coverage (methods analysed vs | ||
| skipped) and the picture is complete: how much we looked at, and how our verdicts | ||
| line up with two independent engines. | ||
|
|
||
| ## Honest gaps (v1) | ||
|
|
||
| - **No tool versions pinned in the report yet.** `microsoft/infersharpaction@v1.5` | ||
| and `github/codeql-action@v3` float on tags; the report header names the tools | ||
| but not exact analyser versions. A later pass can stamp them. | ||
| - **CodeQL runs the default suite, filtered in the comparator** (rather than a | ||
| single-query pack). Simpler and robust to suite/version drift; the filter keys | ||
| on the dispose/leak rule family. | ||
| - **One target, by hand.** Same discipline as mining: a deliberate spot-check, | ||
| not a crawler. Be a good citizen (shallow, read-only). | ||
| - **Agreement is necessary, not sufficient.** Two tools can share a blind spot. | ||
| The oracle raises confidence; it does not prove soundness (that is the Boogie/ | ||
| Dafny backend's job, still roadmap). |
Oops, something went wrong.
Oops, something went wrong.
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.