Skip to content

Support verus! blocks in Rust #73

Closed

Description

@seebees

Summary

Tree-sitter does not expand macros, so the interior of an invocation-style macro is an opaque token tree: every function defined inside gets no node, no span, and no call edges. For some macros this hides the most important code in the project. Verus is the sharpest example: a verification language for Rust where executable code plus specifications (requires/ensures, spec fn, proof fn) live inside a verus! { ... } proc-macro in ordinary .rs files. In a verified Rust codebase, the verified core — the most security-critical code — is exactly the code missing from the graph.

Tree-sitter has a first-class mechanism for this situation: Parser.included_ranges, designed for embedded languages (the canonical case is JavaScript inside HTML <script> regions). This issue proposes using it for macro interiors.

Proposed feature

A two-pass parse for configured (host language, macro name, secondary grammar) triples:

  1. The host grammar parses the file normally. Configured macro invocations (e.g. verus!) come back as token trees with exact spans.
  2. Those spans become included_ranges for a second parse with the secondary grammar (e.g. tree-sitter-verus, a tree-sitter-rust fork with Python bindings).
  3. Because included_ranges reports node spans in whole-file coordinates, nodes and edges from both passes drop into one CodeGraph with no coordinate translation.

Each grammar stays on home turf: plain Rust is parsed by the grammar that will never drift from Rust; Verus interiors by the grammar built for them. Neither grammar needs to be a superset of the other.

Implementation notes: if the macro interior doesn't parse cleanly on its own, the range can include the macro invocation itself rather than just its interior. Calls from interior functions to host-pass functions resolve at graph level, the same way cross-file calls do today. Grammar distribution has precedent in tree_sitter_custom/ and the separate tree-sitter-sql wheel; configuration could follow the shape of .trailmark/links.toml — a repo-local file declaring macro-name → grammar mappings.

The mechanism is general — any embedded DSL in any host language (SQL in string-building macros, template DSLs, other verifier macros) — with Verus as the concrete first case. Since tree-sitter-verus forks tree-sitter-rust, plain-Rust node types inside the interior (function_item, impl_item, ...) keep their names, so the existing Rust extraction logic should apply to the secondary tree with minimal modification. Verus-specific constructs (spec fn / proof fn, requires/ensures) could later map to node metadata — a separable follow-on; the base feature already yields nodes, spans, and call edges for everything inside verus! blocks.

Motivation / use case

I want to join trailmark's code graph with Duvet requirement-traceability data: spec citations anchored at (file, line-range), resolved to function nodes by interval containment. On verified Rust codebases, every citation inside a verus! block currently fails to resolve because no function node's span contains it. The same applies to any line-anchored external finding (SARIF included), and reachability queries (attack_surface(), entrypoint_paths_to()) silently stop at the macro boundary.

Acceptance test

Parse a file containing (a) a plain Rust function, (b) a function under an attribute macro, (c) a function inside verus! { ... } that calls (a). All three appear as function nodes with correct whole-file spans; the call edge from (c) to (a) resolves.

Activity

  1. dzmitry-lahoda commented on Sep 12, 2026

    @dzmitry-lahoda
    Contributor

    Yes, same for me. trailmark parses only 25% of our solution, rest chokes on macroses.

    So could solution be based on rustc internals (same as used by cargo expand macro?) or RustaAnalyser?

  2. tob-scott-a commented on Sep 14, 2026

    @tob-scott-a
    Collaborator

    Does #76 solve the issue for you both? @seebees @dzmitry-lahoda

  3. dzmitry-lahoda commented on Sep 22, 2026

    @dzmitry-lahoda
    Contributor

    I have other macros failing too. So not sure what to do here. I was thinking to expand whole workspace before giving it to trailmark.

  4. tob-scott-a commented on Sep 22, 2026

    @tob-scott-a
    Collaborator

    That might work. Can you (or Claude/Codex) give me a list of macros that are failing? I want to try a few different approaches to ensure we're covering them all.

  5. tob-scott-a commented on Sep 22, 2026

    @tob-scott-a
    Collaborator

    Does #73 solve the issue for you both?

    I just realized I created a self-referencing comment earlier. The link has been corrected to #76.

  6. dzmitry-lahoda commented on Sep 25, 2026

    @dzmitry-lahoda
    Contributor
    1. at some point of time ago i for sure saw macro issues - so do not recall if that was AI output
    2. i run now trailmark analyze --language rust /Users/dz/overlay/github.com/n1xyz/proton/nord > out.json, some macros are fine for sure.
    3. i see that our HTTP API is found, even so we use non conventional axiom API entries (we use typed aide).
    4. i see proxy.unresolved 20K+ items in output.

    specifically,

    it fails on bon:

          "id": "proxy.unresolved:MarketBase::builder__.size_decimals_market.size_decimals__.market_type_market.market_type__.price_decimals",
          "name": "MarketBase::builder()\n                        .size_decimals(market.size_decimals)\n                        .market_type(market.market_type)\n                        .price_decimals",
          "kind": "proxy",
          "location": {
    

    not really care - FEAT: need to ignore some crates/macros.

    I see a lot for TryFrom proxy.unresolved - not sure if related, but we use derive_more and educe macros.

    so some may be manually implemented.

    Seems I have question not related to versus! issues - but how handle proxy.unresolved?'

  7. dzmitry-lahoda commented on Oct 15, 2026

    @dzmitry-lahoda
    Contributor

    We have next. Not sure if it is bad for analysis or not? Would returned result type and calls on it be found?

    ===

    Typical unresolved calls in Nord are:

    Pattern Examples
    Standard Rust methods .unwrap(), .expect(), .clone(), .len()
    Iterator operations .map(), .iter(), .collect()
    Trait conversions .into(), .try_into(), TokenId::try_from()
    External library functions prost_build::Config::new(), UdpSocket::bind()
    Generated builders Action::builder().timestamp(...)
    Local methods needing receiver types engine.execute(), self.side.converse()
    Enum constructors treated as calls ActionKind::Deposit, Ok(...), Err(...)

    For scale, 2,797 proxy nodes end in unwrap, and 1,042 end in expect.

    Trailmark parses syntax without Rust compiler type resolution or macro expansion, so many ordinary, valid calls remain unresolved

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions