Validation of Witnesses with Ghosts by michael-schwarz · Pull Request #2072 · goblint/analyzer

michael-schwarz · 2026-07-10T10:31:39Z

Remaining issues:

Prevent making things atomic that are not actually atomic in the code by surrounding it with ghosts updates
Carefully review placement code
Get back the OS X CI

Postponed for further PRs:

Generalize pattern
Delay publication inside atomic blocks

…init (#1998) * Reject witness on duplicate ghost variable declarations * Fix ghost global initinfo construction * Fix Formatcil.cType partial application compilation error Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/28884c57-57a6-4417-9509-264ab8dba17f Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Add cram test for ghost variable injection from YAML witness Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/9da67fc2-69ae-48ea-904b-4e7ae68c4735 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Move YamlWitness.init() before justcil check and update cram test to verify CIL output Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/86acd990-3af7-4033-b7b4-95622c8d6391 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Fix cram test: match actual CIL printer output with extra spaces around initializer Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/6246b7e7-f321-48b7-83ce-3fb435a854f5 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Initial plan * Implement ghost update instrumentation in yamlWitness.ml init() Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/21e7ba62-2fe5-46fc-8eae-445d9d9c6580 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Fix Hashtbl.t type: add missing string key argument Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/203eec74-e6e4-49c5-8eac-f64d219b9262 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Check for existing __VERIFIER_atomic_begin/end before creating varinfos Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/769cff72-d99d-4307-a362-bf6f91c1dd2d Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Warn when a ghost update could not be placed in the CIL AST Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/885e41d9-75d3-4c35-a63e-9c33fa26b0d7 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Add regression tests and prevent successful validation for unplaced ghost updates Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/3c1ba5d9-eb7a-44e7-8949-62deba46d000 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Build set of ghost vars during yamlWitness init * Fix regression test: remove justcil from unplaced ghost update warning test Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/47fdf870-86a7-4795-9f3c-1cd7ce2166c8 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Fix: move has_unplaced_ghost_updates declaration before init() to fix unbound value error Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/b5589f8b-23a0-4723-bb0b-29d01fe34c54 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Add extra ghosts * Fix: emit unplaced ghost update warnings from validate() not init() (should_warn is false during init) Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/82cbdf26-d090-4fa5-9c27-06f30c6e112e Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Ignore codex file * Remove cop out when ghost instrumentation is encountered --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>

* Detect if accesses come from different threads * Add phase ghosts to `goblint_lib.ml` * More documentation for extraGhosts * Start second part of phaseGhost detection * Progress on `phaseGhost` detection * Test `phaseGhost` detection * Uniqueness + Example * Turn into cram test * Fix verifier atomic type * Reuse Locator

…2005) * Initial plan * fix(mcp): apply sync transfer to split paths created during sync Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/351c80a9-dc9f-4603-a357-a186a213399d Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * refactor(mcp): clarify sync split-transform flag naming Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/351c80a9-dc9f-4603-a357-a186a213399d Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * style(mcp): simplify sync helper parameter name Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/351c80a9-dc9f-4603-a357-a186a213399d Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * fix(constraints): apply assign to sync-split states before join Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/9fbe3c8e-0b5b-4c06-af38-fee7944ab663 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * refactor(constraints): replay transfer over sync-split states for all tfs Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/f5a74b34-4b24-4b72-87d1-d3dfb162caf2 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * refactor(constraints): share split-replay helper with call transfer Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/f5a74b34-4b24-4b72-87d1-d3dfb162caf2 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * refactor(constraints): clarify split replay helpers for generic and call tf Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/f5a74b34-4b24-4b72-87d1-d3dfb162caf2 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

Ghost Phase Path-Sensitivity

michael-schwarz · 2026-08-03T04:34:24Z

@copilot: Review, but ignore the contents of the folders under tests/.

Copilot · 2026-08-03T04:38:41Z

@copilot: Review, but ignore the contents of the folders under tests/.

Reviewed the PR while excluding all tests/ folders and fixed two non-test issues in commit 15b13d3e9: guarded TIDs.elements against Top in phaseGhost queries and restored full-path witness locator matching to avoid basename collisions.

michael-schwarz · 2026-08-03T06:02:09Z

@copilot: Add an option to use the lenient location matching that was removed in the last commit.

Copilot · 2026-08-03T06:04:33Z

@copilot: Add an option to use the lenient location matching that was removed in the last commit.

Implemented in commit 704e566: added opt-in witness.yaml.lenient-location-matching to restore basename-based location matching behavior when needed, while keeping full-path matching as the default.

This reverts commit 15b13d3.

michael-schwarz · 2026-10-12T05:13:16Z

