Skip to content

Support verus! blocks in Rust #73

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.

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