Skip to content

Rust MaD: add blanket-impl fallback for sink/source/barrier matching and model GlobalAlloc::realloc - #22442

Closed
hvitved with Copilot wants to merge 2 commits into
mainfrom
copilot/rust-implements-fallback
Closed

Rust MaD: add blanket-impl fallback for sink/source/barrier matching and model GlobalAlloc::realloc#22442
hvitved with Copilot wants to merge 2 commits into
mainfrom
copilot/rust-implements-fallback

Conversation

Copilot AI commented Aug 27, 2026

Copy link
Copy Markdown
Contributor

Blanket-impl trait methods now have canonical paths like <_ as Trait>::method, but Rust MaD sink/source/barrier matching only handled exact path equality. That caused blanket-impl calls (notably GlobalAlloc methods used by std::alloc::System) to miss modeled flow.

  • MaD matching parity for non-summary models

    • Extended FlowSourceFromModel, FlowSinkFromModel, FlowBarrierFromModel, and FlowBarrierGuardFromModel to support an implements fallback, mirroring summary-side behavior.
    • Fallback models are emitted as generated provenance to preserve precedence semantics against exact/manual models.
  • Dedup guard for concrete impls

    • Constrained fallback to blanket-impl canonical paths (<_ as ...>) so concrete impl methods do not match both exact and inherited paths.
  • Missing realloc sink model

    • Added core::alloc::global::GlobalAlloc::realloc sink entry in alloc.model.yml (Argument[2], alloc-size), enabling System.realloc(..) sink coverage.
  • Targeted MaD barrier coverage

    • Added trait-method blanket-impl cases in barrier library tests to exercise fallback behavior for barrierModel and barrierGuardModel paths as well.
// ModelsAsData.qll (fallback branch shape)
this.implements(f) and
not this.getCanonicalPath() = path and
this.getCanonicalPath().matches("<_ as %") and
provenance_ = "hq-generated"
# alloc.model.yml
- ["core::alloc::global::GlobalAlloc::realloc", "Argument[2]", "alloc-size", "manual"]

Co-authored-by: hvitved <3667920+hvitved@users.noreply.github.com>
Copilot AI changed the title [WIP] Fix MaD sink/source/barrier matching to include implements fallback Rust MaD: add blanket-impl fallback for sink/source/barrier matching and model GlobalAlloc::realloc Aug 27, 2026
Copilot AI requested a review from hvitved August 27, 2026 10:04
@hvitved hvitved closed this Aug 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants