Validation of Witnesses with Ghosts#2072
Draft
michael-schwarz wants to merge 180 commits into
Draft
Conversation
…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
Ghost examples
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| let owner = man.ask (Queries.Owner var) in | ||
| let phase_ghost = is_phase_ghost man var in | ||
| let may_advance = phase_ghost && possible_advances_here local var <> [] in | ||
| M.tracel "phaseGhost" "Ghost %a is %sa phase ghost, has owner %a and may %s be advanced here" (* nosemgrep: trace-not-in-tracing *) |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Remaining issues:
atomicprivatizations to check soundness