Repository navigation
Support verus! blocks in Rust #73
Description
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:
- The host grammar parses the file normally. Configured macro invocations (e.g.
verus!) come back as token trees with exact spans. - Those spans become
included_rangesfor a second parse with the secondary grammar (e.g. tree-sitter-verus, a tree-sitter-rust fork with Python bindings). - Because
included_rangesreports node spans in whole-file coordinates, nodes and edges from both passes drop into oneCodeGraphwith 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
dzmitry-lahoda commentedon Sep 12, 2026
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?
tob-scott-a commentedon Sep 14, 2026
Does #76 solve the issue for you both? @seebees @dzmitry-lahoda
dzmitry-lahoda commentedon Sep 22, 2026
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.
tob-scott-a commentedon Sep 22, 2026
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.
tob-scott-a commentedon Sep 22, 2026
I just realized I created a self-referencing comment earlier. The link has been corrected to #76.
dzmitry-lahoda commentedon Sep 25, 2026
trailmark analyze --language rust /Users/dz/overlay/github.com/n1xyz/proton/nord > out.json, some macros are fine for sure.proxy.unresolved20K+ items in output.specifically,
it fails on
bon: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 handleproxy.unresolved?'dzmitry-lahoda commentedon Oct 15, 2026
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:
For scale, 2,797 proxy nodes end in
unwrap, and 1,042 end inexpect.Trailmark parses syntax without Rust compiler type resolution or macro expansion, so many ordinary, valid calls remain unresolved