trailofbits / trailofbits/trailmark
Support verus! blocks in Rust
Nobody has claimed this yet.
- Dominant language
- C
- Stars
- 487
- Forks
- 30
- PR merge metrics
- No merged PRs in 30d
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.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by examining the existing grammar distribution precedent in tree_sitter_custom/ and the repository configuration shape in .trailmark/links.toml. Implement the configured two-pass parsing flow for host macros and secondary grammars, then validate it with the acceptance case: plain Rust, an attribute-macro function, and a function inside verus! with correct whole-file spans and a resolved call edge.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- python, rust
- Domain
- compilers, devtools
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Active
- Clarity
- Mostly clear
- Newbie friendliness
- 38/100