Given the underlying work has now been conditionally accepted, I think it would be nice to move towards merging this. This could be a potential SV-COMP '28 Goblint Validator paper.

@sim642: Would you be open to reviewing this PR? I think especially the things that touch the constraint generation, it would be very helpful to have someone else with framework experience taking a look.

sim642 · 2026-10-12T07:17:05Z

Are you thinking of getting this in for SV-COMP 2027 or is it not in such a rush?

michael-schwarz · 2026-10-12T07:21:10Z

I don't think we need to get it done before SV-COMP '27, especially since there are no tools except Goblint that can currently produce such a witness.

Once the paper is out, I will write to the mailing list to advertise this support, and then perhaps in 2028 people will actually produce these witnesses.

michael-schwarz and others added 30 commits March 3, 2026 11:08

Add test

b1f548d

Merge branch 'master' into ghosts

ad88403

Fix a reference

ba3ac74

Merge branch 'ghosts' into phase-digest

031e77b

Phase ghost split

c437774

Emit eval query, add cram test

6039e7d

Document PhaseGhostSplit

f275fa3

Record phase on return, use in join

ac12893

Add TODO

2691423

Add phaseDigest query

120391a

Add phaseChange event

a00b85e

Add ghost variants of privatizations

4c821de

Add flag to indicate wether action on phaseChange is needed

4e81956

BasePriv: Add phaseChange transfer function

d7abdc7

Record how the phase changed in event

c9747d4

Emit PhaseChange after Deadcode

b7ce15c

Allow accessing raw digest-less globals

a06e4cb

Progress

cdb91bb

Progress

bcf8331

Progress

d7b7ff6

Add MHP TODO

cccc320

Update test

2b50644

Add test for rejecting witness if ghost hypothesis is not confirmed

ebc47c8

Get rid of Object.magic

fad9199

Merge pull request #2007 from goblint/phase-digest

9f052a7

Ghost Phase Path-Sensitivity

Clarify propagation comment

1fc5dbc

michael-schwarz unassigned sim642 Jul 29, 2026

michael-schwarz requested review from Ang9876 and sim642 July 29, 2026 14:29

Copilot started work on behalf of michael-schwarz August 3, 2026 04:35 View session

Fix phase ghost top handling and locator file matching

15b13d3

Copilot finished work on behalf of michael-schwarz August 3, 2026 04:39

Copilot started work on behalf of michael-schwarz August 3, 2026 06:02 View session

Add optional lenient witness location matching

704e566

Copilot finished work on behalf of michael-schwarz August 3, 2026 06:05

michael-schwarz added 11 commits August 3, 2026 14:08

Revert "Fix phase ghost top handling and locator file matching"

ea63614

This reverts commit 15b13d3.

Handle top

3d487af

Fix issue with nested atomicity mutexes

8657c56

Merge branch 'master' into ghosts

be24b1d

Produce run-time stats

7d08dc2

Table 3

dc9a671

Rm files belonging to ultimate workaround

d507c91

19 reduce ultimate specific annotations

3b04e23

Merge branch 'master' into ghosts

b317a7c

Adapt location matching to new CIL version, warn deterministic

6eff8a4

19/19: inc-split milder

54b40ba

michael-schwarz and others added 2 commits October 12, 2026 17:45

Add task with original constants

e07a6f7

Switch over MutexGhost analysis

0e4e6c0

sim642 added this to the SV-COMP 2028 milestone Oct 13, 2026

Navigation Menu

Repository navigation

Validation of Witnesses with Ghosts - #2072

Validation of Witnesses with Ghosts#2072
michael-schwarz wants to merge 226 commits into
masterfrom
ghosts

michael-schwarz commented Jul 10, 2026 •

edited

Loading

Uh oh!

michael-schwarz commented Aug 3, 2026

Uh oh!

Copilot AI commented Aug 3, 2026

Uh oh!

michael-schwarz commented Aug 3, 2026

Uh oh!

Copilot AI commented Aug 3, 2026

Uh oh!

michael-schwarz commented Oct 12, 2026

Uh oh!

sim642 commented Oct 12, 2026

Uh oh!

michael-schwarz commented Oct 12, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

michael-schwarz commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michael-schwarz commented Aug 3, 2026

Uh oh!

Copilot AI commented Aug 3, 2026

Uh oh!

michael-schwarz commented Aug 3, 2026

Uh oh!

Copilot AI commented Aug 3, 2026

Uh oh!

michael-schwarz commented Oct 12, 2026

Uh oh!

sim642 commented Oct 12, 2026

Uh oh!

michael-schwarz commented Oct 12, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

michael-schwarz commented Jul 10, 2026 •

edited

Loading